Estimation.Efficiency

Semiparametric efficiency: tangent spaces, pathwise differentiability, and the efficiency bound for the ATE functional.

LAN 28 core · 33 supporting · 1 submodule Local asymptotic normality (LAN) and the scalar Hájek–Le Cam convolution theorem.
Exponential­Tilt 4 core · 7 supporting This module defines normalized exponential-tilt laws, proves that they are probability measures dominated by the base law, and proves the derivative of tilted expectations. ★ hasDerivAt_tiltExp

Normalized exponential tilts

This module defines normalized exponential-tilt laws, proves that they are probability measures dominated by the base law, and proves the derivative of tilted expectations. TiltTangent.lean uses these analytic facts to establish the DQM property required of regular submodels.

Reference: van der Vaart, Asymptotic Statistics (1998), §25.3; Bickel--Klaassen--Ritov--Wellner (1993), §3.3.

def tiltNorm reviewed
Causalean.Estimation.Efficiency

For a measurable sample space, a measure on that space, a real-valued score function, and a real perturbation parameter, the normalizing constant of the exponential tilt is ∫exp⁡(ts(z)) dP(z)\int \exp(ts(z))\,dP(z).

Definition (Lean source)
Z :
Type u_1
shared
P :
s :
Z → ℝ
t :
ℝ
tiltNorm P s t :
ℝ
∫ z, exp (t * s z) ∂P
Causalean.Estimation.Efficiency.tiltNorm · Causalean/Estimation/Efficiency/ExponentialTilt.lean:38
def tiltExp reviewed
Causalean.Estimation.Efficiency

For a measurable sample space, a measure on that space, a real-valued score function, a real-valued integrand, and a real perturbation parameter, the exponentially tilted expectation is ∫ϕ(z)exp⁡(ts(z)) dP(z)\int \phi(z)\exp(ts(z))\,dP(z) divided by ∫exp⁡(ts(z)) dP(z)\int \exp(ts(z))\,dP(z).

Definition (Lean source)
Z :
Type u_1
shared
P :
s φ :
Z → ℝ
t :
ℝ
tiltExp P s φ t :
ℝ
(∫ z, φ z * exp (t * s z) ∂P) / tiltNorm P s t
Causalean.Estimation.Efficiency.tiltExp · Causalean/Estimation/Efficiency/ExponentialTilt.lean:46
def tiltMeasure reviewed
Causalean.Estimation.Efficiency

For a measurable sample space, a measure on that space, a real-valued score function, and a real perturbation parameter, the exponentially tilted measure assigns density exp⁡(ts(z))/∫exp⁡(ts(u)) dP(u)\exp(ts(z))/\int\exp(ts(u))\,dP(u) relative to the given measure.

Definition (Lean source)
Z :
Type u_1
shared
P :
s :
Z → ℝ
t :
ℝ
tiltMeasure P s t :
(ofReal (tiltNorm P s t))⁻¹ • P.withDensity (fun z => ofReal (exp (t * s z)))
Causalean.Estimation.Efficiency.tiltMeasure · Causalean/Estimation/Efficiency/ExponentialTilt.lean:56
theorem hasDerivAt_tiltExp reviewed
Causalean.Estimation.Efficiency

The tilt-derivative lemma. Along the exponential tilt with a measurable score s that is bounded in absolute value by a constant M and has mean zero under P, the tilted expectation of a fixed function φ that is almost-everywhere strongly measurable and integrable against P is differentiable at t = 0, with derivative equal to ∫ φ·s dP. (Mean-zero s makes the normalizing-constant contribution vanish, so the derivative is the raw covariance ∫ φ·s dP.)

