Estimation.OrthogonalMoments.AutoDebias

Linear 9 core · 2 supporting This file develops the linear core of automatic debiasing for regression-based targets. ★ linRieszScore_meanZero★ linRieszScore_directional_g_zero★ linRieszScore_directional_α_zero★ linRieszLoss_excess_eq_l2dist★ linRieszLoss_FOC_iff_representer

Automatic Debiasing for Linear Regression Functionals

This file develops the linear core of automatic debiasing for regression-based targets. It defines the regression-functional system, constructs the population linear functional and Riesz score, and proves the mean-zero, orthogonality, and Riesz-loss identities that underlie the debiased estimator.

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)

fields

Z :

Type*

MeasurableSpace Z

P_Z :

Measure Z

IsProbabilityMeasure P_Z

X :

Type*

MeasurableSpace X

P_X :

Measure X

H_γ :

Type*

AddCommGroup H_γ

Module ℝ H_γ

proj_X :

Z → X

proj_X_meas :

Measurable proj_X

Y_obs :

Z → ℝ

Y_obs_meas :

Measurable Y_obs

γ_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 → ℝ

if

Measurable α

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:39

def L_of_m reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Population linear functional L(γ) := ∫ m_lin(z, γ) dP_Z.

Definition (Lean source)

noncomputable def L_of_m (S : LinRegFnSys) : S.H_γ → ℝ := fun γ => ∫ z, S.m_lin z γ ∂S.P_Z

Causalean.Estimation.OrthogonalMoments.AutoDebias.L_of_m · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:101 · uses LinRegFnSys

def linRieszScore reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Linear Riesz score: alias of the generic rieszScore applied to the linear regression-functional system's data.

Definition (Lean source)

noncomputable def linRieszScore (S : LinRegFnSys) (γ : S.H_γ) (α : S.X → ℝ) (θ : ℝ) (z : S.Z) : ℝ := rieszScore S.γ_target (L_of_m S) S.proj_X S.Y_obs γ α θ z

Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszScore · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:123 · uses LinRegFnSys

theorem linRieszScore_meanZero reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Mean-zero of the debiased linear score at the truth. Given the linear regression-functional system with Riesz representer rep, assume the α₀-weighted regression-residual product at the truth is integrable. Then the population mean of the linear Riesz score, evaluated at the true regression function and the representer's α₀, equals zero.

Formal statement

hypotheses

S :

LinRegFnSys

rep :

RieszRepresentation 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

conclusion

∫ 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 : RieszRepresentation 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) : ∫ z, linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z ∂S.P_Z = 0 := by unfold linRieszScore exact rieszScore_meanZero rep S.g₀ S.proj_X S.Y_obs (S.regression_resid_orthog rep.α₀ rep.α₀_meas h_α₀_resid_int)

Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszScore_meanZero · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:129 · uses L_of_m , LinRegFnSys , linRieszScore , RieszRepresentation

theorem linRieszScore_directional_g_zero reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Directional zero in the regression direction. For a linear regression-functional system with Riesz representer and any perturbation ν_g of the regression nuisance, the Gateaux derivative of the population debiased moment in the g-direction at the truth vanishes — equivalently, this is the representer identity for the perturbation ν_g.

Formal statement

hypotheses

S :

LinRegFnSys

rep :

RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X

ν_g :

S.H_γ

conclusion

