Estimation.ATE.Remainder

lemma aipw_remainder_identity (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (η : NuisanceVec γ) (hη : η ∈ H_ε_aeL2 S ε) (hΔμ_memLp : ∀ a, MemLp (fun x => η.μ_fn a x - S.μ_val a x) 2 S.P_X) : ∫ z, aipwMomentFunctional η z S.θ₀ ∂(S.P_Z) = ∫ x, (η.e_fn x - S.e_val x) * ((η.μ_fn true x - S.μ_val true x) / η.e_fn x + (η.μ_fn false x - S.μ_val false x) / (1 - η.e_fn x)) ∂(S.P_X) := by let X : P.Ω → γ := S.toPOBackdoorSystem.factualX let Y : P.Ω → ℝ := S.toPOBackdoorSystem.factualY let indT : P.Ω → ℝ := S.toPOBackdoorSystem.dVar.indicator true let indF : P.Ω → ℝ := S.toPOBackdoorSystem.dVar.indicator false let dμT : P.Ω → ℝ := fun ω => η.μ_fn true (X ω) - S.μ_val true (X ω) let dμF : P.Ω → ℝ := fun ω => η.μ_fn false (X ω) - S.μ_val false (X ω) let wT : P.Ω → ℝ := fun ω => indT ω / η.e_fn (X ω) let wF : P.Ω → ℝ := fun ω => indF ω / (1 - η.e_fn (X ω)) let base : P.Ω → ℝ := fun ω => S.μ_val true (X ω) - S.μ_val false (X ω) - S.θ₀ let rT : P.Ω → ℝ := fun ω => wT ω * (Y ω - S.μ_val true (X ω)) let rF : P.Ω → ℝ := fun ω => wF ω * (Y ω - S.μ_val false (X ω)) let iT : P.Ω → ℝ := fun ω => wT ω * dμT ω let iF : P.Ω → ℝ := fun ω => wF ω * dμF ω let pT : P.Ω → ℝ := fun ω => (dμT ω / η.e_fn (X ω)) * S.e_val_label true (X ω) let pF : P.Ω → ℝ := fun ω => (dμF ω / (1 - η.e_fn (X ω))) * S.e_val_label false (X ω) let crossInd : P.Ω → ℝ := fun ω => dμT ω - dμF ω - iT ω + iF ω let crossProp : P.Ω → ℝ := fun ω => dμT ω - dμF ω - pT ω + pF ω let remΩ : P.Ω → ℝ := fun ω => (η.e_fn (X ω) - S.e_val (X ω)) * (dμT ω / η.e_fn (X ω) + dμF ω / (1 - η.e_fn (X ω))) let remX : γ → ℝ := fun x => (η.e_fn x - S.e_val x) * ((η.μ_fn true x - S.μ_val true x) / η.e_fn x + (η.μ_fn false x - S.μ_val false x) / (1 - η.e_fn x)) have hindA_true : ∀ ω, indA (S.factualZ ω) = indT ω := by intro ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : indT ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [BackdoorEstimationSystem.factualZ, indA, projA, indT, hD, hInd] · have hF : S.toPOBackdoorSystem.factualD ω = false := by cases h' : S.toPOBackdoorSystem.factualD ω <;> simp [h'] at hD ⊢ have hInd : indT ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [BackdoorEstimationSystem.factualZ, indA, projA, indT, hD, hInd] have hindA_false : ∀ ω, 1 - indA (S.factualZ ω) = indF ω := by intro ω have hsum : indT ω + indF ω = 1 := by simpa [indT, indF] using S.toPOBackdoorSystem.dVar.indicator_add_indicator_not ω calc 1 - indA (S.factualZ ω) = 1 - indT ω := by rw [hindA_true ω] _ = indF ω := by linarith have hη_X : ∀ᵐ ω ∂P.μ, ε ≤ η.e_fn (X ω) ∧ η.e_fn (X ω) ≤ 1 - ε := by simpa [X] using H_ε_aeL2_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 : ∀ d : Bool, MemLp (fun ω => S.μ_val d (X ω)) 2 P.μ := by intro d have hYd_L2 : MemLp (S.toPOBackdoorSystem.YofD d) 2 P.μ := by exact (memLp_two_iff_integrable_sq (S.toPOBackdoorSystem.measurable_YofD d).aestronglyMeasurable).2 (h_yd2 d) have hcond_L2 : MemLp (P.μ[S.toPOBackdoorSystem.YofD d | S.toPOBackdoorSystem.sigmaX]) 2 P.μ := hYd_L2.condExp one_le_two exact hcond_L2.ae_eq (by simpa [X] using S.μ_compat hA d) have hdμ_L2 : ∀ d : Bool, MemLp (fun ω => η.μ_fn d (X ω) - S.μ_val d (X ω)) 2 P.μ := by intro d have hd : MemLp (fun x => η.μ_fn d x - S.μ_val d x) 2 S.P_X := hΔμ_memLp d simp only [X] exact MemLp.comp_of_map (f := S.toPOBackdoorSystem.factualX) hd S.toPOBackdoorSystem.measurable_factualX.aemeasurable have hwT_bound : ∀ᵐ ω ∂P.μ, ‖wT ω‖ ≤ ε⁻¹ := by filter_upwards [hη_X] with ω hηω have hη_pos_ω : 0 < η.e_fn (X ω) := lt_of_lt_of_le h_overlap.1 hηω.1 by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : indT ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD have hle : (η.e_fn (X ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hη_pos_ω h_overlap.1).2 hηω.1 simpa [wT, hInd, one_div, Real.norm_eq_abs, abs_of_pos hη_pos_ω] using hle · have hInd : indT ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr h_overlap.1.le simpa [wT, hInd] using hεinv_nonneg have hwF_bound : ∀ᵐ ω ∂P.μ, ‖wF ω‖ ≤ ε⁻¹ := by filter_upwards [hη_X] with ω hηω have hη_false_pos_ω : 0 < 1 - η.e_fn (X ω) := by have : ε ≤ 1 - η.e_fn (X ω) := by linarith [hηω.2] exact lt_of_lt_of_le h_overlap.1 this by_cases hD : S.toPOBackdoorSystem.factualD ω = false · have hInd : indF ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD have hden : ε ≤ 1 - η.e_fn (X ω) := by linarith [hηω.2] have hle : (1 - η.e_fn (X ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hη_false_pos_ω h_overlap.1).2 hden simpa [wF, hInd, one_div, Real.norm_eq_abs, abs_of_pos hη_false_pos_ω] using hle · have hInd : indF ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := false) hD have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr h_overlap.1.le simpa [wF, hInd] using hεinv_nonneg have hwT_Linf : MemLp wT ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ hwT_bound apply Measurable.aestronglyMeasurable exact S.toPOBackdoorSystem.dVar.measurable_indicator true (MeasurableSet.singleton true) |>.div (η.e_meas.comp S.toPOBackdoorSystem.measurable_factualX) have hwF_Linf : MemLp wF ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ hwF_bound apply Measurable.aestronglyMeasurable exact S.toPOBackdoorSystem.dVar.measurable_indicator false (MeasurableSet.singleton false) |>.div (measurable_const.sub (η.e_meas.comp S.toPOBackdoorSystem.measurable_factualX)) have hrT_int : Integrable rT P.μ := by have hL2 : MemLp rT 2 P.μ := by simp only [rT, Y, X, wT] exact (hY_L2.sub (hμ_L2 true)).mul hwT_Linf exact hL2.integrable (by norm_num) have hrF_int : Integrable rF P.μ := by have hL2 : MemLp rF 2 P.μ := by simp only [rF, Y, X, wF] exact (hY_L2.sub (hμ_L2 false)).mul hwF_Linf exact hL2.integrable (by norm_num) have hiT_int : Integrable iT P.μ := by have hL2 : MemLp iT 2 P.μ := by simp only [iT, dμT, X, wT] exact (hdμ_L2 true).mul hwT_Linf exact hL2.integrable (by norm_num) have hiF_int : Integrable iF P.μ := by have hL2 : MemLp iF 2 P.μ := by simp only [iF, dμF, X, wF] exact (hdμ_L2 false).mul hwF_Linf exact hL2.integrable (by norm_num) have hdμT_int : Integrable dμT P.μ := (hdμ_L2 true).integrable (by norm_num) have hdμF_int : Integrable dμF P.μ := (hdμ_L2 false).integrable (by norm_num) have hbase_int : Integrable base P.μ := by have hdiff : Integrable (fun ω => S.μ_val true (X ω) - S.μ_val false (X ω)) P.μ := ((hμ_L2 true).sub (hμ_L2 false)).integrable (by norm_num) simpa [base, sub_eq_add_neg] using hdiff.sub (integrable_const (S.θ₀)) have hcrossInd_int : Integrable crossInd P.μ := by simp only [crossInd] exact ((hdμT_int.sub hdμF_int).sub hiT_int).add hiF_int have hbase_zero : ∫ ω, base ω ∂P.μ = 0 := by have hθ : S.θ₀ = ∫ ω, S.μ_val true (X ω) - S.μ_val false (X ω) ∂P.μ := by simpa [X] using theta_zero_factualX_integral S have hdiff : Integrable (fun ω => S.μ_val true (X ω) - S.μ_val false (X ω)) P.μ := ((hμ_L2 true).sub (hμ_L2 false)).integrable (by norm_num) have hconst : (∫ _ : P.Ω, S.θ₀ ∂P.μ) = S.θ₀ := by haveI : IsProbabilityMeasure P.μ := inferInstance simp calc ∫ ω, base ω ∂P.μ = (∫ ω, S.μ_val true (X ω) - S.μ_val false (X ω) ∂P.μ) - ∫ _ : P.Ω, S.θ₀ ∂P.μ := by rw [show base = (fun ω => (S.μ_val true (X ω) - S.μ_val false (X ω)) - S.θ₀) from rfl] rw [integral_sub] · exact hdiff · exact integrable_const (S.θ₀) _ = S.θ₀ - S.θ₀ := by rw [← hθ, hconst] _ = 0 := by ring have hrT_zero : ∫ ω, rT ω ∂P.μ = 0 := by have hg_meas : Measurable (fun x => 1 / η.e_fn x) := measurable_const.div η.e_meas have h_int : Integrable (fun ω => (1 / η.e_fn (X ω)) * (indT ω * (Y ω - S.μ_val true (X ω)))) P.μ := by refine hrT_int.congr ?_ exact Filter.Eventually.of_forall fun ω => by simp [rT, wT, X, Y, indT] ring calc ∫ ω, rT ω ∂P.μ = ∫ ω, (1 / η.e_fn (X ω)) * (indT ω * (Y ω - S.μ_val true (X ω))) ∂P.μ := by apply MeasureTheory.integral_congr_ae exact Filter.Eventually.of_forall fun ω => by simp [rT, wT, X, Y, indT] ring _ = 0 := by simpa [X, Y, indT] using weighted_residual_integral_zero S hA true (fun x => 1 / η.e_fn x) hg_meas h_int (cond_exp_residual_zero S hA true) have hrF_zero : ∫ ω, rF ω ∂P.μ = 0 := by have hg_meas : Measurable (fun x => 1 / (1 - η.e_fn x)) := measurable_const.div (measurable_const.sub η.e_meas) have h_int : Integrable (fun ω => (1 / (1 - η.e_fn (X ω))) * (indF ω * (Y ω - S.μ_val false (X ω)))) P.μ := by refine hrF_int.congr ?_ exact Filter.Eventually.of_forall fun ω => by simp [rF, wF, X, Y, indF] ring calc ∫ ω, rF ω ∂P.μ = ∫ ω, (1 / (1 - η.e_fn (X ω))) * (indF ω * (Y ω - S.μ_val false (X ω))) ∂P.μ := by apply MeasureTheory.integral_congr_ae exact Filter.Eventually.of_forall fun ω => by simp [rF, wF, X, Y, indF] ring _ = 0 := by simpa [X, Y, indF] using weighted_residual_integral_zero S hA false (fun x => 1 / (1 - η.e_fn x)) hg_meas h_int (cond_exp_residual_zero S hA false) have hmoment_eq : (fun ω => aipwMomentFunctional η (S.factualZ ω) S.θ₀) =ᵐ[P.μ] (fun ω => base ω + rT ω - rF ω + crossInd ω) := by refine Filter.Eventually.of_forall ?_ intro ω change aipwMomentFunctional η (S.factualZ ω) S.θ₀ = base ω + rT ω - rF ω + crossInd ω unfold aipwMomentFunctional aipwMoment base rT rF crossInd iT iF wT wF dμT dμF X Y have hnot_indT : 1 - indT ω = indF ω := by -- … truncated; follow the source link for the rest …

theorem aipw_remainder_bound (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (η : NuisanceVec γ) (hη : η ∈ H_ε_aeL2 S ε) (hΔμ_memLp : ∀ a, MemLp (fun x => η.μ_fn a x - S.μ_val a x) 2 S.P_X) (hΔe_memLp : MemLp (fun x => η.e_fn x - S.e_val x) 2 S.P_X) : |∫ z, aipwMomentFunctional η z S.θ₀ ∂(S.P_Z)| ≤ aipw_rem_const ε * ∑ a : Bool, (eLpNorm (fun x => η.μ_fn a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => η.e_fn x - S.e_val x) 2 S.P_X).toReal := by let dμT : γ → ℝ := fun x => η.μ_fn true x - S.μ_val true x let dμF : γ → ℝ := fun x => η.μ_fn false x - S.μ_val false x let de : γ → ℝ := fun x => η.e_fn x - S.e_val x let rem : γ → ℝ := fun x => de x * (dμT x / η.e_fn x + dμF x / (1 - η.e_fn x)) let bound : γ → ℝ := fun x => aipw_rem_const ε * |dμT x * de x| + aipw_rem_const ε * |dμF x * de x| have hC_ge_inv : ε⁻¹ ≤ aipw_rem_const ε := by unfold aipw_rem_const have hpos : 0 < ε := h_overlap.1 have hone : 0 < 1 - ε := by linarith [h_overlap.2.1] have hden : 0 < ε * (1 - ε) := mul_pos hpos hone rw [div_eq_mul_inv] field_simp [hpos.ne', hden.ne'] nlinarith [h_overlap.2.1] have hC_nonneg : 0 ≤ aipw_rem_const ε := (inv_nonneg.mpr h_overlap.1.le).trans hC_ge_inv have hpoint : ∀ᵐ x ∂S.P_X, |rem x| ≤ bound x := by filter_upwards [hη.1] with x hηx have hη_pos_x : 0 < η.e_fn x := lt_of_lt_of_le h_overlap.1 hηx.1 have hη_false_pos_x : 0 < 1 - η.e_fn x := by have : ε ≤ 1 - η.e_fn x := by linarith [hηx.2] exact lt_of_lt_of_le h_overlap.1 this have hdenT : η.e_fn x ≠ 0 := hη_pos_x.ne' have hdenF : 1 - η.e_fn x ≠ 0 := hη_false_pos_x.ne' have hinvT : |(η.e_fn x)⁻¹| ≤ aipw_rem_const ε := by have hle : (η.e_fn x)⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hη_pos_x h_overlap.1).2 hηx.1 rw [abs_of_pos (inv_pos.mpr hη_pos_x)] exact hle.trans hC_ge_inv have hinvF : |(1 - η.e_fn x)⁻¹| ≤ aipw_rem_const ε := by have hden : ε ≤ 1 - η.e_fn x := by linarith [hηx.2] have hle : (1 - η.e_fn x)⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hη_false_pos_x h_overlap.1).2 hden rw [abs_of_pos (inv_pos.mpr hη_false_pos_x)] exact hle.trans hC_ge_inv have hT : |de x * (dμT x / η.e_fn x)| ≤ aipw_rem_const ε * |dμT x * de x| := by calc |de x * (dμT x / η.e_fn x)| = |dμT x * de x| * |(η.e_fn x)⁻¹| := by rw [div_eq_mul_inv] simp [abs_mul, mul_assoc, mul_left_comm, mul_comm] _ ≤ |dμT x * de x| * aipw_rem_const ε := mul_le_mul_of_nonneg_left hinvT (abs_nonneg _) _ = aipw_rem_const ε * |dμT x * de x| := by ring have hF : |de x * (dμF x / (1 - η.e_fn x))| ≤ aipw_rem_const ε * |dμF x * de x| := by calc |de x * (dμF x / (1 - η.e_fn x))| = |dμF x * de x| * |(1 - η.e_fn x)⁻¹| := by rw [div_eq_mul_inv] simp [abs_mul, mul_assoc, mul_left_comm, mul_comm] _ ≤ |dμF x * de x| * aipw_rem_const ε := mul_le_mul_of_nonneg_left hinvF (abs_nonneg _) _ = aipw_rem_const ε * |dμF x * de x| := by ring calc |rem x| = |de x * (dμT x / η.e_fn x) + de x * (dμF x / (1 - η.e_fn x))| := by simp [rem, mul_add] _ ≤ |de x * (dμT x / η.e_fn x)| + |de x * (dμF x / (1 - η.e_fn x))| := abs_add_le _ _ _ ≤ bound x := by dsimp [bound] exact add_le_add hT hF 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 BackdoorEstimationSystem.P_X infer_instance have hprodT_int : Integrable (fun x => dμT x * de x) S.P_X := by have hmul : MemLp (fun x => dμT x * de x) 1 S.P_X := by exact hΔe_memLp.mul' (hΔμ_memLp true) exact hmul.integrable (by norm_num) have hprodF_int : Integrable (fun x => dμF x * de x) S.P_X := by have hmul : MemLp (fun x => dμF x * de x) 1 S.P_X := by exact hΔe_memLp.mul' (hΔμ_memLp false) exact hmul.integrable (by norm_num) have hbound_int : Integrable bound S.P_X := by exact ((hprodT_int.norm.const_mul (aipw_rem_const ε)).add (hprodF_int.norm.const_mul (aipw_rem_const ε))) have hrem_meas : Measurable rem := by dsimp [rem, dμT, dμF, de] exact ((η.e_meas.sub S.e_meas).mul ((((η.μ_meas true).sub (S.μ_meas true)).div η.e_meas).add (((η.μ_meas false).sub (S.μ_meas false)).div (measurable_const.sub η.e_meas)))) have hrem_abs_int : Integrable (fun x => |rem x|) S.P_X := hbound_int.mono' hrem_meas.abs.aestronglyMeasurable (by filter_upwards [hpoint] with x hx simpa [Real.norm_eq_abs] using hx) have hCS_T : ∫ x, |dμT x * de x| ∂(S.P_X) ≤ (eLpNorm dμT 2 S.P_X).toReal * (eLpNorm de 2 S.P_X).toReal := by simpa [dμT, de] using integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := S.P_X) (hΔμ_memLp true) hΔe_memLp have hCS_F : ∫ x, |dμF x * de x| ∂(S.P_X) ≤ (eLpNorm dμF 2 S.P_X).toReal * (eLpNorm de 2 S.P_X).toReal := by simpa [dμF, de] using integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := S.P_X) (hΔμ_memLp false) hΔe_memLp have hident := aipw_remainder_identity S h_overlap hA h_y2 h_yd2 η hη hΔμ_memLp calc |∫ z, aipwMomentFunctional η 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 ε * (∫ x, |dμT x * de x| ∂(S.P_X)) + aipw_rem_const ε * (∫ x, |dμF x * de x| ∂(S.P_X)) := by rw [show bound = (fun x => aipw_rem_const ε * |dμT x * de x| + aipw_rem_const ε * |dμF x * de x|) from rfl] change ∫ x, aipw_rem_const ε * |dμT x * de x| + aipw_rem_const ε * |dμF x * de x| ∂S.P_X = aipw_rem_const ε * (∫ x, |dμT x * de x| ∂S.P_X) + aipw_rem_const ε * (∫ x, |dμF x * de x| ∂S.P_X) rw [show (fun x => aipw_rem_const ε * |dμT x * de x| + aipw_rem_const ε * |dμF x * de x|) = (fun x => aipw_rem_const ε * ‖dμT x * de x‖ + aipw_rem_const ε * ‖dμF x * de x‖) by funext x simp [Real.norm_eq_abs]] rw [integral_add (hprodT_int.norm.const_mul (aipw_rem_const ε)) (hprodF_int.norm.const_mul (aipw_rem_const ε))] rw [integral_const_mul, integral_const_mul] simp [Real.norm_eq_abs] _ ≤ aipw_rem_const ε * ((eLpNorm dμT 2 S.P_X).toReal * (eLpNorm de 2 S.P_X).toReal) + aipw_rem_const ε * ((eLpNorm dμF 2 S.P_X).toReal * (eLpNorm de 2 S.P_X).toReal) := by exact add_le_add (mul_le_mul_of_nonneg_left hCS_T hC_nonneg) (mul_le_mul_of_nonneg_left hCS_F hC_nonneg) _ = aipw_rem_const ε * ∑ a : Bool, (eLpNorm (fun x => η.μ_fn a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => η.e_fn x - S.e_val x) 2 S.P_X).toReal := by simp [dμT, dμF, de] ring

