Estimation.ATE · Causalean Library

Setup 8 core · 5 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

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

P :

POSystem

γ :

Type*

MeasurableSpace γ

StandardBorelSpace P.Ω

IsFiniteMeasure P.μ

extends :

POBackdoorSystem P γ

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 ω))

Causalean.Estimation.ATE.BackdoorEstimationSystem · Causalean/Estimation/ATE/Setup.lean:52 · uses POSystem

def StrictOverlap reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For a potential-outcome system with a standard-Borel sample space and finite probability measure, a measurable covariate space, a back-door estimation system, and a real overlap level, the strict-overlap condition holds precisely when $ε>0$ , $ε\leq 1/2$ , and almost surely under the population measure, the probability of treatment is between $ε$ and $1-ε$ .

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

BackdoorEstimationSystem P γ

ε :

ℝ

def

StrictOverlap S ε :

Prop

given by

clause 1

0 < ε

clause 2

ε ≤ 1 / 2

clause 3

∀ᵐ ω ∂P.μ, ε

≤ S.toPOBackdoorSystem.propScore true ω ∧ S.toPOBackdoorSystem.propScore true ω ≤ 1 - ε

Causalean.Estimation.ATE.BackdoorEstimationSystem.StrictOverlap · Causalean/Estimation/ATE/Setup.lean:115 · uses BackdoorEstimationSystem , POSystem

def P_X reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For a potential-outcome system with a standard-Borel sample space and finite probability measure, a measurable covariate space, and a back-door estimation system, the covariate marginal law is the image of the population measure under the factual covariate.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

BackdoorEstimationSystem P γ

def

P_X S :

Measure γ

given by

P.μ.map S.toPOBackdoorSystem.factualX

Causalean.Estimation.ATE.BackdoorEstimationSystem.P_X · Causalean/Estimation/ATE/Setup.lean:125 · uses BackdoorEstimationSystem , POSystem

def factualZ reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For a potential-outcome system with a standard-Borel sample space and finite probability measure, a measurable covariate space, and a back-door estimation system, the factual data map sends every sample point to its observed covariate, binary treatment, and outcome triple.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

BackdoorEstimationSystem P γ

def

factualZ S :

P.Ω → γ × Bool × ℝ

given by

fun ω

=> (S.toPOBackdoorSystem.factualX ω, S.toPOBackdoorSystem.factualD ω, S.toPOBackdoorSystem.factualY ω)

Causalean.Estimation.ATE.BackdoorEstimationSystem.factualZ · Causalean/Estimation/ATE/Setup.lean:136 · uses BackdoorEstimationSystem , POSystem

def P_Z reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For a potential-outcome system with a standard-Borel sample space and finite probability measure, a measurable covariate space, and a back-door estimation system, the observed-data law is the image of the population measure under the factual covariate--treatment--outcome map.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

BackdoorEstimationSystem P γ

def

P_Z S :

Measure (γ × Bool × ℝ)

given by

P.μ.map S.factualZ

Causalean.Estimation.ATE.BackdoorEstimationSystem.P_Z · Causalean/Estimation/ATE/Setup.lean:151 · uses BackdoorEstimationSystem , POSystem

def θ₀ reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For a potential-outcome system with a standard-Borel sample space and finite probability measure, a measurable covariate space, and a back-door estimation system, the value-space average treatment effect is the covariate-law integral of the true treated outcome regression minus the true control outcome regression.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

BackdoorEstimationSystem P γ

def

θ₀ S :

ℝ

given by

∫ x, S.μ_val true x - S.μ_val false x ∂(S.P_X)

Causalean.Estimation.ATE.BackdoorEstimationSystem.θ₀ · Causalean/Estimation/ATE/Setup.lean:175 · uses BackdoorEstimationSystem , POSystem

theorem θ₀_eq_ATE reviewed

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

P :

POSystem

shared

γ :

Type u_1

shared

S :

BackdoorEstimationSystem P γ

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

