ML.Causal­Application

This roll-up is the causal-application layer for Causalean.ML, kept separate from the causal-free core.

Regression­Bridge 3 core · 1 supporting This file is part of the causal-application layer of Causalean.ML: files under Causalean/ML/CausalApplication/ may import causal and estimation modules, while the Causalean/ML/ core remains causal-free. ★ isL2Projection_of_condExp★ condExp_of_isL2Projection

Conditional expectations as squared-loss population targets

This file is part of the causal-application layer of Causalean.ML: files under Causalean/ML/CausalApplication/ may import causal and estimation modules, while the Causalean/ML/ core remains causal-free.

The ML population-target keystone (square_loss_population_target_of_isL2Projection) is stated for a function whose residual is orthogonal to every function of the covariate (IsL2Projection). Here we connect that to Mathlib's condExp: the conditional mean E[Y ∣ X] is exactly such a projection. This lets a known causal nuisance (defined via condExp, as in Estimation.ATE.BackdoorEstimationSystem.μ_compat) be recognized as the ML squared-loss population minimizer, and vice versa.

def covarSigma reviewed
Causalean.ML.Causal

The covariate sigma-algebra records exactly the information carried by the covariate in a joint covariate-response observation.

Definition (Lean source)
def covarSigma : MeasurableSpace (X × ℝ) := comap fst inferInstance
Causalean.ML.Causal.covarSigma · Causalean/ML/CausalApplication/RegressionBridge.lean:31
theorem isL2Projection_of_condExp reviewed
Causalean.ML.Causal

On a finite joint covariate–response law P, if the candidate function m is measurable, the response coordinate is integrable, and m agrees P-almost everywhere with the conditional expectation of the response given the covariate σ-algebra, then m is an L² projection of the response onto functions of the covariate: its residual is uncorrelated with every measurable, integrable function of the covariate.

Formal statement
hypotheses
P :
Measure (X × ℝ)
IsFiniteMeasure P
m :
X → ℝ
hm :
Measurable m
hY :
Integrable (fun z => z.2) P
hcond :
(fun z => m z.1) =ᵐ[P] (P[fun z => z.2 | covarSigma (X := X)])
conclusion
IsL2Projection P m
Proof (Lean source)
theorem isL2Projection_of_condExp (P : Measure (X × ℝ)) [IsFiniteMeasure P] {m : X → ℝ} (hm : Measurable m) (hY : Integrable (fun z => z.2) P) (hcond : (fun z => m z.1) =ᵐ[P] (P[fun z => z.2 | covarSigma (X := X)])) : IsL2Projection P m := by intro g hgm hg have hF : covarSigma (X := X) ≤ (inferInstance : MeasurableSpace (X × ℝ)) := covarSigma_le (X := X) have hfst : Measurable[covarSigma (X := X)] (fun z : X × ℝ => z.1) := by rw [measurable_iff_comap_le] exact le_rfl have hM_sm : StronglyMeasurable[covarSigma (X := X)] (fun z : X × ℝ => m z.1) := by exact (hm.comp hfst).stronglyMeasurable have hG_sm : StronglyMeasurable[covarSigma (X := X)] (fun z : X × ℝ => g z.1) := by exact (hgm.comp hfst).stronglyMeasurable have hM_int : Integrable (fun z : X × ℝ => m z.1) P := by exact (MeasureTheory.integrable_condExp (μ := P) (m := covarSigma (X := X)) (f := fun z : X × ℝ => z.2)).congr hcond.symm have hres_int : Integrable (fun z : X × ℝ => z.2 - m z.1) P := hY.sub hM_int have hM_ce : P[(fun z : X × ℝ => m z.1) | covarSigma (X := X)] = (fun z : X × ℝ => m z.1) := by exact MeasureTheory.condExp_of_stronglyMeasurable hF hM_sm hM_int have hres_ce : P[(fun z : X × ℝ => z.2 - m z.1) | covarSigma (X := X)] =ᵐ[P] 0 := by calc P[(fun z : X × ℝ => z.2 - m z.1) | covarSigma (X := X)] =ᵐ[P] P[(fun z : X × ℝ => z.2) | covarSigma (X := X)] - P[(fun z : X × ℝ => m z.1) | covarSigma (X := X)] := MeasureTheory.condExp_sub (μ := P) (m := covarSigma (X := X)) hY hM_int _ =ᵐ[P] P[(fun z : X × ℝ => z.2) | covarSigma (X := X)] - (fun z : X × ℝ => m z.1) := by rw [hM_ce] _ =ᵐ[P] 0 := by filter_upwards [hcond] with z hz change P[(fun z : X × ℝ => z.2) | covarSigma (X := X)] z - m z.1 = 0 rw [← hz] simp have hprod_ce : P[(fun z : X × ℝ => (z.2 - m z.1) * g z.1) | covarSigma (X := X)] =ᵐ[P] 0 := by calc P[(fun z : X × ℝ => (z.2 - m z.1) * g z.1) | covarSigma (X := X)] =ᵐ[P] P[(fun z : X × ℝ => z.2 - m z.1) | covarSigma (X := X)] * (fun z : X × ℝ => g z.1) := MeasureTheory.condExp_mul_of_stronglyMeasurable_right (μ := P) (m := covarSigma (X := X)) (f := fun z : X × ℝ => z.2 - m z.1) (g := fun z : X × ℝ => g z.1) hG_sm hg hres_int _ =ᵐ[P] 0 := by filter_upwards [hres_ce] with z hz change P[(fun z : X × ℝ => z.2 - m z.1) | covarSigma (X := X)] z * g z.1 = 0 rw [hz] simp calc ∫ z, (z.2 - m z.1) * g z.1 ∂P = ∫ z, (P[(fun z : X × ℝ => (z.2 - m z.1) * g z.1) | covarSigma (X := X)]) z ∂P := by exact (MeasureTheory.integral_condExp hF (μ := P) (f := fun z : X × ℝ => (z.2 - m z.1) * g z.1)).symm _ = ∫ z, (0 : ℝ) ∂P := by exact integral_congr_ae hprod_ce _ = 0 := by simp
Causalean.ML.Causal.isL2Projection_of_condExp · Causalean/ML/CausalApplication/RegressionBridge.lean:40 · uses covarSigma , IsL2Projection
theorem condExp_of_isL2Projection reviewed
Causalean.ML.Causal

