Estimation.Orthogonal­Moments

Neyman-orthogonal moment functions: construction, cross-fitting, parametric examples, and automatic debiasing.

Auto­Debias 22 core · 6 supporting · 3 submodules Automatic debiasing: Riesz-representer-based construction of orthogonal moments for linear functionals.
Moment­Functional 6 core · 0 supporting This file defines the moment-functional interface used by the double machine learning layer. ★ J₀_mul_J₀_inv

Abstract Moment Functionals

This file defines the moment-functional interface used by the double machine learning layer. The interface records the observed-data moment, the true nuisance and scalar target, the local perturbation set, bilinear seminorms for product-rate bounds, and the nonzero Jacobian of the population moment. Concrete double-machine-learning instances reduce to filling this interface, which centralizes the generic asymptotic-linearity machinery.

structure GeneralMoment reviewed
Causalean.Estimation.OrthogonalMoments

A general moment bundles a score function of a nuisance, an observation, and a scalar parameter, a truth nuisance η₀ and truth parameter θ₀, a set of admissible nuisance perturbations, and a pair of bilinear seminorms used to bound product-rate remainders, subject to: the score is jointly measurable in the observation for every nuisance and parameter value, the truth nuisance belongs to the perturbation set, and the population moment's parameter-derivative at the truth (its Jacobian) is nonzero, so that its inverse is well-defined.

Definition (Lean source)
parameters
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
Z :
Type*
MeasurableSpace Z
P_Z :
Measure Z
H :
Type*
AddCommGroup H
Module ℝ H
fields
m :
H → Z → ℝ → ℝ
η₀ :
H
θ₀ :
ℝ
H_ε :
Set H
ρ₁ :
H → H → NNReal
ρ₂ :
H → H → NNReal
m_meas :
∀ η θ, Measurable (fun z => m η z θ)
η₀_mem :
η₀ ∈ H_ε
J₀ :
ℝ
J₀_ne_zero :
J₀ ≠ 0
Causalean.Estimation.OrthogonalMoments.GeneralMoment · Causalean/Estimation/OrthogonalMoments/MomentFunctional.lean:36
def J₀_inv reviewed
Causalean.Estimation.OrthogonalMoments.GeneralMoment

For a general moment system, the inverse population Jacobian is the reciprocal of the system's nonzero population Jacobian.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
def
J₀_inv M :
ℝ
given by
M.J₀⁻¹
Causalean.Estimation.OrthogonalMoments.GeneralMoment.J₀_inv · Causalean/Estimation/OrthogonalMoments/MomentFunctional.lean:83 · uses GeneralMoment
lemma J₀_mul_J₀_inv reviewed
Causalean.Estimation.OrthogonalMoments.GeneralMoment

Jacobian times its inverse is one. For a general orthogonal-moment system, the population Jacobian times its inverse equals one.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
conclusion
M.J₀ * M.J₀_inv = 1
Proof (Lean source)
@[simp] lemma J₀_mul_J₀_inv (M : GeneralMoment Ω μ Z P_Z H) : M.J₀ * M.J₀_inv = 1 := by unfold J₀_inv exact mul_inv_cancel₀ M.J₀_ne_zero
Causalean.Estimation.OrthogonalMoments.GeneralMoment.J₀_mul_J₀_inv · Causalean/Estimation/OrthogonalMoments/MomentFunctional.lean:90 · uses GeneralMoment , J₀_inv
def MeanZero reviewed
Causalean.Estimation.OrthogonalMoments

For a general moment system, the mean-zero condition states that the population expectation of its score at the true nuisance and true scalar target is zero.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
def
MeanZero M :
Prop
given by
∫ z, M.m M.η₀ z M.θ₀ ∂P_Z = 0
Causalean.Estimation.OrthogonalMoments.MeanZero · Causalean/Estimation/OrthogonalMoments/MomentFunctional.lean:103 · uses GeneralMoment
def H_ε_PerturbClosed reviewed
Causalean.Estimation.OrthogonalMoments

For a general moment system, perturbation-set segment closure states that, for every nuisance value in its admissible perturbation set and every weight in the closed unit interval, the corresponding point on the line segment from the true nuisance to that value also belongs to the admissible set.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
η ∈ M.H_ε :
t ∈ Set.Icc (0 : ℝ) 1 :
def
H_ε_PerturbClosed M :
Prop
given by
M.η₀ + t • (η - M.η₀) ∈ M.H_ε
Causalean.Estimation.OrthogonalMoments.H_ε_PerturbClosed · Causalean/Estimation/OrthogonalMoments/MomentFunctional.lean:109 · uses GeneralMoment
structure LinearMoment reviewed
Causalean.Estimation.OrthogonalMoments

A linear moment is a general moment whose score is affine in the scalar target parameter.

Definition (Lean source)
parameters
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
Z :
Type*
MeasurableSpace Z
P_Z :
Measure Z
H :
Type*
AddCommGroup H
Module ℝ H
extends :
GeneralMoment Ω μ Z P_Z H
fields
m_a :
H → Z → ℝ
m_b :
H → Z → ℝ
m_a_meas :
∀ η, Measurable (m_a η)
m_b_meas :
∀ η, Measurable (m_b η)
m_decomp :
∀ η z θ, m η z θ = m_a η z * θ + m_b η z
Jacobian field is consistent with the linear decomposition: `J₀ = ∫ m_a(η₀, z) dP_Z`.
J₀_eq :
J₀ = ∫ z, m_a η₀ z ∂P_Z
Causalean.Estimation.OrthogonalMoments.LinearMoment · Causalean/Estimation/OrthogonalMoments/MomentFunctional.lean:116
Directional­Deriv 1 core · 0 supporting This file packages the pointwise nuisance directional derivative data required by the abstract double machine learning framework.

Directional Derivatives for Abstract Moments

This file packages the pointwise nuisance directional derivative data required by the abstract double machine learning framework. The data include convergence of difference quotients along nuisance line segments and measurability of the derivative functions.

structure HasDirDeriv reviewed
Causalean.Estimation.OrthogonalMoments

For a general moment, a candidate pointwise directional-derivative function dM of the score along the line segment from the truth to a perturbed nuisance, evaluated at each observation, together with the witnesses that for every perturbation in the admissible set and every observation, the score's difference quotient along that segment tends to dM's value there as the step size shrinks to zero, and that dM at each perturbation is measurable in the observation.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
μ :
Measure Ω
shared
Z :
Type u_2
shared
P_Z :
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
fields
dM :
H → Z → ℝ
pointwise_tendsto :
∀ η ∈ M.H_ε,
∀ z,
Tendsto (fun t : ℝ => (M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ - M.m M.η₀ z M.θ₀) / t) (𝓝[≠] 0) (𝓝 (dM η z))
dM_meas :
∀ η, Measurable (dM η)
Causalean.Estimation.OrthogonalMoments.HasDirDeriv · Causalean/Estimation/OrthogonalMoments/DirectionalDeriv.lean:35 · uses GeneralMoment
DMLChernozhukov 2 core · 0 supporting This file proves the abstract one-shot double machine learning theorem in the classical Chernozhukov form. ★ dml_chernozhukov_asymptoticLinear

Chernozhukov-Form Double Machine Learning

This file proves the abstract one-shot double machine learning theorem in the classical Chernozhukov form. The estimator evaluates the moment at the true target, rescales by the inverse Jacobian, and yields asymptotic linearity with the corresponding influence function.

def dmlChernozhukovEstimator reviewed
Causalean.Estimation.OrthogonalMoments

For a measurable population space with a population measure, a measurable observed-data space with its observed-data law, and a real vector space of nuisance values, a general moment system, an independent and identically distributed sample, a one-shot evaluation-fold split of that sample, a sequence of nuisance estimators, and a sample-size index, the Chernozhukov one-step double-machine-learning estimator maps each population state to the true target minus the inverse Jacobian times the evaluation-fold empirical mean of the moment evaluated at that target and at the estimated nuisance.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
sample :
IIDSample Ω Z μ P_Z
split :
OneShotSplit sample
η_hat :
ℕ → Ω → H
n :
ℕ
def
dmlChernozhukovEstimator M sample split η_hat n :
Ω → ℝ
given by
fun ω
=> M.θ₀
- M.J₀_inv * (((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m (η_hat n ω) (sample.Z i ω) M.θ₀)
Causalean.Estimation.OrthogonalMoments.dmlChernozhukovEstimator · Causalean/Estimation/OrthogonalMoments/DMLChernozhukov.lean:57 · uses GeneralMoment , IIDSample , OneShotSplit
theorem dml_chernozhukov_asymptoticLinear reviewed
Causalean.Estimation.OrthogonalMoments

Asymptotic linearity of the Chernozhukov DML estimator. Drops the zero-centering hypothesis hθ_zero from dml_asymptoticLinear. Given a general moment M with mean zero at the truth, assume the truth-evaluated score is square-integrable (finite variance). Given an i.i.d. sample with a one-shot fold split whose fold-B fraction converges to a strictly positive limit c > 0 along card (foldB n) / n → c, and a sequence of cross-fitted nuisance estimators η̂, suppose the population moment at η̂ is bounded by a constant times the product of the two bilinear-remainder seminorms, at every fold and sample point. Assume the technical regularity package that the moment at η̂ is jointly measurable, fold-A-measurable in ω, and, at every fold and sample point, integrable and square-integrable. Finally suppose the L² score difference between the estimated and true nuisance is o_P(1), and the product of the two nuisance-error rates decays at the parametric rate o_P(n^{-1/2}). Then the Chernozhukov one-step estimator is asymptotically linear at the truth M.θ₀, with influence function −J₀⁻¹ · m(η₀, ·, θ₀) and asymptotic variance J₀⁻¹ Σ J₀⁻ᵀ where Σ := ∫ m(η₀, z, θ₀)² dP_Z, indexed over split.foldB.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
StandardBorelSpace Ω
IsFiniteMeasure μ
IsProbabilityMeasure μ
M :
GeneralMoment Ω μ Z P_Z H
_hMZ :
MeanZero M
_hFV :
Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z
sample :
IIDSample Ω Z μ P_Z
split :
OneShotSplit sample
c :
ℝ
_hc_pos :
0 < c
_h_split_rate :
Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)
η_hat :
ℕ → Ω → H
Crem :
ℝ
_hBR_at :
∀ n ω,
|∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z|
≤ Crem * ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ)
_h_m_meas :
∀ n, Measurable (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 M.θ₀)
_h_m_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n ω) z M.θ₀)
_h_m_foldA_uncurry :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 M.θ₀)
_h_m_int :
∀ n ω, Integrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Z
_h_m_sq_int :
∀ n ω, Integrable (fun z => (M.m (η_hat n ω) z M.θ₀) ^ 2) P_Z
_h_score_diff_rate :
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
_h_product_rate :
IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ
conclusion
IsAsymLinear (dmlChernozhukovEstimator M sample split η_hat) M.θ₀ (fun z => -M.J₀_inv * M.m M.η₀ z M.θ₀) sample split.foldB
Proof (Lean source)
theorem dml_chernozhukov_asymptoticLinear [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : GeneralMoment Ω μ Z P_Z H) (_hMZ : MeanZero M) (_hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample) {c : ℝ} (_hc_pos : 0 < c) (_h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_hat : ℕ → Ω → H) {Crem : ℝ} (_hBR_at : ∀ n ω, |∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z| ≤ Crem * ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ)) (_h_m_meas : ∀ n, Measurable (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 M.θ₀)) (_h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n ω) z M.θ₀)) (_h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 M.θ₀)) (_h_m_int : ∀ n ω, Integrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Z) (_h_m_sq_int : ∀ n ω, Integrable (fun z => (M.m (η_hat n ω) z M.θ₀) ^ 2) P_Z) (_h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (_h_product_rate : IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) : IsAsymLinear (dmlChernozhukovEstimator M sample split η_hat) M.θ₀ (fun z => -M.J₀_inv * M.m M.η₀ z M.θ₀) sample split.foldB := by refine ⟨?_, ?_, ?_⟩ · -- mean_zero rw [integral_const_mul] rw [show (∫ a, M.m M.η₀ a M.θ₀ ∂P_Z) = 0 by simpa [MeanZero] using _hMZ] ring · -- finite_var simpa [mul_pow, mul_assoc, mul_left_comm, mul_comm] using (_hFV.const_mul (M.J₀_inv ^ 2)) · -- remainder: centered fold-B fluctuation plus population remainder. let f : ℕ → Ω → Z → ℝ := fun n ω z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀ let G : ℕ → Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (f n ω (sample.Z i ω) - ∫ z, f n ω z ∂P_Z) let B : ℕ → Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * ∫ z, f n ω z ∂P_Z let R : ℕ → Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * (dmlChernozhukovEstimator M sample split η_hat n ω - M.θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (-M.J₀_inv * M.m M.η₀ (sample.Z i ω) M.θ₀) haveI : IsProbabilityMeasure P_Z := by rw [← sample.law] exact Measure.isProbabilityMeasure_map (sample.meas 0).aemeasurable have htruth_L2 : MemLp (fun z => M.m M.η₀ z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas M.η₀ M.θ₀).aestronglyMeasurable).2 _hFV have hf_meas : ∀ n, Measurable (uncurry (f n)) := by intro n change Measurable (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (_h_m_meas n).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω => f n ω) := by intro n change Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) exact (_h_m_foldA n).sub measurable_const have hf_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (f n)) := by intro n change Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (_h_m_foldA_uncurry n).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_memLp : ∀ n ω, MemLp (f n ω) 2 P_Z := by intro n ω have hrand_L2 : MemLp (fun z => M.m (η_hat n ω) z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas (η_hat n ω) M.θ₀).aestronglyMeasurable).2 (_h_m_sq_int n ω) exact hrand_L2.sub htruth_L2 have hf_rate_one : IsLittleOp (fun n ω => (eLpNorm (f n ω) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ := by simpa [f] using _h_score_diff_rate have hG : IsLittleOp G (fun _ => (1 : ℝ)) μ := by simpa [G] using foldB_centered_sum_isLittleOp_one sample split f hf_meas hf_uncurry_foldA hf_memLp hf_rate_one have h_int_eq : ∀ n ω, ∫ z, f n ω z ∂P_Z = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z := by intro n ω have hf_int : Integrable (f n ω) P_Z := (hf_memLp n ω).integrable (by norm_num : (1 : ENNReal) ≤ 2) have htruth_int : Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z := htruth_L2.integrable (by norm_num : (1 : ENNReal) ≤ 2) have hzero : (∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) = 0 := by simpa [MeanZero] using _hMZ calc ∫ z, f n ω z ∂P_Z = ∫ z, (M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) ∂P_Z := by rfl _ = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z := integral_sub (_h_m_int n ω) htruth_int _ = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z := by rw [hzero] ring have h_int_raw_rate : IsLittleOp (fun n ω => ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ let K : ℝ := |Crem| + 1 have hKpos : 0 < K := by dsimp [K] linarith [abs_nonneg Crem] have htarget := (ENNReal.tendsto_nhds_zero.mp (_h_product_rate (ε / K) (div_pos hε hKpos))) δ hδ exact htarget.mono fun n hn => (measure_mono (by intro ω hω let prodρ : ℝ := ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ) have hprod_nonneg : 0 ≤ prodρ := by dsimp [prodρ] exact mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _) have hbr := _hBR_at n ω have hbr0 : |∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z| ≤ Crem * prodρ := by simpa [prodρ, mul_assoc] using hbr have hle_abs : |∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z| ≤ |Crem| * prodρ := hbr0.trans (mul_le_mul_of_nonneg_right (le_abs_self Crem) hprod_nonneg) have hKbound : |∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z| ≤ K * prodρ := by refine hle_abs.trans ?_ exact mul_le_mul_of_nonneg_right (by dsimp [K]; linarith) hprod_nonneg have hlt_bound : ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) < K * prodρ := lt_of_lt_of_le hω hKbound have hdiv_lt : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / K < prodρ := by rw [div_lt_iff₀ hKpos] simpa [mul_comm, mul_left_comm, mul_assoc] using hlt_bound have hsmall : (ε / K) * ((n : ℝ) ^ (-(1 / 2 : ℝ))) < |prodρ| := by have hdiv_eq : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / K = (ε / K) * ((n : ℝ) ^ (-(1 / 2 : ℝ))) := by ring rw [← hdiv_eq] simpa [abs_of_nonneg hprod_nonneg] using hdiv_lt exact hsmall)).trans hn have h_int_rate : IsLittleOp (fun n ω => ∫ z, f n ω z ∂P_Z) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by convert h_int_raw_rate using 1 funext n ω exact h_int_eq n ω have hB : IsLittleOp B (fun _ => (1 : ℝ)) μ := by intro ε' hε' rw [ENNReal.tendsto_nhds_zero] intro δ hδ let C : ℝ := sqrt c + 1 have hCpos : 0 < C := by dsimp [C] linarith [Real.sqrt_nonneg c] have hCnonneg : 0 ≤ C := le_of_lt hCpos have hC2 : c < C ^ 2 := by dsimp [C] nlinarith [Real.sq_sqrt (le_of_lt _hc_pos), Real.sqrt_nonneg c] have hratio_event : ∀ᶠ n in atTop, ((split.foldB n).card : ℝ) / n < C ^ 2 := by exact _h_split_rate.eventually_lt_const hC2 have hn_event : ∀ᶠ n : ℕ in atTop, n ≠ 0 := by exact eventually_ne_atTop 0 have hint_event := (ENNReal.tendsto_nhds_zero.mp (h_int_rate (ε' / C) (div_pos hε' hCpos))) δ hδ -- … truncated; follow the source link for the rest …
Causalean.Estimation.OrthogonalMoments.dml_chernozhukov_asymptoticLinear · Causalean/Estimation/OrthogonalMoments/DMLChernozhukov.lean:83 · uses GeneralMoment , J₀_inv , MeanZero , dmlChernozhukovEstimator , IIDSample , IsAsymLinear , IsLittleOp , OneShotSplit , foldA , foldB
Neyman­Orthogonal 3 core · 0 supporting This file defines Neyman orthogonality for a moment functional through the vanishing population integral of its nuisance directional derivative. ★ integratedMoment_diffQuotient_tendsto_zero

