Estimation.ATE.DML

This roll-up exports dmlEstimator, the one-shot sample-split augmented inverse-probability weighted estimator for the back-door average treatment effect.

Basic 1 core · 0 supporting Defines dmlEstimator, the fold-B empirical average of the AIPW pseudo-outcome for a one-shot sample split.

One-shot ATE DML estimator

Defines dmlEstimator, the fold-B empirical average of the AIPW pseudo-outcome for a one-shot sample split. Asymptotic linearity and normality are proved in the two downstream files of this directory.

def dmlEstimator reviewed
Causalean.Estimation.ATE

For a potential-outcome system with a measurable covariate space, a back-door estimation system, an independent and identically distributed sample of observed covariate, treatment, and outcome triples from its observable data law, a one-shot split of that sample, an outcome-regression learner indexed by sample size and population realization, a propensity-score learner indexed in the same way, and a nonnegative integer sample-size index, the one-shot DML/AIPW estimator of the back-door average treatment effect assigns to each population realization the average AIPW moment over that index's estimation fold.

Definition (Lean source)
parameters
P :
POSystem
shared
γ :
Type u_1
shared
S :
BackdoorEstimationSystem P γ
sample :
IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
μ_hat :
ℕ → P.Ω → (Bool → γ → ℝ)
e_hat :
ℕ → P.Ω → (γ → ℝ)
n :
ℕ
def
dmlEstimator S sample split μ_hat e_hat n :
P.Ω → ℝ
given by
fun ω
=> ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, aipwMoment (sample.Z i ω) (μ_hat n ω) (e_hat n ω) 0
Causalean.Estimation.ATE.dmlEstimator · Causalean/Estimation/ATE/DML/Basic.lean:36 · uses BackdoorEstimationSystem , P_Z , POSystem , IIDSample , OneShotSplit
Asymptotic­Linearity 1 core · 1 supporting Proves the good-event, almost-everywhere good-event, and direct forms of asymptotic linearity for dmlEstimator. ★ dml_ATE_isAsymLinear_of_goodSet

Asymptotic linearity for one-shot ATE DML

Proves the good-event, almost-everywhere good-event, and direct forms of asymptotic linearity for dmlEstimator. These wrappers discharge the abstract AIPW DML interface from overlap, moment, sample-split, measurability, and nuisance-rate assumptions.

theorem dml_ATE_isAsymLinear_of_goodSet reviewed
Causalean.Estimation.ATE

Asymptotic linearity of the one-shot DML estimator of the average treatment effect. For a back-door estimation system satisfying the back-door identification assumptions, with an overlap threshold ε such that 0 < ε ≤ 1/2 and the true propensity score lies between ε and 1 − ε almost surely, a square-integrable observed outcome and square-integrable potential outcomes, let an i.i.d. sample be split once into a training fold and an evaluation fold whose evaluation-fold share converges to a limit c that is positive, and let μ̂_n and ê_n be the outcome-regression and propensity learners. Suppose there are events G_n whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Assume (ω, x) ↦ μ̂_n(ω)(a, x) is jointly measurable for each arm a and so is (ω, x) ↦ ê_n(ω)(x); on G_n each μ̂_n(a, ·) is square-integrable under the covariate law, ê_n is square-integrable under the covariate law and ε ≤ ê_n ≤ 1 − ε almost everywhere under the covariate law; μ̂_n and ê_n are measurable with respect to the product of the σ-algebra generated by the training-fold observations and the covariate σ-algebra; for each arm the L² error of μ̂_n under the covariate law is o_p(1), the L² error of ê_n is o_p(1), and for each arm the product of these two L² errors is o_p(n^(−1/2)). Then the evaluation-fold augmented inverse-probability-weighted estimator built from μ̂_n and ê_n is asymptotically linear at the true average treatment effect along the evaluation fold, with the augmented inverse-probability-weighted influence function evaluated at the true regression and propensity.