Causalean.Estimation.ATE.BackdoorEstimationSystem.θ₀_eq_ATE · Causalean/Estimation/ATE/Setup.lean:179 · uses BackdoorEstimationSystem , θ₀ , ATE , Assumptions , POSystem

def toBackdoorEstimationSystem reviewed

Causalean.PO.POBackdoorSystem

Given a potential-outcome system with a standard-Borel sample space and finite probability measure, a measurable covariate space, a back-door potential-outcome system, the assumption that its treated propensity is strictly between zero and one almost surely, and an integrable factual outcome, the associated back-door estimation system uses the value-space outcome regression and a propensity score that equals the lifted propensity on its strict-overlap support and equals one half elsewhere.

Definition (Lean source)

parameters

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.μ

def

toBackdoorEstimationSystem S hov hY :

BackdoorEstimationSystem P γ

given by

clause 1

toPOBackdoorSystem := S

clause 2

μ_val := fun b x => S.regFn (b, x)

clause 3

μ_meas := fun _ => S.measurable_regFn.comp (measurable_const.prodMk measurable_id)

clause 4

e_val := Set.piecewise {x : γ | 0 < S.eLift x ∧ S.eLift x < 1} S.eLift (fun _ => 1 / 2)

clause 5

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)

clause 6

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

clause 7

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

clause 8

μ_reg_compat := fun d

=> (S.regression_adjustment d hY (S.propScore_ne_of_overlap hov d)).symm

clause 9

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]

Causalean.PO.POBackdoorSystem.toBackdoorEstimationSystem · Causalean/Estimation/ATE/Setup.lean:217 · uses BackdoorEstimationSystem , POBackdoorSystem , factualY , propScore , POSystem

5 supporting declarations (lemmas, instances)

μ_compat lemma — 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.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

hA :

S.toPOBackdoorSystem.Assumptions

d :

Bool

conclusion

P.μ[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

Causalean.Estimation.ATE.BackdoorEstimationSystem.μ_compat · Causalean/Estimation/ATE/Setup.lean:101
P_X_eq lemma — The covariate marginal is the image of the population measure under the factual covariate map.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

conclusion

S.P_X = P.μ.map S.toPOBackdoorSystem.factualX

Proof (Lean source)

@[causal_defs_simps] lemma P_X_eq (S : BackdoorEstimationSystem P γ) : S.P_X = P.μ.map S.toPOBackdoorSystem.factualX := rfl

Causalean.Estimation.ATE.BackdoorEstimationSystem.P_X_eq · Causalean/Estimation/ATE/Setup.lean:129
measurable_factualZ lemma — The observed covariate, treatment, and outcome triple is measurable.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

conclusion

Measurable S.factualZ

Proof (Lean source)

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

Causalean.Estimation.ATE.BackdoorEstimationSystem.measurable_factualZ · Causalean/Estimation/ATE/Setup.lean:143
P_Z_eq lemma — The joint data law is the image of the population measure under the map recording the observed covariate, treatment, and outcome.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

conclusion

S.P_Z = P.μ.map S.factualZ

Proof (Lean source)

@[causal_defs_simps] lemma P_Z_eq (S : BackdoorEstimationSystem P γ) : S.P_Z = P.μ.map S.factualZ := rfl

Causalean.Estimation.ATE.BackdoorEstimationSystem.P_Z_eq · Causalean/Estimation/ATE/Setup.lean:156
P_Z_map_projX_eq_P_X lemma — 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).

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

conclusion

S.P_Z.map (fun z : γ × Bool × ℝ => z.1) = S.P_X

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

Causalean.Estimation.ATE.BackdoorEstimationSystem.P_Z_map_projX_eq_P_X · Causalean/Estimation/ATE/Setup.lean:163

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

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.lean:62 · uses BackdoorEstimationSystem , P_Z , POSystem , IIDSample , OneShotSplit

