Estimation.ATT

theorem θ₀_eq_ATT (S : TreatedEstimationSystem P γ) (hA : S.toPOBackdoorSystem.ATTAssumptions) : S.θ₀ = S.toPOBackdoorSystem.ATT := by unfold θ₀ exact (S.toPOBackdoorSystem.ATT_eq_adjustedATT hA).symm

theorem att_dml_isAsymLinear (S : TreatedEstimationSystem P γ) {ε : ℝ} (hη₀_mem : S.η₀ ∈ H_ε S ε) (h_e_lb : ∀ x, 0 ≤ S.e_val x) (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.μ) (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.μ) (sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (_hc_lt : c < 1) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_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_diff_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X) (h_e_diff_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X) (h_IPW_at : ∀ 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_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀)) (h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => aipwMomentATTFunctional (η_hat n ω) z S.θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀)) (h_m_int : ∀ n ω, Integrable (fun z => aipwMomentATTFunctional (η_hat n ω) z S.θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => (aipwMomentATTFunctional (η_hat n ω) z S.θ₀) ^ 2) S.P_Z) (h_indiv_rate_ρ₁ : IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ) (h_indiv_rate_ρ₂ : IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * (((attGeneralMoment S hη₀_mem hπ_pos).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) : IsAsymLinear (dmlChernozhukovEstimator (attGeneralMoment S hη₀_mem hπ_pos) sample split η_hat) S.θ₀ (fun z => -(attGeneralMoment S hη₀_mem hπ_pos).J₀_inv * aipwMomentATTFunctional S.η₀ z S.θ₀) sample split.foldB := by have hMZ := att_meanZero S hη₀_mem h_overlap hA hπ_pos h_y2 h_y0_2 hIPW have hFV : Integrable (fun z => ((attGeneralMoment S hη₀_mem hπ_pos).m (attGeneralMoment S hη₀_mem hπ_pos).η₀ z (attGeneralMoment S hη₀_mem hπ_pos).θ₀) ^ 2) S.P_Z := by simpa [attGeneralMoment, ψ_ATT, η₀, aipwMomentATTFunctional] using aipw_finite_var_ATT S h_overlap hA h_y2 h_y0_2 have hBR_at : ∀ n ω, |∫ z, (attGeneralMoment S hη₀_mem hπ_pos).m (η_hat n ω) z (attGeneralMoment S hη₀_mem hπ_pos).θ₀ ∂S.P_Z| ≤ aipw_rem_const_ATT ε * (((attGeneralMoment S hη₀_mem hπ_pos).ρ₁ (η_hat n ω) (attGeneralMoment S hη₀_mem hπ_pos).η₀ : NNReal) : ℝ) * (((attGeneralMoment S hη₀_mem hπ_pos).ρ₂ (η_hat n ω) (attGeneralMoment S hη₀_mem hπ_pos).η₀ : NNReal) : ℝ) := by intro n ω have h := aipw_remainder_bound_ATT S h_overlap hA hπ_pos h_y2 h_y0_2 (η_hat n ω) (h_in_Hε n ω) (h_mu_diff_memLp n ω) (h_e_diff_memLp n ω) (h_IPW_at n ω) change |∫ 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 exact h have h_mu_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ := by exact h_indiv_rate_ρ₁ have 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.μ := by exact h_indiv_rate_ρ₂ have h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => (attGeneralMoment S hη₀_mem hπ_pos).m (η_hat n ω) z (attGeneralMoment S hη₀_mem hπ_pos).θ₀ - (attGeneralMoment S hη₀_mem hπ_pos).m (attGeneralMoment S hη₀_mem hπ_pos).η₀ z (attGeneralMoment S hη₀_mem hπ_pos).θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by simpa [attGeneralMoment] using aipw_score_diff_isLittleOp_one_ATT S h_overlap hη₀_mem h_e_lb hA h_y2 h_y0_2 η_hat h_in_Hε h_e_lb_hat h_mu_diff_memLp h_e_diff_memLp h_mu_rate h_e_rate simpa [attGeneralMoment] using (dml_chernozhukov_asymptoticLinear (attGeneralMoment S hη₀_mem hπ_pos) hMZ hFV sample split hc_pos h_split_rate η_hat (Crem := aipw_rem_const_ATT ε) hBR_at h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate)

theorem dml_ATT_isAsymLinear (S : TreatedEstimationSystem P γ) {ε : ℝ} (h_e_overlap : ∀ᵐ x ∂S.P_X, S.e_val x ≤ 1 - ε) (h_e_lb : ∀ x, 0 ≤ S.e_val x) (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.μ) (sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (hc_lt : c < 1) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (μ₀_hat : ℕ → P.Ω → (γ → ℝ)) (e_hat : ℕ → P.Ω → (γ → ℝ)) (h_e_hat_overlap : ∀ n ω, ∀ᵐ x ∂S.P_X, e_hat n ω x ≤ 1 - ε) (h_e_hat_lb : ∀ n ω x, 0 ≤ e_hat n ω x) (h_μ₀_meas : ∀ n, Measurable (fun (p : P.Ω × γ) => μ₀_hat n p.1 p.2)) (h_e_meas : ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_μ₀_memLp : ∀ n ω, MemLp (fun x => μ₀_hat n ω x) 2 S.P_X) (h_e_memLp : ∀ n ω, MemLp (fun x => e_hat n ω x) 2 S.P_X) (h_μ₀_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (μ₀_hat n)) (h_e_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (e_hat n)) (h_μ₀_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => μ₀_hat n p.1 p.2)) (h_e_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_m_int : ∀ n ω, Integrable (fun z => aipwMomentATT z (μ₀_hat n ω) (e_hat n ω) S.θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => (aipwMomentATT z (μ₀_hat n ω) (e_hat n ω) S.θ₀) ^ 2) S.P_Z) (h_mu_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => μ₀_hat n ω x - S.μ₀_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_e_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => μ₀_hat n ω x - S.μ₀_val x) 2 S.P_X).toReal * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) : IsAsymLinear (dmlEstimator_ATT S sample split μ₀_hat e_hat) S.θ₀ S.ψ_ATT sample split.foldB := by -- 0. Discharge the truth-nuisance IPW integrability gate from overlap + L². have hIPW := ipw_truth_integrable S h_overlap hA h_y2 h_y0_2 -- 1. Build the abstract `η_hat : ℕ → P.Ω → TreatedNuisanceVec γ`. let η_hat : ℕ → P.Ω → TreatedNuisanceVec γ := fun n ω => { μ₀_fn := μ₀_hat n ω e_fn := e_hat n ω μ₀_meas := (h_μ₀_meas n).comp (Measurable.prodMk measurable_const measurable_id) e_meas := (h_e_meas n).comp (Measurable.prodMk measurable_const measurable_id) } -- `S.P_X` is a probability measure (used by `MemLp.of_bound` for `S.e_val`). haveI : IsProbabilityMeasure S.P_X := by unfold TreatedEstimationSystem.P_X exact Measure.isProbabilityMeasure_map S.toPOBackdoorSystem.measurable_factualX.aemeasurable -- `S.P_Z` is a probability measure (used by score integrability transport). haveI : IsProbabilityMeasure S.P_Z := by unfold TreatedEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable -- 2. Per-η̂ L² differences for the abstract remainder bound. have hμ₀_val_memLp : MemLp S.μ₀_val 2 S.P_X := by have hY0_L2 : MemLp (S.toPOBackdoorSystem.YofD false) 2 P.μ := (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) have hcomp_L2 : MemLp (fun ω => S.μ₀_val (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := hcond_L2.ae_eq (S.μ₀_compat hA) rw [TreatedEstimationSystem.P_X] exact (memLp_map_measure_iff S.μ₀_meas.aestronglyMeasurable S.toPOBackdoorSystem.measurable_factualX.aemeasurable).2 hcomp_L2 have he_val_memLp : MemLp S.e_val 2 S.P_X := by refine MemLp.of_bound S.e_meas.aestronglyMeasurable 1 ?_ filter_upwards [h_e_overlap] with x hx rw [Real.norm_eq_abs] exact abs_le.mpr ⟨by linarith [h_e_lb x], by linarith [hx, h_overlap.1]⟩ have he_val_memLp_top : MemLp S.e_val ⊤ S.P_X := by refine MemLp.of_bound S.e_meas.aestronglyMeasurable 1 ?_ filter_upwards [h_e_overlap] with x hx rw [Real.norm_eq_abs] exact abs_le.mpr ⟨by linarith [h_e_lb x], by linarith [hx, h_overlap.1]⟩ have hη₀_mem : S.η₀ ∈ H_ε S ε := by refine ⟨h_e_overlap, ?_, ?_⟩ · simpa [TreatedEstimationSystem.η₀] using hμ₀_val_memLp · simpa [TreatedEstimationSystem.η₀] using he_val_memLp_top have h_in_Hε : ∀ n ω, η_hat n ω ∈ H_ε S ε := by intro n ω refine ⟨h_e_hat_overlap n ω, ?_, ?_⟩ · simpa [η_hat] using h_μ₀_memLp n ω · refine MemLp.of_bound (η_hat n ω).e_meas.aestronglyMeasurable 1 ?_ filter_upwards [h_e_hat_overlap n ω] with x hx rw [Real.norm_eq_abs] exact abs_le.mpr ⟨by linarith [h_e_hat_lb n ω x], by linarith [hx, h_overlap.1]⟩ have h_mu_diff_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X := by intro n ω exact (h_μ₀_memLp n ω).sub hμ₀_val_memLp have h_e_diff_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X := by intro n ω exact (h_e_memLp n ω).sub he_val_memLp -- 3. Translate score measurability to the abstract interface. have h_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀) := by intro n unfold aipwMomentATTFunctional aipwMomentATT unfold indA projX projA projY dsimp [η_hat] have hA : Measurable (fun p : P.Ω × (γ × Bool × ℝ) => p.2.2.1) := measurable_snd.snd.fst have hY : Measurable (fun p : P.Ω × (γ × Bool × ℝ) => p.2.2.2) := measurable_snd.snd.snd have hproj : Measurable (fun p : P.Ω × (γ × Bool × ℝ) => (p.1, p.2.1)) := Measurable.prodMk measurable_fst measurable_snd.fst have hμ : Measurable (fun p : P.Ω × (γ × Bool × ℝ) => μ₀_hat n p.1 p.2.1) := (h_μ₀_meas n).comp hproj have he : Measurable (fun p : P.Ω × (γ × Bool × ℝ) => e_hat n p.1 p.2.1) := (h_e_meas n).comp hproj have hindA : Measurable (fun p : P.Ω × (γ × Bool × ℝ) => if p.2.2.1 = true then (1 : ℝ) else 0) := by refine Measurable.ite ?_ measurable_const measurable_const exact hA (MeasurableSet.singleton true) have hOne : Measurable (fun _ : P.Ω × (γ × Bool × ℝ) => (1 : ℝ)) := measurable_const have hθ : Measurable (fun _ : P.Ω × (γ × Bool × ℝ) => S.θ₀) := measurable_const simpa [mul_assoc] using (((hindA.fun_mul (hY.fun_sub hμ)).fun_sub ((hOne.fun_sub hindA).fun_mul ((he.fun_div (hOne.fun_sub he)).fun_mul (hY.fun_sub hμ)))).fun_sub (hindA.fun_mul hθ)) have h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => aipwMomentATTFunctional (η_hat n ω) z S.θ₀) := by intro n unfold aipwMomentATTFunctional aipwMomentATT unfold indA projX projA projY dsimp [η_hat] fun_prop have h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀) := by intro n change Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] -- … truncated; follow the source link for the rest …