Estimation.OrthogonalMoments
Neyman-orthogonal moment functions: construction, cross-fitting, parametric examples, and automatic debiasing.
MomentFunctional 6 core · 0 supporting This file defines the moment-functional interface used by the double machine learning layer. ★ linScale_mul_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 a nonzero linearization scale. Concrete double-machine-learning instances reduce to filling this interface, which centralizes the generic asymptotic-linearity machinery.
For randomness and observed-data spaces with measures and a real nuisance vector space, a general scaled moment system bundles a score function, a truth nuisance, a truth parameter, an admissible perturbation set, two error gauges, and a caller-supplied linearization scale, subject to score measurability, truth membership in the perturbation set, and nonvanishing of the scale.
For a general moment system, the inverse linearization scale is the reciprocal of the system's nonzero caller-supplied scale.
Definition (Lean source)
For a general orthogonal-moment system, its linearization scale times its reciprocal equals one.
Formal statement
Proof (Lean source)
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)
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)
For randomness and observed-data spaces with measures and a real nuisance vector space, a linear moment system is a general moment with coefficient and constant score terms, measurability of those terms, an affine score decomposition, and identification of the linearization scale with the population coefficient mean.
Definition (Lean source)
DirectionalDeriv 1 core · 0 supporting This file packages the almost-everywhere nuisance directional derivative data required by the abstract double machine learning framework.
Directional Derivatives for Abstract Moments
This file packages the almost-everywhere 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.
For a general moment, a candidate almost-everywhere 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 almost 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)
NeymanOrthogonal 4 core · 1 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.
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)
For a general moment system, Gateaux Neyman orthogonality means that the population moment along every admissible nuisance direction has derivative zero at the true nuisance.
Definition (Lean source)
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)
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
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
hasDirDeriv_to_neymanOrthogonalGateauxtheorem — DCT bridge to the standard Gateaux form. Given a general moment system, almost-everywhere directional derivatives, vanishing integrated directional derivatives, and a dominating difference-quotient envelope, if every nonzero point on each admissible nuisance path has an integrable moment and the true moment is integrable, then the population moment is Gateaux Neyman-orthogonal.hypothesesH :sharedType u_3M :GeneralMoment Ω μ Z P_Z HD :hNO :NeymanOrthogonal M DhEnv :hMt_int :∀ η ∈ M.H_ε, ∀ t ≠ (0 : ℝ), Integrable (fun z => M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀) P_ZhM0_int :Integrable (fun z => M.m M.η₀ z M.θ₀) P_ZconclusionProof (Lean source)
theorem hasDirDeriv_to_neymanOrthogonalGateaux (M : GeneralMoment Ω μ Z P_Z H) (D : HasDirDeriv M) (hNO : NeymanOrthogonal M D) (hEnv : DiffQuotientEnvelope M) (hMt_int : ∀ η ∈ M.H_ε, ∀ 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) : NeymanOrthogonalGateaux M := by intro η hη rw [hasDerivAt_iff_tendsto_slope_zero] simpa [div_eq_mul_inv, mul_comm] using integratedMoment_diffQuotient_tendsto_zero M D hNO hEnv hη (hMt_int η hη) hM0_int
RemainderBound 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.
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 times the product of its two seminorm distances from the true nuisance.
Definition (Lean source)
Integrated smoothness bridge to a bilinear remainder bound. For a general moment system, a directional derivative, and Neyman orthogonality, suppose the linearization residual has an integrated L² bound with constant K, the directional derivative is integrable, the baseline moment is integrable, every perturbed moment is integrable, and the true moment has mean zero. Then the population moment obeys a bilinear remainder bound. This integrated hypothesis, unlike a pointwise envelope, is directly usable for AIPW and other square-integrable scores.
Formal statement
Proof (Lean source)
DMLChernozhukov 2 core · 4 supporting This file proves the abstract one-shot double machine learning theorem in the classical Chernozhukov form. ★ oneStepOracleDML_isAsymLinear_of_goodSet
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 linearization scale, and yields asymptotic linearity with the corresponding influence function.
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 linearization scale times the evaluation-fold empirical mean of the moment at that target and the estimated nuisance.
Definition (Lean source)
Asymptotic linearity of the oracle one-step DML estimator on a nuisance good set. Take a moment system with score m, true nuisance η₀, true parameter θ₀, a set 𝒯 of admissible nuisance values, two error gauges ρ₁ and ρ₂, and a nonzero linearization scale J₀ whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split once into a training fold and an evaluation fold whose evaluation-fold share of the first n observations converges to a positive limit, and let η̂_n be the nuisance fit at sample size n. Assume for every η in 𝒯 the population moment of m(η, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η, η₀)·ρ₂(η, η₀); η̂_n falls outside 𝒯 with probability at most Δ_n, where Δ_n is a sequence of bounds that tends to zero; the map (ω, z) ↦ m(η̂_n(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the training-fold observations and the σ-algebra on the observation space; for every η in 𝒯 the score m(η, ·, θ₀) is integrable and square-integrable under the observation law; the L² distance between m(η̂_n, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and the product ρ₁(η̂_n, η₀)·ρ₂(η̂_n, η₀) is o_p(n^(−1/2)). Then the oracle one-step estimator, θ₀ minus J₀⁻¹ times the evaluation-fold average of m(η̂_n, Z_i, θ₀), is asymptotically linear at θ₀ along the evaluation fold with influence function −J₀⁻¹·m(η₀, z, θ₀).
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
oneStepOracleDML_isAsymLinear_on_highProbEventtheorem — Asymptotic linearity of the Chernozhukov DML estimator on high-probability events. Given a general moment system with mean-zero and finite-variance truth score, an i.i.d. sample and one-shot split whose evaluation fraction converges to a positive limit, nuisance fits and good events, vanishing failure bounds for those events, a remainder constant and a bilinear bound on each good event, joint and uncurried training-fold product measurability, score integrability and square-integrability on the good events, and vanishing score-difference and product rates, the one-step estimator is asymptotically linear with the inverse-scale-weighted true score.hypothesesH :sharedType u_3M :GeneralMoment Ω μ Z P_Z H_hMZ :MeanZero M_hFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit samplec :ℝ_hc_pos :0 < cη_hat :ℕ → Ω → HgoodSet :ℕ → Set ΩΔ :ℕ → ℝ≥0∞_hfail :∀ n, μ (goodSet n)ᶜ ≤ Δ nCrem :ℝ_hBR_at :_h_m_meas :∀ n, Measurable (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 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 ωifω ∈ goodSet nthenIntegrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Z_h_m_sq_int :∀ n ωifω ∈ goodSet nthenIntegrable (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 : ℝ))) μconclusionIsAsymLinear (oneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldBProof (Lean source)
theorem oneStepOracleDML_isAsymLinear_on_highProbEvent [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) (goodSet : ℕ → Set Ω) (Δ : ℕ → ℝ≥0∞) (_hΔ : Tendsto Δ atTop (𝓝 0)) (_hfail : ∀ n, μ (goodSet n)ᶜ ≤ Δ n) {Crem : ℝ} (_hBR_at : ∀ n ω, ω ∈ goodSet 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_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 ω, ω ∈ goodSet n → Integrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Z) (_h_m_sq_int : ∀ n ω, ω ∈ goodSet 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 (oneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB := by classical 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.linScaleInv ^ 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 : ℝ) * (oneStepOracleDML M sample split η_hat n ω - M.θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (-M.linScaleInv * 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_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 ω, ω ∈ goodSet n → MemLp (f n ω) 2 P_Z := by intro n ω hω have hsq := _h_m_sq_int n ω hω 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 hsq 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_of_memLp_on_highProbEvent sample split f goodSet Δ _hΔ _hfail hf_meas hf_uncurry_foldA hf_memLp hf_rate_one have h_int_eq : ∀ n ω, ω ∈ goodSet n → ∫ z, f n ω z ∂P_Z = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z := by intro n ω hω have hf_L2 := hf_memLp n ω hω have hm_int := _h_m_int n ω hω have hf_int : Integrable (f n ω) P_Z := hf_L2.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 hm_int htruth_int _ = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z := by rw [hzero] ring let mGood : ℕ → Ω → ℝ := fun n ω => if ω ∈ goodSet n then ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z else 0 have h_int_good_rate : IsLittleOp mGood (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δ filter_upwards [htarget, eventually_ge_atTop (1 : ℕ)] with n hn hn_one exact (measure_mono (by intro ω hω change ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) ≤ ‖mGood n ω‖ at hω by_cases hgood : ω ∈ goodSet n · have hbr := _hBR_at n ω hgood rw [show mGood n ω = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z by simp [mGood, hgood]] at hω rw [Real.norm_eq_abs] at 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 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 hthreshold_le_bound : ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) ≤ K * prodρ := hω.trans hKbound have hdiv_le : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / K ≤ prodρ := by rw [div_le_iff₀ hKpos] simpa [mul_comm, mul_left_comm, mul_assoc] using hthreshold_le_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_le exact hsmall · have hn_pos : 0 < (n : ℝ) := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hn_one) have hthreshold_pos : 0 < ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) := mul_pos hε (Real.rpow_pos_of_pos hn_pos _) exact False.elim ((not_le_of_gt hthreshold_pos) (by simpa [mGood, hgood, Real.norm_eq_abs] using hω)) )).trans hn have h_int_raw_rate : IsLittleOp (fun n ω => ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by apply isLittleOp_of_isLittleOp_on_highProbEvent goodSet Δ _hΔ _hfail · intro n ω hω change (∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z) = (if ω ∈ goodSet n then ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z else 0) rw [if_pos hω] · exact h_int_good_rate have h_int_rate : IsLittleOp (fun n ω => ∫ z, f n ω z ∂P_Z) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by apply isLittleOp_of_isLittleOp_on_highProbEvent goodSet Δ _hΔ _hfail · exact h_int_eq · exact h_int_raw_rate 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] -- … truncated; follow the source link for the rest … -
oneStepOracleDML_isAsymLinear_of_aetheorem — Given a moment system with its mean-zero and finite-variance conditions, a one-shot sample split with a positive limiting evaluation fraction, and nuisance fits, assume the population remainder, score integrability, and score square-integrability conditions hold almost surely, the score has joint and uncurried training-fold product measurability, and the score and product rates vanish. Then the one-step estimator is asymptotically linear.hypothesesH :sharedType u_3M :GeneralMoment Ω μ Z P_Z H_hMZ :MeanZero M_hFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit samplec :ℝ_hc_pos :0 < cη_hat :ℕ → Ω → HCrem :ℝ_hBR_at :_h_m_meas :∀ n, Measurable (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 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 : ℝ))) μconclusionIsAsymLinear (oneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldBProof (Lean source)
theorem oneStepOracleDML_isAsymLinear_of_ae [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_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 (oneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB := by let goodSet : ℕ → Set Ω := fun n => {ω | |∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z| ≤ Crem * ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ) ∧ Integrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Z ∧ Integrable (fun z => (M.m (η_hat n ω) z M.θ₀) ^ 2) P_Z} have hgood : ∀ n, ∀ᵐ ω ∂μ, ω ∈ goodSet n := by intro n filter_upwards [_hBR_at n, _h_m_int n, _h_m_sq_int n] with ω hbr hint hsq exact ⟨hbr, hint, hsq⟩ apply oneStepOracleDML_isAsymLinear_on_highProbEvent M _hMZ _hFV sample split _hc_pos _h_split_rate η_hat goodSet (fun _ => 0) tendsto_const_nhds · intro n have hz : μ (goodSet n)ᶜ = 0 := by apply ae_iff.mp filter_upwards [hgood n] with ω hω exact hω simp [hz] · intro n ω hω exact hω.1 · exact _h_m_meas · exact _h_m_foldA_uncurry · intro n ω hω exact hω.2.1 · intro n ω hω exact hω.2.2 · exact _h_score_diff_rate · exact _h_product_rate -
oneStepOracleDML_isAsymLinear_of_goodSet_aetheorem — Given the one-shot DML setup and uniform deterministic-good-set conditions, the measurability, integrability, and rate inputs used by the proof, if the nuisance fit belongs to the set almost surely at every sample size, then the one-step estimator is asymptotically linear.hypothesesH :sharedType u_3M :GeneralMoment Ω μ Z P_Z H_hMZ :MeanZero M_hFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit samplec :ℝ_hc_pos :0 < cη_hat :ℕ → Ω → HCrem :ℝ_hBR :BilinearRemainder M Crem_hT :∀ n, ∀ᵐ ω ∂μ, η_hat n ω ∈ M.H_ε_h_m_meas :∀ n, Measurable (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 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 :∀ η ∈ M.H_ε, Integrable (fun z => M.m η z M.θ₀) P_Z_h_m_sq_int :∀ η ∈ M.H_ε, Integrable (fun z => (M.m η 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 : ℝ))) μconclusionIsAsymLinear (oneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldBProof (Lean source)
theorem oneStepOracleDML_isAsymLinear_of_goodSet_ae [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 : BilinearRemainder M Crem) (_hT : ∀ n, ∀ᵐ ω ∂μ, η_hat n ω ∈ M.H_ε) (_h_m_meas : ∀ n, Measurable (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 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 : ∀ η ∈ M.H_ε, Integrable (fun z => M.m η z M.θ₀) P_Z) (_h_m_sq_int : ∀ η ∈ M.H_ε, Integrable (fun z => (M.m η 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 (oneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB := by apply oneStepOracleDML_isAsymLinear_of_goodSet M _hMZ _hFV sample split _hc_pos _h_split_rate η_hat (fun _ => 0) tendsto_const_nhds _hBR · intro n have hz : μ {ω | η_hat n ω ∉ M.H_ε} = 0 := by apply ae_iff.mp filter_upwards [_hT n] with ω hω exact hω simpa [hz] · exact _h_m_meas · exact _h_m_foldA_uncurry · exact _h_m_int · exact _h_m_sq_int · exact _h_score_diff_rate · exact _h_product_rate -
oneStepOracleDML_isAsymLinear_of_everywheretheorem — Everywhere-good one-shot DML interface. Under pointwise nuisance regularity and the remaining moment and sampling conditions, joint and uncurried product measurability, and the score and product rates, the one-step estimator is asymptotically linear.hypothesesH :sharedType u_3M :GeneralMoment Ω μ Z P_Z H_hMZ :MeanZero M_hFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit samplec :ℝ_hc_pos :0 < cη_hat :ℕ → Ω → HCrem :ℝ_hBR_at :_h_m_meas :∀ n, Measurable (fun (p : Ω × Z) => M.m (η_hat n p.1) p.2 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 : ℝ))) μconclusionIsAsymLinear (oneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldBProof (Lean source)
theorem oneStepOracleDML_isAsymLinear_of_everywhere [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_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 (oneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB := by apply oneStepOracleDML_isAsymLinear_of_ae M _hMZ _hFV sample split _hc_pos _h_split_rate η_hat · exact fun n => Filter.Eventually.of_forall (_hBR_at n) · exact _h_m_meas · exact _h_m_foldA_uncurry · exact fun n => Filter.Eventually.of_forall (_h_m_int n) · exact fun n => Filter.Eventually.of_forall (_h_m_sq_int n) · exact _h_score_diff_rate · exact _h_product_rate
Riesz 3 core · 2 supporting This file provides a mean-pairing representation assumed for maps on a regression class. ★ pairingScore_meanZero
Mean-Pairing Scores for Orthogonal Moments
This file provides a mean-pairing representation assumed for maps on a regression class. It defines the representation witness, the corresponding score, and mean-zero and bilinear-remainder identities. It does not encode linearity or continuity of the represented map.
For a regression class, its evaluation map, a real-valued map, and a covariate measure, a mean-pairing representation stores a function α₀ on the covariate space that is measurable, square-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)
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 map on regression functions, an observed-data-to-covariate map, an observed outcome map, a regression function, a pairing function, a scalar target, and an observed-data realization, the augmented pairing score is the supplied map evaluated at the regression function plus the pairing term times its observed residual, minus the target.
Definition (Lean source)
Mean-zero of the pairing score at the truth. Given a mean-pairing representation rep for 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 score pairingScore evaluated at the truth (γ₀, α₀, L γ₀) integrates to zero under P_Z:
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
α₀_integrabletheorem — On a probability space, the representer's square-integrability implies that the representer is integrable.hypothesesconclusionIntegrable rep.α₀ P_XProof (Lean source)
@[fun_prop] theorem MeanPairingRepresentation.α₀_integrable {H_γ : Type*} [AddCommGroup H_γ] [Module ℝ H_γ] {γ_target : H_γ → X → ℝ} {L : H_γ → ℝ} {P_X : Measure X} [IsProbabilityMeasure P_X] (rep : MeanPairingRepresentation H_γ γ_target L P_X) : Integrable rep.α₀ P_X := rep.α₀_memLp.integrable (by norm_num) -
pairingScore_bilinearRemtheorem — Bilinear remainder identity for the pairing score. For any perturbation (γ, α) with finite residual and product moments, the population orthogonal moment at θ₀ := L γ₀ factorises as a product of the regression error and the representer error:hypothesesX :sharedType u_3H_γ :P_X :Measure Xrep :MeanPairingRepresentation H_γ γ_target L P_Xγ₀ γ :H_γα :X → ℝproj_X :Z → XY_obs :Z → ℝh_pushforward :P_X = P_Z.map proj_Xh_proj_meas :Measurable proj_Xh_orthog_α₀ :∫ z, rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0h_orthog_α :∫ z, α (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0h_int_resid_α :Integrable (fun z => α (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z))) P_Zh_int_αγ :Integrable (fun z => α (proj_X z) * γ_target γ (proj_X z)) P_Zh_int_αγ₀ :Integrable (fun z => α (proj_X z) * γ_target γ₀ (proj_X z)) P_Zh_int_α₀γ :Integrable (fun x => rep.α₀ x * γ_target γ x) P_Xh_int_α₀γ₀ :Integrable (fun x => rep.α₀ x * γ_target γ₀ x) P_Xh_int_α :Integrable α P_Xh_int_γ :Integrable (γ_target γ) P_Xh_int_γ₀ :Integrable (γ_target γ₀) P_Xconclusion(∫ z, pairingScore γ_target L proj_X Y_obs γ α (L γ₀) z ∂P_Z)- (∫ z, pairingScore γ_target L proj_X Y_obs γ₀ rep.α₀ (L γ₀) z ∂P_Z)= - ∫ x, (α x - rep.α₀ x) * (γ_target γ x - γ_target γ₀ x) ∂P_XProof (Lean source)
theorem pairingScore_bilinearRem {H_γ : Type*} [AddCommGroup H_γ] [Module ℝ H_γ] {γ_target : H_γ → X → ℝ} {L : H_γ → ℝ} {P_X : Measure X} [IsProbabilityMeasure P_Z] (rep : MeanPairingRepresentation 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, pairingScore γ_target L proj_X Y_obs γ α (L γ₀) z ∂P_Z) - (∫ z, pairingScore γ_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, pairingScore γ_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 := pairingScore_integral_eq γ₀ γ α proj_X Y_obs h_orthog_α h_int_resid_α h_int_αγ h_int_αγ₀ have htruth : ∫ z, pairingScore γ_target L proj_X Y_obs γ₀ rep.α₀ (L γ₀) z ∂P_Z = 0 := pairingScore_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
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 oneStepOracleDML_isAsymLinear_of_everywhere to the AIPW score.
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 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)
Headline AIPW DML asymptotic-linearity theorem, derived from the abstract oneStepOracleDML_isAsymLinear_of_everywhere 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 and uncurried product-measurable. At every fold and sample point it is 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
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
aipw_meanZerotheorem — AIPW satisfies MeanZero.hypothesesγ :sharedType u_1S :ε :ℝhη₀_mem :S.η₀ ∈ H_ε_aeL2 S ε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.μconclusionMeanZero (aipwGeneralMoment S hη₀_mem)Proof (Lean source)
theorem aipw_meanZero (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.μ) : MeanZero (aipwGeneralMoment S hη₀_mem) := by unfold MeanZero aipwGeneralMoment exact aipw_mean_zero_of_square_integrable S h_overlap hA h_y2 h_yd2 -
aipw_bilinearRemtheorem — AIPW satisfies BilinearRemainder with constant aipw_rem_const ε.hypothesesγ :sharedType u_1S :ε :ℝhη₀_mem :S.η₀ ∈ H_ε_aeL2 S εh_overlap :S.StrictOverlap εhA :S.toPOBackdoorSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μh_yd2 :∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μconclusion∃ C, BilinearRemainder (aipwGeneralMoment S hη₀_mem) CProof (Lean source)
theorem aipw_bilinearRem (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.μ) (h_L2 : ∀ η ∈ H_ε_aeL2 S ε, (∀ d, MemLp (fun x => η.μ_fn d x - S.μ_val d x) 2 S.P_X) ∧ MemLp (fun x => η.e_fn x - S.e_val x) 2 S.P_X) : ∃ C, BilinearRemainder (aipwGeneralMoment S hη₀_mem) C := by refine ⟨aipw_rem_const ε, ?_⟩ intro η hη obtain ⟨hμ, hΔe⟩ := h_L2 η hη have h := BackdoorEstimationSystem.aipw_remainder_bound S h_overlap hA h_y2 h_yd2 η hη hμ hΔe -- Convert the Σ_a (‖Δμ_a‖ * ‖Δe‖) RHS shape into (‖Δμ_T‖ + ‖Δμ_F‖) * ‖Δe‖. have hsum : ∑ a : Bool, (eLpNorm (fun x => η.μ_fn a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => η.e_fn x - S.e_val x) 2 S.P_X).toReal = ((eLpNorm (fun x => η.μ_fn true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => η.μ_fn false x - S.μ_val false x) 2 S.P_X).toReal) * (eLpNorm (fun x => η.e_fn x - S.e_val x) 2 S.P_X).toReal := by rw [Fintype.sum_bool, add_mul] rw [hsum] at h -- After unfolding `M = aipwGeneralMoment`, the goal reduces to `h` -- (η₀.μ_fn = S.μ_val, η₀.e_fn = S.e_val by the constructor of η₀). change |∫ z, aipwMomentFunctional η z S.θ₀ ∂(S.P_Z)| ≤ aipw_rem_const ε * ((eLpNorm (fun x => η.μ_fn true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => η.μ_fn false x - S.μ_val false x) 2 S.P_X).toReal) * (eLpNorm (fun x => η.e_fn x - S.e_val x) 2 S.P_X).toReal linarith [h]
LinearSmoother 5 core · 1 supporting This file augments the abstract second-stage operator with auxiliary weights. ★ smoother_bias_holder★ smoother_bias_product_holder
Weighted Second-Stage Operators
This file augments the abstract second-stage operator with auxiliary weights. A separate predicate records the weighted-sum representation using explicitly supplied weights; no relation to the stored auxiliary weights is imposed.
For a randomness space with measure and a query space, a second-stage operator with weights extends the abstract second-stage operator with an unconstrained array of auxiliary weights indexed by sample size, randomness scope, query point, and data tuple. The structure does not connect these weights to the operator's evaluations.
Definition (Lean source)
Given a weighted second-stage operator, a sample size, a randomness realization, a query point, an index type and finite data fold, real weights on that index set, and the corresponding data tuples, the weighted-sum representation states that, for every real-valued pseudo-outcome function, the operator's estimate equals the weighted sum of that function over the fold.
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)
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
Proof (Lean source)
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
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
WeightedNorm_nonneglemma — The weighted norm is non-negative.Proof (Lean source)
lemma WeightedNorm_nonneg {ι : Type*} (B : Finset ι) (w : ι → ℝ) (g : ι → ℝ) (p : ℝ) : 0 ≤ WeightedNorm B w g p := by unfold WeightedNorm refine Real.rpow_nonneg ?_ _ refine Finset.sum_nonneg ?_ intro i _ refine mul_nonneg ?_ (Real.rpow_nonneg (abs_nonneg _) _) exact div_nonneg (abs_nonneg _) (Finset.sum_nonneg fun _ _ => abs_nonneg _)
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 ★ oneStepOracle_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
oneStepOracle_asymptoticLinear proves that the resulting Chernozhukov estimator
has an identically zero remainder after subtracting its influence-function
partial sum.
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 linearization scale, 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)
Algebraic identity for the scaled parametric one-step estimator. Fix a score m_par with a nonzero scale J₀, 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 scaled one-step estimator built from m_par and J₀ is asymptotically linear at θ₀ with influence function ψ(z) := −J₀⁻¹·m_par(θ₀, z).
Formal statement
Proof (Lean source)
SecondStageOperator 6 core · 0 supporting This file defines the target-agnostic second-stage operator used in DR-Learner CATE estimation. ★ isLittleOp
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-additivity predicate SecondStageOperator.IsAdditiveInInput, the oracle
estimator and oracle risk scale, the stability predicate Stable, and the
elimination lemma Stable.isLittleOp. It separates the operator itself from
additivity and conditional-bias identification assumptions.
For randomness and query spaces with a measure, an abstract second-stage regression operator stores an operator mapping a sample size, a randomness scope, a real-valued pseudo-outcome function, and a query point to an estimate, together with joint measurability for constant pseudo-outcomes. Stronger measurability and linearity are deferred to concrete instances and separate predicates.
Definition (Lean source)
For a second-stage regression operator, additivity 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. This predicate does not assert scalar homogeneity.
Definition (Lean source)
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)
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)
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)
Given a second-stage operator and all data appearing in a stability claim, stability for those data, consistency of the supplied distance, and the caller-supplied bias-identification assertion, the discrepancy in the definition of stability is little-o in probability of the oracle risk scale.