Estimation.ATE.Score
AIPW score infrastructure for ATE DML: moment definitions, influence functions, finite variance, mean-zero identities, L2 continuity, and pull-out lemmas.
AIPWMoment 12 core · 12 supporting Defines the AIPW score objects used throughout the back-door ATE estimation theory. ★ H_ε_aeL2_mu_memLp
Defines the AIPW score objects used throughout the back-door ATE estimation theory.
The main declarations are the observed-data projections projX, projA,
projY, the treatment indicator indA, the AIPW moment aipwMoment, the
truth influence function ψ_AIPW, and the nuisance vector space
NuisanceVec. The file also defines the truth nuisance η₀, the legacy
pointwise overlap class H_ε, the source-shaped a.e./L² nuisance class
H_ε_aeL2, transport lemmas for its a.e. overlap condition, and
aipwMomentFunctional for use in orthogonality and DML theorems.
def projX reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Projection (x, a, y) ↦ x.
Definition (Lean source)
def projX : γ × Bool × ℝ → γ := fun z => z.1
def projA reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Projection (x, a, y) ↦ a.
def projY reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Projection (x, a, y) ↦ y.
Definition (Lean source)
def projY : γ × Bool × ℝ → ℝ := fun z => z.2.2
def indA reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Real-valued indicator of {a = true} viewed as a function of the data.
def aipwMoment reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
The AIPW moment m_AIPW(η, z, θ) from def:est-aipw-moment:
Definition (Lean source)
def ψ_AIPW reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
The AIPW influence function at the truth: ψ_AIPW(z) := m_AIPW(η₀, z, θ₀) with η₀ = (μ_val, e_val).
Definition (Lean source)
noncomputable def ψ_AIPW (S : BackdoorEstimationSystem P γ)
(z : γ × Bool × ℝ) : ℝ :=
aipwMoment z S.μ_val S.e_val (S.θ₀)
structure NuisanceVec reviewed
⚑ flagged
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*
fields
def η₀ reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
The truth η₀ : NuisanceVec γ.
Definition (Lean source)
noncomputable def η₀ (S : BackdoorEstimationSystem P γ) : NuisanceVec γ :=
⟨S.μ_val, S.e_val, S.μ_meas, S.e_meas⟩
def H_ε reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
The legacy overlap-bounded realization set consists of nuisance vectors whose propensity component lies between ε and 1 - ε at every covariate value.
Definition (Lean source)
def H_ε (ε : ℝ) : Set (NuisanceVec γ) :=
{ η | ∀ x, ε ≤ η.e_fn x ∧ η.e_fn x ≤ 1 - ε }
def H_ε_aeL2 reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Source-shaped AIPW nuisance class: the propensity is overlap-bounded P_X-almost everywhere, both outcome regressions are square-integrable under the covariate law, and the propensity belongs to L∞(P_X).
Definition (Lean source)
def H_ε_aeL2 (S : BackdoorEstimationSystem P γ) (ε : ℝ) :
Set (NuisanceVec γ) :=
{ η | (∀ᵐ 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 }
lemma H_ε_aeL2_mu_memLp reviewed
⚑ flagged
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
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
def aipwMomentFunctional reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
The AIPW moment as a moment functional NuisanceVec γ → X → ℝ → ℝ, suitable for feeding NeymanOrthogonal.
Definition (Lean source)
noncomputable def aipwMomentFunctional :
NuisanceVec γ → (γ × Bool × ℝ) → ℝ → ℝ :=
fun η z θ => aipwMoment z η.μ_fn η.e_fn θ
12 supporting declarations (lemmas, instances)
-
instZeroinstance — The zero nuisance sets both outcome regressions and the propensity function to zero.instance : Zero (NuisanceVec γ) where zero := ⟨fun _ _ => 0, fun _ => 0, fun _ => measurable_const, measurable_const⟩ -
instAddinstance — Addition of nuisance vectors is componentwise addition of the outcome regressions and propensity function.instance : Add (NuisanceVec γ) where 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⟩ -
instNeginstance — Negation of a nuisance vector negates each outcome regression and the propensity function.instance : Neg (NuisanceVec γ) where neg η := ⟨fun b x => -η.μ_fn b x, fun x => -η.e_fn x, fun b => (η.μ_meas b).neg, η.e_meas.neg⟩ -
instSubinstance — Subtraction of nuisance vectors is componentwise subtraction of the outcome regressions and propensity function.instance : Sub (NuisanceVec γ) where 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⟩ -
instSMulRealinstance — Scalar multiplication of a nuisance vector scales each outcome regression and the propensity function.instance : SMul ℝ (NuisanceVec γ) where 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⟩ -
exttheorem — Two AIPW nuisance vectors are equal when their outcome regressions and propensity functions agree everywhere.hypothesesconclusionη = η'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 -
ext_ifftheorem∀ {γ : Type u_1} [inst : MeasurableSpace γ] {η η' : NuisanceVec γ}, η = η' ↔ (∀ (b : Bool) (x : γ), η.μ_fn b x = η'.μ_fn b x) ∧ ∀ (x : γ), η.e_fn x = η'.e_fn xProof (Lean source)
@[ext] -
instAddCommGroupinstance — Nuisance vectors form an additive commutative group under componentwise operations.instance : AddCommGroup (NuisanceVec γ) where zero := 0 add := (· + ·) neg := neg sub := Sub.sub nsmul := nsmulRec zsmul := zsmulRec nsmul_zero η := by rfl nsmul_succ n η := by rfl zsmul_zero' η := by rfl zsmul_succ' n η := by rfl zsmul_neg' n η := by rfl 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) 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) zero_add η := by apply ext <;> intro b · intro x exact zero_add (η.μ_fn b x) · exact zero_add (η.e_fn b) add_zero η := by apply ext <;> intro b · intro x exact add_zero (η.μ_fn b x) · exact add_zero (η.e_fn b) neg_add_cancel η := by apply ext <;> intro b · intro x exact neg_add_cancel (η.μ_fn b x) · exact neg_add_cancel (η.e_fn b) 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) -
instModuleRealinstance — Nuisance vectors form a real vector space under componentwise scalar multiplication.instance : Module ℝ (NuisanceVec γ) where smul := (· • ·) 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 _ 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 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 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 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 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 _ -
H_ε_aeL2_overlap_factualXlemma — Membership in H_ε_aeL2 transports its a.e. overlap condition from the covariate law to the original probability space along the observed covariate.hypothesesconclusion∀ᵐ ω ∂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 -
H_ε_aeL2_overlap_P_Zlemma — Membership in H_ε_aeL2 transports its a.e. overlap condition from the covariate law to the observed-data law along the covariate projection.hypothesesProof (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 -
H_ε_aeL2_e_memLp_toplemma — The propensity component of an H_ε_aeL2 nuisance is in L∞(P_X).hypothesesconclusionMemLp η.e_fn ⊤ S.P_XProof (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
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
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Pointwise Lipschitz constant for the AIPW moment in η on H_ε: K_AIPW ε := 1 + 2/ε + 2/ε². Tracks the quadratic blow-up of the inverse weights 1/ê, 1/(1−ê) and the cross terms (ê − e)/(ê·e).
Definition (Lean source)
noncomputable def K_AIPW (ε : ℝ) : ℝ := 1 + 2 / ε + 2 / ε ^ 2
def YMuVal_residual_sq reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
The "tilted" cross-term integrand (|y − μ_val(1, x)| + |y − μ_val(0, x)|)², viewed as a fixed L¹(P_Z) function (witness via h_y2 + h_yd2 + Cauchy–Schwarz).
Definition (Lean source)
noncomputable def YMuVal_residual_sq
(S : BackdoorEstimationSystem P γ) : (γ × Bool × ℝ) → ℝ :=
fun z => (|projY z - S.μ_val true (projX z)|
+ |projY z - S.μ_val false (projX z)|) ^ 2
theorem aipw_score_diff_isLittleOp_one reviewed
⚑ flagged
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
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
2 supporting declarations (lemmas, instances)
-
aipw_score_diff_pointwise_boundtheorem — AIPW score Lipschitz bound on H_ε, P_Z-a.e.hypothesesconclusion∀ᵐ z ∂S.P_Z,|aipwMomentFunctional η z S.θ₀ - aipwMomentFunctional S.η₀ z S.θ₀|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) -
yMuVal_residual_sq_integrabletheorem — 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).hypothesesS :hA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μconclusionIntegrable (S.YMuVal_residual_sq) S.P_ZProof (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
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
⚑ flagged
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
S :
ε :
ℝ
h_overlap :
S.StrictOverlap ε
h_y2 :
Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 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
1 supporting declaration (lemmas, instances)
-
aipw_finite_var_of_counterfactual_sqtheorem — Counterfactual second moments are a stronger sufficient condition for aipw_finite_var.hypothesesS :ε :ℝh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μconclusionIntegrable (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
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
⚑ flagged
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
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
5 supporting declarations (lemmas, instances)
-
measurable_ψ_AIPWlemma — The AIPW influence function is measurable as a function of the observed data triple.Proof (Lean source)
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) -
propScore_ne_zerolemma — The conditional treatment probability for either treatment label is nonzero almost surely under the back-door assumptions.hypothesesconclusion∀ᵐ ω ∂P.μ, S.toPOBackdoorSystem.propScore d ω ≠ 0Proof (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 -
cond_exp_residual_zerolemma — 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.hypothesesconclusionP.μ[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 -
theta_zero_factualX_integrallemma — The estimand θ₀ = ∫ x, (μ_val(1,x) − μ_val(0,x)) ∂P_X lifts back to the ambient measure via factualX.hypothesesS :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] -
aipw_mean_zero_of_square_integrabletheorem — A stronger sufficient-condition corollary for aipw_mean_zero.hypothesesS :ε :ℝh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_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)) = 0Proof (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)
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
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Value-space propensity for label d: e_val for d = true, 1 − e_val for d = false.
Definition (Lean source)
noncomputable def e_val_label (S : BackdoorEstimationSystem P γ)
(d : Bool) (x : γ) : ℝ :=
if d then S.e_val x else 1 - S.e_val x
lemma weighted_residual_integral_zero reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Weighted-residual mean-zero identity (pull-out lemma). Fix a treatment label 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
S :
hA :
S.toPOBackdoorSystem.Assumptions
d :
g :
γ → ℝ
hg_meas :
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 _ _
lemma indicator_to_propScore_integral reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Propensity-score pull-out for the treatment indicator. Fix a treatment label , 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
S :
hA :
S.toPOBackdoorSystem.Assumptions
d :
f :
γ → ℝ
hf_meas :
hf_ind_int :
Integrable (fun ω => f (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ
conclusion
∫ ω, f (S.toPOBackdoorSystem.factualX ω) * S.toPOBackdoorSystem.dVar.indicator d ω ∂P.μ
= ∫ ω, f (S.toPOBackdoorSystem.factualX ω) * S.e_val_label d (S.toPOBackdoorSystem.factualX ω) ∂P.μ
Proof (Lean source)
lemma indicator_to_propScore_integral
(S : BackdoorEstimationSystem P γ)
(hA : S.toPOBackdoorSystem.Assumptions) (d : Bool)
(f : γ → ℝ) (hf_meas : Measurable f)
(hf_ind_int : Integrable
(fun ω => f (S.toPOBackdoorSystem.factualX ω) *
S.toPOBackdoorSystem.dVar.indicator d ω) P.μ) :
∫ ω, f (S.toPOBackdoorSystem.factualX ω) *
S.toPOBackdoorSystem.dVar.indicator d ω ∂P.μ
= ∫ ω, f (S.toPOBackdoorSystem.factualX ω) *
S.e_val_label d (S.toPOBackdoorSystem.factualX ω) ∂P.μ := by
have hf_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX]
(fun ω => f (S.toPOBackdoorSystem.factualX ω)) := by
change StronglyMeasurable[
comap S.toPOBackdoorSystem.factualX inferInstance]
(fun ω => f (S.toPOBackdoorSystem.factualX ω))
exact (hf_meas.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 hCE_pull :=
MeasureTheory.condExp_mul_of_stronglyMeasurable_left
(μ := P.μ) (m := S.toPOBackdoorSystem.sigmaX) hf_sm hf_ind_int hind_int
have hCE_replace :
P.μ[fun ω => f (S.toPOBackdoorSystem.factualX ω) *
S.toPOBackdoorSystem.dVar.indicator d ω |
S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ]
(fun ω => f (S.toPOBackdoorSystem.factualX ω) *
S.e_val_label d (S.toPOBackdoorSystem.factualX ω)) := by
refine hCE_pull.trans ?_
filter_upwards [propScore_eq_e_val_label_ae S hA d] with ω hω
have hω' :
P.μ[S.toPOBackdoorSystem.dVar.indicator d |
S.toPOBackdoorSystem.sigmaX] ω
= S.e_val_label d (S.toPOBackdoorSystem.factualX ω) := hω
rw [Pi.mul_apply, hω']
calc
∫ ω, f (S.toPOBackdoorSystem.factualX ω) *
S.toPOBackdoorSystem.dVar.indicator d ω ∂P.μ
= ∫ ω, P.μ[fun ω => f (S.toPOBackdoorSystem.factualX ω) *
S.toPOBackdoorSystem.dVar.indicator d ω |
S.toPOBackdoorSystem.sigmaX] ω ∂P.μ :=
(MeasureTheory.integral_condExp S.toPOBackdoorSystem.sigmaX_le).symm
_ = ∫ ω, f (S.toPOBackdoorSystem.factualX ω) *
S.e_val_label d (S.toPOBackdoorSystem.factualX ω) ∂P.μ :=
MeasureTheory.integral_congr_ae hCE_replace
3 supporting declarations (lemmas, instances)
-
measurable_e_val_labellemma — The value-space propensity for any treatment label is measurable.Proof (Lean source)
lemma measurable_e_val_label (S : BackdoorEstimationSystem P γ) (d : Bool) : Measurable (S.e_val_label d) := by cases d · exact measurable_const.sub S.e_meas · exact S.e_meas -
propScore_false_aelemma — propScore false =ᵐ 1 - propScore true under back-door assumptions. The indicator-pair sums to one pointwise, conditional expectation is linear, and preserves constants.hypothesesS :_hA :S.toPOBackdoorSystem.AssumptionsProof (Lean source)
lemma propScore_false_ae (S : BackdoorEstimationSystem P γ) (_hA : S.toPOBackdoorSystem.Assumptions) : S.toPOBackdoorSystem.propScore false =ᵐ[P.μ] (fun ω => 1 - S.toPOBackdoorSystem.propScore true ω) := by 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] with ω h1 h2 have hsum_ω : 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 linarith -
propScore_eq_e_val_label_aelemma — The σ(X)-conditional expectation of 1_{D=d} is e_val_label d (X) a.s.hypothesesconclusionS.toPOBackdoorSystem.propScore d=ᵐ[P.μ] (fun ω => S.e_val_label d (S.toPOBackdoorSystem.factualX ω))Proof (Lean source)
lemma propScore_eq_e_val_label_ae (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (d : Bool) : S.toPOBackdoorSystem.propScore d =ᵐ[P.μ] (fun ω => S.e_val_label d (S.toPOBackdoorSystem.factualX ω)) := by cases d · -- `d = false` filter_upwards [propScore_false_ae S hA, S.e_compat] with ω hf hc simp [e_val_label, hf, hc] · -- `d = true` filter_upwards [S.e_compat] with ω hc simp [e_val_label, hc]