theorem aipw_remainder_op (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (η_hat : ℕ → P.Ω → NuisanceVec γ) (h_in_H : ∀ n ω, η_hat n ω ∈ H_ε_aeL2 S ε) (hΔμ_memLp : ∀ n ω a, MemLp (fun x => (η_hat n ω).μ_fn a x - S.μ_val a 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_product_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a 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, aipwMomentFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ := by let rn : ℕ → ℝ := fun n => (n : ℝ) ^ (-(1 / 2 : ℝ)) let prodTerm : Bool → ℕ → P.Ω → ℝ := fun a n ω => (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal have hrn_nonneg : ∀ᶠ n : ℕ in atTop, 0 ≤ rn n := by filter_upwards with n exact Real.rpow_nonneg (Nat.cast_nonneg n) _ have hsum_rate : IsLittleOp (fun n ω => ∑ a : Bool, prodTerm a n ω) rn P.μ := by simpa [prodTerm, rn] using IsLittleOp.add_eventually_nonneg_rate (μ := P.μ) hrn_nonneg (h_product_rate true) (h_product_rate false) have hCpos : 0 < aipw_rem_const ε := by unfold aipw_rem_const have hden_pos : 0 < ε * (1 - ε) := by have h1 : 0 < 1 - ε := by linarith [h_overlap.2.1] exact mul_pos h_overlap.1 h1 positivity refine IsLittleOp.of_abs_le_const_mul (μ := P.μ) hCpos hsum_rate ?_ intro n ω have hsum_nonneg : 0 ≤ ∑ a : Bool, prodTerm a n ω := by refine sum_nonneg ?_ intro a ha exact mul_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg have hbound := aipw_remainder_bound S h_overlap hA h_y2 h_yd2 (η_hat n ω) (h_in_H n ω) (hΔμ_memLp n ω) (hΔe_memLp n ω) have hsum_nonneg' : 0 ≤ prodTerm true n ω + prodTerm false n ω := by simpa [prodTerm] using hsum_nonneg have habs_sum' : |prodTerm true n ω + prodTerm false n ω| = prodTerm true n ω + prodTerm false n ω := abs_of_nonneg hsum_nonneg' simpa [prodTerm, rn, habs_sum'] using hbound