Neyman Orthogonality for Abstract Moments

This file defines Neyman orthogonality for a moment functional through the vanishing population integral of its nuisance directional derivative. It also records the dominated-convergence envelope needed to pass pointwise directional derivatives through integration.

def NeymanOrthogonal reviewed
Causalean.Estimation.OrthogonalMoments

Given a general moment system equipped with a directional derivative of that moment, Neyman orthogonality means that, for every nuisance value in its admissible perturbation set, the population integral of the directional derivative is zero.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
D :
HasDirDeriv M
η ∈ M.H_ε :
def
NeymanOrthogonal M D :
Prop
given by
∫ z, D.dM η z ∂P_Z = 0
Causalean.Estimation.OrthogonalMoments.NeymanOrthogonal · Causalean/Estimation/OrthogonalMoments/NeymanOrthogonal.lean:38 · uses GeneralMoment , HasDirDeriv
def DiffQuotientEnvelope reviewed
Causalean.Estimation.OrthogonalMoments

For a general moment system, the difference-quotient envelope condition requires that, for every admissible nuisance value, there is a positive radius and an integrable envelope function such that, almost everywhere under the data distribution, every nonzero displacement within that radius has its moment difference quotient along the line from the true nuisance to that value bounded in norm by the envelope.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
η ∈ M.H_ε :
def
DiffQuotientEnvelope M :
Prop
given by
∃ δ : ℝ,
0 < δ
clause 1
∃ g : Z → ℝ,
Integrable g P_Z
∀ᵐ z ∂P_Z, ∀ t : ℝ, t ∈ Ioo (-δ) δ → t
≠ 0 → ‖(M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ - M.m M.η₀ z M.θ₀) / t‖ ≤ g z
Causalean.Estimation.OrthogonalMoments.DiffQuotientEnvelope · Causalean/Estimation/OrthogonalMoments/NeymanOrthogonal.lean:46 · uses GeneralMoment
theorem integratedMoment_diffQuotient_tendsto_zero reviewed
Causalean.Estimation.OrthogonalMoments

