Estimation.Efficiency
Semiparametric efficiency: tangent spaces, pathwise differentiability, and the efficiency bound for the ATE functional.
ExponentialTilt 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.
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 .
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 divided by .
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 relative to the given measure.
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
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
tiltNorm_zerolemma — At t = 0 the normalizing constant is the total mass = 1.hypothesesconclusiontiltNorm P s 0 = 1Proof (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).hypothesesM :sharedℝt :sharedℝhs_meas :hsM :∀ z, |s z| ≤ MconclusionIntegrable (fun z => exp (t * s z)) PProof (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 -
tiltMeasure_eq_withDensity_divlemma — 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.hypothesesZ :sharedType u_1P :s :Z → ℝM t :ℝhs_meas :hsM :∀ z, |s z| ≤ MProof (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] -
isProbabilityMeasure_tiltMeasurelemma — The tilted law tiltMeasure P s t is a probability measure.hypothesesM :sharedℝt :sharedℝhs_meas :hsM :∀ z, |s z| ≤ MconclusionIsProbabilityMeasure (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 -
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.)hypothesesM :sharedℝt :sharedℝhs_meas :hsM :∀ z, |s z| ≤ Mh_fn :Z → ℝconclusion∫ 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
ObservedLawATE 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.
For a covariate space γ, the covariate σ-algebra on observed triples is generated by the projection (x,d,y) ↦ x.
Definition (Lean source)
For a treatment arm d and an observed triple z, the arm indicator is one when the observed treatment equals d and zero otherwise.
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)
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)
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)
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)
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)
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)
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)
Under the backdoor assumptions, the observed-law ATE functional at a backdoor system's true law equals its value-space ATE.
Formal statement
Proof (Lean source)
13 supporting declarations (lemmas, instances)
-
observedCovariateSigma_lelemma — The covariate σ-algebra on observed triples is contained in the ambient product σ-algebra.hypothesesγ :sharedType u_1conclusionProof (Lean source)
lemma observedCovariateSigma_le : observedCovariateSigma (γ := γ) ≤ (inferInstance : MeasurableSpace (γ × Bool × ℝ)) := (measurable_fst : Measurable (fun z : γ × Bool × ℝ => z.1)).comap_le -
measurable_observedArmIndicatorlemma — For a treatment arm d, the observed arm indicator is measurable.Proof (Lean source)
@[fun_prop] lemma measurable_observedArmIndicator (d : Bool) : Measurable (observedArmIndicator (γ := γ) d) := by exact (Measurable.of_discrete (f := fun b : Bool => if b = d then (1 : ℝ) else 0)).comp (measurable_snd.fst : Measurable (fun z : γ × Bool × ℝ => z.2.1)) -
observedATE_eq_observedArmMean_subtheorem — For an observed-data law Q whose two arm regressions are integrable, the observed ATE is the treated-arm mean minus the control-arm mean.hypothesesconclusionProof (Lean source)
theorem observedATE_eq_observedArmMean_sub (Q : Measure (γ × Bool × ℝ)) (hμ : ∀ d, Integrable (observedArmRegression Q d) Q) : observedATE Q = observedArmMean Q true - observedArmMean Q false := by unfold observedATE observedArmMean exact integral_sub (hμ true) (hμ false) -
observedAIPW_eq_armEIF_subtheorem — For an observed-data law Q whose two arm regressions are integrable and an observed triple z, the AIPW influence function is the treated-arm influence function minus the control-arm influence function.hypothesesconclusionProof (Lean source)
theorem observedAIPW_eq_armEIF_sub (Q : Measure (γ × Bool × ℝ)) (hμ : ∀ d, Integrable (observedArmRegression Q d) Q) (z : γ × Bool × ℝ) : observedAIPW Q z = observedArmEIF Q true z - observedArmEIF Q false z := by unfold observedAIPW observedArmEIF observedArmMean observedATE rw [integral_sub (hμ true) (hμ false)] ring -
measurable_observedPropensitylemma — For a law Q and an arm d, the observed propensity is measurable.hypothesesconclusionMeasurable (observedPropensity Q d)Proof (Lean source)
@[fun_prop] lemma measurable_observedPropensity (Q : Measure (γ × Bool × ℝ)) (d : Bool) : Measurable (observedPropensity Q d) := (stronglyMeasurable_condExp (μ := Q) (m := observedCovariateSigma) (f := observedArmIndicator d)).measurable.mono observedCovariateSigma_le le_rfl -
stronglyMeasurable_observedPropensitylemma — For a law Q and an arm d, the observed propensity is strongly measurable for the covariate σ-algebra.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma stronglyMeasurable_observedPropensity (Q : Measure (γ × Bool × ℝ)) (d : Bool) : StronglyMeasurable[observedCovariateSigma] (observedPropensity Q d) := stronglyMeasurable_condExp -
measurable_observedArmNumeratorlemma — For a law Q and an arm d, the observed arm numerator is measurable.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma measurable_observedArmNumerator (Q : Measure (γ × Bool × ℝ)) (d : Bool) : Measurable (observedArmNumerator Q d) := (stronglyMeasurable_condExp (μ := Q) (m := observedCovariateSigma) (f := fun z => ATE.BackdoorEstimationSystem.projY z * observedArmIndicator d z)).measurable.mono observedCovariateSigma_le le_rfl -
stronglyMeasurable_observedArmNumeratorlemma — For a law Q and an arm d, the observed arm numerator is strongly measurable for the covariate σ-algebra.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma stronglyMeasurable_observedArmNumerator (Q : Measure (γ × Bool × ℝ)) (d : Bool) : StronglyMeasurable[observedCovariateSigma] (observedArmNumerator Q d) := stronglyMeasurable_condExp -
measurable_observedArmRegressionlemma — For a law Q and an arm d, the observed arm regression is measurable.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma measurable_observedArmRegression (Q : Measure (γ × Bool × ℝ)) (d : Bool) : Measurable (observedArmRegression Q d) := by unfold observedArmRegression fun_prop -
stronglyMeasurable_observedArmRegressionlemma — For a law Q and an arm d, the observed arm regression is strongly measurable for the covariate σ-algebra.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma stronglyMeasurable_observedArmRegression (Q : Measure (γ × Bool × ℝ)) (d : Bool) : StronglyMeasurable[observedCovariateSigma] (observedArmRegression Q d) := by unfold observedArmRegression fun_prop -
observedPropensity_P_Z_aelemma — At a backdoor system's observed law, the law-recomputed arm propensity equals the system's label-specific value-space propensity almost everywhere.hypothesesconclusionobservedPropensity S.P_Z d=ᵐ[S.P_Z] fun z => S.e_val_label d (ATE.BackdoorEstimationSystem.projX z)Proof (Lean source)
lemma observedPropensity_P_Z_ae (S : ATE.BackdoorEstimationSystem P γ) (d : Bool) : observedPropensity S.P_Z d =ᵐ[S.P_Z] fun z => S.e_val_label d (ATE.BackdoorEstimationSystem.projX z) := by letI : IsProbabilityMeasure S.P_Z := by unfold ATE.BackdoorEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable have hi : Integrable (observedArmIndicator (γ := γ) d) S.P_Z := by apply Integrable.of_bound (measurable_observedArmIndicator d).aestronglyMeasurable 1 filter_upwards with z by_cases h : ATE.BackdoorEstimationSystem.projA z = d <;> simp [observedArmIndicator, h] have htransport := condExp_comp_of_map_eq S.factualZ S.measurable_factualZ S.P_Z_eq (observedCovariateSigma (γ := γ)) observedCovariateSigma_le hi have hcomap : comap S.factualZ (observedCovariateSigma (γ := γ)) = S.toPOBackdoorSystem.sigmaX := by unfold observedCovariateSigma POBackdoorSystem.sigmaX rw [MeasurableSpace.comap_comp] congr 1 rw [hcomap, observedArmIndicator_comp_factualZ S d] at htransport have hsource : (observedPropensity S.P_Z d) ∘ S.factualZ =ᵐ[P.μ] (fun z => S.e_val_label d (ATE.BackdoorEstimationSystem.projX z)) ∘ S.factualZ := by exact htransport.symm.trans (S.propScore_eq_e_val_label_ae d) rw [S.P_Z_eq] at hsource rw [S.P_Z_eq] apply (ae_map_iff S.measurable_factualZ.aemeasurable ?_).2 · filter_upwards [hsource] with x hx exact hx · exact measurableSet_eq_fun (measurable_observedPropensity S.P_Z d) ((S.measurable_e_val_label d).comp measurable_fst) -
observedArmRegression_P_Z_aelemma — At a backdoor system's observed law, the law-recomputed arm outcome regression equals the system's value-space arm regression almost everywhere, under the backdoor assumptions.hypothesesγ :sharedType u_1S :ATE.BackdoorEstimationSystem P γhA :S.toPOBackdoorSystem.Assumptionsd :conclusionobservedArmRegression S.P_Z d=ᵐ[S.P_Z] fun z => S.μ_val d (ATE.BackdoorEstimationSystem.projX z)Proof (Lean source)
lemma observedArmRegression_P_Z_ae (S : ATE.BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (d : Bool) : observedArmRegression S.P_Z d =ᵐ[S.P_Z] fun z => S.μ_val d (ATE.BackdoorEstimationSystem.projX z) := by letI : IsProbabilityMeasure S.P_Z := by unfold ATE.BackdoorEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable have hYind : Integrable (fun z : γ × Bool × ℝ => ATE.BackdoorEstimationSystem.projY z * observedArmIndicator d z) S.P_Z := by rw [S.P_Z_eq] have hmeas : Measurable (fun z : γ × Bool × ℝ => ATE.BackdoorEstimationSystem.projY z * observedArmIndicator d z) := (measurable_snd.snd : Measurable (fun z : γ × Bool × ℝ => z.2.2)).mul (measurable_observedArmIndicator d) apply (integrable_map_measure hmeas.aestronglyMeasurable S.measurable_factualZ.aemeasurable).2 rw [observedOutcomeIndicator_comp_factualZ S d] exact S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (measurableSet_singleton d) hA.integrable_factualY have htransport := condExp_comp_of_map_eq S.factualZ S.measurable_factualZ S.P_Z_eq (observedCovariateSigma (γ := γ)) observedCovariateSigma_le hYind have hcomap : comap S.factualZ (observedCovariateSigma (γ := γ)) = S.toPOBackdoorSystem.sigmaX := by unfold observedCovariateSigma POBackdoorSystem.sigmaX rw [MeasurableSpace.comap_comp] congr 1 rw [hcomap, observedOutcomeIndicator_comp_factualZ S d] at htransport have hprop := observedPropensity_P_Z_ae S d have hnum_source : (observedArmNumerator S.P_Z d) ∘ S.factualZ =ᵐ[P.μ] P.μ[fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] := htransport.symm have hreg_source : (observedArmRegression S.P_Z d) ∘ S.factualZ =ᵐ[P.μ] (fun z => S.μ_val d (ATE.BackdoorEstimationSystem.projX z)) ∘ S.factualZ := by rw [S.P_Z_eq] at hprop have hprop_source := ae_of_ae_map S.measurable_factualZ.aemeasurable hprop have hprop_source' : (observedPropensity S.P_Z d) ∘ S.factualZ =ᵐ[P.μ] (fun z => S.e_val_label d (ATE.BackdoorEstimationSystem.projX z)) ∘ S.factualZ := by filter_upwards [hprop_source] with x hx exact hx have hbaseprop := S.propScore_eq_e_val_label_ae d filter_upwards [hnum_source, hprop_source', S.μ_reg_compat d, hbaseprop] with ω hnum hprop hμ hbaseprop change observedArmNumerator S.P_Z d (S.factualZ ω) / observedPropensity S.P_Z d (S.factualZ ω) = _ change observedArmNumerator S.P_Z d (S.factualZ ω) = _ at hnum change observedPropensity S.P_Z d (S.factualZ ω) = S.e_val_label d (ATE.BackdoorEstimationSystem.projX (S.factualZ ω)) at hprop rw [hnum, hprop] change P.μ[fun ω => S.toPOBackdoorSystem.factualY ω * S.toPOBackdoorSystem.dVar.indicator d ω | S.toPOBackdoorSystem.sigmaX] ω / S.e_val_label d (S.toPOBackdoorSystem.factualX ω) = S.μ_val d (S.toPOBackdoorSystem.factualX ω) rw [← hbaseprop] simpa [POBackdoorSystem.adjustedCE, ATE.BackdoorEstimationSystem.factualZ] using hμ.symm rw [S.P_Z_eq] at hreg_source rw [S.P_Z_eq] apply (ae_map_iff S.measurable_factualZ.aemeasurable ?_).2 · filter_upwards [hreg_source] with x hx exact hx · exact measurableSet_eq_fun (measurable_observedArmRegression S.P_Z d) ((S.μ_meas d).comp measurable_fst) -
observedAIPW_P_Z_aetheorem — Under the backdoor assumptions, the law-recomputed AIPW function at the true observed law equals the system's existing AIPW influence function almost everywhere.hypothesesγ :sharedType u_1S :ATE.BackdoorEstimationSystem P γhA :S.toPOBackdoorSystem.AssumptionsconclusionobservedAIPW S.P_Z =ᵐ[S.P_Z] S.ψ_AIPWProof (Lean source)
theorem observedAIPW_P_Z_ae (S : ATE.BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) : observedAIPW S.P_Z =ᵐ[S.P_Z] S.ψ_AIPW := by filter_upwards [observedArmRegression_P_Z_ae S hA true, observedArmRegression_P_Z_ae S hA false, observedPropensity_P_Z_ae S true, observedPropensity_P_Z_ae S false] with z hμ1 hμ0 he1 he0 rw [observedAIPW, hμ1, hμ0, he1, he0, observedATE_P_Z_eq S hA] unfold ATE.BackdoorEstimationSystem.ψ_AIPW ATE.BackdoorEstimationSystem.aipwMoment ATE.BackdoorEstimationSystem.e_val_label ATE.BackdoorEstimationSystem.indA observedArmIndicator by_cases hd : ATE.BackdoorEstimationSystem.projA z = true · have hd' : ATE.BackdoorEstimationSystem.projA z ≠ false := by simpa [hd] simp [hd] ring · have hd' : ATE.BackdoorEstimationSystem.projA z = false := by cases h : ATE.BackdoorEstimationSystem.projA z <;> simp [h] at hd ⊢ simp [hd, hd'] ring
TangentProjection 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.
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)
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)
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)
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
Proof (Lean source)
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)
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)
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.hypothesesconclusionψ = efficientIF T gProof (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.hypothesesH :sharedType u_1T T' :Submodule ℝ HT.HasOrthogonalProjectionT'.HasOrthogonalProjectionhle :T' ≤ Tg :Hhg :g ∈ T'Proof (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]⟩
PathwiseGradient 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.
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)
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)
If two regular submodels through P have the same law path, then their DQM scores are equal.
Formal statement
Proof (Lean source)
For a base probability law P, the constant regular submodel keeps the law equal to P and has zero score.
Definition (Lean source)
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)
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)
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)
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)
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)
If two candidates are efficient influence functions for the same functional and submodel family, then they are equal.
Formal statement
Proof (Lean source)
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
Proof (Lean source)
11 supporting declarations (lemmas, instances)
-
dqm_integral_tendstotheorem — For a DQM regular submodel m, the integral of the squared square-root-density quotient error converges to zero. This is the integral form of van der Vaart's equation (25.13), with the quotient represented canonically in L²(P).hypothesesconclusionTendsto (fun t => letI := m.path_probability t ∫ z, (dqmQuotient P (m.path t) t z - ((2 : ℝ)⁻¹ • m.score) z) ^ 2 ∂P) (𝓝[≠] 0) (𝓝 0)Proof (Lean source)
theorem dqm_integral_tendsto {P : Measure Z} [IsProbabilityMeasure P] (m : RegularSubmodel P) : Tendsto (fun t => letI := m.path_probability t ∫ z, (dqmQuotient P (m.path t) t z - ((2 : ℝ)⁻¹ • m.score) z) ^ 2 ∂P) (𝓝[≠] 0) (𝓝 0) := by have hdiff := m.dqm.sub (tendsto_const_nhds : Tendsto (fun _ : ℝ => (2 : ℝ)⁻¹ • m.score) (𝓝[≠] 0) (𝓝 ((2 : ℝ)⁻¹ • m.score))) have hsq := hdiff.norm.pow 2 have hsq0 : Tendsto (fun t => letI := m.path_probability t ‖dqmQuotient P (m.path t) t - (2 : ℝ)⁻¹ • m.score‖ ^ 2) (𝓝[≠] 0) (𝓝 0) := by simpa only [sub_self, norm_zero, zero_pow (by norm_num : 2 ≠ 0)] using hsq simp_rw [lpNorm_sq_eq_integral_sq] at hsq0 convert hsq0 using 1 funext t letI : IsProbabilityMeasure (m.path t) := m.path_probability t apply integral_congr_ae filter_upwards [Lp.coeFn_sub (dqmQuotient P (m.path t) t) ((2 : ℝ)⁻¹ • m.score)] with z hz rw [hz] rfl -
score_eq_zero_of_path_eq_consttheorem — If a regular submodel through P has the constant law path, then its score is zero.hypothesesm :hpath :m.path = fun _ => Pconclusionm.score = 0Proof (Lean source)
theorem score_eq_zero_of_path_eq_const {P : Measure Z} [IsProbabilityMeasure P] (m : RegularSubmodel P) (hpath : m.path = fun _ => P) : m.score = 0 := by simpa [constant] using m.score_eq_of_path_eq (constant P) hpath -
score_mem_tangentSpacetheorem — Every score of a submodel m belonging to S lies in the tangent space generated by S.Proof (Lean source)
theorem score_mem_tangentSpace {P : Measure Z} [IsProbabilityMeasure P] {S : Set (RegularSubmodel P)} {m : RegularSubmodel P} (hm : m ∈ S) : m.score ∈ tangentSpace P S := by apply Submodule.le_topologicalClosure (span ℝ (scoreSet P S)) apply Submodule.subset_span exact ⟨m, hm, rfl⟩ -
tangentSpaceHasOrthogonalProjectioninstance — For a probability law P and a submodel family S, the closed generated tangent space has an orthogonal projection.parametersinstancegiven byby letI : CompleteSpace (tangentSpace P S) := by rw [tangentSpace] infer_instance infer_instance -
inner_score_eq_of_isPathwiseGradienttheorem — If two candidates are pathwise gradients relative to the same family, then they have the same inner product with every score in that family.hypothesesψ :Measure Z → ℝS :Set (RegularSubmodel P)g g' :Lp ℝ 2 Phg :IsPathwiseGradient P ψ g Shg' :IsPathwiseGradient P ψ g' Sm :hm :m ∈ Sconclusion⟪g, m.score⟫_ℝ = ⟪g', m.score⟫_ℝProof (Lean source)
theorem inner_score_eq_of_isPathwiseGradient {P : Measure Z} [IsProbabilityMeasure P] {ψ : Measure Z → ℝ} {S : Set (RegularSubmodel P)} {g g' : Lp ℝ 2 P} (hg : IsPathwiseGradient P ψ g S) (hg' : IsPathwiseGradient P ψ g' S) {m : RegularSubmodel P} (hm : m ∈ S) : ⟪g, m.score⟫_ℝ = ⟪g', m.score⟫_ℝ := (hg m hm).unique (hg' m hm) -
sub_mem_orthogonal_of_isPathwiseGradienttheorem — If two candidates are pathwise gradients relative to the same family, then their difference is orthogonal to the generated tangent space.hypothesesψ :Measure Z → ℝS :Set (RegularSubmodel P)g g' :Lp ℝ 2 Phg :IsPathwiseGradient P ψ g Shg' :IsPathwiseGradient P ψ g' Sconclusiong - g' ∈ (tangentSpace P S)ᗮProof (Lean source)
theorem sub_mem_orthogonal_of_isPathwiseGradient {P : Measure Z} [IsProbabilityMeasure P] {ψ : Measure Z → ℝ} {S : Set (RegularSubmodel P)} {g g' : Lp ℝ 2 P} (hg : IsPathwiseGradient P ψ g S) (hg' : IsPathwiseGradient P ψ g' S) : g - g' ∈ (tangentSpace P S)ᗮ := by rw [tangentSpace, Submodule.orthogonal_closure, Submodule.mem_orthogonal'] intro u hu let W : Submodule ℝ (Lp ℝ 2 P) := { carrier := {v | ⟪g - g', v⟫_ℝ = 0} zero_mem' := by simp add_mem' := by intros; simp_all [inner_add_right] smul_mem' := by intros; simp_all [inner_smul_right] } have hspan : span ℝ (scoreSet P S) ≤ W := by rw [Submodule.span_le] rintro _ ⟨m, hm, rfl⟩ change ⟪g - g', m.score⟫_ℝ = 0 rw [inner_sub_left, inner_score_eq_of_isPathwiseGradient hg hg' hm, sub_self] exact hspan hu -
canonicalGradient_isPathwiseGradienttheorem — If a candidate g is a pathwise gradient, then its canonical gradient is also a pathwise gradient.hypothesesconclusionIsPathwiseGradient P ψ (canonicalGradient P S g) SProof (Lean source)
theorem canonicalGradient_isPathwiseGradient {P : Measure Z} [IsProbabilityMeasure P] {ψ : Measure Z → ℝ} {S : Set (RegularSubmodel P)} {g : Lp ℝ 2 P} (hg : IsPathwiseGradient P ψ g S) : IsPathwiseGradient P ψ (canonicalGradient P S g) S := by intro m hm have hinner : ⟪canonicalGradient P S g, m.score⟫_ℝ = ⟪g, m.score⟫_ℝ := by rw [canonicalGradient, efficientIF] exact (tangentSpace P S).inner_orthogonalProjection_eq_of_mem_right ⟨m.score, score_mem_tangentSpace hm⟩ g simpa [hinner] using hg m hm -
canonicalGradient_isEfficientInfluenceFunctiontheorem — If a candidate g is a pathwise gradient, then its canonical gradient is an efficient influence function.hypothesesconclusionIsEfficientInfluenceFunction P ψ (canonicalGradient P S g) SProof (Lean source)
theorem canonicalGradient_isEfficientInfluenceFunction {P : Measure Z} [IsProbabilityMeasure P] {ψ : Measure Z → ℝ} {S : Set (RegularSubmodel P)} {g : Lp ℝ 2 P} (hg : IsPathwiseGradient P ψ g S) : IsEfficientInfluenceFunction P ψ (canonicalGradient P S g) S := ⟨canonicalGradient_isPathwiseGradient hg, efficientIF_mem g⟩ -
canonicalGradient_eq_of_isEfficientInfluenceFunctiontheorem — If an efficient influence function g is known and another candidate v is a pathwise gradient, then the canonical gradient of v equals g.hypothesesψ :Measure Z → ℝS :Set (RegularSubmodel P)g v :Lp ℝ 2 Phg :IsEfficientInfluenceFunction P ψ g Shv :IsPathwiseGradient P ψ v SconclusioncanonicalGradient P S v = gProof (Lean source)
theorem canonicalGradient_eq_of_isEfficientInfluenceFunction {P : Measure Z} [IsProbabilityMeasure P] {ψ : Measure Z → ℝ} {S : Set (RegularSubmodel P)} {g v : Lp ℝ 2 P} (hg : IsEfficientInfluenceFunction P ψ g S) (hv : IsPathwiseGradient P ψ v S) : canonicalGradient P S v = g := by exact efficientInfluenceFunction_unique (canonicalGradient_isEfficientInfluenceFunction hv) hg -
isGradient_canonicalGradienttheorem — Every square-integrable candidate g is a Hilbert-space gradient of its canonical projection onto the tangent space generated by S. This connects the canonical gradient to the abstract IsGradient/effBound projection API.hypothesesconclusionIsGradient (tangentSpace P S) (canonicalGradient P S g) gProof (Lean source)
theorem isGradient_canonicalGradient {P : Measure Z} [IsProbabilityMeasure P] {S : Set (RegularSubmodel P)} {g : Lp ℝ 2 P} : IsGradient (tangentSpace P S) (canonicalGradient P S g) g := by intro s hs rw [canonicalGradient, efficientIF] exact ((tangentSpace P S).inner_orthogonalProjection_eq_of_mem_right ⟨s, hs⟩ g).symm -
mono_of_tangentSpace_eqtheorem — Let a smaller regular-submodel family S be contained in S' and suppose both families generate the same tangent space. If g is the efficient influence function relative to S and ψ has some pathwise gradient v along the enlarged family S', then g remains the efficient influence function relative to S'.hypothesesψ :Measure Z → ℝS S' :Set (RegularSubmodel P)g v :Lp ℝ 2 Phg :IsEfficientInfluenceFunction P ψ g ShSS' :S ⊆ S'hT :tangentSpace P S = tangentSpace P S'hv :IsPathwiseGradient P ψ v S'conclusionIsEfficientInfluenceFunction P ψ g S'Proof (Lean source)
theorem IsEfficientInfluenceFunction.mono_of_tangentSpace_eq {P : Measure Z} [IsProbabilityMeasure P] {ψ : Measure Z → ℝ} {S S' : Set (RegularSubmodel P)} {g v : Lp ℝ 2 P} (hg : IsEfficientInfluenceFunction P ψ g S) (hSS' : S ⊆ S') (hT : tangentSpace P S = tangentSpace P S') (hv : IsPathwiseGradient P ψ v S') : IsEfficientInfluenceFunction P ψ g S' := by have hvS : IsPathwiseGradient P ψ v S := fun m hm => hv m (hSS' hm) have hcanon : canonicalGradient P S v = g := canonicalGradient_eq_of_isEfficientInfluenceFunction hg hvS constructor · intro m hm have hscore : m.score ∈ tangentSpace P S := by rw [hT] exact score_mem_tangentSpace hm have hinner : ⟪g, m.score⟫_ℝ = ⟪v, m.score⟫_ℝ := by rw [← hcanon, canonicalGradient, efficientIF] exact (tangentSpace P S).inner_orthogonalProjection_eq_of_mem_right ⟨m.score, hscore⟩ v simpa only [hinner] using hv m hm · rw [← hT] exact hg.2
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.
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 space.
Definition (Lean source)
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 space is the equivalence class of the function that equals one everywhere.
Definition (Lean source)
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 space.
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
Proof (Lean source)
12 supporting declarations (lemmas, instances)
-
propensity_score_residual_integral_zerolemma — Any covariate-measurable multiplier has zero integral against the propensity-score residual.hypothesesγ :sharedType u_1S :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 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.hypothesesγ :sharedType u_1S :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 — 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.parametersinstancegiven byby 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.hypothesesγ :sharedType u_1S :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 — 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.parametersinstancegiven by -
instHasOrthogonalProjection_Tfullinstance — 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.parametersinstancegiven byby rw [Tfull] exact Submodule.instHasOrthogonalProjectionOrthogonal (ℝ ∙ S.oneLp) -
inner_oneLptheorem — Inner product against the constant-one function equals integration under the observed data law.hypothesesconclusion⟪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.hypothesesγ :sharedType u_1S :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.hypothesesγ :sharedType u_1S :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) -
aipwProjectionNormSq_eq_secondMomenttheorem — 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.hypothesesγ :sharedType u_1S :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.μconclusioneffBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) = ∫ z, (S.ψ_AIPW z) ^ 2 ∂S.P_ZProof (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] -
aipwProjectionNormSq_le_normSqtheorem — 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 ψ.hypothesesγ :sharedType u_1S :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.μψ :Lp ℝ 2 S.P_Zhψ :IsGradient S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) ψconclusioneffBound S.Tfull (S.aipwLp h_overlap hA h_y2 h_yd2) ≤ ‖ψ‖ ^ 2Proof (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ψ -
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.hypothesesγ :sharedType u_1S :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
TiltTangent 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.
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)
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)
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)
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)
For a probability law P, the tangent space generated by bounded exponential tilts is all of L²₀(P).
Formal statement
Proof (Lean source)
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
Proof (Lean source)
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
Proof (Lean source)
12 supporting declarations (lemmas, instances)
-
hasDerivAt_expHalfLptheorem — For a probability law P, a measurable function g bounded by M, and its L² certificate, the exponential half-density curve has L² derivative g/2 at zero.hypothesesconclusionHasDerivAt (expHalfLp P g M hg_meas hgM) ((2 : ℝ)⁻¹ • hg.toLp g) 0Proof (Lean source)
theorem hasDerivAt_expHalfLp (P : Measure Z) [IsProbabilityMeasure P] (g : Z → ℝ) (M : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hg : MemLp g 2 P) : HasDerivAt (expHalfLp P g M hg_meas hgM) ((2 : ℝ)⁻¹ • hg.toLp g) 0 := by rw [hasDerivAt_iff_isLittleO_nhds_zero] let h : Z → ℝ := fun z => (2 : ℝ)⁻¹ * g z have hh : MemLp h 2 P := by change MemLp ((2 : ℝ)⁻¹ • g) 2 P exact hg.const_smul (2 : ℝ)⁻¹ let r : ℝ → Z → ℝ := fun t z => exp (t * g z / 2) - 1 - t * h z have he (t : ℝ) : MemLp (fun z => exp (t * g z / 2)) 2 P := by exact 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]) have hr (t : ℝ) : MemLp (r t) 2 P := by exact ((he t).sub (memLp_const (1 : ℝ))).sub (hh.const_smul t) have hremainder (t : ℝ) : expHalfLp P g M hg_meas hgM t - expHalfLp P g M hg_meas hgM 0 - t • ((2 : ℝ)⁻¹ • hg.toLp g) = (hr t).toLp (r t) := by change (he t).toLp (fun z => exp (t * g z / 2)) - (he 0).toLp (fun z => exp (0 * g z / 2)) - t • ((2 : ℝ)⁻¹ • hg.toLp g) = _ have hone : (he 0).toLp (fun z => exp (0 * g z / 2)) = (memLp_const (1 : ℝ)).toLp (fun _ : Z => (1 : ℝ)) := by apply MemLp.toLp_congr exact ae_of_all _ fun z => by simp rw [hone] have hhLp : hh.toLp h = (2 : ℝ)⁻¹ • hg.toLp g := by change (hg.const_smul (2 : ℝ)⁻¹).toLp ((2 : ℝ)⁻¹ • g) = _ exact MemLp.toLp_const_smul (2 : ℝ)⁻¹ hg rw [← hhLp, ← MemLp.toLp_const_smul, ← MemLp.toLp_sub, ← MemLp.toLp_sub] apply MemLp.toLp_congr exact ae_of_all _ fun z => by simp [r, h, Pi.smul_apply, smul_eq_mul] have hlocal : ∀ᶠ t in 𝓝 (0 : ℝ), |t| * |M| ≤ 1 := by by_cases hM : |M| = 0 · simp [hM] · apply Metric.eventually_nhds_iff.mpr have hMpos : 0 < |M| := lt_of_le_of_ne (abs_nonneg M) (Ne.symm hM) refine ⟨|M|⁻¹, inv_pos.mpr hMpos, ?_⟩ intro t ht rw [Real.dist_eq, sub_zero] at ht exact le_of_lt <| calc |t| * |M| < |M|⁻¹ * |M| := mul_lt_mul_of_pos_right ht hMpos _ = 1 := inv_mul_cancel₀ hM have hnorm : ∀ᶠ t in 𝓝 (0 : ℝ), ‖expHalfLp P g M hg_meas hgM t - expHalfLp P g M hg_meas hgM 0 - t • ((2 : ℝ)⁻¹ • hg.toLp g)‖ ≤ |M| ^ 2 * ‖t ^ 2‖ := by filter_upwards [hlocal] with t ht rw [hremainder] apply (sq_le_sq₀ (norm_nonneg _) (mul_nonneg (sq_nonneg _) (norm_nonneg _))).mp rw [norm_toLp_sq_eq_integral_sq] have hrint : Integrable (fun z => r t z ^ 2) P := by have hi := (memLp_two_iff_integrable_sq_norm (hr t).1).1 (hr t) simpa only [Real.norm_eq_abs, sq_abs] using hi calc (∫ z, r t z ^ 2 ∂P) ≤ ∫ _z, ((|t| * |M|) ^ 2) ^ 2 ∂P := by apply integral_mono · exact hrint · exact integrable_const _ · intro z dsimp only rw [← sq_abs (r t z)] apply (sq_le_sq₀ (abs_nonneg _) (sq_nonneg _)).2 dsimp only [r, h] have hx : t * ((2 : ℝ)⁻¹ * g z) = t * g z / 2 := by ring rw [hx] have harg : |t * g z / 2| ≤ |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] exact (Real.abs_exp_sub_one_sub_id_le (harg.trans ht)).trans (by rw [sq_le_sq, abs_of_nonneg (mul_nonneg (abs_nonneg t) (abs_nonneg M))] exact harg) _ = ((|t| * |M|) ^ 2) ^ 2 := by simp _ = (|M| ^ 2 * ‖t ^ 2‖) ^ 2 := by rw [Real.norm_eq_abs, abs_sq] congr 1 rw [mul_pow, sq_abs, sq_abs] ring have hbig : (fun t => expHalfLp P g M hg_meas hgM t - expHalfLp P g M hg_meas hgM 0 - t • ((2 : ℝ)⁻¹ • hg.toLp g)) =O[𝓝 0] fun t : ℝ => t ^ 2 := Asymptotics.IsBigO.of_bound (|M| ^ 2) hnorm simpa only [zero_add] using hbig.trans_isLittleO (isLittleO_pow_id (by norm_num : 1 < 2)) -
tiltMeasure_zerotheorem — For a probability law P and a real function g, the exponential tilt passes through P at parameter zero.hypothesesconclusiontiltMeasure P g 0 = PProof (Lean source)
@[simp] theorem tiltMeasure_zero (P : Measure Z) [IsProbabilityMeasure P] (g : Z → ℝ) : tiltMeasure P g 0 = P := by rw [tiltMeasure, tiltNorm_zero] simp -
rnSqrtDensityLp_tiltMeasuretheorem — For a probability law P, a measurable score g bounded by M, and a perturbation t, the L² square-root Radon--Nikodym density of the normalized tilt is the exponential half-density scaled by the inverse square root of its normalizer.hypothesesZ :sharedType u_1P :g :Z → ℝM t :ℝhg_meas :hgM :∀ z, |g z| ≤ Mconclusion(let _ : IsProbabilityMeasure (tiltMeasure P g t) := isProbabilityMeasure_tiltMeasure hg_meas hgM rnSqrtDensityLp P (tiltMeasure P g t))Proof (Lean source)
theorem rnSqrtDensityLp_tiltMeasure (P : Measure Z) [IsProbabilityMeasure P] (g : Z → ℝ) (M t : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) : (let _ : IsProbabilityMeasure (tiltMeasure P g t) := isProbabilityMeasure_tiltMeasure hg_meas hgM rnSqrtDensityLp P (tiltMeasure P g t)) = (sqrt (tiltNorm P g t))⁻¹ • expHalfLp P g M hg_meas hgM t := by letI : IsProbabilityMeasure (tiltMeasure P g t) := isProbabilityMeasure_tiltMeasure hg_meas hgM change rnSqrtDensityLp P (tiltMeasure P g t) = _ have hc : 0 < tiltNorm P g t := tiltNorm_pos hg_meas hgM have hrn : (tiltMeasure P g t).rnDeriv P =ᵐ[P] fun z => ofReal (exp (t * g z) / tiltNorm P g t) := by rw [tiltMeasure_eq_withDensity_div P g M t hg_meas hgM] exact Measure.rnDeriv_withDensity P (by fun_prop) have hexp_ae : (expHalfLp P g M hg_meas hgM t : Z → ℝ) =ᵐ[P] fun z => exp (t * g z / 2) := by unfold expHalfLp exact MemLp.coeFn_toLp _ have hsmul_ae := Lp.coeFn_smul (sqrt (tiltNorm P g t))⁻¹ (expHalfLp P g M hg_meas hgM t) apply Lp.ext filter_upwards [(rnSqrtDensity_memLp P (tiltMeasure P g t)).coeFn_toLp, hrn, hexp_ae, hsmul_ae] with z hz hrnz hexpz hsmulz rw [show rnSqrtDensityLp P (tiltMeasure P g t) z = rnSqrtDensity P (tiltMeasure P g t) z from hz] simp only [rnSqrtDensity, hrnz] rw [ENNReal.toReal_ofReal (div_nonneg (Real.exp_pos _).le hc.le)] rw [Real.sqrt_div (Real.exp_pos _).le, ← Real.exp_half] rw [hsmulz, Pi.smul_apply, smul_eq_mul, hexpz] simp [div_eq_mul_inv, mul_comm] -
hasDerivAt_rnSqrtDensityLp_tiltMeasuretheorem — For a probability law P, a measurable bounded mean-zero score g, and its L² certificate, the L² square-root density curve of the normalized exponential tilt has derivative g/2 at zero.hypothesesZ :sharedType u_1P :g :Z → ℝM :ℝhg_meas :hgM :∀ z, |g z| ≤ Mhg_mean :∫ z, g z ∂P = 0hg :MemLp g 2 PconclusionHasDerivAt (fun t => letI := isProbabilityMeasure_tiltMeasure (P := P) (t := t) hg_meas hgM rnSqrtDensityLp P (tiltMeasure P g t)) ((2 : ℝ)⁻¹ • hg.toLp g) 0Proof (Lean source)
theorem hasDerivAt_rnSqrtDensityLp_tiltMeasure (P : Measure Z) [IsProbabilityMeasure P] (g : Z → ℝ) (M : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hg_mean : ∫ z, g z ∂P = 0) (hg : MemLp g 2 P) : HasDerivAt (fun t => letI := isProbabilityMeasure_tiltMeasure (P := P) (t := t) hg_meas hgM rnSqrtDensityLp P (tiltMeasure P g t)) ((2 : ℝ)⁻¹ • hg.toLp g) 0 := by have hc : HasDerivAt (fun t => tiltNorm P g t) 0 0 := by have h := hasDerivAt_tilt_numerator (P := P) (s := g) (φ := fun _ => (1 : ℝ)) hg_meas hgM aestronglyMeasurable_const (integrable_const (1 : ℝ)) simpa [tiltNorm, hg_mean] using h have hsqrt : HasDerivAt (fun t => sqrt (tiltNorm P g t)) 0 0 := by simpa using hc.sqrt (by simp) have hinv := hsqrt.inv (by simp) have hexp := hasDerivAt_expHalfLp P g M hg_meas hgM hg have hprod := hinv.smul hexp have hcurve : (fun t => letI := isProbabilityMeasure_tiltMeasure (P := P) (t := t) hg_meas hgM rnSqrtDensityLp P (tiltMeasure P g t)) = ((fun t => sqrt (tiltNorm P g t))⁻¹ • expHalfLp P g M hg_meas hgM) := by funext t letI : IsProbabilityMeasure (tiltMeasure P g t) := isProbabilityMeasure_tiltMeasure hg_meas hgM change rnSqrtDensityLp P (tiltMeasure P g t) = (sqrt (tiltNorm P g t))⁻¹ • expHalfLp P g M hg_meas hgM t exact rnSqrtDensityLp_tiltMeasure P g M t hg_meas hgM rw [hcurve] apply hprod.congr_deriv simp -
hasDerivAt_integral_tiltMeasuretheorem — Along the normalized exponential tilt of a probability law P by a measurable, bounded, mean-zero score g, the expectation of a fixed almost-everywhere strongly measurable and integrable test function φ is differentiable at zero with derivative ∫ φ g dP.hypothesesg φ :Z → ℝM :ℝhg_meas :hgM :∀ z, |g z| ≤ Mhg_mean :∫ z, g z ∂P = 0hφ_meas :hφ_int :Integrable φ PconclusionHasDerivAt (fun t => ∫ z, φ z ∂(tiltMeasure P g t)) (∫ z, φ z * g z ∂P) 0Proof (Lean source)
theorem hasDerivAt_integral_tiltMeasure {P : Measure Z} [IsProbabilityMeasure P] {g φ : Z → ℝ} {M : ℝ} (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hg_mean : ∫ z, g z ∂P = 0) (hφ_meas : AEStronglyMeasurable φ P) (hφ_int : Integrable φ P) : HasDerivAt (fun t => ∫ z, φ z ∂(tiltMeasure P g t)) (∫ z, φ z * g z ∂P) 0 := by have hfun : (fun t => ∫ z, φ z ∂(tiltMeasure P g t)) = tiltExp P g φ := by funext t exact integral_tiltMeasure hg_meas hgM rw [hfun] exact hasDerivAt_tiltExp hg_meas hgM hg_mean hφ_meas hφ_int -
hasDerivAt_integral_tiltMeasure_of_memLptheorem — Along the normalized exponential tilt of a probability law P by a measurable, bounded, mean-zero score g, the expectation of every square-integrable test function φ is differentiable at zero with derivative ∫ φ g dP.hypothesesconclusionHasDerivAt (fun t => ∫ z, φ z ∂(tiltMeasure P g t)) (∫ z, φ z * g z ∂P) 0Proof (Lean source)
theorem hasDerivAt_integral_tiltMeasure_of_memLp {P : Measure Z} [IsProbabilityMeasure P] {g φ : Z → ℝ} {M : ℝ} (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hg_mean : ∫ z, g z ∂P = 0) (hφ : MemLp φ 2 P) : HasDerivAt (fun t => ∫ z, φ z ∂(tiltMeasure P g t)) (∫ z, φ z * g z ∂P) 0 := hasDerivAt_integral_tiltMeasure hg_meas hgM hg_mean hφ.1 (hφ.integrable (by norm_num)) -
tiltScoreSpan_eq_meanZeroLptheorem — For a probability law P, the closed linear span of bounded exponential-tilt scores is exactly the mean-zero subspace of L²(P).hypothesesZ :sharedType u_1P :conclusionProof (Lean source)
theorem tiltScoreSpan_eq_meanZeroLp (P : Measure Z) [IsProbabilityMeasure P] : (span ℝ (tiltScoreSet P)).topologicalClosure = meanZeroLp P := by apply le_antisymm · apply Submodule.topologicalClosure_minimal · rw [Submodule.span_le] rintro f ⟨g, _M, hg, _hg_meas, _hgM, hg_mean, rfl⟩ apply Submodule.mem_orthogonal_singleton_iff_inner_left.mpr rw [inner_lpOne_eq_integral] rw [integral_congr_ae hg.coeFn_toLp] exact hg_mean · exact Submodule.isClosed_orthogonal (ℝ ∙ lpOne P) · rw [← boundedCenteredLp_topologicalClosure] apply Submodule.topologicalClosure_mono intro f hf apply Submodule.subset_span exact mem_boundedCenteredLp_exists P f hf -
tiltScoreSet_subset_scoreSettheorem — For a probability law P, every bounded exponential-tilt score is a score in the efficiency layer's abstract regular-submodel score set.hypothesesZ :sharedType u_1P :conclusionProof (Lean source)
theorem tiltScoreSet_subset_scoreSet (P : Measure Z) [IsProbabilityMeasure P] : tiltScoreSet P ⊆ scoreSet P (boundedTiltSubmodels P) := by rintro f ⟨g, M, hg, hg_meas, hgM, hg_mean, hgf⟩ refine ⟨tiltRegularSubmodel P g M hg_meas hgM hg_mean hg, ?_, ?_⟩ · exact ⟨g, M, hg_meas, hgM, hg_mean, hg, rfl⟩ · simpa [tiltRegularSubmodel] using hgf -
scoreSet_boundedTiltSubmodels_eq_tiltScoreSettheorem — For a probability law P, the score set of the bounded-tilt submodel family is the set of bounded centered L² scores.hypothesesZ :sharedType u_1P :conclusionProof (Lean source)
theorem scoreSet_boundedTiltSubmodels_eq_tiltScoreSet (P : Measure Z) [IsProbabilityMeasure P] : scoreSet P (boundedTiltSubmodels P) = tiltScoreSet P := by apply Set.Subset.antisymm · rintro f ⟨m, ⟨g, M, hg_meas, hgM, hg_mean, hg, rfl⟩, rfl⟩ exact ⟨g, M, hg, hg_meas, hgM, hg_mean, rfl⟩ · exact tiltScoreSet_subset_scoreSet P -
tangentSpace_eq_meanZeroLptheorem — For a probability law P, the abstract tangent space generated by all regular submodels equals the full mean-zero subspace of L²(P); bounded exponential tilts already generate the reverse inclusion.Proof (Lean source)
theorem tangentSpace_eq_meanZeroLp (P : Measure Z) [IsProbabilityMeasure P] : tangentSpace P univ = meanZeroLp P := by apply le_antisymm · rw [tangentSpace] apply Submodule.topologicalClosure_minimal · rw [Submodule.span_le] rintro f ⟨m, _, rfl⟩ exact m.score_meanZero · exact Submodule.isClosed_orthogonal (ℝ ∙ lpOne P) · rw [← tiltScoreSpan_eq_meanZeroLp] apply Submodule.topologicalClosure_mono apply Submodule.span_mono intro f hf rcases tiltScoreSet_subset_scoreSet P hf with ⟨m, _hm, rfl⟩ exact ⟨m, Set.mem_univ m, rfl⟩ -
isEfficientInfluenceFunction_of_hasDerivAt_tilttheorem — Nonparametric efficient-influence-function recipe. Given a probability law P, a law functional ψ, and a mean-zero L² candidate φ, suppose for every measurable bounded mean-zero score g, the derivative of ψ along the normalized exponential tilt equals ⟪φ,g⟫. Then φ is the efficient influence function of ψ in the nonparametric model generated by bounded tilts.hypothesesZ :sharedType u_1P :ψ :Measure Z → ℝφ :Lp ℝ 2 Phφ :φ ∈ meanZeroLp Phderiv :∀ (g : Z → ℝ) (M : ℝ) (hg : MemLp g 2 P)ifand(∀ z, |g z| ≤ M)and(∫ z, g z ∂P) = 0thenHasDerivAt (fun t => ψ (tiltMeasure P g t)) ⟪φ, hg.toLp g⟫_ℝ 0conclusionProof (Lean source)
theorem isEfficientInfluenceFunction_of_hasDerivAt_tilt (P : Measure Z) [IsProbabilityMeasure P] (ψ : Measure Z → ℝ) (φ : Lp ℝ 2 P) (hφ : φ ∈ meanZeroLp P) (hderiv : ∀ (g : Z → ℝ) (M : ℝ) (hg : MemLp g 2 P), Measurable g → (∀ z, |g z| ≤ M) → (∫ z, g z ∂P) = 0 → HasDerivAt (fun t => ψ (tiltMeasure P g t)) ⟪φ, hg.toLp g⟫_ℝ 0) : IsEfficientInfluenceFunction P ψ φ (boundedTiltSubmodels P) := by constructor · intro m hm rcases hm with ⟨g, M, hg_meas, hgM, hg_mean, hg, rfl⟩ simpa [tiltRegularSubmodel] using hderiv g M hg hg_meas hgM hg_mean · rw [tangentSpace_boundedTiltSubmodels_eq_meanZeroLp] exact hφ -
tangentSpace_eq_Tfulltheorem — For a backdoor ATE estimation system S, the abstract tangent space at its observed-data law equals the ATE layer's full mean-zero tangent space Tfull.hypothesesconclusiontangentSpace S.P_Z (boundedTiltSubmodels S.P_Z) = S.TfullProof (Lean source)
theorem tangentSpace_eq_Tfull (S : ATE.BackdoorEstimationSystem P γ) : tangentSpace S.P_Z (boundedTiltSubmodels S.P_Z) = S.Tfull := by change tangentSpace S.P_Z (boundedTiltSubmodels S.P_Z) = meanZeroLp S.P_Z exact tangentSpace_boundedTiltSubmodels_eq_meanZeroLp S.P_Z
ArmMeanEfficientIF 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.
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
Proof (Lean source)
9 supporting declarations (lemmas, instances)
-
observedArmMean_tilt_exact_expansiontheorem — Exact per-arm expansion along an exponential tilt. Given a probability observed-data law P, an arm d, a measurable score g bounded by M, a nonnegative outcome bound B, a positive overlap level ε, bounded outcomes, and strict overlap in arm d, the arm-mean change minus the tilted mean of its base-law EIF is exactly minus the product of the propensity and regression changes.hypothesesγ :sharedType u_1P :d :g :γ × Bool × ℝ → ℝM B ε t :ℝhg_meas :hgM :∀ z, |g z| ≤ MhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ᵐ z ∂P, ε ≤ observedPropensity P d zconclusionobservedArmMean (tiltMeasure P g t) d- observedArmMean P d- ∫ z, observedArmEIF P d z ∂(tiltMeasure P g t)= -(∫ z, (observedPropensity (tiltMeasure P g t) d z - observedPropensity P d z) / observedPropensity P d z * (observedArmRegression (tiltMeasure P g t) d z - observedArmRegression P d z) ∂(tiltMeasure P g t))Proof (Lean source)
theorem observedArmMean_tilt_exact_expansion (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (d : Bool) (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 : ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) : observedArmMean (tiltMeasure P g t) d - observedArmMean P d - ∫ z, observedArmEIF P d z ∂(tiltMeasure P g t) = -(∫ z, (observedPropensity (tiltMeasure P g t) d z - observedPropensity P d z) / observedPropensity P d z * (observedArmRegression (tiltMeasure P g t) d z - observedArmRegression P d 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 := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hY have hp0P : ∀ᵐ z ∂P, 0 < observedPropensity P d z := by filter_upwards [hoverlap] with z hz exact hε.trans_le hz have hp0 : ∀ᵐ z ∂Pt, 0 < observedPropensity P d z := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hp0P have hpP : ∀ᵐ z ∂P, 0 < observedPropensity Pt d z := by dsimp [Pt] exact observedPropensity_tilt_pos_ae P g M t d hg_meas hgM hp0P have hp : ∀ᵐ z ∂Pt, 0 < observedPropensity Pt d z := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hpP 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 : Integrable (observedArmRegression P d) Pt := by apply Integrable.of_bound (measurable_observedArmRegression P d).aestronglyMeasurable B exact (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (by simpa [Real.norm_eq_abs] using observedArmRegression_abs_le P d B hB hY hp0P) have hμ1 : Integrable (observedArmRegression Pt d) Pt := integrable_observedArmRegression_of_bounded Pt d B hB hYt hp have hinv : ∀ᵐ z ∂Pt, |(observedPropensity P d z)⁻¹| ≤ ε⁻¹ := by have hbase := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hoverlap 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 : 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μb := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (observedArmRegression_abs_le P d B hB hY hp0P) filter_upwards [hYt, hμb, hinv] 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 exact (mul_le_mul hfrac (abs_sub _ _) (abs_nonneg _) (by positivity)).trans (by gcongr) have hprod : 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) have hμ1b := observedArmRegression_abs_le Pt d B hB hYt hp 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] 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 _ ≤ 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 observedArmMean_sub_integral_observedArmEIF_eq_product P Pt d ε⁻¹ hYint hμ0 hμ1 hinv hp0 hp hres hprod -
observedArmMean_tilt_remainder_boundtheorem — Under a measurable bounded tilt score, nonnegative score and outcome bounds, a positive overlap level, bounded outcomes, strict arm overlap, and the local condition |t|M ≤ 1, the treatment-specific-mean von Mises remainder is bounded by the product of the two first-order nuisance bounds.hypothesesγ :sharedType u_1P :d :g :γ × Bool × ℝ → ℝM B ε t :ℝhg_meas :hgM :∀ z, |g z| ≤ MhM :0 ≤ MhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ᵐ z ∂P, ε ≤ observedPropensity P d zht :|t| * M ≤ 1conclusion|observedArmMean (tiltMeasure P g t) d- observedArmMean P d- ∫ z, observedArmEIF P d z ∂(tiltMeasure P g t)|Proof (Lean source)
theorem observedArmMean_tilt_remainder_bound (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (d : Bool) (g : γ × Bool × ℝ → ℝ) (M B ε t : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hM : 0 ≤ M) (hB : 0 ≤ B) (hε : 0 < ε) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hoverlap : ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) (ht : |t| * M ≤ 1) : |observedArmMean (tiltMeasure P g t) d - observedArmMean P d - ∫ z, observedArmEIF P d z ∂(tiltMeasure P g t)| ≤ ε⁻¹ * (4 * (|t| * M) / exp (-|t| * M)) * (4 * B * (|t| * M) / exp (-|t| * M)) := by let Pt := tiltMeasure P g t let Cp := 4 * (|t| * M) / exp (-|t| * M) let Cμ := 4 * B * (|t| * M) / exp (-|t| * M) let K := ε⁻¹ * Cp * Cμ let _ : IsProbabilityMeasure Pt := isProbabilityMeasure_tiltMeasure hg_meas hgM have hp0P : ∀ᵐ z ∂P, 0 < observedPropensity P d z := by filter_upwards [hoverlap] with z hz exact hε.trans_le hz have hinv : ∀ᵐ z ∂Pt, |(observedPropensity P d z)⁻¹| ≤ ε⁻¹ := by have hb := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hoverlap filter_upwards [hb] with z hz have hpz := hε.trans_le hz rw [abs_of_pos (inv_pos.mpr hpz)] exact (inv_le_inv₀ hpz hε).2 hz have hpropP := observedPropensity_tilt_firstOrder P g M t d hg_meas hgM hM ht have hprop : ∀ᵐ z ∂Pt, |observedPropensity Pt d z - observedPropensity P d z| ≤ Cp := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (by simpa [Pt, Cp] using hpropP) have hμP := observedArmRegression_tilt_firstOrder P g M B t d hg_meas hgM hM hB hY hp0P ht have hμ : ∀ᵐ z ∂Pt, |observedArmRegression Pt d z - observedArmRegression P d z| ≤ Cμ := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (by simpa [Pt, Cμ] using hμP) have hpoint : ∀ᵐ z ∂Pt, ‖(observedPropensity Pt d z - observedPropensity P d z) / observedPropensity P d z * (observedArmRegression Pt d z - observedArmRegression P d z)‖ ≤ K := by filter_upwards [hprop, hμ, hinv] with z hpz hμz hinvz rw [Real.norm_eq_abs, abs_mul, abs_div, div_eq_mul_inv, ← abs_inv] have hCp : 0 ≤ Cp := by dsimp [Cp]; positivity have hCμ : 0 ≤ Cμ := by dsimp [Cμ]; positivity have hfirst := mul_le_mul hpz hinvz (abs_nonneg _) hCp exact (mul_le_mul hfirst hμz (abs_nonneg _) (mul_nonneg hCp (inv_nonneg.mpr hε.le))).trans_eq (by dsimp [K]; ring) have hexact := observedArmMean_tilt_exact_expansion P d g M B ε t hg_meas hgM hB hε hY hoverlap rw [hexact, abs_neg] simpa [K, Cp, Cμ] using norm_integral_le_of_norm_le_const hpoint -
observedArmMean_tilt_remainder_quadratictheorem — Under a measurable bounded tilt score, nonnegative score and outcome bounds, a positive overlap level, bounded outcomes, strict arm overlap, and the local condition |t|M ≤ 1, the treatment-specific-mean remainder is bounded by an explicit constant times t².hypothesesγ :sharedType u_1P :d :g :γ × Bool × ℝ → ℝM B ε t :ℝhg_meas :hgM :∀ z, |g z| ≤ MhM :0 ≤ MhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ᵐ z ∂P, ε ≤ observedPropensity P d zht :|t| * M ≤ 1conclusion|observedArmMean (tiltMeasure P g t) d- observedArmMean P d- ∫ z, observedArmEIF P d z ∂(tiltMeasure P g t)|≤ (16 * ε⁻¹ * B * M ^ 2 * exp 2) * t ^ 2Proof (Lean source)
theorem observedArmMean_tilt_remainder_quadratic (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (d : Bool) (g : γ × Bool × ℝ → ℝ) (M B ε t : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hM : 0 ≤ M) (hB : 0 ≤ B) (hε : 0 < ε) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hoverlap : ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) (ht : |t| * M ≤ 1) : |observedArmMean (tiltMeasure P g t) d - observedArmMean P d - ∫ z, observedArmEIF P d z ∂(tiltMeasure P g t)| ≤ (16 * ε⁻¹ * B * M ^ 2 * exp 2) * t ^ 2 := by have hraw := observedArmMean_tilt_remainder_bound P d g M B ε t hg_meas hgM hM hB hε hY hoverlap ht let x := |t| * M have hrecip : (exp (-x))⁻¹ ≤ exp 1 := by rw [← Real.exp_neg] simp only [neg_neg] exact Real.exp_le_exp.mpr ht have hp : 4 * x / exp (-x) ≤ 4 * x * exp 1 := by rw [div_eq_mul_inv] exact mul_le_mul_of_nonneg_left hrecip (by positivity) have hμ : 4 * B * x / exp (-x) ≤ 4 * B * x * exp 1 := by rw [div_eq_mul_inv] exact mul_le_mul_of_nonneg_left hrecip (by positivity) calc _ ≤ ε⁻¹ * (4 * x / exp (-x)) * (4 * B * x / exp (-x)) := by simpa [x] using hraw _ ≤ ε⁻¹ * (4 * x * exp 1) * (4 * B * x * exp 1) := by gcongr _ = (16 * ε⁻¹ * B * M ^ 2 * exp 2) * t ^ 2 := by rw [show exp 2 = exp 1 * exp 1 by simpa only [one_add_one_eq_two] using Real.exp_add 1 1] dsimp [x] ring_nf rw [sq_abs] ring -
observedArmMean_abs_letheorem — Given a probability observed-data law P, an arm d, a nonnegative outcome bound B, bounded outcomes, and positive arm propensity, the absolute arm mean is at most B.hypothesesγ :sharedType u_1P :d :B :ℝhB :0 ≤ BhY :∀ᵐ z ∂P, |projY z| ≤ Bhp :∀ᵐ z ∂P, 0 < observedPropensity P d zconclusion|observedArmMean P d| ≤ BProof (Lean source)
theorem observedArmMean_abs_le (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (d : Bool) (B : ℝ) (hB : 0 ≤ B) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hp : ∀ᵐ z ∂P, 0 < observedPropensity P d z) : |observedArmMean P d| ≤ B := by rw [observedArmMean] have hb : ∀ᵐ z ∂P, ‖observedArmRegression P d z‖ ≤ B := by simpa [Real.norm_eq_abs] using observedArmRegression_abs_le P d B hB hY hp simpa [Real.norm_eq_abs] using norm_integral_le_of_norm_le_const hb -
memLp_observedArmEIFtheorem — 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 treatment-specific-mean influence function belongs to L²(P).hypothesesγ :sharedType u_1P :d :B ε :ℝhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ᵐ z ∂P, ε ≤ observedPropensity P d zconclusionMemLp (observedArmEIF P d) 2 PProof (Lean source)
theorem memLp_observedArmEIF (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) : MemLp (observedArmEIF P d) 2 P := by have hp : ∀ᵐ z ∂P, 0 < observedPropensity P d z := by filter_upwards [hoverlap] with z hz exact hε.trans_le hz have hμ := observedArmRegression_abs_le P d B hB hY hp have hψ := observedArmMean_abs_le P d B hB hY hp apply MemLp.of_bound (((measurable_observedArmIndicator d).div (measurable_observedPropensity P d) |>.mul (measurable_snd.snd.sub (measurable_observedArmRegression P d)) |>.add (measurable_observedArmRegression P d) |>.sub measurable_const).aestronglyMeasurable) (ε⁻¹ * (B + B) + B + B) filter_upwards [hY, hμ, hoverlap] with z hYz hμz hez rw [Real.norm_eq_abs] change |observedArmIndicator d z / observedPropensity P d z * (projY z - observedArmRegression P d z) + observedArmRegression P d z - observedArmMean P d| ≤ ε⁻¹ * (B + B) + B + B have hpz : 0 < observedPropensity P d z := hε.trans_le hez have hinv : |(observedPropensity P d z)⁻¹| ≤ ε⁻¹ := by rw [abs_of_pos (inv_pos.mpr hpz)] exact (inv_le_inv₀ hpz hε).2 hez 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_mul] exact (mul_le_of_le_one_left (abs_nonneg _) hI).trans hinv have hdiff : |projY z - observedArmRegression P d z| ≤ B + B := (abs_sub _ _).trans (by linarith) have hres : |observedArmIndicator d z / observedPropensity P d z * (projY z - observedArmRegression P d z)| ≤ ε⁻¹ * (B + B) := by rw [abs_mul] exact mul_le_mul hfrac hdiff (abs_nonneg _) (by positivity) have hcenter : |observedArmRegression P d z - observedArmMean P d| ≤ B + B := (abs_sub _ _).trans (by linarith) calc _ = |observedArmIndicator d z / observedPropensity P d z * (projY z - observedArmRegression P d z) + (observedArmRegression P d z - observedArmMean P d)| := by ring_nf _ ≤ |observedArmIndicator d z / observedPropensity P d z * (projY z - observedArmRegression P d z)| + |observedArmRegression P d z - observedArmMean P d| := abs_add_le _ _ _ ≤ ε⁻¹ * (B + B) + (B + B) := add_le_add hres hcenter _ = ε⁻¹ * (B + B) + B + B := by ring -
integral_observedArmEIF_eq_zerotheorem — 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 treatment-specific-mean influence function has mean zero.hypothesesγ :sharedType u_1P :d :B ε :ℝhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ᵐ z ∂P, ε ≤ observedPropensity P d zconclusion∫ z, observedArmEIF P d z ∂P = 0Proof (Lean source)
theorem integral_observedArmEIF_eq_zero (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) : ∫ z, observedArmEIF P d z ∂P = 0 := by have h := observedArmMean_tilt_exact_expansion P d (fun _ => 0) 0 B ε 0 measurable_const (fun _ => by simp) hB hε hY hoverlap simpa [tiltMeasure_zero] using h -
hasDerivAt_observedArmMean_tilttheorem — Given a probability observed-data law P, an arm d, a measurable score g bounded by a nonnegative constant M, a nonnegative outcome bound B, a positive overlap level ε, bounded outcomes, strict arm overlap, and a mean-zero score, the arm mean along its exponential tilt has derivative equal to the covariance with the arm EIF.hypothesesγ :sharedType u_1P :d :g :γ × Bool × ℝ → ℝM B ε :ℝhg_meas :hgM :∀ z, |g z| ≤ Mhg_mean :∫ z, g z ∂P = 0hM :0 ≤ MhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ᵐ z ∂P, ε ≤ observedPropensity P d zconclusionProof (Lean source)
theorem hasDerivAt_observedArmMean_tilt (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (d : Bool) (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 : ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) : HasDerivAt (fun t => observedArmMean (tiltMeasure P g t) d) (∫ z, observedArmEIF P d z * g z ∂P) 0 := by have hφ := memLp_observedArmEIF P d B ε hB hε hY hoverlap have hφ_mean := integral_observedArmEIF_eq_zero P d B ε hB hε hY hoverlap let C : ℝ := 16 * ε⁻¹ * B * M ^ 2 * exp 2 apply hasDerivAt_tilt_of_quadratic_vonMises_remainder P (fun Q => observedArmMean Q d) (observedArmEIF P d) g M C hφ hg_meas hgM hg_mean have ht : ∀ᶠ t in 𝓝 (0 : ℝ), |t| * M ≤ 1 := by rcases hM.eq_or_lt with rfl | hMpos · simp · apply Metric.eventually_nhds_iff.mpr refine ⟨M⁻¹, inv_pos.mpr hMpos, ?_⟩ intro t ht rw [Real.dist_eq, sub_zero] at ht exact le_of_lt <| calc |t| * M < M⁻¹ * M := mul_lt_mul_of_pos_right ht hMpos _ = 1 := inv_mul_cancel₀ hMpos.ne' filter_upwards [ht] with t ht simpa [C, hφ_mean] using observedArmMean_tilt_remainder_quadratic P d g M B ε t hg_meas hgM hM hB hε hY hoverlap ht -
memLp_observedAIPWtheorem — Given a probability observed-data law P, a nonnegative outcome bound B, a positive overlap level ε, bounded outcomes, and strict overlap in both arms, the observed- law AIPW influence function belongs to L²(P).hypothesesγ :sharedType u_1P :B ε :ℝhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d zconclusionMemLp (observedAIPW P) 2 PProof (Lean source)
theorem memLp_observedAIPW (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) : MemLp (observedAIPW P) 2 P := 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 hsub := (memLp_observedArmEIF P true B ε hB hε hY (hoverlap true)).sub (memLp_observedArmEIF P false B ε hB hε hY (hoverlap false)) exact (memLp_congr_ae (ae_of_all P fun z => observedAIPW_eq_armEIF_sub P hμ z)).2 hsub -
integral_observedAIPW_eq_zerotheorem — Given a probability observed-data law P, a nonnegative outcome bound B, a positive overlap level ε, bounded outcomes, and strict overlap in both arms, the observed- law AIPW influence function has mean zero.hypothesesγ :sharedType u_1P :B ε :ℝhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d zconclusion∫ z, observedAIPW P z ∂P = 0Proof (Lean source)
theorem integral_observedAIPW_eq_zero (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) : ∫ z, observedAIPW P 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 htrue := integral_observedArmEIF_eq_zero P true B ε hB hε hY (hoverlap true) have hfalse := integral_observedArmEIF_eq_zero P false B ε hB hε hY (hoverlap false) have hint (d : Bool) := (memLp_observedArmEIF P d B ε hB hε hY (hoverlap d)).integrable (by norm_num) calc _ = ∫ z, observedArmEIF P true z - observedArmEIF P false z ∂P := by apply integral_congr_ae filter_upwards with z rw [observedAIPW_eq_armEIF_sub P hμ] _ = (∫ z, observedArmEIF P true z ∂P) - ∫ z, observedArmEIF P false z ∂P := integral_sub (hint true) (hint false) _ = 0 := by rw [htrue, hfalse, sub_zero]
ATEEfficientIF 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.
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
Proof (Lean source)
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
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
observedOutcome_boundedlemma — Given a backdoor estimation system S and a factual-outcome bound B, the induced observed outcome is bounded by B almost everywhere.hypothesesγ :sharedType u_1S :ATE.BackdoorEstimationSystem P γB :ℝhY_bound :∀ ω, |S.toPOBackdoorSystem.factualY ω| ≤ Bconclusion∀ᵐ z ∂S.P_Z, |projY z| ≤ BProof (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) -
observedPropensity_overlaplemma — Given a backdoor estimation system S and strict overlap at level ε, the induced observed law has overlap at level ε in both arms.hypothesesγ :sharedType u_1S :ATE.BackdoorEstimationSystem P γε :ℝh_overlap :S.StrictOverlap εd :conclusion∀ᵐ z ∂S.P_Z, ε ≤ observedPropensity S.P_Z d zProof (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 -
observedAIPW_memLp_of_boundedtheorem — 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².hypothesesγ :sharedType u_1S :ATE.BackdoorEstimationSystem P γε B :ℝh_overlap :S.StrictOverlap εhB :0 ≤ BhY_bound :∀ ω, |S.toPOBackdoorSystem.factualY ω| ≤ BconclusionMemLp (observedAIPW S.P_Z) 2 S.P_ZProof (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)
ATEPathwiseDerivative 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.
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
Proof (Lean source)
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
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
observedATE_tilt_remainder_boundtheorem — Under a measurable bounded tilt score, nonnegative tilt and outcome bounds and a positive overlap level, bounded outcomes, strict overlap, and a local tilt satisfying |t|M ≤ 1, the exact ATE remainder is bounded by the product of the two first-order nuisance bounds, hence is quadratic in the tilt size.hypothesesγ :sharedType u_1P :g :γ × Bool × ℝ → ℝM B ε t :ℝhg_meas :hgM :∀ z, |g z| ≤ MhM :0 ≤ MhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d zht :|t| * M ≤ 1conclusionProof (Lean source)
theorem observedATE_tilt_remainder_bound (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M B ε t : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hM : 0 ≤ M) (hB : 0 ≤ B) (hε : 0 < ε) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hoverlap : ∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) (ht : |t| * M ≤ 1) : |observedATE (tiltMeasure P g t) - observedATE P - ∫ z, observedAIPW P z ∂(tiltMeasure P g t)| ≤ 2 * (ε⁻¹ * (4 * (|t| * M) / exp (-|t| * M)) * (4 * B * (|t| * M) / exp (-|t| * M))) := by let Pt := tiltMeasure P g t let Cp := 4 * (|t| * M) / exp (-|t| * M) let Cμ := 4 * B * (|t| * M) / exp (-|t| * M) let K := ε⁻¹ * Cp * Cμ let _ : IsProbabilityMeasure Pt := isProbabilityMeasure_tiltMeasure hg_meas hgM 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 hinv (d : Bool) : ∀ᵐ z ∂Pt, |(observedPropensity P d z)⁻¹| ≤ ε⁻¹ := by have hb := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (hoverlap d) filter_upwards [hb] with z hz have hpz := hε.trans_le hz rw [abs_of_pos (inv_pos.mpr hpz)] exact (inv_le_inv₀ hpz hε).2 hz have hpropP (d : Bool) := observedPropensity_tilt_firstOrder P g M t d hg_meas hgM hM ht have hprop (d : Bool) : ∀ᵐ z ∂Pt, |observedPropensity Pt d z - observedPropensity P d z| ≤ Cp := by exact (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (by simpa [Pt, Cp] using hpropP d) have hμP (d : Bool) := observedArmRegression_tilt_firstOrder P g M B t d hg_meas hgM hM hB hY (hp0P d) ht have hμ (d : Bool) : ∀ᵐ z ∂Pt, |observedArmRegression Pt d z - observedArmRegression P d z| ≤ Cμ := by exact (ae_tiltMeasure_iff P g M t hg_meas hgM).2 (by simpa [Pt, Cμ] using hμP d) have hterm (d : Bool) : |∫ z, (observedPropensity Pt d z - observedPropensity P d z) / observedPropensity P d z * (observedArmRegression Pt d z - observedArmRegression P d z) ∂Pt| ≤ K := by have hpoint : ∀ᵐ z ∂Pt, ‖(observedPropensity Pt d z - observedPropensity P d z) / observedPropensity P d z * (observedArmRegression Pt d z - observedArmRegression P d z)‖ ≤ K := by filter_upwards [hprop d, hμ d, hinv d] with z hpz hμz hinvz rw [Real.norm_eq_abs, abs_mul, abs_div, div_eq_mul_inv, ← abs_inv] have hCp : 0 ≤ Cp := by dsimp [Cp] positivity have hCμ : 0 ≤ Cμ := by dsimp [Cμ] positivity have hfirst : |observedPropensity Pt d z - observedPropensity P d z| * |(observedPropensity P d z)⁻¹| ≤ Cp * ε⁻¹ := mul_le_mul hpz hinvz (abs_nonneg _) hCp have hall := mul_le_mul hfirst hμz (abs_nonneg _) (mul_nonneg hCp (inv_nonneg.mpr hε.le)) calc _ ≤ (Cp * ε⁻¹) * Cμ := hall _ = K := by dsimp [K]; ring simpa [K] using norm_integral_le_of_norm_le_const hpoint have hexact := observedATE_tilt_exact_expansion P g M B ε t hg_meas hgM hB hε hY hoverlap rw [hexact] calc |-(∫ z, (observedPropensity Pt true z - observedPropensity P true z) / observedPropensity P true z * (observedArmRegression Pt true z - observedArmRegression P true z) ∂Pt) + ∫ z, (observedPropensity Pt false z - observedPropensity P false z) / observedPropensity P false z * (observedArmRegression Pt false z - observedArmRegression P false z) ∂Pt| ≤ |(∫ z, (observedPropensity Pt true z - observedPropensity P true z) / observedPropensity P true z * (observedArmRegression Pt true z - observedArmRegression P true z) ∂Pt)| + |(∫ z, (observedPropensity Pt false z - observedPropensity P false z) / observedPropensity P false z * (observedArmRegression Pt false z - observedArmRegression P false z) ∂Pt)| := by simpa only [abs_neg] using abs_add_le (-(∫ z, (observedPropensity Pt true z - observedPropensity P true z) / observedPropensity P true z * (observedArmRegression Pt true z - observedArmRegression P true z) ∂Pt)) (∫ z, (observedPropensity Pt false z - observedPropensity P false z) / observedPropensity P false z * (observedArmRegression Pt false z - observedArmRegression P false z) ∂Pt) _ ≤ K + K := add_le_add (hterm true) (hterm false) _ = 2 * (ε⁻¹ * (4 * (|t| * M) / exp (-|t| * M)) * (4 * B * (|t| * M) / exp (-|t| * M))) := by simp only [K, Cp, Cμ] ring -
observedATE_tilt_remainder_quadratictheorem — Under a measurable bounded tilt score, nonnegative tilt and outcome bounds and a positive overlap level, bounded outcomes and strict overlap, and a local tilt, the ATE remainder is bounded by an explicit constant times t².hypothesesγ :sharedType u_1P :g :γ × Bool × ℝ → ℝM B ε t :ℝhg_meas :hgM :∀ z, |g z| ≤ MhM :0 ≤ MhB :0 ≤ Bhε :0 < εhY :∀ᵐ z ∂P, |projY z| ≤ Bhoverlap :∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d zht :|t| * M ≤ 1conclusion|observedATE (tiltMeasure P g t)- observedATE P- ∫ z, observedAIPW P z ∂(tiltMeasure P g t)|≤ (32 * ε⁻¹ * B * M ^ 2 * exp 2) * t ^ 2Proof (Lean source)
theorem observedATE_tilt_remainder_quadratic (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M B ε t : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hM : 0 ≤ M) (hB : 0 ≤ B) (hε : 0 < ε) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) (hoverlap : ∀ d, ∀ᵐ z ∂P, ε ≤ observedPropensity P d z) (ht : |t| * M ≤ 1) : |observedATE (tiltMeasure P g t) - observedATE P - ∫ z, observedAIPW P z ∂(tiltMeasure P g t)| ≤ (32 * ε⁻¹ * B * M ^ 2 * exp 2) * t ^ 2 := by have hraw := observedATE_tilt_remainder_bound P g M B ε t hg_meas hgM hM hB hε hY hoverlap ht let x := |t| * M have hx : 0 ≤ x := by dsimp [x]; positivity have hrecip : (exp (-x))⁻¹ ≤ exp 1 := by rw [← Real.exp_neg] simp only [neg_neg] exact Real.exp_le_exp.mpr ht have hp : 4 * x / exp (-x) ≤ 4 * x * exp 1 := by rw [div_eq_mul_inv] exact mul_le_mul_of_nonneg_left hrecip (by positivity) have hμ : 4 * B * x / exp (-x) ≤ 4 * B * x * exp 1 := by rw [div_eq_mul_inv] exact mul_le_mul_of_nonneg_left hrecip (by positivity) calc |observedATE (tiltMeasure P g t) - observedATE P - ∫ z, observedAIPW P z ∂(tiltMeasure P g t)| ≤ 2 * (ε⁻¹ * (4 * x / exp (-x)) * (4 * B * x / exp (-x))) := by simpa [x] using hraw _ ≤ 2 * (ε⁻¹ * (4 * x * exp 1) * (4 * B * x * exp 1)) := by gcongr _ = (32 * ε⁻¹ * B * M ^ 2 * exp 2) * t ^ 2 := by rw [show exp 2 = exp 1 * exp 1 by simpa only [one_add_one_eq_two] using Real.exp_add 1 1] dsimp [x] ring_nf rw [sq_abs] ring
ATETiltNuisance 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.
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
Proof (Lean source)
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
Proof (Lean source)
13 supporting declarations (lemmas, instances)
-
abs_condExp_le_mul_condExp_of_abs_lelemma — If two integrable functions f and h satisfy the pointwise domination |f| ≤ K h, then the conditional expectation of f is dominated by K times the conditional expectation of h.hypothesesconclusion∀ᵐ z ∂P, |P[f | m] z| ≤ K * P[h | m] zProof (Lean source)
lemma abs_condExp_le_mul_condExp_of_abs_le {m₀ : MeasurableSpace Z} {P : @Measure Z m₀} [IsFiniteMeasure P] {m : MeasurableSpace Z} {f h : Z → ℝ} {K : ℝ} (hf : Integrable f P) (hh : Integrable h P) (hdom : ∀ᵐ z ∂P, |f z| ≤ K * h z) : ∀ᵐ z ∂P, |P[f | m] z| ≤ K * P[h | m] z := by have hnorm := norm_condExp_le (μ := P) (m := m) f have hmono : P[fun w => ‖f w‖ | m] ≤ᵐ[P] P[K • h | m] := condExp_mono (m := m) hf.norm (hh.smul K) (by filter_upwards [hdom] with z hz simpa [Real.norm_eq_abs, Pi.smul_apply, smul_eq_mul] using hz) have hsmul := condExp_smul (μ := P) K h m filter_upwards [hnorm, hmono, hsmul] with z hn hz hs rw [show |P[f | m] z| = ‖P[f | m] z‖ by rfl] calc ‖P[f | m] z‖ ≤ P[fun w => ‖f w‖ | m] z := hn _ ≤ P[K • h | m] z := hz _ = K * P[h | m] z := by simpa [Pi.smul_apply, smul_eq_mul] using hs -
abs_exp_score_sub_one_lelemma — A bounded score g at a local perturbation satisfying |t|M ≤ 1 gives an exponential weight whose distance from one is at most 2|t|M.hypothesesconclusion|exp (t * g z) - 1| ≤ 2 * (|t| * M)Proof (Lean source)
lemma abs_exp_score_sub_one_le (g : Z → ℝ) (M t : ℝ) (hgM : ∀ z, |g z| ≤ M) (ht : |t| * M ≤ 1) (z : Z) : |exp (t * g z) - 1| ≤ 2 * (|t| * M) := by have harg : |t * g z| ≤ |t| * M := by rw [abs_mul] exact mul_le_mul_of_nonneg_left (hgM z) (abs_nonneg t) exact (Real.abs_exp_sub_one_le (harg.trans ht)).trans (mul_le_mul_of_nonneg_left harg (by norm_num)) -
exp_neg_abs_mul_le_exp_scorelemma — A bounded score g gives an exponential weight bounded below by exp(-|t|M).hypothesesProof (Lean source)
lemma exp_neg_abs_mul_le_exp_score (g : Z → ℝ) (M t : ℝ) (hgM : ∀ z, |g z| ≤ M) (z : Z) : exp (-|t| * M) ≤ exp (t * g z) := by apply Real.exp_le_exp.mpr calc -|t| * M = -(|t| * M) := by ring _ ≤ -|t * g z| := neg_le_neg (by rw [abs_mul] exact mul_le_mul_of_nonneg_left (hgM z) (abs_nonneg t)) _ ≤ t * g z := neg_abs_le _ -
condExp_tiltMeasure_ae_eq_div_explemma — Under a conditioning σ-algebra contained in the ambient σ-algebra and a bounded exponential tilt, the conditional expectation of an integrable target is the ratio of the base-law conditional expectations weighted by the unnormalized exponential.hypothesesP :m :hm :m ≤ mZg f :Z → ℝM t :ℝhg_meas :@Measurable Z ℝ mZ _ ghgM :∀ z, |g z| ≤ Mhf :Integrable f (@tiltMeasure Z mZ P g t)Proof (Lean source)
lemma condExp_tiltMeasure_ae_eq_div_exp (P : Measure Z) [IsProbabilityMeasure P] {m : MeasurableSpace Z} (hm : m ≤ mZ) (g f : Z → ℝ) (M t : ℝ) (hg_meas : @Measurable Z ℝ mZ _ g) (hgM : ∀ z, |g z| ≤ M) (hf : Integrable f (@tiltMeasure Z mZ P g t)) : @condExp Z ℝ m mZ _ _ (@tiltMeasure Z mZ P g t) f =ᵐ[P] fun z => P[fun y => f y * exp (t * g y) | m] z / P[fun y => exp (t * g y) | m] z := by let c := ∫ y, exp (t * g y) ∂P have hc : 0 < c := by simpa [c, tiltNorm] using (@tiltNorm_pos Z mZ P _ g M t hg_meas hgM) have hP : @tiltMeasure Z mZ P g t = P.withDensity (fun z => ofReal (exp (t * g z) / c)) := by simpa [c] using (@tiltMeasure_eq_withDensity_div Z mZ P _ g M t hg_meas hgM) have hf' : Integrable f (P.withDensity (fun z => ofReal (exp (t * g z) / c))) := by simpa [hP] using hf have hbayes := @condExp_expTilt_ae_eq_div Z mZ P _ m hm g f t hg_meas ⟨M, hgM⟩ hf' have hnum := condExp_smul (μ := P) (c⁻¹) (fun y => f y * exp (t * g y)) m have hden := condExp_smul (μ := P) (c⁻¹) (fun y => exp (t * g y)) m rw [hP] filter_upwards [hbayes, hnum, hden] with z hb hn hd rw [hb] change P[fun y => f y * (exp (t * g y) / c) | m] z / P[fun y => exp (t * g y) / c | m] z = _ have hnum_eq : P[fun y => f y * (exp (t * g y) / c) | m] z = c⁻¹ * P[fun y => f y * exp (t * g y) | m] z := by calc _ = P[c⁻¹ • fun y => f y * exp (t * g y) | m] z := by congr 2 funext y simp only [Pi.smul_apply, smul_eq_mul] field_simp _ = (c⁻¹ • P[fun y => f y * exp (t * g y) | m]) z := hn _ = _ := by simp only [Pi.smul_apply, smul_eq_mul] have hden_eq : P[fun y => exp (t * g y) / c | m] z = c⁻¹ * P[fun y => exp (t * g y) | m] z := by calc _ = P[c⁻¹ • fun y => exp (t * g y) | m] z := by congr 2 funext y simp only [Pi.smul_apply, smul_eq_mul] field_simp _ = (c⁻¹ • P[fun y => exp (t * g y) | m]) z := hd _ = _ := by simp only [Pi.smul_apply, smul_eq_mul] rw [hnum_eq, hden_eq] field_simp -
ae_tiltMeasure_ifflemma — Under a measurable bounded score, a property holds almost everywhere under an exponential tilt exactly when it holds almost everywhere under the base probability law, because the normalized exponential density is everywhere strictly positive.hypothesesP :g :Z → ℝM t :ℝhg_meas :hgM :∀ z, |g z| ≤ Mp :Z → Propconclusion(∀ᵐ z ∂tiltMeasure P g t, p z) ↔ ∀ᵐ z ∂P, p zProof (Lean source)
lemma ae_tiltMeasure_iff (P : Measure Z) [IsProbabilityMeasure P] (g : Z → ℝ) (M t : ℝ) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) {p : Z → Prop} : (∀ᵐ z ∂tiltMeasure P g t, p z) ↔ ∀ᵐ z ∂P, p z := by rw [tiltMeasure_eq_withDensity_div P g M t hg_meas hgM] have hdens_meas : Measurable (fun z => ofReal (exp (t * g z) / ∫ y, exp (t * g y) ∂P)) := by fun_prop rw [ae_withDensity_iff hdens_meas] have hc : 0 < ∫ y, exp (t * g y) ∂P := by simpa [tiltNorm] using tiltNorm_pos (P := P) (s := g) (t := t) hg_meas hgM constructor · intro hp filter_upwards [hp] with z hz exact hz (ENNReal.ofReal_ne_zero_iff.mpr (div_pos (Real.exp_pos _) hc)) · intro hp filter_upwards [hp] with z hz _ exact hz -
abs_div_sub_div_le_of_relative_boundslemma — If two numerator-denominator pairs are first-order close, the base denominator is positive, the retained fraction, envelope constant, and perturbation size have the required signs, the perturbed denominator retains a fraction a of it, and the base numerator is controlled by the base denominator, then their ratios differ by at most 2 K δ / a.hypothesesA At p pt K δ a :ℝhp :0 < pha :0 < ahpt_lower :a * p ≤ pthK :0 ≤ Khδ :0 ≤ δhA :|A| ≤ K * phAt :|At - A| ≤ K * δ * phpt :|pt - p| ≤ δ * pconclusion|At / pt - A / p| ≤ 2 * K * δ / aProof (Lean source)
lemma abs_div_sub_div_le_of_relative_bounds {A At p pt K δ a : ℝ} (hp : 0 < p) (ha : 0 < a) (hpt_lower : a * p ≤ pt) (hK : 0 ≤ K) (hδ : 0 ≤ δ) (hA : |A| ≤ K * p) (hAt : |At - A| ≤ K * δ * p) (hpt : |pt - p| ≤ δ * p) : |At / pt - A / p| ≤ 2 * K * δ / a := by have hpt_pos : 0 < pt := (mul_pos ha hp).trans_le hpt_lower have hnum : |At * p - A * pt| ≤ 2 * K * δ * p ^ 2 := by calc |At * p - A * pt| = |(At - A) * p + A * (p - pt)| := by ring_nf _ ≤ |At - A| * |p| + |A| * |p - pt| := by simpa only [abs_mul] using abs_add_le ((At - A) * p) (A * (p - pt)) _ ≤ (K * δ * p) * p + (K * p) * (δ * p) := by rw [abs_of_pos hp, abs_sub_comm p pt] exact add_le_add (mul_le_mul_of_nonneg_right hAt hp.le) (mul_le_mul hA hpt (abs_nonneg _) (mul_nonneg hK hp.le)) _ = 2 * K * δ * p ^ 2 := by ring rw [div_sub_div At A hpt_pos.ne' hp.ne'] have hmul : At * p - pt * A = At * p - A * pt := by ring rw [hmul, abs_div, abs_of_pos (mul_pos hpt_pos hp)] apply (div_le_iff₀ (mul_pos hpt_pos hp)).2 calc |At * p - A * pt| ≤ 2 * K * δ * p ^ 2 := hnum _ ≤ (2 * K * δ / a) * (pt * p) := by have hfac : 0 ≤ 2 * K * δ / a := by positivity have := mul_le_mul_of_nonneg_right hpt_lower hp.le calc 2 * K * δ * p ^ 2 = (2 * K * δ / a) * ((a * p) * p) := by field_simp <;> ring _ ≤ (2 * K * δ / a) * (pt * p) := mul_le_mul_of_nonneg_left this hfac -
abs_condExp_mul_sub_condExp_lelemma — If two functions are integrable, the weight is measurable, the envelope constant is nonnegative, the conditioning function is nonnegative, a target f is dominated by K h, and a weight u differs from one by at most δ, then weighting changes the conditional expectation of f by at most K δ times the conditional expectation of h.hypothesesm :f h u :Z → ℝK δ :ℝhf :Integrable f Phh :Integrable h Phu_meas :@Measurable Z ℝ m₀ _ uhK :0 ≤ Khhnonneg :∀ᵐ z ∂P, 0 ≤ h zhdom :∀ᵐ z ∂P, |f z| ≤ K * h zhu_bound :∀ z, |u z - 1| ≤ δconclusion∀ᵐ z ∂P, |P[fun y => f y * u y | m] z - P[f | m] z| ≤ K * δ * P[h | m] zProof (Lean source)
lemma abs_condExp_mul_sub_condExp_le {m₀ : MeasurableSpace Z} {P : @Measure Z m₀} [IsFiniteMeasure P] {m : MeasurableSpace Z} {f h u : Z → ℝ} {K δ : ℝ} (hf : Integrable f P) (hh : Integrable h P) (hu_meas : @Measurable Z ℝ m₀ _ u) (hK : 0 ≤ K) (hhnonneg : ∀ᵐ z ∂P, 0 ≤ h z) (hdom : ∀ᵐ z ∂P, |f z| ≤ K * h z) (hu_bound : ∀ z, |u z - 1| ≤ δ) : ∀ᵐ z ∂P, |P[fun y => f y * u y | m] z - P[f | m] z| ≤ K * δ * P[h | m] z := by have hdiff : Integrable (fun z => f z * (u z - 1)) P := hf.mul_bdd (hu_meas.sub measurable_const).aestronglyMeasurable (Eventually.of_forall fun z => by simpa only [Real.norm_eq_abs] using hu_bound z) have hfu : Integrable (fun z => f z * u z) P := by refine (hdiff.add hf).congr (Eventually.of_forall fun z => ?_) simp only [Pi.add_apply] ring have hce_sub := condExp_sub hfu hf m have hce_congr : P[(fun z => f z * u z) - f | m] =ᵐ[P] P[fun z => f z * (u z - 1) | m] := by apply condExp_congr_ae filter_upwards with z simp only [Pi.sub_apply] ring have hdiff_dom : ∀ᵐ z ∂P, |f z * (u z - 1)| ≤ (K * δ) * h z := by filter_upwards [hdom, hhnonneg] with z hfz hhz rw [abs_mul] calc |f z| * |u z - 1| ≤ (K * h z) * δ := mul_le_mul hfz (hu_bound z) (abs_nonneg _) (mul_nonneg hK hhz) _ = (K * δ) * h z := by ring have hbound := abs_condExp_le_mul_condExp_of_abs_le (m := m) hdiff hh hdiff_dom filter_upwards [hce_sub, hce_congr, hbound] with z hsub hcongr hboundz change P[(fun z => f z * u z) - f | m] z = P[fun z => f z * u z | m] z - P[f | m] z at hsub rw [← hsub, hcongr] exact hboundz -
abs_condExp_ratio_mul_sub_lelemma — Suppose the numerator and conditioning weight are integrable, the envelope constant and retained fraction have the required signs, a nonnegative conditioning weight h has positive conditional mean, a numerator f is bounded by K h, and a measurable perturbation weight u within δ of one and at least a. Then the corresponding conditional ratios differ by at most 2 K δ / a.hypothesesm :f h u :Z → ℝK δ a :ℝhf :Integrable f Phh :Integrable h Phu_meas :@Measurable Z ℝ m₀ _ uhK :0 ≤ Khδ :0 ≤ δha :0 < ahhnonneg :∀ᵐ z ∂P, 0 ≤ h zhp :∀ᵐ z ∂P, 0 < P[h | m] zhdom :∀ᵐ z ∂P, |f z| ≤ K * h zhu_bound :∀ z, |u z - 1| ≤ δhu_lower :∀ z, a ≤ u zconclusion∀ᵐ z ∂P, |P[fun y => f y * u y | m] z / P[fun y => h y * u y | m] z- P[f | m] z / P[h | m] z|≤ 2 * K * δ / aProof (Lean source)
lemma abs_condExp_ratio_mul_sub_le {m₀ : MeasurableSpace Z} {P : @Measure Z m₀} [IsFiniteMeasure P] {m : MeasurableSpace Z} {f h u : Z → ℝ} {K δ a : ℝ} (hf : Integrable f P) (hh : Integrable h P) (hu_meas : @Measurable Z ℝ m₀ _ u) (hK : 0 ≤ K) (hδ : 0 ≤ δ) (ha : 0 < a) (hhnonneg : ∀ᵐ z ∂P, 0 ≤ h z) (hp : ∀ᵐ z ∂P, 0 < P[h | m] z) (hdom : ∀ᵐ z ∂P, |f z| ≤ K * h z) (hu_bound : ∀ z, |u z - 1| ≤ δ) (hu_lower : ∀ z, a ≤ u z) : ∀ᵐ z ∂P, |P[fun y => f y * u y | m] z / P[fun y => h y * u y | m] z - P[f | m] z / P[h | m] z| ≤ 2 * K * δ / a := by have hu_norm : ∀ z, |u z| ≤ δ + 1 := by intro z calc |u z| = |(u z - 1) + 1| := by ring_nf _ ≤ |u z - 1| + |(1 : ℝ)| := abs_add_le _ _ _ ≤ δ + 1 := by simpa using add_le_add_right (hu_bound z) 1 have hhu : Integrable (fun z => h z * u z) P := hh.mul_bdd hu_meas.aestronglyMeasurable (Eventually.of_forall fun z => by simpa only [Real.norm_eq_abs] using hu_norm z) have hfu : Integrable (fun z => f z * u z) P := hf.mul_bdd hu_meas.aestronglyMeasurable (Eventually.of_forall fun z => by simpa only [Real.norm_eq_abs] using hu_norm z) have hAt := abs_condExp_mul_sub_condExp_le (m := m) hf hh hu_meas hK hhnonneg hdom hu_bound have hhdom : ∀ᵐ z ∂P, |h z| ≤ (1 : ℝ) * h z := by filter_upwards [hhnonneg] with z hz simp [abs_of_nonneg hz] have hpt := abs_condExp_mul_sub_condExp_le (m := m) hh hh hu_meas (show 0 ≤ (1 : ℝ) by norm_num) hhnonneg hhdom hu_bound have hA := abs_condExp_le_mul_condExp_of_abs_le (m := m) hf hh hdom have hlower_raw : P[a • h | m] ≤ᵐ[P] P[fun z => h z * u z | m] := condExp_mono (hh.smul a) hhu (by filter_upwards [hhnonneg] with z hz simp only [Pi.smul_apply, smul_eq_mul] simpa only [mul_comm] using mul_le_mul_of_nonneg_left (hu_lower z) hz) have hsmul := condExp_smul (μ := P) a h m filter_upwards [hp, hAt, hpt, hA, hlower_raw, hsmul] with z hpz hAtz hptz hAz hlowerz hsmulz have hlower : a * P[h | m] z ≤ P[fun y => h y * u y | m] z := by calc a * P[h | m] z = (a • P[h | m]) z := by simp only [Pi.smul_apply, smul_eq_mul] _ = P[a • h | m] z := hsmulz.symm _ ≤ P[fun y => h y * u y | m] z := hlowerz apply abs_div_sub_div_le_of_relative_bounds hpz ha hlower hK hδ hAz hAtz simpa using hptz -
observedPropensity_tilt_ae_eq_expRatiolemma — For a probability law P and a bounded measurable tilt score g, the propensity recomputed under the tilted law is the conditional ratio of unnormalized exponentially weighted arm indicators.hypothesesconclusionobservedPropensity (tiltMeasure P g t) d=ᵐ[P] fun z => P[fun y => observedArmIndicator d y * exp (t * g y) | observedCovariateSigma] z / P[fun y => exp (t * g y) | observedCovariateSigma] zProof (Lean source)
lemma observedPropensity_tilt_ae_eq_expRatio (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M t : ℝ) (d : Bool) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) : observedPropensity (tiltMeasure P g t) d =ᵐ[P] fun z => P[fun y => observedArmIndicator d y * exp (t * g y) | observedCovariateSigma] z / P[fun y => exp (t * g y) | observedCovariateSigma] z := by let _ : IsProbabilityMeasure (tiltMeasure P g t) := isProbabilityMeasure_tiltMeasure hg_meas hgM have hi : Integrable (observedArmIndicator d) (tiltMeasure P g t) := integrable_observedArmIndicator _ d simpa only [observedPropensity] using condExp_tiltMeasure_ae_eq_div_exp P observedCovariateSigma_le g (observedArmIndicator d) M t hg_meas hgM hi -
observedArmRegression_tilt_ae_eq_expRatiolemma — If the observed outcome is bounded by B, then under a bounded measurable tilt, the arm regression recomputed under the tilted law is the ratio of the unnormalized weighted outcome-arm and arm conditional expectations.hypothesesγ :sharedType u_2P :g :γ × Bool × ℝ → ℝM B t :ℝd :hg_meas :hgM :∀ z, |g z| ≤ MhY :∀ᵐ z ∂P, |projY z| ≤ BconclusionobservedArmRegression (tiltMeasure P g t) d=ᵐ[P] fun z => P[fun y => projY y * observedArmIndicator d y * exp (t * g y) | observedCovariateSigma] z / P[fun y => observedArmIndicator d y * exp (t * g y) | observedCovariateSigma] zProof (Lean source)
lemma observedArmRegression_tilt_ae_eq_expRatio (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M B t : ℝ) (d : Bool) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hY : ∀ᵐ z ∂P, |projY z| ≤ B) : observedArmRegression (tiltMeasure P g t) d =ᵐ[P] fun z => P[fun y => projY y * observedArmIndicator d y * exp (t * g y) | observedCovariateSigma] z / P[fun y => observedArmIndicator d y * exp (t * g y) | observedCovariateSigma] z := by let _ : IsProbabilityMeasure (tiltMeasure P g t) := isProbabilityMeasure_tiltMeasure hg_meas hgM have hi : Integrable (observedArmIndicator d) (tiltMeasure P g t) := integrable_observedArmIndicator _ d have hYt : ∀ᵐ z ∂tiltMeasure P g t, |projY z| ≤ B := (ae_tiltMeasure_iff P g M t hg_meas hgM).2 hY have hyi : Integrable (fun z => projY z * observedArmIndicator d z) (tiltMeasure P g t) := by apply Integrable.of_bound ((measurable_snd.snd.mul (measurable_observedArmIndicator d)).aestronglyMeasurable) B filter_upwards [hYt] with z hYz change |projY z * observedArmIndicator d z| ≤ B rw [abs_mul] by_cases hz : projA z = d · simpa [observedArmIndicator, hz] using hYz · have hB : 0 ≤ B := (abs_nonneg (projY z)).trans hYz simpa [observedArmIndicator, hz] using hB have hi_bayes := condExp_tiltMeasure_ae_eq_div_exp P observedCovariateSigma_le g (observedArmIndicator d) M t hg_meas hgM hi have hyi_bayes := condExp_tiltMeasure_ae_eq_div_exp P observedCovariateSigma_le g (fun z => projY z * observedArmIndicator d z) M t hg_meas hgM hyi let u : γ × Bool × ℝ → ℝ := fun z => exp (t * g z) have hu_int : Integrable u P := tilt_exp_integrable hg_meas hgM have hlower : ∀ z, exp (-|t| * M) ≤ u z := exp_neg_abs_mul_le_exp_score g M t hgM have hce_lower : (fun _ => exp (-|t| * M)) ≤ᵐ[P] P[u | observedCovariateSigma] := by have hmono := condExp_mono (m := observedCovariateSigma) (integrable_const (exp (-|t| * M))) hu_int (Eventually.of_forall hlower) simpa [condExp_const observedCovariateSigma_le] using hmono filter_upwards [hi_bayes, hyi_bayes, hce_lower] with z hi_z hyi_z hlower_z change (tiltMeasure P g t)[fun w => projY w * observedArmIndicator d w | observedCovariateSigma] z / (tiltMeasure P g t)[observedArmIndicator d | observedCovariateSigma] z = _ rw [hi_z, hyi_z] change ((P[fun y => projY y * observedArmIndicator d y * u y | observedCovariateSigma] z / P[u | observedCovariateSigma] z) / (P[fun y => observedArmIndicator d y * u y | observedCovariateSigma] z / P[u | observedCovariateSigma] z)) = _ have hden : P[u | observedCovariateSigma] z ≠ 0 := ne_of_gt ((Real.exp_pos _).trans_le hlower_z) field_simp simp only [u] -
observedPropensity_tilt_pos_aetheorem — If the base arm propensity is positive and the tilt score is measurable and bounded, then the arm propensity recomputed under that exponential tilt remains positive.hypothesesγ :sharedType u_2P :g :γ × Bool × ℝ → ℝM t :ℝd :hg_meas :hgM :∀ z, |g z| ≤ Mhp :∀ᵐ z ∂P, 0 < observedPropensity P d zconclusion∀ᵐ z ∂P, 0 < observedPropensity (tiltMeasure P g t) d zProof (Lean source)
theorem observedPropensity_tilt_pos_ae (P : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure P] (g : γ × Bool × ℝ → ℝ) (M t : ℝ) (d : Bool) (hg_meas : Measurable g) (hgM : ∀ z, |g z| ≤ M) (hp : ∀ᵐ z ∂P, 0 < observedPropensity P d z) : ∀ᵐ z ∂P, 0 < observedPropensity (tiltMeasure P g t) d z := by let u : γ × Bool × ℝ → ℝ := fun z => exp (t * g z) let a := exp (-|t| * M) have ha : 0 < a := Real.exp_pos _ have hu : Integrable u P := tilt_exp_integrable hg_meas hgM have hI : Integrable (observedArmIndicator d) P := integrable_observedArmIndicator P d have hIu : Integrable (fun z => observedArmIndicator d z * u z) P := by apply hI.mul_bdd (by dsimp [u]; fun_prop) filter_upwards with z rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] exact Real.exp_le_exp.mpr ((le_abs_self _).trans (by rw [abs_mul] exact mul_le_mul_of_nonneg_left (hgM z) (abs_nonneg t))) have hden_lower : (fun _ => a) ≤ᵐ[P] P[u | observedCovariateSigma] := by have hmono := condExp_mono (m := observedCovariateSigma) (integrable_const a) hu (Eventually.of_forall fun z => by simpa [u, a] using exp_neg_abs_mul_le_exp_score g M t hgM z) simpa [condExp_const observedCovariateSigma_le] using hmono have hnum_lower : (fun z => a * observedPropensity P d z) ≤ᵐ[P] P[fun z => observedArmIndicator d z * u z | observedCovariateSigma] := by have hmono := condExp_mono (m := observedCovariateSigma) (hI.smul a) hIu (by filter_upwards with z simp only [Pi.smul_apply, smul_eq_mul] have hl := exp_neg_abs_mul_le_exp_score g M t hgM z have hInonneg : 0 ≤ observedArmIndicator d z := by by_cases hz : projA z = d <;> simp [observedArmIndicator, hz] simpa [u, a, mul_comm] using mul_le_mul_of_nonneg_left hl hInonneg) have hsmul := condExp_smul (μ := P) a (observedArmIndicator d) observedCovariateSigma filter_upwards [hmono, hsmul] with z hz hs simpa [observedPropensity, Pi.smul_apply, smul_eq_mul] using hs.symm.le.trans hz have hbayes := observedPropensity_tilt_ae_eq_expRatio P g M t d hg_meas hgM filter_upwards [hp, hden_lower, hnum_lower, hbayes] with z hpz hdenz hnumz hbayesz rw [hbayesz] exact div_pos ((mul_pos ha hpz).trans_le hnumz) (ha.trans_le hdenz) -
observedArmRegression_abs_lelemma — If the outcome bound is nonnegative, the outcome is bounded by B, and an arm propensity is positive, then the observed arm regression is bounded by B.hypothesesγ :sharedType u_2Q :d :B :ℝhB :0 ≤ BhY :∀ᵐ z ∂Q, |projY z| ≤ Bhp :∀ᵐ z ∂Q, 0 < observedPropensity Q d zconclusion∀ᵐ z ∂Q, |observedArmRegression Q d z| ≤ BProof (Lean source)
lemma observedArmRegression_abs_le (Q : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure Q] (d : Bool) (B : ℝ) (hB : 0 ≤ B) (hY : ∀ᵐ z ∂Q, |projY z| ≤ B) (hp : ∀ᵐ z ∂Q, 0 < observedPropensity Q d z) : ∀ᵐ z ∂Q, |observedArmRegression Q d z| ≤ B := by have hI : Integrable (observedArmIndicator d) Q := integrable_observedArmIndicator Q d have hYI : Integrable (fun z => projY z * observedArmIndicator d z) Q := by apply Integrable.of_bound ((measurable_snd.snd.mul (measurable_observedArmIndicator d)).aestronglyMeasurable) B filter_upwards [hY] with z hYz 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 ∂Q, |projY z * observedArmIndicator d z| ≤ B * observedArmIndicator d z := by filter_upwards [hY] with z hYz rw [abs_mul] by_cases hz : projA z = d · simpa [observedArmIndicator, hz] using hYz · simp [observedArmIndicator, hz] have hnum := abs_condExp_le_mul_condExp_of_abs_le (m := observedCovariateSigma) hYI hI hdom filter_upwards [hnum, hp] with z hnumz hpz change 0 < Q[observedArmIndicator d | observedCovariateSigma] z at hpz rw [observedArmRegression, observedArmNumerator, observedPropensity, abs_div, abs_of_pos hpz] exact (div_le_iff₀ hpz).2 hnumz -
integrable_observedArmRegression_of_boundedlemma — Under a nonnegative outcome bound, bounded outcomes, and a positive arm propensity, the corresponding observed arm regression is integrable.hypothesesγ :sharedType u_2Q :d :B :ℝhB :0 ≤ BhY :∀ᵐ z ∂Q, |projY z| ≤ Bhp :∀ᵐ z ∂Q, 0 < observedPropensity Q d zconclusionIntegrable (observedArmRegression Q d) QProof (Lean source)
lemma integrable_observedArmRegression_of_bounded (Q : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure Q] (d : Bool) (B : ℝ) (hB : 0 ≤ B) (hY : ∀ᵐ z ∂Q, |projY z| ≤ B) (hp : ∀ᵐ z ∂Q, 0 < observedPropensity Q d z) : Integrable (observedArmRegression Q d) Q := Integrable.of_bound (measurable_observedArmRegression Q d).aestronglyMeasurable B (by simpa [Real.norm_eq_abs] using observedArmRegression_abs_le Q d B hB hY hp)
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.
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
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
dml_ATE_tendstoNormal_hahnVariance_on_highProbEventtheorem — 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.hypothesesγ :sharedType u_1S :ε :ℝhA :S.toPOBackdoorSystem.Assumptionsh_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 samplec :ℝhc_pos :0 < cμ_hat :ℕ → P.Ω → (Bool → γ → ℝ)e_hat :ℕ → P.Ω → (γ → ℝ)goodSet :ℕ → Set P.ΩΔ :ℕ → ℝ≥0∞hfail :∀ n, P.μ (goodSet n)ᶜ ≤ Δ nh_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 nthen∀ a, MemLp (fun x => μ_hat n ω a x) 2 S.P_Xh_e_memLp :∀ n ωifω ∈ goodSet nthenMemLp (fun x => e_hat n ω x) 2 S.P_Xh_e_overlap :∀ n ωifω ∈ goodSet nthen∀ᵐ 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 :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.μconclusionModes.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 -
dml_ATE_tendstoNormal_hahnVariancetheorem — 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.hypothesesγ :sharedType u_1S :ε :ℝhA :S.toPOBackdoorSystem.Assumptionsh_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 samplec :ℝhc_pos :0 < 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_Xh_e_memLp :∀ n ω, MemLp (fun x => e_hat n ω x) 2 S.P_Xh_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 :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.μconclusionModes.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
ObservedLawExpansion 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.
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
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
integrable_observedArmIndicatorlemma — For a probability law Q and an arm d, the arm indicator is integrable.hypothesesconclusionProof (Lean source)
@[fun_prop] lemma integrable_observedArmIndicator (Q : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure Q] (d : Bool) : Integrable (observedArmIndicator d) Q := by apply Integrable.of_bound (measurable_observedArmIndicator d).aestronglyMeasurable 1 filter_upwards with z by_cases h : projA z = d <;> simp [observedArmIndicator, h] -
observedPropensity_mem_Icc_aelemma — For a probability law Q and an arm d, the recomputed arm propensity lies between zero and one almost everywhere.hypothesesconclusion∀ᵐ z ∂Q, 0 ≤ observedPropensity Q d z ∧ observedPropensity Q d z ≤ 1Proof (Lean source)
lemma observedPropensity_mem_Icc_ae (Q : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure Q] (d : Bool) : ∀ᵐ z ∂Q, 0 ≤ observedPropensity Q d z ∧ observedPropensity Q d z ≤ 1 := by have hnonneg : 0 ≤ᵐ[Q] observedPropensity Q d := condExp_nonneg (Eventually.of_forall fun z => by by_cases h : projA z = d <;> simp [observedArmIndicator, h]) have hmono : observedPropensity Q d ≤ᵐ[Q] (fun _ => (1 : ℝ)) := by have h := condExp_mono (m := observedCovariateSigma) (integrable_observedArmIndicator Q d) (integrable_const (1 : ℝ)) (Eventually.of_forall fun z => by by_cases hz : projA z = d <;> simp [observedArmIndicator, hz]) simpa [observedPropensity, condExp_const observedCovariateSigma_le (1 : ℝ)] using h exact hnonneg.and hmono -
integrable_observedPropensitylemma — For a probability law Q and an arm d, the recomputed arm propensity is integrable.hypothesesconclusionIntegrable (observedPropensity Q d) QProof (Lean source)
@[fun_prop] lemma integrable_observedPropensity (Q : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure Q] (d : Bool) : Integrable (observedPropensity Q d) Q := integrable_condExp -
integral_mul_eq_integral_mul_condExplemma — If the conditioning σ-algebra is contained in the ambient one, a weight h is measurable for that σ-algebra, bounded, and a target f is integrable, then integrating h f is unchanged by replacing f with its conditional expectation.hypothesesΩ :m :hm :m ≤ m₀h f :Ω → ℝhh :StronglyMeasurable[m] hC :ℝhh_bound :∀ᵐ z ∂Q, |h z| ≤ Chf :Integrable f Qconclusion∫ z, h z * f z ∂Q = ∫ z, h z * Q[f | m] z ∂QProof (Lean source)
lemma integral_mul_eq_integral_mul_condExp {Ω : Type*} {m₀ : MeasurableSpace Ω} {Q : Measure Ω} [IsFiniteMeasure Q] {m : MeasurableSpace Ω} (hm : m ≤ m₀) {h f : Ω → ℝ} (hh : StronglyMeasurable[m] h) (C : ℝ) (hh_bound : ∀ᵐ z ∂Q, |h z| ≤ C) (hf : Integrable f Q) : ∫ z, h z * f z ∂Q = ∫ z, h z * Q[f | m] z ∂Q := by have hh_norm : ∀ᵐ z ∂Q, ‖h z‖ ≤ C := by simpa [Real.norm_eq_abs] using hh_bound have hprod : Integrable (h * f) Q := hf.bdd_mul (hh.mono hm).aestronglyMeasurable hh_norm calc ∫ z, h z * f z ∂Q = ∫ z, Q[h * f | m] z ∂Q := (integral_condExp (μ := Q) (f := h * f) hm).symm _ = ∫ z, h z * Q[f | m] z ∂Q := integral_congr_ae (condExp_mul_of_stronglyMeasurable_left hh hprod hf) -
integral_weighted_observed_residuallemma — Let the evaluation law Q be a probability law, fix an arm d, and compare base-law nuisance functions from Q₀ with the nuisances recomputed under Q. If the outcome and the base-law arm regression are integrable, the inverse base propensity is bounded, and the evaluation-law arm propensity is positive, then the inverse-base-propensity residual integral equals the propensity ratio times the arm-regression change.hypothesesγ :sharedType u_1Q₀ Q :d :C :ℝhY :Integrable (projY : γ × Bool × ℝ → ℝ) Qhμ0 :Integrable (observedArmRegression Q₀ d) Qhinv :∀ᵐ z ∂Q, |(observedPropensity Q₀ d z)⁻¹| ≤ Chp :∀ᵐ z ∂Q, 0 < observedPropensity Q d zconclusion∫ z, observedArmIndicator d z / observedPropensity Q₀ d z * (projY z - observedArmRegression Q₀ d z) ∂Q= ∫ z, observedPropensity Q d z / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z) ∂QProof (Lean source)
lemma integral_weighted_observed_residual (Q₀ Q : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure Q] (d : Bool) (C : ℝ) (hY : Integrable (projY : γ × Bool × ℝ → ℝ) Q) (hμ0 : Integrable (observedArmRegression Q₀ d) Q) (hinv : ∀ᵐ z ∂Q, |(observedPropensity Q₀ d z)⁻¹| ≤ C) (hp : ∀ᵐ z ∂Q, 0 < observedPropensity Q d z) : ∫ z, observedArmIndicator d z / observedPropensity Q₀ d z * (projY z - observedArmRegression Q₀ d z) ∂Q = ∫ z, observedPropensity Q d z / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z) ∂Q := by let I : γ × Bool × ℝ → ℝ := observedArmIndicator d let p₀ : γ × Bool × ℝ → ℝ := observedPropensity Q₀ d let p : γ × Bool × ℝ → ℝ := observedPropensity Q d let μ₀ : γ × Bool × ℝ → ℝ := observedArmRegression Q₀ d let μ : γ × Bool × ℝ → ℝ := observedArmRegression Q d let Y : γ × Bool × ℝ → ℝ := projY have hI : Integrable I Q := integrable_observedArmIndicator Q d have hp_int : Integrable p Q := integrable_observedPropensity Q d have hIY : Integrable (fun z => I z * Y z) Q := by have hI_bound : ∀ᵐ z ∂Q, ‖I z‖ ≤ 1 := by filter_upwards with z by_cases hz : projA z = d <;> simp [I, observedArmIndicator, hz] exact hY.bdd_mul (measurable_observedArmIndicator d).aestronglyMeasurable hI_bound have hIμ₀ : Integrable (fun z => I z * μ₀ z) Q := by have hI_bound : ∀ᵐ z ∂Q, ‖I z‖ ≤ 1 := by filter_upwards with z by_cases hz : projA z = d <;> simp [I, observedArmIndicator, hz] exact hμ0.bdd_mul (measurable_observedArmIndicator d).aestronglyMeasurable hI_bound have hres : Integrable (fun z => I z * (Y z - μ₀ z)) Q := by refine (hIY.sub hIμ₀).congr ?_ filter_upwards with z simp only [Pi.sub_apply, mul_sub] have hinv_meas : StronglyMeasurable[observedCovariateSigma] (fun z => (p₀ z)⁻¹) := by dsimp [p₀] fun_prop have hpμ₀ : Integrable (fun z => p z * μ₀ z) Q := by have hp_bound : ∀ᵐ z ∂Q, ‖p z‖ ≤ 1 := by filter_upwards [observedPropensity_mem_Icc_ae Q d] with z hz simpa [p, Real.norm_eq_abs, abs_of_nonneg hz.1] using hz.2 exact hμ0.bdd_mul (measurable_observedPropensity Q d).aestronglyMeasurable hp_bound have hcond_sub : Q[fun z => I z * (Y z - μ₀ z) | observedCovariateSigma] =ᵐ[Q] fun z => observedArmNumerator Q d z - μ₀ z * p z := by have hsub := condExp_sub hIY hIμ₀ observedCovariateSigma have hpull := condExp_mul_of_stronglyMeasurable_right (stronglyMeasurable_observedArmRegression Q₀ d) hIμ₀ hI have hce : Q[fun z => I z * (Y z - μ₀ z) | observedCovariateSigma] =ᵐ[Q] Q[(fun z => I z * Y z) - (fun z => I z * μ₀ z) | observedCovariateSigma] := condExp_congr_ae (Eventually.of_forall fun z => by simp [mul_sub]) have hIYce : Q[fun z => I z * Y z | observedCovariateSigma] =ᵐ[Q] observedArmNumerator Q d := by apply condExp_congr_ae filter_upwards with z simp [I, Y, observedArmNumerator, mul_comm] filter_upwards [hce, hsub, hpull, hIYce] with z hcez hsubz hpullz hIYcez change Q[fun w => I w * μ₀ w | observedCovariateSigma] z = p z * μ₀ z at hpullz rw [hcez, hsubz] change Q[fun w => I w * Y w | observedCovariateSigma] z - Q[fun w => I w * μ₀ w | observedCovariateSigma] z = _ rw [hIYcez, hpullz] ring have hnum : ∀ᵐ z ∂Q, observedArmNumerator Q d z = p z * μ z := by filter_upwards [hp] with z hpz dsimp [μ, observedArmRegression, p] field_simp have hrewrite : Q[fun z => I z * (Y z - μ₀ z) | observedCovariateSigma] =ᵐ[Q] fun z => p z * (μ z - μ₀ z) := by filter_upwards [hcond_sub, hnum] with z hcond hnumz rw [hcond, hnumz] ring calc ∫ z, I z / p₀ z * (Y z - μ₀ z) ∂Q = ∫ z, (p₀ z)⁻¹ * (I z * (Y z - μ₀ z)) ∂Q := by apply integral_congr_ae filter_upwards with z ring _ = ∫ z, (p₀ z)⁻¹ * Q[fun w => I w * (Y w - μ₀ w) | observedCovariateSigma] z ∂Q := integral_mul_eq_integral_mul_condExp observedCovariateSigma_le hinv_meas C hinv hres _ = ∫ z, (p₀ z)⁻¹ * (p z * (μ z - μ₀ z)) ∂Q := integral_congr_ae ((EventuallyEq.rfl.mul hrewrite)) _ = ∫ z, p z / p₀ z * (μ z - μ₀ z) ∂Q := by apply integral_congr_ae filter_upwards with z ring -
observedArmMean_sub_integral_observedArmEIF_eq_producttheorem — Exact treatment-specific-mean expansion. Compare a base probability law Q₀ with an evaluation probability law Q for one treatment arm d. If the outcome and both arm regressions are integrable, the inverse base propensity is bounded, both relevant propensities are positive, and the residual and product terms are integrable, then the arm-mean change minus the evaluation-law mean of the base EIF is exactly minus the product of the propensity and outcome-regression errors.hypothesesγ :sharedType u_1Q₀ Q :d :C :ℝhY :Integrable (projY : γ × Bool × ℝ → ℝ) Qhμ0 :Integrable (observedArmRegression Q₀ d) Qhμ1 :Integrable (observedArmRegression Q d) Qhinv :∀ᵐ z ∂Q, |(observedPropensity Q₀ d z)⁻¹| ≤ Chp0 :∀ᵐ z ∂Q, 0 < observedPropensity Q₀ d zhp :∀ᵐ z ∂Q, 0 < observedPropensity Q d zhres :Integrable (fun z => observedArmIndicator d z / observedPropensity Q₀ d z * (projY z - observedArmRegression Q₀ d z)) Qhprod :Integrable (fun z => (observedPropensity Q d z - observedPropensity Q₀ d z) / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z)) Qconclusion= -(∫ z, (observedPropensity Q d z - observedPropensity Q₀ d z) / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z) ∂Q)Proof (Lean source)
theorem observedArmMean_sub_integral_observedArmEIF_eq_product (Q₀ Q : Measure (γ × Bool × ℝ)) [IsProbabilityMeasure Q] (d : Bool) (C : ℝ) (hY : Integrable (projY : γ × Bool × ℝ → ℝ) Q) (hμ0 : Integrable (observedArmRegression Q₀ d) Q) (hμ1 : Integrable (observedArmRegression Q d) Q) (hinv : ∀ᵐ z ∂Q, |(observedPropensity Q₀ d z)⁻¹| ≤ C) (hp0 : ∀ᵐ z ∂Q, 0 < observedPropensity Q₀ d z) (hp : ∀ᵐ z ∂Q, 0 < observedPropensity Q d z) (hres : Integrable (fun z => observedArmIndicator d z / observedPropensity Q₀ d z * (projY z - observedArmRegression Q₀ d z)) Q) (hprod : Integrable (fun z => (observedPropensity Q d z - observedPropensity Q₀ d z) / observedPropensity Q₀ d z * (observedArmRegression Q d z - observedArmRegression Q₀ d z)) Q) : observedArmMean Q d - observedArmMean Q₀ d - ∫ z, observedArmEIF 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 have hr := integral_weighted_observed_residual Q₀ Q d C hY hμ0 hinv hp have hratio : ∫ 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] with z hz field_simp ring _ = _ := integral_add (hμ1.sub hμ0) hprod have hconst : Integrable (fun _ : γ × Bool × ℝ => observedArmMean Q₀ d) Q := integrable_const _ unfold observedArmMean observedArmEIF integral_linearity rw [integral_const, probReal_univ, one_smul, hr, hratio, integral_sub hμ1 hμ0] rw [show observedArmMean Q₀ d = ∫ z, observedArmRegression Q₀ d z ∂Q₀ from rfl] ring
VonMises 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.
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.