Formal statement
hypotheses
P :
POSystem
shared
γ :
Type u_1
shared
S :
BackdoorEstimationSystem P γ
ε :
ℝ
hA :
S.toPOBackdoorSystem.Assumptions
h_overlap :
S.StrictOverlap ε
h_y2 :
Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
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 → γ → ℝ)
e_hat :
ℕ → P.Ω → (γ → ℝ)
goodSet :
ℕ → Set P.Ω
Δ :
ℕ → ℝ≥0∞
hΔ :
Tendsto Δ atTop (𝓝 0)
hfail :
∀ n, P.μ (goodSet n)ᶜ ≤ Δ n
h_mu_meas :
∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
h_e_meas :
∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
h_mu_memLp :
∀ n ω
if
ω ∈ goodSet n
then
∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X
h_e_memLp :
∀ n ω
if
ω ∈ goodSet n
then
MemLp (fun x => e_hat n ω x) 2 S.P_X
h_e_overlap :
∀ n ω
if
ω ∈ goodSet n
then
∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε
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_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_mu_rate :
∀ a : Bool,
IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 :
∀ a : Bool,
IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 (dmlEstimator S sample split μ_hat e_hat) S.θ₀ (S.ψ_AIPW) sample split.foldB
Proof (Lean source)
theorem dml_ATE_isAsymLinear_of_goodSet (S : BackdoorEstimationSystem P γ) {ε : ℝ} (hA : S.toPOBackdoorSystem.Assumptions) (h_overlap : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (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 → γ → ℝ)) (e_hat : ℕ → P.Ω → (γ → ℝ)) (goodSet : ℕ → Set P.Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, P.μ (goodSet n)ᶜ ≤ Δ n) (h_mu_meas : ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_e_meas : ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_mu_memLp : ∀ n ω, ω ∈ goodSet n → ∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X) (h_e_memLp : ∀ n ω, ω ∈ goodSet n → MemLp (fun x => e_hat n ω x) 2 S.P_X) (h_e_overlap : ∀ n ω, ω ∈ goodSet n → ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε) (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_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_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 S sample split μ_hat e_hat) S.θ₀ (S.ψ_AIPW) sample split.foldB := by classical -- 1. Build the abstract `η_hat : ℕ → P.Ω → NuisanceVec γ` from `(μ_hat, e_hat)`. let η_hat : ℕ → P.Ω → NuisanceVec γ := fun n ω => { μ_fn := μ_hat n ω e_fn := e_hat n ω μ_meas := fun a => (h_mu_meas n a).comp (prodMk measurable_const measurable_id) e_meas := (h_e_meas n).comp (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 BackdoorEstimationSystem.P_X exact Measure.isProbabilityMeasure_map S.toPOBackdoorSystem.measurable_factualX.aemeasurable -- `S.P_Z` is a probability measure (used by `MemLp.integrable` on the score). haveI : IsProbabilityMeasure S.P_Z := by unfold BackdoorEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable -- 2. `S.μ_val a` is L²(P_X) (via condExp of square-integrable counterfactual outcomes). 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 (by norm_num) 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 -- 3. `S.e_val` is L²(P_X) (via boundedness in `[0, 1]`). have he_val_memLp : MemLp S.e_val 2 S.P_X := by refine MemLp.of_bound S.e_meas.aestronglyMeasurable 1 ?_ refine Eventually.of_forall fun x => ?_ rw [Real.norm_eq_abs] exact abs_le.mpr ⟨by linarith [S.e_pos x], by linarith [S.e_lt_one x]⟩ have he_val_memLp_top : MemLp S.e_val ⊤ S.P_X := by refine MemLp.of_bound S.e_meas.aestronglyMeasurable 1 ?_ refine Eventually.of_forall fun x => ?_ rw [Real.norm_eq_abs] exact abs_le.mpr ⟨by linarith [S.e_pos x], by linarith [S.e_lt_one x]⟩ have hη₀_mem : S.η₀ ∈ H_ε_aeL2 S ε := by refine ⟨?_, ?_, ?_⟩ · have hset : MeasurableSet {x : γ | ε ≤ S.e_val x ∧ S.e_val x ≤ 1 - ε} := by exact measurableSet_Icc.preimage S.e_meas have hΩ : ∀ᵐ ω ∂P.μ, ε ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) ∧ S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by filter_upwards [h_overlap.2.2, S.e_compat] with ω hover hcomp simpa [hcomp] using hover unfold BackdoorEstimationSystem.P_X exact (MeasureTheory.ae_map_iff S.toPOBackdoorSystem.measurable_factualX.aemeasurable hset).mpr hΩ · exact hμ_val_memLp · exact he_val_memLp_top have h_in_Hε : ∀ n ω, ω ∈ goodSet n → η_hat n ω ∈ H_ε_aeL2 S ε := by intro n ω hω have hμ := h_mu_memLp n ω hω have hover := h_e_overlap n ω hω refine ⟨hover, hμ, ?_⟩ refine MemLp.of_bound (η_hat n ω).e_meas.aestronglyMeasurable 1 ?_ filter_upwards [hover] with x hx rw [Real.norm_eq_abs] exact abs_le.mpr ⟨by linarith [h_overlap.1, hx.1], by linarith [h_overlap.1, hx.2]⟩ -- 4. Per-η̂_n L² of the differences (needed by the abstract). have h_mu_diff_memLp : ∀ n ω, ω ∈ goodSet n → ∀ a, MemLp (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X := by intro n ω hω have hμ := h_mu_memLp n ω hω exact fun a => (hμ a).sub (hμ_val_memLp a) have h_e_diff_memLp : ∀ n ω, ω ∈ goodSet n → MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X := by intro n ω hω have he := h_e_memLp n ω hω exact he.sub he_val_memLp -- 5. Translate the production rate hypotheses to the abstract `ρ₁ / ρ₂`. -- `ρ₁ η η₀ = ‖Δμ_T‖ + ‖Δμ_F‖`, `ρ₂ η η₀ = ‖Δe‖`. have h_indiv_rate_ρ₁ : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ := by exact IsLittleOp.add_one (h_mu_rate true) (h_mu_rate false) have h_indiv_rate_ρ₂ : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ := by exact h_e_rate have h_product_rate_abs : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ := by have hrn_nonneg : ∀ᶠ n : ℕ in atTop, 0 ≤ (n : ℝ) ^ (-(1 / 2 : ℝ)) := by filter_upwards with n positivity have hcomb := IsLittleOp.add_eventually_nonneg_rate hrn_nonneg (h_product_rate true) (h_product_rate false) have hfun : (fun n (ω : P.Ω) => (eLpNorm (fun x => μ_hat n ω true x - S.μ_val true x) 2 S.P_X).toReal * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal + (eLpNorm (fun x => μ_hat n ω false x - S.μ_val false x) 2 S.P_X).toReal * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) = fun n ω => ((eLpNorm (fun x => μ_hat n ω true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => μ_hat n ω false x - S.μ_val false x) 2 S.P_X).toReal) * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal := by funext n ω ring rw [hfun] at hcomb exact hcomb -- 6. Translate score measurability / integrability to the abstract form. have h_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentFunctional (η_hat n p.1) p.2 S.θ₀) := by intro n unfold aipwMomentFunctional aipwMoment indA projX projA projY η_hat -- … truncated; follow the source link for the rest …
Causalean.Estimation.ATE.dml_ATE_isAsymLinear_of_goodSet · Causalean/Estimation/ATE/DML/AsymptoticLinearity.lean:35 · uses BackdoorEstimationSystem , P_X , P_Z , StrictOverlap , θ₀ , ψ_AIPW , dmlEstimator , Assumptions , YofD , factualY , POSystem , IIDSample , IsAsymLinear , IsLittleOp , OneShotSplit , foldA , foldB
1 supporting declaration (lemmas, instances)
  • dml_ATE_isAsymLinear_of_goodSet_ae theorem — For an ATE estimation system and threshold, identification, overlap, and moment assumptions, a sample and one-shot split with an evaluation-fold share converging to a positive limit, and nuisance learners, assume ambient measurability, almost-sure square-integrability and overlap at every horizon, training-fold measurability, and the individual and product rates. Then the one-shot DML/AIPW estimator is asymptotically linear.
    hypotheses
    P :
    POSystem
    shared
    γ :
    Type u_1
    shared
    S :
    BackdoorEstimationSystem P γ
    ε :
    ℝ
    hA :
    S.toPOBackdoorSystem.Assumptions
    h_overlap :
    S.StrictOverlap ε
    h_y2 :
    Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
    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 → γ → ℝ)
    e_hat :
    ℕ → P.Ω → (γ → ℝ)
    h_mu_meas :
    ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
    h_e_meas :
    ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
    h_mu_memLp :
    ∀ n, ∀ᵐ ω ∂P.μ, ∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X
    h_e_memLp :
    ∀ n, ∀ᵐ ω ∂P.μ, MemLp (fun x => e_hat n ω x) 2 S.P_X
    h_e_overlap :
    ∀ n, ∀ᵐ ω ∂P.μ, ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε
    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_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_mu_rate :
    ∀ a : Bool,
    IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 :
    ∀ a : Bool,
    IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 (dmlEstimator S sample split μ_hat e_hat) S.θ₀ (S.ψ_AIPW) sample split.foldB
    Proof (Lean source)
    theorem dml_ATE_isAsymLinear_of_goodSet_ae (S : BackdoorEstimationSystem P γ) {ε : ℝ} (hA : S.toPOBackdoorSystem.Assumptions) (h_overlap : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (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 → γ → ℝ)) (e_hat : ℕ → P.Ω → (γ → ℝ)) (h_mu_meas : ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_e_meas : ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_mu_memLp : ∀ n, ∀ᵐ ω ∂P.μ, ∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X) (h_e_memLp : ∀ n, ∀ᵐ ω ∂P.μ, MemLp (fun x => e_hat n ω x) 2 S.P_X) (h_e_overlap : ∀ n, ∀ᵐ ω ∂P.μ, ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε) (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_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_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 S sample split μ_hat e_hat) S.θ₀ (S.ψ_AIPW) sample split.foldB := by classical let goodSet : ℕ → Set P.Ω := fun n => {ω | (∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X) ∧ MemLp (fun x => e_hat n ω x) 2 S.P_X ∧ (∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε)} have hgood : ∀ n, ∀ᵐ ω ∂P.μ, ω ∈ goodSet n := by intro n filter_upwards [h_mu_memLp n, h_e_memLp n, h_e_overlap n] with ω hμ he hover exact ⟨hμ, he, hover⟩ apply dml_ATE_isAsymLinear_of_goodSet S hA h_overlap h_y2 h_yd2 sample split hc_pos h_split_rate μ_hat e_hat goodSet (fun _ => 0) tendsto_const_nhds · intro n have hz : P.μ (goodSet n)ᶜ = 0 := by apply ae_iff.mp filter_upwards [hgood n] with ω hω exact hω simpa [hz] · exact h_mu_meas · exact h_e_meas · intro n ω hω exact hω.1 · intro n ω hω exact hω.2.1 · intro n ω hω exact hω.2.2 · exact h_mu_uncurry_foldA · exact h_e_uncurry_foldA · exact h_mu_rate · exact h_e_rate · exact h_product_rate
    Causalean.Estimation.ATE.dml_ATE_isAsymLinear_of_goodSet_ae · Causalean/Estimation/ATE/DML/AsymptoticLinearity.lean:853