Formal statement
Z :
Type u_1
Z → ℝ
Z → ℝ
shared
M :
ℝ
shared
hs_meas :
hsM :
∀ z, |s z| ≤ M
hs_mean :
∫ z, s z ∂P = 0
hφ_meas :
hφ_int :
HasDerivAt (tiltExp P s φ) (∫ z, φ z * s z ∂P) 0
Proof (Lean source)
theorem hasDerivAt_tiltExp (hs_meas : Measurable s) (hsM : ∀ z, |s z| ≤ M) (hs_mean : ∫ z, s z ∂P = 0) (hφ_meas : AEStronglyMeasurable φ P) (hφ_int : Integrable φ P) : HasDerivAt (tiltExp P s φ) (∫ z, φ z * s z ∂P) 0 := by have hN : HasDerivAt (fun t => ∫ z, φ z * exp (t * s z) ∂P) (∫ z, φ z * s z ∂P) 0 := hasDerivAt_tilt_numerator hs_meas hsM hφ_meas hφ_int have hc : HasDerivAt (fun t => tiltNorm P s t) (∫ z, s z ∂P) 0 := by have := hasDerivAt_tilt_numerator (P := P) (φ := fun _ => (1 : ℝ)) hs_meas hsM aestronglyMeasurable_const (integrable_const (1 : ℝ)) simpa [tiltNorm, one_mul] using this have hc0_ne : tiltNorm P s 0 ≠ 0 := by rw [tiltNorm_zero]; norm_num have hquot := hN.div hc hc0_ne rw [tiltNorm_zero, hs_mean] at hquot have hfun : ((fun t => ∫ z, φ z * exp (t * s z) ∂P) / fun t => tiltNorm P s t) = tiltExp P s φ := by funext t; rfl rw [hfun] at hquot simpa [mul_zero, sub_zero, one_pow, div_one, mul_one] using hquot
Causalean.Estimation.Efficiency.hasDerivAt_tiltExp · Causalean/Estimation/Efficiency/ExponentialTilt.lean:153 · uses tiltExp
7 supporting declarations (lemmas, instances)
  • tiltNorm_zero lemma — At t = 0 the normalizing constant is the total mass = 1.
    Z :
    Type u_1
    shared
    s :
    Z → ℝ
    tiltNorm P s 0 = 1
    Proof (Lean source)
    @[simp] lemma tiltNorm_zero {P : Measure Z} [IsProbabilityMeasure P] {s : Z → ℝ} : tiltNorm P s 0 = 1 := by simp [tiltNorm]
    Causalean.Estimation.Efficiency.tiltNorm_zero · Causalean/Estimation/Efficiency/ExponentialTilt.lean:66
  • hasDerivAt_tilt_numerator lemma — Numerator derivative. d/dt ∫ φ·e^{t·s} dP |₀ = ∫ φ·s dP, for bounded measurable score s and integrable φ.
    Z :
    Type u_1
    Z → ℝ
    Z → ℝ
    shared
    M :
    ℝ
    shared
    hs_meas :
    hsM :
    ∀ z, |s z| ≤ M
    hφ_meas :
    hφ_int :
    HasDerivAt (fun t => ∫ z, φ z * exp (t * s z) ∂P) (∫ z, φ z * s z ∂P) 0
    Proof (Lean source)
    lemma hasDerivAt_tilt_numerator (hs_meas : Measurable s) (hsM : ∀ z, |s z| ≤ M) (hφ_meas : AEStronglyMeasurable φ P) (hφ_int : Integrable φ P) : HasDerivAt (fun t => ∫ z, φ z * exp (t * s z) ∂P) (∫ z, φ z * s z ∂P) 0 := by have hZ : Nonempty Z := nonempty_of_isProbabilityMeasure P set F : ℝ → Z → ℝ := fun t z => φ z * exp (t * s z) with hF set F' : ℝ → Z → ℝ := fun t z => φ z * s z * exp (t * s z) with hF' set bound : Z → ℝ := fun z => |φ z| * (M * exp M) with hbound have hM0 : 0 ≤ M := le_trans (abs_nonneg (s hZ.some)) (hsM hZ.some) have hset : ball (0 : ℝ) 1 ∈ 𝓝 (0 : ℝ) := Metric.ball_mem_nhds 0 one_pos have hF_meas : ∀ᶠ t in 𝓝 (0 : ℝ), AEStronglyMeasurable (F t) P := by filter_upwards with t exact hφ_meas.mul ((hs_meas.const_mul t).exp.aestronglyMeasurable) have hF0_int : Integrable (F 0) P := by simpa [hF] using hφ_int have hF'_meas : AEStronglyMeasurable (F' 0) P := by have : AEStronglyMeasurable (fun z => φ z * s z) P := hφ_meas.mul hs_meas.aestronglyMeasurable simpa [hF'] using this have h_bound : ∀ᵐ z ∂P, ∀ t ∈ ball (0 : ℝ) 1, ‖F' t z‖ ≤ bound z := by filter_upwards with z t ht have htlt : |t| < 1 := by simpa [Real.dist_eq] using ht have hexp_le : exp (t * s z) ≤ exp M := by apply Real.exp_le_exp.2 calc t * s z ≤ |t * s z| := le_abs_self _ _ = |t| * |s z| := abs_mul _ _ _ ≤ 1 * M := by apply mul_le_mul (le_of_lt htlt) (hsM z) (abs_nonneg _) (by norm_num) _ = M := one_mul _ calc ‖F' t z‖ = |φ z| * |s z| * exp (t * s z) := by rw [hF'] rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_pos (Real.exp_pos _)] _ ≤ |φ z| * M * exp M := by apply mul_le_mul · exact mul_le_mul_of_nonneg_left (hsM z) (abs_nonneg _) · exact hexp_le · exact (Real.exp_pos _).le · exact mul_nonneg (abs_nonneg _) hM0 _ = bound z := by rw [hbound]; ring have hbound_int : Integrable bound P := by rw [hbound]; exact hφ_int.abs.mul_const _ have h_diff : ∀ᵐ z ∂P, ∀ t ∈ ball (0 : ℝ) 1, HasDerivAt (fun t => F t z) (F' t z) t := by filter_upwards with z t _ have h1 : HasDerivAt (fun t : ℝ => t * s z) (s z) t := by simpa using (hasDerivAt_id t).mul_const (s z) have h2 : HasDerivAt (fun t : ℝ => exp (t * s z)) (exp (t * s z) * s z) t := h1.exp have h3 := h2.const_mul (φ z) simpa [hF, hF', mul_comm, mul_left_comm, mul_assoc] using h3 have hmain := hasDerivAt_integral_of_dominated_loc_of_deriv_le (bound := bound) (F := F) (F' := F') (x₀ := (0 : ℝ)) (s := ball (0 : ℝ) 1) hset hF_meas hF0_int hF'_meas h_bound hbound_int h_diff have hconc := hmain.2 have heq : (∫ z, F' 0 z ∂P) = ∫ z, φ z * s z ∂P := by apply integral_congr_ae filter_upwards with z simp [hF'] rw [heq] at hconc exact hconc
    Causalean.Estimation.Efficiency.hasDerivAt_tilt_numerator · Causalean/Estimation/Efficiency/ExponentialTilt.lean:89
  • tilt_exp_integrable lemma — For a bounded measurable score, e^{t·s} is P-integrable (it is bounded by the constant e^{|t|·M} on the finite measure P).
    Z :
    Type u_1
    Z → ℝ
    shared
    M :
    ℝ
    shared
    t :
    ℝ
    shared
    hs_meas :
    hsM :
    ∀ z, |s z| ≤ M
    Integrable (fun z => exp (t * s z)) P
    Proof (Lean source)
    lemma tilt_exp_integrable (hs_meas : Measurable s) (hsM : ∀ z, |s z| ≤ M) : Integrable (fun z => exp (t * s z)) P := by apply Integrable.mono' (integrable_const (exp (|t| * M))) (hs_meas.const_mul t).exp.aestronglyMeasurable filter_upwards with z rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] apply Real.exp_le_exp.2 calc t * s z ≤ |t * s z| := le_abs_self _ _ = |t| * |s z| := abs_mul _ _ _ ≤ |t| * M := mul_le_mul_of_nonneg_left (hsM z) (abs_nonneg _)
    Causalean.Estimation.Efficiency.tilt_exp_integrable · Causalean/Estimation/Efficiency/ExponentialTilt.lean:196
  • tiltNorm_pos lemma — The normalizing constant c(t) = ∫ e^{t·s} dP is strictly positive.
    Z :
    Type u_1
    Z → ℝ
    shared
    M :
    ℝ
    shared
    t :
    ℝ
    shared
    hs_meas :
    hsM :
    ∀ z, |s z| ≤ M
    0 < tiltNorm P s t
    Proof (Lean source)
    lemma tiltNorm_pos (hs_meas : Measurable s) (hsM : ∀ z, |s z| ≤ M) : 0 < tiltNorm P s t := by have hlow : ∀ z, exp (-(|t| * M)) ≤ exp (t * s z) := by intro z apply Real.exp_le_exp.2 have : -(|t| * M) ≤ t * s z := by have h1 : -(|t| * M) ≤ -|t * s z| := by rw [neg_le_neg_iff, abs_mul] exact mul_le_mul_of_nonneg_left (hsM z) (abs_nonneg _) exact le_trans h1 (neg_abs_le _) exact this calc (0 : ℝ) < exp (-(|t| * M)) := Real.exp_pos _ _ = ∫ _z, exp (-(|t| * M)) ∂P := by rw [integral_const, probReal_univ, one_smul] _ ≤ tiltNorm P s t := integral_mono (integrable_const _) (tilt_exp_integrable hs_meas hsM) hlow
    Causalean.Estimation.Efficiency.tiltNorm_pos · Causalean/Estimation/Efficiency/ExponentialTilt.lean:209
  • tiltMeasure_eq_withDensity_div lemma — For a probability law P, a measurable bounded score s, and a perturbation t, the exponential tilt is P weighted by the normalized density exp(ts)/∫exp(ts)dP.
    Z :
    Type u_1
    shared
    s :
    Z → ℝ
    M t :
    ℝ
    hs_meas :
    hsM :
    ∀ z, |s z| ≤ M
    tiltMeasure P s t
    = P.withDensity (fun z => ofReal (exp (t * s z) / ∫ y, exp (t * s y) ∂P))
    Proof (Lean source)
    lemma tiltMeasure_eq_withDensity_div (P : Measure Z) [IsProbabilityMeasure P] (s : Z → ℝ) (M t : ℝ) (hs_meas : Measurable s) (hsM : ∀ z, |s z| ≤ M) : tiltMeasure P s t = P.withDensity (fun z => ofReal (exp (t * s z) / ∫ y, exp (t * s y) ∂P)) := by have hc : 0 < tiltNorm P s t := tiltNorm_pos hs_meas hsM have he_meas : Measurable (fun z => ofReal (exp (t * s z))) := by fun_prop rw [tiltMeasure, ← withDensity_smul (ofReal (tiltNorm P s t))⁻¹ he_meas] congr 1 funext z rw [Pi.smul_apply, smul_eq_mul] rw [← ENNReal.ofReal_inv_of_pos hc] rw [← ENNReal.ofReal_mul (inv_nonneg.mpr hc.le)] congr 1 simp [tiltNorm, div_eq_mul_inv, mul_comm]
    Causalean.Estimation.Efficiency.tiltMeasure_eq_withDensity_div · Causalean/Estimation/Efficiency/ExponentialTilt.lean:227
  • isProbabilityMeasure_tiltMeasure lemma — The tilted law tiltMeasure P s t is a probability measure.
    Z :
    Type u_1
    Z → ℝ
    shared
    M :
    ℝ
    shared
    t :
    ℝ
    shared
    hs_meas :
    hsM :
    ∀ z, |s z| ≤ M
    IsProbabilityMeasure (tiltMeasure P s t)
    Proof (Lean source)
    lemma isProbabilityMeasure_tiltMeasure (hs_meas : Measurable s) (hsM : ∀ z, |s z| ≤ M) : IsProbabilityMeasure (tiltMeasure P s t) := by constructor have hnn : 0 ≤ᵐ[P] fun z => exp (t * s z) := Filter.Eventually.of_forall fun z => (Real.exp_pos _).le have hmass : (P.withDensity (fun z => ofReal (exp (t * s z)))) univ = ofReal (tiltNorm P s t) := by rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ, ← ofReal_integral_eq_lintegral_ofReal (tilt_exp_integrable hs_meas hsM) hnn] rfl rw [tiltMeasure, Measure.smul_apply, hmass, smul_eq_mul] have hne0 : ofReal (tiltNorm P s t) ≠ 0 := by rw [Ne, ENNReal.ofReal_eq_zero, not_le] exact tiltNorm_pos hs_meas hsM exact ENNReal.inv_mul_cancel hne0 ENNReal.ofReal_ne_top
    Causalean.Estimation.Efficiency.isProbabilityMeasure_tiltMeasure · Causalean/Estimation/Efficiency/ExponentialTilt.lean:248
  • integral_tiltMeasure lemma — The expectation of h_fn under the tilted law equals tiltExp P s h_fn t. (No integrability hypothesis is needed: both sides reduce to the same P-integral of h_fn · e^{t·s} scaled by 1/c(t), and a non-integrable h_fn makes both the integral and tiltExp's numerator the same junk default.)
    Z :
    Type u_1
    Z → ℝ
    shared
    M :
    ℝ
    shared
    t :
    ℝ
    shared
    hs_meas :
    hsM :
    ∀ z, |s z| ≤ M
    h_fn :
    Z → ℝ
    ∫ z, h_fn z ∂(tiltMeasure P s t) = tiltExp P s h_fn t
    Proof (Lean source)
    lemma integral_tiltMeasure (hs_meas : Measurable s) (hsM : ∀ z, |s z| ≤ M) {h_fn : Z → ℝ} : ∫ z, h_fn z ∂(tiltMeasure P s t) = tiltExp P s h_fn t := by rw [tiltMeasure, integral_smul_measure] have hdens : (fun z => ofReal (exp (t * s z))) = (fun z => (((exp (t * s z)).toNNReal : NNReal) : ENNReal)) := rfl have hwd : ∫ z, h_fn z ∂(P.withDensity (fun z => ofReal (exp (t * s z)))) = ∫ z, exp (t * s z) * h_fn z ∂P := by rw [hdens, integral_withDensity_eq_integral_smul₀ ((hs_meas.const_mul t).exp.real_toNNReal.aemeasurable) h_fn] apply integral_congr_ae filter_upwards with z rw [NNReal.smul_def, smul_eq_mul, Real.coe_toNNReal _ (Real.exp_pos _).le] rw [hwd] rw [ENNReal.toReal_inv, ENNReal.toReal_ofReal (tiltNorm_pos hs_meas hsM).le, smul_eq_mul] rw [tiltExp, div_eq_inv_mul] congr 1 apply integral_congr_ae filter_upwards with z ring
    Causalean.Estimation.Efficiency.integral_tiltMeasure · Causalean/Estimation/Efficiency/ExponentialTilt.lean:267
Observed­Law­ATE 10 core · 13 supporting This module defines the propensity score, arm regressions, and g-formula ATE directly from a probability law on observed triples (X, D, Y). ★ observedATE_P_Z_eq

The average treatment effect as a functional of an observed-data law

This module defines the propensity score, arm regressions, and g-formula ATE directly from a probability law on observed triples (X, D, Y). All nuisance functions are recomputed from the supplied law by conditioning on the σ-algebra generated by the covariate projection. The final lemmas identify these canonical observed-law nuisances at a backdoor system's true law with the system's existing value-space representatives.

def observedCovariateSigma reviewed
Causalean.Estimation.Efficiency

For a covariate space γ, the covariate σ-algebra on observed triples is generated by the projection (x,d,y) ↦ x.

Definition (Lean source)
γ :
Type u_1
shared
observedCovariateSigma :
MeasurableSpace (γ × Bool × ℝ)
comap ATE.BackdoorEstimationSystem.projX inferInstance
Causalean.Estimation.Efficiency.observedCovariateSigma · Causalean/Estimation/Efficiency/ObservedLawATE.lean:36
def observedArmIndicator reviewed
Causalean.Estimation.Efficiency

For a treatment arm d and an observed triple z, the arm indicator is one when the observed treatment equals d and zero otherwise.

Definition (Lean source)
γ :
Type u_1
shared
d :
z :
γ × Bool × ℝ
observedArmIndicator d z :
ℝ
if ATE.BackdoorEstimationSystem.projA z = d then 1 else 0
Causalean.Estimation.Efficiency.observedArmIndicator · Causalean/Estimation/Efficiency/ObservedLawATE.lean:47
def observedPropensity reviewed
Causalean.Estimation.Efficiency

For a probability law Q on observed triples and a treatment arm d, the law's arm propensity is the conditional expectation of the arm indicator given the covariate σ-algebra.

Definition (Lean source)
γ :
Type u_1
shared
Q :
Measure (γ × Bool × ℝ)
d :
observedPropensity Q d :
γ × Bool × ℝ → ℝ
@condExp (γ × Bool × ℝ) ℝ (observedCovariateSigma (γ := γ)) _ _ _ Q (observedArmIndicator d)
Causalean.Estimation.Efficiency.observedPropensity · Causalean/Estimation/Efficiency/ObservedLawATE.lean:59
def observedArmNumerator reviewed
Causalean.Estimation.Efficiency

For a probability law Q on observed triples and a treatment arm d, the law's arm outcome numerator is the conditional expectation of Y 1{D=d} given the covariate σ-algebra.

Definition (Lean source)
γ :
Type u_1
shared
Q :
Measure (γ × Bool × ℝ)
d :
observedArmNumerator Q d :
γ × Bool × ℝ → ℝ
@condExp (γ × Bool × ℝ) ℝ (observedCovariateSigma (γ := γ)) _ _ _ Q (fun z => ATE.BackdoorEstimationSystem.projY z * observedArmIndicator d z)
Causalean.Estimation.Efficiency.observedArmNumerator · Causalean/Estimation/Efficiency/ObservedLawATE.lean:67
def observedArmRegression reviewed
Causalean.Estimation.Efficiency

For a probability law Q on observed triples and a treatment arm d, the law's arm outcome regression is the conditional Y 1{D=d} numerator divided by the corresponding arm propensity.

Definition (Lean source)
γ :
Type u_1
shared
Q :
Measure (γ × Bool × ℝ)
d :
observedArmRegression Q d :
γ × Bool × ℝ → ℝ
Causalean.Estimation.Efficiency.observedArmRegression · Causalean/Estimation/Efficiency/ObservedLawATE.lean:75
def observedArmMean reviewed
Causalean.Estimation.Efficiency

For a probability law Q on observed triples and a treatment arm d, the observed-law arm mean functional integrates the recomputed arm regression μ_d(X) against Q.

Definition (Lean source)
γ :
Type u_1
shared
Q :
Measure (γ × Bool × ℝ)
d :
observedArmMean Q d :
ℝ
∫ z, observedArmRegression Q d z ∂Q
Causalean.Estimation.Efficiency.observedArmMean · Causalean/Estimation/Efficiency/ObservedLawATE.lean:82
def observedATE reviewed
Causalean.Estimation.Efficiency

For a probability law Q on observed triples, the observed-law average treatment-effect functional integrates the recomputed treated-minus-control arm regression against Q.

Definition (Lean source)
γ :
Type u_1
shared
Q :
Measure (γ × Bool × ℝ)
observedATE Q :
ℝ
Causalean.Estimation.Efficiency.observedATE · Causalean/Estimation/Efficiency/ObservedLawATE.lean:88
def observedAIPW reviewed
Causalean.Estimation.Efficiency

For a base observed-data law Q and an observed triple z, the law-recomputed AIPW influence function is the arm-regression contrast centered by observedATE Q, augmented by the two inverse-arm-propensity residuals.

Definition (Lean source)
γ :
Type u_1
shared
Q :
Measure (γ × Bool × ℝ)
z :
γ × Bool × ℝ
observedAIPW Q z :
ℝ
+ observedArmIndicator true z / observedPropensity Q true z * (ATE.BackdoorEstimationSystem.projY z - observedArmRegression Q true z)
- observedArmIndicator false z / observedPropensity Q false z * (ATE.BackdoorEstimationSystem.projY z - observedArmRegression Q false z)
Causalean.Estimation.Efficiency.observedAIPW · Causalean/Estimation/Efficiency/ObservedLawATE.lean:104
def observedArmEIF reviewed
Causalean.Estimation.Efficiency

For a base observed-data law Q, a treatment arm d, and an observed triple z, the efficient-influence-function candidate for the arm mean is the inverse-propensity-weighted arm residual plus μ_d(X), centered by the arm mean.

Definition (Lean source)
γ :
Type u_1
shared
Q :
Measure (γ × Bool × ℝ)
d :
z :
γ × Bool × ℝ
observedArmEIF Q d z :
ℝ
observedArmIndicator d z / observedPropensity Q d z * (ATE.BackdoorEstimationSystem.projY z - observedArmRegression Q d z)
Causalean.Estimation.Efficiency.observedArmEIF · Causalean/Estimation/Efficiency/ObservedLawATE.lean:114
theorem observedATE_P_Z_eq reviewed
Causalean.Estimation.Efficiency.ATE.BackdoorEstimationSystem

Under the backdoor assumptions, the observed-law ATE functional at a backdoor system's true law equals its value-space ATE.

Formal statement
γ :
Type u_1
shared
P :
shared
S :
ATE.BackdoorEstimationSystem P γ
hA :
S.toPOBackdoorSystem.Assumptions
observedATE S.P_Z = S.θ₀
Proof (Lean source)
theorem observedATE_P_Z_eq (S : ATE.BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) : observedATE S.P_Z = S.θ₀ := by unfold observedATE ATE.BackdoorEstimationSystem.θ₀ apply Eq.trans (integral_congr_ae ((observedArmRegression_P_Z_ae S hA true).sub (observedArmRegression_P_Z_ae S hA false))) rw [← S.P_Z_map_projX_eq_P_X] simpa only [ATE.BackdoorEstimationSystem.projX, Pi.sub_apply, Function.comp_apply] using (integral_map measurable_fst.aemeasurable ((S.μ_meas true).sub (S.μ_meas false)).aestronglyMeasurable).symm
Causalean.Estimation.Efficiency.ATE.BackdoorEstimationSystem.observedATE_P_Z_eq · Causalean/Estimation/Efficiency/ObservedLawATE.lean:308 · uses BackdoorEstimationSystem , P_Z , θ₀ , observedATE , Assumptions , POSystem
13 supporting declarations (lemmas, instances)
Tangent­Projection 6 core · 8 supporting This file defines equality of directional inner products along a tangent subspace, the orthogonal projection of a reference vector, and the projection's squared norm. ★ normSq_gradient_decomp★ effBound_le_normSq★ norm_eq_iff_eq_efficientIF

Tangent-space projection geometry

This file defines equality of directional inner products along a tangent subspace, the orthogonal projection of a reference vector, and the projection's squared norm. It proves the associated minimum-norm and tangent-shrinking identities used after a statistical model supplies the pathwise-gradient bridge.

def IsGradient reviewed
Causalean.Estimation.Efficiency

Given a real normed inner-product space, a linear subspace designated as the tangent space, and two vectors, a reference influence function and a candidate gradient, the candidate is a gradient of the reference relative to the tangent space exactly when, for every vector in that subspace, its inner product with the candidate equals its inner product with the reference.

Definition (Lean source)
H :
Type u_1
shared
T :
Submodule ℝ H
g ψ :
H
s ∈ T :
IsGradient T g ψ :
Prop
⟪ψ, s⟫_ℝ = ⟪g, s⟫_ℝ
Causalean.Estimation.Efficiency.IsGradient · Causalean/Estimation/Efficiency/TangentProjection.lean:47
def efficientIF reviewed
Causalean.Estimation.Efficiency

Given a real normed inner-product space, a tangent subspace admitting an orthogonal projection, and a reference vector, the projected reference vector is the orthogonal projection of g onto that tangent subspace.

Definition (Lean source)
H :
Type u_1
shared
T :
Submodule ℝ H
T.HasOrthogonalProjection
g :
H
efficientIF T g :
H
(T.orthogonalProjection g : H)
Causalean.Estimation.Efficiency.efficientIF · Causalean/Estimation/Efficiency/TangentProjection.lean:60
def effBound reviewed
Causalean.Estimation.Efficiency

Given a real normed inner-product space, a tangent subspace admitting an orthogonal projection, and a reference vector, the projection-norm functional is the squared norm of the projected reference vector.

Definition (Lean source)
H :
Type u_1
shared
T :
Submodule ℝ H
T.HasOrthogonalProjection
g :
H
effBound T g :
ℝ
‖efficientIF T g‖ ^ 2
Causalean.Estimation.Efficiency.effBound · Causalean/Estimation/Efficiency/TangentProjection.lean:70
theorem normSq_gradient_decomp reviewed
Causalean.Estimation.Efficiency

Pythagoras for gradients. For any function ψ that is a gradient at g, the squared norm of ψ splits into the efficiency bound plus the squared norm of the remainder orthogonal to the efficient influence function.

Formal statement
H :
Type u_1
Submodule ℝ H
H
shared
h :
IsGradient T g ψ
‖ψ‖ ^ 2 = ‖efficientIF T g‖ ^ 2 + ‖ψ - efficientIF T g‖ ^ 2
Proof (Lean source)
theorem normSq_gradient_decomp {g ψ : H} (h : IsGradient T g ψ) : ‖ψ‖ ^ 2 = ‖efficientIF T g‖ ^ 2 + ‖ψ - efficientIF T g‖ ^ 2 := by have hproj : (T.orthogonalProjection ψ : H) = efficientIF T g := orthogonalProjection_eq_of_isGradient h have hmem : efficientIF T g ∈ T := efficientIF_mem g have horth : ψ - efficientIF T g ∈ Tᗮ := by rw [← hproj] exact T.sub_starProjection_mem_orthogonal ψ have hzero : ⟪efficientIF T g, ψ - efficientIF T g⟫_ℝ = 0 := (Submodule.mem_orthogonal _ _).1 horth _ hmem have hsplit : ψ = efficientIF T g + (ψ - efficientIF T g) := by abel calc ‖ψ‖ ^ 2 = ‖efficientIF T g + (ψ - efficientIF T g)‖ ^ 2 := by rw [← hsplit] _ = ‖efficientIF T g‖ ^ 2 + ‖ψ - efficientIF T g‖ ^ 2 := by rw [norm_add_sq_real, hzero]; ring
Causalean.Estimation.Efficiency.normSq_gradient_decomp · Causalean/Estimation/Efficiency/TangentProjection.lean:124 · uses IsGradient , efficientIF
theorem effBound_le_normSq reviewed
Causalean.Estimation.Efficiency

Efficiency lower bound. For any function ψ that is a gradient at g, the efficiency bound is at most the squared norm of ψ.

Formal statement
H :
Type u_1
Submodule ℝ H
H
shared
h :
IsGradient T g ψ
effBound T g ≤ ‖ψ‖ ^ 2
Proof (Lean source)
theorem effBound_le_normSq {g ψ : H} (h : IsGradient T g ψ) : effBound T g ≤ ‖ψ‖ ^ 2 := by rw [effBound, normSq_gradient_decomp h] have : (0 : ℝ) ≤ ‖ψ - efficientIF T g‖ ^ 2 := sq_nonneg _ linarith
Causalean.Estimation.Efficiency.effBound_le_normSq · Causalean/Estimation/Efficiency/TangentProjection.lean:142 · uses IsGradient , effBound
theorem norm_eq_iff_eq_efficientIF reviewed
Causalean.Estimation.Efficiency

Sharpness. For any function ψ that is a gradient at g, ψ attains the efficiency bound if and only if it equals the efficient influence function.

Formal statement
H :
Type u_1
Submodule ℝ H
H
shared
h :
IsGradient T g ψ
‖ψ‖ ^ 2 = effBound T g ↔ ψ = efficientIF T g
Proof (Lean source)
theorem norm_eq_iff_eq_efficientIF {g ψ : H} (h : IsGradient T g ψ) : ‖ψ‖ ^ 2 = effBound T g ↔ ψ = efficientIF T g := by rw [effBound, normSq_gradient_decomp h] constructor · intro heq have hsq : ‖ψ - efficientIF T g‖ ^ 2 = 0 := by linarith have hnorm : ‖ψ - efficientIF T g‖ = 0 := by exact pow_eq_zero_iff (by norm_num) |>.1 hsq rw [norm_eq_zero, sub_eq_zero] at hnorm exact hnorm · intro heq rw [heq, sub_self, norm_zero]; ring
Causalean.Estimation.Efficiency.norm_eq_iff_eq_efficientIF · Causalean/Estimation/Efficiency/TangentProjection.lean:150 · uses IsGradient , effBound , efficientIF
8 supporting declarations (lemmas, instances)
Pathwise­Gradient 11 core · 11 supporting This module implements the standard semiparametric framework of van der Vaart (1998), §25.3. ★ score_eq_of_path_eq★ efficientInfluenceFunction_unique★ canonicalGradient_normSq_le

DQM submodels, tangent spaces, and pathwise gradients

This module implements the standard semiparametric framework of van der Vaart (1998), §25.3. A regular submodel is a path of probability laws dominated by the base law whose square-root Radon--Nikodym densities are differentiable in quadratic mean. Its score is therefore determined by its path.

A model is represented by a chosen family of regular submodels. Its tangent space is the closed linear span of their scores. A pathwise gradient represents the derivative of the functional along every member of that family, and its orthogonal projection onto the tangent space is the canonical gradient, or efficient influence function.

The restriction P_t ≪ P does not shrink the tangent space of the nonparametric model: TiltTangent.lean constructs dominated bounded exponential tilts whose scores already span a dense subspace of L²₀(P).

Paths are indexed by all t ∈ ℝ, and derivatives at zero are two-sided. This is the usual nonparametric or regular-parametric setting with the base law at an interior parameter value. One-sided tangent cones and boundary models are not represented by this interface.

def dqmQuotient reviewed
Causalean.Estimation.Efficiency

Given a base probability law P, a probability law Q, and a perturbation parameter t, the DQM square-root-density quotient is t⁻¹(sqrt(dQ/dP) - 1) as an element of L²(P).

Definition (Lean source)
Z :
Type u_1
shared
t :
ℝ
dqmQuotient P Q t :
Lp ℝ 2 P
t⁻¹ • (rnSqrtDensityLp P Q - lpOne P)
Causalean.Estimation.Efficiency.dqmQuotient · Causalean/Estimation/Efficiency/PathwiseGradient.lean:48
structure RegularSubmodel reviewed
Causalean.Estimation.Efficiency

A regular submodel through a probability law P consists of a path of probability laws passing through P at zero, dominated by P, and a mean-zero square-integrable score coupled to that path by differentiability in quadratic mean.

Definition (Lean source)
Z :
Type u_1
shared
The two-sided one-parameter path of laws, indexed by every real `t`.
path :
ℝ → Measure Z
Every law on the path is a probability measure.
path_probability :
∀ t, IsProbabilityMeasure (path t)
The path passes through the base law at zero.
path_zero :
path 0 = P
Every path law is absolutely continuous with respect to the base law.
path_ac :
∀ t, path t ≪ P
The square-integrable score.
score :
Lp ℝ 2 P
The score has mean zero under the base law.
score_meanZero :
score ∈ meanZeroLp P
The square-root-density difference quotient converges in L² to half the score.
dqm :
Tendsto (fun t => letI := path_probability t; dqmQuotient P (path t) t) (𝓝[≠] 0) (𝓝 ((2 : ℝ)⁻¹ • score))
Causalean.Estimation.Efficiency.RegularSubmodel · Causalean/Estimation/Efficiency/PathwiseGradient.lean:61
theorem score_eq_of_path_eq reviewed
Causalean.Estimation.Efficiency.RegularSubmodel

If two regular submodels through P have the same law path, then their DQM scores are equal.

Formal statement
Z :
Type u_1
shared
m n :
hpath :
m.path = n.path
m.score = n.score
Proof (Lean source)
theorem score_eq_of_path_eq {P : Measure Z} [IsProbabilityMeasure P] (m n : RegularSubmodel P) (hpath : m.path = n.path) : m.score = n.score := by have hm := m.dqm have hn := n.dqm have hcurve : (fun t => letI := m.path_probability t; dqmQuotient P (m.path t) t) = (fun t => letI := n.path_probability t; dqmQuotient P (n.path t) t) := by funext t exact @dqmQuotient_congr Z _ P (m.path t) (n.path t) _ (m.path_probability t) (n.path_probability t) t (congrFun hpath t) rw [hcurve] at hm have hhalf : (2 : ℝ)⁻¹ • m.score = (2 : ℝ)⁻¹ • n.score := tendsto_nhds_unique hm hn have hscaled := congrArg (fun x : Lp ℝ 2 P => (2 : ℝ) • x) hhalf simpa [smul_smul] using hscaled
Causalean.Estimation.Efficiency.RegularSubmodel.score_eq_of_path_eq · Causalean/Estimation/Efficiency/PathwiseGradient.lean:122 · uses RegularSubmodel
def constant reviewed
Causalean.Estimation.Efficiency.RegularSubmodel

For a base probability law P, the constant regular submodel keeps the law equal to P and has zero score.

Definition (Lean source)
Z :
Type u_1
shared
constant P :
clause 1
path := fun _ => P
clause 2
path_probability := fun _ => inferInstance
clause 3
path_zero := rfl
clause 4
path_ac := fun _ => Measure.AbsolutelyContinuous.rfl
clause 5
score := 0
clause 6
score_meanZero := (meanZeroLp P).zero_mem
clause 7
dqm := by simpa [dqmQuotient] using (tendsto_const_nhds : Tendsto (fun _ : ℝ => (0 : Lp ℝ 2 P)) (𝓝[≠] 0) (𝓝 0))
Causalean.Estimation.Efficiency.RegularSubmodel.constant · Causalean/Estimation/Efficiency/PathwiseGradient.lean:140 · uses RegularSubmodel
def scoreSet reviewed
Causalean.Estimation.Efficiency

Given a probability law P and a chosen family S of regular submodels through it, the tangent score set consists of the scores of members of S.

Definition (Lean source)
Z :
Type u_1
shared
scoreSet P S :
Set (Lp ℝ 2 P)
{g | ∃ m ∈ S, m.score = g}
Causalean.Estimation.Efficiency.scoreSet · Causalean/Estimation/Efficiency/PathwiseGradient.lean:162 · uses RegularSubmodel
def tangentSpace reviewed
Causalean.Estimation.Efficiency

Given a probability law P and a chosen family S of regular submodels, the generated tangent space is the closed linear span of their score set.

Definition (Lean source)
Z :
Type u_1
shared
tangentSpace P S :
Submodule ℝ (Lp ℝ 2 P)
Causalean.Estimation.Efficiency.tangentSpace · Causalean/Estimation/Efficiency/PathwiseGradient.lean:169 · uses RegularSubmodel
def IsPathwiseGradient reviewed
Causalean.Estimation.Efficiency

Given a probability law P, a functional ψ, an L² candidate g, and a family S of regular submodels, the candidate is a pathwise gradient relative to S when every path derivative equals its inner product with that path's DQM score.

Definition (Lean source)
Z :
Type u_1
shared
ψ :
Measure Z → ℝ
g :
Lp ℝ 2 P
m ∈ S :
IsPathwiseGradient P ψ g S :
Prop
HasDerivAt (fun t => ψ (m.path t)) ⟪g, m.score⟫_ℝ 0
Causalean.Estimation.Efficiency.IsPathwiseGradient · Causalean/Estimation/Efficiency/PathwiseGradient.lean:195 · uses RegularSubmodel
def canonicalGradient reviewed
Causalean.Estimation.Efficiency

Given a probability law P, a submodel family S, and a reference gradient g, the canonical gradient is the orthogonal projection of g onto the tangent space generated by S.

Definition (Lean source)
Z :
Type u_1
shared
g :
Lp ℝ 2 P
canonicalGradient P S g :
Lp ℝ 2 P
efficientIF (tangentSpace P S) g
Causalean.Estimation.Efficiency.canonicalGradient · Causalean/Estimation/Efficiency/PathwiseGradient.lean:234 · uses RegularSubmodel
def IsEfficientInfluenceFunction reviewed
Causalean.Estimation.Efficiency

Given a probability law P, a functional ψ, a candidate g, and a submodel family S, the candidate is an efficient influence function when it is a pathwise gradient and belongs to the generated tangent space.

Definition (Lean source)
Z :
Type u_1
shared
ψ :
Measure Z → ℝ
g :
Lp ℝ 2 P
IsEfficientInfluenceFunction P ψ g S :
Prop
clause 1
clause 2
g ∈ tangentSpace P S
Causalean.Estimation.Efficiency.IsEfficientInfluenceFunction · Causalean/Estimation/Efficiency/PathwiseGradient.lean:241 · uses RegularSubmodel
theorem efficientInfluenceFunction_unique reviewed
Causalean.Estimation.Efficiency

If two candidates are efficient influence functions for the same functional and submodel family, then they are equal.

Formal statement
Z :
Type u_1
shared
ψ :
Measure Z → ℝ
g g' :
Lp ℝ 2 P
g = g'
Proof (Lean source)
theorem efficientInfluenceFunction_unique {P : Measure Z} [IsProbabilityMeasure P] {ψ : Measure Z → ℝ} {S : Set (RegularSubmodel P)} {g g' : Lp ℝ 2 P} (hg : IsEfficientInfluenceFunction P ψ g S) (hg' : IsEfficientInfluenceFunction P ψ g' S) : g = g' := by have horth := sub_mem_orthogonal_of_isPathwiseGradient hg.1 hg'.1 have hzero : g - g' = 0 := by apply (inner_self_eq_zero (𝕜 := ℝ)).mp exact (Submodule.mem_orthogonal' (tangentSpace P S) (g - g')).1 horth (g - g') ((tangentSpace P S).sub_mem hg.2 hg'.2) exact sub_eq_zero.mp hzero
Causalean.Estimation.Efficiency.efficientInfluenceFunction_unique · Causalean/Estimation/Efficiency/PathwiseGradient.lean:272 · uses IsEfficientInfluenceFunction , RegularSubmodel
theorem canonicalGradient_normSq_le reviewed
Causalean.Estimation.Efficiency

The squared norm of the canonical gradient of a square-integrable candidate g is no larger than the squared norm of g, the Hilbert-space efficiency bound. The corresponding statistical lower bound is AsymptoticLanConvolution.regular_asymptoticVariance_ge_gradientNormSq, which shows that a regular estimator's asymptotic variance cannot fall below the canonical-gradient norm squared.

Formal statement
Z :
Type u_1
shared
g :
Lp ℝ 2 P
‖canonicalGradient P S g‖ ^ 2 ≤ ‖g‖ ^ 2
Proof (Lean source)
theorem canonicalGradient_normSq_le {P : Measure Z} [IsProbabilityMeasure P] {S : Set (RegularSubmodel P)} {g : Lp ℝ 2 P} : ‖canonicalGradient P S g‖ ^ 2 ≤ ‖g‖ ^ 2 := by have hbound := effBound_le_normSq (isGradient_canonicalGradient (S := S) (g := g)) have hmem : canonicalGradient P S g ∈ tangentSpace P S := by exact efficientIF_mem g rw [effBound, efficientIF_eq_self_of_mem (tangentSpace P S) hmem] at hbound exact hbound
Causalean.Estimation.Efficiency.canonicalGradient_normSq_le · Causalean/Estimation/Efficiency/PathwiseGradient.lean:308 · uses RegularSubmodel , canonicalGradient
11 supporting declarations (lemmas, instances)
ATETangent 4 core · 12 supporting This module proves an integrable-product cancellation identity for the augmented inverse-probability weighted function and propensity-score residuals. ★ aipwProjectionNormSq_eq_hahnVariance

ATE tangent-space efficiency identities

This module proves an integrable-product cancellation identity for the augmented inverse-probability weighted function and propensity-score residuals. It also records projection properties for a separately constructed square-integrable AIPW element.

The second half builds the full mean-zero subspace Tfull, represents the AIPW score as aipwLp, proves aipwLp_mem_tangent, and derives projection-norm and variance identities. These are Hilbert-space statements about the supplied AIPW reference vector, not pathwise-gradient results under the file's finite-moment hypotheses. The final tangent-shrinking theorem gives equality of abstract bounds for any supplied smaller tangent space that still contains the AIPW score; it does not construct the known-propensity tangent space. The pathwise-gradient/canonical-gradient bridge is developed in ATEEfficientIF.lean.

def aipwLp reviewed
Causalean.Estimation.ATE.BackdoorEstimationSystem

Given a potential-outcome system with a standard-Borel sample space and finite probability measure, a measurable covariate space, a back-door estimation system, a real overlap level satisfying strict overlap, the back-door identification assumptions, an integrable squared factual outcome, and integrable squared potential outcomes under each treatment, the square-integrable AIPW influence function is the equivalence class of that influence function in the observed-data L2L^2 space.

Definition (Lean source)
P :
shared
γ :
Type u_1
shared
S :
ATE.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.μ
aipwLp S h_overlap hA h_y2 h_yd2 :
Lp ℝ 2 S.P_Z
(S.aipw_memLp h_overlap hA h_y2 h_yd2).toLp _
def oneLp reviewed
Causalean.Estimation.ATE.BackdoorEstimationSystem

Given 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 constant-one element of the observed-data L2L^2 space is the equivalence class of the function that equals one everywhere.

Definition (Lean source)
P :
shared
γ :
Type u_1
shared
S :
ATE.BackdoorEstimationSystem P γ
oneLp S :
Lp ℝ 2 S.P_Z
(memLp_const (1 : ℝ)).toLp _
Causalean.Estimation.ATE.BackdoorEstimationSystem.oneLp · Causalean/Estimation/Efficiency/ATETangent.lean:453 · uses BackdoorEstimationSystem , P_Z , POSystem
def Tfull reviewed
Causalean.Estimation.ATE.BackdoorEstimationSystem

Given 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 full mean-zero tangent space is the orthogonal complement of the constant functions in the observed-data L2L^2 space.

Definition (Lean source)
P :
shared
γ :
Type u_1
shared
S :
ATE.BackdoorEstimationSystem P γ
Tfull S :
Submodule ℝ (Lp ℝ 2 S.P_Z)
(ℝ ∙ S.oneLp)ᗮ
Causalean.Estimation.ATE.BackdoorEstimationSystem.Tfull · Causalean/Estimation/Efficiency/ATETangent.lean:458 · uses BackdoorEstimationSystem , P_Z , POSystem
theorem aipwProjectionNormSq_eq_hahnVariance reviewed
Causalean.Estimation.ATE.BackdoorEstimationSystem

The AIPW projection norm equals Hahn's three-term variance formula. Let S be a backdoor average-treatment-effect estimation system with strict overlap at level ε, satisfying the system's core identification assumptions, in which the observed outcome has finite second moment and each potential outcome under treatment level d has finite second moment. Then the projected squared norm of the AIPW reference vector equals the sum of the between-arms regression-contrast variance ∫(μ(1,X)-μ(0,X)-θ₀)²dP_X, the treated-arm weighted residual variance ∫(A/e(X)²)(Y-μ(1,X))²dP_Z, and the control-arm weighted residual variance ∫((1-A)/(1-e(X))²)(Y-μ(0,X))²dP_Z.

Formal statement
P :
shared
γ :
Type u_1
shared
S :
ATE.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.μ
effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2)
= (∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X)
+ (∫ z, (indA z / (S.e_val (projX z)) ^ 2) * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z)
+ (∫ z, ((1 - indA z) / (1 - S.e_val (projX z)) ^ 2) * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z)
Proof (Lean source)
theorem aipwProjectionNormSq_eq_hahnVariance (S : ATE.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.μ) : effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) = (∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X) + (∫ z, (indA z / (S.e_val (projX z)) ^ 2) * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z) + (∫ z, ((1 - indA z) / (1 - S.e_val (projX z)) ^ 2) * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z) := by rw [S.aipwProjectionNormSq_eq_secondMoment h_overlap hA h_y2 h_yd2, S.aipw_variance_hahn_decomposition h_overlap hA h_y2 h_yd2]
12 supporting declarations (lemmas, instances)
  • propensity_score_residual_integral_zero lemma — Any covariate-measurable multiplier has zero integral against the propensity-score residual.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    h :
    γ → ℝ
    hh_meas :
    h_int :
    Integrable (fun ω => h (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω))) P.μ
    ∫ ω, h (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω)) ∂P.μ
    = 0
    Proof (Lean source)
    lemma propensity_score_residual_integral_zero (S : ATE.BackdoorEstimationSystem P γ) (h : γ → ℝ) (hh_meas : Measurable h) (h_int : Integrable (fun ω => h (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω))) P.μ) : ∫ ω, h (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω)) ∂P.μ = 0 := by -- `h(X)` is σ(X)-measurable. have hh_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] (fun ω => h (S.toPOBackdoorSystem.factualX ω)) := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => h (S.toPOBackdoorSystem.factualX ω)) exact (hh_meas.comp (comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable -- Integrability of the residual `a − e(X)`. have hind_int : Integrable (S.toPOBackdoorSystem.dVar.indicator true) P.μ := S.toPOBackdoorSystem.dVar.integrable_indicator true (MeasurableSet.singleton true) have he_int : Integrable (fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω)) P.μ := by -- `e_val(X)` is bounded (it equals `propScore true` a.e., which is in [0,1]), -- but here we only need integrability; it is the a.e.-limit of a bounded -- conditional expectation. We get it directly from `e_compat`. have hps_int : Integrable (S.toPOBackdoorSystem.propScore true) P.μ := by unfold POBackdoorSystem.propScore exact integrable_condExp exact hps_int.congr S.e_compat have hresid_int : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω)) P.μ := hind_int.sub he_int -- `E[a − e(X) | σ(X)] = 0` a.s. have hresid_ce_zero : P.μ[fun ω => S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by have he_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] (fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω)) := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω)) exact (S.e_meas.comp (comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable -- `E[a | σ(X)] = propScore true =ᵐ e_val(X)`. have hce_ind : P.μ[S.toPOBackdoorSystem.dVar.indicator true | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω)) := by have h1 : P.μ[S.toPOBackdoorSystem.dVar.indicator true | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] S.toPOBackdoorSystem.propScore true := by unfold POBackdoorSystem.propScore exact EventuallyEq.rfl exact h1.trans S.e_compat -- `E[e(X) | σ(X)] = e(X)` since `e(X)` is σ(X)-measurable. have hce_e : P.μ[fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω)) := Filter.EventuallyEq.of_eq (condExp_of_stronglyMeasurable S.toPOBackdoorSystem.sigmaX_le he_sm he_int) have hsub : P.μ[fun ω => S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] P.μ[S.toPOBackdoorSystem.dVar.indicator true | S.toPOBackdoorSystem.sigmaX] - P.μ[fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω) | S.toPOBackdoorSystem.sigmaX] := condExp_sub hind_int he_int S.toPOBackdoorSystem.sigmaX filter_upwards [hsub, hce_ind, hce_e] with ω hsubω hindω heω rw [hsubω, Pi.sub_apply, hindω, heω, sub_self] -- Pull `h(X)` out of the conditional expectation, then use the residual = 0. have hcondexp_pull := condExp_mul_of_stronglyMeasurable_left (μ := P.μ) (m := S.toPOBackdoorSystem.sigmaX) hh_sm h_int hresid_int have hhresid_ce_zero : P.μ[fun ω => h (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω)) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by refine hcondexp_pull.trans ?_ filter_upwards [hresid_ce_zero] with ω hω have : ((fun ω' => h (S.toPOBackdoorSystem.factualX ω')) * P.μ[fun ω' => S.toPOBackdoorSystem.dVar.indicator true ω' - S.e_val (S.toPOBackdoorSystem.factualX ω') | S.toPOBackdoorSystem.sigmaX]) ω = 0 := by rw [Pi.mul_apply, hω, mul_zero] exact this calc ∫ ω, h (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω)) ∂P.μ = ∫ ω, P.μ[fun ω => h (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω)) | S.toPOBackdoorSystem.sigmaX] ω ∂P.μ := by rw [MeasureTheory.integral_condExp S.toPOBackdoorSystem.sigmaX_le] _ = ∫ _, (0 : ℝ) ∂P.μ := MeasureTheory.integral_congr_ae hhresid_ce_zero _ = 0 := MeasureTheory.integral_zero _ _
    Causalean.Estimation.Efficiency.BackdoorEstimationSystem.propensity_score_residual_integral_zero · Causalean/Estimation/Efficiency/ATETangent.lean:83
  • aipw_orthogonal_propensity_score theorem — The observed-law mean of an AIPW function times a covariate multiplier and propensity residual is zero for a backdoor ATE estimation system satisfying the backdoor assumptions and strict overlap, provided the multiplier is measurable and the three product terms are integrable.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    hA :
    S.toPOBackdoorSystem.Assumptions
    ε :
    ℝ
    h_overlap :
    S.StrictOverlap ε
    α :
    γ → ℝ
    hα_meas :
    `α(X)·(a − e(X))` is integrable (e.g. `α` bounded, or `α(X) ∈ L²`).
    h_sA_int :
    Integrable (fun ω => ((S.μ_val true (S.toPOBackdoorSystem.factualX ω) - S.μ_val false (S.toPOBackdoorSystem.factualX ω) - S.θ₀) * α (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω))) P.μ
    h_sB_int :
    Integrable (fun ω => (fun x => α x * (1 - S.e_val x) / S.e_val x) (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)))) P.μ
    h_sC_int :
    Integrable (fun ω => (fun x => α x * S.e_val x / (1 - S.e_val x)) (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)))) P.μ
    ∫ z, S.ψ_AIPW z * (α (projX z) * (indA z - S.e_val (projX z))) ∂S.P_Z = 0
    Proof (Lean source)
    theorem aipw_orthogonal_propensity_score (S : ATE.BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (α : γ → ℝ) (hα_meas : Measurable α) -- `α(X)·(a − e(X))` is integrable (e.g. `α` bounded, or `α(X) ∈ L²`). (h_sA_int : Integrable (fun ω => ((S.μ_val true (S.toPOBackdoorSystem.factualX ω) - S.μ_val false (S.toPOBackdoorSystem.factualX ω) - S.θ₀) * α (S.toPOBackdoorSystem.factualX ω)) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω))) P.μ) (h_sB_int : Integrable (fun ω => (fun x => α x * (1 - S.e_val x) / S.e_val x) (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)))) P.μ) (h_sC_int : Integrable (fun ω => (fun x => α x * S.e_val x / (1 - S.e_val x)) (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)))) P.μ) : ∫ z, S.ψ_AIPW z * (α (projX z) * (indA z - S.e_val (projX z))) ∂S.P_Z = 0 := by classical -- `h_overlap` records the overlap setting in which the propensity directions -- (and the bounded inverse-propensity weights) are well-defined. have _hε_pos : 0 < ε := h_overlap.1 -- Push the integral to `Ω`. have hmeas_integrand : Measurable (fun z : γ × Bool × ℝ => S.ψ_AIPW z * (α (projX z) * (indA z - S.e_val (projX z)))) := by have hx : Measurable (fun z : γ × Bool × ℝ => z.1) := measurable_fst have hψ : Measurable S.ψ_AIPW := S.measurable_ψ_AIPW have hα' : Measurable (fun z : γ × Bool × ℝ => α (projX z)) := hα_meas.comp hx have hind : Measurable (fun z : γ × Bool × ℝ => indA z) := by unfold indA projA exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp measurable_snd.fst have he : Measurable (fun z : γ × Bool × ℝ => S.e_val (projX z)) := S.e_meas.comp hx exact hψ.mul (hα'.mul (hind.sub he)) rw [BackdoorEstimationSystem.P_Z, MeasureTheory.integral_map S.measurable_factualZ.aemeasurable hmeas_integrand.aestronglyMeasurable] -- Ω-level abbreviations. set X : P.Ω → γ := S.toPOBackdoorSystem.factualX with hX set Y : P.Ω → ℝ := S.toPOBackdoorSystem.factualY with hY set a : P.Ω → ℝ := fun ω => indA (S.factualZ ω) with ha set e : P.Ω → ℝ := fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω) with he set μ1 : P.Ω → ℝ := fun ω => S.μ_val true (S.toPOBackdoorSystem.factualX ω) with hμ1 set μ0 : P.Ω → ℝ := fun ω => S.μ_val false (S.toPOBackdoorSystem.factualX ω) with hμ0 set Afn : P.Ω → ℝ := fun ω => μ1 ω - μ0 ω - S.θ₀ with hAfn set Bfn : P.Ω → ℝ := fun ω => (a ω / e ω) * (Y ω - μ1 ω) with hBfn set Cfn : P.Ω → ℝ := fun ω => ((1 - a ω) / (1 - e ω)) * (Y ω - μ0 ω) with hCfn -- `a ω ∈ {0, 1}` and the indicator identities. have ha01 : ∀ ω, a ω = 0 ∨ a ω = 1 := by intro ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · right; simp [ha, indA, projA, ATE.BackdoorEstimationSystem.factualZ, hD] · left; simp [ha, indA, projA, ATE.BackdoorEstimationSystem.factualZ, hD] have ha_ind : ∀ ω, a ω = 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 [ha, indA, projA, ATE.BackdoorEstimationSystem.factualZ, hD, hInd] · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [ha, indA, projA, ATE.BackdoorEstimationSystem.factualZ, hD, hInd] have hna_ind : ∀ ω, 1 - a ω = 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 ω rw [ha_ind ω]; linarith -- Strict positivity of the propensity weights (from overlap). have he_pos : ∀ ω, 0 < e ω := fun ω => S.e_pos _ have he_lt_one : ∀ ω, e ω < 1 := fun ω => S.e_lt_one _ -- Pointwise: `ψ_AIPW(factualZ ω) · s_e(factualZ ω)` -- = Afn·α(X)·(a−e) + sB-residual + sC-residual, -- where the sB / sC residuals match `weighted_residual_integral_zero`. set sA : P.Ω → ℝ := fun ω => (Afn ω * α (X ω)) * (S.toPOBackdoorSystem.dVar.indicator true ω - e ω) with hsA set sB : P.Ω → ℝ := fun ω => (fun x => α x * (1 - S.e_val x) / S.e_val x) (X ω) * (S.toPOBackdoorSystem.dVar.indicator true ω * (Y ω - μ1 ω)) with hsB set sC : P.Ω → ℝ := fun ω => (fun x => α x * S.e_val x / (1 - S.e_val x)) (X ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (Y ω - μ0 ω)) with hsC have hpt : ∀ ω, S.ψ_AIPW (S.factualZ ω) * (α (projX (S.factualZ ω)) * (indA (S.factualZ ω) - S.e_val (projX (S.factualZ ω)))) = sA ω + sB ω + sC ω := by intro ω -- `ψ_AIPW(factualZ ω) = Afn ω + Bfn ω − Cfn ω`. have hexpand : S.ψ_AIPW (S.factualZ ω) = Afn ω + Bfn ω - Cfn ω := by unfold ATE.BackdoorEstimationSystem.ψ_AIPW ATE.BackdoorEstimationSystem.aipwMoment simp only [ATE.BackdoorEstimationSystem.factualZ, projX, projY, hBfn, hCfn, ha, he, hμ1, hμ0, hY] ring -- The propensity-direction factor at `factualZ ω`. have hfac : α (projX (S.factualZ ω)) * (indA (S.factualZ ω) - S.e_val (projX (S.factualZ ω))) = α (X ω) * (a ω - e ω) := by simp only [ATE.BackdoorEstimationSystem.factualZ, projX, ha, he, hX] rw [hexpand, hfac] -- Now expand using `a ∈ {0,1}` to collapse the products. have haind := ha_ind ω have hnaind := hna_ind ω have hepos := (he_pos ω).ne' have hediff : (1 - e ω) ≠ 0 := by have := he_lt_one ω; linarith simp only [hsA, hsB, hsC, hAfn, hBfn, hCfn, hμ1, hμ0, hY, he, hX] rcases ha01 ω with h0 | h1 · -- `a ω = 0`: then `1_{D=true} = 0`, `1_{D=false} = 1`. have hi_t : S.toPOBackdoorSystem.dVar.indicator true ω = 0 := by rw [← haind, h0] have hi_f : S.toPOBackdoorSystem.dVar.indicator false ω = 1 := by rw [← hnaind, h0]; ring rw [hi_t, hi_f, h0] field_simp ring · -- `a ω = 1`: then `1_{D=true} = 1`, `1_{D=false} = 0`. have hi_t : S.toPOBackdoorSystem.dVar.indicator true ω = 1 := by rw [← haind, h1] have hi_f : S.toPOBackdoorSystem.dVar.indicator false ω = 0 := by rw [← hnaind, h1]; ring rw [hi_t, hi_f, h1] simp only [zero_mul, mul_zero, one_mul] field_simp ring -- Rewrite the integral via the pointwise identity. rw [MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall hpt)] -- Integrability of the three pieces (from the threaded hypotheses). have hsA_int : Integrable sA P.μ := by refine h_sA_int.congr (Filter.Eventually.of_forall (fun ω => ?_)) simp only [hsA, hAfn, hμ1, hμ0, hX] have hsB_int : Integrable sB P.μ := h_sB_int have hsC_int : Integrable sC P.μ := h_sC_int -- Split the integral. rw [MeasureTheory.integral_add (f := fun ω => sA ω + sB ω) (g := sC) (hsA_int.add hsB_int) hsC_int, MeasureTheory.integral_add (f := sA) (g := sB) hsA_int hsB_int] -- The three integrals each vanish. have hA_zero : ∫ ω, sA ω ∂P.μ = 0 := by have hh_meas : Measurable (fun x => (S.μ_val true x - S.μ_val false x - S.θ₀) * α x) := (((S.μ_meas true).sub (S.μ_meas false)).sub measurable_const).mul hα_meas have hsA_eq : ∀ ω, sA ω = (fun x => (S.μ_val true x - S.μ_val false x - S.θ₀) * α x) (X ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω)) := by intro ω simp only [hsA, hAfn, hμ1, hμ0, he, hX] rw [MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall hsA_eq)] refine propensity_score_residual_integral_zero S _ hh_meas ?_ refine (h_sA_int.congr (Filter.Eventually.of_forall (fun ω => ?_))) simp only [] ring have hB_zero : ∫ ω, sB ω ∂P.μ = 0 := by have hg_meas : Measurable (fun x => α x * (1 - S.e_val x) / S.e_val x) := (hα_meas.mul (measurable_const.sub S.e_meas)).div S.e_meas exact S.weighted_residual_integral_zero hA true (fun x => α x * (1 - S.e_val x) / S.e_val x) hg_meas hsB_int (S.cond_exp_residual_zero hA true) have hC_zero : ∫ ω, sC ω ∂P.μ = 0 := by have hg_meas : Measurable (fun x => α x * S.e_val x / (1 - S.e_val x)) := (hα_meas.mul S.e_meas).div (measurable_const.sub S.e_meas) exact S.weighted_residual_integral_zero hA false (fun x => α x * S.e_val x / (1 - S.e_val x)) hg_meas hsC_int (S.cond_exp_residual_zero hA false) rw [hA_zero, hB_zero, hC_zero] ring
    Causalean.Estimation.Efficiency.BackdoorEstimationSystem.aipw_orthogonal_propensity_score · Causalean/Estimation/Efficiency/ATETangent.lean:197
  • instIsProbabilityMeasure_P_Z instance — For a potential-outcome system with a standard-Borel sample space and finite population measure, a measurable covariate space, and a back-door estimation system, the system's observed-data law is a probability measure.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    instIsProbabilityMeasure_P_Z S :
    by rw [ATE.BackdoorEstimationSystem.P_Z] haveI : IsProbabilityMeasure P.μ := P.isProb exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable
    Causalean.Estimation.ATE.BackdoorEstimationSystem.instIsProbabilityMeasure_P_Z · Causalean/Estimation/Efficiency/ATETangent.lean:425
  • aipw_memLp theorem — The AIPW influence function is square-integrable under the observed data law.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.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.μ
    MemLp S.ψ_AIPW 2 S.P_Z
    Proof (Lean source)
    theorem aipw_memLp (S : ATE.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.μ) : MemLp S.ψ_AIPW 2 S.P_Z := (memLp_two_iff_integrable_sq S.measurable_ψ_AIPW.aestronglyMeasurable).2 (S.aipw_finite_var_of_counterfactual_sq h_overlap hA h_y2 h_yd2)
    Causalean.Estimation.ATE.BackdoorEstimationSystem.aipw_memLp · Causalean/Estimation/Efficiency/ATETangent.lean:432
  • instHasOrthogonalProjection_span_oneLp instance — For a potential-outcome system with a standard-Borel sample space and finite population measure, a measurable covariate space, and a back-door estimation system, the one-dimensional subspace spanned by the constant-one observed-data function admits an orthogonal projection.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    instHasOrthogonalProjection_span_oneLp S :
    (ℝ ∙ S.oneLp).HasOrthogonalProjection
    by have : FiniteDimensional ℝ (ℝ ∙ S.oneLp) := inferInstance exact inferInstance
    Causalean.Estimation.ATE.BackdoorEstimationSystem.instHasOrthogonalProjection_span_oneLp · Causalean/Estimation/Efficiency/ATETangent.lean:463
  • instHasOrthogonalProjection_Tfull instance — For a potential-outcome system with a standard-Borel sample space and finite population measure, a measurable covariate space, and a back-door estimation system, the full mean-zero tangent space admits an orthogonal projection.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    instHasOrthogonalProjection_Tfull S :
    by rw [Tfull] exact Submodule.instHasOrthogonalProjectionOrthogonal (ℝ ∙ S.oneLp)
    Causalean.Estimation.ATE.BackdoorEstimationSystem.instHasOrthogonalProjection_Tfull · Causalean/Estimation/Efficiency/ATETangent.lean:470
  • inner_oneLp theorem — Inner product against the constant-one function equals integration under the observed data law.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    f :
    Lp ℝ 2 S.P_Z
    ⟪f, S.oneLp⟫_ℝ = ∫ z, f z ∂S.P_Z
    Proof (Lean source)
    theorem inner_oneLp (S : ATE.BackdoorEstimationSystem P γ) (f : Lp ℝ 2 S.P_Z) : ⟪f, S.oneLp⟫_ℝ = ∫ z, f z ∂S.P_Z := by rw [inner_eq_integral] refine MeasureTheory.integral_congr_ae ?_ filter_upwards [(memLp_const (1 : ℝ)).coeFn_toLp (p := 2) (μ := S.P_Z)] with z hz rw [show S.oneLp z = (1 : ℝ) from hz, mul_one]
    Causalean.Estimation.ATE.BackdoorEstimationSystem.inner_oneLp · Causalean/Estimation/Efficiency/ATETangent.lean:477
  • aipwLp_mem_tangent theorem — The AIPW influence function lies in the mean-zero tangent space.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.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.μ
    S.aipwLp h_overlap hA h_y2 h_yd2 ∈ S.Tfull
    Proof (Lean source)
    theorem aipwLp_mem_tangent (S : ATE.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.μ) : S.aipwLp h_overlap hA h_y2 h_yd2 ∈ S.Tfull := by rw [Tfull, Submodule.mem_orthogonal_singleton_iff_inner_left, S.inner_oneLp] have hae : (S.aipwLp h_overlap hA h_y2 h_yd2 : γ × Bool × ℝ → ℝ) =ᵐ[S.P_Z] S.ψ_AIPW := (S.aipw_memLp h_overlap hA h_y2 h_yd2).coeFn_toLp rw [MeasureTheory.integral_congr_ae hae] exact S.aipw_mean_zero_of_square_integrable h_overlap hA h_y2 h_yd2
    Causalean.Estimation.ATE.BackdoorEstimationSystem.aipwLp_mem_tangent · Causalean/Estimation/Efficiency/ATETangent.lean:486
  • aipw_score_meanZero_projection_eq theorem — The square-integrable AIPW score is already mean-zero, so projecting it onto the full mean-zero tangent space leaves it unchanged.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.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.μ
    efficientIF S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) = S.aipwLp h_overlap hA h_y2 h_yd2
    Proof (Lean source)
    theorem aipw_score_meanZero_projection_eq (S : ATE.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.μ) : efficientIF S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) = S.aipwLp h_overlap hA h_y2 h_yd2 := efficientIF_eq_self_of_mem S.Tfull (S.aipwLp_mem_tangent h_overlap hA h_y2 h_yd2)
    Causalean.Estimation.ATE.BackdoorEstimationSystem.aipw_score_meanZero_projection_eq · Causalean/Estimation/Efficiency/ATETangent.lean:506
  • aipwProjectionNormSq_eq_secondMoment theorem — The AIPW projection norm equals its second moment. Let S be a backdoor average-treatment-effect estimation system with strict overlap at level ε, satisfying the system's core identification assumptions, in which the observed outcome has finite second moment and each potential outcome under treatment level d has finite second moment. Then the squared norm obtained by projecting the AIPW reference vector onto the full mean-zero subspace equals the second moment of ψ_AIPW under the observed-data law P_Z.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.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.μ
    effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) = ∫ z, (S.ψ_AIPW z) ^ 2 ∂S.P_Z
    Proof (Lean source)
    theorem aipwProjectionNormSq_eq_secondMoment (S : ATE.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.μ) : effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) = ∫ z, (S.ψ_AIPW z) ^ 2 ∂S.P_Z := by rw [effBound, S.aipw_score_meanZero_projection_eq h_overlap hA h_y2 h_yd2, ← real_inner_self_eq_norm_sq, inner_eq_integral] refine MeasureTheory.integral_congr_ae ?_ have hae : (S.aipwLp h_overlap hA h_y2 h_yd2 : γ × Bool × ℝ → ℝ) =ᵐ[S.P_Z] S.ψ_AIPW := (S.aipw_memLp h_overlap hA h_y2 h_yd2).coeFn_toLp filter_upwards [hae] with z hz rw [hz, sq]
    Causalean.Estimation.ATE.BackdoorEstimationSystem.aipwProjectionNormSq_eq_secondMoment · Causalean/Estimation/Efficiency/ATETangent.lean:524
  • aipwProjectionNormSq_le_normSq theorem — The AIPW projection norm lower-bounds every relative gradient's squared norm. Let S be a backdoor average-treatment-effect estimation system with strict overlap at level ε, satisfying the system's core identification assumptions, in which the observed outcome has finite second moment and each potential outcome under treatment level d has finite second moment. If ψ is a square-integrable element of L²(P_Z) that is a gradient for the AIPW influence function relative to the full mean-zero tangent space, then the projected AIPW squared norm is at most the squared L² norm of ψ.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.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.μ
    ψ :
    Lp ℝ 2 S.P_Z
    hψ :
    IsGradient S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) ψ
    effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) ≤ ‖ψ‖ ^ 2
    Proof (Lean source)
    theorem aipwProjectionNormSq_le_normSq (S : ATE.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.μ) (ψ : Lp ℝ 2 S.P_Z) (hψ : IsGradient S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) ψ) : effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) ≤ ‖ψ‖ ^ 2 := effBound_le_normSq hψ
    Causalean.Estimation.ATE.BackdoorEstimationSystem.aipwProjectionNormSq_le_normSq · Causalean/Estimation/Efficiency/ATETangent.lean:581
  • effBound_eq_of_smaller_tangent_containing_aipw theorem — For any supplied smaller tangent space that is contained in the mean-zero tangent space and still contains the AIPW score, the abstract squared-norm efficiency bound is unchanged.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.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.μ
    T' :
    Submodule ℝ (Lp ℝ 2 S.P_Z)
    T'.HasOrthogonalProjection
    hle :
    T' ≤ S.Tfull
    hmem :
    S.aipwLp h_overlap hA h_y2 h_yd2 ∈ T'
    effBound T' (S.aipwLp h_overlap hA h_y2 h_yd2)
    = effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2)
    Proof (Lean source)
    -- TODO(faithfulness): Hahn/standard semiparametric efficiency theory — define the -- known-propensity tangent space and derive AIPW membership from propensity-score -- orthogonality, instead of assuming an arbitrary smaller tangent space containing AIPW. theorem effBound_eq_of_smaller_tangent_containing_aipw (S : ATE.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.μ) (T' : Submodule ℝ (Lp ℝ 2 S.P_Z)) [T'.HasOrthogonalProjection] (hle : T' ≤ S.Tfull) (hmem : S.aipwLp h_overlap hA h_y2 h_yd2 ∈ T') : effBound T' (S.aipwLp h_overlap hA h_y2 h_yd2) = effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) := (effBound_eq_of_mem_sub S.Tfull T' hle hmem).2.2
    Causalean.Estimation.ATE.BackdoorEstimationSystem.effBound_eq_of_smaller_tangent_containing_aipw · Causalean/Estimation/Efficiency/ATETangent.lean:608
