Corollary 13.8 (oracle inequality): for a convex ρ-Lipschitz loss, RLM satisfies E_S[L_D(A(S))] ≤ L_D(w*) + λ‖w*‖² + 2ρ²/(λm) for every w*
ProvedUnderstandingML.rlm_oracle_inequalitylipschitzoracle-inequalityregularization
Corollary 13.8. Assume that the loss function is convex and -Lipschitz. Then the RLM rule with the regularization function satisfies
Measurability: jointly measurable loss and measurable algorithm, with a nonnegative loss bounded at the origin so that all expectations exist (for the RLM rule the minimizer is unique, so measurability of the algorithm is automatic).
Preamble
import Definitions.Def_UnderstandingML_Convex open MeasureTheory open scoped InnerProductSpace
Formal statement
namespace UnderstandingML
/-- **Corollary 13.8** (p. 179). Assume that the loss function is convex and `ρ`-Lipschitz. Then
the RLM rule with the regularization function `λ‖w‖²` satisfies, for all `w*`,
`E_S[L_D(A(S))] ≤ L_D(w*) + λ‖w*‖² + 2ρ²/(λm)`. Measurability as in Corollary 13.6. -/
theorem rlm_oracle_inequality {d : ℕ} {Z : Type*} [MeasurableSpace Z] (loss : Vec d → Z → ℝ)
(hconv : ∀ z, ConvexOn ℝ Set.univ (fun w ↦ loss w z)) {ρ : ℝ}
(hlip : IsLipschitzLoss ρ loss) {lam : ℝ} (hlam : 0 < lam) (A : Learner Z (Vec d))
(hA : IsRLMLearner loss lam A) (hmeas : Measurable (Function.uncurry loss))
(hnonneg : ∀ w z, 0 ≤ loss w z) {C : ℝ} (hC : ∀ z, loss 0 z ≤ C)
(hAmeas : ∀ m, Measurable (A m)) (D : Measure Z) [IsProbabilityMeasure D] (m : ℕ)
(hm : 0 < m) (wstar : Vec d) :
∫ S, risk loss D (A m S) ∂(iidLaw D m) ≤
risk loss D wstar + lam * ‖wstar‖ ^ 2 + 2 * ρ ^ 2 / (lam * m) := by sorry
end UnderstandingML
Source
Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §13.4 p. 179, Corollary 13.8 with its derivation (13.15)-(13.16)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.