Estimation.ATE

lemma μ_compat (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (d : Bool) : P.μ[S.toPOBackdoorSystem.YofD d | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) := (S.toPOBackdoorSystem.conditionalMeanOutcome_backdoor hA d).trans (S.μ_reg_compat d).symm

@[fun_prop] lemma measurable_factualZ (S : BackdoorEstimationSystem P γ) : Measurable S.factualZ := (S.toPOBackdoorSystem.measurable_factualX).prodMk ((S.toPOBackdoorSystem.measurable_factualD).prodMk S.toPOBackdoorSystem.measurable_factualY)

lemma P_Z_map_projX_eq_P_X (S : BackdoorEstimationSystem P γ) : S.P_Z.map (fun z : γ × Bool × ℝ => z.1) = S.P_X := by unfold BackdoorEstimationSystem.P_Z BackdoorEstimationSystem.P_X rw [Measure.map_map (by fun_prop : Measurable (fun z : γ × Bool × ℝ => z.1)) S.measurable_factualZ] rfl

theorem plugInOracle_isAsymLinear (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (μ_hat : ℕ → P.Ω → (Bool → γ → ℝ)) (h_mu_meas : ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_mu_memLp : ∀ n ω a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X) (h_mu_uncurry_foldA : ∀ n a, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_rate : IsLittleOp (fun n ω => sqrt (∑ a : Bool, (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal ^ 2)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) : IsAsymLinear (plugInEstimator S sample split μ_hat) S.θ₀ (ψ_plugin S) sample split.foldB := by refine ⟨?_, ?_, ?_⟩ · -- mean_zero: `ψ_plugin = (μ_val 1 - μ_val 0) - θ₀` integrates to `θ₀ - θ₀ = 0`. have hψ_meas : Measurable (ψ_plugin S) := by unfold ψ_plugin exact ((S.μ_meas true).comp measurable_fst).sub ((S.μ_meas false).comp measurable_fst) |>.sub measurable_const rw [BackdoorEstimationSystem.P_Z, MeasureTheory.integral_map S.measurable_factualZ.aemeasurable hψ_meas.aestronglyMeasurable] have hbase_int : Integrable (fun ω => S.μ_val true (S.toPOBackdoorSystem.factualX ω) - S.μ_val false (S.toPOBackdoorSystem.factualX ω)) P.μ := by have hcate : ∀ d, Integrable (S.toPOBackdoorSystem.conditionalMeanOutcome d) P.μ := fun d => by unfold POBackdoorSystem.conditionalMeanOutcome exact MeasureTheory.integrable_condExp have h1 : Integrable (fun ω => S.μ_val true (S.toPOBackdoorSystem.factualX ω)) P.μ := (hcate true).congr (S.μ_compat hA true) have h0 : Integrable (fun ω => S.μ_val false (S.toPOBackdoorSystem.factualX ω)) P.μ := (hcate false).congr (S.μ_compat hA false) exact h1.sub h0 have hθ_int : Integrable (fun _ : P.Ω => (S.θ₀ : ℝ)) P.μ := integrable_const _ have hθ_const : (∫ _ : P.Ω, (S.θ₀ : ℝ) ∂P.μ) = S.θ₀ := by haveI : IsProbabilityMeasure P.μ := inferInstance simp show ∫ ω, ψ_plugin S (S.factualZ ω) ∂P.μ = 0 have heq : (fun ω => ψ_plugin S (S.factualZ ω)) = (fun ω => (S.μ_val true (S.toPOBackdoorSystem.factualX ω) - S.μ_val false (S.toPOBackdoorSystem.factualX ω)) - S.θ₀) := by funext ω; rfl rw [heq] integral_linearity rw [← theta_zero_factualX_integral S, hθ_const] ring · -- finite_var: ψ_plugin = (μ_val 1 ∘ X) − (μ_val 0 ∘ X) − θ₀ ∈ L²(P_Z). -- L² of `μ_val d ∘ factualX` follows from `h_yd2` via conditional Jensen -- (cf. `aipw_finite_var`); push to `P_Z` along `factualZ`. have hψ_meas : Measurable (ψ_plugin S) := by unfold ψ_plugin exact (((S.μ_meas true).comp measurable_fst).sub ((S.μ_meas false).comp measurable_fst)).sub measurable_const have hμ_L2 : ∀ d : Bool, MemLp (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := by intro d have hYd_L2 : MemLp (S.toPOBackdoorSystem.YofD d) 2 P.μ := (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 (S.μ_compat hA d) have hψ_comp_L2 : MemLp (fun ω => ψ_plugin S (S.factualZ ω)) 2 P.μ := by have hbase_L2 := (hμ_L2 true).sub (hμ_L2 false) have hconst_L2 : MemLp (fun _ : P.Ω => S.θ₀) 2 P.μ := memLp_const _ simp only [ψ_plugin, BackdoorEstimationSystem.factualZ, projX] exact hbase_L2.sub hconst_L2 have hψ_L2 : MemLp (ψ_plugin S) 2 S.P_Z := by rw [BackdoorEstimationSystem.P_Z] exact (memLp_map_measure_iff hψ_meas.aestronglyMeasurable S.measurable_factualZ.aemeasurable).2 hψ_comp_L2 exact hψ_L2.integrable_sq · -- remainder: decompose into centered fold-B fluctuation plus plug-in bias. let δ : ℕ → P.Ω → γ → ℝ := fun n ω x => (μ_hat n ω true x - S.μ_val true x) - (μ_hat n ω false x - S.μ_val false x) let G : ℕ → P.Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (δ n ω (projX (sample.Z i ω)) - ∫ x, δ n ω x ∂S.P_X) let B : ℕ → P.Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * ∫ x, δ n ω x ∂S.P_X let R : ℕ → P.Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * (plugInEstimator S sample split μ_hat n ω - S.θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, ψ_plugin S (sample.Z i ω) have hG : IsLittleOp G (fun _ => (1 : ℝ)) P.μ := by let fZ : ℕ → P.Ω → γ × Bool × ℝ → ℝ := fun n ω z => δ n ω (projX z) haveI : IsProbabilityMeasure S.P_Z := by unfold BackdoorEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable have hf_meas : ∀ n, Measurable (uncurry (fZ n)) := by intro n change Measurable (fun p : P.Ω × (γ × Bool × ℝ) => (μ_hat n p.1 true p.2.1 - S.μ_val true p.2.1) - (μ_hat n p.1 false p.2.1 - S.μ_val false p.2.1)) have hproj : Measurable (fun p : P.Ω × (γ × Bool × ℝ) => (p.1, p.2.1)) := by fun_prop exact (((h_mu_meas n true).comp hproj).sub ((S.μ_meas true).comp measurable_snd.fst)).sub (((h_mu_meas n false).comp hproj).sub ((S.μ_meas false).comp measurable_snd.fst)) have hf_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (uncurry (fZ n)) := by intro n change Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (fun (p : P.Ω × (γ × Bool × ℝ)) => (μ_hat n p.1 true p.2.1 - S.μ_val true p.2.1) - (μ_hat n p.1 false p.2.1 - S.μ_val false p.2.1)) let mA : MeasurableSpace P.Ω := comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance have hx : @Measurable (P.Ω × (γ × Bool × ℝ)) γ (mA.prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))) inferInstance (fun p => p.2.1) := measurable_snd.fst have hproj : @Measurable (P.Ω × (γ × Bool × ℝ)) (P.Ω × γ) (mA.prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))) (mA.prod (inferInstance : MeasurableSpace γ)) (fun p => (p.1, p.2.1)) := prodMk measurable_fst hx exact (((h_mu_uncurry_foldA n true).comp hproj).sub ((S.μ_meas true).comp hx)).sub (((h_mu_uncurry_foldA n false).comp hproj).sub ((S.μ_meas false).comp hx)) have hf_memLp : ∀ n ω, MemLp (fZ n ω) 2 S.P_Z := by have hμ_val_memLp : ∀ a : Bool, MemLp (S.μ_val a) 2 S.P_X := by intro a have hY_L2 : MemLp (S.toPOBackdoorSystem.YofD a) 2 P.μ := (memLp_two_iff_integrable_sq (S.toPOBackdoorSystem.measurable_YofD a).aestronglyMeasurable).2 (h_yd2 a) have hcond_L2 : MemLp (P.μ[S.toPOBackdoorSystem.YofD a | S.toPOBackdoorSystem.sigmaX]) 2 P.μ := hY_L2.condExp one_le_two have hcomp_L2 : MemLp (fun ω => S.μ_val a (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := hcond_L2.ae_eq (S.μ_compat hA a) rw [BackdoorEstimationSystem.P_X] exact (memLp_map_measure_iff (S.μ_meas a).aestronglyMeasurable S.toPOBackdoorSystem.measurable_factualX.aemeasurable).2 hcomp_L2 intro n ω have hδ_memLp : MemLp (δ n ω) 2 S.P_X := by exact ((h_mu_memLp n ω true).sub (hμ_val_memLp true)).sub ((h_mu_memLp n ω false).sub (hμ_val_memLp false)) have hmap : MemLp (δ n ω) 2 (S.P_Z.map (fun z : γ × Bool × ℝ => z.1)) := by simpa [BackdoorEstimationSystem.P_Z_map_projX_eq_P_X S] using hδ_memLp have hδ_aestrong : AEStronglyMeasurable (δ n ω) (S.P_Z.map (fun z : γ × Bool × ℝ => z.1)) := hmap.aestronglyMeasurable have hproj_ae : AEMeasurable (fun z : γ × Bool × ℝ => z.1) S.P_Z := measurable_fst.aemeasurable exact (memLp_map_measure_iff hδ_aestrong hproj_ae).1 hmap have hf_rate_one : IsLittleOp (fun n ω => (eLpNorm (fZ n ω) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by have hμ_val_memLp : ∀ a : Bool, MemLp (S.μ_val a) 2 S.P_X := by intro a have hY_L2 : MemLp (S.toPOBackdoorSystem.YofD a) 2 P.μ := (memLp_two_iff_integrable_sq (S.toPOBackdoorSystem.measurable_YofD a).aestronglyMeasurable).2 (h_yd2 a) have hcond_L2 : MemLp (P.μ[S.toPOBackdoorSystem.YofD a | S.toPOBackdoorSystem.sigmaX]) 2 P.μ := hY_L2.condExp one_le_two have hcomp_L2 : MemLp (fun ω => S.μ_val a (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := hcond_L2.ae_eq (S.μ_compat hA a) rw [BackdoorEstimationSystem.P_X] exact (memLp_map_measure_iff (S.μ_meas a).aestronglyMeasurable S.toPOBackdoorSystem.measurable_factualX.aemeasurable).2 hcomp_L2 have hnorm_bound : ∀ n ω, (eLpNorm (fZ n ω) 2 S.P_Z).toReal ≤ 2 * sqrt (∑ a : Bool, (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal ^ 2) := by intro n ω let dμ : Bool → γ → ℝ := fun a x => μ_hat n ω a x - S.μ_val a x have hdμ_memLp : ∀ a, MemLp (dμ a) 2 S.P_X := fun a => by exact (h_mu_memLp n ω a).sub (hμ_val_memLp a) -- … truncated; follow the source link for the rest …