Estimation.ATT.Score

lemma H_ε_overlap_P_Z (S : TreatedEstimationSystem P γ) {ε : ℝ} {η : TreatedNuisanceVec γ} (hη : η ∈ H_ε S ε) : ∀ᵐ z ∂S.P_Z, η.e_fn (projX z) ≤ 1 - ε := by open Causalean.Estimation.ATE.BackdoorEstimationSystem in have hset : MeasurableSet {x : γ | η.e_fn x ≤ 1 - ε} := by exact measurableSet_Iic.preimage η.e_meas have hx : ∀ᵐ x ∂S.P_X, η.e_fn x ≤ 1 - ε := hη.1 rw [← TreatedEstimationSystem.P_Z_map_projX_eq_P_X S] at hx have hproj : Measurable (fun z : γ × Bool × ℝ => projX z) := by simpa [projX] using (measurable_fst : Measurable (fun z : γ × Bool × ℝ => z.1)) exact (MeasureTheory.ae_map_iff hproj.aemeasurable hset).mp hx

theorem aipw_score_diff_isLittleOp_one_ATT (S : TreatedEstimationSystem P γ) {ε : ℝ} (h_overlap : S.OneSidedOverlap ε) (hη₀_mem : S.η₀ ∈ H_ε S ε) (h_e_lb : ∀ x, 0 ≤ S.e_val x) (hA : S.toPOBackdoorSystem.ATTAssumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_y0_2 : Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ) (η_hat : ℕ → P.Ω → TreatedNuisanceVec γ) (h_in_Hε : ∀ n ω, η_hat n ω ∈ H_ε S ε) (h_e_lb_hat : ∀ n ω x, 0 ≤ (η_hat n ω).e_fn x) (h_mu_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X) (h_e_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X) (h_mu_diff : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_e_diff : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) : IsLittleOp (fun n ω => (eLpNorm (fun z => aipwMomentATTFunctional (η_hat n ω) z S.θ₀ - aipwMomentATTFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by classical rcases h_overlap with ⟨hε_pos, hε_half, hprop⟩ let R : (γ × Bool × ℝ) → ℝ := fun z => |projY z - S.μ₀_val (projX z)| let dμZ : ℕ → P.Ω → (γ × Bool × ℝ) → ℝ := fun n ω z => (η_hat n ω).μ₀_fn (projX z) - S.μ₀_val (projX z) let deZ : ℕ → P.Ω → (γ × Bool × ℝ) → ℝ := fun n ω z => (η_hat n ω).e_fn (projX z) - S.e_val (projX z) let cross : ℕ → P.Ω → (γ × Bool × ℝ) → ℝ := fun n ω z => R z * |deZ n ω z| let score : ℕ → P.Ω → (γ × Bool × ℝ) → ℝ := fun n ω z => aipwMomentATTFunctional (η_hat n ω) z S.θ₀ - aipwMomentATTFunctional S.η₀ z S.θ₀ have hR_meas : Measurable R := by simpa [R] using yMuVal_residual_meas_ATT S have hR_nonneg : ∀ z, 0 ≤ R z := by intro z dsimp [R] positivity have hR_memLp : MemLp R 2 S.P_Z := by simpa [R] using yMuVal_residual_memLp_ATT S hA h_y2 h_y0_2 have hdμZ_memLp : ∀ n ω, MemLp (dμZ n ω) 2 S.P_Z := by intro n ω have hmap : MemLp (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 (S.P_Z.map (fun z : γ × Bool × ℝ => z.1)) := by simpa [TreatedEstimationSystem.P_Z_map_projX_eq_P_X S] using h_mu_memLp n ω have hproj_ae : AEMeasurable (fun z : γ × Bool × ℝ => z.1) S.P_Z := measurable_fst.aemeasurable exact (memLp_map_measure_iff hmap.aestronglyMeasurable hproj_ae).1 hmap have hdeZ_memLp : ∀ n ω, MemLp (deZ n ω) 2 S.P_Z := by intro n ω have hmap : MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 (S.P_Z.map (fun z : γ × Bool × ℝ => z.1)) := by simpa [TreatedEstimationSystem.P_Z_map_projX_eq_P_X S] using h_e_memLp n ω have hproj_ae : AEMeasurable (fun z : γ × Bool × ℝ => z.1) S.P_Z := measurable_fst.aemeasurable exact (memLp_map_measure_iff hmap.aestronglyMeasurable hproj_ae).1 hmap have hdeZ_bdd : ∀ n ω, ∀ᵐ z ∂S.P_Z, |deZ n ω z| ≤ 1 := by intro n ω filter_upwards [H_ε_overlap_P_Z S (h_in_Hε n ω), H_ε_overlap_P_Z S hη₀_mem] with z hη_le_M hS_le_M_raw have hη_nonneg : 0 ≤ (η_hat n ω).e_fn (projX z) := h_e_lb_hat n ω (projX z) have hS_nonneg : 0 ≤ S.e_val (projX z) := h_e_lb (projX z) have hS_le_M : S.e_val (projX z) ≤ 1 - ε := by simpa [TreatedEstimationSystem.η₀] using hS_le_M_raw have hM_le_one : 1 - ε ≤ 1 := by linarith dsimp [deZ] rw [abs_le] constructor · linarith · linarith have hcross_rate : IsLittleOp (fun n ω => (eLpNorm (cross n ω) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by simpa [cross, R, deZ] using residual_mul_e_error_isLittleOp_one_ATT S ⟨hε_pos, hε_half, hprop⟩ hη₀_mem h_e_lb hA h_y2 h_y0_2 η_hat h_in_Hε h_e_lb_hat h_e_memLp h_e_diff have hμZ_rate : IsLittleOp (fun n ω => (eLpNorm (dμZ n ω) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by have heq : (fun n ω => (eLpNorm (dμZ n ω) 2 S.P_Z).toReal) = (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal) := by funext n funext ω dsimp [dμZ] exact congrArg toReal (eLpNorm_comp_projX_eq_ATT (S := S) (f := fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) (h_mu_memLp n ω).aestronglyMeasurable) rw [heq] exact h_mu_diff have hsum_rate : IsLittleOp (fun n ω => (eLpNorm (dμZ n ω) 2 S.P_Z).toReal + (eLpNorm (cross n ω) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by exact IsLittleOp.add_one hμZ_rate hcross_rate have hK_pos : 0 < K_AIPW_ATT ε := lt_of_lt_of_le zero_lt_one (K_AIPW_ATT_one_le hε_pos) refine IsLittleOp.of_abs_le_const_mul_one (C := K_AIPW_ATT ε) hK_pos hsum_rate ?_ intro n ω have hpointwise : ∀ᵐ z ∂S.P_Z, |score n ω z| ≤ K_AIPW_ATT ε * (|dμZ n ω z| + cross n ω z) := by simpa [score, dμZ, cross, R, deZ, mul_add, mul_assoc, add_comm, add_left_comm, add_assoc] using aipw_score_lipschitz_ATT S ⟨hε_pos, hε_half, hprop⟩ hη₀_mem (η_hat n ω) (h_in_Hε n ω) let upper : (γ × Bool × ℝ) → ℝ := fun z => K_AIPW_ATT ε * (|dμZ n ω z| + cross n ω z) have hcross_memLp : MemLp (cross n ω) 2 S.P_Z := by have hcross_meas : Measurable (cross n ω) := by have hde_meas : Measurable (deZ n ω) := by have hx : Measurable (fun z : γ × Bool × ℝ => projX z) := by simpa [projX] using (measurable_fst : Measurable (fun z : γ × Bool × ℝ => z.1)) exact ((η_hat n ω).e_meas.comp hx).sub (S.e_meas.comp hx) exact hR_meas.mul hde_meas.norm refine hR_memLp.mono' hcross_meas.aestronglyMeasurable ?_ filter_upwards [hdeZ_bdd n ω] with z hdez_le have hRz : 0 ≤ R z := hR_nonneg z dsimp [cross] rw [abs_mul, abs_of_nonneg hRz, abs_of_nonneg (abs_nonneg _)] exact mul_le_of_le_one_right hRz hdez_le have hupper_memLp : MemLp upper 2 S.P_Z := by have hsum : MemLp (fun z => |dμZ n ω z| + cross n ω z) 2 S.P_Z := by have hμ : MemLp (fun z => |dμZ n ω z|) 2 S.P_Z := by simpa [Real.norm_eq_abs] using (hdμZ_memLp n ω).norm exact hμ.add hcross_memLp exact hsum.const_smul (K_AIPW_ATT ε) have hmono : (eLpNorm (score n ω) 2 S.P_Z).toReal ≤ (eLpNorm upper 2 S.P_Z).toReal := by have hle_enn : eLpNorm (score n ω) 2 S.P_Z ≤ eLpNorm upper 2 S.P_Z := eLpNorm_mono_ae_real (by filter_upwards [hpointwise] with z hz simpa [Real.norm_eq_abs, upper] using hz) exact ENNReal.toReal_mono hupper_memLp.eLpNorm_ne_top hle_enn have hupper_bound : (eLpNorm upper 2 S.P_Z).toReal ≤ K_AIPW_ATT ε * ((eLpNorm (dμZ n ω) 2 S.P_Z).toReal + (eLpNorm (cross n ω) 2 S.P_Z).toReal) := by let total : (γ × Bool × ℝ) → ℝ := fun z => |dμZ n ω z| + cross n ω z have htotal_memLp : MemLp total 2 S.P_Z := by have hμ : MemLp (fun z => |dμZ n ω z|) 2 S.P_Z := by simpa [Real.norm_eq_abs] using (hdμZ_memLp n ω).norm exact hμ.add hcross_memLp have hupper_eq : upper = K_AIPW_ATT ε • total := by funext z simp [upper, total, smul_eq_mul] rw [hupper_eq] rw [toReal_eLpNorm (htotal_memLp.const_smul (K_AIPW_ATT ε)).aestronglyMeasurable] rw [lpNorm_const_smul] have hcoef : (↑‖K_AIPW_ATT ε‖₊ : ℝ) = K_AIPW_ATT ε := by simp [Real.norm_eq_abs, abs_of_pos hK_pos] rw [hcoef] gcongr have htri : lpNorm total 2 S.P_Z ≤ lpNorm (fun z => |dμZ n ω z|) 2 S.P_Z + lpNorm (cross n ω) 2 S.P_Z := by have htotal_eq : total = (fun z => |dμZ n ω z|) + cross n ω := by funext z simp [total, Pi.add_apply] rw [htotal_eq] have hμ : MemLp (fun z => |dμZ n ω z|) 2 S.P_Z := by simpa [Real.norm_eq_abs] using (hdμZ_memLp n ω).norm exact lpNorm_add_le (f := fun z => |dμZ n ω z|) (g := cross n ω) (μ := S.P_Z) hμ (by norm_num : (1 : ENNReal) ≤ 2) have hnormμ : lpNorm (fun z => |dμZ n ω z|) 2 S.P_Z = (eLpNorm (dμZ n ω) 2 S.P_Z).toReal := by rw [lpNorm_fun_abs (hdμZ_memLp n ω).aestronglyMeasurable] rw [← toReal_eLpNorm (hdμZ_memLp n ω).aestronglyMeasurable] have hnormC : lpNorm (cross n ω) 2 S.P_Z = (eLpNorm (cross n ω) 2 S.P_Z).toReal := by rw [← toReal_eLpNorm hcross_memLp.aestronglyMeasurable] linarith calc |(eLpNorm (score n ω) 2 S.P_Z).toReal| = (eLpNorm (score n ω) 2 S.P_Z).toReal := by rw [abs_of_nonneg ENNReal.toReal_nonneg] _ ≤ (eLpNorm upper 2 S.P_Z).toReal := hmono _ ≤ K_AIPW_ATT ε * ((eLpNorm (dμZ n ω) 2 S.P_Z).toReal + (eLpNorm (cross n ω) 2 S.P_Z).toReal) := hupper_bound _ = K_AIPW_ATT ε * |(eLpNorm (dμZ n ω) 2 S.P_Z).toReal + (eLpNorm (cross n ω) 2 S.P_Z).toReal| := by rw [abs_of_nonneg] positivity

-- Outline: mirror `aipw_finite_var` from `Estimation/ATE/Score/FiniteVar.lean`. -- Steps: (i) measurability of the moment; (ii) `Y, μ₀ ∈ L²` via -- `memLp_two_iff_integrable_sq` and `MemLp.condExp` on `μ[Y(0)|σX]`; -- (iii) `(1−A)·e/(1−e)` is `L^∞` from `e_val ≤ 1−ε`; (iv) `A` is `L^∞`; -- (v) `MemLp.mul`-products; (vi) sum to get the moment in `L²`; (vii) -- transfer from `P.μ` to `P_Z` via `memLp_map_measure_iff`. theorem aipw_finite_var_ATT (S : TreatedEstimationSystem P γ) {ε : ℝ} (h_overlap : S.OneSidedOverlap ε) (hA : S.toPOBackdoorSystem.ATTAssumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_y0_2 : Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ) : Integrable (fun z => (aipwMomentATT z S.μ₀_val S.e_val S.θ₀) ^ 2) S.P_Z := by have hmoment_meas : Measurable (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) := by simpa [aipwMomentATTFunctional, η₀] using (measurable_aipwMomentATTFunctional (η := S.η₀) (θ := S.θ₀)) have hY_L2 : MemLp S.toPOBackdoorSystem.factualY 2 P.μ := by exact (memLp_two_iff_integrable_sq S.toPOBackdoorSystem.measurable_factualY.aestronglyMeasurable).2 h_y2 have hμ₀_L2 : MemLp (fun ω => S.μ₀_val (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := by have hY0_L2 : MemLp (S.toPOBackdoorSystem.YofD false) 2 P.μ := by exact (memLp_two_iff_integrable_sq (S.toPOBackdoorSystem.measurable_YofD false).aestronglyMeasurable).2 h_y0_2 have hcond_L2 : MemLp (P.μ[S.toPOBackdoorSystem.YofD false | S.toPOBackdoorSystem.sigmaX]) 2 P.μ := hY0_L2.condExp one_le_two exact hcond_L2.ae_eq (S.μ₀_compat hA) have hindA_meas : Measurable (fun ω => indA (S.factualZ ω)) := by simp only [indA, ATE.BackdoorEstimationSystem.projA, TreatedEstimationSystem.factualZ] exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp S.toPOBackdoorSystem.measurable_factualD have hA_bound : ∀ᵐ ω ∂P.μ, ‖indA (S.factualZ ω)‖ ≤ (1 : ℝ) := by filter_upwards with ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · simp [TreatedEstimationSystem.factualZ, indA, ATE.BackdoorEstimationSystem.projA, hD] · simp [TreatedEstimationSystem.factualZ, indA, ATE.BackdoorEstimationSystem.projA, hD] have hA_Linf : MemLp (fun ω => indA (S.factualZ ω)) ⊤ P.μ := by exact MemLp.of_bound hindA_meas.aestronglyMeasurable (1 : ℝ) hA_bound have he_nonneg : ∀ᵐ ω ∂P.μ, 0 ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) := by filter_upwards [S.propScore_true_nonneg_ae, S.e_compat] with ω hnonneg hcomp simpa [hcomp] using hnonneg have he_upper : ∀ᵐ ω ∂P.μ, S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by filter_upwards [h_overlap.2.2, S.e_compat] with ω hover hcomp simpa [hcomp] using hover have hw_false_bound : ∀ᵐ ω ∂P.μ, ‖(1 - indA (S.factualZ ω)) * (S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)))‖ ≤ ε⁻¹ := by filter_upwards [he_nonneg, he_upper] with ω hnonneg hupper by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr h_overlap.1.le simpa [TreatedEstimationSystem.factualZ, indA, ATE.BackdoorEstimationSystem.projA, hD] using hεinv_nonneg · have hden : ε ≤ 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) := by linarith have hdenpos : 0 < 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) := lt_of_lt_of_le h_overlap.1 hden have hle_inv : (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hdenpos h_overlap.1).2 hden have he_le_one : S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 := by linarith have hratio_nonneg : 0 ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) := div_nonneg hnonneg hdenpos.le have hratio_le : S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) ≤ ε⁻¹ := by calc S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) = S.e_val (S.toPOBackdoorSystem.factualX ω) * (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))⁻¹ := by rw [div_eq_mul_inv] _ ≤ 1 * ε⁻¹ := by exact mul_le_mul he_le_one hle_inv (inv_nonneg.mpr hdenpos.le) zero_le_one _ = ε⁻¹ := one_mul _ have hnorm_eq : ‖(1 - indA (S.factualZ ω)) * (S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)))‖ = S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) := by have hind_eq : indA (S.factualZ ω) = 0 := by simp only [TreatedEstimationSystem.factualZ, indA, ATE.BackdoorEstimationSystem.projA, hD] rfl rw [hind_eq] change ‖(1 - 0) * (S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)))‖ = S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) rw [sub_zero, one_mul, Real.norm_eq_abs, abs_of_nonneg hratio_nonneg] rw [hnorm_eq] exact hratio_le have hw_false_Linf : MemLp (fun ω => (1 - indA (S.factualZ ω)) * (S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)))) ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ hw_false_bound apply Measurable.aestronglyMeasurable exact (measurable_const.sub hindA_meas).mul ((S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX).div (measurable_const.sub (S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX))) have hterm_true_L2 : MemLp (fun ω => indA (S.factualZ ω) * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω))) 2 P.μ := by exact MemLp.mul' (p := ⊤) (q := 2) (r := 2) (hY_L2.sub hμ₀_L2) hA_Linf have hterm_false_L2 : MemLp (fun ω => ((1 - indA (S.factualZ ω)) * (S.e_val (S.toPOBackdoorSystem.factualX ω) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)))) * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω))) 2 P.μ := by exact MemLp.mul' (p := ⊤) (q := 2) (r := 2) (hY_L2.sub hμ₀_L2) hw_false_Linf have htheta_L2 : MemLp (fun ω => indA (S.factualZ ω) * S.θ₀) 2 P.μ := by exact MemLp.mul' (p := ⊤) (q := 2) (r := 2) (memLp_const (α := P.Ω) S.θ₀) hA_Linf have hmoment_comp_L2 : MemLp (fun ω => aipwMomentATT (S.factualZ ω) S.μ₀_val S.e_val S.θ₀) 2 P.μ := by have hsum_L2 := (hterm_true_L2.sub hterm_false_L2).sub htheta_L2 simp only [aipwMomentATT, TreatedEstimationSystem.factualZ, ATE.BackdoorEstimationSystem.projX, ATE.BackdoorEstimationSystem.projY] exact hsum_L2 have hmoment_L2 : MemLp (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) 2 S.P_Z := by rw [TreatedEstimationSystem.P_Z] exact (memLp_map_measure_iff hmoment_meas.aestronglyMeasurable S.measurable_factualZ.aemeasurable).2 hmoment_comp_L2 exact hmoment_L2.integrable_sq

