Estimation.ATE.Score.AIPWScore­L2

theorem residual_mul_e_error_isLittleOp_one (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_e_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X) (h_e_rate : 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 : γ × Bool × ℝ => (|projY z - S.μ_val true (projX z)| + |projY z - S.μ_val false (projX z)|) * |(η_hat n ω).e_fn (projX z) - S.e_val (projX z)|) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by classical rcases h_overlap with ⟨hε_pos, _hε_half, _hprop⟩ haveI : IsProbabilityMeasure S.P_Z := by unfold BackdoorEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable let R : (γ × Bool × ℝ) → ℝ := fun z => |projY z - S.μ_val true (projX z)| + |projY z - S.μ_val false (projX z)| let deZ : ℕ → P.Ω → (γ × Bool × ℝ) → ℝ := fun n ω z => (η_hat n ω).e_fn (projX z) - S.e_val (projX z) have hR_meas : Measurable R := by simpa [R] using yMuVal_residual_meas 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 S hA h_y2 h_yd2 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 [BackdoorEstimationSystem.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_meas : ∀ n ω, Measurable (deZ n ω) := by intro n ω 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) have hdeZ_bdd : ∀ n ω, ∀ᵐ z ∂S.P_Z, |deZ n ω z| ≤ 1 := by intro n ω filter_upwards [H_ε_aeL2_overlap_P_Z S (h_in_H n ω)] with z hη have hη_nonneg : 0 ≤ (η_hat n ω).e_fn (projX z) := le_trans hε_pos.le hη.1 have hη_le_one : (η_hat n ω).e_fn (projX z) ≤ 1 := by linarith [hη.2, hε_pos.le] have hS_nonneg : 0 ≤ S.e_val (projX z) := le_of_lt (S.e_pos (projX z)) have hS_le_one : S.e_val (projX z) ≤ 1 := le_of_lt (S.e_lt_one (projX z)) dsimp [deZ] rw [abs_le] constructor <;> linarith intro δ hδ rw [ENNReal.tendsto_nhds_zero] intro κ hκ by_cases hκtop : κ = ⊤ · filter_upwards with n simp [hκtop] have hκpos : 0 < κ.toReal := ENNReal.toReal_pos (ne_of_gt hκ) hκtop let τ : ℝ := δ / 4 have hτpos : 0 < τ := by dsimp [τ] linarith obtain ⟨M, hMpos, hMtail⟩ := hR_memLp.eLpNorm_indicator_norm_ge_pos_le hR_meas.stronglyMeasurable hτpos let tail : (γ × Bool × ℝ) → ℝ := {z | M ≤ R z}.indicator R have htail_set : MeasurableSet {z : γ × Bool × ℝ | M ≤ R z} := by exact measurableSet_le measurable_const hR_meas have htail_memLp : MemLp tail 2 S.P_Z := by exact hR_memLp.indicator htail_set have htail_norm_le : (eLpNorm tail 2 S.P_Z).toReal ≤ τ := by have hle : eLpNorm tail 2 S.P_Z ≤ ofReal τ := by have htail_eq : tail = ({z : γ × Bool × ℝ | M ≤ ‖R z‖₊}.indicator R) := by funext z by_cases hz : M ≤ R z · simp [tail, hz, Real.norm_eq_abs, abs_of_nonneg (hR_nonneg z)] · simp [tail, hz, Real.norm_eq_abs, abs_of_nonneg (hR_nonneg z)] simpa [htail_eq] using hMtail calc (eLpNorm tail 2 S.P_Z).toReal ≤ (ofReal τ).toReal := ENNReal.toReal_mono ENNReal.ofReal_ne_top hle _ = τ := ENNReal.toReal_ofReal hτpos.le have hcross_bound : ∀ n ω, (eLpNorm (fun z : γ × Bool × ℝ => R z * |deZ n ω z|) 2 S.P_Z).toReal ≤ M * (eLpNorm (deZ n ω) 2 S.P_Z).toReal + τ := by intro n ω let bulk : (γ × Bool × ℝ) → ℝ := fun z => M * |deZ n ω z| let upper : (γ × Bool × ℝ) → ℝ := fun z => bulk z + tail z have hbulk_memLp : MemLp bulk 2 S.P_Z := by have h_abs : MemLp (fun z => |deZ n ω z|) 2 S.P_Z := by simpa [Real.norm_eq_abs] using (hdeZ_memLp n ω).norm exact h_abs.const_smul M have hupper_memLp : MemLp upper 2 S.P_Z := by exact hbulk_memLp.add htail_memLp have hpoint : ∀ᵐ z ∂S.P_Z, ‖R z * |deZ n ω z|‖ ≤ upper z := by filter_upwards [hdeZ_bdd n ω] with z hdez_le have hRz : 0 ≤ R z := hR_nonneg z have hdez_nonneg : 0 ≤ |deZ n ω z| := abs_nonneg _ by_cases hz : M ≤ R z · have htail_eq : tail z = R z := by simp [tail, hz] have hmain : ‖R z * |deZ n ω z|‖ ≤ R z := by rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg hRz, abs_of_nonneg hdez_nonneg] exact mul_le_of_le_one_right hRz hdez_le dsimp [upper, bulk] rw [htail_eq] have hbulk_nonneg : 0 ≤ M * |deZ n ω z| := mul_nonneg hMpos.le hdez_nonneg exact hmain.trans (by nlinarith) · have htail_eq : tail z = 0 := by simp [tail, hz] have hR_lt_M : R z ≤ M := by exact le_of_not_ge hz have hmain : ‖R z * |deZ n ω z|‖ ≤ M * |deZ n ω z| := by rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg hRz, abs_of_nonneg hdez_nonneg] exact mul_le_mul_of_nonneg_right hR_lt_M hdez_nonneg dsimp [upper, bulk] rw [htail_eq] simpa using hmain have hmono : (eLpNorm (fun z : γ × Bool × ℝ => R z * |deZ n ω z|) 2 S.P_Z).toReal ≤ (eLpNorm upper 2 S.P_Z).toReal := by exact ENNReal.toReal_mono hupper_memLp.eLpNorm_ne_top (eLpNorm_mono_ae_real hpoint) have htri : lpNorm upper 2 S.P_Z ≤ lpNorm bulk 2 S.P_Z + lpNorm tail 2 S.P_Z := by exact lpNorm_add_le (f := bulk) (g := tail) (μ := S.P_Z) hbulk_memLp (by norm_num : (1 : ENNReal) ≤ 2) have hbulk_norm : lpNorm bulk 2 S.P_Z = M * (eLpNorm (deZ n ω) 2 S.P_Z).toReal := by change lpNorm (M • (fun z : γ × Bool × ℝ => |deZ n ω z|)) 2 S.P_Z = M * (eLpNorm (deZ n ω) 2 S.P_Z).toReal rw [lpNorm_const_smul] rw [lpNorm_fun_abs (hdeZ_memLp n ω).aestronglyMeasurable] rw [← toReal_eLpNorm (hdeZ_memLp n ω).aestronglyMeasurable] have hcoef : (↑‖M‖₊ : ℝ) = M := by simp [Real.norm_eq_abs, abs_of_pos hMpos] rw [hcoef] have htail_lp : lpNorm tail 2 S.P_Z = (eLpNorm tail 2 S.P_Z).toReal := by rw [toReal_eLpNorm htail_memLp.aestronglyMeasurable] calc (eLpNorm (fun z : γ × Bool × ℝ => R z * |deZ n ω z|) 2 S.P_Z).toReal ≤ (eLpNorm upper 2 S.P_Z).toReal := hmono _ = lpNorm upper 2 S.P_Z := by rw [toReal_eLpNorm hupper_memLp.aestronglyMeasurable] _ ≤ lpNorm bulk 2 S.P_Z + lpNorm tail 2 S.P_Z := htri _ = M * (eLpNorm (deZ n ω) 2 S.P_Z).toReal + (eLpNorm tail 2 S.P_Z).toReal := by rw [hbulk_norm, htail_lp] _ ≤ M * (eLpNorm (deZ n ω) 2 S.P_Z).toReal + τ := add_le_add_right htail_norm_le (M * (eLpNorm (deZ n ω) 2 S.P_Z).toReal) have hsmall := (ENNReal.tendsto_nhds_zero.mp (h_e_rate (δ / (2 * M)) (by positivity))) κ hκ filter_upwards [hsmall] with n hn refine (measure_mono ?_).trans hn intro ω hω have hnorm_nonneg : 0 ≤ (eLpNorm (fun z : γ × Bool × ℝ => R z * |deZ n ω z|) 2 S.P_Z).toReal := ENNReal.toReal_nonneg have hnorm_large : δ ≤ (eLpNorm (fun z : γ × Bool × ℝ => R z * |deZ n ω z|) 2 S.P_Z).toReal := by simpa [R, deZ, abs_of_nonneg hnorm_nonneg] using hω have hde_large : δ / (2 * M) ≤ (eLpNorm (deZ n ω) 2 S.P_Z).toReal := by have hb := hcross_bound n ω by_contra hnot have hle : (eLpNorm (deZ n ω) 2 S.P_Z).toReal ≤ δ / (2 * M) := (lt_of_not_ge hnot).le have hprod_le : M * (eLpNorm (deZ n ω) 2 S.P_Z).toReal ≤ δ / 2 := by calc M * (eLpNorm (deZ n ω) 2 S.P_Z).toReal ≤ M * (δ / (2 * M)) := mul_le_mul_of_nonneg_left hle hMpos.le _ = δ / 2 := by field_simp [hMpos.ne'] have hcross_le : (eLpNorm (fun z : γ × Bool × ℝ => R z * |deZ n ω z|) 2 S.P_Z).toReal ≤ δ / 2 + τ := by exact hb.trans (add_le_add hprod_le le_rfl) dsimp [τ] at hcross_le nlinarith [hnorm_large] have heq_norm : (eLpNorm (deZ n ω) 2 S.P_Z).toReal = (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal := by simpa [deZ] using e_error_eLpNorm_projX_toReal_eq S (η_hat n ω) (h_e_memLp n ω) have hde_large_X : δ / (2 * M) ≤ (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal := by simpa [heq_norm] using hde_large have hde_nonneg : 0 ≤ (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal := ENNReal.toReal_nonneg simpa [abs_of_nonneg hde_nonneg] using hde_large_X

theorem aipw_score_diff_pointwise_bound (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (η : NuisanceVec γ) (hη : η ∈ H_ε_aeL2 S ε) : ∀ᵐ z ∂S.P_Z, |aipwMomentFunctional η z S.θ₀ - aipwMomentFunctional S.η₀ z S.θ₀| ≤ K_AIPW ε * (|η.μ_fn true (projX z) - S.μ_val true (projX z)| + |η.μ_fn false (projX z) - S.μ_val false (projX z)| + (|projY z - S.μ_val true (projX z)| + |projY z - S.μ_val false (projX z)|) * |η.e_fn (projX z) - S.e_val (projX z)|) := by rcases h_overlap with ⟨hε_pos, _hε_half, hprop⟩ have h_e_ω : ∀ᵐ ω ∂P.μ, ε ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) ∧ S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by filter_upwards [hprop, S.e_compat] with ω hω hcompat rw [hcompat] at hω exact hω have h_e_z : ∀ᵐ z ∂S.P_Z, ε ≤ S.e_val (projX z) ∧ S.e_val (projX z) ≤ 1 - ε := by have hset : MeasurableSet {z : γ × Bool × ℝ | ε ≤ S.e_val (projX z) ∧ S.e_val (projX z) ≤ 1 - ε} := by have hx : Measurable (fun z : γ × Bool × ℝ => projX z) := by simpa [projX] using (measurable_fst : Measurable (fun z : γ × Bool × ℝ => z.1)) exact measurableSet_Icc.preimage (S.e_meas.comp hx) unfold BackdoorEstimationSystem.P_Z rw [MeasureTheory.ae_map_iff S.measurable_factualZ.aemeasurable hset] filter_upwards [h_e_ω] with ω hω simpa [BackdoorEstimationSystem.factualZ, projX] using hω have hη_z : ∀ᵐ z ∂S.P_Z, ε ≤ η.e_fn (projX z) ∧ η.e_fn (projX z) ≤ 1 - ε := H_ε_aeL2_overlap_P_Z S hη filter_upwards [h_e_z, hη_z] with z hz hηz simpa [aipwMomentFunctional, aipwMoment, η₀, indA] using (aipw_real_bound (a := projA z) (ε := ε) (e := S.e_val (projX z)) (ê := η.e_fn (projX z)) (μT := S.μ_val true (projX z)) (μF := S.μ_val false (projX z)) (μhT := η.μ_fn true (projX z)) (μhF := η.μ_fn false (projX z)) (y := projY z) (θ := S.θ₀) hε_pos hz hηz)

theorem aipw_score_diff_isLittleOp_one (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_mu_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_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_e_rate : 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 => aipwMomentFunctional (η_hat n ω) z S.θ₀ - aipwMomentFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by exact aipw_score_diff_isLittleOp_one_truncation_core S h_overlap hA h_y2 h_yd2 η_hat h_in_H h_mu_memLp h_e_memLp h_mu_rate h_e_rate