On a finite joint covariate–response law P, if the candidate function m is measurable, the response coordinate is integrable, the composed function z ↦ m(z.1) is integrable, and m is an L² projection of the response onto functions of the covariate — its residual is uncorrelated with every measurable, integrable function of the covariate, then m agrees P-almost everywhere with the conditional expectation of the response given the covariate σ-algebra.

Formal statement
hypotheses
P :
Measure (X × ℝ)
IsFiniteMeasure P
m :
X → ℝ
hm :
Measurable m
hY :
Integrable (fun z => z.2) P
hmint :
Integrable (fun z => m z.1) P
hproj :
IsL2Projection P m
conclusion
(fun z => m z.1) =ᵐ[P] (P[fun z => z.2 | covarSigma (X := X)])
Proof (Lean source)
theorem condExp_of_isL2Projection (P : Measure (X × ℝ)) [IsFiniteMeasure P] {m : X → ℝ} (hm : Measurable m) (hY : Integrable (fun z => z.2) P) (hmint : Integrable (fun z => m z.1) P) (hproj : IsL2Projection P m) : (fun z => m z.1) =ᵐ[P] (P[fun z => z.2 | covarSigma (X := X)]) := by have hF : covarSigma (X := X) ≤ (inferInstance : MeasurableSpace (X × ℝ)) := covarSigma_le (X := X) haveI : IsFiniteMeasure (P.trim hF) := isFiniteMeasure_trim hF haveI : SigmaFinite (P.trim hF) := inferInstance have hfst : Measurable[covarSigma (X := X)] (fun z : X × ℝ => z.1) := by rw [measurable_iff_comap_le] exact le_rfl have hM_aesm : AEStronglyMeasurable[covarSigma (X := X)] (fun z : X × ℝ => m z.1) P := by exact (hm.comp hfst).stronglyMeasurable.aestronglyMeasurable refine MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq hF hY (fun _s _hs _hfin => hmint.integrableOn) ?_ hM_aesm intro s hs hfin have hs_ambient : MeasurableSet s := hF _ hs change MeasurableSet[comap fst inferInstance] s at hs obtain ⟨A, hA, hAeq⟩ := hs let g₀ : X → ℝ := indicator A (fun _ => (1 : ℝ)) have hg₀ : Measurable g₀ := by exact measurable_const.indicator hA have hres_int : Integrable (fun z : X × ℝ => z.2 - m z.1) P := hY.sub hmint have hprod_eq_indicator : (fun z : X × ℝ => (z.2 - m z.1) * g₀ z.1) = s.indicator (fun z : X × ℝ => z.2 - m z.1) := by funext z by_cases hz : z ∈ s · have hzA : z.1 ∈ A := by rw [← hAeq] at hz exact hz simp [g₀, Set.indicator_of_mem hz, Set.indicator_of_mem hzA] · have hzA : z.1 ∉ A := by intro hzA exact hz (by rw [← hAeq] exact hzA) simp [g₀, Set.indicator_of_notMem hz, Set.indicator_of_notMem hzA] have hg₀int : Integrable (fun z : X × ℝ => (z.2 - m z.1) * g₀ z.1) P := by simpa [hprod_eq_indicator] using hres_int.indicator hs_ambient have horth : ∫ z, (z.2 - m z.1) * g₀ z.1 ∂P = 0 := hproj g₀ hg₀ hg₀int have hres_set_zero : ∫ z in s, z.2 - m z.1 ∂P = 0 := by rw [← MeasureTheory.integral_indicator (μ := P) hs_ambient, ← hprod_eq_indicator] exact horth have hsubeq : ∫ z in s, z.2 ∂P - ∫ z in s, m z.1 ∂P = 0 := by rw [← MeasureTheory.integral_sub hY.integrableOn hmint.integrableOn] exact hres_set_zero exact (sub_eq_zero.mp hsubeq).symm
Causalean.ML.Causal.condExp_of_isL2Projection · Causalean/ML/CausalApplication/RegressionBridge.lean:116 · uses covarSigma , IsL2Projection
1 supporting declaration (lemmas, instances)
Nuisance 3 core · 0 supporting Using the conditional-expectation bridge (RegressionBridge), the population targets of the Causalean.ML learners are exactly the causal nuisance functions that the AIPW / DML machinery consumes: the squared-loss target o ★ mlOutcomeRegression_ae_eq★ mlPropensity_ae_eq★ mlNuisanceVec

