Estimation.CATE.Orthogonal­Learning.DRLearner

η₀ :

NuisanceVec γ

def

BoundedNuisanceDirs η₀ :

Set (NuisanceVec γ)

given by

{ η | (∃ Cμ : ℝ, ∀ b : Bool, ∀ x : γ, |(η - η₀).μ_fn b x| ≤ Cμ) ∧ (∃ Ce : ℝ, ∀ x : γ, |(η - η₀).e_fn x| ≤ Ce) }

Causalean.Estimation.OrthogonalLearning.BoundedNuisanceDirs · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner.lean:59 · uses NuisanceVec

def DRThetaMinimizes reviewed

Causalean.Estimation.OrthogonalLearning

For a CATE estimation system with a standard Borel unit space and finite population measure, a candidate target set, a candidate target, and an evaluation map from candidate targets to functions of the covariates, the DR-Learner target-minimization condition states that, for every target in the candidate set, the population squared error between the true-nuisance augmented inverse-probability-weighted pseudo-outcome and the evaluation of the designated target is no greater than the corresponding squared error for that target.

Definition (Lean source)

parameters

P :

γ :

Type*

S :

Θ :

Type*

Θ_set :

Set Θ

θ₀ :

eval :

Θ → γ → ℝ

θ ∈ Θ_set :

def

DRThetaMinimizes S Θ_set θ₀ eval :

Prop

given by

∫ z, (phi_eta z S.toBackdoorEstimationSystem.η₀ - eval θ₀ z.1)^2 ∂S.toBackdoorEstimationSystem.P_Z

≤ ∫ z, (phi_eta z S.toBackdoorEstimationSystem.η₀ - eval θ z.1)^2 ∂S.toBackdoorEstimationSystem.P_Z

Causalean.Estimation.OrthogonalLearning.DRThetaMinimizes · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner.lean:100 · uses CATEEstimationSystem , POSystem

def DRClampedThetaMinimizes reviewed

Causalean.Estimation.OrthogonalLearning

For a CATE estimation system with a standard Borel unit space and finite population measure, a candidate target set, a candidate target, an evaluation map from candidate targets to functions of the covariates, and a real clamp radius, the clamped DR-Learner target-minimization condition states that, for every target in the candidate set, the population risk obtained by clamping the true-nuisance squared pseudo-outcome error to the interval $[-b,b]$ is no greater for the designated target than for that target.

Definition (Lean source)

parameters

P :

γ :

Type*

S :

Θ :

Type*

Θ_set :

Set Θ

θ₀ :

eval :

Θ → γ → ℝ

b :

ℝ

θ ∈ Θ_set :

def

DRClampedThetaMinimizes S Θ_set θ₀ eval b :

Prop

given by

∫ z, max (-b) (min b ((phi_eta z S.toBackdoorEstimationSystem.η₀ - eval θ₀ z.1)^2)) ∂S.toBackdoorEstimationSystem.P_Z

≤ ∫ z, max (-b) (min b ((phi_eta z S.toBackdoorEstimationSystem.η₀ - eval θ z.1)^2)) ∂S.toBackdoorEstimationSystem.P_Z

Causalean.Estimation.OrthogonalLearning.DRClampedThetaMinimizes · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner.lean:120 · uses CATEEstimationSystem , POSystem

def drLearningSystem reviewed

Causalean.Estimation.OrthogonalLearning

Given a CATE estimation system with a standard Borel unit space and finite population measure, a real inner-product target space, a convex candidate target set, a designated candidate target belonging to that set, an evaluation map whose evaluation is measurable for every candidate, the condition that the designated target evaluates pointwise to the system's conditional average treatment effect, and the condition that it minimizes the true-nuisance population squared pseudo-outcome risk over the candidate set, the DR-Learner orthogonal statistical-learning system has observed-data law given by the CATE system, nuisance functions given by outcome regressions and a propensity score, and squared augmented inverse-probability-weighted pseudo-outcome loss.

