Estimation.ATE.Score

shared

γ :

Type u_1

shared

S :

z :

γ × Bool × ℝ

def

ψ_AIPW S z :

ℝ

given by

aipwMoment z S.μ_val S.e_val (S.θ₀)

Causalean.Estimation.ATE.BackdoorEstimationSystem.ψ_AIPW · Causalean/Estimation/ATE/Score/AIPWMoment.lean:100 · uses BackdoorEstimationSystem , POSystem

structure NuisanceVec reviewed

Causalean.Estimation.ATE

A pair of value-space AIPW nuisance functions, used as the abstract nuisance space for the AIPW moment functional: a treatment-arm-indexed outcome regression and a propensity score, together with their measurability.

Definition (Lean source)

parameters

γ :

Type*

MeasurableSpace γ

fields

μ_fn :

Bool → γ → ℝ

e_fn :

γ → ℝ

μ_meas :

∀ b, Measurable (μ_fn b)

e_meas :

Measurable e_fn

Causalean.Estimation.ATE.NuisanceVec · Causalean/Estimation/ATE/Score/AIPWMoment.lean:114

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 true nuisance vector consists of the system's treatment-specific outcome regressions and propensity score.

Definition (Lean source)

parameters

P :

shared

γ :

Type u_1

shared

S :

def

η₀ S :

NuisanceVec γ

given by

⟨S.μ_val, S.e_val, S.μ_meas, S.e_meas⟩

Causalean.Estimation.ATE.BackdoorEstimationSystem.η₀ · Causalean/Estimation/ATE/Score/AIPWMoment.lean:290 · uses BackdoorEstimationSystem , NuisanceVec , POSystem

def H_ε reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For a measurable covariate space and a real overlap level, the pointwise overlap-bounded nuisance class is the set of all nuisance vectors whose propensity score lies between $ε$ and $1-ε$ at every covariate value.

Definition (Lean source)

parameters

γ :

Type u_1

shared

ε :

ℝ

def

H_ε ε :

Set (NuisanceVec γ)

given by

{ η | ∀ x, ε ≤ η.e_fn x ∧ η.e_fn x ≤ 1 - ε }

Causalean.Estimation.ATE.BackdoorEstimationSystem.H_ε · Causalean/Estimation/ATE/Score/AIPWMoment.lean:294 · uses NuisanceVec

def H_ε_aeL2 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 almost-everywhere $L^2$ AIPW nuisance class is the set of nuisance vectors whose propensity score lies between $ε$ and $1-ε$ almost everywhere under the covariate law, whose two outcome regressions are square-integrable under that law, and whose propensity score is essentially bounded under that law.

Definition (Lean source)

parameters

P :

shared

γ :

Type u_1

shared

S :

ε :

ℝ

def

H_ε_aeL2 S ε :

Set (NuisanceVec γ)

given by

{ η | (∀ᵐ x ∂S.P_X, ε ≤ η.e_fn x ∧ η.e_fn x ≤ 1 - ε) ∧ (∀ d : Bool, MemLp (η.μ_fn d) 2 S.P_X) ∧ MemLp η.e_fn ⊤ S.P_X }

Causalean.Estimation.ATE.BackdoorEstimationSystem.H_ε_aeL2 · Causalean/Estimation/ATE/Score/AIPWMoment.lean:301 · uses BackdoorEstimationSystem , NuisanceVec , POSystem

lemma H_ε_aeL2_mu_memLp reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For an estimation system S, overlap level ε, and treatment arm d, if η is a member of the ε-overlap L² nuisance class H_ε_aeL2, then η's outcome-regression component at arm d lies in L²(P_X).

Formal statement

hypotheses

P :

shared

γ :

Type u_1

shared

S :

ε :

ℝ

η :

NuisanceVec γ

hη :

η ∈ H_ε_aeL2 S ε

d :

conclusion

MemLp (η.μ_fn d) 2 S.P_X

Proof (Lean source)

lemma H_ε_aeL2_mu_memLp (S : BackdoorEstimationSystem P γ) {ε : ℝ} {η : NuisanceVec γ} (hη : η ∈ H_ε_aeL2 S ε) (d : Bool) : MemLp (η.μ_fn d) 2 S.P_X := hη.2.1 d

Causalean.Estimation.ATE.BackdoorEstimationSystem.H_ε_aeL2_mu_memLp · Causalean/Estimation/ATE/Score/AIPWMoment.lean:342 · uses BackdoorEstimationSystem , H_ε_aeL2 , P_X , NuisanceVec , POSystem

def aipwMomentFunctional reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For a measurable covariate space, the AIPW moment functional maps a nuisance vector, an observed covariate--treatment--outcome triple, and a real target value to the corresponding AIPW moment.

Definition (Lean source)

parameters

γ :

Type u_1

shared

def

aipwMomentFunctional :

NuisanceVec γ → (γ × Bool × ℝ) → ℝ → ℝ

given by

fun η z θ => aipwMoment z η.μ_fn η.e_fn θ

Causalean.Estimation.ATE.BackdoorEstimationSystem.aipwMomentFunctional · Causalean/Estimation/ATE/Score/AIPWMoment.lean:358 · uses NuisanceVec

16 supporting declarations (lemmas, instances)

projX_apply lemma — The covariate projection of an observed data triple returns its covariate component.

hypotheses

γ :

Type u_1
shared

z :

γ × Bool × ℝ

conclusion

projX z = z.1

Proof (Lean source)

@[causal_defs_simps] lemma projX_apply (z : γ × Bool × ℝ) : projX z = z.1 := rfl

Causalean.Estimation.ATE.BackdoorEstimationSystem.projX_apply · Causalean/Estimation/ATE/Score/AIPWMoment.lean:58
projA_apply lemma — The treatment projection of an observed data triple returns its treatment component.

hypotheses

γ :

Type u_1
shared

z :

γ × Bool × ℝ

conclusion

projA z = z.2.1

Proof (Lean source)

@[causal_defs_simps] lemma projA_apply (z : γ × Bool × ℝ) : projA z = z.2.1 := rfl

Causalean.Estimation.ATE.BackdoorEstimationSystem.projA_apply · Causalean/Estimation/ATE/Score/AIPWMoment.lean:62
projY_apply lemma — The outcome projection of an observed data triple returns its outcome component.

hypotheses

γ :

Type u_1
shared

z :

γ × Bool × ℝ

conclusion

projY z = z.2.2

Proof (Lean source)

@[causal_defs_simps] lemma projY_apply (z : γ × Bool × ℝ) : projY z = z.2.2 := rfl

Causalean.Estimation.ATE.BackdoorEstimationSystem.projY_apply · Causalean/Estimation/ATE/Score/AIPWMoment.lean:66
aipwMoment_eq lemma — The augmented inverse-probability-weighting moment at a data point, a nuisance pair, and a parameter value is the contrast of the two outcome regressions at the covariate, plus the treated inverse-propensity-weighted outcome residual, minus the control inverse-propensity-weighted outcome residual, minus the parameter value.

hypotheses

γ :

Type u_1
shared

z :

γ × Bool × ℝ

μ_fn :

Bool → γ → ℝ

e_fn :

γ → ℝ

θ :

ℝ

conclusion

aipwMoment z μ_fn e_fn θ
= (μ_fn true (projX z) - μ_fn false (projX z))
+ (indA z / e_fn (projX z)) * (projY z - μ_fn true (projX z))
- ((1 - indA z) / (1 - e_fn (projX z))) * (projY z - μ_fn false (projX z))
- θ

Proof (Lean source)

@[causal_defs_simps] lemma aipwMoment_eq (z : γ × Bool × ℝ) (μ_fn : Bool → γ → ℝ) (e_fn : γ → ℝ) (θ : ℝ) : aipwMoment z μ_fn e_fn θ = (μ_fn true (projX z) - μ_fn false (projX z)) + (indA z / e_fn (projX z)) * (projY z - μ_fn true (projX z)) - ((1 - indA z) / (1 - e_fn (projX z))) * (projY z - μ_fn false (projX z)) - θ := rfl

