Estimation.ATT

AIPW/DML estimation of the average treatment effect on the treated (Hahn-form moment), mirroring the ATE development; the top-level theorem files are pending repair against the current Mathlib pin.

Score 15 core · 22 supporting · 5 submodules AIPW score infrastructure for ATT DML: treated-effect moments, influence functions, finite variance, mean-zero facts, L2 continuity, and arm-specific pull-out lemmas. DML 6 core · 4 supporting · 2 submodules This file defines the population-share oracle comparison for the one-shot sample-split augmented inverse-probability weighted estimator of the back-door average treatment effect on the treated. Remainder 4 core · 0 supporting · 2 submodules How far the population ATT moment moves when the nuisance functions are wrong.

Setup 9 core · 7 supporting Defines the treated-estimation system for ATT estimation under back-door assumptions. ★ θ₀_eq_ATT

Defines the treated-estimation system for ATT estimation under back-door assumptions. The structure bundles value-space representatives for the control outcome regression, propensity score, treatment probability, and compatibility fields needed by ATT AIPW moments.

The file introduces TreatedEstimationSystem, derives the control-arm counterfactual compatibility lemma μ₀_compat, defines the one-sided overlap predicate OneSidedOverlap, the covariate and data laws P_X and P_Z, the value-space target θ₀, and proves θ₀_eq_ATT. It also constructs a TreatedEstimationSystem from a POBackdoorSystem with overlap and an integrable observed outcome via POBackdoorSystem.toTreatedEstimationSystem.

structure TreatedEstimationSystem reviewed

Causalean.Estimation.ATT

A treated estimation system extends a potential-outcome back-door system with a measurable control-arm outcome regression, a measurable propensity score, a pointwise upper propensity bound, almost-everywhere agreement with the observable control regression, and almost-everywhere agreement with the observable propensity.

Definition (Lean source)

parameters

P :

POSystem

γ :

Type*

MeasurableSpace γ

StandardBorelSpace P.Ω

IsFiniteMeasure P.μ

extends :

POBackdoorSystem P γ

fields

Value-space control-arm outcome regression `μ₀(x)`.

μ₀_val :

γ → ℝ

μ₀_meas :

Measurable μ₀_val

Value-space propensity `e(x)`.

e_val :

γ → ℝ

e_meas :

Measurable e_val

Pointwise upper bound on the value-space propensity.

e_lt_one :

∀ x, e_val x < 1

The control-arm regression `μ₀_val` represents the **observable** adjustment functional `adjustedCE false = E[Y·1_{D=0}|σX] / P[D=0|σX]`, with NO identification assumptions: `μ₀_val (factualX ·) =ᵐ adjustedCE false`. This is the ML/regression target (`adjustedCE false` is the control regression `E[Y|D=0,X]`, see `regression_adjustment`). The counterfactual reading `μ[Y(0)|σX] =ᵐ μ₀_val ∘ factualX` is NOT assumed here — it is the *derived* lemma `μ₀_compat` below, which requires the one-sided ATT backdoor assumptions.

μ₀_reg_compat :

(fun ω => μ₀_val (toPOBackdoorSystem.factualX ω))

=ᵐ[P.μ] toPOBackdoorSystem.adjustedCE false

Propensity factors through `factualX`: `propScore true =ᵐ e_val (factualX ·)`.

e_compat :

toPOBackdoorSystem.propScore true =ᵐ[P.μ] (fun ω => e_val (toPOBackdoorSystem.factualX ω))

Causalean.Estimation.ATT.TreatedEstimationSystem · Causalean/Estimation/ATT/Setup.lean:59 · uses POSystem

def OneSidedOverlap reviewed

Causalean.Estimation.ATT.TreatedEstimationSystem

For a potential-outcome system with a measurable covariate space, a treated estimation system, and a real margin, the one-sided overlap condition holds exactly when $0<ε≤1/2$ and the conditional probability of treatment given the covariates is at most $1-ε$ almost surely under the population measure.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

ε :

ℝ

def

OneSidedOverlap S ε :

Prop

given by

clause 1

0 < ε

clause 2

