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)
Directional derivative of the learning-system loss in the nuisance coordinate. Bundles a candidate pointwise directional-derivative function, the witness that the loss's difference quotient along the segment from the distinguished nuisance to any candidate nuisance converges pointwise to that function, and measurability of each resulting observation function.
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)
The population first-order inequality for an orthogonal statistical-learning system and target-derivative data at the distinguished nuisance requires every candidate target's integrated directional derivative at the distinguished target to be nonnegative. It is a directly assumed stationarity condition; without further differentiability and risk-convexity hypotheses, it does not characterize the distinguished target as a global minimizer.
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 domination predicates intended for limit--integral interchange arguments.
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 mixed target--nuisance derivative data, the Neyman-orthogonality condition for the loss states that every admissible target and nuisance direction has zero observation-law integral of its mixed directional derivative.
Definition (Lean source)
For an orthogonal statistical-learning system and a nuisance function, the target-direction difference-quotient envelope condition gives each candidate target a positive neighborhood radius and an integrable envelope that bounds the absolute loss difference quotient almost everywhere for every smaller nonzero perturbation.
Definition (Lean source)
For an orthogonal statistical-learning system, the nuisance-direction difference-quotient envelope condition gives each admissible nuisance a positive neighborhood radius and an integrable envelope that bounds the absolute loss difference quotient almost everywhere for every smaller nonzero perturbation.
Definition (Lean source)
For an orthogonal statistical-learning system and mixed target--nuisance derivative data, the mixed-derivative limit--integral bridge says the integrated centered quotient along every admissible nuisance perturbation tends to the integral of the corresponding mixed directional derivative.
Definition (Lean source)
Integrated-derivative reformulation of Neyman orthogonality. Assume the stated limit--integral bridge for the bundled derivatives. Then Neyman orthogonality is equivalent to zero directional derivative of the integrated map for every admissible target and nuisance 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.
Integrated Target-Derivative Difference 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 integrated pointwise derivative at a plug-in nuisance.
The exported definition is Bias_n. Relating it to a population-risk
derivative or to a quantitative Taylor expansion requires additional analytic
bridges that are not exported here.
The integrated pointwise target-derivative difference measures, in an orthogonal statistical-learning system, how the integrated derivative data at the true nuisance changes when replaced by derivative data at a plug-in nuisance, evaluated at a target estimate. It is the first population integral minus the corresponding plug-in integral.