Estimation.CATE.OrthogonalLearning.DRLearner
Builds the DR-Learner orthogonal-learning system for CATE estimation.
DRLearner 5 core · 1 supporting Builds the DR-Learner orthogonal-learning system for CATE estimation. ★ drNeymanOrthog_witness
Builds the DR-Learner orthogonal-learning system for CATE estimation. It
defines the bounded nuisance slice BoundedNuisanceDirs, target-minimization
predicates for the ordinary and clamped risks, and the drLearningSystem
instance. The theorem drNeymanOrthog_witness adapts abstract score-flatness
and dominated-convergence hypotheses into a NeymanOrthogLoss witness for the
DR-Learner squared loss.
def BoundedNuisanceDirs reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
Bounded-direction nuisance slice anchored at η₀.
Definition (Lean source)
def BoundedNuisanceDirs
{γ : Type*} [MeasurableSpace γ] (η₀ : NuisanceVec γ) :
Set (NuisanceVec γ) :=
{ η | (∃ Cμ : ℝ, ∀ b : Bool, ∀ x : γ, |(η - η₀).μ_fn b x| ≤ Cμ) ∧
(∃ Ce : ℝ, ∀ x : γ, |(η - η₀).e_fn x| ≤ Ce) }
def DRThetaMinimizes reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
The DR-Learner target θ₀ minimizes the population squared-loss risk against the true nuisance over the candidate target class.
Definition (Lean source)
def DRThetaMinimizes
{P : POSystem} {γ : Type*} [MeasurableSpace γ]
[StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(S : CATEEstimationSystem P γ)
{Θ : Type*} (Θ_set : Set Θ) (θ₀ : Θ) (eval : Θ → γ → ℝ) : Prop :=
∀ θ ∈ Θ_set,
∫ 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
def DRClampedThetaMinimizes reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
The DR-Learner target θ₀ minimizes the clamped true-nuisance squared loss used by almost-everywhere empirical-process reductions.
Definition (Lean source)
def DRClampedThetaMinimizes
{P : POSystem} {γ : Type*} [MeasurableSpace γ]
[StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(S : CATEEstimationSystem P γ)
{Θ : Type*} (Θ_set : Set Θ) (θ₀ : Θ) (eval : Θ → γ → ℝ) (b : ℝ) : Prop :=
∀ θ ∈ Θ_set,
∫ 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
def drLearningSystem reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
The DR-Learner orthogonal-learning system: a LearningSystem whose data law is the CATE observation triple's joint law P_Z, target space Θ is a user-provided convex subset of an inner-product space (with a candidate evaluation map eval : Θ → γ → ℝ), nuisance space G := NuisanceVec γ, and loss
Definition (Lean source)
noncomputable def drLearningSystem
{P : POSystem} {γ : Type*} [MeasurableSpace γ]
[StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(S : CATEEstimationSystem P γ)
(Θ : 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) :
LearningSystem P.Ω P.μ (γ × Bool × ℝ) S.toBackdoorEstimationSystem.P_Z
Θ (NuisanceVec γ) where
Θ_set := Θ_set
Θ_convex := Θ_convex
θ₀ := θ₀
θ₀_mem := θ₀_mem
G_set := BoundedNuisanceDirs S.toBackdoorEstimationSystem.η₀
g₀ := S.toBackdoorEstimationSystem.η₀
g₀_mem := anchor_mem_boundedNuisanceDirs _
ℓ := fun z θ η => (phi_eta z η - eval θ z.1)^2
ℓ_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
θ₀_minimizes := θ₀_minimizes
theorem drNeymanOrthog_witness reviewed
⚑ flagged
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*
IsFiniteMeasure P.μ
S :
_hA :
S.toPOBackdoorSystem.Assumptions
_hOverlap :
∃ ε > 0, S.toBackdoorEstimationSystem.StrictOverlap ε
Θ :
Θ_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
1 supporting declaration (lemmas, instances)
-
anchor_mem_boundedNuisanceDirslemma — The anchor η₀ belongs to BoundedNuisanceDirs η₀ (with Cμ = Ce = 0).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]
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
⚑ flagged
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
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
structure NuisanceDirDeriv reviewed
⚑ flagged
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₀ :
fields
The dir-derivative value `D_g phi_eta(z, g₀)[η − g₀]`.
dPhi :
NuisanceVec γ → (γ × Bool × ℝ) → ℝ
pointwise :
∀ η : NuisanceVec γ,
∀ z : γ × Bool × ℝ,
meas :
∀ η, Measurable (dPhi η)
def drMixedDirDeriv reviewed
⚑ flagged
Causalean.Estimation.OrthogonalLearning
The closed-form HasMixedDirDeriv bundle for the DR-Learner orthogonal-learning system.
Definition (Lean source)
noncomputable def drMixedDirDeriv
{P : POSystem} {γ : Type*} [MeasurableSpace γ]
[StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(S : CATEEstimationSystem P γ)
(_hA : S.toPOBackdoorSystem.Assumptions)
{ε : ℝ} (_hε_pos : 0 < ε)
(_h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈
BackdoorEstimationSystem.H_ε (γ := γ) ε)
(Θ : 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)
(D : EvalDirDeriv Θ_set θ₀ eval)
(ND : NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀) :
HasMixedDirDeriv
(drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) where
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)) }
dℓ_θg := fun θ η z =>
-2 * ND.dPhi η z * D.dEval θ z.1
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
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
theorem drNeymanOrthog reviewed
⚑ flagged
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*
IsFiniteMeasure P.μ
S :
hA :
S.toPOBackdoorSystem.Assumptions
ε :
ℝ
hε_pos :
0 < ε
h_overlap_η₀ :
S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
Θ :
Θ_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.η₀
hBridge :
MixedScoreDCTBridge (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) (drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND)
conclusion
NeymanOrthogLoss (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) (drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND)
Proof (Lean source)
theorem drNeymanOrthog
{P : POSystem} {γ : Type*} [MeasurableSpace γ]
[StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(S : CATEEstimationSystem P γ)
(hA : S.toPOBackdoorSystem.Assumptions)
{ε : ℝ} (hε_pos : 0 < ε)
(h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈
BackdoorEstimationSystem.H_ε (γ := γ) ε)
(Θ : 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)
(D : EvalDirDeriv Θ_set θ₀ eval)
(ND : NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀)
(hBridge :
MixedScoreDCTBridge
(drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes)
(drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀
θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND)) :
NeymanOrthogLoss
(drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes)
(drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀
θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND) :=
(neymanOrthog_iff_score_deriv_zero _ _ hBridge).mpr
(dr_scoreFlat S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem
eval eval_meas eval_θ₀ θ₀_minimizes D ND hBridge)
2 supporting declarations (lemmas, instances)
-
dr_scoreZero_of_boundedlemma — Discharge of hScoreZero for bounded nuisance directions.hypothesesP :γ :Type*IsFiniteMeasure P.μS :hA :S.toPOBackdoorSystem.Assumptionsε :ℝhε_pos :0 < εh_overlap_η₀ :S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) εΘ :Θ_set :Set Θθ₀ :Θeval :Θ → γ → ℝD :EvalDirDeriv Θ_set θ₀ evalND :NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀θ :Θhθ :θ ∈ Θ_setη :h_v_μ_bdd :∃ Cμ : ℝ, ∀ b : Bool, ∀ x : γ, |(η - S.toBackdoorEstimationSystem.η₀).μ_fn b x| ≤ Cμh_v_e_bdd :∃ Ce : ℝ, ∀ x : γ, |(η - S.toBackdoorEstimationSystem.η₀).e_fn x| ≤ Ceconclusion∫ z, ND.dPhi η z * D.dEval θ z.1 ∂S.toBackdoorEstimationSystem.P_Z = 0Proof (Lean source)
lemma dr_scoreZero_of_bounded {P : POSystem} {γ : Type*} [MeasurableSpace γ] [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (S : CATEEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) {ε : ℝ} (hε_pos : 0 < ε) (h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε) (Θ : Type*) [NormedAddCommGroup Θ] [InnerProductSpace ℝ Θ] (Θ_set : Set Θ) (θ₀ : Θ) (eval : Θ → γ → ℝ) (D : EvalDirDeriv Θ_set θ₀ eval) (ND : NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀) (θ : Θ) (hθ : θ ∈ Θ_set) (η : NuisanceVec γ) (h_v_μ_bdd : ∃ Cμ : ℝ, ∀ b : Bool, ∀ x : γ, |(η - S.toBackdoorEstimationSystem.η₀).μ_fn b x| ≤ Cμ) (h_v_e_bdd : ∃ Ce : ℝ, ∀ x : γ, |(η - S.toBackdoorEstimationSystem.η₀).e_fn x| ≤ Ce) : ∫ z, ND.dPhi η z * D.dEval θ z.1 ∂S.toBackdoorEstimationSystem.P_Z = 0 := by let v : NuisanceVec γ := η - S.toBackdoorEstimationSystem.η₀ let fZ : γ × Bool × ℝ → ℝ := fun z => phi_eta_dir_deriv S.toBackdoorEstimationSystem.η₀ v z let scoreZ : γ × Bool × ℝ → ℝ := fun z => fZ z * D.dEval θ z.1 have hND_eq : ∀ z : γ × Bool × ℝ, ND.dPhi η z = fZ z := by intro z have hND := ND.pointwise η z have hclosed : Tendsto (fun t : ℝ => (phi_eta z (S.toBackdoorEstimationSystem.η₀ + t • (η - S.toBackdoorEstimationSystem.η₀)) - phi_eta z S.toBackdoorEstimationSystem.η₀) / t) (𝓝[≠] 0) (𝓝 (fZ z)) := by simpa [v, fZ] using phi_eta_dir_deriv_tendsto S.toBackdoorEstimationSystem.η₀ v hε_pos h_overlap_η₀ z exact tendsto_nhds_unique' (NormedField.nhdsNE_neBot (0 : ℝ)) hND hclosed have hscoreZ_meas : Measurable scoreZ := by have hf : Measurable fZ := by simpa [fZ, v] using measurable_phi_eta_dir_deriv S.toBackdoorEstimationSystem.η₀ v have hg : Measurable (fun z : γ × Bool × ℝ => D.dEval θ z.1) := (D.meas θ).comp measurable_fst exact hf.mul hg obtain ⟨M_dEval, hD_bdd⟩ := D.bound θ hθ have hf_int : Integrable (fun ω => fZ (S.toBackdoorEstimationSystem.factualZ ω)) P.μ := by simpa [fZ, v] using integrable_phi_eta_dir_deriv_factualZ S hA hε_pos h_overlap_η₀ v h_v_μ_bdd h_v_e_bdd have hg_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] (fun ω => D.dEval θ (S.toPOBackdoorSystem.factualX ω)) := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => D.dEval θ (S.toPOBackdoorSystem.factualX ω)) exact ((D.meas θ).comp (comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable have hg_meas : Measurable (fun ω => D.dEval θ (S.toPOBackdoorSystem.factualX ω)) := (D.meas θ).comp S.toPOBackdoorSystem.measurable_factualX have hg_aesm : AEStronglyMeasurable (fun ω => D.dEval θ (S.toPOBackdoorSystem.factualX ω)) P.μ := hg_meas.aestronglyMeasurable have hg_bdd : ∀ᵐ ω ∂P.μ, ‖D.dEval θ (S.toPOBackdoorSystem.factualX ω)‖ ≤ M_dEval := Filter.Eventually.of_forall (fun ω => by simpa [Real.norm_eq_abs] using hD_bdd (S.toPOBackdoorSystem.factualX ω)) have hscore_Ω_int' : Integrable (fun ω => fZ (S.toBackdoorEstimationSystem.factualZ ω) * D.dEval θ (S.toPOBackdoorSystem.factualX ω)) P.μ := hf_int.mul_bdd hg_aesm hg_bdd have hscore_comp_int : Integrable (scoreZ ∘ S.toBackdoorEstimationSystem.factualZ) P.μ := by refine hscore_Ω_int'.congr (Filter.Eventually.of_forall ?_) intro ω simp [scoreZ, BackdoorEstimationSystem.factualZ] have hscore_int : Integrable scoreZ (Measure.map S.toBackdoorEstimationSystem.factualZ P.μ) := (MeasureTheory.integrable_map_measure hscoreZ_meas.aestronglyMeasurable S.toBackdoorEstimationSystem.measurable_factualZ.aemeasurable).2 hscore_comp_int have hmap_congr : (fun z : γ × Bool × ℝ => ND.dPhi η z * D.dEval θ z.1) =ᵐ[S.toBackdoorEstimationSystem.P_Z] scoreZ := by exact Filter.Eventually.of_forall (fun z => by simp [scoreZ, hND_eq z]) calc ∫ z, ND.dPhi η z * D.dEval θ z.1 ∂S.toBackdoorEstimationSystem.P_Z = ∫ z, scoreZ z ∂S.toBackdoorEstimationSystem.P_Z := MeasureTheory.integral_congr_ae hmap_congr _ = 0 := by rw [BackdoorEstimationSystem.P_Z] have hpull := MeasureTheory.condExp_mul_of_stronglyMeasurable_right (μ := P.μ) (m := S.toPOBackdoorSystem.sigmaX) hg_sm hscore_Ω_int' hf_int have hinner : P.μ[fun ω => fZ (S.toBackdoorEstimationSystem.factualZ ω) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by simpa [fZ, v] using cond_exp_phi_eta_dir_deriv_at_truth_zero S hA hε_pos h_overlap_η₀ v h_v_μ_bdd h_v_e_bdd have hcond_zero : P.μ[fun ω => fZ (S.toBackdoorEstimationSystem.factualZ ω) * D.dEval θ (S.toPOBackdoorSystem.factualX ω) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by refine hpull.trans ?_ filter_upwards [hinner] with ω hω rw [Pi.mul_apply, hω, zero_mul] calc ∫ z, scoreZ z ∂Measure.map S.toBackdoorEstimationSystem.factualZ P.μ = ∫ ω, scoreZ (S.toBackdoorEstimationSystem.factualZ ω) ∂P.μ := by rw [MeasureTheory.integral_map S.toBackdoorEstimationSystem.measurable_factualZ.aemeasurable hscoreZ_meas.aestronglyMeasurable] _ = ∫ ω, fZ (S.toBackdoorEstimationSystem.factualZ ω) * D.dEval θ (S.toPOBackdoorSystem.factualX ω) ∂P.μ := by refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω simp [scoreZ, BackdoorEstimationSystem.factualZ] _ = ∫ ω, P.μ[fun ω => fZ (S.toBackdoorEstimationSystem.factualZ ω) * D.dEval θ (S.toPOBackdoorSystem.factualX ω) | S.toPOBackdoorSystem.sigmaX] ω ∂P.μ := by rw [MeasureTheory.integral_condExp S.toPOBackdoorSystem.sigmaX_le] _ = ∫ _, (0 : ℝ) ∂P.μ := MeasureTheory.integral_congr_ae hcond_zero _ = 0 := MeasureTheory.integral_zero _ _ -
dr_scoreFlattheorem — The score-flatness hypothesis for drMixedDirDeriv.hypothesesP :γ :Type*IsFiniteMeasure P.μS :hA :S.toPOBackdoorSystem.Assumptionsε :ℝhε_pos :0 < εh_overlap_η₀ :S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) εΘ :Θ_set :Set ΘΘ_convex :Convex ℝ Θ_setθ₀ :Θθ₀_mem :θ₀ ∈ Θ_seteval :Θ → γ → ℝeval_meas :∀ θ, Measurable (eval θ)eval_θ₀ :∀ x, eval θ₀ x = S.τ_val xθ₀_minimizes :DRThetaMinimizes S Θ_set θ₀ evalD :EvalDirDeriv Θ_set θ₀ evalND :NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀hBridge: dominated-convergence bridge for the integrated mixed score quotient.hBridge :MixedScoreDCTBridge (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) (drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND)conclusion∀ θ ∈ Θ_set,∀ η ∈ BoundedNuisanceDirs S.toBackdoorEstimationSystem.η₀,Tendsto (fun t : ℝ => ((∫ z, ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at (S.toBackdoorEstimationSystem.η₀ + t • (η - S.toBackdoorEstimationSystem.η₀))).dℓ_θ θ z ∂S.toBackdoorEstimationSystem.P_Z) - (∫ z, ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at S.toBackdoorEstimationSystem.η₀).dℓ_θ θ z ∂S.toBackdoorEstimationSystem.P_Z)) / t) (𝓝[≠] 0) (𝓝 0)Proof (Lean source)
theorem dr_scoreFlat {P : POSystem} {γ : Type*} [MeasurableSpace γ] [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (S : CATEEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) {ε : ℝ} (hε_pos : 0 < ε) (h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε) (Θ : 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) (D : EvalDirDeriv Θ_set θ₀ eval) (ND : NuisanceDirDeriv S.toBackdoorEstimationSystem.η₀) -- hBridge: dominated-convergence bridge for the integrated mixed score quotient. (hBridge : MixedScoreDCTBridge (drLearningSystem S Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes) (drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND)) : ∀ θ ∈ Θ_set, ∀ η ∈ BoundedNuisanceDirs S.toBackdoorEstimationSystem.η₀, Tendsto (fun t : ℝ => ((∫ z, ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at (S.toBackdoorEstimationSystem.η₀ + t • (η - S.toBackdoorEstimationSystem.η₀))).dℓ_θ θ z ∂S.toBackdoorEstimationSystem.P_Z) - (∫ z, ((drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).Dθ_at S.toBackdoorEstimationSystem.η₀).dℓ_θ θ z ∂S.toBackdoorEstimationSystem.P_Z)) / t) (𝓝[≠] 0) (𝓝 0) := by intro θ hθ η hη have hlim := hBridge θ hθ η hη obtain ⟨h_v_μ_bdd, h_v_e_bdd⟩ := hη have hScoreZero : ∫ z, ND.dPhi η z * D.dEval θ z.1 ∂S.toBackdoorEstimationSystem.P_Z = 0 := dr_scoreZero_of_bounded S hA hε_pos h_overlap_η₀ Θ Θ_set θ₀ eval D ND θ hθ η h_v_μ_bdd h_v_e_bdd have hzero : ∫ z, (drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).dℓ_θg θ η z ∂S.toBackdoorEstimationSystem.P_Z = 0 := by calc ∫ z, (drMixedDirDeriv S hA hε_pos h_overlap_η₀ Θ Θ_set Θ_convex θ₀ θ₀_mem eval eval_meas eval_θ₀ θ₀_minimizes D ND).dℓ_θg θ η z ∂S.toBackdoorEstimationSystem.P_Z = -2 * ∫ z, ND.dPhi η z * D.dEval θ z.1 ∂S.toBackdoorEstimationSystem.P_Z := by simp only [drMixedDirDeriv, neg_mul] rw [show (fun z : γ × Bool × ℝ => -(2 * ND.dPhi η z * D.dEval θ z.1)) = (fun z : γ × Bool × ℝ => (-2) * (ND.dPhi η z * D.dEval θ z.1)) by funext z ring] rw [MeasureTheory.integral_const_mul] ring _ = 0 := by simp [hScoreZero] rw [hzero] at hlim exact hlim