ε ≤ 1 / 2

clause 3

∀ᵐ ω ∂P.μ, S.toPOBackdoorSystem.propScore true ω ≤ 1 - ε

Causalean.Estimation.ATT.TreatedEstimationSystem.OneSidedOverlap · Causalean/Estimation/ATT/Setup.lean:146 · uses TreatedEstimationSystem , POSystem

def P_X reviewed

Causalean.Estimation.ATT.TreatedEstimationSystem

For a potential-outcome system with a measurable covariate space and a treated estimation system, the covariate distribution is the image of the population measure under the factual covariate.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

def

P_X S :

Measure γ

given by

P.μ.map S.toPOBackdoorSystem.factualX

Causalean.Estimation.ATT.TreatedEstimationSystem.P_X · Causalean/Estimation/ATT/Setup.lean:161 · uses TreatedEstimationSystem , POSystem

def factualZ reviewed

Causalean.Estimation.ATT.TreatedEstimationSystem

For a potential-outcome system with a measurable covariate space and a treated estimation system, the factual data-recording map sends every population unit to its observed covariate, observed treatment, and observed outcome.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

def

factualZ S :

P.Ω → γ × Bool × ℝ

given by

fun ω

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

Causalean.Estimation.ATT.TreatedEstimationSystem.factualZ · Causalean/Estimation/ATT/Setup.lean:174 · uses TreatedEstimationSystem , POSystem

def P_Z reviewed

Causalean.Estimation.ATT.TreatedEstimationSystem

For a potential-outcome system with a measurable covariate space and a treated estimation system, the joint observable-data distribution is the image of the population measure under the factual map recording covariate, treatment, and outcome.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

def

P_Z S :

Measure (γ × Bool × ℝ)

given by

P.μ.map S.factualZ

Causalean.Estimation.ATT.TreatedEstimationSystem.P_Z · Causalean/Estimation/ATT/Setup.lean:191 · uses TreatedEstimationSystem , POSystem

def π_val reviewed

Causalean.Estimation.ATT.TreatedEstimationSystem

For a potential-outcome system with a measurable covariate space and a treated estimation system, the marginal treatment probability is the population probability that the factual treatment equals one.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

def

π_val S :

ℝ

given by

S.toPOBackdoorSystem.propTreated

Causalean.Estimation.ATT.TreatedEstimationSystem.π_val · Causalean/Estimation/ATT/Setup.lean:217 · uses TreatedEstimationSystem , POSystem

def θ₀ reviewed

Causalean.Estimation.ATT.TreatedEstimationSystem

For a potential-outcome system with a measurable covariate space and a treated estimation system, the value-space average treatment effect on the treated is the system's adjusted control-regression functional.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

def

θ₀ S :

ℝ

given by

S.toPOBackdoorSystem.adjustedATT

Causalean.Estimation.ATT.TreatedEstimationSystem.θ₀ · Causalean/Estimation/ATT/Setup.lean:226 · uses TreatedEstimationSystem , POSystem

theorem θ₀_eq_ATT reviewed

Causalean.Estimation.ATT.TreatedEstimationSystem

Value-space estimand equals the potential-outcome ATT. Under the one-sided back-door ATT assumptions, the value-space ATT estimand θ₀ (the adjusted control-regression functional) coincides with the average treatment effect on the treated defined on potential outcomes.

Formal statement

hypotheses

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

hA :

S.toPOBackdoorSystem.ATTAssumptions

conclusion

S.θ₀ = S.toPOBackdoorSystem.ATT

Proof (Lean source)

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

Causalean.Estimation.ATT.TreatedEstimationSystem.θ₀_eq_ATT · Causalean/Estimation/ATT/Setup.lean:235 · uses TreatedEstimationSystem , θ₀ , ATT , ATTAssumptions , POSystem

def toTreatedEstimationSystem reviewed

Causalean.PO.POBackdoorSystem

Given a potential-outcome system with a measurable covariate space, a potential-outcome back-door system, the condition that its conditional probability of treatment lies strictly between zero and one almost surely, and an integrable factual outcome, the constructed treated estimation system extends that back-door system with a control-arm outcome regression and a propensity-score representative bounded strictly below one.

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