Causalean.Estimation.ATE.BackdoorEstimationSystem.aipwMoment_eq · Causalean/Estimation/ATE/Score/AIPWMoment.lean:86
instZero instance — For a measurable covariate space, the zero operation on AIPW nuisance vectors sets both treatment-specific outcome regressions and the propensity score to zero.

parameters

γ :

Type u_1
shared

instance

instZero :
Zero (NuisanceVec γ)

given by

zero := ⟨fun _ _ => 0, fun _ => 0, fun _ => measurable_const, measurable_const⟩

Causalean.Estimation.ATE.NuisanceVec.instZero · Causalean/Estimation/ATE/Score/AIPWMoment.lean:129
instAdd instance — For a measurable covariate space, the addition operation on AIPW nuisance vectors is componentwise addition of the treatment-specific outcome regressions and propensity score.

parameters

γ :

Type u_1
shared

instance

instAdd :
Add (NuisanceVec γ)

given by

add η η' := ⟨fun b x
=> η.μ_fn b x
+ η'.μ_fn b x, fun x => η.e_fn x
+ η'.e_fn x, fun b => (η.μ_meas b).add (η'.μ_meas b), η.e_meas.add η'.e_meas⟩

Causalean.Estimation.ATE.NuisanceVec.instAdd · Causalean/Estimation/ATE/Score/AIPWMoment.lean:135
instNeg instance — For a measurable covariate space, the negation operation on AIPW nuisance vectors negates each treatment-specific outcome regression and the propensity score.

parameters

γ :

Type u_1
shared

instance

instNeg :
Neg (NuisanceVec γ)

given by

neg η := ⟨fun b x
=> -η.μ_fn b x, fun x => -η.e_fn x, fun b => (η.μ_meas b).neg, η.e_meas.neg⟩

Causalean.Estimation.ATE.NuisanceVec.instNeg · Causalean/Estimation/ATE/Score/AIPWMoment.lean:144
instSub instance — For a measurable covariate space, the subtraction operation on AIPW nuisance vectors is componentwise subtraction of the treatment-specific outcome regressions and propensity score.

parameters

γ :

Type u_1
shared

instance

instSub :
Sub (NuisanceVec γ)

given by

sub η η' := ⟨fun b x
=> η.μ_fn b x
- η'.μ_fn b x, fun x => η.e_fn x
- η'.e_fn x, fun b => (η.μ_meas b).sub (η'.μ_meas b), η.e_meas.sub η'.e_meas⟩

Causalean.Estimation.ATE.NuisanceVec.instSub · Causalean/Estimation/ATE/Score/AIPWMoment.lean:151
instSMulReal instance — For a measurable covariate space, the real scalar-multiplication operation on AIPW nuisance vectors scales each treatment-specific outcome regression and the propensity score.

parameters

γ :

Type u_1
shared

instance

instSMulReal :
SMul ℝ (NuisanceVec γ)

given by

smul t η := ⟨fun b x
=> t * η.μ_fn b x, fun x => t * η.e_fn x, fun b => measurable_const.mul (η.μ_meas b), measurable_const.mul η.e_meas⟩

Causalean.Estimation.ATE.NuisanceVec.instSMulReal · Causalean/Estimation/ATE/Score/AIPWMoment.lean:160
ext theorem — Two AIPW nuisance vectors are equal when their outcome regressions and propensity functions agree everywhere.

hypotheses

γ :

Type u_1
NuisanceVec γ
shared

hμ :

∀ b x, η.μ_fn b x = η'.μ_fn b x

he :

∀ x, η.e_fn x = η'.e_fn x

conclusion

η = η'

Proof (Lean source)