theorem aipw_mean_zero_ATT (S : TreatedEstimationSystem P γ) (hA : S.toPOBackdoorSystem.ATTAssumptions) (hπ_pos : 0 < S.π_val) (hIPW : Integrable (fun ω => (1 - S.toPOBackdoorSystem.dVar.indicator true ω) * (S.toPOBackdoorSystem.propScore true ω / (1 - S.toPOBackdoorSystem.propScore true ω)) * (S.toPOBackdoorSystem.factualY ω - S.toPOBackdoorSystem.adjustedCE false ω)) P.μ) : ∫ z, aipwMomentATT z S.μ₀_val S.e_val S.θ₀ ∂(S.P_Z) = 0 := by let A : P.Ω → ℝ := fun ω => S.toPOBackdoorSystem.dVar.indicator true ω let R : P.Ω → ℝ := fun ω => S.toPOBackdoorSystem.factualY ω - S.toPOBackdoorSystem.adjustedCE false ω let W : P.Ω → ℝ := fun ω => S.toPOBackdoorSystem.propScore true ω / (1 - S.toPOBackdoorSystem.propScore true ω) let N : ℝ := ∫ ω, A ω * R ω - (1 - A ω) * W ω * R ω ∂P.μ have hadj : S.θ₀ = N / S.π_val := by have h := S.toPOBackdoorSystem.adjustedATT_eq_aipwForm hA hIPW simpa [TreatedEstimationSystem.θ₀, TreatedEstimationSystem.π_val, N, A, R, W] using h have hπ_ne : S.π_val ≠ 0 := ne_of_gt hπ_pos have hN_eq : N = S.π_val * S.θ₀ := by calc N = S.π_val * (N / S.π_val) := by field_simp [hπ_ne] _ = S.π_val * S.θ₀ := by rw [← hadj] have htreated_int : Integrable (fun ω => A ω * R ω) P.μ := by have hY_int : Integrable S.toPOBackdoorSystem.factualY P.μ := S.toPOBackdoorSystem.integrable_factualY_of_consistency hA.consistency hA.integrable_Y1 hA.integrable_Y0 have hYind_int : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator true ω * S.toPOBackdoorSystem.factualY ω) P.μ := by have h := S.toPOBackdoorSystem.dVar.integrable_mul_indicator true (measurableSet_singleton true) hY_int exact h.congr (Filter.Eventually.of_forall (fun ω => by ring)) have hAdjind_int : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator true ω * S.toPOBackdoorSystem.adjustedCE false ω) P.μ := by have h := S.toPOBackdoorSystem.dVar.integrable_mul_indicator true (measurableSet_singleton true) (integrable_adjustedCE S hA) exact h.congr (Filter.Eventually.of_forall (fun ω => by ring)) have hsub := hYind_int.sub hAdjind_int refine hsub.congr ?_ refine Filter.Eventually.of_forall (fun ω => ?_) unfold A R rw [Pi.sub_apply] ring have hN_int : Integrable (fun ω => A ω * R ω - (1 - A ω) * W ω * R ω) P.μ := by exact htreated_int.sub (by simpa [A, R, W] using hIPW) have hAθ_int : Integrable (fun ω => A ω * S.θ₀) P.μ := by have hA_int : Integrable A P.μ := by simpa [A] using S.toPOBackdoorSystem.dVar.integrable_indicator true have h := hA_int.const_mul S.θ₀ exact h.congr (Filter.Eventually.of_forall (fun ω => by unfold A ring)) have hmap : ∫ z, aipwMomentATT z S.μ₀_val S.e_val S.θ₀ ∂(S.P_Z) = ∫ ω, aipwMomentATT (S.factualZ ω) S.μ₀_val S.e_val S.θ₀ ∂P.μ := by rw [TreatedEstimationSystem.P_Z] exact MeasureTheory.integral_map S.measurable_factualZ.aemeasurable (measurable_aipwMomentATT_at_θ₀ S).aestronglyMeasurable rw [hmap] have hrewrite : (fun ω => aipwMomentATT (S.factualZ ω) S.μ₀_val S.e_val S.θ₀) =ᵐ[P.μ] (fun ω => A ω * R ω - (1 - A ω) * W ω * R ω - A ω * S.θ₀) := by filter_upwards [S.μ₀_compat hA, S.e_compat, S.control_cate_backdoor hA] with ω hμ he hcat have hμ_eq : S.μ₀_val (S.toPOBackdoorSystem.factualX ω) = S.toPOBackdoorSystem.adjustedCE false ω := by have hcate_eq : S.toPOBackdoorSystem.CATE false ω = S.μ₀_val (S.toPOBackdoorSystem.factualX ω) := by simpa [POBackdoorSystem.CATE] using hμ rw [← hcate_eq, hcat] have he_eq : S.e_val (S.toPOBackdoorSystem.factualX ω) = S.toPOBackdoorSystem.propScore true ω := he.symm have hindA_true : indA (S.factualZ ω) = A ω := by by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [TreatedEstimationSystem.factualZ, A, indA, projA, hD, hInd] · have hF : S.toPOBackdoorSystem.factualD ω = false := by cases h' : S.toPOBackdoorSystem.factualD ω <;> simp [h'] at hD ⊢ have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [TreatedEstimationSystem.factualZ, A, indA, projA, hD, hInd] unfold aipwMomentATT R W rw [hindA_true] simp [TreatedEstimationSystem.factualZ, projX, projY, hμ_eq, he_eq] calc ∫ ω, aipwMomentATT (S.factualZ ω) S.μ₀_val S.e_val S.θ₀ ∂P.μ = ∫ ω, A ω * R ω - (1 - A ω) * W ω * R ω - A ω * S.θ₀ ∂P.μ := MeasureTheory.integral_congr_ae hrewrite _ = N - ∫ ω, A ω * S.θ₀ ∂P.μ := by exact MeasureTheory.integral_sub hN_int hAθ_int _ = N - S.θ₀ * S.π_val := by have hAconst : ∫ ω, A ω * S.θ₀ ∂P.μ = S.θ₀ * ∫ ω, A ω ∂P.μ := by integral_linearity ring rw [hAconst] simp [TreatedEstimationSystem.π_val, POBackdoorSystem.propTreated, A] _ = 0 := by rw [hN_eq] ring