toTreatedEstimationSystem S hov hY :

TreatedEstimationSystem P γ

given by

clause 1

toPOBackdoorSystem := S

clause 2

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

clause 3

μ₀_meas := S.measurable_regFn.comp (measurable_const.prodMk measurable_id)

clause 4

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

clause 5

e_meas := Measurable.piecewise (measurableSet_lt S.measurable_eLift measurable_const) S.measurable_eLift measurable_const

clause 6

e_lt_one := by intro x by_cases hx : x ∈ {x : γ | S.eLift x < 1} · rw [Set.piecewise_eq_of_mem _ _ _ hx]; exact hx · rw [Set.piecewise_eq_of_notMem _ _ _ hx]; norm_num

clause 7

μ₀_reg_compat := (S.regression_adjustment false hY (S.propScore_ne_of_overlap hov false)).symm

clause 8

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 : γ | S.eLift x < 1} := by rw [Set.mem_setOf_eq, ← heq]; exact hω.2 rw [heq, Set.piecewise_eq_of_mem _ _ _ hmem]

Causalean.PO.POBackdoorSystem.toTreatedEstimationSystem · Causalean/Estimation/ATT/Setup.lean:252 · uses TreatedEstimationSystem , POBackdoorSystem , factualY , propScore , POSystem

7 supporting declarations (lemmas, instances)

conditionalMeanOutcome_backdoor_control lemma — For a treated-outcome estimation system under the one-sided ATT assumptions, the control-arm conditional mean equals its adjusted control outcome. No treated-arm overlap is used.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

TreatedEstimationSystem P γ

hA :

S.toPOBackdoorSystem.ATTAssumptions

conclusion

S.toPOBackdoorSystem.conditionalMeanOutcome false
=ᵐ[P.μ] S.toPOBackdoorSystem.adjustedCE false

Proof (Lean source)

lemma conditionalMeanOutcome_backdoor_control (S : TreatedEstimationSystem P γ) (hA : S.toPOBackdoorSystem.ATTAssumptions) : S.toPOBackdoorSystem.conditionalMeanOutcome false =ᵐ[P.μ] S.toPOBackdoorSystem.adjustedCE false := S.toPOBackdoorSystem.conditionalMeanOutcome_backdoor_of_propScore_ne hA.consistency false hA.unconfoundedness hA.integrable_Y1 hA.integrable_Y0 hA.propScore_false_ne

Causalean.Estimation.ATT.TreatedEstimationSystem.conditionalMeanOutcome_backdoor_control · Causalean/Estimation/ATT/Setup.lean:111
propScore_true_nonneg_ae lemma — Treated propensity nonnegativity. The conditional treatment probability P[D=1 | X] is nonnegative almost surely because it is the conditional expectation of a nonnegative treatment indicator.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

TreatedEstimationSystem P γ

conclusion

∀ᵐ ω ∂P.μ, 0 ≤ S.toPOBackdoorSystem.propScore true ω

Proof (Lean source)

lemma propScore_true_nonneg_ae (S : TreatedEstimationSystem P γ) : ∀ᵐ ω ∂P.μ, 0 ≤ S.toPOBackdoorSystem.propScore true ω := MeasureTheory.condExp_nonneg (Filter.Eventually.of_forall (fun ω => by rcases S.toPOBackdoorSystem.dVar.indicator_eq_one_or_zero true ω with h | h <;> simp [h]))

Causalean.Estimation.ATT.TreatedEstimationSystem.propScore_true_nonneg_ae · Causalean/Estimation/ATT/Setup.lean:122
μ₀_compat lemma — Counterfactual compatibility (derived, under ATT identification). The control-arm outcome-regression representative equals the conditional mean of the untreated potential outcome given the covariates, almost surely.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

TreatedEstimationSystem P γ

hA :

S.toPOBackdoorSystem.ATTAssumptions

conclusion

P.μ[S.toPOBackdoorSystem.YofD false | S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ] (fun ω => S.μ₀_val (S.toPOBackdoorSystem.factualX ω))

Proof (Lean source)