Abstract DCT bridge. Given a general moment M with directional-derivative structure D, assume Neyman orthogonality — the population directional derivative vanishes at every admissible nuisance perturbation, and an L¹(P_Z) envelope dominating the difference quotient of the moment near t = 0. Suppose η lies in the admissible nuisance neighborhood M.H_ε, that the moment along the segment from η₀ to η is integrable at every nonzero t, and that the moment at η₀ is integrable. Then the integrated difference quotient (∫ m(η₀ + t · (η − η₀)) dP_Z − ∫ m(η₀) dP_Z) / t tends to zero as t → 0 along the punctured neighborhood.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
D :
HasDirDeriv M
hNO :
NeymanOrthogonal M D
hEnv :
DiffQuotientEnvelope M
η :
H
hη :
η ∈ M.H_ε
hMt_int :
∀ t ≠ (0 : ℝ), Integrable (fun z => M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀) P_Z
hM0_int :
Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z
conclusion
Tendsto (fun t : ℝ => (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t) (𝓝[≠] 0) (𝓝 0)
Proof (Lean source)
theorem integratedMoment_diffQuotient_tendsto_zero (M : GeneralMoment Ω μ Z P_Z H) (D : HasDirDeriv M) (hNO : NeymanOrthogonal M D) (hEnv : DiffQuotientEnvelope M) {η : H} (hη : η ∈ M.H_ε) (hMt_int : ∀ t ≠ (0 : ℝ), Integrable (fun z => M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀) P_Z) (hM0_int : Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z) : Tendsto (fun t : ℝ => (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t) (𝓝[≠] 0) (𝓝 0) := by rcases hEnv η hη with ⟨δ, hδ_pos, g, hg_int, hg_bound⟩ let F : ℝ → Z → ℝ := fun t z => (M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ - M.m M.η₀ z M.θ₀) / t have hIoo : Ioo (-δ) δ ∈ 𝓝[≠] (0 : ℝ) := by have hIoo_nhds : Ioo (-δ) δ ∈ 𝓝 (0 : ℝ) := by exact Ioo_mem_nhds (by linarith) hδ_pos exact nhdsWithin_le_nhds hIoo_nhds have h_ne : {t : ℝ | t ≠ 0} ∈ 𝓝[≠] (0 : ℝ) := self_mem_nhdsWithin have hlim_integral : Tendsto (fun t : ℝ => ∫ z, F t z ∂P_Z) (𝓝[≠] 0) (𝓝 (∫ z, D.dM η z ∂P_Z)) := by apply MeasureTheory.tendsto_integral_filter_of_dominated_convergence g · exact Filter.Eventually.of_forall (fun t => (((M.m_meas (M.η₀ + t • (η - M.η₀)) M.θ₀).sub (M.m_meas M.η₀ M.θ₀)).div_const t).aestronglyMeasurable) · filter_upwards [hIoo, h_ne] with t htIoo ht_ne exact hg_bound.mono (fun z hz => by simpa [F] using hz t htIoo ht_ne) · exact hg_int · exact Filter.Eventually.of_forall (fun z => by simpa [F] using D.pointwise_tendsto η hη z) have h_eq : (fun t : ℝ => ∫ z, F t z ∂P_Z) =ᶠ[𝓝[≠] (0 : ℝ)] (fun t : ℝ => (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t) := by filter_upwards [h_ne] with t ht_ne calc ∫ z, F t z ∂P_Z = (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ - M.m M.η₀ z M.θ₀ ∂P_Z) / t := by simp [F, MeasureTheory.integral_div] _ = (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t := by rw [MeasureTheory.integral_sub (hMt_int t ht_ne) hM0_int] have hlim_to_deriv : Tendsto (fun t : ℝ => (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t) (𝓝[≠] 0) (𝓝 (∫ z, D.dM η z ∂P_Z)) := hlim_integral.congr' h_eq simpa [NeymanOrthogonal, hNO η hη] using hlim_to_deriv
Causalean.Estimation.OrthogonalMoments.integratedMoment_diffQuotient_tendsto_zero · Causalean/Estimation/OrthogonalMoments/NeymanOrthogonal.lean:58 · uses DiffQuotientEnvelope , GeneralMoment , HasDirDeriv , NeymanOrthogonal
Remainder­Bound 2 core · 0 supporting This file formalizes the product-rate remainder condition for abstract orthogonal moments. ★ bilinear_remainder_of_smoothness

Bilinear Remainder Bounds

This file formalizes the product-rate remainder condition for abstract orthogonal moments. It also gives a smoothness bridge showing that Neyman orthogonality plus a uniform second-order envelope implies such a bilinear population bias bound.

def BilinearRemainder reviewed
Causalean.Estimation.OrthogonalMoments

For a general moment system and a real constant, the bilinear-remainder condition requires that, for every nuisance value in the system's admissible perturbation set, the absolute population moment at the true scalar target is at most CC times the product of its two seminorm distances from the true nuisance.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
C :
ℝ
η ∈ M.H_ε :
def
BilinearRemainder M C :
Prop
given by
|∫ z, M.m η z M.θ₀ ∂P_Z| ≤ C * ((M.ρ₁ η M.η₀ : ℝ)) * ((M.ρ₂ η M.η₀ : ℝ))
Causalean.Estimation.OrthogonalMoments.BilinearRemainder · Causalean/Estimation/OrthogonalMoments/RemainderBound.lean:36 · uses GeneralMoment
theorem bilinear_remainder_of_smoothness reviewed
Causalean.Estimation.OrthogonalMoments

Smoothness bridge to a bilinear remainder bound. For a general moment M with directional derivative D satisfying Neyman orthogonality, given an envelope g that is P_Z-integrable, suppose the linearization residual obeys a uniform second-order envelope with constant K: for every perturbation η in the nuisance neighborhood, |m(η,·,θ₀) − m(η₀,·,θ₀) − dM(η,·)| ≤ K·ρ₁(η,η₀)·ρ₂(η,η₀)·g almost everywhere, with the directional derivative integrable at every such η, the moment integrable at the baseline η₀, the moment integrable at every perturbed η, and the moment having population mean zero. Then some constant C makes the population moment obey the bilinear remainder bound C·ρ₁(η,η₀)·ρ₂(η,η₀) uniformly over the nuisance neighborhood.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
D :
HasDirDeriv M
hNO :
NeymanOrthogonal M D
K :
ℝ
g :
Z → ℝ
hg_int :
Integrable g P_Z
hSecond :
∀ η ∈ M.H_ε,
∀ᵐ z ∂P_Z, |M.m η z M.θ₀ - M.m M.η₀ z M.θ₀ - D.dM η z|
≤ K * ((M.ρ₁ η M.η₀ : ℝ)) * ((M.ρ₂ η M.η₀ : ℝ)) * g z
hdM_int :
∀ η ∈ M.H_ε, Integrable (fun z => D.dM η z) P_Z
hM0_int :
Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z
hMη_int :
∀ η ∈ M.H_ε, Integrable (fun z => M.m η z M.θ₀) P_Z
hMZ :
MeanZero M
conclusion
∃ C, BilinearRemainder M C
Proof (Lean source)
theorem bilinear_remainder_of_smoothness (M : GeneralMoment Ω μ Z P_Z H) (D : HasDirDeriv M) (hNO : NeymanOrthogonal M D) {K : ℝ} {g : Z → ℝ} (hg_int : Integrable g P_Z) (hSecond : ∀ η ∈ M.H_ε, ∀ᵐ z ∂P_Z, |M.m η z M.θ₀ - M.m M.η₀ z M.θ₀ - D.dM η z| ≤ K * ((M.ρ₁ η M.η₀ : ℝ)) * ((M.ρ₂ η M.η₀ : ℝ)) * g z) (hdM_int : ∀ η ∈ M.H_ε, Integrable (fun z => D.dM η z) P_Z) (hM0_int : Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z) (hMη_int : ∀ η ∈ M.H_ε, Integrable (fun z => M.m η z M.θ₀) P_Z) (hMZ : MeanZero M) : ∃ C, BilinearRemainder M C := by refine ⟨|K| * ∫ z, |g z| ∂P_Z, ?_⟩ intro η hη let r₁ : ℝ := M.ρ₁ η M.η₀ let r₂ : ℝ := M.ρ₂ η M.η₀ let rem : Z → ℝ := fun z => M.m η z M.θ₀ - M.m M.η₀ z M.θ₀ - D.dM η z have hr₁_nonneg : 0 ≤ r₁ := by dsimp [r₁] exact NNReal.coe_nonneg _ have hr₂_nonneg : 0 ≤ r₂ := by dsimp [r₂] exact NNReal.coe_nonneg _ have hrem_int : Integrable rem P_Z := by dsimp [rem] exact ((hMη_int η hη).sub hM0_int).sub (hdM_int η hη) have hrem_abs_int : Integrable (fun z => |rem z|) P_Z := by simpa [Real.norm_eq_abs] using hrem_int.norm have hbound_int : Integrable (fun z => |K| * r₁ * r₂ * |g z|) P_Z := by simpa [Real.norm_eq_abs, mul_assoc] using (hg_int.norm.const_mul (|K| * r₁ * r₂)) have hpoint : ∀ᵐ z ∂P_Z, |rem z| ≤ |K| * r₁ * r₂ * |g z| := by filter_upwards [hSecond η hη] with z hz dsimp [rem, r₁, r₂] at hz ⊢ refine hz.trans ?_ calc K * (M.ρ₁ η M.η₀ : ℝ) * (M.ρ₂ η M.η₀ : ℝ) * g z ≤ |K * (M.ρ₁ η M.η₀ : ℝ) * (M.ρ₂ η M.η₀ : ℝ) * g z| := le_abs_self _ _ = |K| * (M.ρ₁ η M.η₀ : ℝ) * (M.ρ₂ η M.η₀ : ℝ) * |g z| := by rw [abs_mul, abs_mul, abs_mul] simp [abs_of_nonneg (NNReal.coe_nonneg (M.ρ₁ η M.η₀)), abs_of_nonneg (NNReal.coe_nonneg (M.ρ₂ η M.η₀)), mul_assoc] have hrem_integral : ∫ z, rem z ∂P_Z = ∫ z, M.m η z M.θ₀ ∂P_Z := by have hdiff_int : Integrable (fun z => M.m η z M.θ₀ - M.m M.η₀ z M.θ₀) P_Z := by exact (hMη_int η hη).sub hM0_int dsimp [rem] change ∫ z, ((fun z : Z => M.m η z M.θ₀ - M.m M.η₀ z M.θ₀) z - (fun z : Z => D.dM η z) z) ∂P_Z = ∫ z, M.m η z M.θ₀ ∂P_Z rw [integral_sub hdiff_int (hdM_int η hη)] rw [integral_sub (hMη_int η hη) hM0_int] rw [hMZ, hNO η hη] ring calc |∫ z, M.m η z M.θ₀ ∂P_Z| = |∫ z, rem z ∂P_Z| := by rw [hrem_integral] _ ≤ ∫ z, |rem z| ∂P_Z := MeasureTheory.abs_integral_le_integral_abs _ ≤ ∫ z, |K| * r₁ * r₂ * |g z| ∂P_Z := integral_mono_ae hrem_abs_int hbound_int hpoint _ = |K| * r₁ * r₂ * (∫ z, |g z| ∂P_Z) := by rw [integral_const_mul] _ = (|K| * ∫ z, |g z| ∂P_Z) * r₁ * r₂ := by ring
Causalean.Estimation.OrthogonalMoments.bilinear_remainder_of_smoothness · Causalean/Estimation/OrthogonalMoments/RemainderBound.lean:46 · uses BilinearRemainder , GeneralMoment , HasDirDeriv , MeanZero , NeymanOrthogonal
Riesz 3 core · 1 supporting This file provides the Riesz-representation pattern for linear-in-regression causal functionals. ★ rieszScore_meanZero

Riesz Scores for Orthogonal Moments

This file provides the Riesz-representation pattern for linear-in-regression causal functionals. It defines the representer, the corresponding orthogonal score, and the mean-zero and bilinear-remainder identities used by automatic debiasing and double machine learning.

structure RieszRepresentation reviewed
Causalean.Estimation.OrthogonalMoments

A Riesz representation for a continuous linear functional on a regression class under a covariate measure: a function α₀ on the covariate space that is measurable, integrable against the covariate measure, and that represents the functional's value at every element of the regression class as the covariate-measure integral of α₀ against that element's evaluation.

Definition (Lean source)
parameters
H_γ :
Type*
AddCommGroup H_γ
Module ℝ H_γ
γ_target :
H_γ → X → ℝ
L :
H_γ → ℝ
P_X :
Measure X
fields
α₀ :
X → ℝ
α₀_meas :
Measurable α₀
α₀_integrable :
Integrable α₀ P_X
representation :
∀ γ : H_γ, L γ = ∫ x, α₀ x * γ_target γ x ∂P_X
Causalean.Estimation.OrthogonalMoments.RieszRepresentation · Causalean/Estimation/OrthogonalMoments/Riesz.lean:48
def rieszScore reviewed
Causalean.Estimation.OrthogonalMoments

For an observed-data space and a covariate space, a regression-function vector space, a map assigning each regression function its value at every covariate, a real-valued linear functional of that regression function, an observed-data-to-covariate map, an observed outcome map, a regression function, a Riesz representer, a scalar target, and an observed-data realization, the generic Riesz orthogonal score is the functional evaluated at the regression function plus the representer times its observed residual, minus the target.

Definition (Lean source)
parameters
Z :
Type u_2
shared
X :
Type u_3
shared
H_γ :
Type*
AddCommGroup H_γ
Module ℝ H_γ
γ_target :
H_γ → X → ℝ
L :
H_γ → ℝ
proj_X :
Z → X
Y_obs :
Z → ℝ
γ :
H_γ
α :
X → ℝ
θ :
ℝ
z :
Z
def
rieszScore γ_target L proj_X Y_obs γ α θ z :
ℝ
given by
L γ + α (proj_X z) * (Y_obs z - γ_target γ (proj_X z)) - θ
Causalean.Estimation.OrthogonalMoments.rieszScore · Causalean/Estimation/OrthogonalMoments/Riesz.lean:66
theorem rieszScore_meanZero reviewed
Causalean.Estimation.OrthogonalMoments

Mean-zero of the Riesz score at the truth. Given a Riesz representation rep of a linear functional L on the regression class H_γ under P_X, with true regression function γ₀, and observed data given by the covariate projection proj_X and the outcome Y_obs, suppose the representer residual α₀(proj_X z)·(Y_obs z − γ_target γ₀ (proj_X z)) has population mean zero under P_Z — which holds when γ_target γ₀ is the conditional expectation of Y_obs given proj_X, since residuals are orthogonal to all square-integrable functions of proj_X. Then the orthogonal score rieszScore evaluated at the truth (γ₀, α₀, L γ₀) integrates to zero under P_Z:

Formal statement
hypotheses
Z :
Type u_2
Measure Z
shared
X :
Type u_3
shared
H_γ :
Type*
AddCommGroup H_γ
Module ℝ H_γ
H_γ → X → ℝ
H_γ → ℝ
P_X :
Measure X
IsProbabilityMeasure P_Z
rep :
RieszRepresentation H_γ γ_target L P_X
γ₀ :
H_γ
proj_X :
Z → X
Y_obs :
Z → ℝ
h_orthog :
∫ z, rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0
conclusion
∫ z, rieszScore γ_target L proj_X Y_obs γ₀ rep.α₀ (L γ₀) z ∂P_Z = 0
Proof (Lean source)
theorem rieszScore_meanZero {H_γ : Type*} [AddCommGroup H_γ] [Module ℝ H_γ] {γ_target : H_γ → X → ℝ} {L : H_γ → ℝ} {P_X : Measure X} [IsProbabilityMeasure P_Z] (rep : RieszRepresentation H_γ γ_target L P_X) (γ₀ : H_γ) (proj_X : Z → X) (Y_obs : Z → ℝ) (h_orthog : ∫ z, rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0) : ∫ z, rieszScore γ_target L proj_X Y_obs γ₀ rep.α₀ (L γ₀) z ∂P_Z = 0 := by unfold rieszScore have h1 : (fun z => L γ₀ + rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) - L γ₀) = fun z => rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) := by funext z ring rw [h1, h_orthog]
Causalean.Estimation.OrthogonalMoments.rieszScore_meanZero · Causalean/Estimation/OrthogonalMoments/Riesz.lean:89 · uses RieszRepresentation , rieszScore
1 supporting declaration (lemmas, instances)
  • rieszScore_bilinearRem theorem — Bilinear remainder identity for the Riesz score.
    hypotheses
    Z :
    Type u_2
    Measure Z
    shared
    X :
    Type u_3
    shared
    H_γ :
    Type*
    AddCommGroup H_γ
    Module ℝ H_γ
    H_γ → X → ℝ
    H_γ → ℝ
    P_X :
    Measure X
    IsProbabilityMeasure P_Z
    rep :
    RieszRepresentation H_γ γ_target L P_X
    γ₀ γ :
    H_γ
    α :
    X → ℝ
    proj_X :
    Z → X
    Y_obs :
    Z → ℝ
    h_pushforward :
    P_X = P_Z.map proj_X
    h_proj_meas :
    Measurable proj_X
    h_orthog_α₀ :
    ∫ z, rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0
    h_orthog_α :
    ∫ z, α (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0
    h_int_resid_α :
    Integrable (fun z => α (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z))) P_Z
    h_int_αγ :
    Integrable (fun z => α (proj_X z) * γ_target γ (proj_X z)) P_Z
    h_int_αγ₀ :
    Integrable (fun z => α (proj_X z) * γ_target γ₀ (proj_X z)) P_Z
    h_int_α₀γ :
    Integrable (fun x => rep.α₀ x * γ_target γ x) P_X
    h_int_α₀γ₀ :
    Integrable (fun x => rep.α₀ x * γ_target γ₀ x) P_X
    h_int_α :
    Integrable α P_X
    h_int_γ :
    Integrable (γ_target γ) P_X
    h_int_γ₀ :
    Integrable (γ_target γ₀) P_X
    conclusion
    (∫ z, rieszScore γ_target L proj_X Y_obs γ α (L γ₀) z ∂P_Z)
    - (∫ z, rieszScore γ_target L proj_X Y_obs γ₀ rep.α₀ (L γ₀) z ∂P_Z)
    = - ∫ x, (α x - rep.α₀ x) * (γ_target γ x - γ_target γ₀ x) ∂P_X
    Proof (Lean source)
    theorem rieszScore_bilinearRem {H_γ : Type*} [AddCommGroup H_γ] [Module ℝ H_γ] {γ_target : H_γ → X → ℝ} {L : H_γ → ℝ} {P_X : Measure X} [IsProbabilityMeasure P_Z] (rep : RieszRepresentation H_γ γ_target L P_X) (γ₀ γ : H_γ) (α : X → ℝ) (proj_X : Z → X) (Y_obs : Z → ℝ) (h_pushforward : P_X = P_Z.map proj_X) (h_proj_meas : Measurable proj_X) (h_orthog_α₀ : ∫ z, rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0) (h_orthog_α : ∫ z, α (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0) (h_int_resid_α : Integrable (fun z => α (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z))) P_Z) (h_int_αγ : Integrable (fun z => α (proj_X z) * γ_target γ (proj_X z)) P_Z) (h_int_αγ₀ : Integrable (fun z => α (proj_X z) * γ_target γ₀ (proj_X z)) P_Z) (h_int_α₀γ : Integrable (fun x => rep.α₀ x * γ_target γ x) P_X) (h_int_α₀γ₀ : Integrable (fun x => rep.α₀ x * γ_target γ₀ x) P_X) (h_int_α : Integrable α P_X) (h_int_γ : Integrable (γ_target γ) P_X) (h_int_γ₀ : Integrable (γ_target γ₀) P_X) : (∫ z, rieszScore γ_target L proj_X Y_obs γ α (L γ₀) z ∂P_Z) - (∫ z, rieszScore γ_target L proj_X Y_obs γ₀ rep.α₀ (L γ₀) z ∂P_Z) = - ∫ x, (α x - rep.α₀ x) * (γ_target γ x - γ_target γ₀ x) ∂P_X := by have h_int_αγ_X : Integrable (fun x => α x * γ_target γ x) P_X := by rw [h_pushforward] have h_asm : AEStronglyMeasurable (fun x => α x * γ_target γ x) (P_Z.map proj_X) := by rw [← h_pushforward] exact h_int_α.aestronglyMeasurable.fun_mul h_int_γ.aestronglyMeasurable exact (MeasureTheory.integrable_map_measure h_asm h_proj_meas.aemeasurable).2 h_int_αγ have h_int_αγ₀_X : Integrable (fun x => α x * γ_target γ₀ x) P_X := by rw [h_pushforward] have h_asm : AEStronglyMeasurable (fun x => α x * γ_target γ₀ x) (P_Z.map proj_X) := by rw [← h_pushforward] exact h_int_α.aestronglyMeasurable.fun_mul h_int_γ₀.aestronglyMeasurable exact (MeasureTheory.integrable_map_measure h_asm h_proj_meas.aemeasurable).2 h_int_αγ₀ have hscore : ∫ z, rieszScore γ_target L proj_X Y_obs γ α (L γ₀) z ∂P_Z = L γ - L γ₀ - ∫ z, α (proj_X z) * γ_target γ (proj_X z) ∂P_Z + ∫ z, α (proj_X z) * γ_target γ₀ (proj_X z) ∂P_Z := rieszScore_integral_eq γ₀ γ α proj_X Y_obs h_orthog_α h_int_resid_α h_int_αγ h_int_αγ₀ have htruth : ∫ z, rieszScore γ_target L proj_X Y_obs γ₀ rep.α₀ (L γ₀) z ∂P_Z = 0 := rieszScore_meanZero rep γ₀ proj_X Y_obs h_orthog_α₀ have hmap_αγ : ∫ z, α (proj_X z) * γ_target γ (proj_X z) ∂P_Z = ∫ x, α x * γ_target γ x ∂P_X := integral_comp_proj_eq h_pushforward h_proj_meas h_int_αγ_X have hmap_αγ₀ : ∫ z, α (proj_X z) * γ_target γ₀ (proj_X z) ∂P_Z = ∫ x, α x * γ_target γ₀ x ∂P_X := integral_comp_proj_eq h_pushforward h_proj_meas h_int_αγ₀_X have hrhs : ∫ x, (α x - rep.α₀ x) * (γ_target γ x - γ_target γ₀ x) ∂P_X = (∫ x, α x * γ_target γ x ∂P_X - ∫ x, rep.α₀ x * γ_target γ x ∂P_X) - (∫ x, α x * γ_target γ₀ x ∂P_X - ∫ x, rep.α₀ x * γ_target γ₀ x ∂P_X) := by let aγ : X → ℝ := fun x => α x * γ_target γ x let rγ : X → ℝ := fun x => rep.α₀ x * γ_target γ x let aγ₀ : X → ℝ := fun x => α x * γ_target γ₀ x let rγ₀ : X → ℝ := fun x => rep.α₀ x * γ_target γ₀ x have hpoint : (fun x => (α x - rep.α₀ x) * (γ_target γ x - γ_target γ₀ x)) = fun x => (aγ x - rγ x) - (aγ₀ x - rγ₀ x) := by funext x simp [aγ, rγ, aγ₀, rγ₀] ring rw [hpoint] change ∫ x, ((aγ - rγ) - (aγ₀ - rγ₀)) x ∂P_X = (∫ x, aγ x ∂P_X - ∫ x, rγ x ∂P_X) - (∫ x, aγ₀ x ∂P_X - ∫ x, rγ₀ x ∂P_X) have haγ : Integrable aγ P_X := h_int_αγ_X have hrγ : Integrable rγ P_X := h_int_α₀γ have haγ₀ : Integrable aγ₀ P_X := h_int_αγ₀_X have hrγ₀ : Integrable rγ₀ P_X := h_int_α₀γ₀ calc ∫ x, aγ x - rγ x - (aγ₀ x - rγ₀ x) ∂P_X = ∫ x, aγ x - rγ x ∂P_X - ∫ x, aγ₀ x - rγ₀ x ∂P_X := by exact integral_sub (haγ.sub hrγ) (haγ₀.sub hrγ₀) _ = (∫ x, aγ x ∂P_X - ∫ x, rγ x ∂P_X) - (∫ x, aγ₀ x ∂P_X - ∫ x, rγ₀ x ∂P_X) := by rw [integral_sub haγ hrγ] rw [integral_sub haγ₀ hrγ₀] rw [hscore, htruth, hmap_αγ, hmap_αγ₀, rep.representation γ, rep.representation γ₀] rw [hrhs] ring
    Causalean.Estimation.OrthogonalMoments.rieszScore_bilinearRem · Causalean/Estimation/OrthogonalMoments/Riesz.lean:188
AIPWInstance 2 core · 2 supporting This file instantiates the abstract orthogonal-moment framework with the augmented inverse-probability weighted moment for the back-door average treatment effect. ★ aipw_dml_isAsymLinear

AIPW General-Moment Instance

This file instantiates the abstract orthogonal-moment framework with the augmented inverse-probability weighted moment for the back-door average treatment effect. It packages mean-zero, finite-variance, and bilinear remainder facts so the general double-machine-learning theorem applies to the AIPW estimator.

The main declarations are aipwGeneralMoment, aipw_meanZero, aipw_bilinearRem, and the headline theorem aipw_dml_isAsymLinear, which specializes dml_chernozhukov_asymptoticLinear to the AIPW score.

def aipwGeneralMoment reviewed
Causalean.Estimation.ATE

Given a potential-outcome system with a measurable covariate space, a back-door estimation system, and a real radius for which the system's true nuisance functions belong to its almost-everywhere L2L^2 nuisance class, the AIPW general-moment specification is the abstract moment model whose data are the observed covariate, treatment, and outcome and whose target is the back-door average treatment effect.

Definition (Lean source)
parameters
P :
POSystem
shared
γ :
Type u_1
shared
S :
BackdoorEstimationSystem P γ
ε :
ℝ
hη₀_mem :
S.η₀ ∈ H_ε_aeL2 S ε
def
aipwGeneralMoment S hη₀_mem :
GeneralMoment P.Ω P.μ (γ × Bool × ℝ) S.P_Z (NuisanceVec γ)
given by
clause 1
m := fun η z θ => aipwMomentFunctional η z θ
clause 2
η₀ := S.η₀
clause 3
θ₀ := S.θ₀
clause 4
H_ε := H_ε_aeL2 S ε
clause 5
ρ₁ := fun η η'
=> ⟨(eLpNorm (fun x => η.μ_fn true x - η'.μ_fn true x) 2 S.P_X).toReal
+ (eLpNorm (fun x => η.μ_fn false x - η'.μ_fn false x) 2 S.P_X).toReal, by positivity⟩
clause 6
ρ₂ := fun η η'
=> ⟨(eLpNorm (fun x => η.e_fn x - η'.e_fn x) 2 S.P_X).toReal, by positivity⟩
clause 7
m_meas := fun η θ => BackdoorEstimationSystem.measurable_aipwMomentFunctional η θ
clause 8
η₀_mem := hη₀_mem
clause 9
J₀ := -1
clause 10
J₀_ne_zero := by norm_num
Causalean.Estimation.ATE.aipwGeneralMoment · Causalean/Estimation/OrthogonalMoments/AIPWInstance.lean:56 · uses BackdoorEstimationSystem , H_ε_aeL2 , P_Z , η₀ , NuisanceVec , instAddCommGroup , instModuleReal , GeneralMoment , POSystem
theorem aipw_dml_isAsymLinear reviewed
Causalean.Estimation.ATE

Headline AIPW DML asymptotic-linearity theorem, derived from the abstract dml_chernozhukov_asymptoticLinear in Estimation/OrthogonalMoments/DMLChernozhukov.lean. For the back-door AIPW estimator with true nuisance η₀ known to lie in the ε-ball H_ε_aeL2 S ε, assume the propensity score has ε-strict overlap, that the identification assumptions of the back-door system hold, and that the factual and potential outcomes are square-integrable. Given an i.i.d. sample with a one-shot fold split whose fold-B fraction converges to a strictly positive limit c > 0 along card (foldB n) / n → c, and a sequence of cross-fitted nuisance estimators η̂ that stay in the ε-ball at every fold and sample point with outcome-regression and propensity-score differences from the truth square-integrable in S.P_X. Assume the technical regularity package that the AIPW moment functional at η̂ is jointly measurable, fold-A-measurable in ω, and, at every fold and sample point, integrable and square-integrable under S.P_Z. Finally suppose the two nuisance-error rates are individually negligible ρ₁(η̂, η₀) = o_P(1), ρ₂(η̂, η₀) = o_P(1), and their product decays at the parametric rate ρ₁(η̂, η₀) · ρ₂(η̂, η₀) = o_P(n^{-1/2}). Then the Chernozhukov one-step AIPW-DML estimator is asymptotically linear at the true parameter S.θ₀ with the standard AIPW influence function ψ(z) = −J₀⁻¹ · ψ_AIPW(η₀, z), indexed over the fold-B subsample.

Formal statement
hypotheses
P :
POSystem
shared
γ :
Type u_1
shared
S :
BackdoorEstimationSystem P γ
ε :
ℝ
hη₀_mem :
S.η₀ ∈ H_ε_aeL2 S ε
h_overlap :
S.StrictOverlap ε
hA :
S.toPOBackdoorSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
h_yd2 :
∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ
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.Ω → NuisanceVec γ
h_in_Hε :
∀ n ω, η_hat n ω ∈ H_ε_aeL2 S ε
h_mu_diff_memLp :
∀ n ω a, MemLp (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X
h_e_diff_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X
h_m_meas :
∀ n,
Measurable (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentFunctional (η_hat n p.1) p.2 S.θ₀)
h_m_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => aipwMomentFunctional (η_hat n ω) z S.θ₀)
h_m_foldA_uncurry :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentFunctional (η_hat n p.1) p.2 S.θ₀)
h_m_int :
∀ n ω, Integrable (fun z => aipwMomentFunctional (η_hat n ω) z S.θ₀) S.P_Z
h_m_sq_int :
∀ n ω, Integrable (fun z => (aipwMomentFunctional (η_hat n ω) z S.θ₀) ^ 2) S.P_Z
h_indiv_rate_ρ₁ :
IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ
h_indiv_rate_ρ₂ :
IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ
h_product_rate :
IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
conclusion
IsAsymLinear (dmlChernozhukovEstimator (aipwGeneralMoment S hη₀_mem) sample split η_hat) S.θ₀ (fun z => -(aipwGeneralMoment S hη₀_mem).J₀_inv * aipwMomentFunctional S.η₀ z S.θ₀) sample split.foldB
Proof (Lean source)
theorem aipw_dml_isAsymLinear (S : BackdoorEstimationSystem P γ) {ε : ℝ} (hη₀_mem : S.η₀ ∈ H_ε_aeL2 S ε) (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (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.Ω → NuisanceVec γ) (h_in_Hε : ∀ n ω, η_hat n ω ∈ H_ε_aeL2 S ε) (h_mu_diff_memLp : ∀ n ω a, MemLp (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X) (h_e_diff_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X) (h_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentFunctional (η_hat n p.1) p.2 S.θ₀)) (h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => aipwMomentFunctional (η_hat n ω) z S.θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentFunctional (η_hat n p.1) p.2 S.θ₀)) (h_m_int : ∀ n ω, Integrable (fun z => aipwMomentFunctional (η_hat n ω) z S.θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => (aipwMomentFunctional (η_hat n ω) z S.θ₀) ^ 2) S.P_Z) (h_indiv_rate_ρ₁ : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ) (h_indiv_rate_ρ₂ : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) : IsAsymLinear (dmlChernozhukovEstimator (aipwGeneralMoment S hη₀_mem) sample split η_hat) S.θ₀ (fun z => -(aipwGeneralMoment S hη₀_mem).J₀_inv * aipwMomentFunctional S.η₀ z S.θ₀) sample split.foldB := by have hMZ := aipw_meanZero S hη₀_mem h_overlap hA h_y2 h_yd2 have hFV : Integrable (fun z => ((aipwGeneralMoment S hη₀_mem).m (aipwGeneralMoment S hη₀_mem).η₀ z (aipwGeneralMoment S hη₀_mem).θ₀) ^ 2) S.P_Z := by simpa [aipwGeneralMoment, BackdoorEstimationSystem.ψ_AIPW, BackdoorEstimationSystem.η₀, aipwMomentFunctional] using BackdoorEstimationSystem.aipw_finite_var_of_counterfactual_sq S h_overlap hA h_y2 h_yd2 -- Per-η̂_n bilinear remainder, built directly from `aipw_remainder_bound`. -- Replaces the ∀-quantified `aipw_bilinearRem` route. have hBR_at : ∀ n ω, |∫ z, (aipwGeneralMoment S hη₀_mem).m (η_hat n ω) z (aipwGeneralMoment S hη₀_mem).θ₀ ∂S.P_Z| ≤ aipw_rem_const ε * (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) (aipwGeneralMoment S hη₀_mem).η₀ : NNReal) : ℝ) * (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) (aipwGeneralMoment S hη₀_mem).η₀ : NNReal) : ℝ) := by intro n ω have h := BackdoorEstimationSystem.aipw_remainder_bound S h_overlap hA h_y2 h_yd2 (η_hat n ω) (h_in_Hε n ω) (h_mu_diff_memLp n ω) (h_e_diff_memLp n ω) -- Convert `Σ_a (‖Δμ_a‖ * ‖Δe‖)` into `(‖Δμ_T‖ + ‖Δμ_F‖) * ‖Δe‖`. have hsum : ∑ a : Bool, (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal = ((eLpNorm (fun x => (η_hat n ω).μ_fn true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => (η_hat n ω).μ_fn false x - S.μ_val false x) 2 S.P_X).toReal) * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal := by rw [Fintype.sum_bool, add_mul] rw [hsum] at h -- Unfold `M = aipwGeneralMoment` (η₀.μ_fn = S.μ_val, η₀.e_fn = S.e_val). change |∫ z, aipwMomentFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)| ≤ aipw_rem_const ε * ((eLpNorm (fun x => (η_hat n ω).μ_fn true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => (η_hat n ω).μ_fn false x - S.μ_val false x) 2 S.P_X).toReal) * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal linarith [h] -- Translate aggregated `ρ₁` rate into per-arm `μ_hat - μ_val` L² rate. have h_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ := by intro a δ hδ rw [ENNReal.tendsto_nhds_zero] intro κ hκ have hsum_event := (ENNReal.tendsto_nhds_zero.mp (h_indiv_rate_ρ₁ δ hδ)) κ hκ filter_upwards [hsum_event] with n hn refine (measure_mono ?_).trans hn intro ω hω have hcoord_le : |(eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal| ≤ |(((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)| := by -- `ρ₁` is an `NNReal` structure literal; unfolding it in the goal blocks -- every later rewrite, so bridge to its real value with a `rfl` equation. have hval : (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) = (eLpNorm (fun x => (η_hat n ω).μ_fn true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => (η_hat n ω).μ_fn false x - S.μ_val false x) 2 S.P_X).toReal := rfl by_cases ha : a = true · subst a rw [hval, abs_of_nonneg ENNReal.toReal_nonneg] exact (le_add_of_nonneg_right ENNReal.toReal_nonneg).trans (le_abs_self _) · have ha_false : a = false := by cases a <;> simp_all subst a rw [hval, abs_of_nonneg ENNReal.toReal_nonneg] exact (le_add_of_nonneg_left ENNReal.toReal_nonneg).trans (le_abs_self _) exact lt_of_lt_of_le hω hcoord_le have h_e_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ := by exact h_indiv_rate_ρ₂ have h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => (aipwGeneralMoment S hη₀_mem).m (η_hat n ω) z (aipwGeneralMoment S hη₀_mem).θ₀ - (aipwGeneralMoment S hη₀_mem).m (aipwGeneralMoment S hη₀_mem).η₀ z (aipwGeneralMoment S hη₀_mem).θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by simpa [aipwGeneralMoment] using BackdoorEstimationSystem.aipw_score_diff_isLittleOp_one S h_overlap hA h_y2 h_yd2 η_hat h_in_Hε h_mu_diff_memLp h_e_diff_memLp h_mu_rate h_e_rate simpa [aipwGeneralMoment] using (dml_chernozhukov_asymptoticLinear (aipwGeneralMoment S hη₀_mem) hMZ hFV sample split hc_pos h_split_rate η_hat (Crem := aipw_rem_const ε) hBR_at h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate)
Causalean.Estimation.ATE.aipw_dml_isAsymLinear · Causalean/Estimation/OrthogonalMoments/AIPWInstance.lean:138 · uses BackdoorEstimationSystem , H_ε_aeL2 , P_X , P_Z , StrictOverlap , aipwMomentFunctional , η₀ , θ₀ , NuisanceVec , instAddCommGroup , instModuleReal , aipwGeneralMoment , J₀_inv , dmlChernozhukovEstimator , Assumptions , YofD , factualY , POSystem , IIDSample , IsAsymLinear , IsLittleOp , OneShotSplit , foldA , foldB
2 supporting declarations (lemmas, instances)
DMLCross­Fit 2 core · 0 supporting This file proves the K-fold analogue of the Chernozhukov-form DML theorem. ★ dml_crossFit_asymptoticLinear

Cross-Fitted Double Machine Learning

This file proves the K-fold analogue of the Chernozhukov-form DML theorem. The estimator dmlCrossFitEstimator evaluates each fold with a nuisance learner trained on the complementary data and averages the fold scores. The main theorem dml_crossFit_asymptoticLinear shows asymptotic linearity with influence function -J₀⁻¹ · m(η₀, ·, θ₀) under the same mean-zero, finite-variance, score-difference, individual-rate, and product-rate hypotheses as the one-shot theorem, but imposed fold by fold.

def dmlCrossFitEstimator reviewed
Causalean.Estimation.OrthogonalMoments

For a measurable population space with a population measure, a measurable observed-data space with its observed-data law, and a real vector space of nuisance values, a general moment system, an independent and identically distributed sample, a number of folds, a K-fold split of that sample, a sequence of fold-specific nuisance estimators, and a sample-size index, the K-fold cross-fitted Chernozhukov double-machine-learning estimator maps each population state to the true target minus the inverse Jacobian times the average, across folds, of each fold's empirical mean moment evaluated at the true target and that fold's nuisance estimate.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
M :
GeneralMoment Ω μ Z P_Z H
sample :
IIDSample Ω Z μ P_Z
K :
ℕ
split :
KFoldSplit sample K
η_hat :
ℕ → Fin K → Ω → H
n :
ℕ
def
dmlCrossFitEstimator M sample split η_hat n :
Ω → ℝ
given by
fun ω
=> M.θ₀
- M.J₀_inv * ((K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m (η_hat n k ω) (sample.Z i ω) M.θ₀)
Causalean.Estimation.OrthogonalMoments.dmlCrossFitEstimator · Causalean/Estimation/OrthogonalMoments/DMLCrossFit.lean:440 · uses GeneralMoment , IIDSample , KFoldSplit
theorem dml_crossFit_asymptoticLinear reviewed
Causalean.Estimation.OrthogonalMoments

Asymptotic linearity of the K-fold cross-fitted Chernozhukov DML estimator. Same Chernozhukov form as dml_chernozhukov_asymptoticLinear, but with K folds. Given a general moment M with mean zero at the truth, assume the truth-evaluated score is square-integrable (finite variance), that there are at least two folds, K > 1, and a sequence of per-fold cross-fitted nuisance estimators η̂. Suppose the population moment at η̂, trained on each fold's complement, is bounded by a constant times the product of the two bilinear-remainder seminorms, at every fold count, fold index, and sample point. Assume the technical regularity package that the moment at η̂ is jointly measurable at every fold, measurable with respect to the fold's training complement, and, at every fold count, fold index, and sample point, integrable and square-integrable. Finally suppose that, at every fold, the L² score difference between the fold's estimated and true nuisance is o_P(1), each of the two nuisance-error rates is individually o_P(1), and their product decays at the parametric rate o_P(n^{-1/2}). Then the K-fold cross-fitted estimator is asymptotically linear at the truth M.θ₀ with influence function −J₀⁻¹ · m(η₀, ·, θ₀), indexed over the full sample (the fold-level sub-aggregations sum to a full-sample average asymptotically).

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
H :
Type u_3
shared
StandardBorelSpace Ω
IsFiniteMeasure μ
IsProbabilityMeasure μ
M :
GeneralMoment Ω μ Z P_Z H
_hMZ :
MeanZero M
_hFV :
Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z
sample :
IIDSample Ω Z μ P_Z
K :
ℕ
_hK_pos :
1 < K
split :
KFoldSplit sample K
η_hat :
ℕ → Fin K → Ω → H
Crem :
ℝ
_hBR_at :
∀ n k ω,
|∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z|
≤ Crem * ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)
_h_m_meas :
∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)
_h_m_train :
∀ n k,
Measurable[comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n k ω) z M.θ₀)
_h_m_train_uncurry :
∀ n k,
Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)
_h_m_int :
∀ n k ω, Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z
_h_m_sq_int :
∀ n k ω, Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z
_h_score_diff_rate :
∀ k,
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
_h_indiv_rate_ρ₁ :
∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) μ
_h_indiv_rate_ρ₂ :
∀ k, IsLittleOp (fun n ω => ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) μ
_h_product_rate :
∀ k,
IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ
conclusion
IsAsymLinear (dmlCrossFitEstimator M sample split η_hat) M.θ₀ (fun z => -M.J₀_inv * M.m M.η₀ z M.θ₀) sample (fun n => range n)
Proof (Lean source)
theorem dml_crossFit_asymptoticLinear [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : GeneralMoment Ω μ Z P_Z H) (_hMZ : MeanZero M) (_hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (_hK_pos : 1 < K) (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) {Crem : ℝ} (_hBR_at : ∀ n k ω, |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Crem * ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (_h_m_meas : ∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)) (_h_m_train : ∀ n k, Measurable[comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n k ω) z M.θ₀)) (_h_m_train_uncurry : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)) (_h_m_int : ∀ n k ω, Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z) (_h_m_sq_int : ∀ n k ω, Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z) (_h_score_diff_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (_h_indiv_rate_ρ₁ : ∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) μ) (_h_indiv_rate_ρ₂ : ∀ k, IsLittleOp (fun n ω => ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) μ) (_h_product_rate : ∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) : IsAsymLinear (dmlCrossFitEstimator M sample split η_hat) M.θ₀ (fun z => -M.J₀_inv * M.m M.η₀ z M.θ₀) sample (fun n => range n) := by let ψ₀ : Z → ℝ := fun z => M.m M.η₀ z M.θ₀ have hMZ_int : ∫ z, ψ₀ z ∂P_Z = 0 := _hMZ refine ⟨?_, ?_, ?_⟩ · -- Mean zero: multiply `MeanZero M` by the fixed scalar `-J₀⁻¹`. show ∫ z, -M.J₀_inv * M.m M.η₀ z M.θ₀ ∂P_Z = 0 calc ∫ z, -M.J₀_inv * M.m M.η₀ z M.θ₀ ∂P_Z = -M.J₀_inv * ∫ z, ψ₀ z ∂P_Z := by simp only [ψ₀, neg_mul, integral_neg, integral_const_mul] _ = 0 := by rw [hMZ_int]; ring · -- Finite variance: fixed scalar multiplication preserves square -- integrability of the Chernozhukov score. show Integrable (fun z => (-M.J₀_inv * M.m M.η₀ z M.θ₀) ^ 2) P_Z have h_eq : ∀ z, (-M.J₀_inv * M.m M.η₀ z M.θ₀) ^ 2 = M.J₀_inv ^ 2 * (M.m M.η₀ z M.θ₀) ^ 2 := by intro z; ring simp_rw [h_eq] exact _hFV.const_mul (M.J₀_inv ^ 2) · -- Remainder: separate the K-fold reduction into the -- stochastic fold terms, the population bias terms, and the final -- full-sample reweighting from fold averages. let foldScoreDiff : ℕ → Fin K → Ω → Z → ℝ := fun n k ω z => M.m (η_hat n k ω) z M.θ₀ - ψ₀ z let foldCentered : ℕ → Fin K → Ω → ℝ := fun n k ω => (sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, (foldScoreDiff n k ω (sample.Z i ω) - ∫ z, foldScoreDiff n k ω z ∂P_Z) let foldBias : ℕ → Fin K → Ω → ℝ := fun n k ω => sqrt ((split.fold n k).card : ℝ) * ∫ z, foldScoreDiff n k ω z ∂P_Z haveI : IsProbabilityMeasure P_Z := by rw [← sample.law] exact Measure.isProbabilityMeasure_map (sample.meas 0).aemeasurable have htruth_L2 : MemLp (fun z => M.m M.η₀ z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas M.η₀ M.θ₀).aestronglyMeasurable).2 _hFV have h_fold_centered : ∀ k, IsLittleOp (fun n ω => foldCentered n k ω) (fun _ => (1 : ℝ)) μ := by intro k let f : ℕ → Ω → Z → ℝ := fun n ω z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀ have hf_meas : ∀ n, Measurable (uncurry (f n)) := by intro n change Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (_h_m_meas n k).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_train : ∀ n, Measurable[comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance] (fun ω => f n ω) := by intro n change Measurable[comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) exact (_h_m_train n k).sub measurable_const have hf_uncurry_train : ∀ n, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (f n)) := by intro n change Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (_h_m_train_uncurry n k).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_memLp : ∀ n ω, MemLp (f n ω) 2 P_Z := by intro n ω have hrand_L2 : MemLp (fun z => M.m (η_hat n k ω) z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas (η_hat n k ω) M.θ₀).aestronglyMeasurable).2 (_h_m_sq_int n k ω) simp only [f] exact hrand_L2.sub htruth_L2 have hf_rate_one : IsLittleOp (fun n ω => (eLpNorm (f n ω) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ := by simpa [f] using _h_score_diff_rate k simpa [foldCentered, foldScoreDiff, ψ₀, f] using KFoldSplit.fold_centered_sum_isLittleOp_one sample split k f hf_meas hf_uncurry_train hf_memLp hf_rate_one have h_fold_bias : ∀ k, IsLittleOp (fun n ω => foldBias n k ω) (fun _ => (1 : ℝ)) μ := by intro k let f : ℕ → Ω → Z → ℝ := fun n ω z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀ have hf_meas : ∀ n, Measurable (uncurry (f n)) := by intro n change Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (_h_m_meas n k).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_memLp : ∀ n ω, MemLp (f n ω) 2 P_Z := by intro n ω have hrand_L2 : MemLp (fun z => M.m (η_hat n k ω) z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas (η_hat n k ω) M.θ₀).aestronglyMeasurable).2 (_h_m_sq_int n k ω) simp only [f] exact hrand_L2.sub htruth_L2 have h_int_eq : ∀ n ω, ∫ z, f n ω z ∂P_Z = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z := by intro n ω have hf_int : Integrable (f n ω) P_Z := (hf_memLp n ω).integrable (by norm_num : (1 : ENNReal) ≤ 2) have htruth_int : Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z := htruth_L2.integrable (by norm_num : (1 : ENNReal) ≤ 2) have hzero : (∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) = 0 := by simpa [MeanZero] using _hMZ calc ∫ z, f n ω z ∂P_Z = ∫ z, (M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) ∂P_Z := by rfl _ = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z := integral_sub (_h_m_int n k ω) htruth_int _ = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z := by rw [hzero] ring have h_int_raw_rate : IsLittleOp (fun n ω => ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ let Kc : ℝ := |Crem| + 1 have hKpos : 0 < Kc := by dsimp [Kc] linarith [abs_nonneg Crem] have htarget := (ENNReal.tendsto_nhds_zero.mp (_h_product_rate k (ε / Kc) (div_pos hε hKpos))) δ hδ exact htarget.mono fun n hn => (measure_mono (by intro ω hω let prodρ : ℝ := ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ) have hprod_nonneg : 0 ≤ prodρ := by dsimp [prodρ] exact mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _) have hbr := _hBR_at n k ω have hbr0 : |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Crem * prodρ := by simpa [prodρ, mul_assoc] using hbr have hle_abs : |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ |Crem| * prodρ := hbr0.trans (mul_le_mul_of_nonneg_right (le_abs_self Crem) hprod_nonneg) have hKbound : |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Kc * prodρ := by refine hle_abs.trans ?_ exact mul_le_mul_of_nonneg_right (by dsimp [Kc]; linarith) hprod_nonneg have hlt_bound : ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) < Kc * prodρ := lt_of_lt_of_le hω hKbound have hdiv_lt : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / Kc < prodρ := by rw [div_lt_iff₀ hKpos] simpa [mul_comm, mul_left_comm, mul_assoc] using hlt_bound have hsmall : (ε / Kc) * ((n : ℝ) ^ (-(1 / 2 : ℝ))) < |prodρ| := by have hdiv_eq : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / Kc = (ε / Kc) * ((n : ℝ) ^ (-(1 / 2 : ℝ))) := by ring rw [← hdiv_eq] -- … truncated; follow the source link for the rest …
Causalean.Estimation.OrthogonalMoments.dml_crossFit_asymptoticLinear · Causalean/Estimation/OrthogonalMoments/DMLCrossFit.lean:467 · uses GeneralMoment , J₀_inv , MeanZero , dmlCrossFitEstimator , IIDSample , IsAsymLinear , IsLittleOp , KFoldSplit , trainComplement
Linear­Smoother 5 core · 1 supporting This file specializes the abstract second-stage regression operator to weighted linear smoothers. ★ smoother_bias_holder★ smoother_bias_product_holder

Linear Smoother Second-Stage Operators

This file specializes the abstract second-stage regression operator to weighted linear smoothers. It records the weighted-sum representation and proves Hölder-type bias bounds for smoothed single functions and products of functions.

structure LinearSmootherOp reviewed
Causalean.Estimation.OrthogonalMoments

Linear-smoother operator (Def def:est-cate-second-stage, smoother form). A second-stage regression operator extended with an abstract array of smoothing weights indexed by sample size, randomness scope, query point, and data tuple, from which the weighted-sum representation of the operator's output can be built; the linear-combination identity itself is not required here but recorded separately as a predicate below.

Definition (Lean source)
parameters
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
γ :
Type*
MeasurableSpace γ
extends :
SecondStageOperator Ω μ γ
fields
weights :
ℕ → Ω → γ → (γ × Bool × ℝ) → ℝ
Causalean.Estimation.OrthogonalMoments.LinearSmootherOp · Causalean/Estimation/OrthogonalMoments/LinearSmoother.lean:43
def IsLinearSmoother reviewed
Causalean.Estimation.OrthogonalMoments.LinearSmootherOp

Given a linear-smoother operator, a sample size, a randomness realization, a query point, a finite index set for the data fold, real weights on that index set, and the corresponding covariate-treatment-outcome data tuples, the linear-smoother condition states that, for every real-valued pseudo-outcome function, the operator's estimate equals the weighted sum of that function over the fold.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
γ :
Type u_2
shared
ι :
Type*
op :
LinearSmootherOp Ω μ γ
n :
ℕ
ω :
Ω
x :
γ
B :
Finset ι
w :
ι → ℝ
xs :
ι → γ × Bool × ℝ
f :
γ × Bool × ℝ → ℝ
def
IsLinearSmoother op n ω x B w xs :
Prop
given by
op.evalAt n ω f x = ∑ i ∈ B, w i * f (xs i)
Causalean.Estimation.OrthogonalMoments.LinearSmootherOp.IsLinearSmoother · Causalean/Estimation/OrthogonalMoments/LinearSmoother.lean:72 · uses LinearSmootherOp
def WeightedNorm reviewed
Causalean.Estimation.OrthogonalMoments

Given a finite index set, real weights on that set, a real-valued function on its indices, and a real exponent, the weighted empirical norm is the normalized absolute-weight power mean of the function's absolute values, with the indicated exponent.

Definition (Lean source)
parameters
ι :
Type*
B :
Finset ι
w :
ι → ℝ
g :
ι → ℝ
p :
ℝ
def
WeightedNorm B w g p :
ℝ
given by
(∑ i ∈ B, |w i| / (∑ j ∈ B, |w j|) * |g i| ^ p) ^ (1 / p)
Causalean.Estimation.OrthogonalMoments.WeightedNorm · Causalean/Estimation/OrthogonalMoments/LinearSmoother.lean:103
theorem smoother_bias_holder reviewed
Causalean.Estimation.OrthogonalMoments

Single-function Hölder bound for a linear smoother. Assume op realises a linear smoother at sample size n, randomness ω, and query point x — its evaluation of any function on the fold B is the weighted sum Σ w_i · f(xs_i), and that the absolute weights sum to at most c_n. Then the absolute smoothed bias of g (evaluated on the γ-component of the data) at x is bounded by c_n times the weighted L¹ norm of g ∘ xs.1.

Formal statement
hypotheses
Ω :
Type*
MeasurableSpace Ω
Measure Ω
γ :
Type*
MeasurableSpace γ
ι :
Type*
op :
LinearSmootherOp Ω μ γ
n :
ℕ
ω :
Ω
x :
γ
g :
γ → ℝ
B :
Finset ι
w :
ι → ℝ
xs :
ι → γ × Bool × ℝ
c_n :
ℝ
hLin :
LinearSmootherOp.IsLinearSmoother op n ω x B w xs
hWeights :
∑ i ∈ B, |w i| ≤ c_n
conclusion
|op.evalAt n ω (fun z => g z.1) x| ≤ c_n * WeightedNorm B w (fun i => g (xs i).1) 1
Proof (Lean source)
theorem smoother_bias_holder {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {γ : Type*} [MeasurableSpace γ] {ι : Type*} (op : LinearSmootherOp Ω μ γ) (n : ℕ) (ω : Ω) (x : γ) (g : γ → ℝ) (B : Finset ι) (w : ι → ℝ) (xs : ι → γ × Bool × ℝ) (c_n : ℝ) (hLin : LinearSmootherOp.IsLinearSmoother op n ω x B w xs) (hWeights : ∑ i ∈ B, |w i| ≤ c_n) : |op.evalAt n ω (fun z => g z.1) x| ≤ c_n * WeightedNorm B w (fun i => g (xs i).1) 1 := by let S : ℝ := ∑ j ∈ B, |w j| have hS_nonneg : 0 ≤ S := by dsimp [S] exact sum_nonneg fun _ _ => abs_nonneg _ have hNorm_nonneg : 0 ≤ WeightedNorm B w (fun i => g (xs i).1) 1 := WeightedNorm_nonneg B w (fun i => g (xs i).1) 1 by_cases hS : S = 0 · have hw_zero : ∀ i ∈ B, w i = 0 := by intro i hi have h_abs_zero : |w i| = 0 := by have h_each := (Finset.sum_eq_zero_iff_of_nonneg (s := B) (f := fun i => |w i|) (fun _ _ => abs_nonneg _)).mp hS exact h_each i hi exact abs_eq_zero.mp h_abs_zero have hEval_zero : op.evalAt n ω (fun z => g z.1) x = 0 := by rw [hLin (fun z => g z.1)] apply Finset.sum_eq_zero intro i hi simp [hw_zero i hi] rw [hEval_zero, abs_zero] exact mul_nonneg (le_trans (by simpa [S] using hS_nonneg) hWeights) hNorm_nonneg · have hS_pos : 0 < S := lt_of_le_of_ne hS_nonneg (Ne.symm hS) have hAbsEval : |op.evalAt n ω (fun z => g z.1) x| ≤ ∑ i ∈ B, |w i| * |g (xs i).1| := by rw [hLin (fun z => g z.1)] calc |∑ i ∈ B, w i * g (xs i).1| ≤ ∑ i ∈ B, |w i * g (xs i).1| := Finset.abs_sum_le_sum_abs (fun i => w i * g (xs i).1) B _ = ∑ i ∈ B, |w i| * |g (xs i).1| := by apply Finset.sum_congr rfl intro i hi rw [abs_mul] have hWeighted : ∑ i ∈ B, |w i| * |g (xs i).1| = S * WeightedNorm B w (fun i => g (xs i).1) 1 := by unfold WeightedNorm simp only [Real.rpow_one, div_one] calc ∑ i ∈ B, |w i| * |g (xs i).1| = ∑ i ∈ B, S * (|w i| / S * |g (xs i).1|) := by apply Finset.sum_congr rfl intro i hi field_simp [hS] _ = S * ∑ i ∈ B, |w i| / S * |g (xs i).1| := by rw [Finset.mul_sum] calc |op.evalAt n ω (fun z => g z.1) x| ≤ S * WeightedNorm B w (fun i => g (xs i).1) 1 := by simpa [hWeighted] using hAbsEval _ ≤ c_n * WeightedNorm B w (fun i => g (xs i).1) 1 := mul_le_mul_of_nonneg_right (by simpa [S] using hWeights) hNorm_nonneg
Causalean.Estimation.OrthogonalMoments.smoother_bias_holder · Causalean/Estimation/OrthogonalMoments/LinearSmoother.lean:135 · uses LinearSmootherOp , IsLinearSmoother , WeightedNorm
theorem smoother_bias_product_holder reviewed
Causalean.Estimation.OrthogonalMoments

Product Hölder bound for a linear smoother (Prop prop:est-cate-linear-smoother-bound). Assume op realises a linear smoother at sample size n, randomness ω, and query point x, that the absolute weights sum to at most c_n, and that p and q are Hölder-conjugate exponents, 1/p + 1/q = 1. Then the absolute smoothed bias of the product g₁ · g₂ (evaluated on the γ-component of the data) at x is bounded by c_n times the weighted L^p norm of g₁ ∘ xs.1 times the weighted L^q norm of g₂ ∘ xs.1.

Formal statement
hypotheses
Ω :
Type*
MeasurableSpace Ω
Measure Ω
γ :
Type*
MeasurableSpace γ
ι :
Type*
op :
LinearSmootherOp Ω μ γ
n :
ℕ
ω :
Ω
x :
γ
g₁ g₂ :
γ → ℝ
B :
Finset ι
w :
ι → ℝ
xs :
ι → γ × Bool × ℝ
c_n p q :
ℝ
hLin :
LinearSmootherOp.IsLinearSmoother op n ω x B w xs
hWeights :
∑ i ∈ B, |w i| ≤ c_n
hConj :
HolderConjugate p q
conclusion
|op.evalAt n ω (fun z => g₁ z.1 * g₂ z.1) x|
≤ c_n * WeightedNorm B w (fun i => g₁ (xs i).1) p * WeightedNorm B w (fun i => g₂ (xs i).1) q
Proof (Lean source)
theorem smoother_bias_product_holder {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {γ : Type*} [MeasurableSpace γ] {ι : Type*} (op : LinearSmootherOp Ω μ γ) (n : ℕ) (ω : Ω) (x : γ) (g₁ g₂ : γ → ℝ) (B : Finset ι) (w : ι → ℝ) (xs : ι → γ × Bool × ℝ) (c_n p q : ℝ) (hLin : LinearSmootherOp.IsLinearSmoother op n ω x B w xs) (hWeights : ∑ i ∈ B, |w i| ≤ c_n) (hConj : HolderConjugate p q) : |op.evalAt n ω (fun z => g₁ z.1 * g₂ z.1) x| ≤ c_n * WeightedNorm B w (fun i => g₁ (xs i).1) p * WeightedNorm B w (fun i => g₂ (xs i).1) q := by let S : ℝ := ∑ j ∈ B, |w j| let α : ι → ℝ := fun i => |w i| / S have hS_nonneg : 0 ≤ S := by dsimp [S] exact sum_nonneg fun _ _ => abs_nonneg _ have hc_nonneg : 0 ≤ c_n := le_trans (by simpa [S] using hS_nonneg) hWeights have hα_nonneg : ∀ i ∈ B, 0 ≤ α i := by intro i hi exact div_nonneg (abs_nonneg _) hS_nonneg have hpq_one : 1 / p + 1 / q = 1 := by simpa using hConj.one_div_add_one_div have hNormHolder : WeightedNorm B w (fun i => g₁ (xs i).1 * g₂ (xs i).1) 1 ≤ WeightedNorm B w (fun i => g₁ (xs i).1) p * WeightedNorm B w (fun i => g₂ (xs i).1) q := by have hHolder := Real.inner_le_Lp_mul_Lq_of_nonneg (s := B) (f := fun i => (α i) ^ (1 / p) * |g₁ (xs i).1|) (g := fun i => (α i) ^ (1 / q) * |g₂ (xs i).1|) hConj (by intro i hi exact mul_nonneg (Real.rpow_nonneg (hα_nonneg i hi) _) (abs_nonneg _)) (by intro i hi exact mul_nonneg (Real.rpow_nonneg (hα_nonneg i hi) _) (abs_nonneg _)) have hLeft : (∑ i ∈ B, ((α i) ^ (1 / p) * |g₁ (xs i).1|) * ((α i) ^ (1 / q) * |g₂ (xs i).1|)) = ∑ i ∈ B, α i * |g₁ (xs i).1 * g₂ (xs i).1| := by apply Finset.sum_congr rfl intro i hi rw [abs_mul] calc ((α i) ^ (1 / p) * |g₁ (xs i).1|) * ((α i) ^ (1 / q) * |g₂ (xs i).1|) = ((α i) ^ (1 / p) * (α i) ^ (1 / q)) * (|g₁ (xs i).1| * |g₂ (xs i).1|) := by ring _ = (α i) ^ (1 / p + 1 / q) * (|g₁ (xs i).1| * |g₂ (xs i).1|) := by rw [Real.rpow_add_of_nonneg (hα_nonneg i hi) hConj.one_div_nonneg hConj.symm.one_div_nonneg] _ = α i * (|g₁ (xs i).1| * |g₂ (xs i).1|) := by rw [hpq_one, Real.rpow_one] have hRight₁ : (∑ i ∈ B, ((α i) ^ (1 / p) * |g₁ (xs i).1|) ^ p) = ∑ i ∈ B, α i * |g₁ (xs i).1| ^ p := by apply Finset.sum_congr rfl intro i hi rw [Real.mul_rpow (Real.rpow_nonneg (hα_nonneg i hi) _) (abs_nonneg _)] rw [one_div, Real.rpow_inv_rpow (hα_nonneg i hi) hConj.ne_zero] have hRight₂ : (∑ i ∈ B, ((α i) ^ (1 / q) * |g₂ (xs i).1|) ^ q) = ∑ i ∈ B, α i * |g₂ (xs i).1| ^ q := by apply Finset.sum_congr rfl intro i hi rw [Real.mul_rpow (Real.rpow_nonneg (hα_nonneg i hi) _) (abs_nonneg _)] rw [one_div, Real.rpow_inv_rpow (hα_nonneg i hi) hConj.symm.ne_zero] unfold WeightedNorm simp only [Real.rpow_one, div_one] change (∑ i ∈ B, α i * |g₁ (xs i).1 * g₂ (xs i).1|) ≤ (∑ i ∈ B, α i * |g₁ (xs i).1| ^ p) ^ (1 / p) * (∑ i ∈ B, α i * |g₂ (xs i).1| ^ q) ^ (1 / q) rw [← hLeft, ← hRight₁, ← hRight₂] simpa [mul_assoc] using hHolder calc |op.evalAt n ω (fun z => g₁ z.1 * g₂ z.1) x| ≤ c_n * WeightedNorm B w (fun i => g₁ (xs i).1 * g₂ (xs i).1) 1 := smoother_bias_holder op n ω x (fun y => g₁ y * g₂ y) B w xs c_n hLin hWeights _ ≤ c_n * WeightedNorm B w (fun i => g₁ (xs i).1) p * WeightedNorm B w (fun i => g₂ (xs i).1) q := by have := mul_le_mul_of_nonneg_left hNormHolder hc_nonneg simpa [mul_assoc] using this
Causalean.Estimation.OrthogonalMoments.smoother_bias_product_holder · Causalean/Estimation/OrthogonalMoments/LinearSmoother.lean:214 · uses LinearSmootherOp , IsLinearSmoother , WeightedNorm
1 supporting declaration (lemmas, instances)
Parametric 2 core · 0 supporting This file shows how the orthogonal-moment machinery specializes to ordinary parametric one-step estimators with no separate nuisance function, covering the classical score-based template behind regression, instrumental v ★ parametric_asymptoticLinear

Parametric Orthogonal Moments

This file shows how the orthogonal-moment machinery specializes to ordinary parametric one-step estimators with no separate nuisance function, covering the classical score-based template behind regression, instrumental variables, and maximum likelihood examples. The definition parametricMoment encodes the no-nuisance GeneralMoment with H = Unit, and parametric_asymptoticLinear proves that the resulting Chernozhukov estimator has an identically zero remainder after subtracting its influence-function partial sum.

def parametricMoment reviewed
Causalean.Estimation.OrthogonalMoments

For a measurable population space with a population measure and a measurable observed-data space with its observed-data law, a real-valued parametric moment function, a target parameter, a nonzero scalar Jacobian, and the condition that the moment is measurable at every parameter value, the no-nuisance parametric moment system is the general moment system whose score is the supplied parametric moment and whose nuisance space contains only a single element.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
m_par :
ℝ → Z → ℝ
θ₀ :
ℝ
J₀ :
ℝ
hJ :
J₀ ≠ 0
m_meas :
∀ θ, Measurable (m_par θ)
def
parametricMoment m_par θ₀ J₀ hJ m_meas :
GeneralMoment Ω μ Z P_Z Unit
given by
clause 1
m := fun _ z θ => m_par θ z
clause 2
η₀ := ()
clause 3
θ₀ := θ₀
clause 4
H_ε := univ
clause 5
ρ₁ := fun _ _ => 0
clause 6
ρ₂ := fun _ _ => 0
clause 7
m_meas := fun _ θ => m_meas θ
clause 8
η₀_mem := Set.mem_univ _
clause 9
J₀ := J₀
clause 10
J₀_ne_zero := hJ
Causalean.Estimation.OrthogonalMoments.parametricMoment · Causalean/Estimation/OrthogonalMoments/Parametric.lean:40 · uses GeneralMoment
theorem parametric_asymptoticLinear reviewed
Causalean.Estimation.OrthogonalMoments

Asymptotic linearity of the parametric one-step estimator. Fix a score m_par with a nonzero scalar Jacobian J₀ at the true parameter θ₀, where m_par θ is measurable for every θ. If the score m_par θ₀ has population mean zero and it has finite second moment, then for an i.i.d. sample and a one-shot fold split of it, the parametric one-step estimator built from m_par and J₀ is asymptotically linear at θ₀ with influence function ψ(z) := −J₀⁻¹·m_par(θ₀, z).

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
shared
Z :
Type u_2
Measure Z
shared
m_par :
ℝ → Z → ℝ
θ₀ :
ℝ
J₀ :
ℝ
hJ :
J₀ ≠ 0
m_meas :
∀ θ, Measurable (m_par θ)
h_mean_zero :
∫ z, m_par θ₀ z ∂P_Z = 0
h_finite_var :
Integrable (fun z => (m_par θ₀ z) ^ 2) P_Z
sample :
IIDSample Ω Z μ P_Z
split :
OneShotSplit sample
conclusion
IsAsymLinear (dmlChernozhukovEstimator (parametricMoment (Ω := Ω) (μ := μ) (P_Z := P_Z) m_par θ₀ J₀ hJ m_meas) sample split (fun _ _ => ())) θ₀ (fun z => -(J₀⁻¹) * m_par θ₀ z) sample split.foldB
Proof (Lean source)
theorem parametric_asymptoticLinear (m_par : ℝ → Z → ℝ) (θ₀ : ℝ) (J₀ : ℝ) (hJ : J₀ ≠ 0) (m_meas : ∀ θ, Measurable (m_par θ)) (h_mean_zero : ∫ z, m_par θ₀ z ∂P_Z = 0) (h_finite_var : Integrable (fun z => (m_par θ₀ z) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample) : IsAsymLinear (dmlChernozhukovEstimator (parametricMoment (Ω := Ω) (μ := μ) (P_Z := P_Z) m_par θ₀ J₀ hJ m_meas) sample split (fun _ _ => ())) θ₀ (fun z => -(J₀⁻¹) * m_par θ₀ z) sample split.foldB := by set M : GeneralMoment Ω μ Z P_Z Unit := parametricMoment m_par θ₀ J₀ hJ m_meas with hM refine ⟨?_, ?_, ?_⟩ · -- mean_zero rw [integral_const_mul, h_mean_zero, mul_zero] · -- finite_var refine (h_finite_var.const_mul (J₀⁻¹ ^ 2)).congr ?_ filter_upwards with z ring · -- remainder: identically zero, since the parametric one-step exactly -- equals the influence-function partial sum. have h_pointwise : ∀ n ω, sqrt ((split.foldB n).card : ℝ) * (dmlChernozhukovEstimator M sample split (fun _ _ => ()) n ω - θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, -(J₀⁻¹) * m_par θ₀ (sample.Z i ω) = 0 := by intro n ω set S : ℝ := ∑ i ∈ split.foldB n, m_par θ₀ (sample.Z i ω) with hS set c : ℝ := ((split.foldB n).card : ℝ) with hc have h_sum_eq : ∑ i ∈ split.foldB n, -(J₀⁻¹) * m_par θ₀ (sample.Z i ω) = -(J₀⁻¹) * S := by rw [hS, ← Finset.mul_sum] have h_est : dmlChernozhukovEstimator M sample split (fun _ _ => ()) n ω = θ₀ - J₀⁻¹ * (c⁻¹ * S) := by simp [dmlChernozhukovEstimator, M, parametricMoment, GeneralMoment.J₀_inv, hS, hc] rw [h_est, h_sum_eq] by_cases hc0 : c = 0 · -- |B(n)| = 0: all sums vanish. have hcard : (split.foldB n).card = 0 := by have hcard_real : ((split.foldB n).card : ℝ) = 0 := by rw [← hc]; exact hc0 exact_mod_cast hcard_real have hS0 : S = 0 := by rw [hS] exact Finset.sum_eq_zero (fun i hi => absurd (Finset.card_pos.mpr ⟨i, hi⟩) (by rw [hcard]; exact lt_irrefl 0)) rw [hc0, hS0] simp · have hc_nn : 0 ≤ c := by rw [hc]; exact Nat.cast_nonneg _ have hc_pos : 0 < c := lt_of_le_of_ne hc_nn (Ne.symm hc0) have hsqrt_pos : 0 < sqrt c := Real.sqrt_pos.mpr hc_pos have hsqrt_ne : sqrt c ≠ 0 := ne_of_gt hsqrt_pos have h_sqrt_sq : sqrt c * sqrt c = c := Real.mul_self_sqrt hc_nn have hsqrt_inv : sqrt c * c⁻¹ = (sqrt c)⁻¹ := by field_simp rw [sq, h_sqrt_sq] calc sqrt c * (θ₀ - J₀⁻¹ * (c⁻¹ * S) - θ₀) - (sqrt c)⁻¹ * (-(J₀⁻¹) * S) = -J₀⁻¹ * (sqrt c * c⁻¹) * S + J₀⁻¹ * (sqrt c)⁻¹ * S := by ring _ = -J₀⁻¹ * (sqrt c)⁻¹ * S + J₀⁻¹ * (sqrt c)⁻¹ * S := by rw [hsqrt_inv] _ = 0 := by ring -- The remainder function equals zero everywhere, so it is `o_p(1)`. intro ε hε have h_zero_set : ∀ n, {ω : Ω | ε * (fun _ => (1 : ℝ)) n < |sqrt ((split.foldB n).card : ℝ) * (dmlChernozhukovEstimator M sample split (fun _ _ => ()) n ω - θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, -(J₀⁻¹) * m_par θ₀ (sample.Z i ω)|} = ∅ := by intro n ext ω simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_lt] rw [h_pointwise n ω] simpa using le_of_lt hε have h_meas_zero : ∀ n, μ {ω : Ω | ε * (fun _ => (1 : ℝ)) n < |sqrt ((split.foldB n).card : ℝ) * (dmlChernozhukovEstimator M sample split (fun _ _ => ()) n ω - θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, -(J₀⁻¹) * m_par θ₀ (sample.Z i ω)|} = 0 := by intro n rw [h_zero_set n] exact MeasureTheory.measure_empty simp_rw [h_meas_zero] exact tendsto_const_nhds
Causalean.Estimation.OrthogonalMoments.parametric_asymptoticLinear · Causalean/Estimation/OrthogonalMoments/Parametric.lean:64 · uses dmlChernozhukovEstimator , parametricMoment , IIDSample , IsAsymLinear , OneShotSplit , foldB
Second­Stage­Operator 6 core · 0 supporting This file defines the target-agnostic second-stage operator used in DR-Learner CATE estimation. ★ oracle_expansion

Abstract Second-Stage Regression Operators

This file defines the target-agnostic second-stage operator used in DR-Learner CATE estimation. The public API consists of SecondStageOperator, the input-linearity predicate SecondStageOperator.IsLinearInInput, the oracle estimator and oracle risk scale, the stability predicate Stable, and the abstract oracle-expansion theorem oracle_expansion. It separates the operator itself from linearity and conditional-bias identification assumptions.

structure SecondStageOperator reviewed
Causalean.Estimation.OrthogonalMoments

Abstract bundle for a second-stage regression operator (Def def:est-cate-second-stage): an operator mapping a sample size, a randomness scope, a real-valued pseudo-outcome function of a data tuple, and a query point to a real-valued estimate, together with the minimal requirement that for every sample size and constant pseudo-outcome, the map from randomness scope and query point to the operator's value is jointly measurable; stronger measurability, and any linearity of the operator in its function input, are deferred to concrete instances or the separate IsLinearInInput predicate.

Definition (Lean source)
parameters
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
γ :
Type*
MeasurableSpace γ
fields
evalAt :
ℕ → Ω → (γ × Bool × ℝ → ℝ) → γ → ℝ
meas_evalAt_const :
∀ (n : ℕ) (c : ℝ), Measurable (fun (p : Ω × γ) => evalAt n p.1 (fun _ => c) p.2)
Causalean.Estimation.OrthogonalMoments.SecondStageOperator · Causalean/Estimation/OrthogonalMoments/SecondStageOperator.lean:47
def IsLinearInInput reviewed
Causalean.Estimation.OrthogonalMoments.SecondStageOperator

For a second-stage regression operator, linearity in the pseudo-outcome input means that, for every sample size, randomness realization, pair of real-valued pseudo-outcome functions, and query point, the estimate for their pointwise sum equals the sum of their separate estimates. Linear smoothers satisfy this predicate; kernel-or-tree mean estimators with random splits need not satisfy it.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
γ :
Type u_2
shared
op :
SecondStageOperator Ω μ γ
n :
ℕ
ω :
Ω
f g :
γ × Bool × ℝ → ℝ
x :
γ
def
IsLinearInInput op :
Prop
given by
op.evalAt n ω (fun z => f z + g z) x = op.evalAt n ω f x + op.evalAt n ω g x
Causalean.Estimation.OrthogonalMoments.SecondStageOperator.IsLinearInInput · Causalean/Estimation/OrthogonalMoments/SecondStageOperator.lean:81 · uses SecondStageOperator
def oracleEstimator reviewed
Causalean.Estimation.OrthogonalMoments.SecondStageOperator

Given a second-stage regression operator and a fixed real-valued pseudo-outcome function, the oracle estimator maps each sample size, randomness realization, and query point to the operator's estimate using that fixed pseudo-outcome.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
γ :
Type u_2
shared
op :
SecondStageOperator Ω μ γ
f :
γ × Bool × ℝ → ℝ
def
oracleEstimator op f :
ℕ → Ω → γ → ℝ
given by
fun n ω x => op.evalAt n ω f x
Causalean.Estimation.OrthogonalMoments.SecondStageOperator.oracleEstimator · Causalean/Estimation/OrthogonalMoments/SecondStageOperator.lean:92 · uses SecondStageOperator
def oracleRiskScale reviewed
Causalean.Estimation.OrthogonalMoments.SecondStageOperator

Given a second-stage regression operator, a fixed real-valued pseudo-outcome function, a target function, a query point, and a sample size, the oracle pointwise risk scale is the square root of the expected squared difference, over the operator's randomness, between the oracle estimator and the target at that query point.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
γ :
Type u_2
shared
op :
SecondStageOperator Ω μ γ
f :
γ × Bool × ℝ → ℝ
target :
γ → ℝ
x :
γ
n :
ℕ
def
oracleRiskScale op f target x n :
ℝ
given by
sqrt (∫ ω, (op.evalAt n ω f x - target x) ^ 2 ∂μ)
Causalean.Estimation.OrthogonalMoments.SecondStageOperator.oracleRiskScale · Causalean/Estimation/OrthogonalMoments/SecondStageOperator.lean:100 · uses SecondStageOperator
def Stable reviewed
Causalean.Estimation.OrthogonalMoments

Given a second-stage regression operator, a target function, a sequence of distances between pseudo-outcomes, a query point, and a conditional-bias identification criterion, stability means that for every estimated pseudo-outcome sequence, true pseudo-outcome, and claimed conditional-bias sequence satisfying the criterion, convergence of the distance to zero in probability implies that the operator discrepancy after subtracting the smoothed bias is negligible in probability relative to the oracle pointwise risk scale.

Definition (Lean source)
parameters
Ω :
Type u_1
Measure Ω
shared
γ :
Type u_2
shared
op :
SecondStageOperator Ω μ γ
target :
γ → ℝ
d_n :
ℕ → Ω → ℝ
x :
γ
BiasIdent :
(ℕ → Ω → γ × Bool × ℝ → ℝ) → (γ × Bool × ℝ → ℝ) → (ℕ → Ω → γ → ℝ) → Prop
fHat_n :
ℕ → Ω → γ × Bool × ℝ → ℝ
f :
γ × Bool × ℝ → ℝ
bHat_n :
ℕ → Ω → γ → ℝ
Tendsto_inProb d_n (fun _ => 0) μ
BiasIdent fHat_n f bHat_n
def
Stable op target d_n x BiasIdent :
Prop
given by
IsLittleOp (fun n ω => op.evalAt n ω (fHat_n n ω) x - op.evalAt n ω f x - op.evalAt n ω (fun z => bHat_n n ω z.1) x) (fun n => SecondStageOperator.oracleRiskScale op f target x n) μ
Causalean.Estimation.OrthogonalMoments.Stable · Causalean/Estimation/OrthogonalMoments/SecondStageOperator.lean:122 · uses SecondStageOperator
theorem oracle_expansion reviewed
Causalean.Estimation.OrthogonalMoments

Oracle expansion for the DR-Learner (Thm thm:est-cate-dr-oracle, abstract operator-level form). Given a second-stage regression operator op that is stable at the query point x for target function target, with respect to a distance d_n between pseudo-outcomes and a caller-supplied conditional-bias identification predicate BiasIdent, suppose d_n converges to zero in probability under μ, i.e. the first-stage pseudo-outcome estimate is consistent, and suppose the estimated pseudo-outcome fHat_n, the true pseudo-outcome f, and the claimed conditional bias bHat_n satisfy BiasIdent. Then the discrepancy between the operator applied to fHat_n and to f, minus the operator applied to bHat_n, is o_p of the oracle risk scale under μ: the operator-level oracle expansion holds modulo o_p(R^*_n(x)).

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
shared
γ :
Type u_2
shared
op :
SecondStageOperator Ω μ γ
target :
γ → ℝ
x :
γ
d_n :
ℕ → Ω → ℝ
fHat_n :
ℕ → Ω → γ × Bool × ℝ → ℝ
f :
γ × Bool × ℝ → ℝ
bHat_n :
ℕ → Ω → γ → ℝ
BiasIdent :
(ℕ → Ω → γ × Bool × ℝ → ℝ) → (γ × Bool × ℝ → ℝ) → (ℕ → Ω → γ → ℝ) → Prop
hStab :
Stable op target d_n x BiasIdent
hCons :
Tendsto_inProb d_n (fun _ => 0) μ
hBias :
BiasIdent fHat_n f bHat_n
conclusion
IsLittleOp (fun n ω => op.evalAt n ω (fHat_n n ω) x - op.evalAt n ω f x - op.evalAt n ω (fun z => bHat_n n ω z.1) x) (fun n => SecondStageOperator.oracleRiskScale op f target x n) μ
Proof (Lean source)
theorem oracle_expansion (op : SecondStageOperator Ω μ γ) (target : γ → ℝ) (x : γ) (d_n : ℕ → Ω → ℝ) (fHat_n : ℕ → Ω → γ × Bool × ℝ → ℝ) (f : γ × Bool × ℝ → ℝ) (bHat_n : ℕ → Ω → γ → ℝ) (BiasIdent : (ℕ → Ω → γ × Bool × ℝ → ℝ) → (γ × Bool × ℝ → ℝ) → (ℕ → Ω → γ → ℝ) → Prop) (hStab : Stable op target d_n x BiasIdent) (hCons : Tendsto_inProb d_n (fun _ => 0) μ) (hBias : BiasIdent fHat_n f bHat_n) : IsLittleOp (fun n ω => op.evalAt n ω (fHat_n n ω) x - op.evalAt n ω f x - op.evalAt n ω (fun z => bHat_n n ω z.1) x) (fun n => SecondStageOperator.oracleRiskScale op f target x n) μ := by exact hStab fHat_n f bHat_n hCons hBias
Causalean.Estimation.OrthogonalMoments.oracle_expansion · Causalean/Estimation/OrthogonalMoments/SecondStageOperator.lean:158 · uses SecondStageOperator , oracleRiskScale , Stable , IsLittleOp , Tendsto_inProb