(∫ 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 : RieszRepresentation 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:146 · uses L_of_m , LinRegFnSys , RieszRepresentation

theorem linRieszScore_directional_α_zero reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Directional zero in the representer direction. For any perturbation ν_α of the representer, assume ν_α is measurable and the ν_α-weighted regression-residual product at the truth is integrable. Then the population mean of the ν_α-weighted regression residual at the truth is zero.

Formal statement

hypotheses

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

conclusion

∫ 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:159 · uses LinRegFnSys

def linRieszLoss reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Linear Riesz loss:

Definition (Lean source)

noncomputable def linRieszLoss (S : LinRegFnSys) (α : S.H_γ) : ℝ := ∫ x, (S.γ_target α x) ^ 2 ∂S.P_X - 2 * L_of_m S α

Causalean.Estimation.OrthogonalMoments.AutoDebias.linRieszLoss · Causalean/Estimation/OrthogonalMoments/AutoDebias/Linear.lean:172 · 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 Riesz representer via rep.α₀ = γ_target α₀_idx pointwise. Assume (γ_target α) ^ 2 is integrable, (γ_target α₀_idx) ^ 2 is integrable, the product γ_target α · γ_target α₀_idx is integrable, and the squared difference (γ_target α − γ_target α₀_idx) ^ 2 is integrable. Then the excess linear Riesz loss of α over α₀_idx equals the squared L²(P_X) distance between γ_target α and γ_target α₀_idx.

Formal statement

hypotheses

S :

LinRegFnSys

α α₀_idx :

S.H_γ

rep :

RieszRepresentation 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

conclusion

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 : RieszRepresentation 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:181 · uses L_of_m , LinRegFnSys , linRieszLoss , RieszRepresentation

theorem linRieszLoss_FOC_iff_representer reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

First-order condition for Riesz loss minimizers (Prop 4, first half). Assume the squared regression functional along every perturbed line α₀_idx + t • ν is integrable, that the linear moment integrand m_lin(·, ν) is integrable for every direction ν, and that the product γ_target α₀_idx · γ_target ν is integrable for every direction ν. Then α₀_idx is a directional minimizer of the Riesz loss along every line through it if and only if it indexes a Riesz representer, i.e. L_of_m S ν = ∫ γ_target α₀_idx · γ_target ν dP_X for every ν.

Formal statement

hypotheses

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

conclusion

(∀ ν : 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:244 · uses L_of_m , LinRegFnSys , linRieszLoss

2 supporting declarations (lemmas, instances)

L_of_m_add theorem — Additivity of L_of_m on integrable summands.

hypotheses

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

conclusion

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:105
L_of_m_smul theorem — ℝ-homogeneity of L_of_m.

hypotheses

S :

LinRegFnSys

c :

ℝ

γ :

S.H_γ

conclusion

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:115

DML 4 core · 2 supporting This file instantiates the abstract Chernozhukov double machine learning framework with the linear automatic-debiasing score. ★ linAutoDML_asymptoticLinear

Automatic Debiasing DML Estimator

This file instantiates the abstract Chernozhukov double machine learning framework with the linear automatic-debiasing score. It packages the joint regression and Riesz-representer nuisance, proves reusable mean-zero and bilinear-remainder lemmas, and states an asymptotic-linearity wrapper under the abstract DML theorem's supplied hypotheses.

def linAutoNuisance reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Joint nuisance type for the linear Auto-DML moment: a regression function γ ∈ H_γ paired with a Riesz-representer candidate α : X → ℝ. Carries componentwise AddCommGroup / Module ℝ.

Definition (Lean source)

def linAutoNuisance (S : LinRegFnSys) : Type _ := S.H_γ × (S.X → ℝ)

Causalean.Estimation.OrthogonalMoments.AutoDebias.linAutoNuisance · Causalean/Estimation/OrthogonalMoments/AutoDebias/DML.lean:46 · uses LinRegFnSys

def linAutoGeneralMoment reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Linear Auto-DML moment as a GeneralMoment instance.

Definition (Lean source)

noncomputable def linAutoGeneralMoment {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : LinRegFnSys) (rep : RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (ε : ℝ) (hε_nn : 0 ≤ ε) (h_score_meas : ∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)) : GeneralMoment Ω μ S.Z S.P_Z (linAutoNuisance S) where m := fun η z θ => linRieszScore S η.1 η.2 θ z η₀ := (S.g₀, rep.α₀) θ₀ := L_of_m S S.g₀ 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 ≤ ε } ρ₁ := fun η η' => ⟨(eLpNorm (fun x => S.γ_target η.1 x - S.γ_target η'.1 x) 2 S.P_X).toReal, ENNReal.toReal_nonneg⟩ ρ₂ := fun η η' => ⟨(eLpNorm (fun x => η.2 x - η'.2 x) 2 S.P_X).toReal, ENNReal.toReal_nonneg⟩ m_meas := h_score_meas η₀_mem := by refine ⟨?_, ?_⟩ · have h1 : (fun x => S.γ_target S.g₀ x - S.γ_target S.g₀ x) = (fun _ : S.X => (0 : ℝ)) := by funext x; ring rw [h1] simp [hε_nn] · have h2 : (fun x => rep.α₀ x - rep.α₀ x) = (fun _ : S.X => (0 : ℝ)) := by funext x; ring rw [h2] simp [hε_nn] J₀ := -1 J₀_ne_zero := by norm_num

