Estimation.Efficiency
Semiparametric efficiency: tangent spaces, pathwise differentiability, and the efficiency bound for the ATE functional.
TangentProjection 6 core · 8 supporting This file develops the Hilbert-space geometry behind semiparametric efficiency: gradients are compared along a tangent subspace, the efficient influence function is the orthogonal projection onto that subspace, and the e ★ normSq_gradient_decomp★ effBound_le_normSq★ norm_eq_iff_eq_efficientIF
Tangent-Space Projection for Efficiency
This file develops the Hilbert-space geometry behind semiparametric efficiency: gradients are compared along a tangent subspace, the efficient influence function is the orthogonal projection onto that subspace, and the efficiency bound is its squared norm. It also proves the abstract tangent-shrinking principle used in the Hahn efficiency formalization.
def IsGradient reviewed
⚑ flagged
Causalean.Estimation.Efficiency
ψ is a gradient of g relative to the tangent space T when its inner product against every tangent direction matches that of g. In semiparametric models g is a reference influence function and the gradients are exactly the influence functions of regular asymptotically linear estimators.
Definition (Lean source)
def IsGradient (T : Submodule ℝ H) (g ψ : H) : Prop :=
∀ s ∈ T, ⟪ψ, s⟫_ℝ = ⟪g, s⟫_ℝ
def efficientIF reviewed
⚑ flagged
Causalean.Estimation.Efficiency
The efficient influence function: the orthogonal projection of the reference gradient g onto the tangent space T, coerced back into H.
Definition (Lean source)
noncomputable def efficientIF (T : Submodule ℝ H) [T.HasOrthogonalProjection]
(g : H) : H :=
(T.orthogonalProjection g : H)
def effBound reviewed
⚑ flagged
Causalean.Estimation.Efficiency
The semiparametric efficiency bound: the squared norm of the efficient influence function.
theorem normSq_gradient_decomp reviewed
⚑ flagged
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
hypotheses
g ψ :
H
h :
IsGradient T g ψ
conclusion
‖ψ‖ ^ 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
theorem effBound_le_normSq reviewed
⚑ flagged
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
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
theorem norm_eq_iff_eq_efficientIF reviewed
⚑ flagged
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
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
8 supporting declarations (lemmas, instances)
-
efficientIF_eq_starProjectiontheorem — efficientIF is the coerced star-projection (the projection seen as an endomorphism of H).Proof (Lean source)
-
efficientIF_memtheorem — The efficient influence function lies in the tangent space.Proof (Lean source)
theorem efficientIF_mem (g : H) : efficientIF T g ∈ T := (T.orthogonalProjection g).2 -
isGradient_iff_sub_mem_orthogonaltheorem — A vector is a gradient of g iff it differs from g by an element of the orthogonal complement of the tangent space.Proof (Lean source)
theorem isGradient_iff_sub_mem_orthogonal (g ψ : H) : IsGradient T g ψ ↔ ψ - g ∈ Tᗮ := by constructor · intro h rw [Submodule.mem_orthogonal] intro s hs rw [inner_sub_right, real_inner_comm ψ s, real_inner_comm g s, h s hs, sub_self] · intro h s hs rw [Submodule.mem_orthogonal] at h have hzero := h s hs rw [inner_sub_right, sub_eq_zero] at hzero rw [real_inner_comm s ψ, real_inner_comm s g, hzero] -
efficientIF_isGradienttheorem — The efficient influence function is itself a gradient of g.Proof (Lean source)
theorem efficientIF_isGradient (g : H) : IsGradient T g (efficientIF T g) := by intro s hs exact T.inner_orthogonalProjection_eq_of_mem_right ⟨s, hs⟩ g -
orthogonalProjection_eq_of_isGradienttheorem — A gradient ψ projects onto the same efficient influence function as g.Proof (Lean source)
theorem orthogonalProjection_eq_of_isGradient {g ψ : H} (h : IsGradient T g ψ) : (T.orthogonalProjection ψ : H) = efficientIF T g := by have hsub : ψ - g ∈ Tᗮ := (isGradient_iff_sub_mem_orthogonal g ψ).1 h have hz : T.orthogonalProjection (ψ - g) = 0 := T.orthogonalProjection_eq_zero_iff.mpr hsub have hlin : T.orthogonalProjection ψ - T.orthogonalProjection g = T.orthogonalProjection (ψ - g) := by rw [map_sub] rw [hz, sub_eq_zero] at hlin rw [efficientIF, hlin] -
efficientIF_uniquetheorem — A gradient that lies in the tangent space is the efficient influence function.Proof (Lean source)
theorem efficientIF_unique {g ψ : H} (h : IsGradient T g ψ) (hψ : ψ ∈ T) : ψ = efficientIF T g := by have hproj : (T.orthogonalProjection ψ : H) = efficientIF T g := orthogonalProjection_eq_of_isGradient h rw [← hproj] exact (T.starProjection_eq_self_iff.mpr hψ).symm -
efficientIF_eq_self_of_memtheorem — If the reference gradient already lies in the tangent space, the efficient influence function equals it.hypothesesconclusionefficientIF T g = gProof (Lean source)
theorem efficientIF_eq_self_of_mem (T : Submodule ℝ H) [T.HasOrthogonalProjection] {g : H} (hg : g ∈ T) : efficientIF T g = g := by rw [efficientIF_eq_starProjection] exact T.starProjection_eq_self_iff.mpr hg -
effBound_eq_of_mem_subtheorem — Tangent-shrinking corollary. If the reference influence function lies in the smaller tangent space T' ≤ T, then both the smaller and larger tangent spaces leave it fixed, so the efficiency bound is unchanged. Interpretation: knowing the propensity score shrinks the tangent space, but if ψ_AIPW already lives in the smaller space the efficiency bound does not move.hypothesesT T' :Submodule ℝ HT.HasOrthogonalProjectionT'.HasOrthogonalProjectionhle :T' ≤ Tg :Hhg :g ∈ T'conclusionProof (Lean source)
theorem effBound_eq_of_mem_sub (T T' : Submodule ℝ H) [T.HasOrthogonalProjection] [T'.HasOrthogonalProjection] (hle : T' ≤ T) {g : H} (hg : g ∈ T') : efficientIF T' g = g ∧ efficientIF T g = g ∧ effBound T' g = effBound T g := by have h1 : efficientIF T' g = g := efficientIF_eq_self_of_mem T' hg have h2 : efficientIF T g = g := efficientIF_eq_self_of_mem T (hle hg) exact ⟨h1, h2, by rw [effBound, effBound, h1, h2]⟩
ATETangent 6 core · 10 supporting This module proves that the augmented inverse-probability weighted score is orthogonal to propensity-score nuisance directions and records its projection properties in the Hilbert space Lp ℝ 2 S.P_Z. ★ effBound_eq_variance★ effBound_eq_hahn★ efficiency_bound_optimal
ATE tangent-space efficiency identities
This module proves that the augmented inverse-probability weighted score is
orthogonal to propensity-score nuisance directions and records its projection
properties in the Hilbert space Lp ℝ 2 S.P_Z. The theorem
BackdoorEstimationSystem.aipw_orthogonal_propensity_score formalizes Hahn's
propensity-score orthogonality calculation.
The second half builds the full mean-zero tangent space Tfull, represents the
AIPW score as aipwLp, proves aipwLp_mem_tangent, and derives the projection
and variance identities effBound_eq_variance, effBound_eq_hahn, and
efficiency_bound_optimal. The final tangent-shrinking theorem states the
abstract known-propensity corollary for any supplied smaller tangent space that
still contains the AIPW score. The pathwise-gradient/canonical-gradient bridge
is developed in ATEEfficientIF.lean.
def aipwLp reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
This is the AIPW influence function represented as a point of the square-integrable Hilbert space.
Definition (Lean source)
noncomputable def aipwLp (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 :=
(S.aipw_memLp h_overlap hA h_y2 h_yd2).toLp _
def oneLp reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
This is the constant-one function represented in the square-integrable Hilbert space.
def Tfull reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
This is the mean-zero tangent space for the backdoor average treatment effect.
theorem effBound_eq_variance reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Semiparametric efficiency bound equals the AIPW variance. 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 semiparametric efficiency bound for the backdoor ATE, computed against the full mean-zero tangent space, equals the second moment of the AIPW influence function ψ_AIPW under the observed-data law P_Z.
Formal statement
hypotheses
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.μ
conclusion
effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) = ∫ z, (S.ψ_AIPW z) ^ 2 ∂S.P_Z
Proof (Lean source)
theorem effBound_eq_variance (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]
theorem effBound_eq_hahn reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
Semiparametric efficiency bound 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 semiparametric efficiency bound for the backdoor ATE 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
hypotheses
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.μ
conclusion
effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2)
Proof (Lean source)
theorem effBound_eq_hahn (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.effBound_eq_variance h_overlap hA h_y2 h_yd2,
S.aipw_variance_hahn_decomposition h_overlap hA h_y2 h_yd2]
theorem efficiency_bound_optimal reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
The efficiency bound lower-bounds every 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 semiparametric efficiency bound is at most the squared L² norm of ψ.
Formal statement
hypotheses
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) ψ
conclusion
effBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) ≤ ‖ψ‖ ^ 2
Proof (Lean source)
theorem efficiency_bound_optimal (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ψ
10 supporting declarations (lemmas, instances)
-
propensity_score_residual_integral_zerolemma — Any covariate-measurable multiplier has zero integral against the propensity-score residual.hypothesesS :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.μconclusion∫ ω, h (S.toPOBackdoorSystem.factualX ω) * (S.toPOBackdoorSystem.dVar.indicator true ω - S.e_val (S.toPOBackdoorSystem.factualX ω)) ∂P.μ= 0Proof (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 _ _ -
aipw_orthogonal_propensity_scoretheorem — The role of the propensity score (Hahn).hypothesesS :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.μ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 -
instIsProbabilityMeasure_P_Zinstance — The observed data law of a backdoor estimation system is a probability measure.instance instIsProbabilityMeasure_P_Z (S : ATE.BackdoorEstimationSystem P γ) : IsProbabilityMeasure S.P_Z := by rw [ATE.BackdoorEstimationSystem.P_Z] haveI : IsProbabilityMeasure P.μ := P.isProb exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable -
aipw_memLptheorem — The AIPW influence function is square-integrable under the observed data law.hypothesesS :ATE.BackdoorEstimationSystem P γε :ℝh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μconclusionMemLp S.ψ_AIPW 2 S.P_ZProof (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) -
instHasOrthogonalProjection_span_oneLpinstance — The span of the constant-one function has an orthogonal projection.instance instHasOrthogonalProjection_span_oneLp (S : ATE.BackdoorEstimationSystem P γ) : (ℝ ∙ S.oneLp).HasOrthogonalProjection := by have : FiniteDimensional ℝ (ℝ ∙ S.oneLp) := inferInstance exact inferInstance -
instHasOrthogonalProjection_Tfullinstance — The mean-zero tangent space has an orthogonal projection.instance instHasOrthogonalProjection_Tfull (S : ATE.BackdoorEstimationSystem P γ) : (S.Tfull).HasOrthogonalProjection := by rw [Tfull] exact Submodule.instHasOrthogonalProjectionOrthogonal (ℝ ∙ S.oneLp) -
inner_oneLptheorem — Inner product against the constant-one function equals integration under the observed data law.hypothesesS :ATE.BackdoorEstimationSystem P γf :Lp ℝ 2 S.P_Zconclusion⟪f, S.oneLp⟫_ℝ = ∫ z, f z ∂S.P_ZProof (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] -
aipwLp_mem_tangenttheorem — The AIPW influence function lies in the mean-zero tangent space.hypothesesS :ATE.BackdoorEstimationSystem P γε :ℝh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μconclusionS.aipwLp h_overlap hA h_y2 h_yd2 ∈ S.TfullProof (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 -
aipw_score_meanZero_projection_eqtheorem — The square-integrable AIPW score is already mean-zero, so projecting it onto the full mean-zero tangent space leaves it unchanged.hypothesesS :ATE.BackdoorEstimationSystem P γε :ℝh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μconclusionefficientIF S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) = S.aipwLp h_overlap hA h_y2 h_yd2Proof (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) -
effBound_eq_of_smaller_tangent_containing_aipwtheorem — 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.hypothesesS :ATE.BackdoorEstimationSystem P γε :ℝh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μT'.HasOrthogonalProjectionhle :T' ≤ S.Tfullhmem :S.aipwLp h_overlap hA h_y2 h_yd2 ∈ T'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
PathwiseGradient 6 core · 7 supporting This is the abstract pathwise-gradient / regular-submodel layer that upgrades the projection algebra of Causalean.Estimation.Efficiency.TangentProjection (IsGradient, efficientIF) into the genuine Hahn (1998) statement: ★ orthogonalProjection_isPathwiseGradient
Regular submodels and pathwise gradients (abstract semiparametric layer)
This is the abstract pathwise-gradient / regular-submodel layer that upgrades
the projection algebra of Causalean.Estimation.Efficiency.TangentProjection
(IsGradient, efficientIF) into the genuine Hahn (1998) statement: an influence
function is the efficient influence function when it is the canonical
(projected) pathwise gradient of the target functional along every regular
submodel.
Fix a real Hilbert space H (in applications Lp ℝ 2 P), a distinguished vector
one : H (in applications the constant function, so mean-zero means
⟪·, one⟫ = 0), and a base law P₀ : 𝓛 in an abstract type of laws 𝓛 on which
functionals ψ : 𝓛 → ℝ are evaluated.
* RegularSubmodel one P₀ packages a one-parameter path of laws t ↦ path t
through P₀ at t = 0, together with a mean-zero L² score s ∈ H (the
tangent direction). The path and score are abstract fields: we never build
parametric families from raw measures here.
* IsPathwiseGradient one P₀ ψ g says g represents the derivative of ψ along
every submodel: t ↦ ψ (path t) is differentiable at 0 with derivative
⟪g, s⟫.
* IsTangentSpace one P₀ T says the closed subspace T is a genuine tangent
space: it contains every score and is contained in the closure of their span
(so T equals the closed span of the score set).
The main results: the orthogonal projection of any pathwise gradient onto a
tangent space T is again a pathwise gradient (orthogonalProjection_isPathwiseGradient);
all pathwise gradients share the same projection onto T
(efficientIF_eq_of_isPathwiseGradient); hence a pathwise gradient lying in T
is the unique such and equals efficientIF T g for every gradient g
(isPathwiseGradient_eq_efficientIF_of_mem) — the efficient influence function is
well-defined as the canonical gradient.
Reference: Hahn (1998, Econometrica); Bickel–Klaassen–Ritov–Wellner (1993); Tsiatis (2006), Ch. 3; van der Vaart (1998), Ch. 25.
structure RegularSubmodel reviewed
⚑ flagged
Causalean.Estimation.Efficiency
A regular submodel through the base law P₀ bundles a one-parameter path of laws, indexed by a real perturbation parameter, that passes through P₀ at parameter zero, together with its tangent direction, an L² score vector required to be mean-zero, i.e. orthogonal to the distinguished vector one.
Definition (Lean source)
parameters
one :
H
P₀ :
𝓛
fields
The one-parameter path of laws.
path :
ℝ → 𝓛
The path passes through the base law at parameter `0`.
path_zero :
path 0 = P₀
The L² score (tangent direction) of the submodel.
score :
H
The score is mean-zero: orthogonal to the distinguished vector `one`.
score_meanZero :
⟪score, one⟫_ℝ = 0
def scoreSet reviewed
⚑ flagged
Causalean.Estimation.Efficiency
The set of all submodel scores (tangent directions) through P₀.
Definition (Lean source)
def tangentSpace reviewed
⚑ flagged
Causalean.Estimation.Efficiency
The tangent space generated by the regular submodels through P₀: the topological closure of the linear span of the score set.
Definition (Lean source)
noncomputable def tangentSpace (one : H) (P₀ : 𝓛) : Submodule ℝ H :=
(span ℝ (scoreSet one P₀)).topologicalClosure
structure IsTangentSpace reviewed
⚑ flagged
Causalean.Estimation.Efficiency
A candidate closed subspace T of the Hilbert space is a genuine tangent space for the regular submodels through the base law P₀ when every submodel's score lies in T and T is contained in the closed linear span of all submodel scores — together these force T to equal that closed span, the tangent space generated by the available parametric perturbations.
Definition (Lean source)
parameters
fields
Every submodel score lies in `T`.
scores_mem :
∀ m : RegularSubmodel one P₀, m.score ∈ T
`T` is contained in the closed span of the score set.
le_closure :
T ≤ tangentSpace one P₀
def IsPathwiseGradient reviewed
⚑ flagged
Causalean.Estimation.Efficiency
g : H is a pathwise gradient of the functional ψ : 𝓛 → ℝ at P₀: along every regular submodel, t ↦ ψ (path t) is differentiable at 0 with derivative ⟪g, score⟫. This is the abstract semiparametric characterization of an influence function as the pathwise derivative of the target functional.
Definition (Lean source)
def IsPathwiseGradient (one : H) (P₀ : 𝓛) (ψ : 𝓛 → ℝ) (g : H) : Prop :=
∀ m : RegularSubmodel one P₀,
HasDerivAt (fun t => ψ (m.path t)) (⟪g, m.score⟫_ℝ) 0
theorem orthogonalProjection_isPathwiseGradient reviewed
⚑ flagged
Causalean.Estimation.Efficiency
The projection of a pathwise gradient is a pathwise gradient. Suppose T is a tangent space for the regular submodels through the base law P₀, and suppose g reproduces the pathwise derivative of the functional ψ along every such submodel — it is a pathwise gradient of ψ at P₀. Then the orthogonal projection of g onto T, written efficientIF T g, is again a pathwise gradient of ψ.
Formal statement
hypotheses
conclusion
IsPathwiseGradient one P₀ ψ (efficientIF T g)
Proof (Lean source)
theorem orthogonalProjection_isPathwiseGradient {one : H} {P₀ : 𝓛} {ψ : 𝓛 → ℝ}
{g : H} (hT : IsTangentSpace one P₀ T) (hg : IsPathwiseGradient one P₀ ψ g) :
IsPathwiseGradient one P₀ ψ (efficientIF T g) := by
intro m
have hinner : ⟪efficientIF T g, m.score⟫_ℝ = ⟪g, m.score⟫_ℝ := by
rw [efficientIF]
exact T.inner_orthogonalProjection_eq_of_mem_right ⟨m.score, hT.scores_mem m⟩ g
simpa [hinner] using hg m
7 supporting declarations (lemmas, instances)
-
inner_score_eq_of_isPathwiseGradienttheorem — Two pathwise gradients of the same functional pair identically with every submodel score: ⟪g, s⟫ = ⟪g', s⟫. (Both equal the pathwise derivative d/dt ψ(path t)|₀, which is unique.)hypothesesone :HP₀ :𝓛ψ :𝓛 → ℝg g' :Hhg :IsPathwiseGradient one P₀ ψ ghg' :IsPathwiseGradient one P₀ ψ g'm :RegularSubmodel one P₀conclusion⟪g, m.score⟫_ℝ = ⟪g', m.score⟫_ℝProof (Lean source)
theorem inner_score_eq_of_isPathwiseGradient {one : H} {P₀ : 𝓛} {ψ : 𝓛 → ℝ} {g g' : H} (hg : IsPathwiseGradient one P₀ ψ g) (hg' : IsPathwiseGradient one P₀ ψ g') (m : RegularSubmodel one P₀) : ⟪g, m.score⟫_ℝ = ⟪g', m.score⟫_ℝ := (hg m).unique (hg' m) -
inner_sub_score_eq_zero_of_isPathwiseGradienttheorem — The difference of two pathwise gradients is orthogonal to every submodel score.hypothesesone :HP₀ :𝓛ψ :𝓛 → ℝg g' :Hhg :IsPathwiseGradient one P₀ ψ ghg' :IsPathwiseGradient one P₀ ψ g'm :RegularSubmodel one P₀conclusion⟪g - g', m.score⟫_ℝ = 0Proof (Lean source)
theorem inner_sub_score_eq_zero_of_isPathwiseGradient {one : H} {P₀ : 𝓛} {ψ : 𝓛 → ℝ} {g g' : H} (hg : IsPathwiseGradient one P₀ ψ g) (hg' : IsPathwiseGradient one P₀ ψ g') (m : RegularSubmodel one P₀) : ⟪g - g', m.score⟫_ℝ = 0 := by rw [inner_sub_left, inner_score_eq_of_isPathwiseGradient hg hg' m, sub_self] -
sub_mem_orthogonal_of_isPathwiseGradienttheorem — The difference of two pathwise gradients lies in the orthogonal complement of any tangent space T.hypothesesone :HP₀ :𝓛ψ :𝓛 → ℝg g' :HT :Submodule ℝ HhT :IsTangentSpace one P₀ Thg :IsPathwiseGradient one P₀ ψ ghg' :IsPathwiseGradient one P₀ ψ g'conclusiong - g' ∈ TᗮProof (Lean source)
theorem sub_mem_orthogonal_of_isPathwiseGradient {one : H} {P₀ : 𝓛} {ψ : 𝓛 → ℝ} {g g' : H} {T : Submodule ℝ H} (hT : IsTangentSpace one P₀ T) (hg : IsPathwiseGradient one P₀ ψ g) (hg' : IsPathwiseGradient one P₀ ψ g') : g - g' ∈ Tᗮ := by apply Submodule.orthogonal_le hT.le_closure rw [tangentSpace, Submodule.orthogonal_closure] rw [Submodule.mem_orthogonal'] intro u hu let Z : Submodule ℝ H := { carrier := {v | ⟪g - g', v⟫_ℝ = 0} zero_mem' := by simp add_mem' := by intro v w hv hw change ⟪g - g', v + w⟫_ℝ = 0 rw [inner_add_right, hv, hw, add_zero] smul_mem' := by intro a v hv change ⟪g - g', a • v⟫_ℝ = 0 rw [inner_smul_right, hv, mul_zero] } have hspan : span ℝ (scoreSet one P₀) ≤ Z := by rw [Submodule.span_le] rintro x ⟨m, rfl⟩ exact inner_sub_score_eq_zero_of_isPathwiseGradient hg hg' m exact hspan hu -
isGradient_of_isPathwiseGradienttheorem — Two pathwise gradients differ by an orthogonal-complement element, i.e. either is a TangentProjection-gradient of the other relative to any tangent space T. This is the bridge from the pathwise (HasDerivAt) layer to the inner product IsGradient algebra of TangentProjection.lean.hypothesesone :HP₀ :𝓛ψ :𝓛 → ℝg g' :HT :Submodule ℝ HhT :IsTangentSpace one P₀ Thg :IsPathwiseGradient one P₀ ψ ghg' :IsPathwiseGradient one P₀ ψ g'conclusionIsGradient T g g'Proof (Lean source)
theorem isGradient_of_isPathwiseGradient {one : H} {P₀ : 𝓛} {ψ : 𝓛 → ℝ} {g g' : H} {T : Submodule ℝ H} (hT : IsTangentSpace one P₀ T) (hg : IsPathwiseGradient one P₀ ψ g) (hg' : IsPathwiseGradient one P₀ ψ g') : IsGradient T g g' := (isGradient_iff_sub_mem_orthogonal g g').2 (sub_mem_orthogonal_of_isPathwiseGradient hT hg' hg) -
efficientIF_eq_of_isPathwiseGradienttheorem — All pathwise gradients share the same projection onto a tangent space. Hence the efficient influence function efficientIF T g does not depend on the chosen pathwise gradient g: it is the canonical gradient.hypothesesone :HP₀ :𝓛ψ :𝓛 → ℝg g' :HhT :IsTangentSpace one P₀ Thg :IsPathwiseGradient one P₀ ψ ghg' :IsPathwiseGradient one P₀ ψ g'conclusionefficientIF T g = efficientIF T g'Proof (Lean source)
theorem efficientIF_eq_of_isPathwiseGradient {one : H} {P₀ : 𝓛} {ψ : 𝓛 → ℝ} {g g' : H} (hT : IsTangentSpace one P₀ T) (hg : IsPathwiseGradient one P₀ ψ g) (hg' : IsPathwiseGradient one P₀ ψ g') : efficientIF T g = efficientIF T g' := by have hgrad : IsGradient T g g' := isGradient_of_isPathwiseGradient hT hg hg' have hproj : (T.orthogonalProjection g' : H) = efficientIF T g := orthogonalProjection_eq_of_isGradient hgrad simpa [efficientIF] using hproj.symm -
isPathwiseGradient_eq_efficientIF_of_memtheorem — The efficient influence function is the unique pathwise gradient in T. If g is any pathwise gradient and g' is a pathwise gradient lying in the tangent space T, then g' = efficientIF T g. Thus a pathwise gradient inside T is uniquely determined and equals the projection of every gradient — the efficient influence function / canonical gradient.hypothesesone :HP₀ :𝓛ψ :𝓛 → ℝg g' :HhT :IsTangentSpace one P₀ Thg :IsPathwiseGradient one P₀ ψ ghg' :IsPathwiseGradient one P₀ ψ g'hmem :g' ∈ Tconclusiong' = efficientIF T gProof (Lean source)
theorem isPathwiseGradient_eq_efficientIF_of_mem {one : H} {P₀ : 𝓛} {ψ : 𝓛 → ℝ} {g g' : H} (hT : IsTangentSpace one P₀ T) (hg : IsPathwiseGradient one P₀ ψ g) (hg' : IsPathwiseGradient one P₀ ψ g') (hmem : g' ∈ T) : g' = efficientIF T g := by exact efficientIF_unique (isGradient_of_isPathwiseGradient hT hg hg') hmem -
efficientIF_eq_self_of_isPathwiseGradient_memtheorem — A pathwise gradient lying in T equals its own projection. This recovers efficientIF_eq_self_of_mem, now as a corollary of "g is the efficient influence function": a gradient already in the tangent space is the canonical gradient.hypothesesone :HP₀ :𝓛ψ :𝓛 → ℝg :HhT :IsTangentSpace one P₀ Thg :IsPathwiseGradient one P₀ ψ ghmem :g ∈ TconclusionefficientIF T g = gProof (Lean source)
theorem efficientIF_eq_self_of_isPathwiseGradient_mem {one : H} {P₀ : 𝓛} {ψ : 𝓛 → ℝ} {g : H} (hT : IsTangentSpace one P₀ T) (hg : IsPathwiseGradient one P₀ ψ g) (hmem : g ∈ T) : efficientIF T g = g := (isPathwiseGradient_eq_efficientIF_of_mem hT hg hg hmem).symm
ATEEfficientIF 1 core · 4 supporting This module connects the abstract pathwise-gradient layer to the backdoor ATE system. ★ aipw_is_efficientInfluenceFunction
AIPW as the efficient influence function for the backdoor ATE
This module connects the abstract pathwise-gradient layer to the backdoor ATE
system. It first rewrites the Hilbert-space inner product against aipwLp as
the covariance pairing with ψ_AIPW, then proves that regular submodel scores
belong to the full mean-zero tangent space Tfull.
Under an explicit Hahn pathwise-derivative identity and an explicit
nonparametric tangent-space hypothesis, aipw_isPathwiseGradient_ATE proves
that the AIPW score is a pathwise gradient of the ATE functional, and
aipw_is_efficientInfluenceFunction proves that this AIPW score is the
canonical efficient influence function in the mean-zero tangent space.
theorem aipw_is_efficientInfluenceFunction reviewed
⚑ flagged
Causalean.Estimation.ATE.BackdoorEstimationSystem
AIPW is the efficient influence function for the backdoor ATE. 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. Suppose a functional ψ of the observed-data law satisfies Hahn's pathwise-derivative identity — along every regular submodel, ψ's derivative at the true law equals the covariance of the AIPW score with the submodel's score, and that the full mean-zero space is a genuine nonparametric tangent space, i.e. it is contained in the closed span of regular-submodel scores. Then the AIPW influence function is a pathwise gradient of ψ, lies in the full mean-zero tangent space, and is the canonical efficient influence function: for every other pathwise gradient g of ψ, projecting g onto the tangent space returns the AIPW influence function.
Formal statement
hypotheses
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.μ
hHahn :
∀ m : RegularSubmodel S.oneLp S.P_Z,
HasDerivAt (fun t => ψ (m.path t)) (∫ z, S.ψ_AIPW z * (m.score z) ∂S.P_Z) 0
hdense :
S.Tfull ≤ tangentSpace S.oneLp S.P_Z
conclusion
IsPathwiseGradient S.oneLp S.P_Z ψ (S.aipwLp h_overlap hA h_y2 h_yd2) ∧
S.aipwLp h_overlap hA h_y2 h_yd2 ∈ S.Tfull ∧
∀ g,
IsPathwiseGradient S.oneLp S.P_Z ψ g → efficientIF S.Tfull g
= S.aipwLp h_overlap hA h_y2 h_yd2
Proof (Lean source)
theorem aipw_is_efficientInfluenceFunction (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.μ)
(ψ : Measure (γ × Bool × ℝ) → ℝ)
(hHahn : ∀ m : RegularSubmodel S.oneLp S.P_Z,
HasDerivAt (fun t => ψ (m.path t))
(∫ z, S.ψ_AIPW z * (m.score z) ∂S.P_Z) 0)
(hdense : S.Tfull ≤ tangentSpace S.oneLp S.P_Z) :
IsPathwiseGradient S.oneLp S.P_Z ψ (S.aipwLp h_overlap hA h_y2 h_yd2)
∧ S.aipwLp h_overlap hA h_y2 h_yd2 ∈ S.Tfull
∧ ∀ g, IsPathwiseGradient S.oneLp S.P_Z ψ g →
efficientIF S.Tfull g = S.aipwLp h_overlap hA h_y2 h_yd2 := by
have hgrad := S.aipw_isPathwiseGradient_ATE h_overlap hA h_y2 h_yd2 ψ hHahn
have hmem := S.aipwLp_mem_tangent h_overlap hA h_y2 h_yd2
have hT := S.isTangentSpace_Tfull hdense
refine ⟨hgrad, hmem, fun g hg => ?_⟩
exact (isPathwiseGradient_eq_efficientIF_of_mem hT hg hgrad hmem).symm
4 supporting declarations (lemmas, instances)
-
inner_aipwLp_eq_integraltheorem — The covariance pairing between the AIPW influence function and any square-integrable score equals the Hilbert-space inner product against the AIPW element in the observed-data square-integrable space.hypothesesS :ATE.BackdoorEstimationSystem P γε :ℝh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μf :Lp ℝ 2 S.P_Zconclusion⟪S.aipwLp h_overlap hA h_y2 h_yd2, f⟫_ℝ = ∫ z, S.ψ_AIPW z * f z ∂S.P_ZProof (Lean source)
theorem inner_aipwLp_eq_integral (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.μ) (f : Lp ℝ 2 S.P_Z) : ⟪S.aipwLp h_overlap hA h_y2 h_yd2, f⟫_ℝ = ∫ z, S.ψ_AIPW z * f z ∂S.P_Z := by rw [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] -
score_mem_Tfulltheorem — Every regular submodel score is mean-zero, so every such score belongs to the full nonparametric tangent space for the observed-data law.hypothesesS :ATE.BackdoorEstimationSystem P γm :RegularSubmodel S.oneLp S.P_Zconclusionm.score ∈ S.TfullProof (Lean source)
theorem score_mem_Tfull (S : ATE.BackdoorEstimationSystem P γ) (m : RegularSubmodel S.oneLp S.P_Z) : m.score ∈ S.Tfull := by rw [Tfull, Submodule.mem_orthogonal_singleton_iff_inner_left] exact m.score_meanZero -
isTangentSpace_Tfulltheorem — The full mean-zero space is a genuine tangent space once the supplied nonparametric-model hypothesis says it is contained in the closed span of regular-submodel scores.hypothesesS :ATE.BackdoorEstimationSystem P γhdense :S.Tfull ≤ tangentSpace S.oneLp S.P_ZconclusionIsTangentSpace S.oneLp S.P_Z S.Tfull where scores_mem mProof (Lean source)
theorem isTangentSpace_Tfull (S : ATE.BackdoorEstimationSystem P γ) (hdense : S.Tfull ≤ tangentSpace S.oneLp S.P_Z) : IsTangentSpace S.oneLp S.P_Z S.Tfull where scores_mem m := S.score_mem_Tfull m le_closure := hdense -
aipw_isPathwiseGradient_ATEtheorem — Hahn's pathwise-derivative identity makes the AIPW score a pathwise gradient of the backdoor ATE functional along every regular submodel.hypothesesS :ATE.BackdoorEstimationSystem P γε :ℝh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μhHahn :∀ m : RegularSubmodel S.oneLp S.P_Z,HasDerivAt (fun t => ψ (m.path t)) (∫ z, S.ψ_AIPW z * (m.score z) ∂S.P_Z) 0conclusionIsPathwiseGradient S.oneLp S.P_Z ψ (S.aipwLp h_overlap hA h_y2 h_yd2)Proof (Lean source)
theorem aipw_isPathwiseGradient_ATE (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.μ) (ψ : Measure (γ × Bool × ℝ) → ℝ) (hHahn : ∀ m : RegularSubmodel S.oneLp S.P_Z, HasDerivAt (fun t => ψ (m.path t)) (∫ z, S.ψ_AIPW z * (m.score z) ∂S.P_Z) 0) : IsPathwiseGradient S.oneLp S.P_Z ψ (S.aipwLp h_overlap hA h_y2 h_yd2) := by intro m rw [S.inner_aipwLp_eq_integral h_overlap hA h_y2 h_yd2 m.score] exact hHahn m
ATEVariance 2 core · 0 supporting This module develops the L² and variance algebra behind the Hahn (1998) semiparametric efficiency bound for the backdoor ATE. ★ aipw_variance_hahn_decomposition★ dml_ATE_attains_hahn_bound
Hahn variance decomposition for the AIPW influence function
This module develops the L² and variance algebra behind the Hahn (1998)
semiparametric efficiency bound 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 theorem dml_ATE_attains_hahn_bound rewrites the limiting
variance in the one-shot DML central-limit theorem by this Hahn decomposition.
theorem aipw_variance_hahn_decomposition reviewed
⚑ flagged
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 Hahn semiparametric efficiency bound V_H.
Formal statement
hypotheses
S :
ε :
ℝ
h_overlap :
S.StrictOverlap ε
hA :
S.toPOBackdoorSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
h_yd2 :
∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ
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 …
theorem dml_ATE_attains_hahn_bound reviewed
⚑ flagged
Causalean.Estimation.ATE
The one-shot DML ATE attains the Hahn efficiency bound. 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 training-fold share converges to a limit c strictly between 0 and 1. 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 a measurable function of the training fold alone, 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 is the Hahn semiparametric efficiency bound.
Formal statement
hypotheses
S :
ε :
ℝ
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.μ
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
hc_lt :
c < 1
μ_hat :
ℕ → P.Ω → (Bool → γ → ℝ)
e_hat :
ℕ → P.Ω → (γ → ℝ)
h_mu_meas :
∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
h_e_meas :
∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
h_mu_memLp :
∀ n ω a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X
h_e_memLp :
∀ n ω, MemLp (fun x => e_hat n ω x) 2 S.P_X
h_e_overlap :
∀ n ω, ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε
h_mu_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (μ_hat n)
h_e_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (e_hat n)
h_mu_uncurry_foldA :
∀ n a,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2)
h_e_uncurry_foldA :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace γ)] (fun (p : P.Ω × γ) => e_hat n p.1 p.2)
h_mu_rate :
∀ a : Bool,
IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
h_e_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
h_product_rate :
∀ a : Bool,
IsLittleOp (fun n ω => (eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
hψ_meas :
Measurable (S.ψ_AIPW)
hθn_meas :
∀ n : ℕ,
AEMeasurable (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ
hSum_meas :
∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ
conclusion
Tendsto_dist (IsAsymLinear.rescaledEstimator (dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB) (gaussianMeasure 0 ((∫ x, (S.μ_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))) P.μ hθn_meas
Proof (Lean source)
theorem dml_ATE_attains_hahn_bound
(S : BackdoorEstimationSystem P γ)
{ε : ℝ}
(hA : S.toPOBackdoorSystem.Assumptions)
(h_overlap : S.StrictOverlap ε)
(h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ)
(h_yd2 : ∀ d : Bool, Integrable
(fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ)
(sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z)
(split : OneShotSplit sample)
{c : ℝ} (hc_pos : 0 < c) (hc_lt : c < 1)
(h_split_rate :
Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c))
(μ_hat : ℕ → P.Ω → (Bool → γ → ℝ))
(e_hat : ℕ → P.Ω → (γ → ℝ))
(h_mu_meas :
∀ n a, Measurable (fun (p : P.Ω × γ) => μ_hat n p.1 a p.2))
(h_e_meas :
∀ n, Measurable (fun (p : P.Ω × γ) => e_hat n p.1 p.2))
(h_mu_memLp :
∀ n ω a, MemLp (fun x => μ_hat n ω a x) 2 S.P_X)
(h_e_memLp :
∀ n ω, MemLp (fun x => e_hat n ω x) 2 S.P_X)
(h_e_overlap :
∀ n ω, ∀ᵐ x ∂S.P_X, ε ≤ e_hat n ω x ∧ e_hat n ω x ≤ 1 - ε)
(h_mu_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(μ_hat n))
(h_e_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(e_hat n))
(h_mu_uncurry_foldA :
∀ n a,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace γ)]
(fun (p : P.Ω × γ) => μ_hat n p.1 a p.2))
(h_e_uncurry_foldA :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace γ)]
(fun (p : P.Ω × γ) => e_hat n p.1 p.2))
(h_mu_rate :
∀ a : Bool,
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_e_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_product_rate :
∀ a : Bool,
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => μ_hat n ω a x - S.μ_val a x) 2 S.P_X).toReal *
(eLpNorm (fun x => e_hat n ω x - S.e_val x) 2 S.P_X).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(hψ_meas : Measurable (S.ψ_AIPW))
(hθn_meas : ∀ n : ℕ, AEMeasurable
(IsAsymLinear.rescaledEstimator
(dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB n) P.μ)
(hSum_meas : ∀ n : ℕ, AEMeasurable
(IsAsymLinear.normalizedSum sample (S.ψ_AIPW) split.foldB n) P.μ) :
Tendsto_dist
(IsAsymLinear.rescaledEstimator
(dmlEstimator S sample split μ_hat e_hat) S.θ₀ split.foldB)
(gaussianMeasure 0
((∫ x, (S.μ_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)))
P.μ
hθn_meas := by
rw [← S.aipw_variance_hahn_decomposition h_overlap hA h_y2 h_yd2]
exact dml_ATE_tendstoNormal S hA h_overlap h_y2 h_yd2
sample split hc_pos hc_lt h_split_rate μ_hat e_hat h_mu_meas h_e_meas
h_mu_memLp h_e_memLp h_e_overlap h_mu_foldA h_e_foldA
h_mu_uncurry_foldA h_e_uncurry_foldA h_mu_rate h_e_rate h_product_rate
hψ_meas hθn_meas hSum_meas
Submodel 4 core · 6 supporting Defines exponential-tilt submodels and score paths used in semiparametric efficiency arguments. ★ hasDerivAt_tiltExp
Defines exponential-tilt submodels and score paths used in semiparametric efficiency arguments. The module provides the differentiable perturbation interface for tangent-space calculations.
def tiltNorm reviewed
⚑ flagged
Causalean.Estimation.Efficiency
Normalizing constant c(t) = ∫ e^{t·s} dP of the exponential tilt.
def tiltExp reviewed
⚑ flagged
Causalean.Estimation.Efficiency
Tilted expectation E_{P_t}[φ] = (∫ φ·e^{t·s} dP)/(∫ e^{t·s} dP). This is the expectation of φ under the exponentially tilted law P_t.
def tiltMeasure reviewed
⚑ flagged
Causalean.Estimation.Efficiency
The exponentially tilted measure P_t = (e^{t·s}/c(t)) · P.
theorem hasDerivAt_tiltExp reviewed
⚑ flagged
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
hypotheses
conclusion
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
6 supporting declarations (lemmas, instances)
-
tiltNorm_zerolemma — At t = 0 the normalizing constant is the total mass = 1.Proof (Lean source)
@[simp] lemma tiltNorm_zero {P : Measure Z} [IsProbabilityMeasure P] {s : Z → ℝ} : tiltNorm P s 0 = 1 := by simp [tiltNorm] -
hasDerivAt_tilt_numeratorlemma — Numerator derivative. d/dt ∫ φ·e^{t·s} dP |₀ = ∫ φ·s dP, for bounded measurable score s and integrable φ.hypothesesconclusionHasDerivAt (fun t => ∫ z, φ z * exp (t * s z) ∂P) (∫ z, φ z * s z ∂P) 0Proof (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 -
tilt_exp_integrablelemma — 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).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 _) -
tiltNorm_poslemma — The normalizing constant c(t) = ∫ e^{t·s} dP is strictly positive.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 -
isProbabilityMeasure_tiltMeasurelemma — The tilted law tiltMeasure P s t is a probability measure.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 -
integral_tiltMeasurelemma — 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.)hypothesesconclusion∫ z, h_fn z ∂(tiltMeasure P s t) = tiltExp P s h_fn tProof (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