Tilt­Tangent 7 core · 12 supporting This module realizes every bounded measurable mean-zero function as the score of the normalized exponential tilt through a probability law. ★ tangentSpace_boundedTiltSubmodels_eq_meanZeroLp★ isEfficientInfluenceFunction_of_hasDerivAt_tilt'★ mean_isEfficientInfluenceFunction

Bounded exponential tilts generate the nonparametric tangent space

This module realizes every bounded measurable mean-zero function as the score of the normalized exponential tilt through a probability law. It proves the derivative of tilted expectations, proves the DQM square-root-density expansion, shows that the closed linear span of these tilt scores is all of L²₀, and identifies the generated tangent space with that mean-zero subspace. The final specialization identifies this space with the ATE layer's Tfull. The regular submodel construction plays the score-realization role of van der Vaart (1998), Example 25.16, using normalized exponential tilts instead of its bounded-link paths; the later tangent-space and efficient-influence-function results are proved separately here.

def tiltScoreSet reviewed
Causalean.Estimation.Efficiency

For a probability law P, the bounded exponential-tilt score set consists of L² classes that have an everywhere measurable, everywhere bounded, mean-zero representative whose L² class is the specified vector.

Definition (Lean source)
Z :
Type u_1
shared
tiltScoreSet P :
Set (Lp ℝ 2 P)
{f | ∃ (g : Z → ℝ) (M : ℝ) (hg : MemLp g 2 P), Measurable g ∧ (∀ z, |g z| ≤ M) ∧ (∫ z, g z ∂P) = 0 ∧ hg.toLp g = f}
Causalean.Estimation.Efficiency.tiltScoreSet · Causalean/Estimation/Efficiency/TiltTangent.lean:40
def expHalfLp reviewed
Causalean.Estimation.Efficiency