@[ext] theorem ext {η η' : NuisanceVec γ} (hμ : ∀ b x, η.μ_fn b x = η'.μ_fn b x) (he : ∀ x, η.e_fn x = η'.e_fn x) : η = η' := by cases η cases η' simp only at hμ he congr · funext b x exact hμ b x · funext x exact he x

Causalean.Estimation.ATE.NuisanceVec.ext · Causalean/Estimation/ATE/Score/AIPWMoment.lean:168
ext_iff theorem

∀ {γ : Type u_1} [inst : MeasurableSpace γ] {η η' : NuisanceVec γ}, η = η' ↔ (∀ (b : Bool) (x : γ), η.μ_fn b x = η'.μ_fn b x) ∧ ∀ (x : γ), η.e_fn x = η'.e_fn x

Proof (Lean source)

@[ext]

Causalean.Estimation.ATE.NuisanceVec.ext_iff · Causalean/Estimation/ATE/Score/AIPWMoment.lean:170
instAddCommGroup instance — For a measurable covariate space, the additive commutative group structure on AIPW nuisance vectors uses the zero vector, componentwise addition, componentwise negation, componentwise subtraction, natural-number scalar multiplication, and integer scalar multiplication, and satisfies the natural-zero rule, the natural-successor rule, the integer-zero rule, the positive-integer-successor rule, the negative-integer-successor rule, subtraction as addition of an inverse, associativity, the left-zero law, the right-zero law, inverse cancellation, and commutativity.

parameters

γ :

Type u_1
shared

instance

instAddCommGroup :
AddCommGroup (NuisanceVec γ)

given by

clause 1
zero := 0
clause 2
add := (· + ·)
clause 3
neg := neg
clause 4
sub := Sub.sub
clause 5
nsmul := nsmulRec
clause 6
zsmul := zsmulRec
clause 7
nsmul_zero η := by rfl
clause 8
nsmul_succ n η := by rfl
clause 9
zsmul_zero' η := by rfl
clause 10
zsmul_succ' n η := by rfl
clause 11
zsmul_neg' n η := by rfl
clause 12
sub_eq_add_neg η η' := by apply ext <;> intro b · intro x exact sub_eq_add_neg (η.μ_fn b x) (η'.μ_fn b x) · exact sub_eq_add_neg (η.e_fn b) (η'.e_fn b)
clause 13
add_assoc η η' η'' := by apply ext <;> intro b · intro x exact add_assoc (η.μ_fn b x) (η'.μ_fn b x) (η''.μ_fn b x) · exact add_assoc (η.e_fn b) (η'.e_fn b) (η''.e_fn b)
clause 14
zero_add η := by apply ext <;> intro b · intro x exact zero_add (η.μ_fn b x) · exact zero_add (η.e_fn b)
clause 15
add_zero η := by apply ext <;> intro b · intro x exact add_zero (η.μ_fn b x) · exact add_zero (η.e_fn b)
clause 16
neg_add_cancel η := by apply ext <;> intro b · intro x exact neg_add_cancel (η.μ_fn b x) · exact neg_add_cancel (η.e_fn b)
clause 17
add_comm η η' := by apply ext <;> intro b · intro x exact add_comm (η.μ_fn b x) (η'.μ_fn b x) · exact add_comm (η.e_fn b) (η'.e_fn b)

Causalean.Estimation.ATE.NuisanceVec.instAddCommGroup · Causalean/Estimation/ATE/Score/AIPWMoment.lean:183
instModuleReal instance — For a measurable covariate space, the real vector-space structure on AIPW nuisance vectors uses componentwise scalar multiplication and satisfies multiplication by one, compatibility of successive scalar multiplications, multiplication of zero vectors, distribution over vector addition, distribution over scalar addition, and multiplication by the zero scalar.

parameters

γ :

Type u_1
shared

instance

instModuleReal :
Module ℝ (NuisanceVec γ)

given by

clause 1
smul := (· • ·)
clause 2
one_smul η := by apply ext <;> intro b · intro x change (1 : ℝ) * η.μ_fn b x
= η.μ_fn b x exact one_mul _ · change (1 : ℝ) * η.e_fn b = η.e_fn b exact one_mul _
clause 3
mul_smul t u η := by apply ext <;> intro b · intro x change (t * u) * η.μ_fn b x
= t * (u * η.μ_fn b x) ring · change (t * u) * η.e_fn b = t * (u * η.e_fn b) ring
clause 4
smul_zero t := by apply ext <;> intro b · intro x change t * (0 : ℝ)
= 0 exact mul_zero t · change t * (0 : ℝ) = 0 exact mul_zero t
clause 5
smul_add t η η' := by apply ext <;> intro b · intro x change t * (η.μ_fn b x + η'.μ_fn b x)
= t * η.μ_fn b x
+ t * η'.μ_fn b x ring · change t * (η.e_fn b + η'.e_fn b) = t * η.e_fn b
+ t * η'.e_fn b ring
clause 6
add_smul t u η := by apply ext <;> intro b · intro x change (t + u) * η.μ_fn b x
= t * η.μ_fn b x
+ u * η.μ_fn b x ring · change (t + u) * η.e_fn b = t * η.e_fn b
+ u * η.e_fn b ring
clause 7
zero_smul η := by apply ext <;> intro b · intro x change (0 : ℝ) * η.μ_fn b x
= 0 exact zero_mul _ · change (0 : ℝ) * η.e_fn b = 0 exact zero_mul _

Causalean.Estimation.ATE.NuisanceVec.instModuleReal · Causalean/Estimation/ATE/Score/AIPWMoment.lean:235
H_ε_aeL2_overlap_factualX lemma — Membership in H_ε_aeL2 transports its a.e. overlap condition from the covariate law to the original probability space along the observed covariate.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

ε :

ℝ

η :

NuisanceVec γ

hη :

η ∈ H_ε_aeL2 S ε

conclusion

∀ᵐ ω ∂P.μ, ε
≤ η.e_fn (S.toPOBackdoorSystem.factualX ω) ∧
η.e_fn (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε

Proof (Lean source)

lemma H_ε_aeL2_overlap_factualX (S : BackdoorEstimationSystem P γ) {ε : ℝ} {η : NuisanceVec γ} (hη : η ∈ H_ε_aeL2 S ε) : ∀ᵐ ω ∂P.μ, ε ≤ η.e_fn (S.toPOBackdoorSystem.factualX ω) ∧ η.e_fn (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by have hset : MeasurableSet {x : γ | ε ≤ η.e_fn x ∧ η.e_fn x ≤ 1 - ε} := by exact measurableSet_Icc.preimage η.e_meas have hx : ∀ᵐ x ∂S.P_X, ε ≤ η.e_fn x ∧ η.e_fn x ≤ 1 - ε := hη.1 unfold BackdoorEstimationSystem.P_X at hx exact (MeasureTheory.ae_map_iff S.toPOBackdoorSystem.measurable_factualX.aemeasurable hset).mp hx

Causalean.Estimation.ATE.BackdoorEstimationSystem.H_ε_aeL2_overlap_factualX · Causalean/Estimation/ATE/Score/AIPWMoment.lean:312
H_ε_aeL2_overlap_P_Z lemma — Membership in H_ε_aeL2 transports its a.e. overlap condition from the covariate law to the observed-data law along the covariate projection.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

ε :

ℝ

η :

NuisanceVec γ

hη :

η ∈ H_ε_aeL2 S ε

conclusion

∀ᵐ z ∂S.P_Z, ε ≤ η.e_fn (projX z) ∧ η.e_fn (projX z) ≤ 1 - ε

Proof (Lean source)

lemma H_ε_aeL2_overlap_P_Z (S : BackdoorEstimationSystem P γ) {ε : ℝ} {η : NuisanceVec γ} (hη : η ∈ H_ε_aeL2 S ε) : ∀ᵐ z ∂S.P_Z, ε ≤ η.e_fn (projX z) ∧ η.e_fn (projX z) ≤ 1 - ε := by have hset : MeasurableSet {x : γ | ε ≤ η.e_fn x ∧ η.e_fn x ≤ 1 - ε} := by exact measurableSet_Icc.preimage η.e_meas have hx : ∀ᵐ x ∂S.P_X, ε ≤ η.e_fn x ∧ η.e_fn x ≤ 1 - ε := hη.1 rw [← BackdoorEstimationSystem.P_Z_map_projX_eq_P_X S] at hx have hproj : Measurable (fun z : γ × Bool × ℝ => projX z) := by simpa [projX] using (measurable_fst : Measurable (fun z : γ × Bool × ℝ => z.1)) exact (MeasureTheory.ae_map_iff hproj.aemeasurable hset).mp hx

Causalean.Estimation.ATE.BackdoorEstimationSystem.H_ε_aeL2_overlap_P_Z · Causalean/Estimation/ATE/Score/AIPWMoment.lean:327
H_ε_aeL2_e_memLp_top lemma — The propensity component of an H_ε_aeL2 nuisance is in L∞(P_X).

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

ε :

ℝ

η :

NuisanceVec γ

hη :

η ∈ H_ε_aeL2 S ε

conclusion

MemLp η.e_fn ⊤ S.P_X

Proof (Lean source)

lemma H_ε_aeL2_e_memLp_top (S : BackdoorEstimationSystem P γ) {ε : ℝ} {η : NuisanceVec γ} (hη : η ∈ H_ε_aeL2 S ε) : MemLp η.e_fn ⊤ S.P_X := hη.2.2

Causalean.Estimation.ATE.BackdoorEstimationSystem.H_ε_aeL2_e_memLp_top · Causalean/Estimation/ATE/Score/AIPWMoment.lean:351

AIPWScoreL2 3 core · 2 supporting Proves L² continuity of the AIPW score on the a.e. ★ aipw_score_diff_isLittleOp_one

Proves L² continuity of the AIPW score on the a.e. overlap-bounded nuisance space, supplying the empirical-process input used by double machine learning for the average treatment effect.

The file defines the overlap-dependent Lipschitz constant K_AIPW, proves the a.e. pointwise score bound aipw_score_diff_pointwise_bound, shows integrability of the residual-weighted cross term via yMuVal_residual_sq_integrable, and packages the final o_p(1) L²-score continuity theorem as aipw_score_diff_isLittleOp_one.

def K_AIPW reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

For a real number, the AIPW Lipschitz constant is $1+2/ε+2/ε^2$ .

Definition (Lean source)

parameters

ε :

ℝ

def

K_AIPW ε :

ℝ

given by

1 + 2 / ε + 2 / ε ^ 2

Causalean.Estimation.ATE.BackdoorEstimationSystem.K_AIPW · Causalean/Estimation/ATE/Score/AIPWScoreL2.lean:72

def YMuVal_residual_sq 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 squared residual-sum integrand maps each observed triple to the square of the sum of the absolute residuals from its two true outcome regressions.

Definition (Lean source)

parameters

P :

shared

γ :

Type u_1

shared

S :

def

YMuVal_residual_sq S :

(γ × Bool × ℝ) → ℝ

given by

fun z => (|projY z - S.μ_val true (projX z)| + |projY z - S.μ_val false (projX z)|) ^ 2

Causalean.Estimation.ATE.BackdoorEstimationSystem.YMuVal_residual_sq · Causalean/Estimation/ATE/Score/AIPWScoreL2.lean:351 · uses BackdoorEstimationSystem , POSystem

theorem aipw_score_diff_isLittleOp_one reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

Fix strict overlap at level ε, the back-door identification assumptions, and finite second moments of the observed and potential outcomes. For a sequence of nuisance estimators η̂ such that every realization lies in the ε-overlap L² nuisance class, with outcome-regression errors in L²(P_X) at every horizon and realization and propensity errors in L²(P_X) at every horizon and realization, if the outcome-regression error converges to zero in L²(P_X) in probability and the propensity error converges to zero in L²(P_X) in probability, then the L²(P_Z) norm of the AIPW score difference between the estimated and true nuisance converges to zero in probability.

Formal statement

hypotheses

P :

shared

γ :

Type u_1

shared

S :

ε :

ℝ

h_overlap :

S.StrictOverlap ε

hA :

S.toPOBackdoorSystem.Assumptions

h_y2 :

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

h_yd2 :

∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ

η_hat :

ℕ → P.Ω → NuisanceVec γ

h_in_H :

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

h_mu_memLp :

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

h_e_memLp :

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

h_mu_rate :

∀ a : Bool,

IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ

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

conclusion

IsLittleOp (fun n ω => (eLpNorm (fun z => aipwMomentFunctional (η_hat n ω) z S.θ₀ - aipwMomentFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ

Proof (Lean source)

theorem aipw_score_diff_isLittleOp_one (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (η_hat : ℕ → P.Ω → NuisanceVec γ) (h_in_H : ∀ n ω, η_hat n ω ∈ H_ε_aeL2 S ε) (h_mu_memLp : ∀ n ω a, MemLp (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X) (h_e_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X) (h_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (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.μ) : IsLittleOp (fun n ω => (eLpNorm (fun z => aipwMomentFunctional (η_hat n ω) z S.θ₀ - aipwMomentFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by exact aipw_score_diff_isLittleOp_one_truncation_core S h_overlap hA h_y2 h_yd2 η_hat h_in_H h_mu_memLp h_e_memLp h_mu_rate h_e_rate

Causalean.Estimation.ATE.BackdoorEstimationSystem.aipw_score_diff_isLittleOp_one · Causalean/Estimation/ATE/Score/AIPWScoreL2.lean:941 · uses BackdoorEstimationSystem , H_ε_aeL2 , P_X , P_Z , StrictOverlap , aipwMomentFunctional , η₀ , θ₀ , NuisanceVec , Assumptions , YofD , factualY , POSystem , IsLittleOp

2 supporting declarations (lemmas, instances)

aipw_score_diff_pointwise_bound theorem — AIPW score Lipschitz bound on H_ε, P_Z-a.e.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

ε :

ℝ

h_overlap :

S.StrictOverlap ε

η :

NuisanceVec γ

hη :

η ∈ H_ε_aeL2 S ε

conclusion

∀ᵐ z ∂S.P_Z, |aipwMomentFunctional η z S.θ₀ - aipwMomentFunctional S.η₀ z S.θ₀|
≤ K_AIPW ε * (|η.μ_fn true (projX z) - S.μ_val true (projX z)| + |η.μ_fn false (projX z) - S.μ_val false (projX z)| + (|projY z - S.μ_val true (projX z)| + |projY z - S.μ_val false (projX z)|) * |η.e_fn (projX z) - S.e_val (projX z)|)

Proof (Lean source)

theorem aipw_score_diff_pointwise_bound (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (η : NuisanceVec γ) (hη : η ∈ H_ε_aeL2 S ε) : ∀ᵐ z ∂S.P_Z, |aipwMomentFunctional η z S.θ₀ - aipwMomentFunctional S.η₀ z S.θ₀| ≤ K_AIPW ε * (|η.μ_fn true (projX z) - S.μ_val true (projX z)| + |η.μ_fn false (projX z) - S.μ_val false (projX z)| + (|projY z - S.μ_val true (projX z)| + |projY z - S.μ_val false (projX z)|) * |η.e_fn (projX z) - S.e_val (projX z)|) := by rcases h_overlap with ⟨hε_pos, _hε_half, hprop⟩ have h_e_ω : ∀ᵐ ω ∂P.μ, ε ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) ∧ S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by filter_upwards [hprop, S.e_compat] with ω hω hcompat rw [hcompat] at hω exact hω have h_e_z : ∀ᵐ z ∂S.P_Z, ε ≤ S.e_val (projX z) ∧ S.e_val (projX z) ≤ 1 - ε := by have hset : MeasurableSet {z : γ × Bool × ℝ | ε ≤ S.e_val (projX z) ∧ S.e_val (projX z) ≤ 1 - ε} := by have hx : Measurable (fun z : γ × Bool × ℝ => projX z) := by simpa [projX] using (measurable_fst : Measurable (fun z : γ × Bool × ℝ => z.1)) exact measurableSet_Icc.preimage (S.e_meas.comp hx) unfold BackdoorEstimationSystem.P_Z rw [MeasureTheory.ae_map_iff S.measurable_factualZ.aemeasurable hset] filter_upwards [h_e_ω] with ω hω simpa [BackdoorEstimationSystem.factualZ, projX] using hω have hη_z : ∀ᵐ z ∂S.P_Z, ε ≤ η.e_fn (projX z) ∧ η.e_fn (projX z) ≤ 1 - ε := H_ε_aeL2_overlap_P_Z S hη filter_upwards [h_e_z, hη_z] with z hz hηz simpa [aipwMomentFunctional, aipwMoment, η₀, indA] using (aipw_real_bound (a := projA z) (ε := ε) (e := S.e_val (projX z)) (ê := η.e_fn (projX z)) (μT := S.μ_val true (projX z)) (μF := S.μ_val false (projX z)) (μhT := η.μ_fn true (projX z)) (μhF := η.μ_fn false (projX z)) (y := projY z) (θ := S.θ₀) hε_pos hz hηz)

Causalean.Estimation.ATE.BackdoorEstimationSystem.aipw_score_diff_pointwise_bound · Causalean/Estimation/ATE/Score/AIPWScoreL2.lean:270
yMuVal_residual_sq_integrable theorem — The cross-term integrand is P_Z-integrable, with the bound coming from (a+b)² ≤ 2(a² + b²) and Y² ∈ L¹(P_Z), μ_val(d, X)² ∈ L¹(P_Z).

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

hA :

S.toPOBackdoorSystem.Assumptions

h_y2 :

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

h_yd2 :

∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ

conclusion

Integrable (S.YMuVal_residual_sq) S.P_Z

Proof (Lean source)

theorem yMuVal_residual_sq_integrable (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) : Integrable (S.YMuVal_residual_sq) S.P_Z := by have _ := hA have hY_L2 : MemLp S.toPOBackdoorSystem.factualY 2 P.μ := by exact (memLp_two_iff_integrable_sq S.toPOBackdoorSystem.measurable_factualY.aestronglyMeasurable).2 h_y2 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.μ := by exact (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) let g : γ × Bool × ℝ → ℝ := fun z => |projY z - S.μ_val true (projX z)| + |projY z - S.μ_val false (projX z)| have hg_meas : Measurable g := by have hx : Measurable (fun z : γ × Bool × ℝ => projX z) := by simpa [projX] using (measurable_fst : Measurable (fun z : γ × Bool × ℝ => z.1)) have hy : Measurable (fun z : γ × Bool × ℝ => projY z) := by simpa [projY] using (measurable_snd.snd : Measurable (fun z : γ × Bool × ℝ => z.2.2)) have hμt : Measurable (fun z : γ × Bool × ℝ => S.μ_val true (projX z)) := (S.μ_meas true).comp hx have hμf : Measurable (fun z : γ × Bool × ℝ => S.μ_val false (projX z)) := (S.μ_meas false).comp hx exact (continuous_abs.measurable.comp (hy.sub hμt)).add (continuous_abs.measurable.comp (hy.sub hμf)) have hg_comp_L2 : MemLp (fun ω => g (S.factualZ ω)) 2 P.μ := by have ht : MemLp (fun ω => S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := hY_L2.sub (hμ_L2 true) have hf : MemLp (fun ω => S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := hY_L2.sub (hμ_L2 false) exact ht.norm.add hf.norm have hg_L2 : MemLp g 2 S.P_Z := by rw [BackdoorEstimationSystem.P_Z] exact (memLp_map_measure_iff hg_meas.aestronglyMeasurable S.measurable_factualZ.aemeasurable).2 hg_comp_L2 exact hg_L2.integrable_sq

Causalean.Estimation.ATE.BackdoorEstimationSystem.yMuVal_residual_sq_integrable · Causalean/Estimation/ATE/Score/AIPWScoreL2.lean:376

FiniteVar 1 core · 1 supporting This file proves square integrability of the augmented inverse-probability weighted influence function for the back-door average treatment effect. ★ aipw_finite_var

Finite Variance for AIPW

This file proves square integrability of the augmented inverse-probability weighted influence function for the back-door average treatment effect. The result supplies the finite-variance condition needed by asymptotic linearity and efficiency arguments in the estimation layer.

The headline theorem aipw_finite_var assumes direct L² gates for μ_val(d, X), while aipw_finite_var_of_counterfactual_sq derives those gates from counterfactual second moments under the back-door assumptions.

theorem aipw_finite_var reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

Finite variance of ψ_AIPW — lem:est-aipw-finite-var. For an estimation system S, if the true propensity satisfies strict overlap at some level in (0, 1/2], the observed outcome has finite second moment, and each treatment arm's outcome regression, evaluated at the covariate, is square-integrable, then the AIPW influence function is square-integrable against the observed-data law P_Z.

Formal statement

hypotheses

P :

shared

γ :

Type u_1

shared

S :

ε :

ℝ

h_overlap :

S.StrictOverlap ε

h_y2 :

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

hμ_L2 :

∀ d : Bool, MemLp (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) 2 P.μ

conclusion

Integrable (fun z => (S.ψ_AIPW z) ^ 2) (S.P_Z)

Proof (Lean source)

theorem aipw_finite_var (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (hμ_L2 : ∀ d : Bool, MemLp (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) 2 P.μ) : Integrable (fun z => (S.ψ_AIPW z) ^ 2) (S.P_Z) := by have hψ_meas : Measurable S.ψ_AIPW := by unfold BackdoorEstimationSystem.ψ_AIPW aipwMoment indA projX projA projY have hx : Measurable (fun z : γ × Bool × ℝ => z.1) := measurable_fst have hy : Measurable (fun z : γ × Bool × ℝ => z.2.2) := by measurability have hμt : Measurable (fun z : γ × Bool × ℝ => S.μ_val true z.1) := (S.μ_meas true).comp hx have hμf : Measurable (fun z : γ × Bool × ℝ => S.μ_val false z.1) := (S.μ_meas false).comp hx have he : Measurable (fun z : γ × Bool × ℝ => S.e_val z.1) := S.e_meas.comp hx have hind : Measurable (fun z : γ × Bool × ℝ => if z.2.1 = true then (1 : ℝ) else 0) := by have ha : Measurable (fun z : γ × Bool × ℝ => z.2.1) := by measurability exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp ha exact ((((hμt.sub hμf).add ((hind.div he).mul (hy.sub hμt))).sub (((measurable_const.sub hind).div (measurable_const.sub he)).mul (hy.sub hμf))).sub measurable_const) have hY_L2 : MemLp S.toPOBackdoorSystem.factualY 2 P.μ := by exact (memLp_two_iff_integrable_sq S.toPOBackdoorSystem.measurable_factualY.aestronglyMeasurable).2 h_y2 have he_lower : ∀ᵐ ω ∂P.μ, ε ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) := by filter_upwards [h_overlap.2.2, S.e_compat] with ω hover hcomp simpa [hcomp] using hover.1 have he_upper : ∀ᵐ ω ∂P.μ, S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by filter_upwards [h_overlap.2.2, S.e_compat] with ω hover hcomp simpa [hcomp] using hover.2 have hw_true_bound : ∀ᵐ ω ∂P.μ, ‖indA (S.factualZ ω) / S.e_val (S.toPOBackdoorSystem.factualX ω)‖ ≤ ε⁻¹ := by filter_upwards [he_lower] with ω he by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hpos : 0 < S.e_val (S.toPOBackdoorSystem.factualX ω) := S.e_pos _ have hle : (S.e_val (S.toPOBackdoorSystem.factualX ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hpos h_overlap.1).2 he simpa [BackdoorEstimationSystem.factualZ, indA, projA, projX, hD, one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle · have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr h_overlap.1.le simpa [BackdoorEstimationSystem.factualZ, indA, projA, projX, hD] using hεinv_nonneg have hw_false_bound : ∀ᵐ ω ∂P.μ, ‖(1 - indA (S.factualZ ω)) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))‖ ≤ ε⁻¹ := by filter_upwards [he_upper] with ω he by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr h_overlap.1.le simpa [BackdoorEstimationSystem.factualZ, indA, projA, projX, hD] using hεinv_nonneg · have hden : ε ≤ 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) := by linarith have hdenpos : 0 < 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) := lt_of_lt_of_le h_overlap.1 hden have hle : (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hdenpos h_overlap.1).2 hden simpa [BackdoorEstimationSystem.factualZ, indA, projA, projX, hD, one_div, Real.norm_eq_abs, abs_of_pos hdenpos] using hle have hw_true_Linf : MemLp (fun ω => indA (S.factualZ ω) / S.e_val (S.toPOBackdoorSystem.factualX ω)) ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ hw_true_bound apply Measurable.aestronglyMeasurable have hind : Measurable (fun ω => indA (S.factualZ ω)) := by simp only [indA, projA, BackdoorEstimationSystem.factualZ] exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp S.toPOBackdoorSystem.measurable_factualD exact hind.div (S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX) have hw_false_Linf : MemLp (fun ω => (1 - indA (S.factualZ ω)) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ hw_false_bound apply Measurable.aestronglyMeasurable have hind : Measurable (fun ω => indA (S.factualZ ω)) := by simp only [indA, projA, BackdoorEstimationSystem.factualZ] exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp S.toPOBackdoorSystem.measurable_factualD exact (measurable_const.sub hind).div (measurable_const.sub (S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX)) have hterm_true_L2 : MemLp (fun ω => (indA (S.factualZ ω) / S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω))) 2 P.μ := by exact (hY_L2.sub (hμ_L2 true)).mul hw_true_Linf have hterm_false_L2 : MemLp (fun ω => ((1 - indA (S.factualZ ω)) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω))) 2 P.μ := by exact (hY_L2.sub (hμ_L2 false)).mul hw_false_Linf have hψ_comp_L2 : MemLp (fun ω => S.ψ_AIPW (S.factualZ ω)) 2 P.μ := by have hbase_L2 : MemLp (fun ω => S.μ_val true (S.toPOBackdoorSystem.factualX ω) - S.μ_val false (S.toPOBackdoorSystem.factualX ω)) 2 P.μ := (hμ_L2 true).sub (hμ_L2 false) have hconst_L2 : MemLp (fun _ : P.Ω => S.θ₀) 2 P.μ := memLp_const _ have hsum_L2 := ((hbase_L2.add hterm_true_L2).sub hterm_false_L2).sub hconst_L2 exact hsum_L2 have hψ_L2 : MemLp S.ψ_AIPW 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

Causalean.Estimation.ATE.BackdoorEstimationSystem.aipw_finite_var · Causalean/Estimation/ATE/Score/FiniteVar.lean:39 · uses BackdoorEstimationSystem , P_Z , StrictOverlap , ψ_AIPW , factualX , factualY , POSystem

1 supporting declaration (lemmas, instances)

aipw_finite_var_of_counterfactual_sq theorem — Counterfactual second moments are a stronger sufficient condition for aipw_finite_var.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

ε :

ℝ

h_overlap :

S.StrictOverlap ε

hA :

S.toPOBackdoorSystem.Assumptions

h_y2 :

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

h_yd2 :

∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ

conclusion

Integrable (fun z => (S.ψ_AIPW z) ^ 2) (S.P_Z)

Proof (Lean source)

theorem aipw_finite_var_of_counterfactual_sq (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) : Integrable (fun z => (S.ψ_AIPW z) ^ 2) (S.P_Z) := by 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.μ := by exact (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) exact S.aipw_finite_var h_overlap h_y2 hμ_L2

Causalean.Estimation.ATE.BackdoorEstimationSystem.aipw_finite_var_of_counterfactual_sq · Causalean/Estimation/ATE/Score/FiniteVar.lean:174

MeanZero 1 core · 5 supporting Proves measurability and mean-zero properties of the AIPW influence function for back-door average treatment effect estimation. ★ aipw_mean_zero

Proves measurability and mean-zero properties of the AIPW influence function for back-door average treatment effect estimation.

The file establishes measurable_ψ_AIPW, residual and propensity-score pull-out lemmas used by the proof, the source-level mean-zero theorem aipw_mean_zero, and the square-integrability corollary aipw_mean_zero_of_square_integrable that derives the weighted residual integrability gates from strict overlap and second moments.

theorem aipw_mean_zero reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

Mean zero of the AIPW influence function. Under the back-door identification assumptions, if the inverse-propensity-weighted residual correction on the treated arm, 1{D=1}/e(X) · (Y − μ(1,X)), is integrable and the analogous correction on the control arm, 1{D=0}/(1 − e(X)) · (Y − μ(0,X)), is integrable, then the AIPW influence function ψ_AIPW has mean zero under the joint law of the covariates, treatment indicator, and outcome.

Formal statement

hypotheses

P :

shared

γ :

Type u_1

shared

S :

hA :

S.toPOBackdoorSystem.Assumptions

hB_int :

Integrable (fun ω => (1 / S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.dVar.indicator true ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)))) P.μ

hC_int :

Integrable (fun ω => (1 / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)))) P.μ

conclusion

(∫ z, S.ψ_AIPW z ∂(S.P_Z)) = 0

Proof (Lean source)

theorem aipw_mean_zero (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (hB_int : Integrable (fun ω => (1 / S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.dVar.indicator true ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)))) P.μ) (hC_int : Integrable (fun ω => (1 / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)))) P.μ) : (∫ z, S.ψ_AIPW z ∂(S.P_Z)) = 0 := by rw [BackdoorEstimationSystem.P_Z] rw [MeasureTheory.integral_map S.measurable_factualZ.aemeasurable (measurable_ψ_AIPW S).aestronglyMeasurable] exact aipw_factualZ_integral_zero S hA hB_int hC_int

Causalean.Estimation.ATE.BackdoorEstimationSystem.aipw_mean_zero · Causalean/Estimation/ATE/Score/MeanZero.lean:615 · uses BackdoorEstimationSystem , P_Z , ψ_AIPW , Assumptions , dVar , factualX , factualY , POSystem , indicator

5 supporting declarations (lemmas, instances)

measurable_ψ_AIPW lemma — The AIPW influence function is measurable as a function of the observed data triple.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

conclusion

Measurable S.ψ_AIPW

Proof (Lean source)

@[fun_prop] lemma measurable_ψ_AIPW (S : BackdoorEstimationSystem P γ) : Measurable S.ψ_AIPW := by unfold BackdoorEstimationSystem.ψ_AIPW aipwMoment indA projX projA projY have hx : Measurable (fun z : γ × Bool × ℝ => z.1) := measurable_fst have hy : Measurable (fun z : γ × Bool × ℝ => z.2.2) := by measurability have hμt : Measurable (fun z : γ × Bool × ℝ => S.μ_val true z.1) := (S.μ_meas true).comp hx have hμf : Measurable (fun z : γ × Bool × ℝ => S.μ_val false z.1) := (S.μ_meas false).comp hx have he : Measurable (fun z : γ × Bool × ℝ => S.e_val z.1) := S.e_meas.comp hx have hind : Measurable (fun z : γ × Bool × ℝ => if z.2.1 = true then (1 : ℝ) else 0) := by have ha : Measurable (fun z : γ × Bool × ℝ => z.2.1) := by measurability exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp ha exact ((((hμt.sub hμf).add ((hind.div he).mul (hy.sub hμt))).sub (((measurable_const.sub hind).div (measurable_const.sub he)).mul (hy.sub hμf))).sub measurable_const)

Causalean.Estimation.ATE.BackdoorEstimationSystem.measurable_ψ_AIPW · Causalean/Estimation/ATE/Score/MeanZero.lean:48
propScore_ne_zero lemma — The conditional treatment probability for either treatment label is nonzero almost surely under the back-door assumptions.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

hA :

S.toPOBackdoorSystem.Assumptions

d :

Bool

conclusion

∀ᵐ ω ∂P.μ, S.toPOBackdoorSystem.propScore d ω ≠ 0

Proof (Lean source)

lemma propScore_ne_zero (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (d : Bool) : ∀ᵐ ω ∂P.μ, S.toPOBackdoorSystem.propScore d ω ≠ 0 := by cases d · have hindD_integrable : ∀ e : Bool, Integrable (S.toPOBackdoorSystem.dVar.indicator e) P.μ := fun e => S.toPOBackdoorSystem.dVar.integrable_indicator e (MeasurableSet.singleton e) have hsum_ptwise : (fun ω => S.toPOBackdoorSystem.dVar.indicator true ω + S.toPOBackdoorSystem.dVar.indicator false ω) = (fun _ : P.Ω => (1 : ℝ)) := by funext ω exact S.toPOBackdoorSystem.dVar.indicator_add_indicator_not ω have hsum : P.μ[fun ω => S.toPOBackdoorSystem.dVar.indicator true ω + S.toPOBackdoorSystem.dVar.indicator false ω | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (1 : ℝ)) := by rw [hsum_ptwise] exact Filter.EventuallyEq.of_eq (MeasureTheory.condExp_const S.toPOBackdoorSystem.sigmaX_le (1 : ℝ)) have hadd : P.μ[fun ω => S.toPOBackdoorSystem.dVar.indicator true ω + S.toPOBackdoorSystem.dVar.indicator false ω | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] P.μ[S.toPOBackdoorSystem.dVar.indicator true | S.toPOBackdoorSystem.sigmaX] + P.μ[S.toPOBackdoorSystem.dVar.indicator false | S.toPOBackdoorSystem.sigmaX] := MeasureTheory.condExp_add (hindD_integrable true) (hindD_integrable false) S.toPOBackdoorSystem.sigmaX filter_upwards [hsum, hadd, hA.overlap] with ω h1 h2 hT have heq : S.toPOBackdoorSystem.propScore true ω + S.toPOBackdoorSystem.propScore false ω = 1 := by have : P.μ[S.toPOBackdoorSystem.dVar.indicator true | S.toPOBackdoorSystem.sigmaX] ω + P.μ[S.toPOBackdoorSystem.dVar.indicator false | S.toPOBackdoorSystem.sigmaX] ω = 1 := by rw [← Pi.add_apply, ← h2, h1] unfold POBackdoorSystem.propScore exact this have hps_false : S.toPOBackdoorSystem.propScore false ω = 1 - S.toPOBackdoorSystem.propScore true ω := by linarith rw [hps_false] linarith [hT.2] · filter_upwards [hA.overlap] with ω hω exact ne_of_gt hω.1

Causalean.Estimation.ATE.BackdoorEstimationSystem.propScore_ne_zero · Causalean/Estimation/ATE/Score/MeanZero.lean:72
cond_exp_residual_zero lemma — Conditional expectation of the residual ind_d · (Y − μ_val d X) given σ(X) is zero a.s. — the σ(X)-cleared form of lem:est-aipw-mean-zero.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

hA :

S.toPOBackdoorSystem.Assumptions

d :

Bool

conclusion

P.μ[fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω)) | S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ] (fun _ => (0 : ℝ))

Proof (Lean source)

lemma cond_exp_residual_zero (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (d : Bool) : P.μ[fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω)) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by have hYind_int : Integrable (fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ := S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (measurableSet_singleton d) hA.integrable_factualY have hμx_int : Integrable (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) P.μ := by have hcate_int : Integrable (S.toPOBackdoorSystem.CATE d) P.μ := by unfold POBackdoorSystem.CATE exact MeasureTheory.integrable_condExp exact hcate_int.congr (S.μ_compat hA d) have hμx_meas : Measurable (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) := (S.μ_meas d).comp S.toPOBackdoorSystem.measurable_factualX have hμind_int : Integrable (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ := S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (measurableSet_singleton d) hμx_int have hres_eq : (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω))) = (fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator d ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω) := by funext ω ring have hsub : P.μ[fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator d ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] P.μ[fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] - P.μ[fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] := MeasureTheory.condExp_sub hYind_int hμind_int S.toPOBackdoorSystem.sigmaX have hYce : P.μ[fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] S.toPOBackdoorSystem.propScore d * S.toPOBackdoorSystem.CATE d := by have hcate := S.toPOBackdoorSystem.cate_backdoor hA d filter_upwards [hcate, propScore_ne_zero S hA d] with ω hcat hneω unfold POBackdoorSystem.adjustedCE at hcat rw [Pi.mul_apply, hcat] field_simp [hneω] have hμx_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) exact ((S.μ_meas d).comp (comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable have hind_int : Integrable (S.toPOBackdoorSystem.dVar.indicator d) P.μ := S.toPOBackdoorSystem.dVar.integrable_indicator d (MeasurableSet.singleton d) have hμce : P.μ[fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) * S.toPOBackdoorSystem.propScore d := by have hpull := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := P.μ) (m := S.toPOBackdoorSystem.sigmaX) hμx_sm hμind_int hind_int exact hpull rw [hres_eq] refine hsub.trans ?_ filter_upwards [hYce, hμce, S.μ_compat hA d] with ω hy hmu hcompat have hcate_comp : S.toPOBackdoorSystem.CATE d ω = S.μ_val d (S.toPOBackdoorSystem.factualX ω) := by simpa [POBackdoorSystem.CATE] using hcompat rw [Pi.sub_apply, hy, hmu, Pi.mul_apply, Pi.mul_apply, hcate_comp] ring

Causalean.Estimation.ATE.BackdoorEstimationSystem.cond_exp_residual_zero · Causalean/Estimation/ATE/Score/MeanZero.lean:125
theta_zero_factualX_integral lemma — The estimand θ₀ = ∫ x, (μ_val(1,x) − μ_val(0,x)) ∂P_X lifts back to the ambient measure via factualX.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

conclusion

S.θ₀
= ∫ ω, S.μ_val true (S.toPOBackdoorSystem.factualX ω)
- S.μ_val false (S.toPOBackdoorSystem.factualX ω) ∂P.μ

Proof (Lean source)

lemma theta_zero_factualX_integral (S : BackdoorEstimationSystem P γ) : S.θ₀ = ∫ ω, S.μ_val true (S.toPOBackdoorSystem.factualX ω) - S.μ_val false (S.toPOBackdoorSystem.factualX ω) ∂P.μ := by unfold BackdoorEstimationSystem.θ₀ BackdoorEstimationSystem.P_X 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]

Causalean.Estimation.ATE.BackdoorEstimationSystem.theta_zero_factualX_integral · Causalean/Estimation/ATE/Score/MeanZero.lean:261
aipw_mean_zero_of_square_integrable theorem — A stronger sufficient-condition corollary for aipw_mean_zero.

hypotheses

P :

POSystem
shared

γ :

Type u_1
shared

S :

BackdoorEstimationSystem P γ

ε :

ℝ

h_overlap :

S.StrictOverlap ε

hA :

S.toPOBackdoorSystem.Assumptions

h_y2 :

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

h_yd2 :

∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ

conclusion

(∫ z, S.ψ_AIPW z ∂(S.P_Z)) = 0

Proof (Lean source)

theorem aipw_mean_zero_of_square_integrable (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) : (∫ z, S.ψ_AIPW z ∂(S.P_Z)) = 0 := by have hindA_true : ∀ ω, indA (S.factualZ ω) = S.toPOBackdoorSystem.dVar.indicator true ω := by intro ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [BackdoorEstimationSystem.factualZ, indA, projA, hD, hInd] · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [BackdoorEstimationSystem.factualZ, indA, projA, hD, hInd] have hindA_false : ∀ ω, 1 - indA (S.factualZ ω) = S.toPOBackdoorSystem.dVar.indicator false ω := by intro ω have hsum : S.toPOBackdoorSystem.dVar.indicator true ω + S.toPOBackdoorSystem.dVar.indicator false ω = 1 := S.toPOBackdoorSystem.dVar.indicator_add_indicator_not ω calc 1 - indA (S.factualZ ω) = 1 - S.toPOBackdoorSystem.dVar.indicator true ω := by rw [hindA_true ω] _ = S.toPOBackdoorSystem.dVar.indicator false ω := by linarith have hY_L2 : MemLp S.toPOBackdoorSystem.factualY 2 P.μ := (memLp_two_iff_integrable_sq S.toPOBackdoorSystem.measurable_factualY.aestronglyMeasurable).2 h_y2 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 he_lower : ∀ᵐ ω ∂P.μ, ε ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) := by filter_upwards [h_overlap.2.2, S.e_compat] with ω hprop hcomp simpa [hcomp] using hprop.1 have he_upper : ∀ᵐ ω ∂P.μ, S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by filter_upwards [h_overlap.2.2, S.e_compat] with ω hprop hcomp simpa [hcomp] using hprop.2 have hw_true_bound : ∀ᵐ ω ∂P.μ, ‖indA (S.factualZ ω) / S.e_val (S.toPOBackdoorSystem.factualX ω)‖ ≤ ε⁻¹ := by filter_upwards [he_lower] with ω he by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hpos : 0 < S.e_val (S.toPOBackdoorSystem.factualX ω) := S.e_pos _ have hle : (S.e_val (S.toPOBackdoorSystem.factualX ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hpos h_overlap.1).2 he simpa [BackdoorEstimationSystem.factualZ, indA, projA, hD, one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle · have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr h_overlap.1.le simpa [BackdoorEstimationSystem.factualZ, indA, projA, hD] using hεinv_nonneg have hw_false_bound : ∀ᵐ ω ∂P.μ, ‖(1 - indA (S.factualZ ω)) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))‖ ≤ ε⁻¹ := by filter_upwards [he_upper] with ω he by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr h_overlap.1.le simpa [BackdoorEstimationSystem.factualZ, indA, projA, hD] using hεinv_nonneg · have hden : ε ≤ 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) := by linarith have hdenpos : 0 < 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) := lt_of_lt_of_le h_overlap.1 hden have hle : (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hdenpos h_overlap.1).2 hden simpa [BackdoorEstimationSystem.factualZ, indA, projA, hD, one_div, Real.norm_eq_abs, abs_of_pos hdenpos] using hle have hw_true_Linf : MemLp (fun ω => indA (S.factualZ ω) / S.e_val (S.toPOBackdoorSystem.factualX ω)) ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ hw_true_bound apply Measurable.aestronglyMeasurable have hind : Measurable (fun ω => indA (S.factualZ ω)) := by simp only [indA, projA, BackdoorEstimationSystem.factualZ] exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp S.toPOBackdoorSystem.measurable_factualD exact hind.div (S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX) have hw_false_Linf : MemLp (fun ω => (1 - indA (S.factualZ ω)) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ hw_false_bound apply Measurable.aestronglyMeasurable have hind : Measurable (fun ω => indA (S.factualZ ω)) := by simp only [indA, projA, BackdoorEstimationSystem.factualZ] exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp S.toPOBackdoorSystem.measurable_factualD exact (measurable_const.sub hind).div (measurable_const.sub (S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX)) have hB_L2 : MemLp (fun ω => indA (S.factualZ ω) / S.e_val (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω))) 2 P.μ := by exact (hY_L2.sub (hμ_L2 true)).mul hw_true_Linf have hC_L2 : MemLp (fun ω => (1 - indA (S.factualZ ω)) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω))) 2 P.μ := by exact (hY_L2.sub (hμ_L2 false)).mul hw_false_Linf have hB_eq : (fun ω => (1 / S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.dVar.indicator true ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)))) =ᵐ[P.μ] (fun ω => indA (S.factualZ ω) / S.e_val (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω))) := by refine Filter.Eventually.of_forall ?_ intro ω calc (1 / S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.dVar.indicator true ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω))) = (S.toPOBackdoorSystem.dVar.indicator true ω / S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)) := by ring _ = indA (S.factualZ ω) / S.e_val (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)) := by rw [hindA_true ω] have hC_eq : (fun ω => (1 / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)))) =ᵐ[P.μ] (fun ω => (1 - indA (S.factualZ ω)) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω))) := by refine Filter.Eventually.of_forall ?_ intro ω calc (1 / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω))) = (S.toPOBackdoorSystem.dVar.indicator false ω / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)) := by ring _ = (1 - indA (S.factualZ ω)) / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)) := by rw [hindA_false ω] exact aipw_mean_zero S hA ((hB_L2.integrable (by norm_num)).congr hB_eq.symm) ((hC_L2.integrable (by norm_num)).congr hC_eq.symm)