-- Outline: pull `g(X)` out of `μ[·|σ(X)]` via -- `condExp_mul_of_stronglyMeasurable_left`, then apply -- `residual_false_condExp_zero` and `integral_condExp`. lemma weighted_residual_false_integral_zero (S : TreatedEstimationSystem P γ) (hA : S.toPOBackdoorSystem.ATTAssumptions) (g : γ → ℝ) (hg_meas : Measurable g) (h_int : Integrable (fun ω => g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω)))) P.μ) : ∫ ω, g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω))) ∂P.μ = 0 := by have hg_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] (fun ω => g (S.toPOBackdoorSystem.factualX ω)) := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => g (S.toPOBackdoorSystem.factualX ω)) exact (hg_meas.comp (comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable have hY_int : Integrable S.toPOBackdoorSystem.factualY P.μ := S.toPOBackdoorSystem.integrable_factualY_of_consistency hA.consistency hA.integrable_Y1 hA.integrable_Y0 have hYind_int : Integrable (fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator false ω) P.μ := S.toPOBackdoorSystem.dVar.integrable_mul_indicator false (measurableSet_singleton false) hY_int have hμ₀x_int : Integrable (fun ω => S.μ₀_val (S.toPOBackdoorSystem.factualX ω)) P.μ := by have hcate_int : Integrable (S.toPOBackdoorSystem.CATE false) P.μ := by unfold POBackdoorSystem.CATE exact MeasureTheory.integrable_condExp exact hcate_int.congr (S.μ₀_compat hA) have hμ₀x_meas : Measurable (fun ω => S.μ₀_val (S.toPOBackdoorSystem.factualX ω)) := S.μ₀_meas.comp S.toPOBackdoorSystem.measurable_factualX have hμ₀ind_int : Integrable (fun ω => S.μ₀_val (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator false ω) P.μ := S.toPOBackdoorSystem.dVar.integrable_mul_indicator false (measurableSet_singleton false) hμ₀x_int have hresid_int : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω))) P.μ := by have hYind_int' : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator false ω * S.toPOBackdoorSystem.factualY ω) P.μ := by simpa [mul_comm] using hYind_int have hμ₀ind_int' : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator false ω * S.μ₀_val (S.toPOBackdoorSystem.factualX ω)) P.μ := by simpa [mul_comm] using hμ₀ind_int have hsub := hYind_int'.sub hμ₀ind_int' refine hsub.congr ?_ refine Filter.Eventually.of_forall (fun ω => ?_) change S.toPOBackdoorSystem.dVar.indicator false ω * S.toPOBackdoorSystem.factualY ω - S.toPOBackdoorSystem.dVar.indicator false ω * S.μ₀_val (S.toPOBackdoorSystem.factualX ω) = S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω)) ring have hcondexp_pull := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := P.μ) (m := S.toPOBackdoorSystem.sigmaX) hg_sm h_int hresid_int have hgresid_ce_zero : P.μ[fun ω => g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω))) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by refine hcondexp_pull.trans ?_ filter_upwards [residual_false_condExp_zero S hA] with ω hω have : ((fun ω' => g (S.toPOBackdoorSystem.factualX ω')) * P.μ[fun ω' => S.toPOBackdoorSystem.dVar.indicator false ω' * (S.toPOBackdoorSystem.factualY ω' - S.μ₀_val (S.toPOBackdoorSystem.factualX ω')) | S.toPOBackdoorSystem.sigmaX]) ω = 0 := by rw [Pi.mul_apply, hω, mul_zero] exact this calc ∫ ω, g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω))) ∂P.μ = ∫ ω, P.μ[fun ω => g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ₀_val (S.toPOBackdoorSystem.factualX ω))) | S.toPOBackdoorSystem.sigmaX] ω ∂P.μ := by rw [MeasureTheory.integral_condExp S.toPOBackdoorSystem.sigmaX_le] _ = ∫ _, (0 : ℝ) ∂P.μ := MeasureTheory.integral_congr_ae hgresid_ce_zero _ = 0 := MeasureTheory.integral_zero _ _