Given a probability law P, a measurable function g bounded in absolute value by M, and a perturbation t, the L² exponential half-density is represented by z ↦ exp(t g(z)/2).

Definition (Lean source)
Z :
Type u_1
shared
g :
Z → ℝ
M :
ℝ
hg_meas :
hgM :
∀ z, |g z| ≤ M
t :
ℝ
expHalfLp P g M hg_meas hgM t :
Lp ℝ 2 P
(MemLp.of_bound ((hg_meas.const_mul t).div_const 2 |>.exp.aestronglyMeasurable) (exp (|t| * |M|)) (ae_of_all _ fun z => by rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] apply Real.exp_le_exp.mpr calc t * g z / 2 ≤ |t * g z / 2| := le_abs_self _ _ ≤ |t| * |M| := by rw [abs_div, abs_mul] have hgM' : |g z| ≤ |M| := (hgM z).trans (le_abs_self M) nlinarith [abs_nonneg t, abs_nonneg M] )).toLp (fun z => exp (t * g z / 2))
Causalean.Estimation.Efficiency.expHalfLp · Causalean/Estimation/Efficiency/TiltTangent.lean:47
def tiltRegularSubmodel reviewed
Causalean.Estimation.Efficiency

The normalized exponential tilt is a regular submodel with the prescribed square-integrable score for a probability law and a measurable score that is bounded, mean zero, and square-integrable.

Definition (Lean source)
Z :
Type u_1
shared
g :
Z → ℝ
M :
ℝ
hg_meas :
hgM :
∀ z, |g z| ≤ M
hg_mean :
∫ z, g z ∂P = 0
hg :
MemLp g 2 P
tiltRegularSubmodel P g M hg_meas hgM hg_mean hg :
clause 1
path := fun t => tiltMeasure P g t
clause 2
path_probability := fun t => isProbabilityMeasure_tiltMeasure hg_meas hgM
clause 3
path_zero := by simp
clause 4
path_ac := fun t
=> by rw [tiltMeasure_eq_withDensity_div P g M t hg_meas hgM] exact withDensity_absolutelyContinuous _ _
clause 5
score := hg.toLp g
clause 6
score_meanZero := by rw [meanZeroLp, Submodule.mem_orthogonal_singleton_iff_inner_left, inner_lpOne_eq_integral] rw [integral_congr_ae hg.coeFn_toLp] exact hg_mean
clause 7
dqm := by have hd := hasDerivAt_rnSqrtDensityLp_tiltMeasure P g M hg_meas hgM hg_mean hg have hslope := hd.tendsto_slope_zero simpa [dqmQuotient, tiltMeasure_zero] using hslope
Causalean.Estimation.Efficiency.tiltRegularSubmodel · Causalean/Estimation/Efficiency/TiltTangent.lean:258 · uses RegularSubmodel
def boundedTiltSubmodels reviewed
Causalean.Estimation.Efficiency

For a probability law P, the bounded exponential-tilt submodel family consists exactly of the regular submodels constructed from measurable bounded mean-zero scores.

Definition (Lean source)
Z :
Type u_1
shared
boundedTiltSubmodels P :
{m | ∃ (g : Z → ℝ) (M : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hg_mean : ∫ z, g z ∂P = 0) (hg : MemLp g 2 P), m = tiltRegularSubmodel P g M hg_meas hgM hg_mean hg}
Causalean.Estimation.Efficiency.boundedTiltSubmodels · Causalean/Estimation/Efficiency/TiltTangent.lean:287 · uses RegularSubmodel
theorem tangentSpace_boundedTiltSubmodels_eq_meanZeroLp reviewed
Causalean.Estimation.Efficiency

For a probability law P, the tangent space generated by bounded exponential tilts is all of L²₀(P).

Formal statement
Z :
Type u_1
shared
tangentSpace P (boundedTiltSubmodels P) = meanZeroLp P
Proof (Lean source)
Causalean.Estimation.Efficiency.tangentSpace_boundedTiltSubmodels_eq_meanZeroLp · Causalean/Estimation/Efficiency/TiltTangent.lean:365 · uses boundedTiltSubmodels , tangentSpace , meanZeroLp
theorem isEfficientInfluenceFunction_of_hasDerivAt_tilt' reviewed
Causalean.Estimation.Efficiency

The square-integrable class represented by a candidate function is the efficient influence function of a law functional in the nonparametric bounded-tilt model when the underlying law is a probability law, the functional is real-valued, the candidate is square-integrable with mean zero, and its pairing with every measurable bounded mean-zero exponential-tilt score gives the functional's derivative along that tilt.

Formal statement
Z :
Type u_1
shared
ψ :
Measure Z → ℝ
φ :
Z → ℝ
hφ :
MemLp φ 2 P
hφ_mean :
∫ z, φ z ∂P = 0
hderiv :
∀ (g : Z → ℝ) (M : ℝ)
and
(∀ z, |g z| ≤ M)
and
(∫ z, g z ∂P) = 0
then
HasDerivAt (fun t => ψ (tiltMeasure P g t)) (∫ z, φ z * g z ∂P) 0
Proof (Lean source)
theorem isEfficientInfluenceFunction_of_hasDerivAt_tilt' (P : Measure Z) [IsProbabilityMeasure P] (ψ : Measure Z → ℝ) (φ : Z → ℝ) (hφ : MemLp φ 2 P) (hφ_mean : ∫ z, φ z ∂P = 0) (hderiv : ∀ (g : Z → ℝ) (M : ℝ), Measurable g → (∀ z, |g z| ≤ M) → (∫ z, g z ∂P) = 0 → HasDerivAt (fun t => ψ (tiltMeasure P g t)) (∫ z, φ z * g z ∂P) 0) : IsEfficientInfluenceFunction P ψ (hφ.toLp φ) (boundedTiltSubmodels P) := by have hφ0 : hφ.toLp φ ∈ meanZeroLp P := by rw [meanZeroLp, Submodule.mem_orthogonal_singleton_iff_inner_left, inner_lpOne_eq_integral, integral_congr_ae hφ.coeFn_toLp] exact hφ_mean apply isEfficientInfluenceFunction_of_hasDerivAt_tilt P ψ (hφ.toLp φ) hφ0 intro g M hg hg_meas hgM hg_mean have hcoef : ⟪hφ.toLp φ, hg.toLp g⟫_ℝ = ∫ z, φ z * g z ∂P := by rw [inner_eq_integral] apply integral_congr_ae filter_upwards [hφ.coeFn_toLp, hg.coeFn_toLp] with z hφz hgz rw [hφz, hgz] rw [hcoef] exact hderiv g M hg_meas hgM hg_mean
Causalean.Estimation.Efficiency.isEfficientInfluenceFunction_of_hasDerivAt_tilt' · Causalean/Estimation/Efficiency/TiltTangent.lean:418 · uses IsEfficientInfluenceFunction , boundedTiltSubmodels , tiltMeasure
theorem mean_isEfficientInfluenceFunction reviewed
Causalean.Estimation.Efficiency

The centered outcome is the efficient influence function of the mean functional in the nonparametric bounded-tilt model whenever a probability law on the real line has a square-integrable identity variable.

Formal statement
hY :
MemLp (fun y : ℝ => y) 2 P
IsEfficientInfluenceFunction P (fun Q => ∫ y, y ∂Q) ((hY.sub (memLp_const (∫ y, y ∂P))).toLp (fun y => y - ∫ x, x ∂P)) (boundedTiltSubmodels P)
Proof (Lean source)
theorem mean_isEfficientInfluenceFunction (P : Measure ℝ) [IsProbabilityMeasure P] (hY : MemLp (fun y : ℝ => y) 2 P) : IsEfficientInfluenceFunction P (fun Q => ∫ y, y ∂Q) ((hY.sub (memLp_const (∫ y, y ∂P))).toLp (fun y => y - ∫ x, x ∂P)) (boundedTiltSubmodels P) := by let μ : ℝ := ∫ y, y ∂P have hcenter : MemLp (fun y : ℝ => y - μ) 2 P := hY.sub (memLp_const μ) apply isEfficientInfluenceFunction_of_hasDerivAt_tilt' P (fun Q => ∫ y, y ∂Q) (fun y => y - μ) hcenter · rw [integral_sub (hY.integrable (by norm_num)) (integrable_const μ), integral_const, probReal_univ, one_smul] dsimp [μ] ring · intro g M hg_meas hgM hg_mean have hg : MemLp g 2 P := MemLp.of_bound hg_meas.aestronglyMeasurable M (ae_of_all _ fun z => by simpa [Real.norm_eq_abs] using hgM z) have hg_int : Integrable g P := hg.integrable (by norm_num) have hYg : Integrable (fun y : ℝ => y * g y) P := by have h := (hY.integrable (by norm_num)).bdd_mul hg_meas.aestronglyMeasurable (ae_of_all _ fun z => by simpa [Real.norm_eq_abs] using hgM z) exact h.congr (ae_of_all _ fun z => by ring) have hμg : Integrable (fun y : ℝ => μ * g y) P := hg_int.const_mul μ have hcoef : (∫ y, (y - μ) * g y ∂P) = ∫ y, y * g y ∂P := by calc (∫ y, (y - μ) * g y ∂P) = ∫ y, y * g y - μ * g y ∂P := by apply integral_congr_ae filter_upwards with y ring _ = (∫ y, y * g y ∂P) - ∫ y, μ * g y ∂P := integral_sub hYg hμg _ = ∫ y, y * g y ∂P := by rw [integral_const_mul, hg_mean, mul_zero, sub_zero] rw [hcoef] exact hasDerivAt_integral_tiltMeasure_of_memLp hg_meas hgM hg_mean hY
Causalean.Estimation.Efficiency.mean_isEfficientInfluenceFunction · Causalean/Estimation/Efficiency/TiltTangent.lean:450 · uses IsEfficientInfluenceFunction , boundedTiltSubmodels
12 supporting declarations (lemmas, instances)
Arm­Mean­Efficient­IF 1 core · 9 supporting For an observed law on (X,D,Y), this module studies the arm functional ψ_d(P)=E_P[μ_d(X)]. ★ observedArmEIF_isEfficientInfluenceFunction

Efficient influence function for a treatment-specific mean

For an observed law on (X,D,Y), this module studies the arm functional ψ_d(P)=E_P[μ_d(X)]. It proves its exact doubly robust expansion, an explicit quadratic remainder along bounded exponential tilts, and the standard efficient influence function

1{D=d}(Y-μ_d(X))/e_d(X) + μ_d(X) - ψ_d(P).

The average-treatment-effect result is obtained downstream by subtracting the two arm derivatives. Reference: Kennedy (2024), Semiparametric doubly robust targeted double machine learning: a review.

theorem observedArmEIF_isEfficientInfluenceFunction reviewed
Causalean.Estimation.Efficiency

Treatment-specific-mean bounded-tilt EIF (Kennedy (2024)). Given a probability observed-data law P, an arm d, a nonnegative outcome bound B, a positive overlap level ε, bounded outcomes, and strict arm overlap, the usual inverse- propensity residual plus centered arm regression is efficient for the arm mean relative to the bounded-tilt submodel class, whose tangent space is the full nonparametric L²₀(P) space.

Formal statement
γ :
Type u_1
shared
P :
d :
B ε :
ℝ
hB :
0 ≤ B
hε :
0 < ε
hY :
∀ᵐ z ∂P, |projY z| ≤ B
hoverlap :
∀ᵐ z ∂P, ε ≤ observedPropensity P d z
IsEfficientInfluenceFunction P (fun Q => observedArmMean Q d) ((memLp_observedArmEIF P d B ε hB hε hY hoverlap).toLp (observedArmEIF P d)) (boundedTiltSubmodels P)
Proof (Lean source)
theorem observedArmEIF_isEfficientInfluenceFunction (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (d : Bool) (B ε : ℝ) (hB : 0 ≤ B) (hε : 0 < ε) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hoverlap : ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) : IsEfficientInfluenceFunction P (fun Q => observedArmMean Q d) ((memLp_observedArmEIF P d B ε hB hε hY hoverlap).toLp (observedArmEIF P d)) (boundedTiltSubmodels P) := by let hφ := memLp_observedArmEIF P d B ε hB hε hY hoverlap apply isEfficientInfluenceFunction_of_hasDerivAt_tilt' P (fun Q => observedArmMean Q d) (observedArmEIF P d) hφ (integral_observedArmEIF_eq_zero P d B ε hB hε hY hoverlap) intro g M hg_meas hgM hg_mean exact hasDerivAt_observedArmMean_tilt P d g |M| B ε hg_meas (fun z => (hgM z).trans (le_abs_self M)) hg_mean (abs_nonneg M) hB hε hY hoverlap
9 supporting declarations (lemmas, instances)
ATEEfficient­IF 2 core · 3 supporting This module proves that the AIPW function is an efficient influence function for the observed-law ATE relative to bounded exponential tilts. ★ observedAIPW_isEfficientInfluenceFunction_ATE★ aipw_is_efficientInfluenceFunction_ATE

AIPW as the efficient influence function for the observed-law ATE

This module proves that the AIPW function is an efficient influence function for the observed-law ATE relative to bounded exponential tilts. The result assumes bounded outcomes and strict overlap, and a backdoor estimation system inherits it by transporting those observed-law conditions. The AIPW target is motivated by Hahn (1998), but these bounded-tilt results are not a formalization of Hahn's Theorem 1.

theorem observedAIPW_isEfficientInfluenceFunction_ATE reviewed
Causalean.Estimation.Efficiency

The recomputed AIPW function is efficient for the observed-law ATE relative to the bounded-tilt submodel class when the observed law of covariates, treatment, and outcome has outcomes bounded by a nonnegative constant and strict overlap in both arms at a positive level. This class generates the full nonparametric mean-zero square-integrable tangent space.

Formal statement
γ :
Type u_1
shared
P :
B ε :
ℝ
hB :
0 ≤ B
hε :
0 < ε
hY :
∀ᵐ z ∂P, |projY z| ≤ B
hoverlap :
∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d z
Proof (Lean source)
theorem observedAIPW_isEfficientInfluenceFunction_ATE (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (B ε : ℝ) (hB : 0 ≤ B) (hε : 0 < ε) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hoverlap : ∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) : IsEfficientInfluenceFunction P observedATE ((memLp_observedAIPW P B ε hB hε hY hoverlap).toLp (observedAIPW P)) (boundedTiltSubmodels P) := by let hφ := memLp_observedAIPW P B ε hB hε hY hoverlap apply isEfficientInfluenceFunction_of_hasDerivAt_tilt' P observedATE (observedAIPW P) hφ (integral_observedAIPW_eq_zero P B ε hB hε hY hoverlap) intro g M hg_meas hgM hg_mean exact hasDerivAt_observedATE_tilt P g |M| B ε hg_meas (fun z => (hgM z).trans (le_abs_self M)) hg_mean (abs_nonneg M) hB hε hY hoverlap
theorem aipw_is_efficientInfluenceFunction_ATE reviewed
Causalean.Estimation.ATE.BackdoorEstimationSystem

The observed-law AIPW function is efficient for the observed-law ATE relative to the bounded-tilt submodel class for a backdoor ATE estimation system satisfying strict overlap at a positive level and factual outcomes bounded by a nonnegative constant. No separate factual- or potential-outcome second-moment premise is required.

Formal statement
P :
shared
γ :
Type u_1
shared
S :
ATE.BackdoorEstimationSystem P γ
ε B :
ℝ
h_overlap :
S.StrictOverlap ε
hB :
0 ≤ B
hY_bound :
∀ ω, |S.toPOBackdoorSystem.factualY ω| ≤ B
IsEfficientInfluenceFunction S.P_Z observedATE ((S.observedAIPW_memLp_of_bounded h_overlap hB hY_bound).toLp (observedAIPW S.P_Z)) (boundedTiltSubmodels S.P_Z)
Proof (Lean source)
theorem aipw_is_efficientInfluenceFunction_ATE (S : ATE.BackdoorEstimationSystem P γ) {ε B : ℝ} (h_overlap : S.StrictOverlap ε) (hB : 0 ≤ B) (hY_bound : ∀ ω, |S.toPOBackdoorSystem.factualY ω| ≤ B) : IsEfficientInfluenceFunction S.P_Z observedATE ((S.observedAIPW_memLp_of_bounded h_overlap hB hY_bound).toLp (observedAIPW S.P_Z)) (boundedTiltSubmodels S.P_Z) := by exact observedAIPW_isEfficientInfluenceFunction_ATE S.P_Z B ε hB h_overlap.1 (S.observedOutcome_bounded B hY_bound) (S.observedPropensity_overlap h_overlap)
3 supporting declarations (lemmas, instances)
  • observedOutcome_bounded lemma — Given a backdoor estimation system S and a factual-outcome bound B, the induced observed outcome is bounded by B almost everywhere.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    B :
    ℝ
    hY_bound :
    ∀ ω, |S.toPOBackdoorSystem.factualY ω| ≤ B
    ∀ᵐ z ∂S.P_Z, |projY z| ≤ B
    Proof (Lean source)
    lemma observedOutcome_bounded (S : ATE.BackdoorEstimationSystem P γ) (B : ℝ) (hY_bound : ∀ ω, |S.toPOBackdoorSystem.factualY ω| ≤ B) : ∀ᵐ z ∂S.P_Z, |projY z| ≤ B := by rw [S.P_Z_eq] apply (ae_map_iff S.measurable_factualZ.aemeasurable ?_).2 · filter_upwards with ω simpa [ATE.BackdoorEstimationSystem.factualZ, projY] using hY_bound ω · exact measurableSet_Iic.preimage ((measurable_snd.snd : Measurable (fun z : γ × Bool × ℝ => z.2.2)).abs)
    Causalean.Estimation.ATE.BackdoorEstimationSystem.observedOutcome_bounded · Causalean/Estimation/Efficiency/ATEEfficientIF.lean:69
  • observedPropensity_overlap lemma — Given a backdoor estimation system S and strict overlap at level ε, the induced observed law has overlap at level ε in both arms.
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    ε :
    ℝ
    h_overlap :
    S.StrictOverlap ε
    d :
    ∀ᵐ z ∂S.P_Z, ε ≤ observedPropensity S.P_Z d z
    Proof (Lean source)
    lemma observedPropensity_overlap (S : ATE.BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) : ∀ d, ∀ᵐ z ∂S.P_Z, ε ≤ observedPropensity S.P_Z d z := by have heZ : ∀ᵐ z ∂S.P_Z, ε ≤ S.e_val (projX z) ∧ S.e_val (projX z) ≤ 1 - ε := by have heΩ : ∀ᵐ ω ∂P.μ, ε ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) ∧ S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by filter_upwards [h_overlap.2.2, S.e_compat] with ω hover hcomp simpa [hcomp] using hover have hset : MeasurableSet {z : γ × Bool × ℝ | ε ≤ S.e_val (projX z) ∧ S.e_val (projX z) ≤ 1 - ε} := by exact measurableSet_Icc.preimage (S.e_meas.comp measurable_fst) rw [S.P_Z_eq] apply (ae_map_iff S.measurable_factualZ.aemeasurable hset).2 filter_upwards [heΩ] with ω hω simpa [ATE.BackdoorEstimationSystem.factualZ, projX] using hω intro d have hp := observedPropensity_P_Z_ae S d cases d · filter_upwards [hp, heZ] with z hpz hez rw [hpz] simp only [e_val_label, Bool.false_eq_true, ↓reduceIte] linarith [hez.2] · filter_upwards [hp, heZ] with z hpz hez rw [hpz] simpa [e_val_label] using hez.1
    Causalean.Estimation.ATE.BackdoorEstimationSystem.observedPropensity_overlap · Causalean/Estimation/Efficiency/ATEEfficientIF.lean:83
  • observedAIPW_memLp_of_bounded theorem — Given a backdoor estimation system S, strict overlap at level ε, a nonnegative outcome bound B, and bounded factual outcomes, the observed-law AIPW function belongs to L².
    P :
    shared
    γ :
    Type u_1
    shared
    S :
    ATE.BackdoorEstimationSystem P γ
    ε B :
    ℝ
    h_overlap :
    S.StrictOverlap ε
    hB :
    0 ≤ B
    hY_bound :
    ∀ ω, |S.toPOBackdoorSystem.factualY ω| ≤ B
    MemLp (observedAIPW S.P_Z) 2 S.P_Z
    Proof (Lean source)
    theorem observedAIPW_memLp_of_bounded (S : ATE.BackdoorEstimationSystem P γ) {ε B : ℝ} (h_overlap : S.StrictOverlap ε) (hB : 0 ≤ B) (hY_bound : ∀ ω, |S.toPOBackdoorSystem.factualY ω| ≤ B) : MemLp (observedAIPW S.P_Z) 2 S.P_Z := memLp_observedAIPW S.P_Z B ε hB h_overlap.1 (S.observedOutcome_bounded B hY_bound) (S.observedPropensity_overlap h_overlap)
    Causalean.Estimation.ATE.BackdoorEstimationSystem.observedAIPW_memLp_of_bounded · Causalean/Estimation/Efficiency/ATEEfficientIF.lean:117