ML learners as causal nuisance estimators

Using the conditional-expectation bridge (RegressionBridge), the population targets of the Causalean.ML learners are exactly the causal nuisance functions that the AIPW / DML machinery consumes: the squared-loss target on a treatment arm is the outcome regression μ(d, x) = E[Y ∣ X, D=d], and the squared-loss target on the treatment indicator is the propensity e(x) = P(D=1 ∣ X). mlNuisanceVec packages two such targets into the Estimation.ATE.NuisanceVec the AIPW moment expects.

theorem mlOutcomeRegression_ae_eq reviewed
Causalean.ML.Causal

Outcome-regression recovery. On a finite covariate–outcome law Pd, if the candidate regression function m is measurable, the outcome coordinate is integrable, the composed function z ↦ m(z.1) is integrable, and m is the squared-loss population target — its residual Y − m(X) is uncorrelated with every measurable, integrable function of the covariate, then m agrees Pd-almost everywhere with the conditional expectation of the outcome given the covariate σ-algebra, i.e. m is the outcome regression μ(d, x) = E[Y ∣ X = x, D = d].

Formal statement
hypotheses
Pd :
Measure (γ × ℝ)
IsFiniteMeasure Pd
m :
γ → ℝ
hm :
Measurable m
hY :
Integrable (fun z => z.2) Pd
hmint :
Integrable (fun z => m z.1) Pd
hproj :
IsL2Projection Pd m
conclusion
(fun z => m z.1) =ᵐ[Pd] (Pd[fun z => z.2 | covarSigma (X := γ)])
Proof (Lean source)
theorem mlOutcomeRegression_ae_eq (Pd : Measure (γ × ℝ)) [IsFiniteMeasure Pd] {m : γ → ℝ} (hm : Measurable m) (hY : Integrable (fun z => z.2) Pd) (hmint : Integrable (fun z => m z.1) Pd) (hproj : IsL2Projection Pd m) : (fun z => m z.1) =ᵐ[Pd] (Pd[fun z => z.2 | covarSigma (X := γ)]) := condExp_of_isL2Projection Pd hm hY hmint hproj
Causalean.ML.Causal.mlOutcomeRegression_ae_eq · Causalean/ML/CausalApplication/Nuisance.lean:26 · uses covarSigma , IsL2Projection
theorem mlPropensity_ae_eq reviewed
Causalean.ML.Causal

Propensity recovery. On a finite covariate–treatment-indicator law Pe, if the candidate propensity function e is measurable, the treatment indicator is integrable, the composed function z ↦ e(z.1) is integrable, and e is the squared-loss population target — its residual is uncorrelated with every measurable, integrable function of the covariate, then e agrees Pe-almost everywhere with the conditional expectation of the treatment indicator given the covariate σ-algebra, i.e. e is the propensity P(D = 1 ∣ X).