theorem dml_ATE_isAsymLinear reviewed

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 $\varepsilon \le e(X) \le 1-\varepsilon$ for the true propensity and a.e. overlap at the same $\varepsilon$ for every learner realization $\hat e(n,\omega)$ , 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 $c$ with $0 < c < 1$ . Suppose the outcome-regression and propensity learners $\hat\mu, \hat e$ are measurable, lie in $L^2(P_X)$ at every realization, depend only on the nuisance-training fold $A(n)$ , both as functions of that fold alone and jointly with the covariate, and converge individually to the truth in $L^2(P_X)$ at rate $o_p(1)$ with a product rate of $o_p(n^{-1/2})$ . Then the one-shot DML/AIPW estimator of the back-door ATE is asymptotically linear at the true ATE $\theta_0$ with influence function $\psi_{AIPW}$ along the training folds.

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

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.μ

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 …

Causalean.Estimation.ATE.dml_ATE_isAsymLinear · Causalean/Estimation/ATE/DML.lean:101 · uses BackdoorEstimationSystem , P_X , P_Z , StrictOverlap , θ₀ , ψ_AIPW , dmlEstimator , Assumptions , YofD , factualY , POSystem , IIDSample , IsAsymLinear , IsLittleOp , OneShotSplit , foldA , foldB

theorem dml_ATE_tendstoNormal reviewed

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

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

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.μ

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

Causalean.Estimation.ATE.dml_ATE_tendstoNormal · Causalean/Estimation/ATE/DML.lean:936 · uses BackdoorEstimationSystem , P_X , P_Z , StrictOverlap , θ₀ , ψ_AIPW , dmlEstimator , Assumptions , YofD , factualY , POSystem , IIDSample , normalizedSum , rescaledEstimator , IsLittleOp , OneShotSplit , foldA , foldB , Tendsto_dist , gaussianMeasure , instIsProbabilityMeasureGaussianMeasure

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

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, and a nonnegative integer sample-size index, the sample-split plug-in estimator of the back-door average treatment effect assigns to each population realization the estimation-fold average of the estimated treated-minus-control outcome regression at the observed covariates.

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 → γ → ℝ)

n :

ℕ

def

plugInEstimator S sample split μ_hat n :

P.Ω → ℝ

given by

fun ω

=> ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, (μ_hat n ω true (projX (sample.Z i ω)) - μ_hat n ω false (projX (sample.Z i ω)))

Causalean.Estimation.ATE.plugInEstimator · Causalean/Estimation/ATE/PlugIn.lean:64 · uses BackdoorEstimationSystem , P_Z , POSystem , IIDSample , OneShotSplit

def ψ_plugin reviewed

Causalean.Estimation.ATE

For a potential-outcome system with a measurable covariate space, a back-door estimation system, and an observed covariate, treatment, and outcome triple, the plug-in influence-function value is the true treated-minus-control outcome regression at that triple's covariate, centered at the system's true average treatment effect.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

BackdoorEstimationSystem P γ

z :

γ × Bool × ℝ

def

ψ_plugin S z :

ℝ

given by

S.μ_val true (projX z) - S.μ_val false (projX z) - S.θ₀

Causalean.Estimation.ATE.ψ_plugin · Causalean/Estimation/ATE/PlugIn.lean:98 · uses BackdoorEstimationSystem , POSystem

theorem plugIn_isAsymLinear reviewed

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

P :

POSystem

shared

γ :

Type u_1

shared

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.μ

conclusion