ATEPathwise­Derivative 2 core · 2 supporting This module combines the exact doubly robust expansion with the first-order tilt bounds. ★ observedATE_tilt_exact_expansion★ hasDerivAt_observedATE_tilt

Pathwise derivative of the observed-law average treatment effect

This module combines the exact doubly robust expansion with the first-order tilt bounds. Under bounded outcomes and strict overlap, the expansion's two product terms are quadratic in the tilt parameter. The remaining fixed-AIPW expectation is differentiated by the bounded-tilt theorem, yielding Hahn's covariance derivative without assuming it.

theorem observedATE_tilt_exact_expansion reviewed
Causalean.Estimation.Efficiency

Exact ATE expansion along an exponential tilt. Given a measurable uniformly bounded tilt score, a nonnegative outcome bound and positive overlap level, bounded outcomes, and strict base arm propensities, the change in the observed-law ATE minus the tilted mean of the base-law AIPW function is exactly the sum of the treated and control products of propensity and regression errors.

Formal statement
γ :
Type u_1
shared
P :
g :
γ × Bool × ℝ → ℝ
M B ε t :
ℝ
hg_meas :
hgM :
∀ z, |g z| ≤ M
hB :
0 ≤ B
hε :
0 < ε
hY :
∀ᵐ z ∂P, |projY z| ≤ B
hoverlap :
∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d z
observedATE (tiltMeasure P g t)
- ∫ z, observedAIPW P z ∂(tiltMeasure P g t)
= -(∫ z, (observedPropensity (tiltMeasure P g t) true z - observedPropensity P true z) / observedPropensity P true z * (observedArmRegression (tiltMeasure P g t) true z - observedArmRegression P true z) ∂(tiltMeasure P g t))
+ ∫ z, (observedPropensity (tiltMeasure P g t) false z - observedPropensity P false z) / observedPropensity P false z * (observedArmRegression (tiltMeasure P g t) false z - observedArmRegression P false z) ∂(tiltMeasure P g t)
Proof (Lean source)
theorem observedATE_tilt_exact_expansion (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M B ε t : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hB : 0 ≤ B) (hε : 0 < ε) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hoverlap : ∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) : observedATE (tiltMeasure P g t) - observedATE P - ∫ z, observedAIPW P z ∂(tiltMeasure P g t) = -(∫ z, (observedPropensity (tiltMeasure P g t) true z - observedPropensity P true z) / observedPropensity P true z * (observedArmRegression (tiltMeasure P g t) true z - observedArmRegression P true z) ∂(tiltMeasure P g t)) + ∫ z, (observedPropensity (tiltMeasure P g t) false z - observedPropensity P false z) / observedPropensity P false z * (observedArmRegression (tiltMeasure P g t) false z - observedArmRegression P false z) ∂(tiltMeasure P g t) := by let Pt := tiltMeasure P g t let _ : IsProbabilityMeasure Pt := isProbabilityMeasure_tiltMeasure hg_meas hgM have hYt : ∀ᵐ z ∂Pt, |projY z| ≤ B := by exact (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hY have hp0P (d : Bool) : ∀ᵐ z ∂P, 0 < observedPropensity P d z := by filter_upwards [hoverlap d] with z hz exact hε.trans_le hz have hp0 (d : Bool) : ∀ᵐ z ∂Pt, 0 < observedPropensity P d z := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (hp0P d) have hpP (d : Bool) : ∀ᵐ z ∂P, 0 < observedPropensity Pt d z := by dsimp [Pt] exact observedPropensity_tilt_pos_ae P g M t d hg_meas hgM (hp0P d) have hp (d : Bool) : ∀ᵐ z ∂Pt, 0 < observedPropensity Pt d z := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (hpP d) have hYint : Integrable (projY : γ × Bool × ℝ → ℝ) Pt := Integrable.of_bound measurable_snd.snd.aestronglyMeasurable B (by simpa [Real.norm_eq_abs] using hYt) have hμ0 (d : Bool) : Integrable (observedArmRegression P d) Pt := by apply Integrable.of_bound (measurable_observedArmRegression P d).aestronglyMeasurable B have hbP := observedArmRegression_abs_le P d B hB hY (hp0P d) exact (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (by simpa [Real.norm_eq_abs] using hbP) have hμ1 (d : Bool) : Integrable (observedArmRegression Pt d) Pt := integrable_observedArmRegression_of_bounded Pt d B hB hYt (hp d) have hinv (d : Bool) : ∀ᵐ z ∂Pt, |(observedPropensity P d z)⁻¹| ≤ ε⁻¹ := by have hbase := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (hoverlap d) filter_upwards [hbase] with z hz have hpz : 0 < observedPropensity P d z := hε.trans_le hz rw [abs_of_pos (inv_pos.mpr hpz)] exact (inv_le_inv₀ hpz hε).2 hz have hres (d : Bool) : Integrable (fun z => observedArmIndicator d z / observedPropensity P d z * (projY z - observedArmRegression P d z)) Pt := by apply Integrable.of_bound (((measurable_observedArmIndicator d).div (measurable_observedPropensity P d)).mul (measurable_snd.snd.sub (measurable_observedArmRegression P d))).aestronglyMeasurable (ε⁻¹ * (B + B)) have hμbP := observedArmRegression_abs_le P d B hB hY (hp0P d) have hμb := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hμbP filter_upwards [hYt, hμb, hinv d] with z hYz hμz hinvz change |(observedArmIndicator d z / observedPropensity P d z) * (projY z - observedArmRegression P d z)| ≤ ε⁻¹ * (B + B) rw [abs_mul, abs_div] have hI : |observedArmIndicator d z| ≤ 1 := by by_cases hz : projA z = d <;> simp [observedArmIndicator, hz] have hfrac : |observedArmIndicator d z| / |observedPropensity P d z| ≤ ε⁻¹ := by rw [div_eq_mul_inv, ← abs_inv] exact (mul_le_of_le_one_left (abs_nonneg _) hI).trans hinvz calc |observedArmIndicator d z| / |observedPropensity P d z| * |projY z - observedArmRegression P d z| ≤ ε⁻¹ * (|projY z| + |observedArmRegression P d z|) := mul_le_mul hfrac (abs_sub _ _) (abs_nonneg _) (by positivity) _ ≤ ε⁻¹ * (B + B) := by gcongr have hprod (d : Bool) : Integrable (fun z => (observedPropensity Pt d z - observedPropensity P d z) / observedPropensity P d z * (observedArmRegression Pt d z - observedArmRegression P d z)) Pt := by have hpI := observedPropensity_mem_Icc_ae Pt d have hp0I := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (observedPropensity_mem_Icc_ae P d) have hμ0b := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (observedArmRegression_abs_le P d B hB hY (hp0P d)) have hμ1b := observedArmRegression_abs_le Pt d B hB hYt (hp d) apply Integrable.of_bound ((((measurable_observedPropensity Pt d).sub (measurable_observedPropensity P d)).div (measurable_observedPropensity P d)).mul ((measurable_observedArmRegression Pt d).sub (measurable_observedArmRegression P d))).aestronglyMeasurable (ε⁻¹ * (2 * (2 * B))) filter_upwards [hpI, hp0I, hμ0b, hμ1b, hinv d] with z hpIz hp0Iz hμ0z hμ1z hinvz change |((observedPropensity Pt d z - observedPropensity P d z) / observedPropensity P d z) * (observedArmRegression Pt d z - observedArmRegression P d z)| ≤ ε⁻¹ * (2 * (2 * B)) rw [abs_mul, abs_div, div_eq_mul_inv, ← abs_inv] have hpropdiff : |observedPropensity Pt d z - observedPropensity P d z| ≤ 2 := (abs_sub _ _).trans (by rw [abs_of_nonneg hpIz.1, abs_of_nonneg hp0Iz.1] linarith [hpIz.2, hp0Iz.2]) have hμdiff : |observedArmRegression Pt d z - observedArmRegression P d z| ≤ 2 * B := (abs_sub _ _).trans (by linarith) calc |observedPropensity Pt d z - observedPropensity P d z| * |(observedPropensity P d z)⁻¹| * |observedArmRegression Pt d z - observedArmRegression P d z| ≤ 2 * ε⁻¹ * (2 * B) := by exact mul_le_mul (mul_le_mul hpropdiff hinvz (abs_nonneg _) (by norm_num)) hμdiff (abs_nonneg _) (by positivity) _ = ε⁻¹ * (2 * (2 * B)) := by ring simpa only [Pt] using observedATE_sub_integral_observedAIPW_eq_product P Pt (fun _ => ε⁻¹) hYint hμ0 hμ1 hinv hp0 hp hres hprod
theorem hasDerivAt_observedATE_tilt reviewed
Causalean.Estimation.Efficiency

Given a probability observed-data law P, a measurable score g that is bounded by a nonnegative constant M and has mean zero, a nonnegative outcome bound B, and strict arm overlap at level ε, the observed-law ATE along the normalized exponential tilt has derivative equal to the AIPW covariance with g. The result is the treated-arm derivative minus the control-arm derivative.

Formal statement
γ :
Type u_1
shared
P :
g :
γ × Bool × ℝ → ℝ
M B ε :
ℝ
hg_meas :
hgM :
∀ z, |g z| ≤ M
hg_mean :
∫ z, g z ∂P = 0
hM :
0 ≤ M
hB :
0 ≤ B
hε :
0 < ε
hY :
∀ᵐ z ∂P, |projY z| ≤ B
hoverlap :
∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d z
HasDerivAt (fun t => observedATE (tiltMeasure P g t)) (∫ z, observedAIPW P z * g z ∂P) 0
Proof (Lean source)
theorem hasDerivAt_observedATE_tilt (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M B ε : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hg_mean : ∫ z, g z ∂P = 0) (hM : 0 ≤ M) (hB : 0 ≤ B) (hε : 0 < ε) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hoverlap : ∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) : HasDerivAt (fun t => observedATE (tiltMeasure P g t)) (∫ z, observedAIPW P z * g z ∂P) 0 := by have hp (d : Bool) : ∀ᵐ z ∂P, 0 < observedPropensity P d z := by filter_upwards [hoverlap d] with z hz exact hε.trans_le hz have hμ (d : Bool) : Integrable (observedArmRegression P d) P := integrable_observedArmRegression_of_bounded P d B hB hY (hp d) have hfun : (fun t => observedATE (tiltMeasure P g t)) = fun t => observedArmMean (tiltMeasure P g t) true - observedArmMean (tiltMeasure P g t) false := by funext t let Pt := tiltMeasure P g t let _ : IsProbabilityMeasure Pt := isProbabilityMeasure_tiltMeasure hg_meas hgM have hYt : ∀ᵐ z ∂Pt, |projY z| ≤ B := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hY apply observedATE_eq_observedArmMean_sub intro d have hptP : ∀ᵐ z ∂P, 0 < observedPropensity Pt d z := by dsimp [Pt] exact observedPropensity_tilt_pos_ae P g M t d hg_meas hgM (hp d) have hpt : ∀ᵐ z ∂Pt, 0 < observedPropensity Pt d z := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hptP exact integrable_observedArmRegression_of_bounded Pt d B hB hYt hpt have hd (d : Bool) := hasDerivAt_observedArmMean_tilt P d g M B ε hg_meas hgM hg_mean hM hB hε hY (hoverlap d) have hφ (d : Bool) := memLp_observedArmEIF P d B ε hB hε hY (hoverlap d) have hint (d : Bool) : Integrable (fun z => observedArmEIF P d z * g z) P := by have h := (hφ d).integrable (by norm_num) |>.bdd_mul hg_meas.aestronglyMeasurable (ae_of_all P fun z => by simpa [Real.norm_eq_abs] using hgM z) exact h.congr (ae_of_all P fun z => by ring) have hcoef : (∫ z, observedArmEIF P true z * g z ∂P) - ∫ z, observedArmEIF P false z * g z ∂P = ∫ z, observedAIPW P z * g z ∂P := by rw [← integral_sub (hint true) (hint false)] apply integral_congr_ae filter_upwards with z rw [observedAIPW_eq_armEIF_sub P hμ] ring rw [hfun] change HasDerivAt ((fun t => observedArmMean (tiltMeasure P g t) true) - fun t => observedArmMean (tiltMeasure P g t) false) (∫ z, observedAIPW P z * g z ∂P) 0 simpa only [hcoef] using (hd true).sub (hd false)
2 supporting declarations (lemmas, instances)
ATETilt­Nuisance 2 core · 13 supporting This module combines the conditional Bayes formula with elementary uniform bounds for exponential weights. ★ observedPropensity_tilt_firstOrder★ observedArmRegression_tilt_firstOrder

First-order control of observed-law nuisances along bounded tilts

This module combines the conditional Bayes formula with elementary uniform bounds for exponential weights. It identifies the propensity and arm regressions recomputed from a tilted observed law and bounds their changes by an explicit multiple of the perturbation size.

theorem observedPropensity_tilt_firstOrder reviewed
Causalean.Estimation.Efficiency

Along a bounded measurable exponential tilt with a nonnegative bound and local perturbation, the recomputed arm propensity changes by at most a constant times |t|M. This is the first-order propensity control used in the ATE remainder.

Formal statement
γ :
Type u_2
shared
P :
g :
γ × Bool × ℝ → ℝ
M t :
ℝ
d :
hg_meas :
hgM :
∀ z, |g z| ≤ M
hM :
0 ≤ M
ht :
|t| * M ≤ 1
∀ᵐ z ∂P, |observedPropensity (tiltMeasure P g t) d z - observedPropensity P d z|
≤ 4 * (|t| * M) / exp (-|t| * M)
Proof (Lean source)
theorem observedPropensity_tilt_firstOrder (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M t : ℝ) (d : Bool) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hM : 0 ≤ M) (ht : |t| * M ≤ 1) : ∀ᵐ z ∂P, |observedPropensity (tiltMeasure P g t) d z - observedPropensity P d z| ≤ 4 * (|t| * M) / exp (-|t| * M) := by let u : γ × Bool × ℝ → ℝ := fun z => exp (t * g z) let δ := 2 * (|t| * M) let a := exp (-|t| * M) have hδ : 0 ≤ δ := by positivity have ha : 0 < a := Real.exp_pos _ have hi := integrable_observedArmIndicator P d have hone : Integrable (fun _ : γ × Bool × ℝ => (1 : ℝ)) P := integrable_const _ have hratio := abs_condExp_ratio_mul_sub_le (m := observedCovariateSigma) hi hone (hg_meas.const_mul t).exp (show 0 ≤ (1 : ℝ) by norm_num) hδ ha (Eventually.of_forall fun _ => zero_le_one) (Eventually.of_forall fun z => by simp [condExp_const observedCovariateSigma_le]) (Eventually.of_forall fun z => by by_cases hz : projA z = d <;> simp [observedArmIndicator, hz]) (fun z => by simpa [u, δ] using abs_exp_score_sub_one_le g M t hgM ht z) (fun z => by simpa [u, a] using exp_neg_abs_mul_le_exp_score g M t hgM z) have hbayes := observedPropensity_tilt_ae_eq_expRatio P g M t d hg_meas hgM filter_upwards [hratio, hbayes] with z hz hbayes_z rw [hbayes_z] simp only [u, observedPropensity, condExp_const observedCovariateSigma_le] at hz ⊢ convert hz using 1 <;> ring
Causalean.Estimation.Efficiency.observedPropensity_tilt_firstOrder · Causalean/Estimation/Efficiency/ATETiltNuisance.lean:388 · uses observedPropensity , tiltMeasure
theorem observedArmRegression_tilt_firstOrder reviewed
Causalean.Estimation.Efficiency

