Estimation.ATT.Remainder

-- Outline: -- 1. Apply `aipw_remainder_identity_ATT` to rewrite -- `|∫ m_AIPW(η, z, θ₀) dP_Z|` as `|∫ ((ê − e_val)/(1 − ê))·(μ̂₀ − μ₀_val) dP_X|`. -- 2. Bound `|((ê − e_val)/(1 − ê))·(μ̂₀ − μ₀_val)| ≤ (1/ε)·|(ê − e_val)·(μ̂₀ − μ₀_val)|` -- `P_X`-a.e. on `H_ε` (since `ê ≤ 1 − ε ⇒ 1/(1 − ê) ≤ 1/ε`). -- 3. Apply `integral_abs_mul_le_eLpNorm_mul_eLpNorm` to the product -- `(ê − e_val) · (μ̂₀ − μ₀_val)` to obtain the L² product bound. theorem aipw_remainder_bound_ATT (S : TreatedEstimationSystem P γ) {ε : ℝ} (h_overlap : S.OneSidedOverlap ε) (hA : S.toPOBackdoorSystem.ATTAssumptions) (hπ_pos : 0 < S.π_val) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_y0_2 : Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ) (η : TreatedNuisanceVec γ) (hη : η ∈ H_ε S ε) (hΔμ₀_memLp : MemLp (fun x => η.μ₀_fn x - S.μ₀_val x) 2 S.P_X) (hΔe_memLp : MemLp (fun x => η.e_fn x - S.e_val x) 2 S.P_X) (hIPW : Integrable (fun z => (1 - indA z) * (η.e_fn (projX z) / (1 - η.e_fn (projX z))) * (projY z - η.μ₀_fn (projX z))) S.P_Z) : |∫ z, aipwMomentATTFunctional η z S.θ₀ ∂(S.P_Z)| ≤ aipw_rem_const_ATT ε * (eLpNorm (fun x => η.μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal * (eLpNorm (fun x => η.e_fn x - S.e_val x) 2 S.P_X).toReal := by let dμ : γ → ℝ := fun x => η.μ₀_fn x - S.μ₀_val x let de : γ → ℝ := fun x => η.e_fn x - S.e_val x let rem : γ → ℝ := fun x => (de x / (1 - η.e_fn x)) * dμ x let bound : γ → ℝ := fun x => aipw_rem_const_ATT ε * |de x * dμ x| have hC_nonneg : 0 ≤ aipw_rem_const_ATT ε := by unfold aipw_rem_const_ATT exact one_div_nonneg.mpr h_overlap.1.le have hpoint : ∀ᵐ x ∂S.P_X, |rem x| ≤ bound x := by filter_upwards [hη.1] with x hηx have hden : ε ≤ 1 - η.e_fn x := by linarith [hηx] have hη_false_pos_x : 0 < 1 - η.e_fn x := lt_of_lt_of_le h_overlap.1 hden have hinv_le : (1 - η.e_fn x)⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hη_false_pos_x h_overlap.1).2 hden have hinv_abs_le : |(1 - η.e_fn x)⁻¹| ≤ aipw_rem_const_ATT ε := by rw [abs_of_pos (inv_pos.mpr hη_false_pos_x)] simpa [aipw_rem_const_ATT, one_div] using hinv_le calc |rem x| = |de x * dμ x| * |(1 - η.e_fn x)⁻¹| := by rw [show rem x = de x * dμ x * (1 - η.e_fn x)⁻¹ by dsimp [rem] rw [div_eq_mul_inv] ring] simp [abs_mul] _ ≤ |de x * dμ x| * aipw_rem_const_ATT ε := mul_le_mul_of_nonneg_left hinv_abs_le (abs_nonneg _) _ = bound x := by ring haveI : ENNReal.HolderTriple (2 : ENNReal) (2 : ENNReal) (1 : ENNReal) := by constructor simpa using ENNReal.inv_two_add_inv_two haveI : IsFiniteMeasure S.P_X := by unfold TreatedEstimationSystem.P_X infer_instance have hprod_int : Integrable (fun x => de x * dμ x) S.P_X := by have hmul : MemLp (fun x => de x * dμ x) 1 S.P_X := by exact hΔμ₀_memLp.mul' hΔe_memLp exact hmul.integrable (by norm_num) have hbound_int : Integrable bound S.P_X := by simpa [bound] using hprod_int.norm.const_mul (aipw_rem_const_ATT ε) have hrem_meas : Measurable rem := by dsimp [rem, dμ, de] exact ((η.e_meas.sub S.e_meas).div (measurable_const.sub η.e_meas)).mul ((η.μ₀_meas).sub S.μ₀_meas) have hrem_abs_int : Integrable (fun x => |rem x|) S.P_X := hbound_int.mono' (by simpa [Real.norm_eq_abs] using hrem_meas.norm.aestronglyMeasurable) (by filter_upwards [hpoint] with x hx simpa [Real.norm_eq_abs] using hx) have hCS : ∫ x, |de x * dμ x| ∂(S.P_X) ≤ (eLpNorm dμ 2 S.P_X).toReal * (eLpNorm de 2 S.P_X).toReal := by have h := integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := S.P_X) hΔμ₀_memLp hΔe_memLp simpa [dμ, de, mul_comm] using h have hident := aipw_remainder_identity_ATT S h_overlap hA hπ_pos h_y2 h_y0_2 η hη hΔμ₀_memLp hΔe_memLp hIPW calc |∫ z, aipwMomentATTFunctional η z S.θ₀ ∂(S.P_Z)| = |∫ x, rem x ∂(S.P_X)| := by rw [hident] _ ≤ ∫ x, |rem x| ∂(S.P_X) := MeasureTheory.abs_integral_le_integral_abs _ ≤ ∫ x, bound x ∂(S.P_X) := integral_mono_ae hrem_abs_int hbound_int hpoint _ = aipw_rem_const_ATT ε * (∫ x, |de x * dμ x| ∂(S.P_X)) := by rw [show bound = (fun x => aipw_rem_const_ATT ε * ‖de x * dμ x‖) by funext x simp [bound, Real.norm_eq_abs]] rw [integral_const_mul] simp [Real.norm_eq_abs] _ ≤ aipw_rem_const_ATT ε * ((eLpNorm dμ 2 S.P_X).toReal * (eLpNorm de 2 S.P_X).toReal) := mul_le_mul_of_nonneg_left hCS hC_nonneg _ = aipw_rem_const_ATT ε * (eLpNorm (fun x => η.μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal * (eLpNorm (fun x => η.e_fn x - S.e_val x) 2 S.P_X).toReal := by simp [dμ, de] ring

-- Outline: -- 1. Apply `aipw_remainder_bound_ATT` pointwise in `(n, ω)` to get -- `|∫ m_AIPW(η_hat n ω, z, θ₀) dP_Z| ≤ C(ε) · prodTerm n ω`. -- 2. Conclude `IsLittleOp (∫ m …) (n^{-1/2}) P.μ` via -- `IsLittleOp.of_abs_le_const_mul` applied to `h_product_rate`. theorem aipw_remainder_op_ATT (S : TreatedEstimationSystem P γ) {ε : ℝ} (h_overlap : S.OneSidedOverlap ε) (hA : S.toPOBackdoorSystem.ATTAssumptions) (hπ_pos : 0 < S.π_val) (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Δμ₀_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) (hIPW : ∀ n ω, Integrable (fun z => (1 - indA z) * ((η_hat n ω).e_fn (projX z) / (1 - (η_hat n ω).e_fn (projX z))) * (projY z - (η_hat n ω).μ₀_fn (projX z))) S.P_Z) (h_product_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) : IsLittleOp (fun n ω => ∫ z, aipwMomentATTFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ := by let rn : ℕ → ℝ := fun n => (n : ℝ) ^ (-(1 / 2 : ℝ)) let prodTerm : ℕ → P.Ω → ℝ := fun n ω => (eLpNorm (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal have hCpos : 0 < aipw_rem_const_ATT ε := by unfold aipw_rem_const_ATT exact one_div_pos.mpr h_overlap.1 refine IsLittleOp.of_abs_le_const_mul (μ := P.μ) hCpos (by simpa [prodTerm, rn] using h_product_rate) ?_ intro n ω have hprod_nonneg : 0 ≤ prodTerm n ω := by exact mul_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg have hbound := aipw_remainder_bound_ATT S h_overlap hA hπ_pos h_y2 h_y0_2 (η_hat n ω) (h_in_H n ω) (hΔμ₀_memLp n ω) (hΔe_memLp n ω) (hIPW n ω) have habs_prod : |prodTerm n ω| = prodTerm n ω := abs_of_nonneg hprod_nonneg calc |∫ z, aipwMomentATTFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)| ≤ aipw_rem_const_ATT ε * (eLpNorm (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal := hbound _ = aipw_rem_const_ATT ε * prodTerm n ω := by simp [prodTerm] ring _ = aipw_rem_const_ATT ε * |prodTerm n ω| := by rw [habs_prod]

-- Outline: -- 1. Push `∫ … dP_Z` back to `∫ … dP.μ` via `integral_map`. -- 2. Decompose the AIPW moment around `η₀` into: -- (a) `m(η₀, z, θ₀)`, mean zero by `aipw_mean_zero_ATT`; -- (b) `A · (μ₀_val(X) − μ̂₀(X))`, whose integral against `P.μ` factors -- through `propScore true =ᵐ e_val ∘ factualX` into -- `∫ e_val · (μ₀_val − μ̂₀) dP_X`; -- (c) `−(1 − A) · (ê/(1 − ê)) · (Y − μ̂₀(X)) -- + (1 − A) · (e_val/(1 − e_val)) · (Y − μ₀_val(X))`, -- which reduces (via `weighted_residual_false_integral_zero` on the -- `Y − μ₀_val` half and the σ(X)-pull-out for the `Y − μ̂₀` half) to -- `−∫ (ê/(1 − ê)) · (1 − e_val) · (μ₀_val − μ̂₀) dP_X`. -- 3. Combine: the integrand simplifies to -- `(e_val(1 − ê) − ê(1 − e_val))/(1 − ê) · (μ₀_val − μ̂₀) -- = ((e_val − ê)/(1 − ê)) · (μ₀_val − μ̂₀) -- = ((ê − e_val)/(1 − ê)) · (μ̂₀ − μ₀_val)`. theorem aipw_remainder_identity_ATT (S : TreatedEstimationSystem P γ) {ε : ℝ} (h_overlap : S.OneSidedOverlap ε) (hA : S.toPOBackdoorSystem.ATTAssumptions) (hπ_pos : 0 < S.π_val) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_y0_2 : Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ) (η : TreatedNuisanceVec γ) (hη : η ∈ H_ε S ε) (hΔμ₀_memLp : MemLp (fun x => η.μ₀_fn x - S.μ₀_val x) 2 S.P_X) (hΔe_memLp : MemLp (fun x => η.e_fn x - S.e_val x) 2 S.P_X) (hIPW : Integrable (fun z => (1 - indA z) * (η.e_fn (projX z) / (1 - η.e_fn (projX z))) * (projY z - η.μ₀_fn (projX z))) S.P_Z) : ∫ z, aipwMomentATTFunctional η z S.θ₀ ∂(S.P_Z) = ∫ x, (η.e_fn x - S.e_val x) / (1 - η.e_fn x) * (η.μ₀_fn x - S.μ₀_val x) ∂(S.P_X) := by let X : P.Ω → γ := S.toPOBackdoorSystem.factualX let Y : P.Ω → ℝ := S.toPOBackdoorSystem.factualY let A : P.Ω → ℝ := S.toPOBackdoorSystem.dVar.indicator true let F : P.Ω → ℝ := S.toPOBackdoorSystem.dVar.indicator false let dμ : P.Ω → ℝ := fun ω => η.μ₀_fn (X ω) - S.μ₀_val (X ω) let gηX : P.Ω → ℝ := fun ω => η.e_fn (X ω) / (1 - η.e_fn (X ω)) let g₀X : P.Ω → ℝ := fun ω => S.e_val (X ω) / (1 - S.e_val (X ω)) let truth : P.Ω → ℝ := fun ω => aipwMomentATT (S.factualZ ω) S.μ₀_val S.e_val S.θ₀ let cand : P.Ω → ℝ := fun ω => aipwMomentATTFunctional η (S.factualZ ω) S.θ₀ let resid : P.Ω → ℝ := fun ω => (gηX ω - g₀X ω) * (F ω * (Y ω - S.μ₀_val (X ω))) let crossInd : P.Ω → ℝ := fun ω => -A ω * dμ ω + F ω * gηX ω * dμ ω let crossProp : P.Ω → ℝ := fun ω => -S.e_val (X ω) * dμ ω + (1 - S.e_val (X ω)) * gηX ω * dμ ω let remΩ : P.Ω → ℝ := fun ω => (η.e_fn (X ω) - S.e_val (X ω)) / (1 - η.e_fn (X ω)) * dμ ω let remX : γ → ℝ := fun x => (η.e_fn x - S.e_val x) / (1 - η.e_fn x) * (η.μ₀_fn x - S.μ₀_val x) haveI : IsFiniteMeasure S.P_Z := by unfold TreatedEstimationSystem.P_Z infer_instance haveI : IsFiniteMeasure S.P_X := by unfold TreatedEstimationSystem.P_X infer_instance have hindA_true : ∀ ω, indA (S.factualZ ω) = A ω := by intro ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : A ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [TreatedEstimationSystem.factualZ, indA, projA, A, hD, hInd] · have hF : S.toPOBackdoorSystem.factualD ω = false := by cases h' : S.toPOBackdoorSystem.factualD ω <;> simp [h'] at hD ⊢ have hInd : A ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [TreatedEstimationSystem.factualZ, indA, projA, A, hD, hInd] have hfalse_ind : ∀ ω, 1 - A ω = F ω := by intro ω have hsum : A ω + F ω = 1 := by simpa [A, F] using S.toPOBackdoorSystem.dVar.indicator_add_indicator_not ω linarith have hη_X : ∀ᵐ ω ∂P.μ, η.e_fn (X ω) ≤ 1 - ε := by simpa [X] using H_ε_overlap_factualX S hη have hY_L2 : MemLp Y 2 P.μ := by dsimp [Y] exact (memLp_two_iff_integrable_sq S.toPOBackdoorSystem.measurable_factualY.aestronglyMeasurable).2 h_y2 have hμ₀_L2 : MemLp (fun ω => S.μ₀_val (X ω)) 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 (by norm_num) exact hcond_L2.ae_eq (by simpa [X] using S.μ₀_compat hA) have hdμ_L2 : MemLp dμ 2 P.μ := by have hd := MemLp.comp_of_map (f := S.toPOBackdoorSystem.factualX) hΔμ₀_memLp S.toPOBackdoorSystem.measurable_factualX.aemeasurable exact hd have hdμ_int : Integrable dμ P.μ := hdμ_L2.integrable (by norm_num) have hA_meas : Measurable A := by simpa [A] using S.toPOBackdoorSystem.dVar.measurable_indicator true have hF_meas : Measurable F := by simpa [F] using S.toPOBackdoorSystem.dVar.measurable_indicator false have hA_bound : ∀ᵐ ω ∂P.μ, ‖A ω‖ ≤ (1 : ℝ) := by filter_upwards with ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : A ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [hInd] · have hInd : A ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [hInd] have hF_bound : ∀ᵐ ω ∂P.μ, ‖F ω‖ ≤ (1 : ℝ) := by filter_upwards with ω by_cases hD : S.toPOBackdoorSystem.factualD ω = false · have hInd : F ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [hInd] · have hInd : F ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := false) hD simp [hInd] have hA_Linf : MemLp A ⊤ P.μ := MemLp.of_bound hA_meas.aestronglyMeasurable (1 : ℝ) hA_bound have hF_Linf : MemLp F ⊤ P.μ := MemLp.of_bound hF_meas.aestronglyMeasurable (1 : ℝ) hF_bound have htreatedη_int : Integrable (fun ω => A ω * (Y ω - η.μ₀_fn (X ω))) P.μ := by have hημ_L2 : MemLp (fun ω => η.μ₀_fn (X ω)) 2 P.μ := by have hsum := hdμ_L2.add hμ₀_L2 refine hsum.ae_eq ?_ filter_upwards with ω simp [dμ] have hL2 : MemLp (fun ω => A ω * (Y ω - η.μ₀_fn (X ω))) 2 P.μ := by exact (hY_L2.sub hημ_L2).mul' hA_Linf exact hL2.integrable (by norm_num) have htreated₀_int : Integrable (fun ω => A ω * (Y ω - S.μ₀_val (X ω))) P.μ := by have hL2 : MemLp (fun ω => A ω * (Y ω - S.μ₀_val (X ω))) 2 P.μ := by exact (hY_L2.sub hμ₀_L2).mul' hA_Linf exact hL2.integrable (by norm_num) have hAθ_int : Integrable (fun ω => A ω * S.θ₀) P.μ := by have hL2 : MemLp (fun ω => A ω * S.θ₀) 2 P.μ := by exact MemLp.mul' (p := ⊤) (q := 2) (r := 2) (memLp_const (α := P.Ω) S.θ₀) hA_Linf exact hL2.integrable (by norm_num) have hIPWΩ : Integrable (fun ω => F ω * gηX ω * (Y ω - η.μ₀_fn (X ω))) P.μ := by have hmap : Integrable (fun ω => (1 - indA (S.factualZ ω)) * (η.e_fn (projX (S.factualZ ω)) / (1 - η.e_fn (projX (S.factualZ ω)))) * (projY (S.factualZ ω) - η.μ₀_fn (projX (S.factualZ ω)))) P.μ := by exact (MeasureTheory.integrable_map_measure hIPW.aestronglyMeasurable S.measurable_factualZ.aemeasurable).1 hIPW refine hmap.congr ?_ filter_upwards with ω have hnot : 1 - indA (S.factualZ ω) = F ω := by rw [hindA_true ω, hfalse_ind ω] dsimp [gηX, X, Y] rw [hnot] rfl have hη_comp_int : Integrable cand P.μ := by have hsum := (htreatedη_int.sub hIPWΩ).sub hAθ_int refine hsum.congr ?_ filter_upwards with ω unfold cand aipwMomentATTFunctional aipwMomentATT rw [hindA_true ω, hfalse_ind ω] simp [TreatedEstimationSystem.factualZ, projX, projY, A, F, X, Y, gηX] have htruth_sq : Integrable (fun z => (aipwMomentATT z S.μ₀_val S.e_val S.θ₀) ^ 2) S.P_Z := aipw_finite_var_ATT S h_overlap hA h_y2 h_y0_2 have htruth_meas : Measurable (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) := by simpa [aipwMomentATTFunctional, η₀] using (measurable_aipwMomentATTFunctional (η := S.η₀) (θ := S.θ₀)) have htruth_L2 : MemLp (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) 2 S.P_Z := (memLp_two_iff_integrable_sq htruth_meas.aestronglyMeasurable).2 htruth_sq have htruthPZ_int : Integrable (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) S.P_Z := htruth_L2.integrable (by norm_num) have htruth_int : Integrable truth P.μ := by exact (MeasureTheory.integrable_map_measure htruth_meas.aestronglyMeasurable S.measurable_factualZ.aemeasurable).1 (by simpa [TreatedEstimationSystem.P_Z] using htruthPZ_int) have hfalse₀_int : Integrable (fun ω => F ω * g₀X ω * (Y ω - S.μ₀_val (X ω))) P.μ := by have hcomb : Integrable (fun ω => A ω * (Y ω - S.μ₀_val (X ω)) - truth ω - A ω * S.θ₀) P.μ := (htreated₀_int.sub htruth_int).sub hAθ_int refine hcomb.congr ?_ filter_upwards with ω unfold truth aipwMomentATT rw [hindA_true ω, hfalse_ind ω] simp [TreatedEstimationSystem.factualZ, projX, projY, A, F, X, Y, g₀X] ring have 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.μ := by refine hfalse₀_int.congr ?_ filter_upwards [S.e_compat, S.μ₀_compat hA, S.control_cate_backdoor hA] with ω he hμ hcat have hμ_eq : S.μ₀_val (X ω) = 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 (X ω) = S.toPOBackdoorSystem.propScore true ω := by simpa [X] using he.symm have hfalse_eq : S.toPOBackdoorSystem.dVar.indicator false ω = 1 - S.toPOBackdoorSystem.dVar.indicator true ω := by simpa [A, F] using (hfalse_ind ω).symm dsimp [F, g₀X, X, Y] rw [he_eq, hμ_eq, hfalse_eq] have htruth_zero : ∫ z, aipwMomentATT z S.μ₀_val S.e_val S.θ₀ ∂(S.P_Z) = 0 := aipw_mean_zero_ATT S hA hπ_pos hIPW₀ have htruth_zero_Ω : ∫ ω, truth ω ∂P.μ = 0 := by have hmap : ∫ z, aipwMomentATT z S.μ₀_val S.e_val S.θ₀ ∂(S.P_Z) = ∫ ω, truth ω ∂P.μ := by unfold TreatedEstimationSystem.P_Z exact MeasureTheory.integral_map S.measurable_factualZ.aemeasurable htruth_meas.aestronglyMeasurable simpa [hmap] using htruth_zero have hpushη : -- … truncated; follow the source link for the rest …