Definition (Lean source)

parameters

P :

γ :

Type*

S :

Θ :

Type*

Θ_set :

Set Θ

Θ_convex :

Convex ℝ Θ_set

θ₀ :

θ₀_mem :

θ₀ ∈ Θ_set

eval :

Θ → γ → ℝ

eval_meas :

∀ θ, Measurable (eval θ)

_eval_θ₀ :

∀ x, eval θ₀ x = S.τ_val x

θ₀_minimizes :

DRThetaMinimizes S Θ_set θ₀ eval

def

drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas _eval_θ₀ θ₀_minimizes :

LearningSystem P.Ω P.μ (γ × Bool × ℝ) S.toBackdoorEstimationSystem.P_Z Θ (NuisanceVec γ)

given by

clause 1

Θ_set := Θ_set

clause 2

Θ_convex := Θ_convex

clause 3

θ₀ := θ₀

clause 4

θ₀_mem := θ₀_mem

clause 5

G_set := BoundedNuisanceDirs S.toBackdoorEstimationSystem.η₀

clause 6

g₀ := S.toBackdoorEstimationSystem.η₀

clause 7

g₀_mem := anchor_mem_boundedNuisanceDirs _

clause 8

ℓ := fun z θ η => (phi_eta z η - eval θ z.1)^2

clause 9

ℓ_meas := by intro θ η have h1 : Measurable (fun z : γ × Bool × ℝ => phi_eta z η) := measurable_phi_eta η have h2 : Measurable (fun z : γ × Bool × ℝ => eval θ z.1) := (eval_meas θ).comp measurable_fst exact (h1.sub h2).pow_const 2

clause 10

θ₀_minimizes := θ₀_minimizes

Causalean.Estimation.OrthogonalLearning.drLearningSystem · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner.lean:142 · uses P_Z , NuisanceVec , instAddCommGroup , instModuleReal , CATEEstimationSystem , τ_val , DRThetaMinimizes , LearningSystem , POSystem

theorem drNeymanOrthog_witness reviewed

Causalean.Estimation.OrthogonalLearning

DR-Learner loss orthogonality (prop:est-osl-dr-loss-orthogonal). For a CATE estimation system built on a potential-outcome model that satisfies the back-door identification assumptions with the propensity score bounded away from 0 and 1 by some margin (strict overlap), fix a convex candidate target class inside an inner-product space together with a real-valued evaluation map on it, and suppose the candidate θ₀ belongs to this class, every candidate's evaluation is measurable, θ₀'s evaluation agrees pointwise with the true value-space CATE, and θ₀ minimizes the population AIPW pseudo-outcome squared-loss risk against the true nuisance over the candidate class. If, for the resulting DR-Learner learning system, a dominated-convergence bridge licenses passing the limit defining the mixed target/nuisance directional derivative through the integral and the integrated target-directional score has vanishing derivative, at every point of the bounded nuisance slice and for every candidate target, along the segment toward that point from the true nuisance, then the DR-Learner squared loss is Neyman-orthogonal: its integrated mixed directional derivative between target and nuisance directions vanishes at the truth (θ₀, η₀) for every admissible target and nuisance direction.

Formal statement

hypotheses

P :

γ :

Type*

S :

_hA :

S.toPOBackdoorSystem.Assumptions

_hOverlap :

∃ ε > 0, S.toBackdoorEstimationSystem.StrictOverlap ε

Θ :

Type*

Θ_set :

Set Θ

Θ_convex :

Convex ℝ Θ_set

θ₀ :

θ₀_mem :

θ₀ ∈ Θ_set

eval :

Θ → γ → ℝ

eval_meas :

∀ θ, Measurable (eval θ)

eval_θ₀ :

∀ x, eval θ₀ x = S.τ_val x

θ₀_minimizes :

DRThetaMinimizes S Θ_set θ₀ eval

M :