If the outcome bound and tilt bound are nonnegative, the outcome is bounded, and the base arm propensity is strictly positive, then along a bounded measurable exponential tilt with a local perturbation, the recomputed arm regression changes by at most a constant times |t|M.

Formal statement
γ :
Type u_2
shared
P :
g :
γ × Bool × ℝ → ℝ
M B t :
ℝ
d :
hg_meas :
hgM :
∀ z, |g z| ≤ M
hM :
0 ≤ M
hB :
0 ≤ B
hY :
∀ᵐ z ∂P, |projY z| ≤ B
hp :
∀ᵐ z ∂P, 0 < observedPropensity P d z
ht :
|t| * M ≤ 1
∀ᵐ z ∂P, |observedArmRegression (tiltMeasure P g t) d z - observedArmRegression P d z|
≤ 4 * B * (|t| * M) / exp (-|t| * M)
Proof (Lean source)
theorem observedArmRegression_tilt_firstOrder (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M B t : ℝ) (d : Bool) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hM : 0 ≤ M) (hB : 0 ≤ B) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hp : ∀ᵐ z ∂P, 0 < observedPropensity P d z) (ht : |t| * M ≤ 1) : ∀ᵐ z ∂P, |observedArmRegression (tiltMeasure P g t) d z - observedArmRegression P d z| ≤ 4 * B * (|t| * M) / exp (-|t| * M) := by let u : γ × Bool × ℝ → ℝ := fun z => exp (t * g z) let δ := 2 * (|t| * M) let a := exp (-|t| * M) let I : γ × Bool × ℝ → ℝ := observedArmIndicator d let f : γ × Bool × ℝ → ℝ := fun z => projY z * I z have hδ : 0 ≤ δ := by positivity have ha : 0 < a := Real.exp_pos _ have hI : Integrable I P := integrable_observedArmIndicator P d have hf : Integrable f P := by apply Integrable.of_bound ((measurable_snd.snd.mul (measurable_observedArmIndicator d)).aestronglyMeasurable) B filter_upwards [hY] with z hYz dsimp [f, I] change |projY z * observedArmIndicator d z| ≤ B rw [abs_mul] by_cases hz : projA z = d · simpa [observedArmIndicator, hz] using hYz · simpa [observedArmIndicator, hz] using hB have hdom : ∀ᵐ z ∂P, |f z| ≤ B * I z := by filter_upwards [hY] with z hYz dsimp [f, I] rw [abs_mul] by_cases hz : projA z = d · simpa [observedArmIndicator, hz] using hYz · simp [observedArmIndicator, hz, hB] have hratio := abs_condExp_ratio_mul_sub_le (m := observedCovariateSigma) hf hI (hg_meas.const_mul t).exp hB hδ ha (Eventually.of_forall fun z => by dsimp [I] by_cases hz : projA z = d <;> simp [observedArmIndicator, hz]) (by simpa [I, observedPropensity] using hp) hdom (fun z => by simpa [u, δ] using abs_exp_score_sub_one_le g M t hgM ht z) (fun z => by simpa [u, a] using exp_neg_abs_mul_le_exp_score g M t hgM z) have hbayes := observedArmRegression_tilt_ae_eq_expRatio P g M B t d hg_meas hgM hY filter_upwards [hratio, hbayes] with z hz hbayes_z rw [hbayes_z] simp only [f, I, u, observedArmRegression, observedArmNumerator, observedPropensity] at hz ⊢ convert hz using 1 <;> ring
Causalean.Estimation.Efficiency.observedArmRegression_tilt_firstOrder · Causalean/Estimation/Efficiency/ATETiltNuisance.lean:468 · uses projY , observedArmRegression , observedPropensity , tiltMeasure
13 supporting declarations (lemmas, instances)
ATEVariance 1 core · 2 supporting This module develops the L² and variance algebra behind the Hahn (1998) variance formula for the backdoor ATE. ★ aipw_variance_hahn_decomposition

