theorem
Chapter3.problem_3_1_ls_oracle_inequality
{n M : ℕ}
(hn : 0 < n)
(Φ : Matrix (Fin n) (Fin M) ℝ)
(f : Fin n → ℝ)
(σ : ℝ)
(hσ : 0 < σ)
(μ : MeasureTheory.Measure (Fin n → ℝ))
[MeasureTheory.IsProbabilityMeasure μ]
(θhat : (Fin n → ℝ) → Fin M → ℝ)
(hLS :
∀ (ε : Fin n → ℝ) (θ : Fin M → ℝ),
(f + ε - Φ.mulVec (θhat ε)) ⬝ᵥ (f + ε - Φ.mulVec (θhat ε)) ≤ (f + ε - Φ.mulVec θ) ⬝ᵥ (f + ε - Φ.mulVec θ))
(hVar : ∀ (i : Fin n), ∫ (ε : Fin n → ℝ), ε i ^ 2 ∂μ ≤ σ ^ 2)
(hMean : ∀ (i : Fin n), ∫ (ε : Fin n → ℝ), ε i ∂μ = 0)
:
Problem 3.1 — Exact oracle inequality for the LS estimator. Given the regression model Y = f + ε with noise variance proxy σ², the LS estimator θ̂^LS satisfies: E[MSE(φ_{θ̂^LS})] ≤ inf_θ MSE(φ_θ) + C σ² M / n for some universal constant C > 0.
Here the LS estimator is modeled as a map θ̂ : (Fin n → ℝ) → Fin M → ℝ
from noise realizations ε to parameter vectors, where θ̂(ε) minimizes
|f + ε − Φθ|² over θ. The expectation is over ε ∼ μ.