Causalean.Estimation.OrthogonalMoments.AutoDebias.linAutoGeneralMoment · Causalean/Estimation/OrthogonalMoments/AutoDebias/DML.lean:61 · uses L_of_m , LinRegFnSys , linAutoNuisance , instAddCommGroup, instModule, linRieszScore , GeneralMoment , RieszRepresentation

def linAutoDMLEstimator reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

One-shot linear Auto-DML estimator.

Definition (Lean source)

noncomputable def linAutoDMLEstimator {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} (S : LinRegFnSys) (rep : RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (ε : ℝ) (hε_nn : 0 ≤ ε) (h_score_meas : ∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)) (sample : IIDSample Ω S.Z μ S.P_Z) (split : OneShotSplit sample) (η_hat : ℕ → Ω → linAutoNuisance S) : ℕ → Ω → ℝ := dmlChernozhukovEstimator (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas) sample split η_hat

Causalean.Estimation.OrthogonalMoments.AutoDebias.linAutoDMLEstimator · Causalean/Estimation/OrthogonalMoments/AutoDebias/DML.lean:220 · uses L_of_m , LinRegFnSys , linAutoNuisance , linRieszScore , RieszRepresentation , IIDSample , OneShotSplit

theorem linAutoDML_asymptoticLinear reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Linear Auto-DML asymptotic-linearity wrapper. Assume ε is nonnegative and that the linear Riesz score is measurable in the observation for every nuisance and target value. Given an i.i.d. sample with a one-shot fold split whose fold-B fraction converges to a strictly positive limit c > 0 along card (foldB n) / n → c, and a sequence of cross-fitted nuisance estimators η̂, suppose the Auto-DML moment has mean zero at the truth, the baseline score is square-integrable (finite variance), and the population moment at η̂ is bounded by a constant times the product of the two bilinear-remainder seminorms, at every fold and sample point. Assume the technical regularity package that the moment at η̂ is jointly measurable, fold-A-measurable in ω, and, at every fold and sample point, integrable and square-integrable. Finally suppose the L² score difference between the estimated and true nuisance is o_P(1), and the product of the two nuisance-error rates decays at the parametric rate o_P(n^{-1/2}). Then the one-shot linear Auto-DML estimator is asymptotically linear at the target value L_of_m S S.g₀, with influence function the baseline linear Riesz score scaled by the inverse Jacobian factor, indexed over the fold-B subsample.

Formal statement

hypotheses

Ω :

Type*

MeasurableSpace Ω

Measure Ω

StandardBorelSpace Ω

IsFiniteMeasure μ

IsProbabilityMeasure μ

S :

LinRegFnSys

rep :

RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X

ε :

ℝ

hε_nn :

0 ≤ ε

h_score_meas :

∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)

sample :

IIDSample Ω S.Z μ S.P_Z

split :

OneShotSplit sample

c :

ℝ

hc_pos :

0 < c

h_split_rate :

Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)

η_hat :

ℕ → Ω → linAutoNuisance S

hMZ :

MeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas)

hFV :

Integrable (fun z => (linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z) ^ 2) S.P_Z

Crem :

ℝ

hBR_at :

∀ n ω,

|∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z|

≤ Crem * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ (η_hat n ω) (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ (η_hat n ω) (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ)

h_m_meas :

∀ n,

Measurable (fun (p : Ω × S.Z) => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n p.1) p.2 (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀)

h_m_foldA :

∀ n,

Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀)