Hahn variance decomposition for the AIPW influence function

This module develops the L² and variance algebra behind the Hahn (1998) variance formula for the backdoor ATE. The main theorem BackdoorEstimationSystem.aipw_variance_hahn_decomposition proves that ∫ ψ_AIPW² dP_Z splits into the conditional-ATE variance term plus the two inverse-propensity-weighted conditional outcome-variance terms.

The helper lemmas establish bounded inverse-propensity weights and L² membership for the regression representatives under overlap and square-integrable outcomes. The final theorems dml_ATE_tendstoNormal_hahnVariance_on_highProbEvent (learner conditions on events of probability tending to one) and its every-realization corollary dml_ATE_tendstoNormal_hahnVariance rewrite the limiting variance in the one-shot DML central-limit theorem by this decomposition; they do not prove regularity under local alternatives or a convolution lower bound.

theorem aipw_variance_hahn_decomposition reviewed
Causalean.Estimation.ATE.BackdoorEstimationSystem

Hahn (1998) variance decomposition of the AIPW influence function. Assume the back-door identifying assumptions and strict overlap of the true propensity score with margin ε, and suppose the factual outcome is square-integrable and every potential outcome Y(d) is square-integrable. Then the variance of the augmented inverse-propensity-weighted (AIPW) influence function decomposes as the variance of the conditional treatment-effect function μ₁ − μ₀ − θ₀ plus two inverse-propensity-weighted conditional-outcome-variance terms, the three-term variance expression used in Hahn's efficiency calculation.

