Estimation.ATT.DML
This file defines the population-share oracle comparison for the one-shot sample-split augmented inverse-probability weighted estimator of the back-door average treatment effect on the treated.
DML 2 core · 2 supporting This file defines the population-share oracle comparison for the one-shot sample-split augmented inverse-probability weighted estimator of the back-door average treatment effect on the treated. ★ oracleEstimator_ATT_isAsymLinear
Double Machine Learning for ATT
This file defines the population-share oracle comparison for the one-shot
sample-split augmented inverse-probability weighted estimator of the back-door
average treatment effect on the treated. The theorem connects the oracle
to the ATT AIPW influence function under the one-sided ATT back-door assumption
bundle, an additional one-sided upper-overlap bound, second-moment,
sample-split, and nuisance-rate conditions. Parallel to
Estimation/ATE/DML.lean.
The main declarations are oracleEstimator_ATT, the derived influence-function
facts ψ_ATT_integral_zero and ψ_ATT_finite_var, and the production wrapper
oracleEstimator_ATT_isAsymLinear, which transports the abstract
att_oneStepOracleDML_isAsymLinear result to the population-π ATT estimator.
def oracleEstimator_ATT reviewed
⚑ flagged
Causalean.Estimation.ATT
For a potential-outcomes system with a standard Borel sample space and finite probability measure, a measurable covariate space, a treated estimation system, an independent and identically distributed sample of observed covariate, treatment, and outcome triples from that system's observed-data distribution, a one-shot split of that sample, a sequence of control-arm outcome-regression estimators, a sequence of propensity-score estimators, and a sample-size index, the population-treated-share oracle ATT estimator is the marginal-treatment-probability-normalized mean, over the split's evaluation fold at that index, of the ATT AIPW score evaluated at zero using the supplied nuisance functions at that index.
Definition (Lean source)
parameters
γ :
Type u_1
S :
split :
OneShotSplit sample
μ₀_hat :
ℕ → P.Ω → (γ → ℝ)
e_hat :
ℕ → P.Ω → (γ → ℝ)
n :
ℕ
def
oracleEstimator_ATT S sample split μ₀_hat e_hat n :
P.Ω → ℝ
given by
fun ω
=> (1 / S.π_val) * (((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, aipwMomentATT (sample.Z i ω) (μ₀_hat n ω) (e_hat n ω) 0)
theorem oracleEstimator_ATT_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.ATT
Asymptotic linearity of the population-share oracle estimator of the average treatment effect on the treated (ATT). For a potential-outcomes system, a measurable covariate space, a treated estimation system, and an overlap margin ε, fix sequences of control-regression fits and propensity fits, an i.i.d. sample of the covariate–treatment–outcome triple, and a one-shot split of that sample into a training fold and an evaluation fold. Under the true propensity score bounded above by 1 − ε almost everywhere under the covariate law, nonnegativity of the true propensity score, one-sided overlap with margin ε for the true propensity score, the one-sided back-door assumptions for the ATT, a strictly positive marginal treatment probability, square-integrability of the observed outcome and of the untreated potential outcome Y(0), and a limit c that is positive and to which the evaluation-fold share of the sample converges: if every fitted propensity is bounded above by 1 − ε almost everywhere under the covariate law, every fitted propensity is nonnegative everywhere, both fits are jointly measurable in the realization and the covariate, both fits are square-integrable under the covariate law at every realization, both fits are measurable with respect to the product of the σ-algebra generated by the training-fold observations and the covariate σ-algebra, the ATT score at every fitted pair and the true ATT is integrable and square-integrable under the observed-data law, the L² errors of the control-regression and propensity fits under the covariate law are each o_p(1), and their product is o_p(n^(−1/2)), then the one-shot augmented inverse-probability-weighted ATT estimator that divides by the population treatment probability is asymptotically linear at the true ATT along the evaluation fold, with the ATT augmented inverse-probability-weighted influence function.
Formal statement
hypotheses
γ :
Type u_1
S :
ε :
ℝ
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.μ
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < 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_μ₀_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.μ
conclusion
IsAsymLinear (oracleEstimator_ATT S sample split μ₀_hat e_hat) S.θ₀ S.ψ_ATT sample split.foldB
Proof (Lean source)
theorem oracleEstimator_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)
(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_μ₀_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
(oracleEstimator_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_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 × ℝ))]
(fun (p : P.Ω × (γ × Bool × ℝ)) =>
aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀)
unfold aipwMomentATTFunctional aipwMomentATT
unfold indA
projX
projA
projY
dsimp [η_hat]
let mA : MeasurableSpace P.Ω :=
comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance
have hproj :
@Measurable (P.Ω × (γ × Bool × ℝ)) (P.Ω × γ)
(mA.prod (inferInstance : MeasurableSpace (γ × Bool × ℝ)))
(mA.prod (inferInstance : MeasurableSpace γ))
(fun p => (p.1, p.2.1)) := by
have hx :
@Measurable (P.Ω × (γ × Bool × ℝ)) γ
(mA.prod (inferInstance : MeasurableSpace (γ × Bool × ℝ)))
inferInstance
(fun p => p.2.1) := measurable_snd.fst
exact Measurable.prodMk measurable_fst hx
have hμ :
Measurable (fun p : P.Ω × (γ × Bool × ℝ) => μ₀_hat n p.1 p.2.1) :=
-- … truncated; follow the source link for the rest …
2 supporting declarations (lemmas, instances)
-
ψ_ATT_integral_zerotheorem — Mean zero of the centered population-π ATT influence function ψ_ATT.hypothesesγ :sharedType u_1S :ε :ℝh_overlap :S.OneSidedOverlap εhA :S.toPOBackdoorSystem.ATTAssumptionshπ_pos :0 < S.π_valh_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.μconclusion∫ z, S.ψ_ATT z ∂(S.P_Z) = 0Proof (Lean source)
theorem ψ_ATT_integral_zero (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.μ) (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.μ) : ∫ z, S.ψ_ATT z ∂(S.P_Z) = 0 := by haveI : IsProbabilityMeasure S.P_Z := by unfold TreatedEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable have hπ_ne : S.π_val ≠ 0 := ne_of_gt hπ_pos have hmz : ∫ z, aipwMomentATT z S.μ₀_val S.e_val S.θ₀ ∂S.P_Z = 0 := aipw_mean_zero_ATT S hA hπ_pos hIPW have hm_meas : Measurable (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) := measurable_aipwMomentATT_at_θ₀ S have hm_int : Integrable (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) S.P_Z := ((memLp_two_iff_integrable_sq hm_meas.aestronglyMeasurable).2 (aipw_finite_var_ATT S h_overlap hA h_y2 h_y0_2)).integrable (by norm_num) have hindA_meas : Measurable (fun z : γ × Bool × ℝ => indA z) := by unfold indA projA refine Measurable.ite ?_ measurable_const measurable_const exact measurable_snd.fst (MeasurableSet.singleton true) have hindA_memLp : MemLp (fun z : γ × Bool × ℝ => indA z) 2 S.P_Z := by refine MemLp.of_bound hindA_meas.aestronglyMeasurable (1 : ℝ) ?_ filter_upwards with z rcases hb : z.2.1 with _ | _ <;> simp [indA, projA, hb] have hindA_int : Integrable (fun z : γ × Bool × ℝ => indA z) S.P_Z := hindA_memLp.integrable (by norm_num) have hindA_integral : ∫ z, indA z ∂S.P_Z = S.π_val := by rw [TreatedEstimationSystem.P_Z, integral_map S.measurable_factualZ.aemeasurable hindA_meas.aestronglyMeasurable] have hpt : (fun ω => indA (S.factualZ ω)) = (fun ω => S.toPOBackdoorSystem.dVar.indicator true ω) := by funext ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [TreatedEstimationSystem.factualZ, indA, projA, hD, hInd] · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [TreatedEstimationSystem.factualZ, indA, projA, hD, hInd] rw [hpt] rfl have hsplit : ∀ z, aipwMomentATT z S.μ₀_val S.e_val 0 = aipwMomentATT z S.μ₀_val S.e_val S.θ₀ + indA z * S.θ₀ := by intro z; unfold aipwMomentATT; ring have hm0_int : Integrable (fun z => aipwMomentATT z S.μ₀_val S.e_val 0) S.P_Z := by refine (hm_int.add (hindA_int.mul_const S.θ₀)).congr ?_ filter_upwards with z simp only [Pi.add_apply] rw [hsplit z] have hm0_integral : ∫ z, aipwMomentATT z S.μ₀_val S.e_val 0 ∂S.P_Z = S.θ₀ * S.π_val := by rw [integral_congr_ae (Filter.Eventually.of_forall hsplit)] integral_linearity rw [hmz, zero_add, hindA_integral] ring have hconst : ∫ _z : γ × Bool × ℝ, S.θ₀ ∂S.P_Z = S.θ₀ := by rw [integral_const]; simp unfold TreatedEstimationSystem.ψ_ATT integral_linearity rw [hm0_integral, hconst, one_div, mul_comm S.θ₀ S.π_val, inv_mul_cancel_left₀ hπ_ne, sub_self] -
ψ_ATT_finite_vartheorem — Finite variance of the centered population-π ATT influence function. Integrable ψ_ATT² against P_Z. Derived (not assumed) from aipw_finite_var_ATT (square-integrability of the moment at θ₀) and boundedness of the treatment indicator, via ψ_ATT = (1/π_T)·(m(η₀,·,θ₀) + θ₀·A) − θ₀ ∈ L²(P_Z).hypothesesγ :sharedType u_1S :ε :ℝh_overlap :S.OneSidedOverlap εhA :S.toPOBackdoorSystem.ATTAssumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_y0_2 :Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μconclusionIntegrable (fun z => (S.ψ_ATT z) ^ 2) S.P_ZProof (Lean source)
theorem ψ_ATT_finite_var (S : TreatedEstimationSystem P γ) {ε : ℝ} (h_overlap : S.OneSidedOverlap ε) (hA : S.toPOBackdoorSystem.ATTAssumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_y0_2 : Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ) : Integrable (fun z => (S.ψ_ATT z) ^ 2) S.P_Z := by haveI : IsProbabilityMeasure S.P_Z := by unfold TreatedEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable have hm_meas : Measurable (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) := measurable_aipwMomentATT_at_θ₀ S have hm_L2 : MemLp (fun z => aipwMomentATT z S.μ₀_val S.e_val S.θ₀) 2 S.P_Z := (memLp_two_iff_integrable_sq hm_meas.aestronglyMeasurable).2 (aipw_finite_var_ATT S h_overlap hA h_y2 h_y0_2) have hindA_meas : Measurable (fun z : γ × Bool × ℝ => indA z) := by unfold indA projA refine Measurable.ite ?_ measurable_const measurable_const exact measurable_snd.fst (MeasurableSet.singleton true) have hindA_L2 : MemLp (fun z : γ × Bool × ℝ => indA z) 2 S.P_Z := by refine MemLp.of_bound hindA_meas.aestronglyMeasurable (1 : ℝ) ?_ filter_upwards with z rcases hb : z.2.1 with _ | _ <;> simp [indA, projA, hb] have hm0_L2 : MemLp (fun z => aipwMomentATT z S.μ₀_val S.e_val 0) 2 S.P_Z := (hm_L2.add (hindA_L2.const_smul S.θ₀)).ae_eq (Filter.Eventually.of_forall fun z => by simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul] unfold aipwMomentATT; ring) have hψeq : (fun z => S.ψ_ATT z) = (fun z => (1 / S.π_val) • aipwMomentATT z S.μ₀_val S.e_val 0 - S.θ₀) := by funext z; unfold TreatedEstimationSystem.ψ_ATT; simp only [smul_eq_mul] have hψ_L2 : MemLp (fun z => S.ψ_ATT z) 2 S.P_Z := by rw [hψeq] exact (hm0_L2.const_smul (1 / S.π_val)).sub (memLp_const S.θ₀) exact hψ_L2.integrable_sq
Feasible 3 core · 2 supporting This file defines the ATT estimator that divides its evaluation-fold AIPW numerator by the evaluation-fold treated share. ★ dml_ATT_isAsymLinear
Feasible one-shot DML estimator for the ATT
This file defines the ATT estimator that divides its evaluation-fold AIPW
numerator by the evaluation-fold treated share. It realizes the ATT score as an
affine LinearMoment, then specializes the generic solved-estimator theorem to
obtain the Chernozhukov et al. (2018), equation (5.4), influence function. In
particular, the expansion contains the -D * θ₀ / p term induced by estimating
the treated share.
def attLinearMoment reviewed
⚑ flagged
Causalean.Estimation.ATT
For a potential-outcomes system, a measurable covariate space, a treated estimation system, an overlap radius, membership of its true nuisance in the overlap-bounded candidate set, and a positive population treated share, the affine ATT AIPW moment system has coefficient -D and constant term equal to the ATT AIPW numerator at parameter zero.
Definition (Lean source)
parameters
γ :
Type u_1
S :
ε :
ℝ
hη₀_mem :
S.η₀ ∈ H_ε S ε
hπ_pos :
0 < S.π_val
def
given by
clause 1
toGeneralMoment := attGeneralMoment S hη₀_mem hπ_pos
clause 2
m_a := fun _ z => -indA z
clause 3
m_b := fun η z => aipwMomentATTFunctional η z 0
clause 4
m_a_meas := fun _
=> by unfold indA projA refine neg (Measurable.ite ?_ measurable_const measurable_const) exact measurable_snd.fst (MeasurableSet.singleton true)
clause 5
m_b_meas := fun η => measurable_aipwMomentATTFunctional η 0
clause 6
m_decomp := by intro η z θ change aipwMomentATTFunctional η z θ
= -indA z * θ
clause 7
linScale_eq := by rw [integral_neg, integral_indA_eq_π_val S] simp [attGeneralMoment]
def dmlEstimator_ATT reviewed
⚑ flagged
Causalean.Estimation.ATT
For a potential-outcomes system, a measurable covariate space, a treated estimation system, an i.i.d. observed-data sample, a one-shot split, a complementary-fold ATT nuisance fit, and a sample-size index, the feasible one-shot ATT DML estimator is the evaluation-fold AIPW numerator mean divided by the evaluation-fold treated share.
Definition (Lean source)
parameters
def
dmlEstimator_ATT S sample split η_hat n :
P.Ω → ℝ
given by
fun ω
=> ((((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, indA (sample.Z i ω))⁻¹) * (((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, aipwMomentATTFunctional (η_hat n ω) (sample.Z i ω) 0)
theorem dml_ATT_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.ATT
Feasible ATT DML asymptotic linearity. For a potential-outcomes system, a measurable covariate space, a treated estimation system, an overlap radius, truth-nuisance overlap membership, a nonnegative true propensity, one-sided overlap, the back-door ATT assumptions, a positive treated share, factual- and untreated-outcome second moments, integrable truth IPW correction, an i.i.d. sample, a one-shot split, a limiting evaluation-fold share, that limit being positive, convergence of the evaluation-fold share, and a complementary-fold nuisance sequence, if every fitted nuisance lies in the overlap set, every fitted propensity is nonnegative, both fitted nuisance errors are square-integrable, each fitted IPW correction is integrable, the fitted score has the required joint and training-fold measurability, the fitted score is integrable and square-integrable, both nuisance errors are individually negligible, and their product is negligible at the root-sample rate, then the sample-treated-share ATT estimator is asymptotically linear with influence function m(η₀,z,θ₀)/p.
Formal statement
hypotheses
γ :
Type u_1
S :
ε :
ℝ
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.μ
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < 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 :
h_m_meas :
∀ n,
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.μ
conclusion
IsAsymLinear (dmlEstimator_ATT S sample split η_hat) S.θ₀ (fun z => (1 / S.π_val) * aipwMomentATTFunctional S.η₀ z S.θ₀) sample split.foldB
Proof (Lean source)
theorem dml_ATT_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)
(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_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 (dmlEstimator_ATT S sample split η_hat) S.θ₀
(fun z => (1 / S.π_val) *
aipwMomentATTFunctional S.η₀ z S.θ₀)
sample split.foldB := by
haveI : IsProbabilityMeasure S.P_Z := by
unfold TreatedEstimationSystem.P_Z
exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable
let M := attLinearMoment S hη₀_mem hπ_pos
have hOracle : IsAsymLinear
(oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀
(fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB := by
change IsAsymLinear
(oneStepOracleDML (attGeneralMoment S hη₀_mem hπ_pos)
sample split η_hat) S.θ₀
(fun z => -(attGeneralMoment S hη₀_mem hπ_pos).linScaleInv *
aipwMomentATTFunctional S.η₀ z S.θ₀) sample split.foldB
exact att_oneStepOracleDML_isAsymLinear S hη₀_mem h_e_lb h_overlap hA hπ_pos
h_y2 h_y0_2 hIPW sample split hc_pos h_split_rate η_hat
h_in_Hε h_e_lb_hat h_mu_diff_memLp h_e_diff_memLp h_IPW_at
h_m_meas h_m_foldA_uncurry h_m_int h_m_sq_int
h_indiv_rate_ρ₁ h_indiv_rate_ρ₂ h_product_rate
have hIndMeas : Measurable (fun z : γ × Bool × ℝ => -indA z) := by
unfold indA projA
refine neg (Measurable.ite ?_ measurable_const measurable_const)
exact measurable_snd.fst (MeasurableSet.singleton true)
have hIndLp : MemLp (fun z : γ × Bool × ℝ => -indA z) 2 S.P_Z := by
refine MemLp.of_bound hIndMeas.aestronglyMeasurable 1 ?_
filter_upwards with z
rcases hb : z.2.1 with _ | _ <;> simp [indA, projA, hb]
have hJraw := OneShotSplit.foldB_sampleMean_tendsto_inProb
sample split hIndMeas hIndLp
have hJ : Modes.TendstoInProbability (fun _ : ℕ => P.μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale) := by
convert hJraw using 1
· funext n ω
simp [M, attLinearMoment]
· funext n
rw [M.linScale_eq]
simp [M, attLinearMoment]
have hψ_meas : Measurable
(fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) := by
simpa [M, attLinearMoment, attGeneralMoment, GeneralMoment.linScaleInv,
TreatedEstimationSystem.η₀, one_div] using
(measurable_aipwMomentATTFunctional S.η₀ S.θ₀).const_mul
(1 / S.π_val)
have hOracle_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(oneStepOracleDML M.toGeneralMoment sample split η_hat)
M.θ₀ split.foldB n) P.μ := by
intro n
have hm : Measurable (fun p : P.Ω × (γ × Bool × ℝ) =>
M.m (η_hat n p.1) p.2 M.θ₀) := by
change Measurable (fun p : P.Ω × (γ × Bool × ℝ) =>
aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀)
exact h_m_meas n
have hsum : Measurable (fun ω =>
∑ i ∈ split.foldB n,
M.m (η_hat n ω) (sample.Z i ω) M.θ₀) :=
Finset.measurable_sum _ (fun i _ =>
hm.comp (prodMk measurable_id (sample.meas i)))
unfold IsAsymLinear.rescaledEstimator oneStepOracleDML
apply aemeasurable
exact measurable_const.mul
((measurable_const.sub
(measurable_const.mul (measurable_const.mul hsum))).sub
measurable_const)
have hSum_meas : ∀ n, AEMeasurable
(IsAsymLinear.normalizedSum sample
(fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) P.μ := by
intro n
unfold IsAsymLinear.normalizedSum
exact ((Finset.measurable_sum _ (fun i _ =>
hψ_meas.comp (sample.meas i))).const_mul _).aemeasurable
have hFeasible := feasibleLinearDML_isAsymLinear_of_jacobianConsistency
M sample split η_hat hOracle hJ hψ_meas hOracle_meas hSum_meas
rw [dmlEstimator_ATT_eq_feasibleLinearDML S hη₀_mem hπ_pos
sample split η_hat]
simpa [M, attLinearMoment, attGeneralMoment, GeneralMoment.linScaleInv,
TreatedEstimationSystem.η₀, one_div] using hFeasible
2 supporting declarations (lemmas, instances)
-
integral_indA_eq_π_vallemma — For a potential-outcomes system, a measurable covariate space, and a treated estimation system, the population integral of the treatment indicator under its observed-data law equals the marginal treated share.hypothesesconclusion∫ z, indA z ∂S.P_Z = S.π_valProof (Lean source)
lemma integral_indA_eq_π_val (S : TreatedEstimationSystem P γ) : ∫ z, indA z ∂S.P_Z = S.π_val := by have hindA_meas : Measurable (fun z : γ × Bool × ℝ => indA z) := by unfold indA projA refine Measurable.ite ?_ measurable_const measurable_const exact measurable_snd.fst (MeasurableSet.singleton true) rw [TreatedEstimationSystem.P_Z, integral_map S.measurable_factualZ.aemeasurable hindA_meas.aestronglyMeasurable] have hpoint : (fun ω => indA (S.factualZ ω)) = (fun ω => S.toPOBackdoorSystem.dVar.indicator true ω) := by funext ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [TreatedEstimationSystem.factualZ, indA, projA, hD, hInd] · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [TreatedEstimationSystem.factualZ, indA, projA, hD, hInd] rw [hpoint] rfl -
dmlEstimator_ATT_eq_feasibleLinearDMLlemma — For a potential-outcomes system, a measurable covariate space, a treated estimation system, an overlap radius, truth-nuisance overlap membership, a positive population treated share, an i.i.d. sample, a one-shot split, and an ATT nuisance fit, the feasible ATT estimator equals the generic solved affine-score DML estimator.hypothesesγ :sharedType u_1S :ε :ℝhη₀_mem :S.η₀ ∈ H_ε S εhπ_pos :0 < S.π_valsplit :OneShotSplit sampleη_hat :ℕ → P.Ω → TreatedNuisanceVec γconclusiondmlEstimator_ATT S sample split η_hat= feasibleLinearDML (attLinearMoment S hη₀_mem hπ_pos) sample split η_hatProof (Lean source)
lemma dmlEstimator_ATT_eq_feasibleLinearDML (S : TreatedEstimationSystem P γ) {ε : ℝ} (hη₀_mem : S.η₀ ∈ H_ε S ε) (hπ_pos : 0 < S.π_val) (sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) (η_hat : ℕ → P.Ω → TreatedNuisanceVec γ) : dmlEstimator_ATT S sample split η_hat = feasibleLinearDML (attLinearMoment S hη₀_mem hπ_pos) sample split η_hat := by funext n ω simp only [dmlEstimator_ATT, feasibleLinearDML, attLinearMoment] rw [Finset.sum_neg_distrib] ring
AsymptoticNormality 1 core · 0 supporting This file derives the true-standard-deviation Gaussian limit of the feasible sample-treated-share ATT estimator from the primitive overlap, moment, cross-fitting, and nuisance-rate assumptions of its asymptotic-linearity ★ dml_ATT_tendstoStandardNormal
Asymptotic normality of feasible one-shot ATT DML
This file derives the true-standard-deviation Gaussian limit of the feasible sample-treated-share ATT estimator from the primitive overlap, moment, cross-fitting, and nuisance-rate assumptions of its asymptotic-linearity theorem.
theorem dml_ATT_tendstoStandardNormal reviewed
⚑ flagged
Causalean.Estimation.ATT
Standard-normal limit of feasible ATT DML. For a potential-outcomes system, a measurable covariate space, a treated estimation system, an overlap radius, truth-nuisance overlap membership, a nonnegative true propensity, one-sided overlap, the back-door ATT assumptions, a positive treated share, factual- and untreated-outcome second moments, integrable truth IPW correction, an i.i.d. sample, a one-shot split, a limiting evaluation-fold share, that limit being positive, convergence of the evaluation-fold share, and a complementary-fold nuisance sequence, if every fitted nuisance lies in the overlap set, every fitted propensity is nonnegative, both fitted nuisance errors are square-integrable, each fitted IPW correction is integrable, the fitted score has the required joint and training-fold measurability, the fitted score is integrable and square-integrable, both nuisance errors are individually negligible, their product is negligible at the root-sample rate, a true influence-function standard deviation is positive and has its defining second-moment identity, and the rescaled estimator and its standardized version are measurable, then the true-standard-deviation-normalized feasible ATT estimator converges to the standard normal law.
Formal statement
hypotheses
γ :
Type u_1
S :
ε :
ℝ
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.μ
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < 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 :
h_m_meas :
∀ n,
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.μ
σ :
ℝ
hσ_pos :
0 < σ
hσ_sq :
σ ^ 2 = ∫ z, ((1 / S.π_val) * aipwMomentATTFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z
hNum_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator_ATT S sample split η_hat) S.θ₀ split.foldB n) P.μ
hStud_meas :
∀ n,
AEMeasurable (fun ω => IsAsymLinear.rescaledEstimator (dmlEstimator_ATT S sample split η_hat) S.θ₀ split.foldB n ω / σ) P.μ
conclusion
Modes.TendstoInLaw (fun _ : ℕ => P.μ) (fun n ω => IsAsymLinear.rescaledEstimator (dmlEstimator_ATT S sample split η_hat) S.θ₀ split.foldB n ω / σ) atTop (gaussianMeasure 0 1)
Proof (Lean source)
theorem dml_ATT_tendstoStandardNormal
(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)
(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_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.μ)
(σ : ℝ) (hσ_pos : 0 < σ)
(hσ_sq : σ ^ 2 = ∫ z,
((1 / S.π_val) *
aipwMomentATTFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z)
(hNum_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(dmlEstimator_ATT S sample split η_hat) S.θ₀ split.foldB n) P.μ)
(hStud_meas : ∀ n, AEMeasurable (fun ω =>
IsAsymLinear.rescaledEstimator
(dmlEstimator_ATT S sample split η_hat) S.θ₀ split.foldB n ω / σ) P.μ) :
Modes.TendstoInLaw (fun _ : ℕ => P.μ) (fun n ω =>
IsAsymLinear.rescaledEstimator
(dmlEstimator_ATT S sample split η_hat) S.θ₀ split.foldB n ω / σ) atTop
(gaussianMeasure 0 1) := by
haveI : IsProbabilityMeasure S.P_Z := by
unfold TreatedEstimationSystem.P_Z
exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable
have hAL := dml_ATT_isAsymLinear S hη₀_mem h_e_lb h_overlap hA hπ_pos
h_y2 h_y0_2 hIPW sample split hc_pos h_split_rate η_hat
h_in_Hε h_e_lb_hat h_mu_diff_memLp h_e_diff_memLp h_IPW_at
h_m_meas h_m_foldA_uncurry h_m_int h_m_sq_int
h_indiv_rate_ρ₁ h_indiv_rate_ρ₂ h_product_rate
have hψ_meas : Measurable (fun z =>
(1 / S.π_val) * aipwMomentATTFunctional S.η₀ z S.θ₀) :=
(measurable_aipwMomentATTFunctional S.η₀ S.θ₀).const_mul _
have hSum_meas : ∀ n, AEMeasurable
(IsAsymLinear.normalizedSum sample
(fun z => (1 / S.π_val) *
aipwMomentATTFunctional S.η₀ z S.θ₀) split.foldB n) P.μ := by
intro n
unfold IsAsymLinear.normalizedSum
exact ((Finset.measurable_sum _ (fun i _ =>
hψ_meas.comp (sample.meas i))).const_mul _).aemeasurable
have hNormal := hAL.tendsto_normal_foldB
split hψ_meas hNum_meas hSum_meas
rw [← hσ_sq] at hNormal
have hScaled := Modes.TendstoInLaw.const_mul_tendsto_gaussian (Xn := IsAsymLinear.rescaledEstimator
(dmlEstimator_ATT S sample split η_hat) S.θ₀ split.foldB)
(a := fun _ : ℕ => 1 / σ)
(a₀ := 1 / σ)
(v := σ ^ 2)
hNormal tendsto_const_nhds
have hvar : (1 / σ) ^ 2 * σ ^ 2 = 1 := by
field_simp [ne_of_gt hσ_pos]
rw [hvar] at hScaled
simpa [div_eq_mul_inv, mul_comm] using hScaled