Estimation.OrthogonalLearning.Population
Population-side orthogonal-learning definitions: directional derivatives, Neyman orthogonality, and nuisance-induced second-order bias.
DirectionalDeriv 4 core · 0 supporting This file packages directional derivatives of an orthogonal statistical-learning loss in the target coordinate, the nuisance coordinate, and the mixed target-nuisance coordinate.
Directional Derivatives for Losses
This file packages directional derivatives of an orthogonal statistical-learning loss in the target coordinate, the nuisance coordinate, and the mixed target-nuisance coordinate. These derivative bundles provide the analytic inputs used to state first-order optimality and Neyman orthogonality for population risks.
The public bundles are HasDirDerivTheta, HasDirDerivG, and
HasMixedDirDeriv. The predicate FirstOrderInequality records the integrated
target-direction first-order condition at the true nuisance.
Directional derivative of the learning-system loss in the target coordinate, at a fixed nuisance g. Bundles a candidate directional-derivative function dℓ_θ, giving a real number for each target θ and observation z, the witness that for every target θ in the system's target class and every observation z, the loss's difference quotient along the segment from θ₀ to θ at nuisance g converges to dℓ_θ θ z as the step size shrinks to zero, and measurability of dℓ_θ θ in the observation for every target θ.
Definition (Lean source)
Pointwise directional derivative of g ↦ ℓ z θ₀ g along the segment from g₀ to g, packaged with the pointwise tendsto witness and measurability.
Definition (Lean source)
Mixed target-nuisance directional derivative of the learning-system loss, at the truth (θ₀, g₀). Bundles a target-direction directional-derivative bundle Dθ_at g anchored at every accessible nuisance value g, a real-valued mixed directional-derivative function dℓ_θg of the target, the nuisance, and the observation, the witness that for every target θ and nuisance g in the system's classes and every observation z, the target-direction derivative anchored at the perturbed nuisance g₀ + t(g - g₀) converges, as t → 0, to dℓ_θg θ g z, and measurability of dℓ_θg θ g in the observation for every target θ and nuisance g.
Definition (Lean source)
Population first-order inequality at the truth: for every admissible target θ ∈ Θ_set, the integrated target directional derivative at the true nuisance is non-negative. This is the population KKT condition characterising θ₀ as a minimizer of L(·, g₀) over the convex set Θ_set.
Definition (Lean source)
NeymanOrthogonal 5 core · 0 supporting This file formulates Neyman orthogonality for an orthogonal statistical-learning loss as the vanishing of the integrated mixed directional derivative in every admissible target and nuisance direction. ★ neymanOrthog_iff_score_deriv_zero
Neyman Orthogonality for Losses
This file formulates Neyman orthogonality for an orthogonal statistical-learning loss as the vanishing of the integrated mixed directional derivative in every admissible target and nuisance direction. It also records the domination assumptions needed to pass between pointwise directional derivatives and derivatives of the population risk.
The main predicate is NeymanOrthogLoss. The auxiliary predicates
DiffQuotientEnvelopeTheta, DiffQuotientEnvelopeG, and MixedScoreDCTBridge
package dominated-convergence hypotheses, and
neymanOrthog_iff_score_deriv_zero proves the score-derivative reformulation
under the bridge hypothesis.
Neyman orthogonality of the loss: for every admissible target and nuisance direction, the integrated mixed directional derivative at (θ₀, g₀) vanishes.
Definition (Lean source)
L¹(P_Z) envelope dominating the target-direction difference quotient of the loss locally near t = 0, uniformly in θ ∈ Θ_set. Mirrors Estimation.OrthogonalMoments.DiffQuotientEnvelope.
Definition (Lean source)
L¹(P_Z) envelope dominating the nuisance-direction difference quotient of the loss locally near t = 0, uniformly in g ∈ G_set. Mirrors Estimation.OrthogonalMoments.DiffQuotientEnvelope.
Definition (Lean source)
DCT-bridge hypothesis for the score reformulation: for every admissible target direction ν_θ = θ - θ₀ and nuisance direction ν_g = g - g₀, the integrated centred difference quotient of the target dir derivatives along the nuisance perturbation tends to the integrated mixed dir derivative ∫ z, M.dℓ_θg θ g z ∂P_Z as t → 0 along 𝓝[≠] 0.
Definition (Lean source)
Score reformulation of Neyman orthogonality. Assume the DCT-bridge condition — the integrated centred target-direction difference quotient along a nuisance perturbation converges to the integrated mixed directional derivative as the perturbation size tends to zero. Then Neyman orthogonality of the loss is equivalent to the score map g' ↦ D_θ L(θ₀, g')[ν_θ] having zero first derivative at g₀, for every admissible target direction ν_θ.
Formal statement
Proof (Lean source)
SecondOrderBias 1 core · 0 supporting This file defines the nuisance-induced bias term for a sample-split orthogonal statistical learning system.
Second-Order Bias in Orthogonal Statistical Learning
This file defines the nuisance-induced bias term for a sample-split orthogonal statistical learning system. The term compares the integrated target-direction derivative at the true nuisance with the corresponding derivative at a plug-in nuisance, and the file records the intended second-order Taylor representation.
The exported definition is Bias_n, the difference between the target-gradient
population-risk derivative at the true nuisance and at the plug-in nuisance,
evaluated in the estimator direction. The quantitative Taylor expansion is
documented as a later API extension rather than exported here.
Loss-gradient nuisance bias for a sample-split plug-in ERM.