lemma μ₀_compat (S : TreatedEstimationSystem P γ) (hA : S.toPOBackdoorSystem.ATTAssumptions) : P.μ[S.toPOBackdoorSystem.YofD false | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun ω => S.μ₀_val (S.toPOBackdoorSystem.factualX ω)) := (S.conditionalMeanOutcome_backdoor_control hA).trans S.μ₀_reg_compat.symm

Causalean.Estimation.ATT.TreatedEstimationSystem.μ₀_compat · Causalean/Estimation/ATT/Setup.lean:132
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 :

TreatedEstimationSystem P γ

conclusion

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

Proof (Lean source)

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

Causalean.Estimation.ATT.TreatedEstimationSystem.P_X_eq · Causalean/Estimation/ATT/Setup.lean:167
measurable_factualZ lemma — Measurability of the data triple.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

TreatedEstimationSystem P γ

conclusion

Measurable S.factualZ

Proof (Lean source)

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

Causalean.Estimation.ATT.TreatedEstimationSystem.measurable_factualZ · Causalean/Estimation/ATT/Setup.lean:183
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 :

TreatedEstimationSystem P γ

conclusion

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

Proof (Lean source)

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

Causalean.Estimation.ATT.TreatedEstimationSystem.P_Z_eq · Causalean/Estimation/ATT/Setup.lean:198
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 :

TreatedEstimationSystem 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 : TreatedEstimationSystem P γ) : S.P_Z.map (fun z : γ × Bool × ℝ => z.1) = S.P_X := by unfold TreatedEstimationSystem.P_Z TreatedEstimationSystem.P_X rw [Measure.map_map (by fun_prop : Measurable (fun z : γ × Bool × ℝ => z.1)) S.measurable_factualZ] rfl

Causalean.Estimation.ATT.TreatedEstimationSystem.P_Z_map_projX_eq_P_X · Causalean/Estimation/ATT/Setup.lean:205

ATTInstance 2 core · 2 supporting Instantiates the abstract orthogonal-moment DML theorem for the average treatment effect on the treated. ★ att_oneStepOracleDML_isAsymLinear

Instantiates the abstract orthogonal-moment DML theorem for the average treatment effect on the treated. It connects the ATT AIPW score, remainder identity, score-continuity bounds, and sample-splitting assumptions to asymptotic linearity.

The main declarations are attGeneralMoment, the MeanZero bridge att_meanZero, the bilinear remainder bridge att_bilinearRem, and the headline abstract asymptotic-linearity theorem att_oneStepOracleDML_isAsymLinear. This file is the ATT specialization of the general orthogonal-moment interface; the user-facing estimator wrapper is in Estimation/ATT/DML.lean.

def attGeneralMoment reviewed

Causalean.Estimation.ATT

For a potential-outcomes system with a standard Borel sample space and finite probability measure, a measurable covariate space, a treated estimation system, a real overlap radius, the condition that the system's true nuisance vector belongs to its overlap-bounded candidate set at that radius, and the condition that its marginal treatment probability is strictly positive, the ATT augmented inverse-probability-weighted general moment is the general moment whose score is the ATT AIPW score, whose target nuisance vector and target parameter are the system's true nuisance vector and ATT, whose candidate set is that overlap-bounded set, whose two seminorms are the $L^2$ distances between control-outcome regressions and between propensity scores, and whose Jacobian is the negative marginal treatment probability.

Definition (Lean source)

parameters

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

ε :

ℝ

hη₀_mem :

S.η₀ ∈ H_ε S ε

hπ_pos :

0 < S.π_val

def

attGeneralMoment S hη₀_mem hπ_pos :

GeneralMoment P.Ω P.μ (γ × Bool × ℝ) S.P_Z (TreatedNuisanceVec γ)

given by

clause 1

m := fun η z θ => aipwMomentATTFunctional η z θ

clause 2

η₀ := S.η₀

clause 3

θ₀ := S.θ₀

clause 4

H_ε := H_ε S ε

clause 5

ρ₁ := fun η η'