Formal statement
P :
shared
γ :
Type u_1
shared
ε :
ℝ
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) ^ 2 ∂S.P_Z)
= (∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X)
+ (∫ z, (indA z / (S.e_val (projX z)) ^ 2) * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z)
+ (∫ z, ((1 - indA z) / (1 - S.e_val (projX z)) ^ 2) * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z)
Proof (Lean source)
theorem aipw_variance_hahn_decomposition (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) ^ 2 ∂S.P_Z) = (∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X) + (∫ z, (indA z / (S.e_val (projX z)) ^ 2) * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z) + (∫ z, ((1 - indA z) / (1 - S.e_val (projX z)) ^ 2) * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z) := by classical -- Ω-level pieces. set X : P.Ω → γ := S.toPOBackdoorSystem.factualX with hX set Y : P.Ω → ℝ := S.toPOBackdoorSystem.factualY with hY set a : P.Ω → ℝ := fun ω => indA (S.factualZ ω) with ha set e : P.Ω → ℝ := fun ω => S.e_val (S.toPOBackdoorSystem.factualX ω) with he set μ1 : P.Ω → ℝ := fun ω => S.μ_val true (S.toPOBackdoorSystem.factualX ω) with hμ1 set μ0 : P.Ω → ℝ := fun ω => S.μ_val false (S.toPOBackdoorSystem.factualX ω) with hμ0 set Afn : P.Ω → ℝ := fun ω => μ1 ω - μ0 ω - S.θ₀ with hAfn set Bfn : P.Ω → ℝ := fun ω => (a ω / e ω) * (Y ω - μ1 ω) with hBfn set Cfn : P.Ω → ℝ := fun ω => ((1 - a ω) / (1 - e ω)) * (Y ω - μ0 ω) with hCfn -- `a ω` is `0` or `1`. have ha01 : ∀ ω, a ω = 0 ∨ a ω = 1 := by intro ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · right; simp [ha, indA, projA, BackdoorEstimationSystem.factualZ, hD] · left; simp [ha, indA, projA, BackdoorEstimationSystem.factualZ, hD] -- `a = 1_{D=true}` and `1 - a = 1_{D=false}`. have ha_ind : ∀ ω, a ω = 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 [ha, indA, projA, BackdoorEstimationSystem.factualZ, hD, hInd] · have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [ha, indA, projA, BackdoorEstimationSystem.factualZ, hD, hInd] have hna_ind : ∀ ω, 1 - a ω = 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 ω rw [ha_ind ω]; linarith -- `L²` membership of the three pieces. have hμ1_L2 : MemLp μ1 2 P.μ := S.hahn_mu_L2 hA h_yd2 true have hμ0_L2 : MemLp μ0 2 P.μ := S.hahn_mu_L2 hA h_yd2 false have hY_L2 : MemLp Y 2 P.μ := (memLp_two_iff_integrable_sq S.toPOBackdoorSystem.measurable_factualY.aestronglyMeasurable).2 h_y2 have hwT_Linf : MemLp (fun ω => a ω / e ω) ⊤ P.μ := S.hahn_weight_true_Linf h_overlap have hwF_Linf : MemLp (fun ω => (1 - a ω) / (1 - e ω)) ⊤ P.μ := S.hahn_weight_false_Linf h_overlap have hA_L2 : MemLp Afn 2 P.μ := (hμ1_L2.sub hμ0_L2).sub (memLp_const _) have hBfn_L2' : MemLp (fun ω => (a ω / e ω) * (Y ω - μ1 ω)) 2 P.μ := by exact (hY_L2.sub hμ1_L2).mul hwT_Linf have hB_L2 : MemLp Bfn 2 P.μ := by simpa [hBfn] using hBfn_L2' have hCfn_L2' : MemLp (fun ω => ((1 - a ω) / (1 - e ω)) * (Y ω - μ0 ω)) 2 P.μ := by exact (hY_L2.sub hμ0_L2).mul hwF_Linf have hC_L2 : MemLp Cfn 2 P.μ := by simpa [hCfn] using hCfn_L2' -- Integrability of the five squared/cross pieces (each a product of two L²). have hAB_int : Integrable (fun ω => Afn ω * Bfn ω) P.μ := hA_L2.integrable_mul hB_L2 have hAC_int : Integrable (fun ω => Afn ω * Cfn ω) P.μ := hA_L2.integrable_mul hC_L2 have hA2_int : Integrable (fun ω => Afn ω ^ 2) P.μ := by simp only [sq] exact hA_L2.integrable_mul hA_L2 have hB2_int : Integrable (fun ω => Bfn ω ^ 2) P.μ := by simp only [sq] exact hB_L2.integrable_mul hB_L2 have hC2_int : Integrable (fun ω => Cfn ω ^ 2) P.μ := by simp only [sq] exact hC_L2.integrable_mul hC_L2 -- Pointwise expansion `ψ(factualZ ω)² = A² + B² + C² + 2AB − 2AC`. have hψ_sq : ∀ ω, (S.ψ_AIPW (S.factualZ ω)) ^ 2 = Afn ω ^ 2 + Bfn ω ^ 2 + Cfn ω ^ 2 + 2 * (Afn ω * Bfn ω) - 2 * (Afn ω * Cfn ω) := by intro ω have hexpand : S.ψ_AIPW (S.factualZ ω) = Afn ω + Bfn ω - Cfn ω := by unfold BackdoorEstimationSystem.ψ_AIPW BackdoorEstimationSystem.aipwMoment simp only [BackdoorEstimationSystem.factualZ, projX, projY, hBfn, hCfn, ha, he, hμ1, hμ0, hY] ring rw [hexpand] simp only [hAfn, hBfn, hCfn] rcases ha01 ω with h0 | h1 · rw [show a ω = 0 from h0]; ring · rw [show a ω = 1 from h1]; ring -- Cross-term weights `g` for the σ(X)-pull-out lemma. set gT : γ → ℝ := fun x => (S.μ_val true x - S.μ_val false x - S.θ₀) / S.e_val x with hgT set gF : γ → ℝ := fun x => (S.μ_val true x - S.μ_val false x - S.θ₀) / (1 - S.e_val x) with hgF have hgT_meas : Measurable gT := (((S.μ_meas true).sub (S.μ_meas false)).sub measurable_const).div S.e_meas have hgF_meas : Measurable gF := (((S.μ_meas true).sub (S.μ_meas false)).sub measurable_const).div (measurable_const.sub S.e_meas) -- `A·B` is the `d = true` weighted residual. have hAB_eq : ∀ ω, Afn ω * Bfn ω = gT (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω))) := by intro ω have hae := ha_ind ω simp only [hAfn, hBfn, hgT, hμ1, hμ0, hY, he] rw [← hae] ring have hAB_int' : Integrable (fun ω => gT (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val true (S.toPOBackdoorSystem.factualX ω)))) P.μ := hAB_int.congr (Filter.Eventually.of_forall hAB_eq) have hAB_zero : ∫ ω, Afn ω * Bfn ω ∂P.μ = 0 := by rw [MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall hAB_eq)] exact S.weighted_residual_integral_zero hA true gT hgT_meas hAB_int' (S.cond_exp_residual_zero hA true) -- `A·C` is the `d = false` weighted residual. have hAC_eq : ∀ ω, Afn ω * Cfn ω = gF (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω))) := by intro ω have hae := hna_ind ω simp only [hAfn, hCfn, hgF, hμ1, hμ0, hY, he] rw [← hae] ring have hAC_int' : Integrable (fun ω => gF (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator false ω * (S.toPOBackdoorSystem.factualY ω - S.μ_val false (S.toPOBackdoorSystem.factualX ω)))) P.μ := hAC_int.congr (Filter.Eventually.of_forall hAC_eq) have hAC_zero : ∫ ω, Afn ω * Cfn ω ∂P.μ = 0 := by rw [MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall hAC_eq)] exact S.weighted_residual_integral_zero hA false gF hgF_meas hAC_int' (S.cond_exp_residual_zero hA false) -- LHS: push `∫ ψ² ∂P_Z` to `∫ ψ(factualZ ·)² ∂P.μ`, expand and integrate. have hψ_meas : Measurable S.ψ_AIPW := S.measurable_ψ_AIPW have hLHS : (∫ z, (S.ψ_AIPW z) ^ 2 ∂S.P_Z) = (∫ ω, Afn ω ^ 2 ∂P.μ) + (∫ ω, Bfn ω ^ 2 ∂P.μ) + (∫ ω, Cfn ω ^ 2 ∂P.μ) := by rw [BackdoorEstimationSystem.P_Z, MeasureTheory.integral_map S.measurable_factualZ.aemeasurable (hψ_meas.pow_const 2).aestronglyMeasurable] rw [MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall hψ_sq)] have iAB : Integrable (fun ω => Afn ω ^ 2 + Bfn ω ^ 2) P.μ := hA2_int.add hB2_int have iABC : Integrable (fun ω => Afn ω ^ 2 + Bfn ω ^ 2 + Cfn ω ^ 2) P.μ := iAB.add hC2_int have icAB : Integrable (fun ω => 2 * (Afn ω * Bfn ω)) P.μ := hAB_int.const_mul 2 have icAC : Integrable (fun ω => 2 * (Afn ω * Cfn ω)) P.μ := hAC_int.const_mul 2 have iABCpAB : Integrable (fun ω => (Afn ω ^ 2 + Bfn ω ^ 2 + Cfn ω ^ 2) + 2 * (Afn ω * Bfn ω)) P.μ := iABC.add icAB rw [MeasureTheory.integral_sub iABCpAB icAC] rw [MeasureTheory.integral_add iABC icAB] rw [MeasureTheory.integral_add iAB hC2_int] rw [MeasureTheory.integral_add hA2_int hB2_int] rw [MeasureTheory.integral_const_mul, MeasureTheory.integral_const_mul] rw [hAB_zero, hAC_zero] ring rw [hLHS] -- Term 1: `∫ A² ∂P.μ = ∫ (μ₁ − μ₀ − θ₀)² ∂P_X`. have hTerm1 : (∫ ω, Afn ω ^ 2 ∂P.μ) = ∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X := by rw [BackdoorEstimationSystem.P_X] rw [MeasureTheory.integral_map S.toPOBackdoorSystem.measurable_factualX.aemeasurable (by exact (((S.μ_meas true).sub (S.μ_meas false)).sub measurable_const).pow_const 2 |>.aestronglyMeasurable)] -- Term 2: `∫ B² ∂P.μ = ∫ (a/e²)(y − μ₁)² ∂P_Z`. have hTerm2 : (∫ ω, Bfn ω ^ 2 ∂P.μ) = ∫ z, indA z / S.e_val (projX z) ^ 2 * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z := by rw [BackdoorEstimationSystem.P_Z] have hmeas2 : Measurable (fun z : γ × Bool × ℝ => indA z / S.e_val (projX z) ^ 2 * (projY z - S.μ_val true (projX z)) ^ 2) := by have hx : Measurable (fun z : γ × Bool × ℝ => z.1) := measurable_fst have hy : Measurable (fun z : γ × Bool × ℝ => z.2.2) := measurable_snd.snd have hind : Measurable (fun z : γ × Bool × ℝ => indA z) := by unfold indA projA exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp measurable_snd.fst have he2 : Measurable (fun z : γ × Bool × ℝ => S.e_val (projX z) ^ 2) := ((S.e_meas.comp hx).pow_const 2) have hμt : Measurable (fun z : γ × Bool × ℝ => S.μ_val true (projX z)) := (S.μ_meas true).comp hx exact (hind.div he2).mul ((hy.sub hμt).pow_const 2) rw [MeasureTheory.integral_map S.measurable_factualZ.aemeasurable hmeas2.aestronglyMeasurable] apply MeasureTheory.integral_congr_ae refine Filter.Eventually.of_forall (fun ω => ?_) change Bfn ω ^ 2 = a ω / e ω ^ 2 * (Y ω - μ1 ω) ^ 2 have hsq : a ω ^ 2 = a ω := by rcases ha01 ω with h | h <;> rw [h] <;> ring simp only [hBfn] rw [mul_pow, div_pow, hsq] -- Term 3: `∫ C² ∂P.μ = ∫ ((1−a)/(1−e)²)(y − μ₀)² ∂P_Z`. have hTerm3 : (∫ ω, Cfn ω ^ 2 ∂P.μ) = ∫ z, (1 - indA z) / (1 - S.e_val (projX z)) ^ 2 * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z := by rw [BackdoorEstimationSystem.P_Z] have hmeas3 : Measurable (fun z : γ × Bool × ℝ => (1 - indA z) / (1 - S.e_val (projX z)) ^ 2 * (projY z - S.μ_val false (projX z)) ^ 2) := by have hx : Measurable (fun z : γ × Bool × ℝ => z.1) := measurable_fst have hy : Measurable (fun z : γ × Bool × ℝ => z.2.2) := measurable_snd.snd have hind : Measurable (fun z : γ × Bool × ℝ => indA z) := by unfold indA projA exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp measurable_snd.fst have he2 : Measurable (fun z : γ × Bool × ℝ => (1 - S.e_val (projX z)) ^ 2) := -- … truncated; follow the source link for the rest …
2 supporting declarations (lemmas, instances)
  • dml_ATE_tendstoNormal_hahnVariance_on_highProbEvent theorem — The one-shot DML ATE has a Gaussian limit with Hahn-form variance, with learner conditions on events of probability tending to one. For a back-door estimation system satisfying the back-door identification assumptions, with an overlap threshold ε such that 0 < ε ≤ 1/2 and the true propensity score lies between ε and 1 − ε almost surely, a square-integrable observed outcome and square-integrable potential outcomes, let an i.i.d. sample be split once into a training fold and an evaluation fold whose evaluation-fold share converges to a limit c that is positive, and let μ̂_n and ê_n be the outcome-regression and propensity learners. Suppose there are events G_n whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Assume (ω, x) ↦ μ̂_n(ω)(a, x) is jointly measurable for each arm a and so is (ω, x) ↦ ê_n(ω)(x); on G_n each μ̂_n(a, ·) is square-integrable under the covariate law, ê_n is square-integrable under the covariate law and ε ≤ ê_n ≤ 1 − ε almost everywhere under the covariate law; μ̂_n and ê_n are measurable with respect to the product of the σ-algebra generated by the training-fold observations and the covariate σ-algebra; for each arm the L² error of μ̂_n under the covariate law is o_p(1), the L² error of ê_n is o_p(1), and for each arm the product of these two L² errors is o_p(n^(−1/2)). Given in addition measurability of the augmented inverse-probability-weighted influence function, almost-everywhere measurability of the rescaled estimator at every sample size, and almost-everywhere measurability of the normalized influence-function sum at every sample size, then √|B(n)|·(θ̂_n − θ₀), where B(n) is the evaluation fold, converges in distribution to the mean-zero Gaussian law whose variance has Hahn's three-term form: the variance of the conditional average treatment effect plus the two inverse-propensity-weighted conditional outcome variances.
    P :
    shared
    γ :
    Type u_1
    shared
    ε :
    ℝ
    hA :
    S.toPOBackdoorSystem.Assumptions
    h_overlap :
    S.StrictOverlap ε
    h_y2 :
    Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
    h_yd2 :
    ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ
    sample :
    IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z
    split :
    c :
    ℝ
    hc_pos :
    0 < c
    h_split_rate :
    Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)
    μ_hat :
    ℕ → P.Ω → (Bool → γ → ℝ)
    e_hat :
    ℕ → P.Ω → (γ → ℝ)
    goodSet :
    ℕ → Set P.Ω
    Δ :
    ℕ → ℝ≥0∞
    hΔ :
    Tendsto Δ atTop (𝓝 0)
    hfail :
    ∀ n, P.μ (goodSet n)ᶜ ≤ Δ n
    h_mu_meas :
    ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
    h_e_meas :
    ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
    h_mu_memLp :
    ∀ n ω
    if
    ω ∈ goodSet n
    then
    ∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X
    h_e_memLp :
    ∀ n ω
    if
    ω ∈ goodSet n
    then
    MemLp (fun x => e_hat n ω x) 2 S.P_X
    h_e_overlap :
    ∀ n ω
    if
    ω ∈ goodSet n
    then
    ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε
    h_mu_uncurry_foldA :
    ∀ n a,
    Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
    h_e_uncurry_foldA :
    ∀ n,
    Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
    h_mu_rate :
    ∀ a : Bool,
    IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
    h_e_rate :
    IsLittleOp (fun n ω => (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
    h_product_rate :
    ∀ a : Bool,
    IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
    hψ_meas :
    Measurable (S.ψ_AIPW)
    hθn_meas :
    ∀ n : ℕ,
    AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ
    hSum_meas :
    ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ
    Modes.TendstoInLaw (fun _ : ℕ => P.μ) (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 ((∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X) + (∫ z, (indA z / (S.e_val (projX z)) ^ 2) * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z) + (∫ z, ((1 - indA z) / (1 - S.e_val (projX z)) ^ 2) * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z)))
    Proof (Lean source)
    theorem dml_ATE_tendstoNormal_hahnVariance_on_highProbEvent (S : BackdoorEstimationSystem P γ) {ε : ℝ} (hA : S.toPOBackdoorSystem.Assumptions) (h_overlap : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (μ_hat : ℕ → P.Ω → (Bool → γ → ℝ)) (e_hat : ℕ → P.Ω → (γ → ℝ)) (goodSet : ℕ → Set P.Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, P.μ (goodSet n)ᶜ ≤ Δ n) (h_mu_meas : ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_e_meas : ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_mu_memLp : ∀ n ω, ω ∈ goodSet n → ∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X) (h_e_memLp : ∀ n ω, ω ∈ goodSet n → MemLp (fun x => e_hat n ω x) 2 S.P_X) (h_e_overlap : ∀ n ω, ω ∈ goodSet n → ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε) (h_mu_uncurry_foldA : ∀ n a, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_e_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_e_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) (hψ_meas : Measurable (S.ψ_AIPW)) (hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ) (hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ) : Modes.TendstoInLaw (fun _ : ℕ => P.μ) (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 ((∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X) + (∫ z, (indA z / (S.e_val (projX z)) ^ 2) * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z) + (∫ z, ((1 - indA z) / (1 - S.e_val (projX z)) ^ 2) * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z))) := by rw [← S.aipw_variance_hahn_decomposition h_overlap hA h_y2 h_yd2] exact dml_ATE_tendstoNormal_on_highProbEvent S hA h_overlap h_y2 h_yd2 sample split hc_pos h_split_rate μ_hat e_hat goodSet Δ hΔ hfail h_mu_meas h_e_meas h_mu_memLp h_e_memLp h_e_overlap h_mu_uncurry_foldA h_e_uncurry_foldA h_mu_rate h_e_rate h_product_rate hψ_meas hθn_meas hSum_meas
    Causalean.Estimation.ATE.dml_ATE_tendstoNormal_hahnVariance_on_highProbEvent · Causalean/Estimation/Efficiency/ATEVariance.lean:435
  • dml_ATE_tendstoNormal_hahnVariance theorem — The one-shot DML ATE has a Gaussian limit with Hahn-form variance. Assume the back-door identifying assumptions and strict overlap of the true propensity score with margin ε, with the factual outcome and every potential outcome Y(d) square-integrable. Let sample be an i.i.d. draw of the observed data and split a one-shot fold split whose evaluation-fold share converges to a positive limit c. For the nuisance estimators μ_hat, e_hat fit on the training fold, assume each is jointly measurable in the training data and the evaluation point and square-integrable against P_X, and each is measurable in the training fold jointly with the evaluation point, that the estimated propensity score also satisfies overlap with margin ε, that each nuisance estimator is L²(P_X)-consistent, and that the product of the two L² estimation errors is o_P(n^{-1/2}) — the Neyman-orthogonality rate condition. Assume finally the AIPW influence function, the rescaled estimator, and the normalized influence-function sum are all measurable. Then the rescaled one-shot DML ATE estimator converges in distribution to the mean-zero Gaussian law whose variance has Hahn's three-term AIPW form.
    P :
    shared
    γ :
    Type u_1
    shared
    ε :
    ℝ
    hA :
    S.toPOBackdoorSystem.Assumptions
    h_overlap :
    S.StrictOverlap ε
    h_y2 :
    Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
    h_yd2 :
    ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ
    sample :
    IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z
    split :
    c :
    ℝ
    hc_pos :
    0 < c
    h_split_rate :
    Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)
    μ_hat :
    ℕ → P.Ω → (Bool → γ → ℝ)
    e_hat :
    ℕ → P.Ω → (γ → ℝ)
    h_mu_meas :
    ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
    h_e_meas :
    ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
    h_mu_memLp :
    ∀ n ω a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X
    h_e_memLp :
    ∀ n ω, MemLp (fun x => e_hat n ω x) 2 S.P_X
    h_e_overlap :
    ∀ n ω, ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε
    h_mu_uncurry_foldA :
    ∀ n a,
    Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
    h_e_uncurry_foldA :
    ∀ n,
    Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
    h_mu_rate :
    ∀ a : Bool,
    IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
    h_e_rate :
    IsLittleOp (fun n ω => (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
    h_product_rate :
    ∀ a : Bool,
    IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
    hψ_meas :
    Measurable (S.ψ_AIPW)
    hθn_meas :
    ∀ n : ℕ,
    AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ
    hSum_meas :
    ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ
    Modes.TendstoInLaw (fun _ : ℕ => P.μ) (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 ((∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X) + (∫ z, (indA z / (S.e_val (projX z)) ^ 2) * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z) + (∫ z, ((1 - indA z) / (1 - S.e_val (projX z)) ^ 2) * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z)))
    Proof (Lean source)
    theorem dml_ATE_tendstoNormal_hahnVariance (S : BackdoorEstimationSystem P γ) {ε : ℝ} (hA : S.toPOBackdoorSystem.Assumptions) (h_overlap : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (μ_hat : ℕ → P.Ω → (Bool → γ → ℝ)) (e_hat : ℕ → P.Ω → (γ → ℝ)) (h_mu_meas : ∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_e_meas : ∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_mu_memLp : ∀ n ω a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X) (h_e_memLp : ∀ n ω, MemLp (fun x => e_hat n ω x) 2 S.P_X) (h_e_overlap : ∀ n ω, ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε) (h_mu_uncurry_foldA : ∀ n a, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)) (h_e_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => e_hat n p.1 p.2)) (h_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_e_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) (hψ_meas : Measurable (S.ψ_AIPW)) (hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ) (hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ) : Modes.TendstoInLaw (fun _ : ℕ => P.μ) (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 ((∫ x, (S.μ_val true x - S.μ_val false x - S.θ₀) ^ 2 ∂S.P_X) + (∫ z, (indA z / (S.e_val (projX z)) ^ 2) * (projY z - S.μ_val true (projX z)) ^ 2 ∂S.P_Z) + (∫ z, ((1 - indA z) / (1 - S.e_val (projX z)) ^ 2) * (projY z - S.μ_val false (projX z)) ^ 2 ∂S.P_Z))) := by exact dml_ATE_tendstoNormal_hahnVariance_on_highProbEvent S hA h_overlap h_y2 h_yd2 sample split hc_pos h_split_rate μ_hat e_hat (fun _ => univ) (fun _ => 0) tendsto_const_nhds (by simp) h_mu_meas h_e_meas (fun n ω _ a => h_mu_memLp n ω a) (fun n ω _ => h_e_memLp n ω) (fun n ω _ => h_e_overlap n ω) h_mu_uncurry_foldA h_e_uncurry_foldA h_mu_rate h_e_rate h_product_rate hψ_meas hθn_meas hSum_meas
    Causalean.Estimation.ATE.dml_ATE_tendstoNormal_hahnVariance · Causalean/Estimation/Efficiency/ATEVariance.lean:545
Observed­Law­Expansion 1 core · 6 supporting This module proves the conditional-expectation algebra behind the exact AIPW remainder. ★ observedATE_sub_integral_observedAIPW_eq_product

Exact doubly-robust expansion for the observed-law ATE

This module proves the conditional-expectation algebra behind the exact AIPW remainder. The main identity compares two observed-data laws and expresses the failure of the base-law AIPW function to be exactly affine as a product of the propensity and arm-regression changes.

theorem observedATE_sub_integral_observedAIPW_eq_product reviewed
Causalean.Estimation.Efficiency

Exact doubly-robust observed-law expansion. Compare a base probability law Q₀ with an evaluation probability law Q. Assume integrability of the outcome and both laws' arm regressions, bounded inverse base arm propensities, positive arm propensities under both laws, and the resulting residual and product integrability gates. Then the ATE change minus the mean of the base-law AIPW function equals exactly the sum of products of propensity and arm-regression errors.

Formal statement
γ :
Type u_1
shared
Q₀ Q :
C :
Bool → ℝ
hY :
Integrable (projY : γ × Bool × ℝ → ℝ) Q
hμ0 :
hμ1 :
hinv :
∀ d, ∀ᵐ z ∂Q, |(observedPropensity Q₀ d z)⁻¹| ≤ C d
hp0 :
∀ d, ∀ᵐ z ∂Q, 0 < observedPropensity Q₀ d z
hp :
∀ d, ∀ᵐ z ∂Q, 0 < observedPropensity Q d z
hres :
∀ d,
Integrable (fun z => observedArmIndicator d z / observedPropensity Q₀ d z * (projY z - observedArmRegression Q₀ d z)) Q
hprod :
∀ d,
Proof (Lean source)
theorem observedATE_sub_integral_observedAIPW_eq_product (Q₀ Q : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure Q] (C : Bool → ℝ) (hY : Integrable (projY : γ × Bool × ℝ → ℝ) Q) (hμ0 : ∀ d, Integrable (observedArmRegression Q₀ d) Q) (hμ1 : ∀ d, Integrable (observedArmRegression Q d) Q) (hinv : ∀ d, ∀ᵐ z ∂Q, |(observedPropensity Q₀ d z)⁻¹| ≤ C d) (hp0 : ∀ d, ∀ᵐ z ∂Q, 0 < observedPropensity Q₀ d z) (hp : ∀ d, ∀ᵐ z ∂Q, 0 < observedPropensity Q d z) (hres : ∀ d, Integrable (fun z => observedArmIndicator d z / observedPropensity Q₀ d z * (projY z - observedArmRegression Q₀ d z)) Q) (hprod : ∀ d, Integrable (fun z => (observedPropensity Q d z - observedPropensity Q₀ d z) / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z)) Q) : observedATE Q - observedATE Q₀ - ∫ z, observedAIPW Q₀ z ∂Q = -(∫ z, (observedPropensity Q true z - observedPropensity Q₀ true z) / observedPropensity Q₀ true z * (observedArmRegression Q true z - observedArmRegression Q₀ true z) ∂Q) + ∫ z, (observedPropensity Q false z - observedPropensity Q₀ false z) / observedPropensity Q₀ false z * (observedArmRegression Q false z - observedArmRegression Q₀ false z) ∂Q := by have hr (d : Bool) := integral_weighted_observed_residual Q₀ Q d (C d) hY (hμ0 d) (hinv d) (hp d) have hratio (d : Bool) : ∫ z, observedPropensity Q d z / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z) ∂Q = ∫ z, observedArmRegression Q d z - observedArmRegression Q₀ d z ∂Q + ∫ z, (observedPropensity Q d z - observedPropensity Q₀ d z) / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z) ∂Q := by calc _ = ∫ z, (observedArmRegression Q d z - observedArmRegression Q₀ d z) + (observedPropensity Q d z - observedPropensity Q₀ d z) / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z) ∂Q := by apply integral_congr_ae filter_upwards [hp0 d] with z hz field_simp ring _ = _ := integral_add ((hμ1 d).sub (hμ0 d)) (hprod d) unfold observedATE observedAIPW have hconst : Integrable (fun _ : γ × Bool × ℝ => observedATE Q₀) Q := integrable_const _ integral_linearity rw [integral_const, probReal_univ, one_smul] rw [hr true, hr false, hratio true, hratio false] rw [integral_sub (hμ1 true) (hμ0 true), integral_sub (hμ1 false) (hμ0 false)] rw [show observedATE Q₀ = ∫ z, observedArmRegression Q₀ true z - observedArmRegression Q₀ false z ∂Q₀ from rfl] change _ - (∫ z, observedArmRegression Q₀ true z - observedArmRegression Q₀ false z ∂Q₀) - _ = _ ring
6 supporting declarations (lemmas, instances)
Von­Mises 1 core · 0 supporting This module packages the generic analytic step behind influence-function calculations: a first-order von Mises expansion whose remainder is locally quadratic along a bounded exponential tilt differentiates to the covaria ★ hasDerivAt_tilt_of_quadratic_vonMises_remainder

Von Mises remainders imply bounded-tilt pathwise derivatives

This module packages the generic analytic step behind influence-function calculations: a first-order von Mises expansion whose remainder is locally quadratic along a bounded exponential tilt differentiates to the covariance of the expansion's representer with the tilt score.

Reference: Kennedy (2024), Semiparametric doubly robust targeted double machine learning: a review.

theorem hasDerivAt_tilt_of_quadratic_vonMises_remainder reviewed
Causalean.Estimation.Efficiency

Quadratic von Mises remainder recipe. Given a probability law P, a law functional ψ, a square-integrable first-order representer φ, and a measurable bounded mean-zero tilt score g, suppose the von Mises expansion error along that tilt is eventually bounded by C t². Then t ↦ ψ(tiltMeasure P g t) has derivative ∫ φg dP at zero.

Formal statement
Z :
Type u_1
shared
ψ :
Measure Z → ℝ
φ g :
Z → ℝ
M C :
ℝ
hφ :
MemLp φ 2 P
hg_meas :
hgM :
∀ z, |g z| ≤ M
hg_mean :
∫ z, g z ∂P = 0
hrem :
∀ᶠ t in 𝓝 (0 : ℝ), |ψ (tiltMeasure P g t)
- ψ P
- ((∫ z, φ z ∂(tiltMeasure P g t)) - ∫ z, φ z ∂P)|
≤ C * t ^ 2
HasDerivAt (fun t => ψ (tiltMeasure P g t)) (∫ z, φ z * g z ∂P) 0
Proof (Lean source)
theorem hasDerivAt_tilt_of_quadratic_vonMises_remainder (P : Measure Z) [IsProbabilityMeasure P] (ψ : Measure Z → ℝ) (φ g : Z → ℝ) (M C : ℝ) (hφ : MemLp φ 2 P) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hg_mean : ∫ z, g z ∂P = 0) (hrem : ∀ᶠ t in 𝓝 (0 : ℝ), |ψ (tiltMeasure P g t) - ψ P - ((∫ z, φ z ∂(tiltMeasure P g t)) - ∫ z, φ z ∂P)| ≤ C * t ^ 2) : HasDerivAt (fun t => ψ (tiltMeasure P g t)) (∫ z, φ z * g z ∂P) 0 := by let F : ℝ → ℝ := fun t => ψ (tiltMeasure P g t) let A : ℝ → ℝ := fun t => (∫ z, φ z ∂(tiltMeasure P g t)) - ∫ z, φ z ∂P let R : ℝ → ℝ := fun t => F t - F 0 - A t have hR0 : R 0 = 0 := by simp [R, F, A, tiltMeasure_zero] have hquad : ∀ᶠ t in 𝓝 (0 : ℝ), |R t| ≤ C * t ^ 2 := by filter_upwards [hrem] with t ht simpa [R, F, A, tiltMeasure_zero] using ht have hbig : R =O[𝓝 (0 : ℝ)] fun t : ℝ => t ^ 2 := by refine IsBigO.of_bound (|C| + 1) ?_ filter_upwards [hquad] with t ht rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (sq_nonneg t)] exact ht.trans (mul_le_mul_of_nonneg_right (le_trans (le_abs_self C) (le_add_of_nonneg_right zero_le_one)) (sq_nonneg t)) have hsmall : R =o[𝓝 (0 : ℝ)] fun t : ℝ => t := hbig.trans_isLittleO (isLittleO_pow_id (by norm_num : 1 < 2)) have hRderiv : HasDerivAt R 0 0 := by rw [hasDerivAt_iff_isLittleO] simpa [hR0] using hsmall have hAderiv : HasDerivAt A (∫ z, φ z * g z ∂P) 0 := by dsimp only [A] exact (hasDerivAt_integral_tiltMeasure_of_memLp hg_meas hgM hg_mean hφ).sub_const (∫ z, φ z ∂P) have hsum := (hRderiv.add_const (F 0)).add hAderiv have heq : F = fun t => R t + F 0 + A t := by funext t dsimp [R] ring rw [show (fun t => ψ (tiltMeasure P g t)) = F from rfl, heq] change HasDerivAt ((fun x => R x + F 0) + A) (∫ z, φ z * g z ∂P) 0 simpa only [zero_add] using hsum
Causalean.Estimation.Efficiency.hasDerivAt_tilt_of_quadratic_vonMises_remainder · Causalean/Estimation/Efficiency/VonMises.lean:32 · uses tiltMeasure