Definition 3.2: Oracle, Oracle Risk, Oracle Inequality

Let R(·) be a risk function and let H = {φ₁,...,φ_M} be a dictionary of functions from ℝ^d to ℝ. Let K ⊆ ℝ^M. The oracle on K w.r.t. R is φ_{θ̄} where θ̄ ∈ K minimizes R(φ_θ). The oracle risk is R_K = R(φ_{θ̄}).

An oracle inequality in expectation holds if there exists C ≥ 1 such that 𝔼[R(f̂)] ≤ C · inf_{θ∈K} R(φ_θ) + φ_{n,M}(K).

An oracle inequality with high probability holds if there exists C ≥ 1 s.t. ℙ{R(f̂) ≤ C · inf_{θ∈K} R(φ_θ) + φ_{n,M,δ}(K)} ≥ 1 - δ, ∀ δ > 0.

If C = 1 the oracle inequality is called exact.

noncomputable def Chapter3.dictCombination {d M : ℕ} (φ : Fin M → Fin d → ℝ) (θ : Fin M → ℝ) : Fin d → ℝ

The linear combination φ_θ = ∑ j, θ_j · φ_j for a dictionary of M functions from ℝ^d to ℝ, evaluated at a point. Here φ j is the j-th dictionary element as a function Fin d → ℝ (i.e., evaluated at the n data points in the fixed-design setting, or representing the function values).

noncomputable def Chapter3.oracleRisk {d M : ℕ} (R : (Fin d → ℝ) → ℝ) (φ : Fin M → Fin d → ℝ) (K : Set (Fin M → ℝ)) : ℝ

Definition 3.2

def Chapter3.IsOracle {d M : ℕ} (R : (Fin d → ℝ) → ℝ) (φ : Fin M → Fin d → ℝ) (K : Set (Fin M → ℝ)) (θbar : Fin M → ℝ) : Prop

θ̄ is an oracle on K if it minimizes R(φ_θ) over K

def Chapter3.SatisfiesOracleInequality {d M : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (R : (Fin d → ℝ) → ℝ) (φ : Fin M → Fin d → ℝ) (fhat : Ω → Fin d → ℝ) (K : Set (Fin M → ℝ)) (C r : ℝ) : Prop

Oracle inequality in expectation with constant C ≥ 1 and remainder r: 𝔼[R(f̂)] ≤ C · inf_{θ∈K} R(φ_θ) + r. The estimator f̂ : Ω → (Fin d → ℝ) is random.

def Chapter3.SatisfiesExactOracleInequality {d M : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (R : (Fin d → ℝ) → ℝ) (φ : Fin M → Fin d → ℝ) (fhat : Ω → Fin d → ℝ) (K : Set (Fin M → ℝ)) (r : ℝ) : Prop

Exact oracle inequality in expectation: C = 1

def Chapter3.SatisfiesHighProbOracleInequality {d M : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (R : (Fin d → ℝ) → ℝ) (φ : Fin M → Fin d → ℝ) (fhat : Ω → Fin d → ℝ) (K : Set (Fin M → ℝ)) (C : ℝ) (rem : ℝ → ℝ) : Prop

Oracle inequality with high probability: C ≥ 1 and ℙ{R(f̂) ≤ C · inf_{θ∈K} R(φ_θ) + rem(δ)} ≥ 1 - δ for all δ > 0.

theorem Chapter3.oracleRisk_le {d M : ℕ} (R : (Fin d → ℝ) → ℝ) (φ : Fin M → Fin d → ℝ) (K : Set (Fin M → ℝ)) (θ : Fin M → ℝ) (hθ : θ ∈ K) (hR_bdd : BddBelow ((fun (θ : Fin M → ℝ) => R (dictCombination φ θ)) '' K)) : oracleRisk R φ K ≤ R (dictCombination φ θ)

For any θ ∈ K, the oracle risk is at most R(φ_θ), given that R is bounded below on the dictionary over K.

theorem Chapter3.oracleRisk_nonneg {d M : ℕ} (R : (Fin d → ℝ) → ℝ) (φ : Fin M → Fin d → ℝ) {K : Set (Fin M → ℝ)} (_hK : K.Nonempty) (hR : ∀ (g : Fin d → ℝ), 0 ≤ R g) : 0 ≤ oracleRisk R φ K

The oracle risk is nonneg if R is nonneg