Causalean.Estimation.ATE.BackdoorEstimationSystem.aipw_mean_zero_of_square_integrable · Causalean/Estimation/ATE/Score/MeanZero.lean:643

ScorePullout 3 core · 3 supporting This file provides conditional-expectation and integral identities that remove score factors and treatment indicators from augmented inverse-probability weighted residual terms. ★ weighted_residual_integral_zero★ indicator_to_propScore_integral

AIPW Score Pull-Out Lemmas

This file provides conditional-expectation and integral identities that remove score factors and treatment indicators from augmented inverse-probability weighted residual terms. These lemmas are shared by the mean-zero proof and the second-order remainder expansion for the back-door average treatment effect.

The main declarations define the label-specific value-space propensity e_val_label, prove propScore_eq_e_val_label_ae, and provide the integral helpers weighted_residual_integral_zero and indicator_to_propScore_integral.

def e_val_label 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, a treatment label, and a covariate value, the label-specific value-space propensity equals the propensity score for the treated label and one minus that score for the control label.

Definition (Lean source)

parameters

P :

shared

γ :

Type u_1

shared

S :

d :

x :

γ

def

e_val_label S d x :

ℝ

given by

if d then S.e_val x else 1 - S.e_val x

Causalean.Estimation.ATE.BackdoorEstimationSystem.e_val_label · Causalean/Estimation/ATE/Score/ScorePullout.lean:40 · uses BackdoorEstimationSystem , POSystem

