Estimation.OrthogonalLearning
Generic orthogonal statistical-learning substrate: population derivative bundles, cross-fitted plug-in ERM, local moduli, oracle inequalities, and sparse specializations.
Setup 4 core · 0 supporting This file defines the basic population system for orthogonal statistical learning: a measurable loss, a convex target class in a Hilbert space, an admissible nuisance class, and distinguished target and nuisance elements
Orthogonal Statistical Learning Setup
This file defines the basic population system for orthogonal statistical learning: a measurable loss, a convex target class in a Hilbert space, an admissible nuisance class, and distinguished target and nuisance elements. It is the loss-based analogue of an orthogonal-moment model.
The central structure is LearningSystem. Its namespace provides the population
risk LearningSystem.L, and the file also exposes the segment-closure predicates
Θ_PerturbClosed and G_PerturbClosed used by later directional-derivative
modules.
Orthogonal statistical-learning system. Bundles a convex target class Θ_set containing a distinguished target θ₀, a nuisance class G_set containing a distinguished nuisance g₀, a jointly measurable loss ℓ, and the condition that θ₀ minimizes the population risk over the target class at the true nuisance g₀.
Definition (Lean source)
Population risk: L(θ, g) := ∫ ℓ(z; θ, g) dP_Z.
Definition (Lean source)
Closure-under-perturbation predicate for Θ_set: every line segment between θ₀ and θ ∈ Θ_set stays in Θ_set. Strictly weaker than convexity; useful for stating directional-derivative hypotheses without requiring the whole set to be convex.
Definition (Lean source)
Closure-under-perturbation predicate for G_set.
Definition (Lean source)
PluginERM 2 core · 0 supporting This file defines the empirical risk on the estimation fold of a sample split and the predicate that an estimator approximately minimizes that empirical risk after plugging in a nuisance estimate.
Sample-Split Plug-In ERM
This file defines the empirical risk on the estimation fold of a sample split and the predicate that an estimator approximately minimizes that empirical risk after plugging in a nuisance estimate. These objects are the estimation-side inputs to the orthogonal statistical-learning oracle inequality.
The main declarations are empRiskFoldB, the fold-B empirical risk, and
SampleSplitPluginERM, the approximate empirical-risk-minimization predicate
for a sample-indexed target estimator and plug-in nuisance estimate.
Empirical risk on the estimation fold B(n): (1 / |B(n)|) · Σ_{i ∈ B(n)} ℓ (Z_i ω) θ g.
Definition (Lean source)
This predicate says that a sample-size-indexed target estimator, evaluated against a plug-in nuisance estimate on the estimation fold, is an approximate empirical-risk minimizer: the optimization slack is nonnegative at every sample size, the estimator's value always lies in the target parameter set, and its fold-B empirical risk at the plug-in nuisance is within that slack of the risk at every other point in the target set.
Definition (Lean source)
OracleInequality 2 core · 0 supporting This file proves deterministic and high-probability conservative oracle inequalities for sample-split plug-in empirical risk minimization with an orthogonal loss. ★ oracle_inequality_plugin_ERM★ oracle_inequality_plugin_ERM_highProb
Orthogonal Statistical Learning Oracle Inequality
This file proves deterministic and high-probability conservative oracle
inequalities for sample-split plug-in empirical risk minimization with an
orthogonal loss. The bounds convert strong convexity, empirical optimality, a
local empirical-process modulus, and second-order bias into squared
target-space error control with the displayed 4/σ optimization-slack
constant.
The deterministic theorem oracle_inequality_plugin_ERM consumes a realized
modulus inequality at one sample point. The high-probability theorem
oracle_inequality_plugin_ERM_highProb packages the same bound on the event
provided by LocalEmpProcessModulus for a fixed plug-in nuisance.
Conservative oracle inequality for the orthogonal sample-split plug-in ERM. Assume the realised nuisance at every sample point admits the directional-derivative structure needed for the first-order expansion of the loss, that the estimator is a sample-split plug-in ERM with optimization slack r_opt, and that the strong-convexity modulus σ is strictly positive. Suppose the population risk at the realised nuisance is σ-strongly convex around θ₀ in the chosen norm, and that the first-order inequality holds at the truth (θ₀, g₀). If, at the specific sample point (n, ω), the local empirical-process modulus inequality is realised for the estimator's target value against the realised nuisance, then the squared target-space estimation error is bounded by 4(1+σ)/σ² · (ρ n)² + (4/σ) · Bias_n + (4/σ) · r_opt n.
Formal statement
Proof (Lean source)
High-probability conservative oracle inequality for the orthogonal sample-split plug-in ERM. Fix a single nuisance value g. Assume the estimator is a sample-split plug-in ERM at this fixed nuisance, with optimization slack r_opt, and that the strong-convexity modulus σ is strictly positive. Suppose the population risk at g is σ-strongly convex around θ₀ in the chosen norm, and that the first-order inequality holds at the truth (θ₀, g₀). If the local empirical-process modulus condition holds at rate ρ and confidence level δ for the fixed nuisance g, then for every sample size n there is an event of probability at least 1 - δ on which the squared target-space estimation error is bounded by 4(1+σ)/σ² · (ρ n)² + (4/σ) · Bias_n + (4/σ) · r_opt n.