Estimation.Orthogonal­Moments.Auto­Debias

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.

structure RegNuisanceMomentSys reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
Z :
X :
P_X :
H :
Type*
Module ℝ H
proj_X :
Z → X
proj_X_meas :
Measurable proj_X
Y_obs :
Z → ℝ
Y_obs_meas :
γ_target :
H → X → ℝ
γ_target_meas :
∀ γ, Measurable (γ_target γ)
γ_target_add :
∀ (γ₁ γ₂ : H) (x : X), γ_target (γ₁ + γ₂) x = γ_target γ₁ x + γ_target γ₂ x
γ_target_smul :
∀ (c : ℝ) (γ : H) (x : X), γ_target (c • γ) x = c * γ_target γ x
g₀ :
H
θ₀ :
ℝ
M :
ℝ → H → ℝ
M_truth :
M θ₀ g₀ = 0
D_g_M :
H → ℝ
D_g_M_hasDerivAt :
∀ ν : H, HasDerivAt (fun r : ℝ => M θ₀ (g₀ + r • ν)) (D_g_M ν) 0
m :
H → Z → ℝ → ℝ
m_meas :
∀ g θ, Measurable (fun z => m g z θ)
m_population :
∀ g θ, M θ g = ∫ z, m g z θ ∂P_Z
pushforward :
P_X = P_Z.map proj_X
regression_resid_orthog :
∀ α : X → ℝ
and
Integrable (fun z => α (proj_X z) * (Y_obs z - γ_target g₀ (proj_X z))) P_Z
then
∫ z, α (proj_X z) * (Y_obs z - γ_target g₀ (proj_X z)) ∂P_Z = 0
Causalean.Estimation.OrthogonalMoments.AutoDebias.RegNuisanceMomentSys · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:48
structure AutoDebiasMeanRepresentation reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
α₀ :
S.X → ℝ
α₀_meas :
α₀_integrable :
Integrable α₀ S.P_X
representation :
∀ ν : S.H, S.D_g_M ν = ∫ x, α₀ x * S.γ_target ν x ∂S.P_X
Causalean.Estimation.OrthogonalMoments.AutoDebias.AutoDebiasMeanRepresentation · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:151 · uses RegNuisanceMomentSys
def autoDebiasedScore reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
g :
S.H
α :
S.X → ℝ
θ :
ℝ
z :
S.Z
autoDebiasedScore S g α θ z :
ℝ
S.m g z θ + α (S.proj_X z) * (S.Y_obs z - S.γ_target g (S.proj_X z))
Causalean.Estimation.OrthogonalMoments.AutoDebias.autoDebiasedScore · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:167 · uses RegNuisanceMomentSys
def autoDebiasedMoment reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
g :
S.H
α :
S.X → ℝ
θ :
ℝ
autoDebiasedMoment S g α θ :
ℝ
∫ z, autoDebiasedScore S g α θ z ∂S.P_Z
Causalean.Estimation.OrthogonalMoments.AutoDebias.autoDebiasedMoment · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:180 · uses RegNuisanceMomentSys
theorem autoDebiasedMoment_meanZero_at_truth reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
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_int_m_truth :
Integrable (fun z => S.m S.g₀ z S.θ₀) S.P_Z
autoDebiasedMoment S S.g₀ rep.α₀ S.θ₀ = 0
Proof (Lean source)
theorem autoDebiasedMoment_meanZero_at_truth (S : RegNuisanceMomentSys) (rep : AutoDebiasMeanRepresentation S) (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_int_m_truth : Integrable (fun z => S.m S.g₀ z S.θ₀) S.P_Z) : autoDebiasedMoment S S.g₀ rep.α₀ S.θ₀ = 0 := by unfold autoDebiasedMoment autoDebiasedScore rw [integral_add h_int_m_truth h_α₀_resid_int] rw [show ∫ z, S.m S.g₀ z S.θ₀ ∂S.P_Z = 0 by have h := S.m_population S.g₀ S.θ₀ rw [← h, S.M_truth]] rw [S.regression_resid_orthog rep.α₀ rep.α₀_meas h_α₀_resid_int] ring
Causalean.Estimation.OrthogonalMoments.AutoDebias.autoDebiasedMoment_meanZero_at_truth · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:194 · uses AutoDebiasMeanRepresentation , RegNuisanceMomentSys , autoDebiasedMoment
theorem autoDebiasedMoment_directional_g_zero reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
ν_g :
S.H
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_dir_int :
Integrable (fun z => rep.α₀ (S.proj_X z) * S.γ_target ν_g (S.proj_X z)) S.P_Z
HasDerivAt (fun r : ℝ => autoDebiasedMoment S (S.g₀ + r • ν_g) rep.α₀ S.θ₀) 0 0
Proof (Lean source)
theorem autoDebiasedMoment_directional_g_zero (S : RegNuisanceMomentSys) (rep : AutoDebiasMeanRepresentation S) (ν_g : S.H) (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_dir_int : Integrable (fun z => rep.α₀ (S.proj_X z) * S.γ_target ν_g (S.proj_X z)) S.P_Z) : HasDerivAt (fun r : ℝ => autoDebiasedMoment S (S.g₀ + r • ν_g) rep.α₀ S.θ₀) 0 0 := by have hpath (r : ℝ) : (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 have hcorr_int (r : ℝ) : 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 [hpath] exact h_resid_int.sub (h_dir_int.const_mul r) have hcorr (r : ℝ) : ∫ z, rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target (S.g₀ + r • ν_g) (S.proj_X z)) ∂S.P_Z = -r * S.D_g_M ν_g := by rw [hpath, integral_sub h_resid_int (h_dir_int.const_mul r), integral_const_mul] rw [S.regression_resid_orthog rep.α₀ rep.α₀_meas h_resid_int] have hmap : ∫ z, rep.α₀ (S.proj_X z) * S.γ_target ν_g (S.proj_X z) ∂S.P_Z = ∫ x, rep.α₀ x * S.γ_target ν_g x ∂S.P_X := by rw [S.pushforward] exact (MeasureTheory.integral_map S.proj_X_meas.aemeasurable (rep.α₀_meas.mul (S.γ_target_meas ν_g)).aestronglyMeasurable).symm rw [hmap, ← rep.representation] ring have hfun : (fun r : ℝ => autoDebiasedMoment S (S.g₀ + r • ν_g) rep.α₀ S.θ₀) = (fun r : ℝ => S.M S.θ₀ (S.g₀ + r • ν_g) - r • S.D_g_M ν_g) := by funext r unfold autoDebiasedMoment autoDebiasedScore rw [integral_add (h_m_int r) (hcorr_int r), ← S.m_population, hcorr] ring rw [hfun] have hderiv : HasDerivAt ((fun r : ℝ => S.M S.θ₀ (S.g₀ + r • ν_g)) - fun r : ℝ => r • S.D_g_M ν_g) 0 0 := by simpa only [id_eq, one_smul, sub_self] using (S.D_g_M_hasDerivAt ν_g).sub ((hasDerivAt_id (0 : ℝ)).smul_const (S.D_g_M ν_g)) exact hderiv.congr_of_eventuallyEq (Filter.Eventually.of_forall fun _ => rfl)
Causalean.Estimation.OrthogonalMoments.AutoDebias.autoDebiasedMoment_directional_g_zero · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:215 · uses AutoDebiasMeanRepresentation , RegNuisanceMomentSys , autoDebiasedMoment
theorem autoDebiasedMoment_directional_α_zero reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
ν_α :
S.X → ℝ
hν_α_meas :
h_m_int :
Integrable (fun z => S.m S.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_dir_int :
Integrable (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z
HasDerivAt (fun r : ℝ => autoDebiasedMoment S S.g₀ (fun x => rep.α₀ x + r * ν_α x) S.θ₀) 0 0
Proof (Lean source)
theorem autoDebiasedMoment_directional_α_zero (S : RegNuisanceMomentSys) (rep : AutoDebiasMeanRepresentation S) (ν_α : S.X → ℝ) (hν_α_meas : Measurable ν_α) (h_m_int : Integrable (fun z => S.m S.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_dir_int : Integrable (fun z => ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z) : HasDerivAt (fun r : ℝ => autoDebiasedMoment S S.g₀ (fun x => rep.α₀ x + r * ν_α x) S.θ₀) 0 0 := by have hdir : ∫ 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 have hfun : (fun r : ℝ => autoDebiasedMoment S S.g₀ (fun x => rep.α₀ x + r * ν_α x) S.θ₀) = fun r : ℝ => autoDebiasedMoment S S.g₀ rep.α₀ S.θ₀ + r * 0 := by funext r unfold autoDebiasedMoment autoDebiasedScore have hbase := h_m_int.add h_resid_int calc _ = ∫ z, (S.m S.g₀ z S.θ₀ + rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) + r * (ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) ∂S.P_Z := by apply integral_congr_ae filter_upwards with z ring _ = (∫ z, S.m S.g₀ z S.θ₀ + rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) ∂S.P_Z) + ∫ z, r * (ν_α (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) ∂S.P_Z := integral_add hbase (h_dir_int.const_mul r) _ = _ := by rw [integral_const_mul, hdir] rw [hfun] simpa using (hasDerivAt_const (x := (0 : ℝ)) (c := autoDebiasedMoment S S.g₀ rep.α₀ S.θ₀))
Causalean.Estimation.OrthogonalMoments.AutoDebias.autoDebiasedMoment_directional_α_zero · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:281 · uses AutoDebiasMeanRepresentation , RegNuisanceMomentSys , autoDebiasedMoment
def genRieszLoss reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
α :
S.H
genRieszLoss S α :
ℝ
∫ x, (S.γ_target α x) ^ 2 ∂S.P_X - 2 * S.D_g_M α
Causalean.Estimation.OrthogonalMoments.AutoDebias.genRieszLoss · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:431 · uses RegNuisanceMomentSys
def finDiffRieszLoss reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
Ω :
Type*
Z_data :
ℕ → Ω → S.Z
θ_hat :
ℕ → Ω → ℝ
g_hat :
ℕ → Ω → S.H
ε :
ℕ → ℝ
α :
S.H
C :
ℕ → Finset ℕ
n :
ℕ
ω :
Ω
finDiffRieszLoss S Z_data θ_hat g_hat ε α C n ω :
ℝ
((C n).card : ℝ)⁻¹ * ∑ i ∈ C n, (S.γ_target α (S.proj_X (Z_data i ω))) ^ 2
- 2 * ( ((C n).card : ℝ)⁻¹ * ∑ i ∈ C n, S.m (g_hat n ω + ε n • α) (Z_data i ω) (θ_hat n ω) - ((C n).card : ℝ)⁻¹ * ∑ i ∈ C n, S.m (g_hat n ω - ε n • α) (Z_data i ω) (θ_hat n ω) ) / (2 * ε n)
Causalean.Estimation.OrthogonalMoments.AutoDebias.finDiffRieszLoss · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:447 · uses RegNuisanceMomentSys
2 supporting declarations (lemmas, instances)
  • D_g_M_smul theorem — 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.
    c :
    ℝ
    ν :
    S.H
    S.D_g_M (c • ν) = c * S.D_g_M ν
    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'
    Causalean.Estimation.OrthogonalMoments.AutoDebias.RegNuisanceMomentSys.D_g_M_smul · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:120
  • autoDebiasedMoment_directional_zero theorem — 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,ν_α).
    ν_g :
    S.H
    ν_α :
    S.X → ℝ
    hν_α_meas :
    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
    Proof (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
    Causalean.Estimation.OrthogonalMoments.AutoDebias.autoDebiasedMoment_directional_zero · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:330
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.

structure LinRegFnSys reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
Z :
X :
P_X :
H_γ :
Type*
Module ℝ H_γ
proj_X :
Z → X
proj_X_meas :
Measurable proj_X
Y_obs :
Z → ℝ
Y_obs_meas :
γ_target :
H_γ → X → ℝ
γ_target_add :
∀ (γ₁ γ₂ : H_γ) (x : X), γ_target (γ₁ + γ₂) x = γ_target γ₁ x + γ_target γ₂ x
γ_target_smul :
∀ (c : ℝ) (γ : H_γ) (x : X), γ_target (c • γ) x = c * γ_target γ x
m_lin :
Z → H_γ → ℝ
m_lin_addLeft :
∀ z (γ₁ γ₂ : H_γ), m_lin z (γ₁ + γ₂) = m_lin z γ₁ + m_lin z γ₂
m_lin_smulLeft :
∀ (c : ℝ) z (γ : H_γ), m_lin z (c • γ) = c * m_lin z γ
m_lin_meas :
∀ γ : H_γ, Measurable (fun z => m_lin z γ)
g₀ :
H_γ
pushforward :
P_X = P_Z.map proj_X
regression_resid_orthog :
∀ α : X → ℝ
and
Integrable (fun z => α (proj_X z) * (Y_obs z - γ_target g₀ (proj_X z))) P_Z
then
∫ z, α (proj_X z) * (Y_obs z - γ_target g₀ (proj_X z)) ∂P_Z = 0
Causalean.Estimation.OrthogonalMoments.AutoDebias.LinRegFnSys · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:44
def L_of_m reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
L_of_m S :
S.H_γ → ℝ
fun γ => ∫ z, S.m_lin z γ ∂S.P_Z
Causalean.Estimation.OrthogonalMoments.AutoDebias.L_of_m · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:108 · uses LinRegFnSys
def linRieszScore reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
γ :
S.H_γ
α :
S.X → ℝ
θ :
ℝ
z :
S.Z
linRieszScore S γ α θ z :
ℝ
S.m_lin z γ + α (S.proj_X z) * (S.Y_obs z - S.γ_target γ (S.proj_X z)) - θ
Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszScore · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:132 · uses LinRegFnSys
def linAutoInfluence reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
rep :
MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X
z :
S.Z
linAutoInfluence S rep z :
ℝ
S.m_lin z S.g₀
- L_of_m S S.g₀
+ rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))
Causalean.Estimation.OrthogonalMoments.AutoDebias.linAutoInfluence · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:146 · uses L_of_m , LinRegFnSys , MeanPairingRepresentation
theorem linRieszScore_directional_g_zero reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
rep :
MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X
ν_g :
S.H_γ
(∫ z, S.m_lin z ν_g ∂S.P_Z) - ∫ x, rep.α₀ x * S.γ_target ν_g x ∂S.P_X = 0
Proof (Lean source)
theorem linRieszScore_directional_g_zero (S : LinRegFnSys) (rep : MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (ν_g : S.H_γ) : (∫ z, S.m_lin z ν_g ∂S.P_Z) - ∫ x, rep.α₀ x * S.γ_target ν_g x ∂S.P_X = 0 := by have hrep := rep.representation ν_g; unfold L_of_m at hrep; linarith
Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszScore_directional_g_zero · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:194 · uses L_of_m , LinRegFnSys , MeanPairingRepresentation
def linRieszLoss reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
α :
S.H_γ
linRieszLoss S α :
ℝ
∫ x, (S.γ_target α x) ^ 2 ∂S.P_X - 2 * L_of_m S α
Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszLoss · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:220 · uses LinRegFnSys
def linEmpiricalRieszLoss reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
Ω :
Type*
Z_data :
ℕ → Ω → S.Z
α :
S.H_γ
C :
ℕ → Finset ℕ
n :
ℕ
ω :
Ω
linEmpiricalRieszLoss S Z_data α C n ω :
ℝ
((C n).card : ℝ)⁻¹ * ∑ i ∈ C n, ((S.γ_target α (S.proj_X (Z_data i ω))) ^ 2 - 2 * S.m_lin (Z_data i ω) α)
Causalean.Estimation.OrthogonalMoments.AutoDebias.linEmpiricalRieszLoss · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:234 · uses LinRegFnSys
def IsLinRieszEmpiricalMinimizer reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
Ω :
Type*
Z_data :
ℕ → Ω → S.Z
A :
Set S.H_γ
C :
ℕ → Finset ℕ
α_hat :
ℕ → Ω → S.H_γ
n ω :
IsLinRieszEmpiricalMinimizer S Z_data A C α_hat :
Prop
clause 1
α_hat n ω ∈ A
clause 2
α ∈ A :
linEmpiricalRieszLoss S Z_data (α_hat n ω) C n ω ≤ linEmpiricalRieszLoss S Z_data α C n ω
Causalean.Estimation.OrthogonalMoments.AutoDebias.IsLinRieszEmpiricalMinimizer · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:250 · uses LinRegFnSys
theorem linRieszLoss_excess_eq_l2dist reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
α α₀_idx :
S.H_γ
rep :
MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X
hRep_eq_idx :
∀ x, rep.α₀ x = S.γ_target α₀_idx x
h_int_α2 :
Integrable (fun x => (S.γ_target α x) ^ 2) S.P_X
h_int_α₀2 :
Integrable (fun x => (S.γ_target α₀_idx x) ^ 2) S.P_X
h_int_αα₀ :
Integrable (fun x => S.γ_target α x * S.γ_target α₀_idx x) S.P_X
h_int_diff_sq :
Integrable (fun x => (S.γ_target α x - S.γ_target α₀_idx x) ^ 2) S.P_X
linRieszLoss S α - linRieszLoss S α₀_idx
= ∫ x, (S.γ_target α x - S.γ_target α₀_idx x) ^ 2 ∂S.P_X
Proof (Lean source)
theorem linRieszLoss_excess_eq_l2dist (S : LinRegFnSys) (α α₀_idx : S.H_γ) (rep : MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (hRep_eq_idx : ∀ x, rep.α₀ x = S.γ_target α₀_idx x) (h_int_α2 : Integrable (fun x => (S.γ_target α x) ^ 2) S.P_X) (h_int_α₀2 : Integrable (fun x => (S.γ_target α₀_idx x) ^ 2) S.P_X) (h_int_αα₀ : Integrable (fun x => S.γ_target α x * S.γ_target α₀_idx x) S.P_X) (h_int_diff_sq : Integrable (fun x => (S.γ_target α x - S.γ_target α₀_idx x) ^ 2) S.P_X) : linRieszLoss S α - linRieszLoss S α₀_idx = ∫ x, (S.γ_target α x - S.γ_target α₀_idx x) ^ 2 ∂S.P_X := by have h_int_α₀α : Integrable (fun x => S.γ_target α₀_idx x * S.γ_target α x) S.P_X := by simpa [mul_comm] using h_int_αα₀ have hL_α : L_of_m S α = ∫ x, S.γ_target α₀_idx x * S.γ_target α x ∂S.P_X := by rw [rep.representation α]; congr 1; funext x; rw [hRep_eq_idx x] have hL_α₀ : L_of_m S α₀_idx = ∫ x, (S.γ_target α₀_idx x) ^ 2 ∂S.P_X := by rw [rep.representation α₀_idx]; congr 1; funext x; rw [hRep_eq_idx x]; ring unfold linRieszLoss rw [hL_α, hL_α₀] have hInt_expand : (∫ x, (S.γ_target α x - S.γ_target α₀_idx x) ^ 2 ∂S.P_X) = ∫ x, (S.γ_target α x) ^ 2 - 2 * (S.γ_target α₀_idx x * S.γ_target α x) + (S.γ_target α₀_idx x) ^ 2 ∂S.P_X := by have _ := h_int_diff_sq; apply integral_congr_ae; filter_upwards with x; ring rw [hInt_expand] have hsplit : (∫ x, (S.γ_target α x) ^ 2 - 2 * (S.γ_target α₀_idx x * S.γ_target α x) + (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) = (∫ x, (S.γ_target α x) ^ 2 ∂S.P_X) - 2 * (∫ x, S.γ_target α₀_idx x * S.γ_target α x ∂S.P_X) + (∫ x, (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) := by calc (∫ x, (S.γ_target α x) ^ 2 - 2 * (S.γ_target α₀_idx x * S.γ_target α x) + (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) = ∫ x, ((S.γ_target α x) ^ 2 - 2 * (S.γ_target α₀_idx x * S.γ_target α x)) + (S.γ_target α₀_idx x) ^ 2 ∂S.P_X := by apply integral_congr_ae; filter_upwards with x; ring _ = (∫ x, (S.γ_target α x) ^ 2 - 2 * (S.γ_target α₀_idx x * S.γ_target α x) ∂S.P_X) + (∫ x, (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) := by exact integral_add (h_int_α2.sub (h_int_α₀α.const_mul 2)) h_int_α₀2 _ = ((∫ x, (S.γ_target α x) ^ 2 ∂S.P_X) - (∫ x, 2 * (S.γ_target α₀_idx x * S.γ_target α x) ∂S.P_X)) + (∫ x, (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) := by rw [integral_sub h_int_α2 (h_int_α₀α.const_mul 2)] _ = (∫ x, (S.γ_target α x) ^ 2 ∂S.P_X) - 2 * (∫ x, S.γ_target α₀_idx x * S.γ_target α x ∂S.P_X) + (∫ x, (S.γ_target α₀_idx x) ^ 2 ∂S.P_X) := by rw [integral_const_mul] rw [hsplit]; ring
Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszLoss_excess_eq_l2dist · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:265 · uses L_of_m , LinRegFnSys , linRieszLoss , MeanPairingRepresentation
theorem linRieszLoss_representer_is_globalMinimizer reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
α₀_idx :
S.H_γ
rep :
MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X
hRep_eq_idx :
∀ x, rep.α₀ x = S.γ_target α₀_idx x
h_target_meas :
∀ α : S.H_γ, AEStronglyMeasurable (S.γ_target α) S.P_X
h_int_sq :
∀ α : S.H_γ, Integrable (fun x => (S.γ_target α x) ^ 2) S.P_X
α :
S.H_γ
linRieszLoss S α₀_idx ≤ linRieszLoss S α
Proof (Lean source)
theorem linRieszLoss_representer_is_globalMinimizer (S : LinRegFnSys) (α₀_idx : S.H_γ) (rep : MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (hRep_eq_idx : ∀ x, rep.α₀ x = S.γ_target α₀_idx x) (h_target_meas : ∀ α : S.H_γ, AEStronglyMeasurable (S.γ_target α) S.P_X) (h_int_sq : ∀ α : S.H_γ, Integrable (fun x => (S.γ_target α x) ^ 2) S.P_X) : ∀ α : S.H_γ, linRieszLoss S α₀_idx ≤ linRieszLoss S α := by intro α have hα : MemLp (S.γ_target α) 2 S.P_X := (memLp_two_iff_integrable_sq (h_target_meas α)).2 (h_int_sq α) have hα₀ : MemLp (S.γ_target α₀_idx) 2 S.P_X := (memLp_two_iff_integrable_sq (h_target_meas α₀_idx)).2 (h_int_sq α₀_idx) have h_int_prod : Integrable (fun x => S.γ_target α x * S.γ_target α₀_idx x) S.P_X := by change Integrable (S.γ_target α * S.γ_target α₀_idx) S.P_X exact hα.integrable_mul hα₀ have h_int_diff_sq : Integrable (fun x => (S.γ_target α x - S.γ_target α₀_idx x) ^ 2) S.P_X := (memLp_two_iff_integrable_sq (hα.sub hα₀).aestronglyMeasurable).1 (hα.sub hα₀) have hexcess := linRieszLoss_excess_eq_l2dist S α α₀_idx rep hRep_eq_idx (h_int_sq α) (h_int_sq α₀_idx) h_int_prod h_int_diff_sq have hnonneg : 0 ≤ ∫ x, (S.γ_target α x - S.γ_target α₀_idx x) ^ 2 ∂S.P_X := integral_nonneg fun x => sq_nonneg _ linarith
Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszLoss_representer_is_globalMinimizer · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:321 · uses L_of_m , LinRegFnSys , linRieszLoss , MeanPairingRepresentation
6 supporting declarations (lemmas, instances)
  • L_of_m_add theorem — Additivity of L_of_m on integrable summands.
    γ₁ γ₂ :
    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 γ₂
    Proof (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₂
    Causalean.Estimation.OrthogonalMoments.AutoDebias.L_of_m_add · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:114
  • L_of_m_smul theorem — ℝ-homogeneity of L_of_m.
    c :
    ℝ
    γ :
    S.H_γ
    L_of_m S (c • γ) = c * L_of_m S γ
    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 γ)
    Causalean.Estimation.OrthogonalMoments.AutoDebias.L_of_m_smul · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:124
  • linRieszScore_truth_eq_influence theorem — 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.
    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
    Proof (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
    Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszScore_truth_eq_influence · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:156
  • linRieszScore_meanZero theorem — 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.
    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
    Proof (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]
    Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszScore_meanZero · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:166
  • linRieszScore_directional_α_zero theorem — 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.
    ν_α :
    S.X → ℝ
    hν_α_meas :
    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
    Proof (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
    Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszScore_directional_α_zero · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:207
  • linRieszLoss_FOC_iff_representer theorem — 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 ν.
    α₀_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)
    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)))
    Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszLoss_FOC_iff_representer · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:364
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.

def linAutoNuisance reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
linAutoNuisance S :
Type _
S.H_γ × (S.X → ℝ)
Causalean.Estimation.OrthogonalMoments.AutoDebias.linAutoNuisance · Causalean/Estimation/OrthogonalMoments/AutoDebias/DML.lean:22 · uses LinRegFnSys
def linAutoLinearMoment reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
Ω :
μ :
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)
linAutoLinearMoment μ S rep ε hε_nn h_score_meas :
LinearMoment Ω μ S.Z S.P_Z (linAutoNuisance S)
clause 1
m := fun η z θ => linRieszScore S η.1 η.2 θ z
clause 2
η₀ := (S.g₀, rep.α₀)
clause 3
θ₀ := L_of_m S S.g₀
clause 4
H_ε := {η : linAutoNuisance S | (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 ≤ ε}
clause 5
ρ₁ := fun η η'
=> ⟨(eLpNorm (fun x => S.γ_target η.1 x - S.γ_target η'.1 x) 2 S.P_X).toReal, ENNReal.toReal_nonneg⟩
clause 6
ρ₂ := fun η η'
=> ⟨(eLpNorm (fun x => η.2 x - η'.2 x) 2 S.P_X).toReal, ENNReal.toReal_nonneg⟩
clause 7
m_meas := h_score_meas
clause 8
η₀_mem := by refine ⟨?_, ?_⟩ · have hz : (fun x => S.γ_target S.g₀ x - S.γ_target S.g₀ x)
= (fun _ : S.X => (0 : ℝ)) := by funext x ring rw [hz] simp [hε_nn] · have hz : (fun x => rep.α₀ x - rep.α₀ x) = (fun _ : S.X => (0 : ℝ)) := by funext x ring rw [hz] simp [hε_nn]
clause 9
linScale := -1
clause 10
linScale_ne_zero := by norm_num
clause 11
m_a := fun _ _ => -1
clause 12
m_b := fun η z
=> S.m_lin z η.1 + η.2 (S.proj_X z) * (S.Y_obs z - S.γ_target η.1 (S.proj_X z))
clause 13
m_a_meas := fun _ => measurable_const
clause 14
m_b_meas := fun η => by simpa [linRieszScore] using h_score_meas η 0
clause 15
m_decomp := by intro η z θ simp [linRieszScore] ring
clause 16
linScale_eq := by simp
def linAutoGeneralMoment reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

Under the same inputs as the affine automatic-debiasing moment, the corresponding general moment forgets only the affine decomposition.

Definition (Lean source)
Ω :
μ :
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)
linAutoGeneralMoment μ S rep ε hε_nn h_score_meas :
GeneralMoment Ω μ S.Z S.P_Z (linAutoNuisance S)
(linAutoLinearMoment μ S rep ε hε_nn h_score_meas).toGeneralMoment
def linAuto_int_pred reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
rep :
MeanPairingRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X
linAuto_int_pred S rep η :
Prop
clause 1
Integrable (fun z => S.m_lin z η.1) S.P_Z
clause 2
Integrable (fun z => S.m_lin z S.g₀) S.P_Z
clause 3
Integrable (fun z => η.2 (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z
clause 4
Integrable (fun z => η.2 (S.proj_X z) * S.γ_target η.1 (S.proj_X z)) S.P_Z
clause 5
Integrable (fun z => η.2 (S.proj_X z) * S.γ_target S.g₀ (S.proj_X z)) S.P_Z
clause 6
Integrable (fun x => rep.α₀ x * S.γ_target η.1 x) S.P_X
clause 7
Integrable (fun x => rep.α₀ x * S.γ_target S.g₀ x) S.P_X
clause 8
Integrable η.2 S.P_X
clause 9
Integrable (S.γ_target η.1) S.P_X
clause 10
Integrable (S.γ_target S.g₀) S.P_X
clause 11
Integrable (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z
clause 12
def linAutoDMLEstimator reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
Ω :
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 :
ℕ
split :
KFoldSplit sample K
g_hat :
ℕ → Fin K → Ω → S.H_γ
α_hat :
ℕ → Fin K → Ω → S.X → ℝ
linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat :
ℕ → Ω → ℝ
feasibleCrossFitLinearDML (linAutoLinearMoment μ S rep ε hε_nn h_score_meas) sample split (fun n k ω => (g_hat n k ω, α_hat n k ω))
theorem linAutoDML_asymptoticLinear reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
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 :
1 < K
split :
KFoldSplit sample K
g_hat :
ℕ → Fin K → Ω → S.H_γ
α_hat :
ℕ → Fin K → Ω → S.X → ℝ
hMZ :
MeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas)
hFV :
Integrable (fun z => (linAutoInfluence S rep z) ^ 2) S.P_Z
hη_mem :
∀ n k ω,
(g_hat n k ω, α_hat n k ω) ∈ (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).H_ε
h_int_pred :
∀ n k ω, linAuto_int_pred S rep (g_hat n k ω, α_hat n k ω)
h_g_memLp :
∀ n k ω, MemLp (fun x => S.γ_target (g_hat n k ω) x - S.γ_target S.g₀ x) 2 S.P_X
h_α_memLp :
∀ n k ω, MemLp (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X
h_m_meas :
∀ n k,
Measurable (fun p : Ω × S.Z => linRieszScore S (g_hat n k p.1) (α_hat n k p.1) (L_of_m S S.g₀) p.2)
h_m_train_uncurry :
∀ n k,
Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace S.Z)] (fun p : Ω × S.Z => linRieszScore S (g_hat n k p.1) (α_hat n k p.1) (L_of_m S S.g₀) p.2)
h_m_int :
∀ n k ω,
Integrable (fun z => linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z) S.P_Z
h_m_sq_int :
∀ n k ω,
Integrable (fun z => (linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z) ^ 2) S.P_Z
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 : ℝ)) μ
h_product_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 * (eLpNorm (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ
hψ_meas :
hOracle_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas) sample split (fun n k ω => (g_hat n k ω, α_hat n k ω))) (L_of_m S S.g₀) (fun n => range n) n) μ
IsAsymLinear (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat) (L_of_m S S.g₀) (linAutoInfluence S rep) sample (fun n => range n)
Proof (Lean source)
theorem linAutoDML_asymptoticLinear {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (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 : 1 < K) (split : KFoldSplit sample K) (g_hat : ℕ → Fin K → Ω → S.H_γ) (α_hat : ℕ → Fin K → Ω → S.X → ℝ) (hMZ : MeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas)) (hFV : Integrable (fun z => (linAutoInfluence S rep z) ^ 2) S.P_Z) (hη_mem : ∀ n k ω, (g_hat n k ω, α_hat n k ω) ∈ (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).H_ε) (h_int_pred : ∀ n k ω, linAuto_int_pred S rep (g_hat n k ω, α_hat n k ω)) (h_g_memLp : ∀ n k ω, MemLp (fun x => S.γ_target (g_hat n k ω) x - S.γ_target S.g₀ x) 2 S.P_X) (h_α_memLp : ∀ n k ω, MemLp (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X) (h_m_meas : ∀ n k, Measurable (fun p : Ω × S.Z => linRieszScore S (g_hat n k p.1) (α_hat n k p.1) (L_of_m S S.g₀) p.2)) (h_m_train_uncurry : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace S.Z)] (fun p : Ω × S.Z => linRieszScore S (g_hat n k p.1) (α_hat n k p.1) (L_of_m S S.g₀) p.2)) (h_m_int : ∀ n k ω, Integrable (fun z => linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z) S.P_Z) (h_m_sq_int : ∀ n k ω, Integrable (fun z => (linRieszScore S (g_hat n k ω) (α_hat n k ω) (L_of_m S S.g₀) z) ^ 2) S.P_Z) (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 : ℝ)) μ) (h_product_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 * (eLpNorm (fun x => α_hat n k ω x - rep.α₀ x) 2 S.P_X).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) (hψ_meas : Measurable (linAutoInfluence S rep)) (hOracle_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas) sample split (fun n k ω => (g_hat n k ω, α_hat n k ω))) (L_of_m S S.g₀) (fun n => range n) n) μ) : IsAsymLinear (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat) (L_of_m S S.g₀) (linAutoInfluence S rep) sample (fun n => range n) := by let M := linAutoLinearMoment μ S rep ε hε_nn h_score_meas let η_hat : ℕ → Fin K → Ω → linAutoNuisance S := fun n k ω => (g_hat n k ω, α_hat n k ω) have hBR_at := linAuto_bilinearRem_at μ S rep ε hε_nn h_score_meas g_hat α_hat hη_mem h_int_pred h_g_memLp h_α_memLp have h_score_diff_rate := linAuto_score_diff_isLittleOp_one μ S rep g_hat α_hat Cscore hCscore h_score_lipschitz h_g_rate h_α_rate have ha : MemLp (M.m_a M.η₀) 2 S.P_Z := by simpa [M, linAutoLinearMoment] using (memLp_const (-1 : ℝ) : MemLp (fun _ : S.Z => (-1 : ℝ)) 2 S.P_Z) have hΔa_meas : ∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z)) := by intro n k dsimp [M, η_hat, linAutoLinearMoment] fun_prop have hΔa_uncurry : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace S.Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z)) := by intro n k dsimp [M, η_hat, linAutoLinearMoment] fun_prop have hΔa_memLp : ∀ n k ω, MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 S.P_Z := by intro n k ω simpa [M, η_hat, linAutoLinearMoment] using (memLp_const (0 : ℝ) : MemLp (fun _ : S.Z => (0 : ℝ)) 2 S.P_Z) have hzero := isLittleOp_zero_one (Ω := Ω) μ have hΔa_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) μ := by intro k simpa [M, η_hat, linAutoLinearMoment] using hzero have hΔa_bias : ∀ k, IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂S.P_Z) (fun _ => (1 : ℝ)) μ := by intro k simpa [M, η_hat, linAutoLinearMoment] using hzero have hψM : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) := by simpa [M, linAutoLinearMoment, GeneralMoment.linScaleInv] using hψ_meas have hFV' : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) S.P_Z := by simpa [M, linAutoLinearMoment] using hFV have h := feasibleCrossFitLinearDML_isAsymLinear M hMZ hFV' sample hK_pos split η_hat hBR_at h_m_meas h_m_train_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate ha hΔa_meas hΔa_uncurry hΔa_memLp hΔa_rate hΔa_bias hψM hOracle_meas simpa [linAutoDMLEstimator, M, η_hat, linAutoLinearMoment, linAutoGeneralMoment, GeneralMoment.linScaleInv] using h
theorem linAutoDML_tendstoNormal reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
Ω :
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 :
ℕ
split :
KFoldSplit sample K
g_hat :
ℕ → Fin K → Ω → S.H_γ
α_hat :
ℕ → Fin K → Ω → S.X → ℝ
hAL :
IsAsymLinear (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat) (L_of_m S S.g₀) (linAutoInfluence S rep) sample (fun n => range n)
hψ_meas :
hEstimator_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat) (L_of_m S S.g₀) (fun n => range n) n) μ
Modes.TendstoInLaw (fun _ : ℕ => μ) (IsAsymLinear.rescaledEstimator (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat) (L_of_m S S.g₀) (fun n => range n)) atTop (gaussianMeasure 0 (∫ z, (linAutoInfluence S rep z) ^ 2 ∂S.P_Z))
Proof (Lean source)
theorem linAutoDML_tendstoNormal {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] (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 : ℕ} (split : KFoldSplit sample K) (g_hat : ℕ → Fin K → Ω → S.H_γ) (α_hat : ℕ → Fin K → Ω → S.X → ℝ) (hAL : IsAsymLinear (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat) (L_of_m S S.g₀) (linAutoInfluence S rep) sample (fun n => range n)) (hψ_meas : Measurable (linAutoInfluence S rep)) (hEstimator_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat) (L_of_m S S.g₀) (fun n => range n) n) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (IsAsymLinear.rescaledEstimator (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split g_hat α_hat) (L_of_m S S.g₀) (fun n => range n)) atTop (gaussianMeasure 0 (∫ z, (linAutoInfluence S rep z) ^ 2 ∂S.P_Z)) := by exact hAL.tendsto_normal hψ_meas hEstimator_meas
7 supporting declarations (lemmas, instances)
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.