Formal statement
hypotheses
Pe :
Measure (γ × ℝ)
IsFiniteMeasure Pe
e :
γ → ℝ
he :
Measurable e
hD :
Integrable (fun z => z.2) Pe
heint :
Integrable (fun z => e z.1) Pe
hproj :
IsL2Projection Pe e
conclusion
(fun z => e z.1) =ᵐ[Pe] (Pe[fun z => z.2 | covarSigma (X := γ)])
Proof (Lean source)
theorem mlPropensity_ae_eq (Pe : Measure (γ × ℝ)) [IsFiniteMeasure Pe] {e : γ → ℝ} (he : Measurable e) (hD : Integrable (fun z => z.2) Pe) (heint : Integrable (fun z => e z.1) Pe) (hproj : IsL2Projection Pe e) : (fun z => e z.1) =ᵐ[Pe] (Pe[fun z => z.2 | covarSigma (X := γ)]) := condExp_of_isL2Projection Pe he hD heint hproj
Causalean.ML.Causal.mlPropensity_ae_eq · Causalean/ML/CausalApplication/Nuisance.lean:41 · uses covarSigma , IsL2Projection
def mlNuisanceVec reviewed
Causalean.ML.Causal

Package ML-learned outcome arms μ_fn and propensity e_fn into the AIPW nuisance vector consumed by Estimation.ATE.

Definition (Lean source)
noncomputable def mlNuisanceVec (μ_fn : Bool → γ → ℝ) (e_fn : γ → ℝ) (hμ : ∀ b, Measurable (μ_fn b)) (he : Measurable e_fn) : NuisanceVec γ where μ_fn := μ_fn e_fn := e_fn μ_meas := hμ e_meas := he
Causalean.ML.Causal.mlNuisanceVec · Causalean/ML/CausalApplication/Nuisance.lean:55 · uses NuisanceVec
AIPWExample 1 core · 0 supporting The payoff of the causal bridge. ★ aipw_mlNuisance_meanZero_of_wellSpecified

End-to-end: ML nuisances → AIPW → the ATE

The payoff of the causal bridge. When the Causalean.ML learners recover the true nuisances, their packaged NuisanceVec makes the AIPW estimating equation mean-zero at the average treatment effect. The squared-loss recovery statements live in ML/CausalApplication/Nuisance; logistic or other learners can enter this theorem after their own population-target results show equality with the same true outcome-regression or propensity functions. This composes the ML side with the existing Estimation.ATE AIPW identification (aipw_mean_zero).

theorem aipw_mlNuisance_meanZero_of_wellSpecified reviewed
Causalean.ML.Causal

End-to-end identification with ML nuisances. In a backdoor estimation system S, suppose the propensity is bounded away from 0 and 1 by ε (strict overlap), the backdoor identification assumptions hold, the squared factual outcome is integrable, and the squared potential outcome under each treatment arm is integrable. If the ML-learned outcome-regression functions and propensity function are measurable and agree pointwise with the true outcome regression and true propensity, respectively (correct specification), then the AIPW moment functional built from the ML-learned nuisance vector integrates to zero at the true average treatment effect S.θ₀ — the doubly-robust estimating equation identifies the ATE with machine-learned nuisances.

Formal statement
hypotheses
S :
BackdoorEstimationSystem P γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
hA :
S.toPOBackdoorSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ
h_yd2 :
∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ
mhat :
Bool → γ → ℝ
ehat :
γ → ℝ
hmhat :
∀ b, Measurable (mhat b)
hehat :
Measurable ehat
hμ_spec :
∀ b x, mhat b x = S.μ_val b x
he_spec :
∀ x, ehat x = S.e_val x
conclusion
(∫ z, BackdoorEstimationSystem.aipwMomentFunctional (mlNuisanceVec mhat ehat hmhat hehat) z S.θ₀ ∂ S.P_Z)
= 0
Proof (Lean source)
theorem aipw_mlNuisance_meanZero_of_wellSpecified (S : BackdoorEstimationSystem P γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) {mhat : Bool → γ → ℝ} {ehat : γ → ℝ} (hmhat : ∀ b, Measurable (mhat b)) (hehat : Measurable ehat) (hμ_spec : ∀ b x, mhat b x = S.μ_val b x) (he_spec : ∀ x, ehat x = S.e_val x) : (∫ z, BackdoorEstimationSystem.aipwMomentFunctional (mlNuisanceVec mhat ehat hmhat hehat) z S.θ₀ ∂ S.P_Z) = 0 := by have hηeq : mlNuisanceVec mhat ehat hmhat hehat = BackdoorEstimationSystem.η₀ S := NuisanceVec.ext hμ_spec he_spec have hfun : (fun z => BackdoorEstimationSystem.aipwMomentFunctional (mlNuisanceVec mhat ehat hmhat hehat) z S.θ₀) = S.ψ_AIPW := by funext z rw [hηeq] rfl rw [hfun] exact BackdoorEstimationSystem.aipw_mean_zero_of_square_integrable S h_overlap hA h_y2 h_yd2
Causalean.ML.Causal.aipw_mlNuisance_meanZero_of_wellSpecified · Causalean/ML/CausalApplication/AIPWExample.lean:27 · uses BackdoorEstimationSystem , P_Z , StrictOverlap , aipwMomentFunctional , θ₀ , mlNuisanceVec , Assumptions , YofD , factualY , POSystem
Rate­Assembly 1 core · 1 supporting The mechanism that consumes per-method L²-estimation rates (proven in the method folders, expressed via ML/Core/Rate) and discharges the three nuisance-rate hypotheses of Estimation.ATE.dml_ATE_tendstoNormal. ★ dml_rate_conditions_of_quarter_rates

