Estimation.ATE
Sample-split AIPW/DML estimation of the back-door average treatment effect: the moment function, its influence function, square-integrability, and the asymptotic-linearity theorem.
Score 20 core · 23 supporting · 5 submodules AIPW score infrastructure for ATE DML: moment definitions, influence functions, finite variance, mean-zero identities, L2 continuity, and pull-out lemmas. Remainder 4 core · 2 supporting · 2 submodules Public entry point for the AIPW second-order remainder theory for back-door average treatment effect estimation.
Setup 8 core · 3 supporting Defines the estimation-layer structure used by back-door ATE estimators. ★ θ₀_eq_ATE
Defines the estimation-layer structure used by back-door ATE estimators.
The file introduces BackdoorEstimationSystem, its strict-overlap predicate
StrictOverlap, the covariate and observed-data laws P_X and P_Z, and the
value-space estimand θ₀. It proves that θ₀ agrees with the PO-level ATE
under the back-door assumptions, derives counterfactual compatibility as
μ_compat, and provides POBackdoorSystem.toBackdoorEstimationSystem to show
that the added value-space compatibility and positivity fields are obtainable
from observable lifts rather than extra causal assumptions.
structure BackdoorEstimationSystem reviewed
⚑ flagged
Causalean.Estimation.ATE
A back-door estimation system extends a potential-outcome back-door system with value-space representatives of the nuisance parameters used by AIPW-style estimators: an outcome regression μ(a,x) and a propensity score e(x) that is bounded away from 0 and away from 1, together with the outcome regression's agreement, almost everywhere, with the σ(X)-measurable observable regression adjustedCE, composed with the factual covariate and the analogous agreement of the propensity score with the observable propensity propScore.
Definition (Lean source)
parameters
fields
Value-space outcome regression `μ(a, x)`.
μ_val :
Bool → γ → ℝ
μ_meas :
∀ b, Measurable (μ_val b)
Value-space propensity `e(x) ∈ (0, 1)`.
e_val :
γ → ℝ
e_meas :
Measurable e_val
e_pos :
∀ x, 0 < e_val x
e_lt_one :
∀ x, e_val x < 1
The value-space outcome regression `μ_val` represents the **observable**
adjustment functional `adjustedCE d = E[Y·1_{D=d}|σX] / P[D=d|σX]`, with NO
identification assumptions: `μ_val d (factualX ·) =ᵐ adjustedCE d`. This is the
ML/regression target (`adjustedCE` is the regression `E[Y|D=d,X]`, see
`regression_adjustment`). The counterfactual reading
`μ[Y(d)|σX] =ᵐ μ_val d ∘ factualX` is NOT assumed here — it is the *derived*
lemma `μ_compat` below, which additionally requires `Assumptions` via
back-door identification (`cate_backdoor`).
μ_reg_compat :
∀ d : Bool,
(fun ω => μ_val d (toPOBackdoorSystem.factualX ω)) =ᵐ[P.μ] toPOBackdoorSystem.adjustedCE d
Propensity factors through `factualX`:
`propScore true =ᵐ e_val (factualX ·)`.
e_compat :
toPOBackdoorSystem.propScore true =ᵐ[P.μ] (fun ω => e_val (toPOBackdoorSystem.factualX ω))
def StrictOverlap reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Strict-overlap predicate ε ≤ propScore true ω ≤ 1 − ε a.s., with ε ∈ (0, 1/2]. Restated to the value-space propensity via e_compat.
Definition (Lean source)
def StrictOverlap (S : BackdoorEstimationSystem P γ) (ε : ℝ) : Prop :=
0 < ε ∧ ε ≤ 1 / 2 ∧
(∀ᵐ ω ∂P.μ, ε ≤ S.toPOBackdoorSystem.propScore true ω ∧
S.toPOBackdoorSystem.propScore true ω ≤ 1 - ε)
def P_X reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Covariate marginal: P_X := μ.map factualX.
Definition (Lean source)
noncomputable def P_X (S : BackdoorEstimationSystem P γ) : Measure γ :=
P.μ.map S.toPOBackdoorSystem.factualX
def factualZ reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Data triple (X, A, Y) : Ω → γ × Bool × ℝ.
Definition (Lean source)
noncomputable def factualZ (S : BackdoorEstimationSystem P γ) :
P.Ω → γ × Bool × ℝ :=
fun ω => (S.toPOBackdoorSystem.factualX ω,
S.toPOBackdoorSystem.factualD ω,
S.toPOBackdoorSystem.factualY ω)
def P_Z reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Joint data law P_Z := μ.map (X, A, Y).
Definition (Lean source)
noncomputable def P_Z (S : BackdoorEstimationSystem P γ) :
Measure (γ × Bool × ℝ) :=
P.μ.map S.factualZ
def θ₀ reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Value-space ATE: θ₀ = ∫ (μ(1, x) - μ(0, x)) dP_X.
Definition (Lean source)
noncomputable def θ₀ (S : BackdoorEstimationSystem P γ) : ℝ :=
∫ x, S.μ_val true x - S.μ_val false x ∂(S.P_X)
theorem θ₀_eq_ATE reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Value-space estimand equals the potential-outcome ATE. Under the back-door identification assumptions, the value-space estimand θ₀ = ∫ (μ(1,x) − μ(0,x)) dP_X, built from the outcome-regression nuisance, coincides with the average treatment effect defined on potential outcomes.
Formal statement
hypotheses
S :
hA :
S.toPOBackdoorSystem.Assumptions
conclusion
S.θ₀ = S.toPOBackdoorSystem.ATE
Proof (Lean source)
theorem θ₀_eq_ATE (S : BackdoorEstimationSystem P γ)
(hA : S.toPOBackdoorSystem.Assumptions) :
S.θ₀ = S.toPOBackdoorSystem.ATE := by
unfold BackdoorEstimationSystem.θ₀ BackdoorEstimationSystem.P_X PO.POBackdoorSystem.ATE
have hmeas_diff : Measurable (fun x => S.μ_val true x - S.μ_val false x) :=
(S.μ_meas true).sub (S.μ_meas false)
rw [MeasureTheory.integral_map S.toPOBackdoorSystem.measurable_factualX.aemeasurable
hmeas_diff.aestronglyMeasurable]
have hcompat :
(fun ω => S.μ_val true (S.toPOBackdoorSystem.factualX ω) -
S.μ_val false (S.toPOBackdoorSystem.factualX ω))
=ᵐ[P.μ]
(fun ω => P.μ[S.toPOBackdoorSystem.YofD true | S.toPOBackdoorSystem.sigmaX] ω -
P.μ[S.toPOBackdoorSystem.YofD false | S.toPOBackdoorSystem.sigmaX] ω) :=
(S.μ_compat hA true).symm.sub (S.μ_compat hA false).symm
rw [MeasureTheory.integral_congr_ae hcompat]
have hsub :
P.μ[S.toPOBackdoorSystem.YofD true - S.toPOBackdoorSystem.YofD false |
S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ]
(fun ω => P.μ[S.toPOBackdoorSystem.YofD true | S.toPOBackdoorSystem.sigmaX] ω -
P.μ[S.toPOBackdoorSystem.YofD false | S.toPOBackdoorSystem.sigmaX] ω) :=
MeasureTheory.condExp_sub hA.integrable_Y1 hA.integrable_Y0 S.toPOBackdoorSystem.sigmaX
rw [MeasureTheory.integral_congr_ae hsub.symm]
rw [MeasureTheory.integral_condExp S.toPOBackdoorSystem.sigmaX_le]
rfl
def toBackdoorEstimationSystem reviewed
⚑ flagged
Causalean.PO.POBackdoorSystem
The compatibility/positivity fields are free. From a POBackdoorSystem with a.e. two-sided overlap and an integrable observed outcome — and no unconfoundedness — one constructs a BackdoorEstimationSystem: μ_val is the value-space outcome regression regFn and e_val is the propensity lift eLift clamped into (0,1) off-support. Every added field is discharged (μ_reg_compat from regression_adjustment; e_pos/e_lt_one from the clamp; e_compat from overlap). So BackdoorEstimationSystem carries no assumption beyond POBackdoorSystem + overlap + integrability — in particular the value-space lifts (μ_compat, e_compat) were never genuine assumptions.
Definition (Lean source)
noncomputable def _root_.Causalean.PO.POBackdoorSystem.toBackdoorEstimationSystem
{P : POSystem} {γ : Type*} [MeasurableSpace γ]
(S : PO.POBackdoorSystem P γ) [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(hov : ∀ᵐ ω ∂P.μ, 0 < S.propScore true ω ∧ S.propScore true ω < 1)
(hY : Integrable S.factualY P.μ) :
BackdoorEstimationSystem P γ where
toPOBackdoorSystem := S
μ_val := fun b x => S.regFn (b, x)
μ_meas := fun _ => S.measurable_regFn.comp (measurable_const.prodMk measurable_id)
e_val := Set.piecewise {x : γ | 0 < S.eLift x ∧ S.eLift x < 1} S.eLift (fun _ => 1 / 2)
e_meas := by
refine Measurable.piecewise ?_ S.measurable_eLift measurable_const
exact (measurableSet_lt measurable_const S.measurable_eLift).inter
(measurableSet_lt S.measurable_eLift measurable_const)
e_pos := by
intro x
by_cases hx : x ∈ {x : γ | 0 < S.eLift x ∧ S.eLift x < 1}
· rw [Set.piecewise_eq_of_mem _ _ _ hx]; exact hx.1
· rw [Set.piecewise_eq_of_notMem _ _ _ hx]; norm_num
e_lt_one := by
intro x
by_cases hx : x ∈ {x : γ | 0 < S.eLift x ∧ S.eLift x < 1}
· rw [Set.piecewise_eq_of_mem _ _ _ hx]; exact hx.2
· rw [Set.piecewise_eq_of_notMem _ _ _ hx]; norm_num
μ_reg_compat := fun d =>
(S.regression_adjustment d hY (S.propScore_ne_of_overlap hov d)).symm
e_compat := by
filter_upwards [hov] with ω hω
have heq : S.propScore true ω = S.eLift (S.factualX ω) :=
congrFun S.propScore_true_eq_eLift ω
have hmem : S.factualX ω ∈ {x : γ | 0 < S.eLift x ∧ S.eLift x < 1} := by
rw [Set.mem_setOf_eq, ← heq]; exact hω
rw [heq, Set.piecewise_eq_of_mem _ _ _ hmem]
3 supporting declarations (lemmas, instances)
-
μ_compatlemma — Counterfactual compatibility (derived, under identification). Recovers the former μ_compat field — the *counterfactual* reading μ[Y(d) | σ(X)] =ᵐ μ_val d ∘ factualX — now as a theorem rather than an assumption. It is the observable μ_reg_compat (μ_val d ∘ factualX =ᵐ adjustedCE d) composed with back-door identification (cate_backdoor : μ[Y(d)|σX] =ᵐ adjustedCE d), so the counterfactual binding is NOT part of the estimation system's data: it holds only under Assumptions. Every downstream proof that used the old field calls this with the ambient hA.hypothesesconclusionP.μ[S.toPOBackdoorSystem.YofD d | S.toPOBackdoorSystem.sigmaX]=ᵐ[P.μ] (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω))Proof (Lean source)
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.cate_backdoor hA d).trans (S.μ_reg_compat d).symm -
measurable_factualZlemma — The observed covariate, treatment, and outcome triple is measurable.Proof (Lean source)
lemma measurable_factualZ (S : BackdoorEstimationSystem P γ) : Measurable S.factualZ := (S.toPOBackdoorSystem.measurable_factualX).prodMk ((S.toPOBackdoorSystem.measurable_factualD).prodMk S.toPOBackdoorSystem.measurable_factualY) -
P_Z_map_projX_eq_P_Xlemma — The covariate marginal P_X is the pushforward of P_Z along the projection (x, a, y) ↦ x. Used to bridge integrals/eLpNorm between P_X (covariates only) and P_Z (full data triple).Proof (Lean source)
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
DML 3 core · 0 supporting This file defines dmlEstimator, the one-shot sample-split augmented inverse-probability weighted estimator for the back-door average treatment effect. ★ dml_ATE_isAsymLinear★ dml_ATE_tendstoNormal
Double Machine Learning for ATE
This file defines dmlEstimator, the one-shot sample-split augmented
inverse-probability weighted estimator for the back-door average treatment
effect. It proves dml_ATE_isAsymLinear, which connects the estimator to the
AIPW influence function under overlap, second-moment, sample-split, and
nuisance-rate conditions, and dml_ATE_tendstoNormal, the resulting fold-scaled
asymptotic normality statement.
def dmlEstimator reviewed
⚑ flagged
Causalean.Estimation.ATE
One-shot DML / AIPW estimator of the back-door ATE (def:est-dml-ate).
Definition (Lean source)
noncomputable def dmlEstimator
(S : BackdoorEstimationSystem P γ)
(sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z)
(split : OneShotSplit sample)
(μ_hat : ℕ → P.Ω → (Bool → γ → ℝ))
(e_hat : ℕ → P.Ω → (γ → ℝ))
(n : ℕ) : P.Ω → ℝ :=
fun ω =>
((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n,
aipwMoment (sample.Z i ω) (μ_hat n ω) (e_hat n ω) 0
theorem dml_ATE_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.ATE
Asymptotic linearity of the one-shot DML ATE — thm:est-dml-ate-al. Fix the back-door identification assumptions for the estimation system S, with strict overlap for the true propensity and a.e. overlap at the same for every learner realization , a finite second moment for the observed outcome, and a finite second moment for each potential outcome. Take a one-shot sample split whose training-fold size fraction converges to a limit with . Suppose the outcome-regression and propensity learners are measurable, lie in at every realization, depend only on the nuisance-training fold , both as functions of that fold alone and jointly with the covariate, and converge individually to the truth in at rate with a product rate of . Then the one-shot DML/AIPW estimator of the back-door ATE is asymptotically linear at the true ATE with influence function along the training folds.
Formal statement
hypotheses
S :
ε :
ℝ
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.μ
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
hc_lt :
c < 1
μ_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_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_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
(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) (hc_lt : c < 1)
(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_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_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
-- 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 ω, η_hat n ω ∈ H_ε_aeL2 S ε := by
intro n ω
refine ⟨h_e_overlap n ω, ?_, ?_⟩
· exact h_mu_memLp n ω
· refine MemLp.of_bound (η_hat n ω).e_meas.aestronglyMeasurable 1 ?_
filter_upwards [h_e_overlap n ω] 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 ω a, MemLp
(fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X := by
intro n ω a
exact (h_mu_memLp n ω a).sub (hμ_val_memLp a)
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
-- 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
have h_add_one : ∀ {Xn Yn : ℕ → P.Ω → ℝ},
IsLittleOp Xn (fun _ => (1 : ℝ)) P.μ →
IsLittleOp Yn (fun _ => (1 : ℝ)) P.μ →
IsLittleOp (fun n ω => Xn n ω + Yn n ω) (fun _ => (1 : ℝ)) P.μ := by
intro Xn Yn hX hY ε hε
rw [ENNReal.tendsto_nhds_zero]
intro δ hδ
by_cases hδtop : δ = ⊤
· filter_upwards with n
simp [hδtop]
have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop
let α : ℝ := δ.toReal / 4
have hαpos : 0 < α := by
dsimp [α]
linarith
let A : ℕ → Set P.Ω := fun n => {ω | (ε / 2) * (1 : ℝ) < |Xn n ω|}
let B : ℕ → Set P.Ω := fun n => {ω | (ε / 2) * (1 : ℝ) < |Yn n ω|}
let C : ℕ → Set P.Ω := fun n => {ω | ε * (1 : ℝ) < |Xn n ω + Yn n ω|}
have hXevent_le := (ENNReal.tendsto_nhds_zero.mp (hX (ε / 2) (by linarith)))
(ofReal α) (ENNReal.ofReal_pos.mpr hαpos)
have hYevent_le := (ENNReal.tendsto_nhds_zero.mp (hY (ε / 2) (by linarith)))
(ofReal α) (ENNReal.ofReal_pos.mpr hαpos)
have htwo_alpha_lt_delta : ofReal (2 * α) < δ := by
rw [ENNReal.ofReal_lt_iff_lt_toReal]
· dsimp [α]
linarith
· dsimp [α]
linarith [le_of_lt hδpos]
· exact hδtop
filter_upwards [hXevent_le, hYevent_le] with n hXA hYB
have hsubset : C n ⊆ A n ∪ B n := by
intro ω hω
by_contra hnot
have hnotA : ¬ ε / 2 < |Xn n ω| := by
intro hx
exact hnot (inl (by simpa [A] using hx))
have hnotB : ¬ ε / 2 < |Yn n ω| := by
intro hy
exact hnot (inr (by simpa [B] using hy))
have hXle : |Xn n ω| ≤ ε / 2 := le_of_not_gt hnotA
have hYle : |Yn n ω| ≤ ε / 2 := le_of_not_gt hnotB
have hsum : |Xn n ω + Yn n ω| ≤ ε := by
-- … truncated; follow the source link for the rest …
theorem dml_ATE_tendstoNormal reviewed
⚑ flagged
Causalean.Estimation.ATE
Asymptotic normality of the one-shot DML ATE (thm:est-dml-ate-al, "In particular ..." clause). Under the back-door identification assumptions for S, with strict overlap for the true propensity and a.e. overlap for every learner realization, finite second moments of the observed and potential outcomes, and a one-shot sample split whose training-fold fraction converges to some c with 0 < c < 1: suppose the learners μ̂, ê are measurable, in L²(P_X) at every realization, depend only on the nuisance-training fold, marginally and jointly with the covariate, and converge individually at rate o_p(1) with product rate o_p(n^{-1/2}) — the same hypotheses as dml_ATE_isAsymLinear. Given in addition measurability of the AIPW influence function, a.e. measurability of the rescaled estimator at every horizon, and a.e. measurability of the normalized influence-sum at every horizon, then the rescaled estimator √|B(n)| (θ̂ⁿ − θ₀) converges in distribution to N(0, ∫ ψ_AIPW² dP_Z).
Formal statement
hypotheses
S :
ε :
ℝ
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.μ
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
hc_lt :
c < 1
μ_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_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_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
Tendsto_dist (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) (gaussianMeasure 0 (∫ x, (S.ψ_AIPW x) ^ 2 ∂S.P_Z)) P.μ hθn_meas
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) (hc_lt : c < 1)
(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_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_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.μ) :
Tendsto_dist
(IsAsymLinear.rescaledEstimator
(dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB)
(gaussianMeasure 0 (∫ x, (S.ψ_AIPW x) ^ 2 ∂S.P_Z))
P.μ
hθn_meas := by
haveI : IsProbabilityMeasure P.μ := inferInstance
have hAL :=
dml_ATE_isAsymLinear S hA h_overlap h_y2 h_yd2 sample split
hc_pos hc_lt h_split_rate μ_hat e_hat h_mu_meas h_e_meas
h_mu_memLp h_e_memLp h_e_overlap
h_mu_foldA h_e_foldA 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
PlugIn 4 core · 0 supporting This file defines the sample-split plug-in estimator for the back-door average treatment effect using only the estimated outcome regression. ★ plugIn_isAsymLinear★ plugIn_tendstoNormal
Plug-In ATE Estimator
This file defines the sample-split plug-in estimator for the back-door average treatment effect using only the estimated outcome regression. It also records the corresponding influence function and the asymptotic-linearity statement that compares this estimator with the target average treatment effect.
The main declarations are plugInEstimator, ψ_plugin,
plugIn_isAsymLinear, and plugIn_tendstoNormal. The proofs use the
covariate-law representation of the ATE, fold-B empirical-process bounds, and
the L² rate of the outcome-regression nuisance to control the plug-in bias.
def plugInEstimator reviewed
⚑ flagged
Causalean.Estimation.ATE
Sample-split plug-in estimator of the back-door ATE (def:est-plug-in-ate).
Definition (Lean source)
noncomputable def plugInEstimator
(S : BackdoorEstimationSystem P γ)
(sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z)
(split : OneShotSplit sample)
(μ_hat : ℕ → P.Ω → (Bool → γ → ℝ))
(n : ℕ) : P.Ω → ℝ :=
fun ω =>
((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n,
(μ_hat n ω true (projX (sample.Z i ω))
- μ_hat n ω false (projX (sample.Z i ω)))
def ψ_plugin reviewed
⚑ flagged
Causalean.Estimation.ATE
Plug-in influence function ψ_plugin(z) := μ(1, x) − μ(0, x) − θ₀ from thm:est-plug-in-ate-al.
theorem plugIn_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.ATE
Asymptotic linearity of the plug-in ATE — thm:est-plug-in-ate-al. Fix the back-door identification assumptions for S, square-integrability of both potential outcomes, and a one-shot sample split whose training-fold fraction converges to some c with 0 < c < 1. Suppose the outcome-regression learner μ̂ is measurable, lies in L²(P_X) at every realization, and depends only on the nuisance-training fold, marginally and jointly with the covariate, with joint L²(P_X) estimation error at rate o_p(n^{-1/2}). Then the sample-split plug-in estimator of the back-door ATE is asymptotically linear at the true ATE θ₀ with influence function ψ_plugin along the training folds.
Formal statement
hypotheses
S :
hA :
S.toPOBackdoorSystem.Assumptions
h_yd2 :
∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
hc_lt :
c < 1
μ_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_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (μ_hat n)
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.μ
conclusion
Proof (Lean source)
theorem plugIn_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) (hc_lt : c < 1)
(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_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(μ_hat n))
(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.CATE d) P.μ := fun d => by
unfold POBackdoorSystem.CATE
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_sub hbase_int hθ_int,
← 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_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(fun ω => fZ n ω) := by
intro n
change Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(fun ω (z : γ × Bool × ℝ) =>
(μ_hat n ω true z.1 - S.μ_val true z.1) -
(μ_hat n ω false z.1 - S.μ_val false z.1))
fun_prop
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)
-- … truncated; follow the source link for the rest …
theorem plugIn_tendstoNormal reviewed
⚑ flagged
Causalean.Estimation.ATE
Asymptotic normality of the plug-in ATE (thm:est-plug-in-ate-al, "In particular ..." clause). Under the back-door identification assumptions for S, square-integrability of both potential outcomes, and a one-shot sample split whose training-fold fraction converges to some c with 0 < c < 1: suppose the learner μ̂ is measurable, in L²(P_X) at every realization, depends only on the nuisance-training fold, marginally and jointly with the covariate, with joint L²(P_X) estimation error at rate o_p(n^{-1/2}) — the same hypotheses as plugIn_isAsymLinear. Given in addition a.e. measurability of the rescaled estimator at every horizon and a.e. measurability of the normalized influence-sum at every horizon, then the rescaled estimator √|B(n)| (θ̂ⁿ − θ₀) converges in distribution to N(0, ∫ ψ_plugin² dP_Z).
Formal statement
hypotheses
S :
hA :
S.toPOBackdoorSystem.Assumptions
h_yd2 :
∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
hc_lt :
c < 1
μ_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_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (μ_hat n)
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.μ
hθn_meas :
∀ n : ℕ,
AEMeasurable (IsAsymLinear.rescaledEstimator (plugInEstimator S sample split μ_hat) S.θ₀ split.foldB n) P.μ
hSum_meas :
∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (ψ_plugin S) split.foldB n) P.μ
conclusion
Tendsto_dist (IsAsymLinear.rescaledEstimator (plugInEstimator S sample split μ_hat) S.θ₀ split.foldB) (gaussianMeasure 0 (∫ x, (ψ_plugin S x) ^ 2 ∂S.P_Z)) P.μ hθn_meas
Proof (Lean source)
theorem plugIn_tendstoNormal
(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) (hc_lt : c < 1)
(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_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(μ_hat n))
(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.μ)
(hθn_meas : ∀ n : ℕ, AEMeasurable
(IsAsymLinear.rescaledEstimator
(plugInEstimator S sample split μ_hat) S.θ₀ split.foldB n) P.μ)
(hSum_meas : ∀ n : ℕ, AEMeasurable
(IsAsymLinear.normalizedSum sample (ψ_plugin S) split.foldB n) P.μ) :
Tendsto_dist
(IsAsymLinear.rescaledEstimator
(plugInEstimator S sample split μ_hat) S.θ₀ split.foldB)
(gaussianMeasure 0 (∫ x, (ψ_plugin S x) ^ 2 ∂S.P_Z))
P.μ
hθn_meas := by
haveI : IsProbabilityMeasure P.μ := inferInstance
have hAL :=
plugIn_isAsymLinear S hA h_yd2 sample split
hc_pos hc_lt h_split_rate μ_hat h_mu_meas h_mu_memLp h_mu_foldA
h_mu_uncurry_foldA h_rate
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
exact hAL.tendsto_normal_foldB split hψ_meas hθn_meas hSum_meas