Estimation.OrthogonalMoments.AutoDebias
Automatic debiasing: Riesz-representer-based construction of orthogonal moments for linear functionals.
General 9 core · 2 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 mean-pairing 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 and measurable, the population moment vanishes at the truth, the supplied Gateaux derivative of the moment at the truth is the actual derivative of the population moment along every nuisance direction, 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)
For a regression-nuisance moment system, an automatic-debiasing mean-pairing witness stores 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 integral pairing 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)
Neyman orthogonality in the regression direction. For a regression-nuisance moment system with a mean-pairing witness and a perturbation ν_g, if the moment path is integrable, the baseline correction is integrable, and the directional correction is integrable, then the Gateaux derivative of the auto-debiased population moment along g₀ + rν_g exists at zero and equals zero. This is the genuine Chernozhukov--Newey--Singh (2022) Neyman-orthogonality statement: the derivative link in RegNuisanceMomentSys.D_g_M_hasDerivAt and the stored pairing identity cancel the two path derivatives.
Formal statement
Proof (Lean source)
Neyman orthogonality in the representer direction. For a regression-nuisance moment system with a mean-pairing witness and a representer perturbation ν_α, assume ν_α is measurable, the baseline score is integrable, and the directional residual correction is integrable. Then the derivative of the automatically debiased moment along α₀ + rν_α exists at zero and equals 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.
Definition (Lean source)
2 supporting declarations (lemmas, instances)
-
D_g_M_smultheorem — For a regression-nuisance moment system, a scalar, and a nuisance direction, the supplied nuisance derivative is homogeneous in its direction. This is derived from uniqueness of the one-dimensional derivative rather than stored as an independent structure field.Proof (Lean source)
theorem RegNuisanceMomentSys.D_g_M_smul (S : RegNuisanceMomentSys) (c : ℝ) (ν : S.H) : S.D_g_M (c • ν) = c * S.D_g_M ν := by have hc : HasDerivAt (fun r : ℝ => r * c) c 0 := by simpa using (hasDerivAt_id (0 : ℝ)).mul_const c have hcomp : HasDerivAt ((fun q : ℝ => S.M S.θ₀ (S.g₀ + q • ν)) ∘ fun r : ℝ => r * c) (S.D_g_M ν * c) 0 := _root_.HasDerivAt.comp_of_eq (𝕜 := ℝ) (𝕜' := ℝ) (h := fun r : ℝ => r * c) (h₂ := fun q : ℝ => S.M S.θ₀ (S.g₀ + q • ν)) (y := 0) 0 (S.D_g_M_hasDerivAt ν) hc (by ring) have hcomp' : HasDerivAt (fun r : ℝ => S.M S.θ₀ (S.g₀ + (r * c) • ν)) (c * S.D_g_M ν) 0 := by change HasDerivAt (fun r : ℝ => S.M S.θ₀ (S.g₀ + (r * c) • ν)) (S.D_g_M ν * c) 0 at hcomp simpa only [mul_comm] using hcomp have heq : (fun r : ℝ => S.M S.θ₀ (S.g₀ + r • (c • ν))) = fun r : ℝ => S.M S.θ₀ (S.g₀ + (r * c) • ν) := by funext r rw [smul_smul] exact (S.D_g_M_hasDerivAt (c • ν)).unique <| by rw [heq] exact hcomp' -
autoDebiasedMoment_directional_zerotheorem — Joint Neyman orthogonality. For a regression-nuisance moment system with a mean-pairing witness, a regression direction, and a measurable representer direction, assume integrability of the moment path and all first- and second-order correction terms. Then the automatically debiased moment has derivative zero when both nuisances move simultaneously along (ν_g,ν_α).hypothesesrep :ν_g :S.Hν_α :S.X → ℝhν_α_meas :Measurable ν_αh_m_int :∀ r : ℝ, Integrable (fun z => S.m (S.g₀ + r • ν_g) z S.θ₀) S.P_Zh_resid_int :Integrable (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Zh_g_dir_int :Integrable (fun z => rep.α₀ (S.proj_X z) * S.γ_target ν_g (S.proj_X z)) S.P_Zh_α_dir_int :Integrable (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Zh_cross_int :Integrable (fun z => ν_α (S.proj_X z) * S.γ_target ν_g (S.proj_X z)) S.P_ZconclusionHasDerivAt (fun r : ℝ => autoDebiasedMoment S (S.g₀ + r • ν_g) (fun x => rep.α₀ x + r * ν_α x) S.θ₀) 0 0Proof (Lean source)
theorem autoDebiasedMoment_directional_zero (S : RegNuisanceMomentSys) (rep : AutoDebiasMeanRepresentation S) (ν_g : S.H) (ν_α : S.X → ℝ) (hν_α_meas : Measurable ν_α) (h_m_int : ∀ r : ℝ, Integrable (fun z => S.m (S.g₀ + r • ν_g) z S.θ₀) S.P_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) (h_g_dir_int : Integrable (fun z => rep.α₀ (S.proj_X z) * S.γ_target ν_g (S.proj_X z)) S.P_Z) (h_α_dir_int : Integrable (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z) (h_cross_int : Integrable (fun z => ν_α (S.proj_X z) * S.γ_target ν_g (S.proj_X z)) S.P_Z) : HasDerivAt (fun r : ℝ => autoDebiasedMoment S (S.g₀ + r • ν_g) (fun x => rep.α₀ x + r * ν_α x) S.θ₀) 0 0 := by have hg := autoDebiasedMoment_directional_g_zero S rep ν_g h_m_int h_resid_int h_g_dir_int have hαzero : ∫ z, ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) ∂S.P_Z = 0 := S.regression_resid_orthog ν_α hν_α_meas h_α_dir_int let K : ℝ := ∫ z, ν_α (S.proj_X z) * S.γ_target ν_g (S.proj_X z) ∂S.P_Z have hfun : (fun r : ℝ => autoDebiasedMoment S (S.g₀ + r • ν_g) (fun x => rep.α₀ x + r * ν_α x) S.θ₀) = fun r : ℝ => autoDebiasedMoment S (S.g₀ + r • ν_g) rep.α₀ S.θ₀ - r ^ 2 * K := by funext r have hαpath : (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z))) = (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) - r * (ν_α (S.proj_X z) * S.γ_target ν_g (S.proj_X z))) := by funext z rw [S.γ_target_add, S.γ_target_smul] ring have hαpath_int : Integrable (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z))) S.P_Z := by rw [hαpath] exact h_α_dir_int.sub (h_cross_int.const_mul r) have hαint : ∫ z, ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z)) ∂S.P_Z = -r * K := by rw [hαpath, integral_sub h_α_dir_int (h_cross_int.const_mul r), integral_const_mul, hαzero] simp [K] have hg_corr_int : Integrable (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z))) S.P_Z := by rw [show (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z))) = (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) - r * (rep.α₀ (S.proj_X z) * S.γ_target ν_g (S.proj_X z))) by funext z rw [S.γ_target_add, S.γ_target_smul] ring] exact h_resid_int.sub (h_g_dir_int.const_mul r) unfold autoDebiasedMoment autoDebiasedScore calc _ = ∫ z, (S.m (S.g₀ + r • ν_g) z S.θ₀ + rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z))) + r * (ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z))) ∂S.P_Z := by apply integral_congr_ae filter_upwards with z ring _ = (∫ z, S.m (S.g₀ + r • ν_g) z S.θ₀ + rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z)) ∂S.P_Z) + ∫ z, r * (ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z))) ∂S.P_Z := integral_add ((h_m_int r).add hg_corr_int) (hαpath_int.const_mul r) _ = (∫ z, S.m (S.g₀ + r • ν_g) z S.θ₀ + rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z)) ∂S.P_Z) + r * (-r * K) := by rw [integral_const_mul, hαint] _ = _ := by ring rw [hfun] have hquad : HasDerivAt (fun r : ℝ => r ^ 2 * K) 0 0 := by simpa [pow_two] using ((hasDerivAt_id (0 : ℝ)).mul (hasDerivAt_id (0 : ℝ))).mul_const K have hsub := hg.sub hquad change HasDerivAt (fun r : ℝ => autoDebiasedMoment S (S.g₀ + r • ν_g) rep.α₀ S.θ₀ - r ^ 2 * K) (0 - 0) 0 at hsub simpa using hsub
Linear 10 core · 6 supporting This file develops the linear core of automatic debiasing for regression-based targets. ★ linRieszScore_directional_g_zero★ linRieszLoss_excess_eq_l2dist★ linRieszLoss_representer_is_globalMinimizer
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 pairing 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 pairing function on the covariate space, a scalar target value, and an observation, the observation-level pairing score adds the observed linear functional to the pairing-weighted regression residual and subtracts the target.
Definition (Lean source)
For a linear regression-functional system, its mean-pairing representation, and an observation, the full automatic-debiasing influence function is the observed target fluctuation m(W;g₀)-θ₀ plus the representer-weighted regression residual α₀(X)(Y-g₀(X)).
Definition (Lean source)
Directional zero in the regression direction. For a linear regression-functional system with a mean-pairing witness 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)
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)
For a linear regression-functional system, sample data, a candidate representer index, training indices, a sample-size index, and a sample realization, the empirical linear Riesz loss averages the candidate's squared value minus twice its observed linear functional over the training indices.
Definition (Lean source)
Given a linear regression-functional system, sample data, a candidate class, training indices, and a sample-indexed fitted representer, the empirical-Riesz-minimizer property says that each fit belongs to the class and has no larger empirical Riesz loss than any other class member.
Definition (Lean source)
Excess Riesz loss equals the squared L²(P_X) distance to the representer. Let α₀_idx index the pairing function 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)
For a linear regression-functional system, a candidate index of the population pairing function, and a mean-pairing representation, suppose the representation is pointwise indexed by that candidate, every candidate's evaluated target is strongly measurable, and every candidate has finite squared risk. Then the indexed representer globally minimizes the population linear Riesz loss; product and squared-distance integrability follow by L² Cauchy–Schwarz and closure.
Formal statement
Proof (Lean source)
6 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 γ) -
linRieszScore_truth_eq_influencetheorem — For a linear regression-functional system, its mean-pairing representation, and an observation, the truth-evaluated pairing score equals the full automatic-debiasing influence function.hypothesesconclusionProof (Lean source)
@[simp] theorem linRieszScore_truth_eq_influence (S : LinRegFnSys) (rep : MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (z : S.Z) : linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z = linAutoInfluence S rep z := by simp [linRieszScore, linAutoInfluence] ring -
linRieszScore_meanZerotheorem — For a linear regression-functional system and its mean-pairing representation, assume the α₀-weighted regression residual is integrable and the observed linear functional at the truth is integrable. Then the population mean of the observation-level pairing score at the truth is zero.hypothesesS :rep :MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_Xh_α₀_resid_int :Integrable (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Zh_m_lin_int :Integrable (fun z => S.m_lin z S.g₀) S.P_Zconclusion∫ z, linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z ∂S.P_Z = 0Proof (Lean source)
theorem linRieszScore_meanZero (S : LinRegFnSys) (rep : MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (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) (h_m_lin_int : Integrable (fun z => S.m_lin z S.g₀) S.P_Z) : ∫ z, linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z ∂S.P_Z = 0 := by let r : S.Z → ℝ := fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) have hr_int : Integrable r S.P_Z := h_α₀_resid_int have hresid : ∫ z, r z ∂S.P_Z = 0 := S.regression_resid_orthog rep.α₀ rep.α₀_meas h_α₀_resid_int change ∫ z, (S.m_lin z S.g₀ + r z) - L_of_m S S.g₀ ∂S.P_Z = 0 calc _ = (∫ z, S.m_lin z S.g₀ + r z ∂S.P_Z) - ∫ _ : S.Z, L_of_m S S.g₀ ∂S.P_Z := by exact integral_sub (h_m_lin_int.add hr_int) (integrable_const _) _ = ((∫ z, S.m_lin z S.g₀ ∂S.P_Z) + ∫ z, r z ∂S.P_Z) - ∫ _ : S.Z, L_of_m S S.g₀ ∂S.P_Z := by rw [integral_add h_m_lin_int hr_int] _ = 0 := by simp [hresid, L_of_m] -
linRieszScore_directional_α_zerotheorem — 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.hypothesesS :ν_α :S.X → ℝhν_α_meas :Measurable ν_αh_int :Integrable (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Zconclusion∫ z, ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) ∂S.P_Z = 0Proof (Lean source)
theorem linRieszScore_directional_α_zero (S : LinRegFnSys) (ν_α : S.X → ℝ) (hν_α_meas : Measurable ν_α) (h_int : Integrable (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z) : ∫ z, ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) ∂S.P_Z = 0 := by exact S.regression_resid_orthog ν_α hν_α_meas h_int -
linRieszLoss_FOC_iff_representertheorem — 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 pairing function, i.e. L_of_m S ν = ∫ γ_target α₀_idx · γ_target ν dP_X for every ν.hypothesesS :α₀_idx :S.H_γh_int_quad :∀ ν : S.H_γ, ∀ t : ℝ, Integrable (fun x => (S.γ_target (α₀_idx + t • ν) x) ^ 2) S.P_Xh_int_L :∀ ν : S.H_γ, Integrable (fun z => S.m_lin z ν) S.P_Zh_int_α₀ν_X :∀ ν : S.H_γ, Integrable (fun x => S.γ_target α₀_idx x * S.γ_target ν x) S.P_Xconclusion(∀ ν : S.H_γ, ∀ t : ℝ, linRieszLoss S α₀_idx ≤ linRieszLoss S (α₀_idx + t • ν))↔ (∀ ν : S.H_γ, L_of_m S ν = ∫ x, S.γ_target α₀_idx x * S.γ_target ν x ∂S.P_X)Proof (Lean source)
theorem linRieszLoss_FOC_iff_representer (S : LinRegFnSys) (α₀_idx : S.H_γ) (h_int_quad : ∀ ν : S.H_γ, ∀ t : ℝ, Integrable (fun x => (S.γ_target (α₀_idx + t • ν) x) ^ 2) S.P_X) (h_int_L : ∀ ν : S.H_γ, Integrable (fun z => S.m_lin z ν) S.P_Z) (h_int_α₀ν_X : ∀ ν : S.H_γ, Integrable (fun x => S.γ_target α₀_idx x * S.γ_target ν x) S.P_X) : (∀ ν : S.H_γ, ∀ t : ℝ, linRieszLoss S α₀_idx ≤ linRieszLoss S (α₀_idx + t • ν)) ↔ (∀ ν : S.H_γ, L_of_m S ν = ∫ x, S.γ_target α₀_idx x * S.γ_target ν x ∂S.P_X) := by have hloss : ∀ ν : S.H_γ, ∀ t : ℝ, linRieszLoss S (α₀_idx + t • ν) - linRieszLoss S α₀_idx = 2 * t * ((∫ x, S.γ_target α₀_idx x * S.γ_target ν x ∂S.P_X) - L_of_m S ν) + t ^ 2 * (∫ x, (S.γ_target ν x) ^ 2 ∂S.P_X) := by intro ν t have hα₀2 : Integrable (fun x => (S.γ_target α₀_idx x) ^ 2) S.P_X := by simpa using h_int_quad ν 0 have hν2 : Integrable (fun x => (S.γ_target ν x) ^ 2) S.P_X := by have hsum : Integrable (fun x => (S.γ_target α₀_idx x) ^ 2 + 2 * (S.γ_target α₀_idx x * S.γ_target ν x) + (S.γ_target ν x) ^ 2) S.P_X := by refine (h_int_quad ν 1).congr ?_; filter_upwards with x rw [S.γ_target_add, S.γ_target_smul]; ring have hbase : Integrable (fun x => (S.γ_target α₀_idx x) ^ 2 + 2 * (S.γ_target α₀_idx x * S.γ_target ν x)) S.P_X := hα₀2.add ((h_int_α₀ν_X ν).const_mul 2) refine (hsum.sub hbase).congr ?_ filter_upwards with x change ((S.γ_target α₀_idx x) ^ 2 + 2 * (S.γ_target α₀_idx x * S.γ_target ν x) + (S.γ_target ν x) ^ 2 - ((S.γ_target α₀_idx x) ^ 2 + 2 * (S.γ_target α₀_idx x * S.γ_target ν x))) = (S.γ_target ν x) ^ 2 ring have hsq : (∫ x, (S.γ_target (α₀_idx + t • ν) x) ^ 2 ∂S.P_X) = (∫ x, (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) + 2 * t * (∫ x, S.γ_target α₀_idx x * S.γ_target ν x ∂S.P_X) + t ^ 2 * (∫ x, (S.γ_target ν x) ^ 2 ∂S.P_X) := by have hpoint : (fun x => (S.γ_target (α₀_idx + t • ν) x) ^ 2) = fun x => (S.γ_target α₀_idx x) ^ 2 + (2 * t) * (S.γ_target α₀_idx x * S.γ_target ν x) + t ^ 2 * (S.γ_target ν x) ^ 2 := by funext x; rw [S.γ_target_add, S.γ_target_smul]; ring rw [hpoint] calc (∫ x, (S.γ_target α₀_idx x) ^ 2 + (2 * t) * (S.γ_target α₀_idx x * S.γ_target ν x) + t ^ 2 * (S.γ_target ν x) ^ 2 ∂S.P_X) = (∫ x, ((S.γ_target α₀_idx x) ^ 2 + (2 * t) * (S.γ_target α₀_idx x * S.γ_target ν x)) + t ^ 2 * (S.γ_target ν x) ^ 2 ∂S.P_X) := by apply integral_congr_ae; filter_upwards with x; ring _ = (∫ x, (S.γ_target α₀_idx x) ^ 2 + (2 * t) * (S.γ_target α₀_idx x * S.γ_target ν x) ∂S.P_X) + (∫ x, t ^ 2 * (S.γ_target ν x) ^ 2 ∂S.P_X) := by exact integral_add (hα₀2.add ((h_int_α₀ν_X ν).const_mul (2 * t))) (hν2.const_mul (t ^ 2)) _ = ((∫ x, (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) + (∫ x, (2 * t) * (S.γ_target α₀_idx x * S.γ_target ν x) ∂S.P_X)) + (∫ x, t ^ 2 * (S.γ_target ν x) ^ 2 ∂S.P_X) := by rw [integral_add hα₀2 ((h_int_α₀ν_X ν).const_mul (2 * t))] _ = (∫ x, (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) + 2 * t * (∫ x, S.γ_target α₀_idx x * S.γ_target ν x ∂S.P_X) + t ^ 2 * (∫ x, (S.γ_target ν x) ^ 2 ∂S.P_X) := by rw [integral_const_mul, integral_const_mul] unfold linRieszLoss; rw [hsq] rw [L_of_m_add S α₀_idx (t • ν) (h_int_L α₀_idx) (h_int_L (t • ν)), L_of_m_smul S t ν]; ring constructor · intro hmin ν let b : ℝ := (∫ x, S.γ_target α₀_idx x * S.γ_target ν x ∂S.P_X) - L_of_m S ν let a : ℝ := ∫ x, (S.γ_target ν x) ^ 2 ∂S.P_X have ha : 0 ≤ a := by dsimp [a]; exact integral_nonneg (fun x => sq_nonneg (S.γ_target ν x)) have hquad : ∀ t : ℝ, 0 ≤ 2 * t * b + t ^ 2 * a := by intro t; dsimp [a, b]; linarith [hmin ν t, hloss ν t] have hb := linear_coeff_eq_zero_of_quad_nonneg ha hquad; dsimp [b] at hb; linarith · intro hrep ν t have hb : (∫ x, S.γ_target α₀_idx x * S.γ_target ν x ∂S.P_X) - L_of_m S ν = 0 := by rw [← hrep ν]; simp rw [← sub_nonneg, hloss ν t, hb] simpa using mul_nonneg (sq_nonneg t) (integral_nonneg (fun x => sq_nonneg (S.γ_target ν x)))
DML 7 core · 7 supporting This file instantiates K-fold affine-score DML with the observation-level automatic-debiasing score. ★ linAutoDML_asymptoticLinear★ linAutoDML_tendstoNormal
Feasible Automatic Debiasing by Cross-Fitting
This file instantiates K-fold affine-score DML with the observation-level
automatic-debiasing score. Each evaluation fold uses a regression fit and a
Riesz fit trained on its complement. The resulting statistic is feasible: its
constant term is m(W; ĝ) + α̂(X)(Y - ĝ(X)), not the population functional
L(ĝ). The main theorem derives the full influence function and the normal
limit follows from the library's asymptotic-linearity CLT.
For a linear regression-function system, the joint nuisance object for feasible automatic debiasing pairs a regression-function index with a candidate pairing function on the covariate space.
Definition (Lean source)
Given an auxiliary sample-space measure, a linear regression-functional system, its mean-pairing representation, a nonnegative nuisance-neighborhood radius, and measurability of every observation-level score, the affine automatic-debiasing moment has coefficient minus one and observed constant term m(W;γ) + α(X)(Y-γ(X)).
Definition (Lean source)
Under the same inputs as the affine automatic-debiasing moment, the corresponding general moment forgets only the affine decomposition.
Definition (Lean source)
For a linear regression-functional system, its mean-pairing representation, and a joint nuisance candidate, the integrability and representer-measurability package used by the bilinear remainder contains the finite population moments needed to compare observed and population scores; the regression equation then supplies residual orthogonality.
Definition (Lean source)
Given a linear regression-functional system, its mean-pairing representation, and score regularity inputs, an i.i.d. sample, a K-fold split, and fold-specific regression fits and Riesz fits, the feasible cross-fitted automatic-debiasing estimator solves the fold-averaged empirical score equation.
Definition (Lean source)
For a linear regression-functional system, its mean-pairing representation, and score regularity inputs, an i.i.d. sample, K-fold split, and fold-specific regression and pairing-function fits, under at least two folds, mean zero and finite variance, foldwise neighborhood, integrability, and square-integrability conditions, the joint and uncurried cross-fit measurability and moment conditions, uniform L² score stability, L² consistency of the regression fit, L² consistency of the fitted pairing function, the parametric product rate, and influence and oracle measurability, the feasible K-fold automatic-debiasing estimator is asymptotically linear with the full influence function.
Formal statement
Proof (Lean source)
For a linear regression-functional system, its mean-pairing representation, and its affine score regularity inputs, an i.i.d. sample and K-fold split, and fold-specific regression and pairing-function fits, if the resulting feasible estimator has the full observation-level asymptotic-linear expansion, its influence function is measurable, and its √n-scaled error is almost-everywhere measurable, then that scaled error converges to a centered Gaussian law whose variance is the second moment of the full influence function.
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
instAddCommGroupinstance — A linear regression function system gives its linear automatic-debiasing nuisance space an additive commutative group structure. -
instModuleinstance — A linear regression function system gives its linear automatic-debiasing nuisance space the pointwise real module structure. -
linAuto_meanZerotheorem — Given the automatic-debiasing system, representation, neighborhood, and score regularity inputs, an integrable observed linear functional at the truth, and an integrable representer-weighted truth residual, the observation-level automatic-debiasing moment is mean zero at the truth.hypothesesΩ :Type*μ :Measure ΩS :rep :MeanPairingRepresentation 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_Zh_m_lin_int :Integrable (fun z => S.m_lin z S.g₀) S.P_ZconclusionMeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas)Proof (Lean source)
theorem linAuto_meanZero {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : LinRegFnSys) (rep : MeanPairingRepresentation 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) (h_m_lin_int : Integrable (fun z => S.m_lin z S.g₀) S.P_Z) : MeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas) := by unfold MeanZero linAutoGeneralMoment exact linRieszScore_meanZero S rep h_α₀_resid_int h_m_lin_int -
linAuto_bilinearRemtheorem — Given the automatic-debiasing system, representation, neighborhood, and score regularity inputs, the absolute population score remainder is bounded by the product of its L² regression and Riesz errors whenever the displayed candidate satisfies the stated integrability, measurability, and L² conditions.hypothesesΩ :Type*μ :Measure ΩS :rep :MeanPairingRepresentation 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 : MeanPairingRepresentation 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η_mem h_int hγ hα change |∫ z, linRieszScore S η.1 η.2 (L_of_m S S.g₀) z ∂S.P_Z| ≤ 1 * (eLpNorm (fun x => S.γ_target η.1 x - S.γ_target S.g₀ x) 2 S.P_X).toReal * (eLpNorm (fun x => η.2 x - rep.α₀ x) 2 S.P_X).toReal exact linAuto_bilinearRem_one μ S rep ε hε_nn h_score_meas η hη_mem h_int hγ hα -
linAuto_bilinearRem_attheorem — Given the automatic-debiasing inputs and foldwise fits, if every fitted pair lies in the nuisance neighborhood, satisfies the population integrability package, and has square-integrable regression and Riesz errors, then the population score remainder obeys the bilinear bound with explicit constant one for every sample size, fold, and realization.hypothesesΩ :Type*μ :Measure ΩS :rep :MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_Xε :ℝhε_nn :0 ≤ εh_score_meas :K :ℕg_hat :ℕ → Fin K → Ω → S.H_γα_hat :ℕ → Fin K → Ω → S.X → ℝhη_mem :∀ n k ω,(g_hat n k ω, α_hat n k ω) ∈ (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).H_εh_int :∀ n k ω, linAuto_int_pred S rep (g_hat n k ω, α_hat n k ω)hγ :∀ n k ω, MemLp (fun x => S.γ_target (g_hat n k ω) x - S.γ_target S.g₀ x) 2 S.P_Xhα :∀ n k ω, MemLp (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_Xn k ω :Proof (Lean source)
theorem linAuto_bilinearRem_at {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : LinRegFnSys) (rep : MeanPairingRepresentation 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)) {K : ℕ} (g_hat : ℕ → Fin K → Ω → S.H_γ) (α_hat : ℕ → Fin K → Ω → S.X → ℝ) (hη_mem : ∀ n k ω, (g_hat n k ω, α_hat n k ω) ∈ (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).H_ε) (h_int : ∀ n k ω, linAuto_int_pred S rep (g_hat n k ω, α_hat n k ω)) (hγ : ∀ n k ω, MemLp (fun x => S.γ_target (g_hat n k ω) x - S.γ_target S.g₀ x) 2 S.P_X) (hα : ∀ n k ω, MemLp (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X) : ∀ n k ω, |∫ z, linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z ∂S.P_Z| ≤ 1 * (eLpNorm (fun x => S.γ_target (g_hat n k ω) x - S.γ_target S.g₀ x) 2 S.P_X).toReal * (eLpNorm (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X).toReal := by intro n k ω exact linAuto_bilinearRem_one μ S rep ε hε_nn h_score_meas (g_hat n k ω, α_hat n k ω) (hη_mem n k ω) (h_int n k ω) (hγ n k ω) (hα n k ω) -
linAutoDMLEstimator_eq_foldAveragetheorem — For a linear regression-functional system, its mean-pairing representation, and score regularity inputs, an i.i.d. sample with a K-fold split and fold-specific nuisance fits, a positive number of folds, a sample-size index, a sample realization, and nonempty evaluation folds, the estimator equals the average of the foldwise observed automatic-debiasing scores.hypothesesΩ :S :rep :MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_Xε :ℝhε_nn :0 ≤ εh_score_meas :sample :IIDSample Ω S.Z μ S.P_ZK :ℕhK_pos :0 < Ksplit :KFoldSplit sample Kg_hat :ℕ → Fin K → Ω → S.H_γα_hat :ℕ → Fin K → Ω → S.X → ℝn :ℕω :Ωhfold :∀ k, (split.fold n k).NonemptyconclusionlinAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat n ω= (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, (S.m_lin (sample.Z i ω) (g_hat n k ω) + α_hat n k ω (S.proj_X (sample.Z i ω)) * (S.Y_obs (sample.Z i ω) - S.γ_target (g_hat n k ω) (S.proj_X (sample.Z i ω))))Proof (Lean source)
theorem linAutoDMLEstimator_eq_foldAverage {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} (S : LinRegFnSys) (rep : MeanPairingRepresentation 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)) (sample : IIDSample Ω S.Z μ S.P_Z) {K : ℕ} (hK_pos : 0 < K) (split : KFoldSplit sample K) (g_hat : ℕ → Fin K → Ω → S.H_γ) (α_hat : ℕ → Fin K → Ω → S.X → ℝ) (n : ℕ) (ω : Ω) (hfold : ∀ k, (split.fold n k).Nonempty) : linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat n ω = (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, (S.m_lin (sample.Z i ω) (g_hat n k ω) + α_hat n k ω (S.proj_X (sample.Z i ω)) * (S.Y_obs (sample.Z i ω) - S.γ_target (g_hat n k ω) (S.proj_X (sample.Z i ω)))) := by have hcoeff : ∀ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, (-1 : ℝ) = -1 := by intro k have hcard : ((split.fold n k).card : ℝ) ≠ 0 := by exact_mod_cast Finset.card_ne_zero.mpr (hfold k) rw [Finset.sum_const] simp [nsmul_eq_mul, hcard] unfold linAutoDMLEstimator feasibleCrossFitLinearDML simp only [linAutoLinearMoment] rw [Finset.sum_congr rfl (fun k _ => hcoeff k)] have hKne : (K : ℝ) ≠ 0 := by exact_mod_cast hK_pos.ne' simp [hKne] -
linAuto_score_diff_isLittleOp_onetheorem — Under the sampling measure, for a linear regression-functional system and foldwise nuisance fits, if the L² score difference is uniformly Lipschitz in the two nuisance errors and the regression and Riesz errors are each o_P(1), then the L² score difference is o_P(1).hypothesesΩ :Type*μ :Measure ΩS :rep :MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_XK :ℕg_hat :ℕ → Fin K → Ω → S.H_γα_hat :ℕ → Fin K → Ω → S.X → ℝCscore :ℝhCscore :0 < Cscoreh_score_lipschitz :∀ n k ω,|(eLpNorm (fun z => linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z - linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z) 2 S.P_Z).toReal|h_g_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun x => S.γ_target (g_hat n k ω) x - S.γ_target S.g₀ x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) μh_α_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) μk :conclusionIsLittleOp (fun n ω => (eLpNorm (fun z => linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z - linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) μProof (Lean source)
theorem linAuto_score_diff_isLittleOp_one {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : LinRegFnSys) (rep : MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) {K : ℕ} (g_hat : ℕ → Fin K → Ω → S.H_γ) (α_hat : ℕ → Fin K → Ω → S.X → ℝ) (Cscore : ℝ) (hCscore : 0 < Cscore) (h_score_lipschitz : ∀ n k ω, |(eLpNorm (fun z => linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z - linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z) 2 S.P_Z).toReal| ≤ Cscore * |(eLpNorm (fun x => S.γ_target (g_hat n k ω) x - S.γ_target S.g₀ x) 2 S.P_X).toReal + (eLpNorm (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X).toReal|) (h_g_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun x => S.γ_target (g_hat n k ω) x - S.γ_target S.g₀ x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) μ) (h_α_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) μ) : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z - linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) μ := by intro k apply IsLittleOp.of_abs_le_const_mul_one hCscore (IsLittleOp.add_one (h_g_rate k) (h_α_rate k)) exact fun n ω => h_score_lipschitz n k ω
ATE 8 core · 1 supporting For finite covariate spaces, every regression direction is bounded and integrable. ★ ateRieszWeight_representation★ ateLinAutoDMLEstimator_eq_foldAverage
A worked ATE regression-nuisance moment system
For finite covariate spaces, every regression direction is bounded and
integrable. This lets the standard back-door assumptions and pointwise strict
overlap produce a fully concrete RegNuisanceMomentSys, its matching
LinRegFnSys, the signed inverse-propensity pairing function, and a feasible
linear-DML estimator.
For a finite measurable covariate space, the ATE regression nuisance type consists of the two unrestricted real regression functions indexed by the treatment arm.
Definition (Lean source)
For a back-door ATE system and an observed covariate--arm pair, the signed inverse-propensity Riesz weight is 1/e(X) on the treated arm and -1/(1-e(X)) on the control arm.
Definition (Lean source)
Given a finite-covariate back-door estimation system satisfying the standard identification assumptions, the ATE regression-nuisance moment system has covariate object (X,D), regression target g(D,X), population moment ∫(g(1,x)-g(0,x))dP_X-θ, and its observation-level counterpart.
Definition (Lean source)
Given a finite-covariate back-door estimation system satisfying the standard identification assumptions, the ATE linear regression-functional system reuses the observation law, regression target, pushforward identity, and residual equation of ateRegNuisanceMomentSys, with observation-level linear functional g(1,X)-g(0,X).
Definition (Lean source)
For a finite-covariate back-door system, under the back-door assumptions and pointwise overlap at the positive level ε, the signed inverse-propensity weight represents the derivative of the ATE regression moment in the chosen regression direction by the displayed integral identity.
Formal statement
Proof (Lean source)
Given a finite-covariate back-door system, the back-door assumptions, and pointwise strict overlap, the ATE automatic-debiasing mean representation uses the signed inverse-propensity weight on (X,D).
Definition (Lean source)
For a finite-covariate back-door system, under the back-door assumptions and strict overlap at the positive level ε, the signed inverse-propensity weight gives a mean-pairing representation for the ATE regression-functional system.
Definition (Lean source)
Given a finite-covariate back-door system, its identifying assumptions, and strict overlap, a nonnegative DML neighborhood radius, an i.i.d. observed-data sample with a positive-fold split, foldwise regression and pairing-function fits, a sample size and realization, and nonempty evaluation folds, the feasible ATE automatic-DML estimator equals the average of its foldwise observed scores.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
ateLinRieszScore_measurabletheorem — For a finite-covariate back-door system under the back-door assumptions, the ATE linear automatic-debiasing score at any nuisance and parameter pair is measurable.hypothesesP :γ :Type*IsFiniteMeasure P.μFinite γS :hA :S.toPOBackdoorSystem.Assumptionsη :linAutoNuisance (ateLinRegFnSys S hA)θ :ℝconclusionProof (Lean source)
@[fun_prop] theorem ateLinRieszScore_measurable {P : POSystem} {γ : Type*} [MeasurableSpace γ] [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] [Finite γ] [MeasurableSingletonClass γ] (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (η : linAutoNuisance (ateLinRegFnSys S hA)) (θ : ℝ) : Measurable (fun z => linRieszScore (ateLinRegFnSys S hA) η.1 η.2 θ z) := by change Measurable (fun z : γ × Bool × ℝ => (η.1 true z.1 - η.1 false z.1) + η.2 (z.1, z.2.1) * (z.2.2 - η.1 z.2.1 z.1) - θ) have hη1 (d : Bool) : Measurable (η.1 d) := measurable_of_finite _ have hη2 : Measurable η.2 := measurable_of_finite _ fun_prop
GeneralDML 3 core · 2 supporting The construction in this file turns RegNuisanceMomentSys and an AutoDebiasMeanRepresentation into a LinearMoment whenever the original score is affine in the scalar target. ★ autoDebiasedGeneralMoment_meanZero
General automatic-debiasing moment for DML
The construction in this file turns RegNuisanceMomentSys and an
AutoDebiasMeanRepresentation into a LinearMoment whenever the original score is
affine in the scalar target. Its observation-level moment
is exactly autoDebiasedScore; its nuisance truth is (g₀, α₀); and its two
error gauges are the L² errors of the regression target and representer.
For a regression-nuisance moment system, the joint nuisance type used by the general automatic-debiasing DML bridge pairs a regression nuisance with a candidate representer on the covariate space.
Definition (Lean source)
Given an auxiliary sampling measure, a regression-nuisance moment system, its automatic-debiasing representer, a nonnegative neighborhood radius, measurability of every debiased score, an affine decomposition of the original score, and a nonzero population mean of the truth coefficient, the associated linear moment uses the joint nuisance (g, α), the automatically debiased observation-level score, and L² regression-target and representer error gauges.
Definition (Lean source)
Under the inputs defining the general automatic-debiasing moment, if the truth baseline moment and representer-weighted truth residual are integrable, then the bridged general moment has population mean zero at its nuisance and parameter truth.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
instAddCommGroupinstance — For a regression-nuisance moment system, its joint automatic-debiasing nuisance type has the componentwise additive commutative group structure. -
instModuleinstance — For a regression-nuisance moment system, its joint automatic-debiasing nuisance type has the componentwise real vector-space structure.