-- Outline: same proof recipe as the ATE counterpart. Pull `f(X)` out of -- `μ[·|σ(X)]`, apply the appropriate `propScore_eq_e_val_ae` / -- `propScore_false_eq_one_minus_e_val_ae` substitution, and re-integrate. lemma indicator_to_propScore_integral (S : TreatedEstimationSystem P γ) (hA : S.toPOBackdoorSystem.ATTAssumptions) (d : Bool) (f : γ → ℝ) (hf_meas : Measurable f) (hf_ind_int : Integrable (fun ω => f (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ) : ∫ ω, f (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω ∂P.μ = ∫ ω, f (S.toPOBackdoorSystem.factualX ω) * (if d = true then S.e_val (S.toPOBackdoorSystem.factualX ω) else 1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) ∂P.μ := by have hf_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] (fun ω => f (S.toPOBackdoorSystem.factualX ω)) := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => f (S.toPOBackdoorSystem.factualX ω)) exact (hf_meas.comp (comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable have hind_int : Integrable (S.toPOBackdoorSystem.dVar.indicator d) P.μ := S.toPOBackdoorSystem.dVar.integrable_indicator d (measurableSet_singleton d) have hCE_pull := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := P.μ) (m := S.toPOBackdoorSystem.sigmaX) hf_sm hf_ind_int hind_int have hprop : S.toPOBackdoorSystem.propScore d =ᵐ[P.μ] (fun ω => if d = true then S.e_val (S.toPOBackdoorSystem.factualX ω) else 1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) := by cases d · simpa using propScore_false_eq_one_minus_e_val_ae S hA · simpa using propScore_eq_e_val_ae S hA have hCE_replace : P.μ[fun ω => f (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun ω => f (S.toPOBackdoorSystem.factualX ω) * (if d = true then S.e_val (S.toPOBackdoorSystem.factualX ω) else 1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) := by refine hCE_pull.trans ?_ filter_upwards [hprop] with ω hω have hω' : P.μ[S.toPOBackdoorSystem.dVar.indicator d | S.toPOBackdoorSystem.sigmaX] ω = (if d = true then S.e_val (S.toPOBackdoorSystem.factualX ω) else 1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) := hω rw [Pi.mul_apply, hω'] calc ∫ ω, f (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω ∂P.μ = ∫ ω, P.μ[fun ω => f (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] ω ∂P.μ := (MeasureTheory.integral_condExp S.toPOBackdoorSystem.sigmaX_le).symm _ = ∫ ω, f (S.toPOBackdoorSystem.factualX ω) * (if d = true then S.e_val (S.toPOBackdoorSystem.factualX ω) else 1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) ∂P.μ := MeasureTheory.integral_congr_ae hCE_replace