Estimation.OrthogonalMoments.AutoDebias
Automatic debiasing: Riesz-representer-based construction of orthogonal moments for linear functionals.
Linear 9 core · 2 supporting This file develops the linear core of automatic debiasing for regression-based targets. ★ linRieszScore_meanZero★ linRieszScore_directional_g_zero★ linRieszScore_directional_α_zero★ linRieszLoss_excess_eq_l2dist★ linRieszLoss_FOC_iff_representer
Automatic Debiasing for Linear Regression Functionals
This file develops the linear core of automatic debiasing for regression-based targets. It defines the regression-functional system, constructs the population linear functional and Riesz score, and proves the mean-zero, orthogonality, and Riesz-loss identities that underlie the debiased estimator.
Linear regression-functional system. Bundles an observation space with an induced regression-argument space, a regression class (a real vector space of nuisance parameters) paired with an evaluation map into the argument space, an observation-level functional linear in the nuisance argument, and a regression truth; the evaluation map is required additive and homogeneous in the nuisance argument, the observation-level functional is likewise additive and homogeneous in that argument and measurable in the observation for every fixed nuisance value, the regression-argument law is the pushforward of the observation law under the projection, and the regression residual at the truth, weighted by any measurable integrable function of the regression argument, integrates to zero.
Definition (Lean source)
For a linear regression-functional system, the population linear functional maps each regression function in that system's admissible class to the integral of its linear moment function under the system's observation measure.
Definition (Lean source)
For a linear regression-functional system, a regression function in its admissible class, a candidate Riesz representer on the covariate space, a scalar target value, and an observation, the linear Riesz score is the generic Riesz score specialized to that system's regression target, population functional, covariate projection, and observed outcome.
Definition (Lean source)
Mean-zero of the debiased linear score at the truth. Given the linear regression-functional system with Riesz representer rep, assume the α₀-weighted regression-residual product at the truth is integrable. Then the population mean of the linear Riesz score, evaluated at the true regression function and the representer's α₀, equals zero.
Formal statement
Proof (Lean source)
Directional zero in the regression direction. For a linear regression-functional system with Riesz representer and any perturbation ν_g of the regression nuisance, the Gateaux derivative of the population debiased moment in the g-direction at the truth vanishes — equivalently, this is the representer identity for the perturbation ν_g.
Formal statement
Proof (Lean source)
Directional zero in the representer direction. For any perturbation ν_α of the representer, assume ν_α is measurable and the ν_α-weighted regression-residual product at the truth is integrable. Then the population mean of the ν_α-weighted regression residual at the truth is zero.
Formal statement
Proof (Lean source)
For a linear regression-functional system and a candidate regression function in its admissible class, the linear Riesz loss is the covariate-distribution mean of the squared regression target of that function minus twice the system's population linear functional evaluated at it.
Definition (Lean source)
Excess Riesz loss equals the squared L²(P_X) distance to the representer. Let α₀_idx index the Riesz representer via rep.α₀ = γ_target α₀_idx pointwise. Assume (γ_target α) ^ 2 is integrable, (γ_target α₀_idx) ^ 2 is integrable, the product γ_target α · γ_target α₀_idx is integrable, and the squared difference (γ_target α − γ_target α₀_idx) ^ 2 is integrable. Then the excess linear Riesz loss of α over α₀_idx equals the squared L²(P_X) distance between γ_target α and γ_target α₀_idx.
Formal statement
Proof (Lean source)
First-order condition for Riesz loss minimizers (Prop 4, first half). Assume the squared regression functional along every perturbed line α₀_idx + t • ν is integrable, that the linear moment integrand m_lin(·, ν) is integrable for every direction ν, and that the product γ_target α₀_idx · γ_target ν is integrable for every direction ν. Then α₀_idx is a directional minimizer of the Riesz loss along every line through it if and only if it indexes a Riesz representer, i.e. L_of_m S ν = ∫ γ_target α₀_idx · γ_target ν dP_X for every ν.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
L_of_m_addtheorem — Additivity of L_of_m on integrable summands.hypothesesS :γ₁ γ₂ :S.H_γh₁ :Integrable (fun z => S.m_lin z γ₁) S.P_Zh₂ :Integrable (fun z => S.m_lin z γ₂) S.P_ZProof (Lean source)
theorem L_of_m_add (S : LinRegFnSys) (γ₁ γ₂ : S.H_γ) (h₁ : Integrable (fun z => S.m_lin z γ₁) S.P_Z) (h₂ : Integrable (fun z => S.m_lin z γ₂) S.P_Z) : L_of_m S (γ₁ + γ₂) = L_of_m S γ₁ + L_of_m S γ₂ := by unfold L_of_m have hpoint : (fun z => S.m_lin z (γ₁ + γ₂)) = fun z => S.m_lin z γ₁ + S.m_lin z γ₂ := by funext z; exact S.m_lin_addLeft z γ₁ γ₂ rw [hpoint]; exact integral_add h₁ h₂ -
L_of_m_smultheorem — ℝ-homogeneity of L_of_m.Proof (Lean source)
theorem L_of_m_smul (S : LinRegFnSys) (c : ℝ) (γ : S.H_γ) : L_of_m S (c • γ) = c * L_of_m S γ := by unfold L_of_m have hpoint : (fun z => S.m_lin z (c • γ)) = fun z => c * S.m_lin z γ := by funext z; exact S.m_lin_smulLeft c z γ rw [hpoint]; exact integral_const_mul c (fun z => S.m_lin z γ)
DML 4 core · 4 supporting This file instantiates the abstract Chernozhukov double machine learning framework with the linear automatic-debiasing score. ★ linAutoDML_asymptoticLinear
Automatic Debiasing DML Estimator
This file instantiates the abstract Chernozhukov double machine learning framework with the linear automatic-debiasing score. It packages the joint regression and Riesz-representer nuisance, proves reusable mean-zero and bilinear-remainder lemmas, and states an asymptotic-linearity wrapper under the abstract DML theorem's supplied hypotheses.
For a linear regression-function system, the joint nuisance object for its linear automatic-debiasing moment is a pair comprising a regression function from the system's regression class and a candidate Riesz representer, which is a real-valued function of the covariates.
Definition (Lean source)
Given a measure on the sample space, a linear regression-function system, a Riesz representation of that system's target functional, a nonnegative neighborhood radius, and measurability of the linear Riesz score for every joint nuisance and scalar target value, the linear automatic-debiasing general moment has that score, its true regression and Riesz representer as nuisance truth, and the target functional evaluated at the true regression as scalar truth.
Definition (Lean source)
Given a linear regression-function system, a Riesz representation of its target functional, a nonnegative neighborhood radius, measurability of the linear Riesz score for every joint nuisance and target value, an independent and identically distributed sample, a one-shot split of that sample, and a sequence of joint nuisance estimators indexed by sample size and randomness, the one-shot linear automatic-debiasing estimator maps each sample size and randomness realization to a real-valued estimate.
Definition (Lean source)
Linear Auto-DML asymptotic-linearity wrapper. Assume ε is nonnegative and that the linear Riesz score is measurable in the observation for every nuisance and target value. 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 Auto-DML moment has mean zero at the truth, the baseline score is square-integrable (finite variance), and 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 one-shot linear Auto-DML estimator is asymptotically linear at the target value L_of_m S S.g₀, with influence function the baseline linear Riesz score scaled by the inverse Jacobian factor, indexed over the fold-B subsample.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
instAddCommGroupinstance -
instModuleinstance -
linAuto_meanZerotheorem — Mean-zero of the linear Auto-DML moment at the truth. Specialises linRieszScore_meanZero.hypothesesΩ :Type*μ :Measure ΩS :rep :RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_Xε :ℝhε_nn :0 ≤ εh_score_meas :h_α₀_resid_int :Integrable (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_ZconclusionMeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas)Proof (Lean source)
theorem linAuto_meanZero {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : LinRegFnSys) (rep : RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (ε : ℝ) (hε_nn : 0 ≤ ε) (h_score_meas : ∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)) (h_α₀_resid_int : Integrable (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z) : MeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas) := by unfold MeanZero linAutoGeneralMoment exact linRieszScore_meanZero S rep h_α₀_resid_int -
linAuto_bilinearRemtheorem — Bilinear remainder bound for the linear Auto-DML moment.hypothesesΩ :Type*μ :Measure ΩS :rep :RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_Xε :ℝhε_nn :0 ≤ εh_score_meas :conclusion∃ C : ℝ,∀ η ∈ (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).H_ε,linAuto_int_pred S rep η → MemLp (fun x => S.γ_target η.1 x - S.γ_target S.g₀ x) 2 S.P_X → MemLp (fun x => η.2 x - rep.α₀ x) 2 S.P_X → |∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m η z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z|≤ C * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ)Proof (Lean source)
theorem linAuto_bilinearRem {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : LinRegFnSys) (rep : RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (ε : ℝ) (hε_nn : 0 ≤ ε) (h_score_meas : ∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)) : ∃ C : ℝ, ∀ η ∈ (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).H_ε, linAuto_int_pred S rep η → MemLp (fun x => S.γ_target η.1 x - S.γ_target S.g₀ x) 2 S.P_X → MemLp (fun x => η.2 x - rep.α₀ x) 2 S.P_X → |∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m η z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z| ≤ C * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) := by refine ⟨1, ?_⟩ intro η _ h_int hγ hα rcases h_int with ⟨h_int_resid_α, h_int_αγ, h_int_αγ₀, h_int_α₀γ, h_int_α₀γ₀, h_int_α, h_int_γ, h_int_γ₀, h_int_resid_α₀, h_orthog_α⟩ let dα : S.X → ℝ := fun x => η.2 x - rep.α₀ x let dγ : S.X → ℝ := fun x => S.γ_target η.1 x - S.γ_target S.g₀ x have h_orthog_α₀ : ∫ z, rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) ∂S.P_Z = 0 := S.regression_resid_orthog rep.α₀ rep.α₀_meas h_int_resid_α₀ have hrem_sub : (∫ z, linRieszScore S η.1 η.2 (L_of_m S S.g₀) z ∂S.P_Z) - (∫ z, linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z ∂S.P_Z) = -∫ x, dα x * dγ x ∂S.P_X := by unfold linRieszScore dα dγ exact Causalean.Estimation.OrthogonalMoments.rieszScore_bilinearRem rep S.g₀ η.1 η.2 S.proj_X S.Y_obs S.pushforward S.proj_X_meas h_orthog_α₀ h_orthog_α h_int_resid_α h_int_αγ h_int_αγ₀ h_int_α₀γ h_int_α₀γ₀ h_int_α h_int_γ h_int_γ₀ have htruth : ∫ z, linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z ∂S.P_Z = 0 := linRieszScore_meanZero S rep h_int_resid_α₀ have hrem : ∫ z, linRieszScore S η.1 η.2 (L_of_m S S.g₀) z ∂S.P_Z = -∫ x, dα x * dγ x ∂S.P_X := by simpa [htruth] using hrem_sub have h_abs_rewrite : |∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m η z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z| = |∫ x, dα x * dγ x ∂S.P_X| := by rw [show (∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m η z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z) = ∫ z, linRieszScore S η.1 η.2 (L_of_m S S.g₀) z ∂S.P_Z by rfl] rw [hrem, abs_neg] have h_abs_int : |∫ x, dα x * dγ x ∂S.P_X| ≤ ∫ x, |dα x * dγ x| ∂S.P_X := MeasureTheory.abs_integral_le_integral_abs have hcs : ∫ x, |dα x * dγ x| ∂S.P_X ≤ (eLpNorm dα 2 S.P_X).toReal * (eLpNorm dγ 2 S.P_X).toReal := by simpa [dα, dγ, abs_mul] using (integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := S.P_X) (f := dα) (g := dγ) hα hγ) have hfin : (eLpNorm dα 2 S.P_X).toReal * (eLpNorm dγ 2 S.P_X).toReal = 1 * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) := by simp [linAutoGeneralMoment, dα, dγ, mul_comm] rfl exact h_abs_rewrite.trans_le ((h_abs_int.trans hcs).trans (le_of_eq hfin))
General 9 core · 0 supporting This file extends the automatic-debiasing construction from linear regression functionals to general scalar moment equations with a regression nuisance. ★ autoDebiasedMoment_meanZero_at_truth★ autoDebiasedMoment_directional_g_zero★ autoDebiasedMoment_directional_α_zero
Automatic Debiasing for General Moments
This file extends the automatic-debiasing construction from linear regression functionals to general scalar moment equations with a regression nuisance. It packages the moment system, the Riesz-representer correction, and the resulting orthogonality identities used to build debiased scores, together with population and finite-difference Riesz objectives for representer fitting.
Regression-nuisance moment system. Bundles an observation space with an induced covariate space, an outcome variable, a regression target functional on a normed nuisance class, the true nuisance and true scalar parameter, a population moment functional of the parameter and nuisance, and an observation-level moment kernel that averages to it; the regression target is required additive and homogeneous in its nuisance argument, the population moment vanishes at the truth, the supplied Gateaux derivative of the moment at the truth is itself additive and homogeneous, the kernel is measurable and integrates against the observation measure to the population moment, the covariate measure is the pushforward of the observation measure under the projection, and the regression residual at the truth, weighted by any measurable integrable function of the covariates, integrates to zero.
Definition (Lean source)
Automatic debiasing representer. For a regression-nuisance moment system, a function α₀ on the covariate space that is measurable and integrable against the covariate measure, and that represents the Gateaux derivative of the population moment at the truth, in every direction, as the L²-inner product of α₀ against the regression target evaluated in that direction.
Definition (Lean source)
For a regression-nuisance moment system, a regression nuisance function, a candidate representer on the covariate space, a scalar target value, and an observation, the automatically debiased score is the baseline moment contribution plus the candidate representer evaluated at the observation's covariates times the observed-outcome residual from the regression target.
Definition (Lean source)
For a regression-nuisance moment system, a regression nuisance function, a candidate representer on the covariate space, and a scalar target value, the automatically debiased population moment is the expectation of the automatically debiased score under the system's observation distribution.
Definition (Lean source)
Mean-zero of the debiased moment at the truth. Given a regression-nuisance moment system with representer rep, assume the α₀-weighted regression-residual product at the truth is integrable and the baseline moment integrand at the truth is integrable. Then the automatically debiased population moment, evaluated at the true nuisance and true parameter, equals zero.
Formal statement
Proof (Lean source)
Directional zero in the regression direction. For a regression-nuisance moment system with Riesz representer and any perturbation ν_g of the regression nuisance, the Gateaux derivative of the population debiased moment in the g-direction at the truth vanishes — equivalently, this is the representer identity for the perturbation ν_g.
Formal statement
Proof (Lean source)
Directional zero in the representer direction. For any perturbation ν_α of the representer, assume ν_α is measurable and the ν_α-weighted regression-residual product at the truth is integrable. Then the directional derivative of the population debiased moment in the α-direction at the truth vanishes: the integral of the weighted regression residual is zero.
Formal statement
Proof (Lean source)
For a regression-nuisance moment system and a candidate regression function in its nuisance class, the general Riesz loss is the covariate-distribution mean of the squared regression target of that function minus twice the directional derivative of the population moment in that function's direction.
Definition (Lean source)
For a regression-nuisance moment system, a sample-indexed auxiliary sample space, observation-valued sample data, sample-indexed target estimates, sample-indexed nuisance estimates, finite-difference scales, a candidate nuisance-direction function, sample-index sets, a sample size, and a realized auxiliary sample point, the finite-difference representer loss is the empirical second moment of the candidate's regression target on the specified index set minus twice the centered finite-difference approximation to the moment's nuisance derivative at the corresponding estimates.