h_m_foldA_uncurry :

∀ n,

Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace S.Z)] (fun (p : Ω × S.Z) => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n p.1) p.2 (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀)

h_m_int :

∀ n ω,

Integrable (fun z => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀) S.P_Z

h_m_sq_int :

∀ n ω,

Integrable (fun z => ((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀) ^ 2) S.P_Z

h_score_diff_rate :

IsLittleOp (fun n ω => (eLpNorm (fun z => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ - (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) μ

h_product_rate :

IsLittleOp (fun n ω => (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ (η_hat n ω) (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ (η_hat n ω) (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ

conclusion

IsAsymLinear (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split η_hat) (L_of_m S S.g₀) (fun z => -(linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).J₀_inv * linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z) sample split.foldB

Proof (Lean source)

theorem linAutoDML_asymptoticLinear {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (S : LinRegFnSys) (rep : RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (ε : ℝ) (hε_nn : 0 ≤ ε) (h_score_meas : ∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)) (sample : IIDSample Ω S.Z μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_hat : ℕ → Ω → linAutoNuisance S) (hMZ : MeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas)) (hFV : Integrable (fun z => (linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z) ^ 2) S.P_Z) {Crem : ℝ} (hBR_at : ∀ n ω, |∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z| ≤ Crem * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ (η_hat n ω) (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ (η_hat n ω) (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ)) (h_m_meas : ∀ n, Measurable (fun (p : Ω × S.Z) => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n p.1) p.2 (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀)) (h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace S.Z)] (fun (p : Ω × S.Z) => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n p.1) p.2 (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀)) (h_m_int : ∀ n ω, Integrable (fun z => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => ((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀) ^ 2) S.P_Z) (h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (η_hat n ω) z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ - (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) μ) (h_product_rate : IsLittleOp (fun n ω => (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ (η_hat n ω) (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ (η_hat n ω) (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) : IsAsymLinear (linAutoDMLEstimator S rep ε hε_nn h_score_meas sample split η_hat) (L_of_m S S.g₀) (fun z => -(linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).J₀_inv * linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z) sample split.foldB := by unfold linAutoDMLEstimator simpa [linAutoGeneralMoment] using (dml_chernozhukov_asymptoticLinear (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas) hMZ hFV sample split hc_pos h_split_rate η_hat (Crem := Crem) hBR_at h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate)

Causalean.Estimation.OrthogonalMoments.AutoDebias.linAutoDML_asymptoticLinear · Causalean/Estimation/OrthogonalMoments/AutoDebias/DML.lean:240 · uses L_of_m , LinRegFnSys , linAutoDMLEstimator , linAutoGeneralMoment , linAutoNuisance , instAddCommGroup, instModule, linRieszScore , J₀_inv , MeanZero , RieszRepresentation , IIDSample , IsAsymLinear , IsLittleOp , OneShotSplit , foldA , foldB

2 supporting declarations (lemmas, instances)

linAuto_meanZero theorem — Mean-zero of the linear Auto-DML moment at the truth. Specialises linRieszScore_meanZero.

hypotheses

Ω :

Type*
MeasurableSpace Ω

μ :

Measure Ω

S :

LinRegFnSys

rep :

RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X

ε :

ℝ

hε_nn :

0 ≤ ε

h_score_meas :

∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)

h_α₀_resid_int :

Integrable (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z

conclusion

MeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas)

Proof (Lean source)

theorem linAuto_meanZero {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : LinRegFnSys) (rep : RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (ε : ℝ) (hε_nn : 0 ≤ ε) (h_score_meas : ∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)) (h_α₀_resid_int : Integrable (fun z => rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z))) S.P_Z) : MeanZero (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas) := by unfold MeanZero linAutoGeneralMoment exact linRieszScore_meanZero S rep h_α₀_resid_int

Causalean.Estimation.OrthogonalMoments.AutoDebias.linAuto_meanZero · Causalean/Estimation/OrthogonalMoments/AutoDebias/DML.lean:102
linAuto_bilinearRem theorem — Bilinear remainder bound for the linear Auto-DML moment.

hypotheses

Ω :

Type*
MeasurableSpace Ω

μ :

Measure Ω

S :

LinRegFnSys

rep :

RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X

ε :

ℝ

hε_nn :

0 ≤ ε

h_score_meas :

∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)

conclusion

∃ C : ℝ,
∀ η ∈ (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).H_ε,
linAuto_int_pred S rep η → MemLp (fun x => S.γ_target η.1 x - S.γ_target S.g₀ x) 2 S.P_X → MemLp (fun x => η.2 x - rep.α₀ x) 2 S.P_X → |∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m η z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z|
≤ C * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ)

Proof (Lean source)

theorem linAuto_bilinearRem {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (S : LinRegFnSys) (rep : RieszRepresentation S.H_γ S.γ_target (L_of_m S) S.P_X) (ε : ℝ) (hε_nn : 0 ≤ ε) (h_score_meas : ∀ η : linAutoNuisance S, ∀ θ : ℝ, Measurable (fun z => linRieszScore S η.1 η.2 θ z)) : ∃ C : ℝ, ∀ η ∈ (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).H_ε, linAuto_int_pred S rep η → MemLp (fun x => S.γ_target η.1 x - S.γ_target S.g₀ x) 2 S.P_X → MemLp (fun x => η.2 x - rep.α₀ x) 2 S.P_X → |∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m η z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z| ≤ C * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) := by refine ⟨1, ?_⟩ intro η _ h_int hγ hα rcases h_int with ⟨h_int_resid_α, h_int_αγ, h_int_αγ₀, h_int_α₀γ, h_int_α₀γ₀, h_int_α, h_int_γ, h_int_γ₀, h_int_resid_α₀, h_orthog_α⟩ let dα : S.X → ℝ := fun x => η.2 x - rep.α₀ x let dγ : S.X → ℝ := fun x => S.γ_target η.1 x - S.γ_target S.g₀ x have h_orthog_α₀ : ∫ z, rep.α₀ (S.proj_X z) * (S.Y_obs z - S.γ_target S.g₀ (S.proj_X z)) ∂S.P_Z = 0 := S.regression_resid_orthog rep.α₀ rep.α₀_meas h_int_resid_α₀ have hrem_sub : (∫ z, linRieszScore S η.1 η.2 (L_of_m S S.g₀) z ∂S.P_Z) - (∫ z, linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z ∂S.P_Z) = -∫ x, dα x * dγ x ∂S.P_X := by unfold linRieszScore dα dγ exact Causalean.Estimation.OrthogonalMoments.rieszScore_bilinearRem rep S.g₀ η.1 η.2 S.proj_X S.Y_obs S.pushforward S.proj_X_meas h_orthog_α₀ h_orthog_α h_int_resid_α h_int_αγ h_int_αγ₀ h_int_α₀γ h_int_α₀γ₀ h_int_α h_int_γ h_int_γ₀ have htruth : ∫ z, linRieszScore S S.g₀ rep.α₀ (L_of_m S S.g₀) z ∂S.P_Z = 0 := linRieszScore_meanZero S rep h_int_resid_α₀ have hrem : ∫ z, linRieszScore S η.1 η.2 (L_of_m S S.g₀) z ∂S.P_Z = -∫ x, dα x * dγ x ∂S.P_X := by simpa [htruth] using hrem_sub have h_abs_rewrite : |∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m η z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z| = |∫ x, dα x * dγ x ∂S.P_X| := by rw [show (∫ z, (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).m η z (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).θ₀ ∂S.P_Z) = ∫ z, linRieszScore S η.1 η.2 (L_of_m S S.g₀) z ∂S.P_Z by rfl] rw [hrem, abs_neg] have h_abs_int : |∫ x, dα x * dγ x ∂S.P_X| ≤ ∫ x, |dα x * dγ x| ∂S.P_X := MeasureTheory.abs_integral_le_integral_abs have hcs : ∫ x, |dα x * dγ x| ∂S.P_X ≤ (eLpNorm dα 2 S.P_X).toReal * (eLpNorm dγ 2 S.P_X).toReal := by simpa [dα, dγ, abs_mul] using (integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := S.P_X) (f := dα) (g := dγ) hα hγ) have hfin : (eLpNorm dα 2 S.P_X).toReal * (eLpNorm dγ 2 S.P_X).toReal = 1 * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₁ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) * (((linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).ρ₂ η (linAutoGeneralMoment μ S rep ε hε_nn h_score_meas).η₀ : NNReal) : ℝ) := by simp [linAutoGeneralMoment, dα, dγ, mul_comm] rfl exact h_abs_rewrite.trans_le ((h_abs_int.trans hcs).trans (le_of_eq hfin))

Causalean.Estimation.OrthogonalMoments.AutoDebias.linAuto_bilinearRem · Causalean/Estimation/OrthogonalMoments/AutoDebias/DML.lean:146

General 9 core · 0 supporting This file extends the automatic-debiasing construction from linear regression functionals to general scalar moment equations with a regression nuisance. ★ autoDebiasedMoment_meanZero_at_truth★ autoDebiasedMoment_directional_g_zero★ autoDebiasedMoment_directional_α_zero

Automatic Debiasing for General Moments

This file extends the automatic-debiasing construction from linear regression functionals to general scalar moment equations with a regression nuisance. It packages the moment system, the Riesz-representer correction, and the resulting orthogonality identities used to build debiased scores, together with population and finite-difference Riesz objectives for representer fitting.

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, the population moment vanishes at the truth, the supplied Gateaux derivative of the moment at the truth is itself additive and homogeneous, the kernel is measurable and integrates against the observation measure to the population moment, the covariate measure is the pushforward of the observation measure under the projection, and the regression residual at the truth, weighted by any measurable integrable function of the covariates, integrates to zero.

Definition (Lean source)

fields

Z :

Type*

MeasurableSpace Z

P_Z :

Measure Z

IsProbabilityMeasure P_Z

X :

Type*

MeasurableSpace X

P_X :

Measure X

H :

Type*

AddCommGroup H

Module ℝ H

proj_X :

Z → X

proj_X_meas :

Measurable proj_X

Y_obs :

Z → ℝ

Y_obs_meas :

Measurable Y_obs

γ_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

g₀ :

H

θ₀ :

ℝ

M :

ℝ → H → ℝ

M_truth :

M θ₀ g₀ = 0

D_g_M :

H → ℝ

D_g_M_add :

∀ (ν₁ ν₂ : H), D_g_M (ν₁ + ν₂) = D_g_M ν₁ + D_g_M ν₂

D_g_M_smul :

∀ (c : ℝ) (ν : H), D_g_M (c • ν) = c * D_g_M ν

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 → ℝ

if

Measurable α

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:42

structure AutoDebiasRepresenter reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Automatic debiasing representer. For a regression-nuisance moment system, a function α₀ on the covariate space that is measurable and integrable against the covariate measure, and that represents the Gateaux derivative of the population moment at the truth, in every direction, as the L²-inner product of α₀ against the regression target evaluated in that direction.

Definition (Lean source)

parameters

S :

RegNuisanceMomentSys

fields

α₀ :

S.X → ℝ

α₀_meas :

Measurable α₀

α₀_integrable :

Integrable α₀ S.P_X

representation :

∀ ν : S.H, S.D_g_M ν = ∫ x, α₀ x * S.γ_target ν x ∂S.P_X

Causalean.Estimation.OrthogonalMoments.AutoDebias.AutoDebiasRepresenter · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:109 · uses RegNuisanceMomentSys

def autoDebiasedScore reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Automatically debiased score (observation-level form):

Definition (Lean source)

noncomputable def autoDebiasedScore (S : RegNuisanceMomentSys) (g : S.H) (α : S.X → ℝ) (θ : ℝ) (z : S.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:125 · uses RegNuisanceMomentSys

def autoDebiasedMoment reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Automatically debiased moment (population form):

Definition (Lean source)

noncomputable def autoDebiasedMoment (S : RegNuisanceMomentSys) (g : S.H) (α : S.X → ℝ) (θ : ℝ) : ℝ := ∫ z, autoDebiasedScore S g α θ z ∂S.P_Z

Causalean.Estimation.OrthogonalMoments.AutoDebias.autoDebiasedMoment · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:132 · 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

hypotheses

S :

RegNuisanceMomentSys

rep :

AutoDebiasRepresenter 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

conclusion

autoDebiasedMoment S S.g₀ rep.α₀ S.θ₀ = 0

Proof (Lean source)

theorem autoDebiasedMoment_meanZero_at_truth (S : RegNuisanceMomentSys) (rep : AutoDebiasRepresenter 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:141 · uses AutoDebiasRepresenter , RegNuisanceMomentSys , autoDebiasedMoment

theorem autoDebiasedMoment_directional_g_zero reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Directional zero in the regression direction. For a regression-nuisance moment system with Riesz representer and any perturbation ν_g of the regression nuisance, the Gateaux derivative of the population debiased moment in the g-direction at the truth vanishes — equivalently, this is the representer identity for the perturbation ν_g.

Formal statement

hypotheses

S :

RegNuisanceMomentSys

rep :

AutoDebiasRepresenter S

ν_g :

S.H

conclusion

S.D_g_M ν_g - ∫ x, rep.α₀ x * S.γ_target ν_g x ∂S.P_X = 0

Proof (Lean source)

theorem autoDebiasedMoment_directional_g_zero (S : RegNuisanceMomentSys) (rep : AutoDebiasRepresenter S) (ν_g : S.H) : S.D_g_M ν_g - ∫ x, rep.α₀ x * S.γ_target ν_g x ∂S.P_X = 0 := by have h := rep.representation ν_g linarith

Causalean.Estimation.OrthogonalMoments.AutoDebias.autoDebiasedMoment_directional_g_zero · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:162 · uses AutoDebiasRepresenter , RegNuisanceMomentSys

theorem autoDebiasedMoment_directional_α_zero reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Directional zero in the representer direction. For any perturbation ν_α of the representer, assume ν_α is measurable and the ν_α-weighted regression-residual product at the truth is integrable. Then the directional derivative of the population debiased moment in the α-direction at the truth vanishes: the integral of the weighted regression residual is zero.

Formal statement

hypotheses

S :

RegNuisanceMomentSys

ν_α :

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

conclusion

∫ 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 autoDebiasedMoment_directional_α_zero (S : RegNuisanceMomentSys) (ν_α : 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.autoDebiasedMoment_directional_α_zero · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:173 · uses RegNuisanceMomentSys

def genRieszLoss reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

General Riesz loss.

Definition (Lean source)

noncomputable def genRieszLoss (S : RegNuisanceMomentSys) (α : S.H) : ℝ := ∫ x, (S.γ_target α x) ^ 2 ∂S.P_X - 2 * S.D_g_M α

Causalean.Estimation.OrthogonalMoments.AutoDebias.genRieszLoss · Causalean/Estimation/OrthogonalMoments/AutoDebias/General.lean:187 · uses RegNuisanceMomentSys

def finDiffRieszLoss reviewed

Causalean.Estimation.OrthogonalMoments.AutoDebias

Finite-difference representer loss.

Definition (Lean source)

noncomputable def finDiffRieszLoss (S : RegNuisanceMomentSys) {Ω : Type*} (Z_data : ℕ → Ω → S.Z) (θ_hat : ℕ → Ω → ℝ) (g_hat : ℕ → Ω → S.H) (ε : ℕ → ℝ) (α : S.H) (C : ℕ → Finset ℕ) (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:198 · uses RegNuisanceMomentSys

Estimation.Orthogonal­Moments.Auto­Debias

Automatic Debiasing for Linear Regression Functionals

Automatic Debiasing DML Estimator

Automatic Debiasing for General Moments