HasMixedDirDeriv (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes)

hBridge :

MixedScoreDCTBridge (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) M

hScoreFlat :

∀ θ ∈ Θ_set,

∀ η ∈ BoundedNuisanceDirs S.toBackdoorEstimationSystem.η₀,

Tendsto (fun t : ℝ => ((∫ z, (M.Dθ_at (S.toBackdoorEstimationSystem.η₀ + t • (η - S.toBackdoorEstimationSystem.η₀))).dℓ_θ θ z ∂S.toBackdoorEstimationSystem.P_Z) - (∫ z, (M.Dθ_at S.toBackdoorEstimationSystem.η₀).dℓ_θ θ z ∂S.toBackdoorEstimationSystem.P_Z)) / t) (𝓝[≠] 0) (𝓝 0)

conclusion

NeymanOrthogLoss (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) M

Proof (Lean source)

theorem drNeymanOrthog_witness {P : POSystem} {γ : Type*} [MeasurableSpace γ] [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (S : CATEEstimationSystem P γ) (_hA : S.toPOBackdoorSystem.Assumptions) (_hOverlap : ∃ ε > 0, S.toBackdoorEstimationSystem.StrictOverlap ε) (Θ : Type*) [NormedAddCommGroup Θ] [InnerProductSpace ℝ Θ] (Θ_set : Set Θ) (Θ_convex : Convex ℝ Θ_set) (θ₀ : Θ) (θ₀_mem : θ₀ ∈ Θ_set) (eval : Θ → γ → ℝ) (eval_meas : ∀ θ, Measurable (eval θ)) (eval_θ₀ : ∀ x, eval θ₀ x = S.τ_val x) (θ₀_minimizes : DRThetaMinimizes S Θ_set θ₀ eval) (M : HasMixedDirDeriv (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes)) (hBridge : MixedScoreDCTBridge (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) M) (hScoreFlat : ∀ θ ∈ Θ_set, ∀ η ∈ BoundedNuisanceDirs S.toBackdoorEstimationSystem.η₀, Tendsto (fun t : ℝ => ((∫ z, (M.Dθ_at (S.toBackdoorEstimationSystem.η₀ + t • (η - S.toBackdoorEstimationSystem.η₀))).dℓ_θ θ z ∂S.toBackdoorEstimationSystem.P_Z) - (∫ z, (M.Dθ_at S.toBackdoorEstimationSystem.η₀).dℓ_θ θ z ∂S.toBackdoorEstimationSystem.P_Z)) / t) (𝓝[≠] 0) (𝓝 0)) : NeymanOrthogLoss (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) M := (neymanOrthog_iff_score_deriv_zero _ M hBridge).mpr hScoreFlat

Causalean.Estimation.OrthogonalLearning.drNeymanOrthog_witness · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner.lean:193 · uses P_Z , StrictOverlap , η₀ , NuisanceVec , instAdd , instAddCommGroup , instModuleReal , instSMulReal , instSub , CATEEstimationSystem , τ_val , BoundedNuisanceDirs , DRThetaMinimizes , HasMixedDirDeriv , MixedScoreDCTBridge , NeymanOrthogLoss , drLearningSystem , Assumptions , POSystem

1 supporting declaration (lemmas, instances)

anchor_mem_boundedNuisanceDirs lemma — The anchor η₀ belongs to BoundedNuisanceDirs η₀ (with Cμ = Ce = 0).

hypotheses

γ :

Type*
MeasurableSpace γ

η₀ :

NuisanceVec γ

conclusion

η₀ ∈ BoundedNuisanceDirs η₀

Proof (Lean source)

lemma anchor_mem_boundedNuisanceDirs {γ : Type*} [MeasurableSpace γ] (η₀ : NuisanceVec γ) : η₀ ∈ BoundedNuisanceDirs η₀ := by refine ⟨⟨0, ?_⟩, ⟨0, ?_⟩⟩ · intro b x have hμ : (η₀ - η₀).μ_fn b x = 0 := by change η₀.μ_fn b x - η₀.μ_fn b x = 0 ring rw [hμ, abs_zero] · intro x have he : (η₀ - η₀).e_fn x = 0 := by change η₀.e_fn x - η₀.e_fn x = 0 ring rw [he, abs_zero]

Causalean.Estimation.OrthogonalLearning.anchor_mem_boundedNuisanceDirs · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner.lean:83

Analytic 4 core · 2 supporting Packages analytic derivative data for the DR-Learner orthogonal-learning system. ★ drNeymanOrthog

Packages analytic derivative data for the DR-Learner orthogonal-learning system. It defines the EvalDirDeriv and NuisanceDirDeriv bundles, builds the closed-form mixed derivative drMixedDirDeriv, proves the bounded-direction score-zero lemma dr_scoreZero_of_bounded, derives score flatness in dr_scoreFlat, and combines these ingredients in drNeymanOrthog.

structure EvalDirDeriv reviewed

Causalean.Estimation.OrthogonalLearning

A pointwise directional-derivative bundle for a candidate evaluation map along the segment from a base point to a candidate parameter: it packages the derivative's value at each covariate together with the fact that the map's difference quotient along the segment converges to that value as the perturbation parameter vanishes, the derivative's measurability in the covariate, and a uniform bound on the derivative over the parameter set.

Definition (Lean source)

parameters

Θ :

Type*

γ :

Type*

Θ_set :

Set Θ

θ₀ :

eval :

Θ → γ → ℝ

fields

dEval :

Θ → γ → ℝ

pointwise :

∀ θ ∈ Θ_set,

∀ x : γ,

Tendsto (fun t : ℝ => (eval (θ₀ + t • (θ - θ₀)) x - eval θ₀ x) / t) (𝓝[≠] 0) (𝓝 (dEval θ x))

meas :

∀ θ, Measurable (dEval θ)

bound :

∀ θ ∈ Θ_set, ∃ M_dEval : ℝ, ∀ x : γ, |dEval θ x| ≤ M_dEval

Causalean.Estimation.OrthogonalLearning.EvalDirDeriv · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner/Analytic.lean:59

structure NuisanceDirDeriv reviewed

Causalean.Estimation.OrthogonalLearning

A nuisance derivative bundle records, for the doubly robust pseudo-outcome, its directional derivative in each nuisance direction as the limit of the corresponding difference quotient, together with that derivative's measurability.

Definition (Lean source)

parameters

γ :

Type*

g₀ :

NuisanceVec γ

fields

The dir-derivative value `D_g phi_eta(z, g₀)[η − g₀]`.

dPhi :

NuisanceVec γ → (γ × Bool × ℝ) → ℝ

pointwise :

∀ η : NuisanceVec γ,

∀ z : γ × Bool × ℝ,

Tendsto (fun t : ℝ => (phi_eta z (g₀ + t • (η - g₀)) - phi_eta z g₀) / t) (𝓝[≠] 0) (𝓝 (dPhi η z))

meas :

∀ η, Measurable (dPhi η)

Causalean.Estimation.OrthogonalLearning.NuisanceDirDeriv · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner/Analytic.lean:90 · uses NuisanceVec

def drMixedDirDeriv reviewed

Causalean.Estimation.OrthogonalLearning

For a potential-outcome system with a standard-Borel sample space and a finite measure, a covariate space with its σ-algebra, a CATE estimation system, its causal identification assumptions, a strictly positive overlap bound, and membership of the system's true nuisance in the corresponding overlap class, together with a target inner-product space, a convex target-parameter set, a target parameter in that set, a measurable target-evaluation rule that equals the true conditional treatment effect at the target parameter, a statement that this parameter minimizes the doubly robust target criterion, an evaluation-rule directional-derivative bundle, and a nuisance directional-derivative bundle, the mixed directional-derivative bundle for the resulting doubly robust learning system is given by the displayed closed-form derivatives.

Definition (Lean source)

parameters

P :

γ :

Type*

S :

_hA :

S.toPOBackdoorSystem.Assumptions

ε :

ℝ

_hε_pos :

0 < ε

_h_overlap_η₀ :

S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε

Θ :

Type*

Θ_set :

Set Θ

Θ_convex :

Convex ℝ Θ_set

θ₀ :

θ₀_mem :

θ₀ ∈ Θ_set

eval :

Θ → γ → ℝ

eval_meas :

∀ θ, Measurable (eval θ)

eval_θ₀ :

∀ x, eval θ₀ x = S.τ_val x

θ₀_minimizes :

DRThetaMinimizes S Θ_set θ₀ eval

D :

EvalDirDeriv Θ_set θ₀ eval

ND :

NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀

def

drMixedDirDeriv S _hA _hε_pos _h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND :

HasMixedDirDeriv (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes)

given by

clause 1

Dθ_at := fun η

=> { dℓ_θ := fun θ z => -2 * (phi_eta z η - eval θ₀ z.1) * D.dEval θ z.1 pointwise_tendsto := by intro θ hθ z have hq := D.pointwise θ hθ z.1 have ht : Tendsto (fun t : ℝ => t) (𝓝[≠] (0 : ℝ)) (𝓝 (0 : ℝ)) := tendsto_nhdsWithin_of_tendsto_nhds tendsto_id have hdiff : Tendsto (fun t : ℝ => eval (θ₀ + t • (θ - θ₀)) z.1 - eval θ₀ z.1) (𝓝[≠] 0) (𝓝 0) := by have hmul := ht.mul hq have hmul' : Tendsto (fun t : ℝ => t * ((eval (θ₀ + t • (θ - θ₀)) z.1 - eval θ₀ z.1) / t)) (𝓝[≠] 0) (𝓝 0) := by simpa using hmul refine hmul'.congr' ?_ filter_upwards [self_mem_nhdsWithin] with t htne have htne' : t ≠ 0 := by simpa using htne field_simp [htne'] have heval : Tendsto (fun t : ℝ => eval (θ₀ + t • (θ - θ₀)) z.1) (𝓝[≠] 0) (𝓝 (eval θ₀ z.1)) := by have h := hdiff.add (tendsto_const_nhds (x := eval θ₀ z.1)) simpa [sub_add_cancel] using h have hsum : Tendsto (fun t : ℝ => (phi_eta z η - eval (θ₀ + t • (θ - θ₀)) z.1) + (phi_eta z η - eval θ₀ z.1)) (𝓝[≠] 0) (𝓝 (2 * (phi_eta z η - eval θ₀ z.1))) := by simpa [two_mul, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using ((tendsto_const_nhds (x := phi_eta z η)).sub heval).add (tendsto_const_nhds (x := phi_eta z η - eval θ₀ z.1)) have hfirst : Tendsto (fun t : ℝ => -((eval (θ₀ + t • (θ - θ₀)) z.1 - eval θ₀ z.1) / t)) (𝓝[≠] 0) (𝓝 (-D.dEval θ z.1)) := hq.neg have hprod : Tendsto (fun t : ℝ => -((eval (θ₀ + t • (θ - θ₀)) z.1 - eval θ₀ z.1) / t) * ((phi_eta z η - eval (θ₀ + t • (θ - θ₀)) z.1) + (phi_eta z η - eval θ₀ z.1))) (𝓝[≠] 0) (𝓝 (-2 * (phi_eta z η - eval θ₀ z.1) * D.dEval θ z.1)) := by simpa [mul_assoc, mul_comm, mul_left_comm] using hfirst.mul hsum refine hprod.congr' ?_ filter_upwards [self_mem_nhdsWithin] with t htne have htne' : t ≠ 0 := by simpa using htne simp [drLearningSystem, pow_two] field_simp [htne'] ring dℓ_θ_meas := by intro θ have hphi : Measurable (fun z : γ × Bool × ℝ => phi_eta z η) := measurable_phi_eta η have heval : Measurable (fun z : γ × Bool × ℝ => eval θ₀ z.1) := (eval_meas θ₀).comp measurable_fst have hdE : Measurable (fun z : γ × Bool × ℝ => D.dEval θ z.1) := (D.meas θ).comp measurable_fst exact (((measurable_const.mul (hphi.sub heval)).mul hdE)) }

clause 2

dℓ_θg := fun θ η z => -2 * ND.dPhi η z * D.dEval θ z.1

clause 3

pointwise_tendsto := by intro θ hθ η hη z have hphi := ND.pointwise η z have hlim : Tendsto (fun t : ℝ => -2 * ((phi_eta z (S.toBackdoorEstimationSystem.η₀ + t • (η - S.toBackdoorEstimationSystem.η₀)) - phi_eta z S.toBackdoorEstimationSystem.η₀) / t) * D.dEval θ z.1) (𝓝[≠] 0) (𝓝 (-2 * ND.dPhi η z * D.dEval θ z.1)) := by simpa [mul_assoc, mul_comm, mul_left_comm] using (((tendsto_const_nhds (x := (-2 : ℝ))).mul hphi).mul (tendsto_const_nhds (x := D.dEval θ z.1))) refine hlim.congr' ?_ filter_upwards [self_mem_nhdsWithin] with t htne have htne' : t

≠ 0 := by simpa using htne simp [drLearningSystem] field_simp [htne'] ring

clause 4

dℓ_θg_meas := by intro θ η have hdPhi : Measurable (fun z : γ × Bool × ℝ => ND.dPhi η z) := ND.meas η have hdE : Measurable (fun z : γ × Bool × ℝ => D.dEval θ z.1) := (D.meas θ).comp measurable_fst exact (measurable_const.mul hdPhi).mul hdE

Causalean.Estimation.OrthogonalLearning.drMixedDirDeriv · Causalean/Estimation/CATE/OrthogonalLearning/DRLearner/Analytic.lean:122 · uses H_ε , P_Z , η₀ , NuisanceVec , instAddCommGroup , instModuleReal , CATEEstimationSystem , τ_val , DRThetaMinimizes , EvalDirDeriv , HasMixedDirDeriv , NuisanceDirDeriv , drLearningSystem , Assumptions , POSystem

theorem drNeymanOrthog reviewed

Causalean.Estimation.OrthogonalLearning

DR-Learner loss orthogonality under a DCT bridge (prop:est-osl-dr-loss-orthogonal). For a CATE estimation system built on a potential-outcome model that satisfies the back-door identification assumptions, fix a margin ε > 0 such that the true nuisance η₀ lies in the strict-overlap slice at that margin, i.e. the propensity score is bounded away from 0 and 1. Fix a convex candidate target class inside an inner-product space together with a real-valued evaluation map on it, and suppose θ₀ belongs to this class, every candidate's evaluation is measurable, θ₀'s evaluation agrees pointwise with the true value-space CATE, and θ₀ minimizes the population AIPW pseudo-outcome squared-loss risk against the true nuisance over the candidate class. Given directional-derivative data for the evaluation map and for the doubly robust pseudo-outcome that together assemble a closed-form mixed directional derivative for the loss, if a dominated-convergence bridge licenses passing the limit defining the integrated mixed target/nuisance score through the integral, then this closed-form derivative witnesses that the DR-Learner squared loss is Neyman-orthogonal: its integrated mixed directional derivative vanishes at the truth (θ₀, η₀) for every admissible target and bounded nuisance direction.

Formal statement

hypotheses

P :

γ :

Type*

S :

hA :

S.toPOBackdoorSystem.Assumptions

ε :

ℝ

hε_pos :

0 < ε

h_overlap_η₀ :

S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε

Θ :

Type*