=> ⟨(eLpNorm (fun x => η.μ₀_fn x - η'.μ₀_fn x) 2 S.P_X).toReal, ENNReal.toReal_nonneg⟩

clause 6

ρ₂ := fun η η'

=> ⟨(eLpNorm (fun x => η.e_fn x - η'.e_fn x) 2 S.P_X).toReal, ENNReal.toReal_nonneg⟩

clause 7

m_meas := fun η θ => TreatedEstimationSystem.measurable_aipwMomentATTFunctional η θ

clause 8

η₀_mem := hη₀_mem

clause 9

linScale := -S.π_val

clause 10

linScale_ne_zero := by intro h have : S.π_val

= 0 := by linarith [show -S.π_val = 0 from h] linarith

Causalean.Estimation.ATT.attGeneralMoment · Causalean/Estimation/ATT/ATTInstance.lean:77 · uses TreatedEstimationSystem , H_ε , P_Z , η₀ , π_val , TreatedNuisanceVec , instAddCommGroup , instModuleReal , GeneralMoment , POSystem

theorem att_oneStepOracleDML_isAsymLinear reviewed

Causalean.Estimation.ATT

Asymptotic linearity of the oracle one-step DML estimator of the average treatment effect on the treated (ATT). Fix a sequence of nuisance fits η̂_n, each a control-regression fit paired with a propensity fit, an i.i.d. sample of the covariate–treatment–outcome triple, and a one-shot split of that sample into a training fold and an evaluation fold. Under membership of the true nuisance in the overlap-bounded nuisance class, nonnegativity of the true propensity score, one-sided overlap with margin ε for the true propensity score, the one-sided back-door assumptions for the ATT, a strictly positive marginal treatment probability, square-integrability of the observed outcome and of the untreated potential outcome Y(0), integrability of the control-arm inverse-probability-weighting correction at the truth, and a positive limit c to which the evaluation-fold share of the sample converges: if every fit η̂_n lies in the overlap-bounded nuisance class, every fitted propensity is nonnegative, the control-regression and propensity errors of every fit are square-integrable under the covariate law, the inverse-probability-weighting correction at every fit is integrable under the observed-data law, the ATT score at the fitted nuisance and the true ATT is measurable jointly in the realization and the observation, and measurable with respect to the product of the σ-algebra generated by the training-fold observations and the observation σ-algebra, that score is integrable and square-integrable under the observed-data law at every fit, the two nuisance error gauges, which measure the L² errors of the fits under the covariate law, are each o_p(1), and their product is o_p(n^(−1/2)), then the oracle one-step estimator, the true ATT plus the evaluation-fold average of the ATT score at the fitted nuisance divided by the marginal treatment probability, is asymptotically linear at the true ATT along the evaluation fold, with influence function equal to the ATT augmented inverse-probability-weighted score at the true nuisance divided by the marginal treatment probability.

Formal statement

hypotheses

P :

POSystem

shared

γ :

Type u_1

shared

S :

TreatedEstimationSystem P γ

ε :

ℝ

hη₀_mem :

S.η₀ ∈ H_ε S ε

h_e_lb :

∀ x, 0 ≤ S.e_val x

h_overlap :

S.OneSidedOverlap ε

hA :

S.toPOBackdoorSystem.ATTAssumptions

hπ_pos :

0 < S.π_val

h_y2 :

Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ

h_y0_2 :

Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ

hIPW :

Integrable (fun ω => (1 - S.toPOBackdoorSystem.dVar.indicator true ω) * (S.toPOBackdoorSystem.propScore true ω / (1 - S.toPOBackdoorSystem.propScore true ω)) * (S.toPOBackdoorSystem.factualY ω - S.toPOBackdoorSystem.adjustedCE false ω)) P.μ

sample :

IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z

split :

OneShotSplit sample

c :

ℝ

hc_pos :

0 < c

h_split_rate :

Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)

η_hat :

ℕ → P.Ω → TreatedNuisanceVec γ

h_in_Hε :

∀ n ω, η_hat n ω ∈ H_ε S ε

h_e_lb_hat :

∀ n ω x, 0 ≤ (η_hat n ω).e_fn x

h_mu_diff_memLp :

∀ n ω, MemLp (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X

h_e_diff_memLp :

∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X

h_IPW_at :

∀ n ω,

Integrable (fun z => (1 - indA z) * ((η_hat n ω).e_fn (projX z) / (1 - (η_hat n ω).e_fn (projX z))) * (projY z - (η_hat n ω).μ₀_fn (projX z))) S.P_Z

h_m_meas :

∀ n,

Measurable (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀)

h_m_foldA_uncurry :

∀ n,

Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀)

h_m_int :

∀ n ω, Integrable (fun z => aipwMomentATTFunctional (η_hat n ω) z S.θ₀) S.P_Z

h_m_sq_int :

∀ n ω, Integrable (fun z => (aipwMomentATTFunctional (η_hat n ω) z S.θ₀) ^ 2) S.P_Z

h_indiv_rate_ρ₁ :

IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ

h_indiv_rate_ρ₂ :

IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ

h_product_rate :

IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * (((attGeneralMoment S hη₀_mem hπ_pos).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ

conclusion

IsAsymLinear (oneStepOracleDML (attGeneralMoment S hη₀_mem hπ_pos) sample split η_hat) S.θ₀ (fun z => -(attGeneralMoment S hη₀_mem hπ_pos).linScaleInv * aipwMomentATTFunctional S.η₀ z S.θ₀) sample split.foldB

Proof (Lean source)

theorem att_oneStepOracleDML_isAsymLinear (S : TreatedEstimationSystem P γ) {ε : ℝ} (hη₀_mem : S.η₀ ∈ H_ε S ε) (h_e_lb : ∀ x, 0 ≤ S.e_val x) (h_overlap : S.OneSidedOverlap ε) (hA : S.toPOBackdoorSystem.ATTAssumptions) (hπ_pos : 0 < S.π_val) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_y0_2 : Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ) (hIPW : Integrable (fun ω => (1 - S.toPOBackdoorSystem.dVar.indicator true ω) * (S.toPOBackdoorSystem.propScore true ω / (1 - S.toPOBackdoorSystem.propScore true ω)) * (S.toPOBackdoorSystem.factualY ω - S.toPOBackdoorSystem.adjustedCE false ω)) P.μ) (sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_hat : ℕ → P.Ω → TreatedNuisanceVec γ) (h_in_Hε : ∀ n ω, η_hat n ω ∈ H_ε S ε) (h_e_lb_hat : ∀ n ω x, 0 ≤ (η_hat n ω).e_fn x) (h_mu_diff_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X) (h_e_diff_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X) (h_IPW_at : ∀ n ω, Integrable (fun z => (1 - indA z) * ((η_hat n ω).e_fn (projX z) / (1 - (η_hat n ω).e_fn (projX z))) * (projY z - (η_hat n ω).μ₀_fn (projX z))) S.P_Z) (h_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentATTFunctional (η_hat n p.1) p.2 S.θ₀)) (h_m_int : ∀ n ω, Integrable (fun z => aipwMomentATTFunctional (η_hat n ω) z S.θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => (aipwMomentATTFunctional (η_hat n ω) z S.θ₀) ^ 2) S.P_Z) (h_indiv_rate_ρ₁ : IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ) (h_indiv_rate_ρ₂ : IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : IsLittleOp (fun n ω => (((attGeneralMoment S hη₀_mem hπ_pos).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * (((attGeneralMoment S hη₀_mem hπ_pos).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) : IsAsymLinear (oneStepOracleDML (attGeneralMoment S hη₀_mem hπ_pos) sample split η_hat) S.θ₀ (fun z => -(attGeneralMoment S hη₀_mem hπ_pos).linScaleInv * aipwMomentATTFunctional S.η₀ z S.θ₀) sample split.foldB := by have hMZ := att_meanZero S hη₀_mem hA hπ_pos hIPW have hFV : Integrable (fun z => ((attGeneralMoment S hη₀_mem hπ_pos).m (attGeneralMoment S hη₀_mem hπ_pos).η₀ z (attGeneralMoment S hη₀_mem hπ_pos).θ₀) ^ 2) S.P_Z := by simpa [attGeneralMoment, ψ_ATT, η₀, aipwMomentATTFunctional] using aipw_finite_var_ATT S h_overlap hA h_y2 h_y0_2 have hBR_at : ∀ n ω, |∫ z, (attGeneralMoment S hη₀_mem hπ_pos).m (η_hat n ω) z (attGeneralMoment S hη₀_mem hπ_pos).θ₀ ∂S.P_Z| ≤ aipw_rem_const_ATT ε * (((attGeneralMoment S hη₀_mem hπ_pos).ρ₁ (η_hat n ω) (attGeneralMoment S hη₀_mem hπ_pos).η₀ : NNReal) : ℝ) * (((attGeneralMoment S hη₀_mem hπ_pos).ρ₂ (η_hat n ω) (attGeneralMoment S hη₀_mem hπ_pos).η₀ : NNReal) : ℝ) := by intro n ω have h := aipw_remainder_bound_ATT S h_overlap hA hπ_pos h_y2 h_y0_2 (η_hat n ω) (h_in_Hε n ω) (h_mu_diff_memLp n ω) (h_e_diff_memLp n ω) (h_IPW_at n ω) change |∫ z, aipwMomentATTFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)| ≤ aipw_rem_const_ATT ε * (eLpNorm (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal exact h have h_mu_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ := by exact h_indiv_rate_ρ₁ have h_e_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ := by exact h_indiv_rate_ρ₂ have h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => (attGeneralMoment S hη₀_mem hπ_pos).m (η_hat n ω) z (attGeneralMoment S hη₀_mem hπ_pos).θ₀ - (attGeneralMoment S hη₀_mem hπ_pos).m (attGeneralMoment S hη₀_mem hπ_pos).η₀ z (attGeneralMoment S hη₀_mem hπ_pos).θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by simpa [attGeneralMoment] using aipw_score_diff_isLittleOp_one_ATT S h_overlap hη₀_mem h_e_lb hA h_y2 h_y0_2 η_hat h_in_Hε h_e_lb_hat h_mu_diff_memLp h_e_diff_memLp h_mu_rate h_e_rate simpa [attGeneralMoment] using (oneStepOracleDML_isAsymLinear_of_everywhere (attGeneralMoment S hη₀_mem hπ_pos) hMZ hFV sample split hc_pos h_split_rate η_hat (Crem := aipw_rem_const_ATT ε) hBR_at h_m_meas h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate)

Causalean.Estimation.ATT.att_oneStepOracleDML_isAsymLinear · Causalean/Estimation/ATT/ATTInstance.lean:173 · uses indA , projX , projY , TreatedEstimationSystem , H_ε , OneSidedOverlap , P_X , P_Z , aipwMomentATTFunctional , η₀ , θ₀ , π_val , TreatedNuisanceVec , instAddCommGroup , instModuleReal , attGeneralMoment , linScaleInv , oneStepOracleDML , ATTAssumptions , YofD , adjustedCE , dVar , factualY , propScore , POSystem , indicator , IIDSample , IsAsymLinear , IsLittleOp , OneShotSplit , foldA , foldB

2 supporting declarations (lemmas, instances)

att_meanZero theorem — ATT AIPW mean-zero packaging. Given membership of the true nuisance in the candidate set, the one-sided ATT assumptions, positive marginal treatment probability, and integrability of the inverse-probability-weighted control residual, the ATT AIPW general moment has mean zero. This is a direct repackaging of aipw_mean_zero_ATT from Estimation/ATT/Score/MeanZero.lean.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

TreatedEstimationSystem P γ

ε :

ℝ

hη₀_mem :

S.η₀ ∈ H_ε S ε

hA :

S.toPOBackdoorSystem.ATTAssumptions

hπ_pos :

0 < S.π_val

hIPW :

Integrable (fun ω => (1 - S.toPOBackdoorSystem.dVar.indicator true ω) * (S.toPOBackdoorSystem.propScore true ω / (1 - S.toPOBackdoorSystem.propScore true ω)) * (S.toPOBackdoorSystem.factualY ω - S.toPOBackdoorSystem.adjustedCE false ω)) P.μ

conclusion

MeanZero (attGeneralMoment S hη₀_mem hπ_pos)

Proof (Lean source)

theorem att_meanZero (S : TreatedEstimationSystem P γ) {ε : ℝ} (hη₀_mem : S.η₀ ∈ H_ε S ε) (hA : S.toPOBackdoorSystem.ATTAssumptions) (hπ_pos : 0 < S.π_val) (hIPW : Integrable (fun ω => (1 - S.toPOBackdoorSystem.dVar.indicator true ω) * (S.toPOBackdoorSystem.propScore true ω / (1 - S.toPOBackdoorSystem.propScore true ω)) * (S.toPOBackdoorSystem.factualY ω - S.toPOBackdoorSystem.adjustedCE false ω)) P.μ) : MeanZero (attGeneralMoment S hη₀_mem hπ_pos) := by unfold MeanZero attGeneralMoment exact aipw_mean_zero_ATT S hA hπ_pos hIPW

Causalean.Estimation.ATT.att_meanZero · Causalean/Estimation/ATT/ATTInstance.lean:114
att_bilinearRem theorem — ATT AIPW satisfies BilinearRemainder with constant aipw_rem_const_ATT ε.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

TreatedEstimationSystem P γ

ε :

ℝ

hη₀_mem :

S.η₀ ∈ H_ε S ε

h_overlap :

S.OneSidedOverlap ε

hA :

S.toPOBackdoorSystem.ATTAssumptions

hπ_pos :

0 < S.π_val

h_y2 :

Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ

h_y0_2 :

Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ

h_L2 :

∀ η ∈ H_ε S ε,
MemLp (fun x => η.μ₀_fn x - S.μ₀_val x) 2 S.P_X ∧
MemLp (fun x => η.e_fn x - S.e_val x) 2 S.P_X

h_IPW :

∀ η ∈ H_ε S ε,
Integrable (fun z => (1 - indA z) * (η.e_fn (projX z) / (1 - η.e_fn (projX z))) * (projY z - η.μ₀_fn (projX z))) S.P_Z

conclusion

∃ C, BilinearRemainder (attGeneralMoment S hη₀_mem hπ_pos) C

Proof (Lean source)

theorem att_bilinearRem (S : TreatedEstimationSystem P γ) {ε : ℝ} (hη₀_mem : S.η₀ ∈ H_ε S ε) (h_overlap : S.OneSidedOverlap ε) (hA : S.toPOBackdoorSystem.ATTAssumptions) (hπ_pos : 0 < S.π_val) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_y0_2 : Integrable (fun ω => (S.toPOBackdoorSystem.YofD false ω) ^ 2) P.μ) (h_L2 : ∀ η ∈ H_ε S ε, MemLp (fun x => η.μ₀_fn x - S.μ₀_val x) 2 S.P_X ∧ MemLp (fun x => η.e_fn x - S.e_val x) 2 S.P_X) (h_IPW : ∀ η ∈ H_ε S ε, Integrable (fun z => (1 - indA z) * (η.e_fn (projX z) / (1 - η.e_fn (projX z))) * (projY z - η.μ₀_fn (projX z))) S.P_Z) : ∃ C, BilinearRemainder (attGeneralMoment S hη₀_mem hπ_pos) C := by refine ⟨aipw_rem_const_ATT ε, ?_⟩ intro η hη obtain ⟨hΔμ₀, hΔe⟩ := h_L2 η hη have h := aipw_remainder_bound_ATT S h_overlap hA hπ_pos h_y2 h_y0_2 η hη hΔμ₀ hΔe (h_IPW η hη) change |∫ z, aipwMomentATTFunctional η z S.θ₀ ∂(S.P_Z)| ≤ aipw_rem_const_ATT ε * (eLpNorm (fun x => η.μ₀_fn x - S.μ₀_val x) 2 S.P_X).toReal * (eLpNorm (fun x => η.e_fn x - S.e_val x) 2 S.P_X).toReal exact h

Causalean.Estimation.ATT.att_bilinearRem · Causalean/Estimation/ATT/ATTInstance.lean:135