Asymptotic­Normality 1 core · 1 supporting Proves dml_ATE_tendstoNormal_on_highProbEvent, the normal limit when the learner square-integrability and overlap conditions hold on events of probability tending to one, by combining good-set asymptotic linearity with t ★ dml_ATE_tendstoNormal

Asymptotic normality for one-shot ATE DML

Proves dml_ATE_tendstoNormal_on_highProbEvent, the normal limit when the learner square-integrability and overlap conditions hold on events of probability tending to one, by combining good-set asymptotic linearity with the fold-level central limit theorem. dml_ATE_tendstoNormal is its corollary for learners satisfying those conditions at every realization. This file owns the normal-limit wrappers, not the estimator or linearity proof.

theorem dml_ATE_tendstoNormal reviewed
Causalean.Estimation.ATE

Asymptotic normality of the one-shot DML estimator of the average treatment effect. Under the back-door identification assumptions, with strict overlap for the true propensity score and the same overlap bounds holding almost everywhere under the covariate law for every realization of the propensity learner, finite second moments of the observed and potential outcomes, and a one-shot sample split whose evaluation-fold share converges to a positive limit c: suppose the outcome-regression and propensity learners μ̂_n, ê_n are jointly measurable in the realization and the covariate, square-integrable under the covariate law at every realization, measurable with respect to the product of the σ-algebra generated by the training-fold observations and the covariate σ-algebra, and have L² errors under the covariate law that are each o_p(1), with the product of the outcome-regression and propensity L² errors being o_p(n^(−1/2)) for each arm. These nuisance conditions are imposed at every realization of the learners, not only on a high-probability event. Given in addition measurability of the augmented inverse-probability-weighted influence function, almost-everywhere measurability of the rescaled estimator at every sample size, and almost-everywhere measurability of the normalized influence-function sum at every sample size, then √|B(n)|·(θ̂_n − θ₀), where B(n) is the evaluation fold, converges in distribution to the centered normal law whose variance is the second moment of the augmented inverse-probability-weighted influence function under the observed-data law.