abbrev ATERegressionNuisance reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
γ :
Type*
ATERegressionNuisance γ :
Type u_1
Bool → γ → ℝ
Causalean.Estimation.OrthogonalMoments.AutoDebias.ATERegressionNuisance · Causalean/Estimation/OrthogonalMoments/AutoDebias/ATE.lean:68
def ateRieszWeight reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
ateRieszWeight S xd :
ℝ
if xd.2 then (S.e_val xd.1)⁻¹ else -((1 - S.e_val xd.1)⁻¹)
Causalean.Estimation.OrthogonalMoments.AutoDebias.ateRieszWeight · Causalean/Estimation/OrthogonalMoments/AutoDebias/ATE.lean:73 · uses BackdoorEstimationSystem , POSystem
def ateRegNuisanceMomentSys reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
P :
γ :
Finite γ
hA :
S.toPOBackdoorSystem.Assumptions
ateRegNuisanceMomentSys S hA :
by letI : IsProbabilityMeasure S.P_X := by unfold BackdoorEstimationSystem.P_X exact Measure.isProbabilityMeasure_map S.measurable_factualX.aemeasurable letI : IsProbabilityMeasure S.P_Z := by unfold BackdoorEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable exact { Z := γ × Bool × ℝ P_Z := S.P_Z X := γ × Bool P_X := S.P_Z.map (fun z => (z.1, z.2.1)) H := ATERegressionNuisance γ proj_X := fun z => (z.1, z.2.1) proj_X_meas := Measurable.prod measurable_fst (measurable_fst.comp measurable_snd) Y_obs := fun z => z.2.2 Y_obs_meas := measurable_snd.comp measurable_snd γ_target := fun g xd => g xd.2 xd.1 γ_target_meas := fun _ => measurable_of_finite _ γ_target_add := by intros; rfl γ_target_smul := by intros; rfl g₀ := S.μ_val θ₀ := S.θ₀ M := fun θ g => ∫ x, g true x - g false x ∂S.P_X - θ M_truth := by simp [BackdoorEstimationSystem.θ₀] D_g_M := fun ν => ∫ x, ν true x - ν false x ∂S.P_X D_g_M_hasDerivAt := by intro ν have hμ (d : Bool) : Integrable (S.μ_val d) S.P_X := (finite_fun_memLp (S.μ_val d) 1 S.P_X).integrable (by norm_num) have hν (d : Bool) : Integrable (ν d) S.P_X := (finite_fun_memLp (ν d) 1 S.P_X).integrable (by norm_num) have hpath : (fun r : ℝ => (∫ x, (S.μ_val + r • ν) true x - (S.μ_val + r • ν) false x ∂S.P_X) - S.θ₀) = fun r : ℝ => ((∫ x, S.μ_val true x - S.μ_val false x ∂S.P_X) - S.θ₀) + r * (∫ x, ν true x - ν false x ∂S.P_X) := by funext r simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul] rw [show (fun x => (S.μ_val true x + r * ν true x) - (S.μ_val false x + r * ν false x)) = (fun x => S.μ_val true x - S.μ_val false x) + r • (fun x => ν true x - ν false x) by funext x; simp [smul_eq_mul]; ring] integral_linearity change (∫ a, S.μ_val true a ∂S.P_X) - (∫ a, S.μ_val false a ∂S.P_X) + (∫ a, r * (ν true a - ν false a) ∂S.P_X) - S.θ₀ = _ rw [MeasureTheory.integral_const_mul] integral_linearity ring rw [hpath] simpa [BackdoorEstimationSystem.θ₀] using ((hasDerivAt_id (0 : ℝ)).mul_const (∫ x, ν true x - ν false x ∂S.P_X)) m := fun g z θ => g true z.1 - g false z.1 - θ m_meas := fun g _ => (((measurable_of_finite (g true)).comp measurable_fst).sub ((measurable_of_finite (g false)).comp measurable_fst)).sub measurable_const m_population := by intro g θ have hmeas : Measurable (fun x : γ => g true x - g false x) := measurable_of_finite _ have hcomp_meas : Measurable (fun z : γ × Bool × ℝ => g true z.1 - g false z.1) := ((measurable_of_finite (g true)).comp measurable_fst).sub ((measurable_of_finite (g false)).comp measurable_fst) rcases Finite.exists_le (fun x : γ => |g true x - g false x|) with ⟨C, hC⟩ have hcomp_int : Integrable (fun z : γ × Bool × ℝ => g true z.1 - g false z.1) S.P_Z := by have hm : MemLp (fun z : γ × Bool × ℝ => g true z.1 - g false z.1) 1 S.P_Z := MemLp.of_bound hcomp_meas.aestronglyMeasurable C (Filter.Eventually.of_forall fun z => by simpa [Real.norm_eq_abs] using hC z.1) exact hm.integrable (by norm_num) rw [show (∫ z, g true z.1 - g false z.1 - θ ∂S.P_Z) = (∫ z, (g true z.1 - g false z.1) ∂S.P_Z) - θ by rw [integral_sub hcomp_int (integrable_const θ)] simp] rw [← S.P_Z_map_projX_eq_P_X, MeasureTheory.integral_map measurable_fst.aemeasurable hmeas.aestronglyMeasurable] pushforward := rfl regression_resid_orthog := by intro α hα h_int have hmap : ∫ z, α (z.1, z.2.1) * (z.2.2 - S.μ_val z.2.1 z.1) ∂S.P_Z = ∫ ω, α (S.factualX ω, S.factualD ω) * (S.factualY ω - S.μ_val (S.factualD ω) (S.factualX ω)) ∂P.μ := by unfold BackdoorEstimationSystem.P_Z rw [MeasureTheory.integral_map S.measurable_factualZ.aemeasurable (by simpa [BackdoorEstimationSystem.P_Z] using h_int.aestronglyMeasurable)] apply integral_congr_ae filter_upwards with ω rfl rw [hmap] let T : P.Ω → ℝ := fun ω => α (S.factualX ω, true) * (S.dVar.indicator true ω * (S.factualY ω - S.μ_val true (S.factualX ω))) let F : P.Ω → ℝ := fun ω => α (S.factualX ω, false) * (S.dVar.indicator false ω * (S.factualY ω - S.μ_val false (S.factualX ω))) have hTF : (fun ω => α (S.factualX ω, S.factualD ω) * (S.factualY ω - S.μ_val (S.factualD ω) (S.factualX ω))) = fun ω => T ω + F ω := by funext ω cases hD : S.factualD ω · have hT : S.dVar.indicator true ω = 0 := S.dVar.indicator_apply_eq_zero (x := true) (by intro he have hd' : S.dVar.factual ω = false := by exact hD rw [he] at hd' contradiction) have hF : S.dVar.indicator false ω = 1 := S.dVar.indicator_apply_eq_one (by exact hD) simp [T, F, hT, hF] · have hT : S.dVar.indicator true ω = 1 := S.dVar.indicator_apply_eq_one (by exact hD) have hF : S.dVar.indicator false ω = 0 := S.dVar.indicator_apply_eq_zero (x := false) (by intro he have hd' : S.dVar.factual ω = true := by exact hD rw [he] at hd' contradiction) simp [T, F, hT, hF] rw [hTF] have harm_resid (d : Bool) : Integrable (fun ω => S.dVar.indicator d ω * (S.factualY ω - S.μ_val d (S.factualX ω))) P.μ := by have hYind : Integrable (fun ω => S.dVar.indicator d ω * S.factualY ω) P.μ := by simpa [mul_comm] using S.dVar.integrable_mul_indicator d (MeasurableSet.singleton d) hA.integrable_factualY have hμx : Integrable (fun ω => S.μ_val d (S.factualX ω)) P.μ := by have hc : Integrable (S.toPOBackdoorSystem.conditionalMeanOutcome d) P.μ := by unfold POBackdoorSystem.conditionalMeanOutcome exact MeasureTheory.integrable_condExp exact hc.congr (S.μ_compat hA d) have hμind : Integrable (fun ω => S.dVar.indicator d ω * S.μ_val d (S.factualX ω)) P.μ := by simpa [mul_comm] using S.dVar.integrable_mul_indicator d (MeasurableSet.singleton d) hμx exact (hYind.sub hμind).congr (Filter.Eventually.of_forall fun _ => by simp only [Pi.sub_apply]; ring) rcases Finite.exists_le (fun xd : γ × Bool => |α xd|) with ⟨C, hC⟩ have hαbound (d : Bool) : ∀ᵐ ω ∂P.μ, ‖α (S.factualX ω, d)‖ ≤ C := Filter.Eventually.of_forall fun ω => by simpa [Real.norm_eq_abs] using hC (S.factualX ω, d) have hαmeas (d : Bool) : AEStronglyMeasurable (fun ω => α (S.factualX ω, d)) P.μ := (hα.comp (prodMk S.measurable_factualX measurable_const)).aestronglyMeasurable have hTint : Integrable T P.μ := by exact (harm_resid true).bdd_mul (hαmeas true) (hαbound true) have hFint : Integrable F P.μ := by exact (harm_resid false).bdd_mul (hαmeas false) (hαbound false) rw [integral_add hTint hFint] dsimp only [T, F] rw [weighted_residual_integral_zero S hA true (fun x => α (x, true)) (by fun_prop) hTint (cond_exp_residual_zero S hA true)] rw [weighted_residual_integral_zero S hA false (fun x => α (x, false)) (by fun_prop) hFint (cond_exp_residual_zero S hA false)] ring }
abbrev ateLinRegFnSys reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
P :
γ :
Finite γ
hA :
S.toPOBackdoorSystem.Assumptions
ateLinRegFnSys S hA :
by letI : IsProbabilityMeasure S.P_Z := by unfold BackdoorEstimationSystem.P_Z exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable exact { Z := γ × Bool × ℝ P_Z := S.P_Z X := γ × Bool P_X := (ateRegNuisanceMomentSys S hA).P_X H_γ := ATERegressionNuisance γ proj_X := fun z => (z.1, z.2.1) proj_X_meas := Measurable.prod measurable_fst (measurable_fst.comp measurable_snd) Y_obs := fun z => z.2.2 Y_obs_meas := measurable_snd.comp measurable_snd γ_target := fun g xd => g xd.2 xd.1 γ_target_add := by intros; rfl γ_target_smul := by intros; rfl m_lin := fun z g => g true z.1 - g false z.1 m_lin_addLeft := by intros simp only [Pi.add_apply] ring m_lin_smulLeft := by intro c z g change (c • g) true z.1 - (c • g) false z.1 = c * (g true z.1 - g false z.1) simp only [Pi.smul_apply, smul_eq_mul] ring m_lin_meas := fun g => ((measurable_of_finite (g true)).comp measurable_fst).sub ((measurable_of_finite (g false)).comp measurable_fst) g₀ := (ateRegNuisanceMomentSys S hA).g₀ pushforward := (ateRegNuisanceMomentSys S hA).pushforward regression_resid_orthog := (ateRegNuisanceMomentSys S hA).regression_resid_orthog }
theorem ateRieszWeight_representation reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
P :
γ :
Finite γ
hA :
S.toPOBackdoorSystem.Assumptions
ε :
ℝ
hε :
0 < ε
hoverlap :
∀ x, ε ≤ S.e_val x ∧ S.e_val x ≤ 1 - ε
(ateRegNuisanceMomentSys S hA).D_g_M ν
= ∫ xd, ateRieszWeight S xd * (ateRegNuisanceMomentSys S hA).γ_target ν xd ∂(ateRegNuisanceMomentSys S hA).P_X
Proof (Lean source)
theorem ateRieszWeight_representation {P : POSystem} {γ : Type*} [MeasurableSpace γ] [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] [Finite γ] [MeasurableSingletonClass γ] (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (ε : ℝ) (hε : 0 < ε) (hoverlap : ∀ x, ε ≤ S.e_val x ∧ S.e_val x ≤ 1 - ε) (ν : ATERegressionNuisance γ) : (ateRegNuisanceMomentSys S hA).D_g_M ν = ∫ xd, ateRieszWeight S xd * (ateRegNuisanceMomentSys S hA).γ_target ν xd ∂(ateRegNuisanceMomentSys S hA).P_X := by let fT : γ → ℝ := fun x => ν true x / S.e_val x let fF : γ → ℝ := fun x => -(ν false x / (1 - S.e_val x)) have hfT_meas : Measurable fT := measurable_of_finite _ have hfF_meas : Measurable fF := measurable_of_finite _ have hfT_int := finite_covariate_indicator_integrable S true fT have hfF_int := finite_covariate_indicator_integrable S false fF have hsplit : (fun ω => ateRieszWeight S (S.factualX ω, S.factualD ω) * ν (S.factualD ω) (S.factualX ω)) = fun ω => fT (S.factualX ω) * S.dVar.indicator true ω + fF (S.factualX ω) * S.dVar.indicator false ω := by funext ω cases hd : S.factualD ω · have hT : S.dVar.indicator true ω = 0 := S.dVar.indicator_apply_eq_zero (x := true) (by intro he have hd' : S.dVar.factual ω = false := by exact hd rw [he] at hd' contradiction) have hF : S.dVar.indicator false ω = 1 := S.dVar.indicator_apply_eq_one (by exact hd) simp [ateRieszWeight, fT, fF, hT, hF, div_eq_mul_inv, mul_comm] · have hT : S.dVar.indicator true ω = 1 := S.dVar.indicator_apply_eq_one (by exact hd) have hF : S.dVar.indicator false ω = 0 := S.dVar.indicator_apply_eq_zero (x := false) (by intro he have hd' : S.dVar.factual ω = true := by exact hd rw [he] at hd' contradiction) simp [ateRieszWeight, fT, fF, hT, hF, div_eq_mul_inv, mul_comm] have hright : (∫ xd, ateRieszWeight S xd * (ateRegNuisanceMomentSys S hA).γ_target ν xd ∂(ateRegNuisanceMomentSys S hA).P_X) = ∫ ω, ateRieszWeight S (S.factualX ω, S.factualD ω) * ν (S.factualD ω) (S.factualX ω) ∂P.μ := by let q : γ × Bool × ℝ → γ × Bool := fun z => (z.1, z.2.1) let k : γ × Bool → ℝ := fun xd => ateRieszWeight S xd * ν xd.2 xd.1 have hq : Measurable q := Measurable.prod measurable_fst (measurable_fst.comp measurable_snd) have hk : Measurable k := measurable_of_finite _ change (∫ xd, k xd ∂(S.P_Z.map q)) = _ calc (∫ xd, k xd ∂(S.P_Z.map q)) = ∫ z, k (q z) ∂S.P_Z := MeasureTheory.integral_map hq.aemeasurable hk.aestronglyMeasurable _ = ∫ ω, k (q (S.factualZ ω)) ∂P.μ := by unfold BackdoorEstimationSystem.P_Z exact MeasureTheory.integral_map S.measurable_factualZ.aemeasurable ((hk.comp hq).aestronglyMeasurable) _ = _ := by rfl have hleft : (ateRegNuisanceMomentSys S hA).D_g_M ν = ∫ ω, ν true (S.factualX ω) - ν false (S.factualX ω) ∂P.μ := by change (∫ x, ν true x - ν false x ∂S.P_X) = _ unfold BackdoorEstimationSystem.P_X rw [MeasureTheory.integral_map S.measurable_factualX.aemeasurable (measurable_of_finite _).aestronglyMeasurable] rw [hleft, hright, hsplit, integral_add hfT_int hfF_int] rw [indicator_to_propScore_integral S true fT hfT_meas hfT_int] rw [indicator_to_propScore_integral S false fF hfF_meas hfF_int] have hTpoint : (fun ω => fT (S.factualX ω) * S.e_val_label true (S.factualX ω)) = fun ω => ν true (S.factualX ω) := by funext ω have he : S.e_val (S.factualX ω) ≠ 0 := ne_of_gt (hε.trans_le (hoverlap (S.factualX ω)).1) simp [fT, e_val_label, he] have hFpoint : (fun ω => fF (S.factualX ω) * S.e_val_label false (S.factualX ω)) = fun ω => -ν false (S.factualX ω) := by funext ω have hce : 1 - S.e_val (S.factualX ω) ≠ 0 := by have := (hoverlap (S.factualX ω)).2 linarith simp [fF, e_val_label, hce] rw [hTpoint, hFpoint, integral_neg] have hνint (d : Bool) : Integrable (fun ω => ν d (S.factualX ω)) P.μ := by rcases Finite.exists_le (fun x => |ν d x|) with ⟨C, hC⟩ exact Integrable.of_bound ((measurable_of_finite (ν d)).comp S.measurable_factualX).aestronglyMeasurable C (Filter.Eventually.of_forall fun ω => by simpa [Real.norm_eq_abs] using hC (S.factualX ω)) rw [integral_sub (hνint true) (hνint false)] ring
def ateAutoDebiasMeanRepresentation reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
P :
γ :
Finite γ
hA :
S.toPOBackdoorSystem.Assumptions
ε :
ℝ
hε :
0 < ε
hoverlap :
∀ x, ε ≤ S.e_val x ∧ S.e_val x ≤ 1 - ε
ateAutoDebiasMeanRepresentation S hA ε hε hoverlap :
AutoDebiasMeanRepresentation (ateRegNuisanceMomentSys S hA)
by let R := ateRegNuisanceMomentSys S hA letI : IsProbabilityMeasure R.P_X := by rw [R.pushforward] exact Measure.isProbabilityMeasure_map R.proj_X_meas.aemeasurable refine { α₀ := ?_ α₀_meas := ?_ α₀_integrable := ?_ representation := ?_ } · change γ × Bool → ℝ exact ateRieszWeight S · change Measurable (ateRieszWeight S) exact measurable_of_finite _ · change Integrable (ateRieszWeight S) (S.P_Z.map fun z : γ × Bool × ℝ => (z.1, z.2.1)) letI : IsFiniteMeasure S.P_Z := by unfold BackdoorEstimationSystem.P_Z exact Measure.isFiniteMeasure_map P.μ S.factualZ letI : IsFiniteMeasure (S.P_Z.map fun z : γ × Bool × ℝ => (z.1, z.2.1)) := Measure.isFiniteMeasure_map S.P_Z fun z
=> (z.1, z.2.1) rcases Finite.exists_le (fun xd : γ × Bool => |ateRieszWeight S xd|) with ⟨C, hC⟩ exact Integrable.of_bound (measurable_of_finite _).aestronglyMeasurable C (Filter.Eventually.of_forall fun xd => by simpa [Real.norm_eq_abs] using hC xd) · change ∀ ν : ATERegressionNuisance γ, (ateRegNuisanceMomentSys S hA).D_g_M ν = ∫ xd, ateRieszWeight S xd * (ateRegNuisanceMomentSys S hA).γ_target ν xd ∂(ateRegNuisanceMomentSys S hA).P_X exact ateRieszWeight_representation S hA ε hε hoverlap
def ateLinMeanPairingRepresentation reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
P :
γ :
Finite γ
hA :
S.toPOBackdoorSystem.Assumptions
ε :
ℝ
hε :
0 < ε
hoverlap :
∀ x, ε ≤ S.e_val x ∧ S.e_val x ≤ 1 - ε
ateLinMeanPairingRepresentation S hA ε hε hoverlap :
by let R := ateRegNuisanceMomentSys S hA let A := ateLinRegFnSys S hA refine { α₀ := ateRieszWeight S α₀_meas := by change Measurable (ateRieszWeight S) exact measurable_of_finite _ α₀_memLp := by have hmeas : Measurable (ateRieszWeight S) := measurable_of_finite _ change MemLp (ateRieszWeight S) 2 (S.P_Z.map fun z : γ × Bool × ℝ => (z.1, z.2.1)) letI : IsFiniteMeasure S.P_Z := by unfold BackdoorEstimationSystem.P_Z exact Measure.isFiniteMeasure_map P.μ S.factualZ letI : IsFiniteMeasure (S.P_Z.map fun z : γ × Bool × ℝ => (z.1, z.2.1)) := Measure.isFiniteMeasure_map S.P_Z fun z => (z.1, z.2.1) rcases Finite.exists_le (fun x : γ × Bool => |ateRieszWeight S x|) with ⟨C, hC⟩ refine MemLp.of_bound hmeas.aestronglyMeasurable C ?_ exact Filter.Eventually.of_forall fun x => by simpa [Real.norm_eq_abs] using hC x representation := ?_ } intro ν have hobs : L_of_m A ν
= R.D_g_M ν := by have hp := R.m_population ν 0 convert hp.symm using 1 <;> simp [L_of_m, A, R, ateLinRegFnSys, ateRegNuisanceMomentSys] apply integral_congr_ae filter_upwards with z simp rw [hobs] exact ateRieszWeight_representation S hA ε hε hoverlap ν
theorem ateLinAutoDMLEstimator_eq_foldAverage reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
P :
γ :
Finite γ
hA :
S.toPOBackdoorSystem.Assumptions
ε :
ℝ
hε :
0 < ε
hoverlap :
∀ x, ε ≤ S.e_val x ∧ S.e_val x ≤ 1 - ε
Ω :
r :
ℝ
hr :
0 ≤ r
sample :
IIDSample Ω (ateLinRegFnSys S hA).Z μ (ateLinRegFnSys S hA).P_Z
K :
ℕ
hK_pos :
0 < K
split :
KFoldSplit sample K
g_hat :
ℕ → Fin K → Ω → (ateLinRegFnSys S hA).H_γ
α_hat :
ℕ → Fin K → Ω → (ateLinRegFnSys S hA).X → ℝ
n :
ℕ
ω :
Ω
hfold :
∀ k, (split.fold n k).Nonempty
linAutoDMLEstimator (ateLinRegFnSys S hA) (ateLinMeanPairingRepresentation S hA ε hε hoverlap) r hr (ateLinRieszScore_measurable S hA) sample split g_hat α_hat n ω
= (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, ((ateLinRegFnSys S hA).m_lin (sample.Z i ω) (g_hat n k ω) + α_hat n k ω ((ateLinRegFnSys S hA).proj_X (sample.Z i ω)) * ((ateLinRegFnSys S hA).Y_obs (sample.Z i ω) - (ateLinRegFnSys S hA).γ_target (g_hat n k ω) ((ateLinRegFnSys S hA).proj_X (sample.Z i ω))))
Proof (Lean source)
theorem ateLinAutoDMLEstimator_eq_foldAverage {P : POSystem} {γ : Type*} [MeasurableSpace γ] [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] [Finite γ] [MeasurableSingletonClass γ] (S : BackdoorEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (ε : ℝ) (hε : 0 < ε) (hoverlap : ∀ x, ε ≤ S.e_val x ∧ S.e_val x ≤ 1 - ε) {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} (r : ℝ) (hr : 0 ≤ r) (sample : IIDSample Ω (ateLinRegFnSys S hA).Z μ (ateLinRegFnSys S hA).P_Z) {K : ℕ} (hK_pos : 0 < K) (split : KFoldSplit sample K) (g_hat : ℕ → Fin K → Ω → (ateLinRegFnSys S hA).H_γ) (α_hat : ℕ → Fin K → Ω → (ateLinRegFnSys S hA).X → ℝ) (n : ℕ) (ω : Ω) (hfold : ∀ k, (split.fold n k).Nonempty) : linAutoDMLEstimator (ateLinRegFnSys S hA) (ateLinMeanPairingRepresentation S hA ε hε hoverlap) r hr (ateLinRieszScore_measurable S hA) sample split g_hat α_hat n ω = (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, ((ateLinRegFnSys S hA).m_lin (sample.Z i ω) (g_hat n k ω) + α_hat n k ω ((ateLinRegFnSys S hA).proj_X (sample.Z i ω)) * ((ateLinRegFnSys S hA).Y_obs (sample.Z i ω) - (ateLinRegFnSys S hA).γ_target (g_hat n k ω) ((ateLinRegFnSys S hA).proj_X (sample.Z i ω)))) := by exact linAutoDMLEstimator_eq_foldAverage (ateLinRegFnSys S hA) (ateLinMeanPairingRepresentation S hA ε hε hoverlap) r hr (ateLinRieszScore_measurable S hA) sample hK_pos split g_hat α_hat n ω hfold
1 supporting declaration (lemmas, instances)
General­DML 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.

abbrev generalAutoNuisance reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
generalAutoNuisance S :
Type _
S.H × (S.X → ℝ)
Causalean.Estimation.OrthogonalMoments.AutoDebias.generalAutoNuisance · Causalean/Estimation/OrthogonalMoments/AutoDebias/GeneralDML.lean:30 · uses RegNuisanceMomentSys
def autoDebiasedGeneralMoment reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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)
Ω :
μ :
ε :
ℝ
hε :
0 ≤ ε
hscore :
∀ θ : ℝ, Measurable (fun z => autoDebiasedScore S η.1 η.2 θ z)
m_a m_b :
S.H → S.Z → ℝ
h_m_a_meas :
∀ g, Measurable (m_a g)
h_m_decomp :
∀ g z θ, S.m g z θ = m_a g z * θ + m_b g z
hJ₀ :
(∫ z, m_a S.g₀ z ∂S.P_Z) ≠ 0
autoDebiasedGeneralMoment μ S rep ε hε hscore m_a m_b h_m_a_meas h_m_decomp hJ₀ :
LinearMoment Ω μ S.Z S.P_Z (generalAutoNuisance S)
clause 1
m := fun η z θ => autoDebiasedScore S η.1 η.2 θ z
clause 2
η₀ := (S.g₀, rep.α₀)
clause 3
θ₀ := S.θ₀
clause 4
H_ε := {η | (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 ≤ ε}
clause 5
ρ₁ := fun η η'
=> ⟨(eLpNorm (fun x => S.γ_target η.1 x - S.γ_target η'.1 x) 2 S.P_X).toReal, ENNReal.toReal_nonneg⟩
clause 6
ρ₂ := fun η η'
=> ⟨(eLpNorm (fun x => η.2 x - η'.2 x) 2 S.P_X).toReal, ENNReal.toReal_nonneg⟩
clause 7
m_meas := hscore
clause 8
η₀_mem := by simp [hε]
clause 9
linScale := ∫ z, m_a S.g₀ z ∂S.P_Z
clause 10
linScale_ne_zero := hJ₀
clause 11
m_a := fun η => m_a η.1
clause 12
m_b := fun η z => m_b η.1 z + η.2 (S.proj_X z) * (S.Y_obs z - S.γ_target η.1 (S.proj_X z))
clause 13
m_a_meas := fun η => h_m_a_meas η.1
clause 14
m_b_meas := fun η
=> by have h0 := hscore η 0 have heq : (fun z => autoDebiasedScore S η.1 η.2 0 z) = fun z => m_b η.1 z
+ η.2 (S.proj_X z) * (S.Y_obs z - S.γ_target η.1 (S.proj_X z)) := by funext z rw [autoDebiasedScore, h_m_decomp] ring rw [← heq] exact h0
clause 15
m_decomp := by intro η z θ rw [autoDebiasedScore, h_m_decomp] ring
clause 16
linScale_eq := rfl
theorem autoDebiasedGeneralMoment_meanZero reviewed
Causalean.Estimation.OrthogonalMoments.AutoDebias

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
Ω :
μ :
ε :
ℝ
hε :
0 ≤ ε
hscore :
∀ θ : ℝ, Measurable (fun z => autoDebiasedScore S η.1 η.2 θ z)
m_a m_b :
S.H → S.Z → ℝ
h_m_a_meas :
∀ g, Measurable (m_a g)
h_m_decomp :
∀ g z θ, S.m g z θ = m_a g z * θ + m_b g z
hJ₀ :
(∫ z, m_a S.g₀ z ∂S.P_Z) ≠ 0
h_m_int :
Integrable (fun z => S.m S.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
MeanZero (autoDebiasedGeneralMoment μ S rep ε hε hscore m_a m_b h_m_a_meas h_m_decomp hJ₀).toGeneralMoment
Proof (Lean source)
theorem autoDebiasedGeneralMoment_meanZero {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : RegNuisanceMomentSys) (rep : AutoDebiasMeanRepresentation S) (ε : ℝ) (hε : 0 ≤ ε) (hscore : ∀ η : generalAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => autoDebiasedScore S η.1 η.2 θ z)) (m_a m_b : S.H → S.Z → ℝ) (h_m_a_meas : ∀ g, Measurable (m_a g)) (h_m_decomp : ∀ g z θ, S.m g z θ = m_a g z * θ + m_b g z) (hJ₀ : (∫ z, m_a S.g₀ z ∂S.P_Z) ≠ 0) (h_m_int : Integrable (fun z => S.m S.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) : MeanZero (autoDebiasedGeneralMoment μ S rep ε hε hscore m_a m_b h_m_a_meas h_m_decomp hJ₀).toGeneralMoment := by exact autoDebiasedMoment_meanZero_at_truth S rep h_resid_int h_m_int
2 supporting declarations (lemmas, instances)