Assembly: per-method rates ⇒ DML nuisance-rate conditions

The mechanism that consumes per-method L²-estimation rates (proven in the method folders, expressed via ML/Core/Rate) and discharges the three nuisance-rate hypotheses of Estimation.ATE.dml_ATE_tendstoNormal.

It is method-agnostic: ridge, OLS, logistic — once each proves an o_p(n^{-1/4}) L²-rate toward its population target (which the Step-1/2 bridge identifies with the causal nuisance) — plug their error sequences in as μErr / eErr. Instantiating μErr a n ω := (eLpNorm (fun x => μ̂ n ω a x − μ_val a x) 2 P_X).toReal (and eErr analogously) makes the three outputs literally DML's h_mu_rate / h_e_rate / h_product_rate.

theorem dml_rate_conditions_of_quarter_rates reviewed
Causalean.ML.Causal

Assembly. If, for every treatment arm, the outcome-regression estimation error is o_p(n^{-1/4}), and the propensity estimation error is o_p(n^{-1/4}), then each error is separately o_p(1), and for every arm the pointwise product of the outcome and propensity errors is o_p(n^{-1/2}) — together these are DML's three nuisance-rate conditions.

Formal statement
hypotheses
μErr :
Bool → ℕ → Ω → ℝ
eErr :
ℕ → Ω → ℝ
hμ :
∀ a, IsLittleOp (μErr a) (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ
he :
IsLittleOp eErr (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ
conclusion
(∀ a, IsLittleOp (μErr a) (fun _ => 1) μ) ∧
IsLittleOp eErr (fun _ => 1) μ ∧
(∀ a, IsLittleOp (fun n ω => μErr a n ω * eErr n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ)
Proof (Lean source)
theorem dml_rate_conditions_of_quarter_rates {μErr : Bool → ℕ → Ω → ℝ} {eErr : ℕ → Ω → ℝ} (hμ : ∀ a, IsLittleOp (μErr a) (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) (he : IsLittleOp eErr (fun n => (n : ℝ) ^ (-(1 / 4 : ℝ))) μ) : (∀ a, IsLittleOp (μErr a) (fun _ => 1) μ) ∧ IsLittleOp eErr (fun _ => 1) μ ∧ (∀ a, IsLittleOp (fun n ω => μErr a n ω * eErr n ω) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) := ⟨fun a => isLittleOp_one_of_le_one rpow_quarter_le_one (hμ a), isLittleOp_one_of_le_one rpow_quarter_le_one he, fun a => isLittleOp_mul_quarter (hμ a) he⟩
Causalean.ML.Causal.dml_rate_conditions_of_quarter_rates · Causalean/ML/CausalApplication/RateAssembly.lean:36 · uses IsLittleOp
1 supporting declaration (lemmas, instances)
  • rpow_quarter_le_one theorem — The n^{-1/4} rate is bounded by 1 (so it weakens to the o_p(1) rate).
    hypotheses
    n :
    ℕ
    conclusion
    (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ 1
    Proof (Lean source)
    theorem rpow_quarter_le_one (n : ℕ) : (n : ℝ) ^ (-(1 / 4 : ℝ)) ≤ 1 := by rcases Nat.eq_zero_or_pos n with hn | hn · subst hn simp · have h1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn exact Real.rpow_le_one_of_one_le_of_nonpos h1 (by norm_num)
    Causalean.ML.Causal.rpow_quarter_le_one · Causalean/ML/CausalApplication/RateAssembly.lean:28