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)
For an orthogonal statistical-learning system and target-direction derivative data for its loss at the distinguished nuisance function, the population first-order inequality holds exactly when, for every target in the system's target class, the integral under the population observation law of the corresponding target directional derivative is nonnegative. This is the population KKT condition characterising the distinguished target as a minimizer of population risk at the distinguished nuisance over the target class.
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.
For an orthogonal statistical-learning system and a bundle of mixed target--nuisance directional derivatives of its loss, the Neyman-orthogonality condition for the loss states that, for every target in the candidate target set and every nuisance function in the admissible nuisance set, the observation-law integral of the mixed directional derivative at those target and nuisance directions equals zero.
Definition (Lean source)
For an orthogonal statistical-learning system and a nuisance function, the target-direction difference-quotient envelope condition states that every candidate target has a positive neighborhood radius and an integrable envelope such that for almost every observation and every nonzero perturbation smaller than that radius, the absolute target-direction loss difference quotient is bounded by the envelope.
Definition (Lean source)
For an orthogonal statistical-learning system, the nuisance-direction difference-quotient envelope condition states that every admissible nuisance function has a positive neighborhood radius and an integrable envelope such that for almost every observation and every nonzero perturbation smaller than that radius, the absolute nuisance-direction loss difference quotient is bounded by the envelope.
Definition (Lean source)
For an orthogonal statistical-learning system and a bundle of mixed target--nuisance directional derivatives of its loss, the mixed-score dominated-convergence bridge states that, for every candidate target and admissible nuisance function, the integrated centered difference quotient of the target-direction derivative along the nuisance perturbation converges, as the nonzero perturbation tends to zero, to the observation-law integral of the corresponding mixed directional derivative.
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.
For an orthogonal statistical-learning system, a target-direction derivative bundle at its true nuisance function, a target-direction derivative bundle at a nuisance function, and a target estimate, the loss-gradient nuisance bias is the population integral of the first bundle evaluated at the target estimate minus the corresponding population integral of the second bundle.