IsAsymLinear (plugInEstimator S sample split μ_hat) S.θ₀ (ψ_plugin S) sample split.foldB

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_linearity rw [← theta_zero_factualX_integral S, hθ_const] ring · -- finite_var: ψ_plugin = (μ_val 1 ∘ X) − (μ_val 0 ∘ X) − θ₀ ∈ L²(P_Z). -- L² of `μ_val d ∘ factualX` follows from `h_yd2` via conditional Jensen -- (cf. `aipw_finite_var`); push to `P_Z` along `factualZ`. have hψ_meas : Measurable (ψ_plugin S) := by unfold ψ_plugin exact (((S.μ_meas true).comp measurable_fst).sub ((S.μ_meas false).comp measurable_fst)).sub measurable_const have hμ_L2 : ∀ d : Bool, MemLp (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := by intro d have hYd_L2 : MemLp (S.toPOBackdoorSystem.YofD d) 2 P.μ := (memLp_two_iff_integrable_sq (S.toPOBackdoorSystem.measurable_YofD d).aestronglyMeasurable).2 (h_yd2 d) have hcond_L2 : MemLp (P.μ[S.toPOBackdoorSystem.YofD d | S.toPOBackdoorSystem.sigmaX]) 2 P.μ := hYd_L2.condExp one_le_two exact hcond_L2.ae_eq (S.μ_compat hA d) have hψ_comp_L2 : MemLp (fun ω => ψ_plugin S (S.factualZ ω)) 2 P.μ := by have hbase_L2 := (hμ_L2 true).sub (hμ_L2 false) have hconst_L2 : MemLp (fun _ : P.Ω => S.θ₀) 2 P.μ := memLp_const _ simp only [ψ_plugin, BackdoorEstimationSystem.factualZ, projX] exact hbase_L2.sub hconst_L2 have hψ_L2 : MemLp (ψ_plugin S) 2 S.P_Z := by rw [BackdoorEstimationSystem.P_Z] exact (memLp_map_measure_iff hψ_meas.aestronglyMeasurable S.measurable_factualZ.aemeasurable).2 hψ_comp_L2 exact hψ_L2.integrable_sq · -- remainder: decompose into centered fold-B fluctuation plus plug-in bias. let δ : ℕ → P.Ω → γ → ℝ := fun n ω x => (μ_hat n ω true x - S.μ_val true x) - (μ_hat n ω false x - S.μ_val false x) let G : ℕ → P.Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (δ n ω (projX (sample.Z i ω)) - ∫ x, δ n ω x ∂S.P_X) let B : ℕ → P.Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * ∫ x, δ n ω x ∂S.P_X let R : ℕ → P.Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * (plugInEstimator S sample split μ_hat n ω - S.θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, ψ_plugin S (sample.Z i ω) have hG : IsLittleOp G (fun _ => (1 : ℝ)) P.μ := by let fZ : ℕ → P.Ω → γ × Bool × ℝ → ℝ := fun n ω z => δ n ω (projX z) haveI : IsProbabilityMeasure S.P_Z := by unfold BackdoorEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable have hf_meas : ∀ n, Measurable (uncurry (fZ n)) := by intro n change Measurable (fun p : P.Ω × (γ × Bool × ℝ) => (μ_hat n p.1 true p.2.1 - S.μ_val true p.2.1) - (μ_hat n p.1 false p.2.1 - S.μ_val false p.2.1)) have hproj : Measurable (fun p : P.Ω × (γ × Bool × ℝ) => (p.1, p.2.1)) := by fun_prop exact (((h_mu_meas n true).comp hproj).sub ((S.μ_meas true).comp measurable_snd.fst)).sub (((h_mu_meas n false).comp hproj).sub ((S.μ_meas false).comp measurable_snd.fst)) have hf_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.μ := -- … truncated; follow the source link for the rest …

Causalean.Estimation.ATE.plugIn_isAsymLinear · Causalean/Estimation/ATE/PlugIn.lean:109 · uses BackdoorEstimationSystem , P_X , P_Z , θ₀ , plugInEstimator , ψ_plugin , Assumptions , YofD , POSystem , IIDSample , IsAsymLinear , IsLittleOp , OneShotSplit , foldA , foldB

theorem plugIn_tendstoNormal reviewed

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

P :

POSystem

shared

γ :

Type u_1

shared

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.μ

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

Causalean.Estimation.ATE.plugIn_tendstoNormal · Causalean/Estimation/ATE/PlugIn.lean:781 · uses BackdoorEstimationSystem , P_X , P_Z , θ₀ , plugInEstimator , ψ_plugin , Assumptions , YofD , POSystem , IIDSample , normalizedSum , rescaledEstimator , IsLittleOp , OneShotSplit , foldA , foldB , Tendsto_dist , gaussianMeasure , instIsProbabilityMeasureGaussianMeasure