lemma weighted_residual_integral_zero reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

Weighted-residual mean-zero identity (pull-out lemma). Fix a treatment label $d$ and a measurable weight function g : γ → ℝ on the covariates, under the back-door identification assumptions. If the product g(X) · 1{D=d} · (Y − μ(d,X)) is integrable and the σ(X)-conditional expectation of the treatment-d residual 1{D=d} · (Y − μ(d,X)) vanishes almost surely, then the integral of the weighted residual against the observed-data law vanishes: ∫ g(X) · 1{D=d} · (Y − μ(d,X)) dμ = 0.

Formal statement

hypotheses

P :

shared

γ :

Type u_1

shared

S :

hA :

S.toPOBackdoorSystem.Assumptions

d :

g :

γ → ℝ

hg_meas :

Measurable g

h_int :

Integrable (fun ω => g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω)))) P.μ

h_residual_ce_zero :

P.μ[fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω)) | S.toPOBackdoorSystem.sigmaX]

=ᵐ[P.μ] (fun _ => (0 : ℝ))

conclusion

∫ ω, g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω))) ∂P.μ

= 0

Proof (Lean source)

lemma weighted_residual_integral_zero (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (d : Bool) (g : γ → ℝ) (hg_meas : Measurable g) (h_int : Integrable (fun ω => g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω)))) P.μ) (h_residual_ce_zero : P.μ[fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω)) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ))) : ∫ ω, g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω))) ∂P.μ = 0 := by have hg_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] (fun ω => g (S.toPOBackdoorSystem.factualX ω)) := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => g (S.toPOBackdoorSystem.factualX ω)) exact (hg_meas.comp (comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable have hYind_int : Integrable (fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ := S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (measurableSet_singleton d) hA.integrable_factualY have hμx_int : Integrable (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) P.μ := by have hcate_int : Integrable (S.toPOBackdoorSystem.CATE d) P.μ := by unfold POBackdoorSystem.CATE exact MeasureTheory.integrable_condExp exact hcate_int.congr (S.μ_compat hA d) have hμx_meas : Measurable (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) := (S.μ_meas d).comp S.toPOBackdoorSystem.measurable_factualX have hμind_int : Integrable (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ := S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (measurableSet_singleton d) hμx_int have hresid_int : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω))) P.μ := by have hYind_int' : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * S.toPOBackdoorSystem.factualY ω) P.μ := by simpa [mul_comm] using hYind_int have hμind_int' : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * S.μ_val d (S.toPOBackdoorSystem.factualX ω)) P.μ := by simpa [mul_comm] using hμind_int have hsub := hYind_int'.sub hμind_int' refine hsub.congr ?_ refine Filter.Eventually.of_forall (fun ω => ?_) change S.toPOBackdoorSystem.dVar.indicator d ω * S.toPOBackdoorSystem.factualY ω - S.toPOBackdoorSystem.dVar.indicator d ω * S.μ_val d (S.toPOBackdoorSystem.factualX ω) = S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω)) ring have hcondexp_pull := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := P.μ) (m := S.toPOBackdoorSystem.sigmaX) hg_sm h_int hresid_int have hgresid_ce_zero : P.μ[fun ω => g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω))) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by refine hcondexp_pull.trans ?_ filter_upwards [h_residual_ce_zero] with ω hω have : ((fun ω' => g (S.toPOBackdoorSystem.factualX ω')) * P.μ[fun ω' => S.toPOBackdoorSystem.dVar.indicator d ω' * (S.toPOBackdoorSystem.factualY ω' - S.μ_val d (S.toPOBackdoorSystem.factualX ω')) | S.toPOBackdoorSystem.sigmaX]) ω = 0 := by rw [Pi.mul_apply, hω, mul_zero] exact this calc ∫ ω, g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω))) ∂P.μ = ∫ ω, P.μ[fun ω => g (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator d ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val d (S.toPOBackdoorSystem.factualX ω))) | S.toPOBackdoorSystem.sigmaX] ω ∂P.μ := by rw [MeasureTheory.integral_condExp S.toPOBackdoorSystem.sigmaX_le] _ = ∫ _, (0 : ℝ) ∂P.μ := MeasureTheory.integral_congr_ae hgresid_ce_zero _ = 0 := MeasureTheory.integral_zero _ _

Causalean.Estimation.ATE.BackdoorEstimationSystem.weighted_residual_integral_zero · Causalean/Estimation/ATE/Score/ScorePullout.lean:114 · uses BackdoorEstimationSystem , Assumptions , dVar , factualX , factualY , sigmaX , POSystem , indicator

lemma indicator_to_propScore_integral reviewed

Causalean.Estimation.ATE.BackdoorEstimationSystem

Propensity-score pull-out for the treatment indicator. Fix a treatment label $d$ , under the back-door identification assumptions. If f : γ → ℝ is measurable and the product f(X) · 1{D=d} is integrable, then replacing the treatment indicator 1{D=d} by the value-space propensity e_val_label d inside the integral leaves the integral unchanged: ∫ f(X) · 1{D=d} dμ = ∫ f(X) · e_val_label d(X) dμ.

Formal statement

hypotheses

P :

shared

γ :

Type u_1

shared

S :

hA :

S.toPOBackdoorSystem.Assumptions

d :