Formal statement
hypotheses
P :
POSystem
shared
γ :
Type u_1
shared
S :
BackdoorEstimationSystem P γ
ε :
ℝ
hA :
S.toPOBackdoorSystem.Assumptions
h_overlap :
S.StrictOverlap ε
h_y2 :
Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
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 → γ → ℝ)
e_hat :
ℕ → P.Ω → (γ → ℝ)
h_mu_meas :
∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
h_e_meas :
∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
h_mu_memLp :
∀ n ω a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X
h_e_memLp :
∀ n ω, MemLp (fun x => e_hat n ω x) 2 S.P_X
h_e_overlap :
∀ n ω, ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε
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_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_mu_rate :
∀ a : Bool,
IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 :
∀ a : Bool,
IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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.μ
hψ_meas :
Measurable (S.ψ_AIPW)
hθn_meas :
∀ n : ℕ,
AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ
hSum_meas :
∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ
conclusion
Modes.TendstoInLaw (fun _ : ℕ => P.μ) (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ x, (S.ψ_AIPW x) ^ 2 ∂S.P_Z))
Proof (Lean source)
theorem dml_ATE_tendstoNormal (S : BackdoorEstimationSystem P γ) {ε : ℝ} (hA : S.toPOBackdoorSystem.Assumptions) (h_overlap : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (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 → γ → ℝ)) (e_hat : ℕ → P.Ω → (γ → ℝ)) (h_mu_meas : ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_e_meas : ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_mu_memLp : ∀ n ω a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X) (h_e_memLp : ∀ n ω, MemLp (fun x => e_hat n ω x) 2 S.P_X) (h_e_overlap : ∀ n ω, ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε) (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_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_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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.μ) (hψ_meas : Measurable (S.ψ_AIPW)) (hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ) (hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ) : Modes.TendstoInLaw (fun _ : ℕ => P.μ) (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ x, (S.ψ_AIPW x) ^ 2 ∂S.P_Z)) := by exact dml_ATE_tendstoNormal_on_highProbEvent S hA h_overlap h_y2 h_yd2 sample split hc_pos h_split_rate μ_hat e_hat (fun _ => univ) (fun _ => 0) tendsto_const_nhds (by simp) h_mu_meas h_e_meas (fun n ω _ a => h_mu_memLp n ω a) (fun n ω _ => h_e_memLp n ω) (fun n ω _ => h_e_overlap n ω) h_mu_uncurry_foldA h_e_uncurry_foldA h_mu_rate h_e_rate h_product_rate hψ_meas hθn_meas hSum_meas
Causalean.Estimation.ATE.dml_ATE_tendstoNormal · Causalean/Estimation/ATE/DML/AsymptoticNormality.lean:141 · uses BackdoorEstimationSystem , P_X , P_Z , StrictOverlap , θ₀ , ψ_AIPW , dmlEstimator , Assumptions , YofD , factualY , POSystem , IIDSample , normalizedSum , rescaledEstimator , IsLittleOp , TendstoInLaw , OneShotSplit , foldA , foldB , gaussianMeasure , instIsProbabilityMeasureGaussianMeasure
1 supporting declaration (lemmas, instances)
  • dml_ATE_tendstoNormal_on_highProbEvent theorem — Asymptotic normality of the one-shot DML estimator of the average treatment effect, with learner conditions on events of probability tending to one. For a back-door estimation system satisfying the back-door identification assumptions, with an overlap threshold ε such that 0 < ε ≤ 1/2 and the true propensity score lies between ε and 1 − ε almost surely, a square-integrable observed outcome and square-integrable potential outcomes, let an i.i.d. sample be split once into a training fold and an evaluation fold whose evaluation-fold share converges to a limit c that is positive, and let μ̂_n and ê_n be the outcome-regression and propensity learners. Suppose there are events G_n whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Assume (ω, x) ↦ μ̂_n(ω)(a, x) is jointly measurable for each arm a and so is (ω, x) ↦ ê_n(ω)(x); on G_n each μ̂_n(a, ·) is square-integrable under the covariate law, ê_n is square-integrable under the covariate law and ε ≤ ê_n ≤ 1 − ε almost everywhere under the covariate law; μ̂_n and ê_n are measurable with respect to the product of the σ-algebra generated by the training-fold observations and the covariate σ-algebra; for each arm the L² error of μ̂_n under the covariate law is o_p(1), the L² error of ê_n is o_p(1), and for each arm the product of these two L² errors is o_p(n^(−1/2)). Given in addition measurability of the augmented inverse-probability-weighted influence function, almost-everywhere measurability of the rescaled estimator at every sample size, and almost-everywhere measurability of the normalized influence-function sum at every sample size, then √|B(n)|·(θ̂_n − θ₀), where B(n) is the evaluation fold, converges in distribution to the centered normal law whose variance is the second moment of the augmented inverse-probability-weighted influence function under the observed-data law.
    hypotheses
    P :
    POSystem
    shared
    γ :
    Type u_1
    shared
    S :
    BackdoorEstimationSystem P γ
    ε :
    ℝ
    hA :
    S.toPOBackdoorSystem.Assumptions
    h_overlap :
    S.StrictOverlap ε
    h_y2 :
    Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
    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 → γ → ℝ)
    e_hat :
    ℕ → P.Ω → (γ → ℝ)
    goodSet :
    ℕ → Set P.Ω
    Δ :
    ℕ → ℝ≥0∞
    hΔ :
    Tendsto Δ atTop (𝓝 0)
    hfail :
    ∀ n, P.μ (goodSet n)ᶜ ≤ Δ n
    h_mu_meas :
    ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
    h_e_meas :
    ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
    h_mu_memLp :
    ∀ n ω
    if
    ω ∈ goodSet n
    then
    ∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X
    h_e_memLp :
    ∀ n ω
    if
    ω ∈ goodSet n
    then
    MemLp (fun x => e_hat n ω x) 2 S.P_X
    h_e_overlap :
    ∀ n ω
    if
    ω ∈ goodSet n
    then
    ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε
    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_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_mu_rate :
    ∀ a : Bool,
    IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 :
    ∀ a : Bool,
    IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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.μ
    hψ_meas :
    Measurable (S.ψ_AIPW)
    hθn_meas :
    ∀ n : ℕ,
    AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ
    hSum_meas :
    ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ
    conclusion
    Modes.TendstoInLaw (fun _ : ℕ => P.μ) (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ x, (S.ψ_AIPW x) ^ 2 ∂S.P_Z))
    Proof (Lean source)
    theorem dml_ATE_tendstoNormal_on_highProbEvent (S : BackdoorEstimationSystem P γ) {ε : ℝ} (hA : S.toPOBackdoorSystem.Assumptions) (h_overlap : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (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 → γ → ℝ)) (e_hat : ℕ → P.Ω → (γ → ℝ)) (goodSet : ℕ → Set P.Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, P.μ (goodSet n)ᶜ ≤ Δ n) (h_mu_meas : ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_e_meas : ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_mu_memLp : ∀ n ω, ω ∈ goodSet n → ∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X) (h_e_memLp : ∀ n ω, ω ∈ goodSet n → MemLp (fun x => e_hat n ω x) 2 S.P_X) (h_e_overlap : ∀ n ω, ω ∈ goodSet n → ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε) (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_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_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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 : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a 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.μ) (hψ_meas : Measurable (S.ψ_AIPW)) (hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ) (hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ) : Modes.TendstoInLaw (fun _ : ℕ => P.μ) (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ x, (S.ψ_AIPW x) ^ 2 ∂S.P_Z)) := by have hAL := dml_ATE_isAsymLinear_of_goodSet S hA h_overlap h_y2 h_yd2 sample split hc_pos h_split_rate μ_hat e_hat goodSet Δ hΔ hfail h_mu_meas h_e_meas h_mu_memLp h_e_memLp h_e_overlap h_mu_uncurry_foldA h_e_uncurry_foldA h_mu_rate h_e_rate h_product_rate exact hAL.tendsto_normal_foldB split hψ_meas hθn_meas hSum_meas
    Causalean.Estimation.ATE.dml_ATE_tendstoNormal_on_highProbEvent · Causalean/Estimation/ATE/DML/AsymptoticNormality.lean:32