Prove2Me

Theorem 29.7: the class H_Ψ = {x ↦ argmaxᵢ ⟨w, Ψ(x,i)⟩ : w ∈ ℝ^d} of linear multiclass predictors has Natarajan dimension ≤ d

Proved
UnderstandingML.linear_multiclass_ndim

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-predictorsmulticlassnatarajan-dimension

Theorem 29.7. Ndim⁡(HΨ)≤d\operatorname{Ndim}(H_\Psi) \le d, for HΨ={x↦argmax⁡i∈[k]⟨w,Ψ(x,i)⟩:w∈Rd}H_\Psi = \{x \mapsto \operatorname{argmax}_{i \in [k]}\langle w, \Psi(x, i)\rangle : w \in \mathbb{R}^d\} (29.1).

Formally: ties in the argmax are broken towards the smallest label (some fixed rule is needed: with arbitrary tie-breaking every function is an argmax predictor of Ψ≡0\Psi \equiv 0).

Preamble
import Definitions.Def_UnderstandingML_MulticlassLearnability

open MeasureTheory
open scoped InnerProductSpace
Formal statement
namespace UnderstandingML

/-- **Theorem 29.7** (p. 406). For a class-sensitive feature mapping `Ψ : X × [k] → ℝ^d` and
`H_Ψ = {x ↦ argmaxᵢ ⟨w, Ψ(x, i)⟩ : w ∈ ℝ^d}` (29.1), `Ndim(H_Ψ) ≤ d`. Ties in the argmax are
broken towards the smallest label. -/
theorem linear_multiclass_ndim {X : Type*} {d k : ℕ} [NeZero k] (Ψ : X → Fin k → Vec d) :
    ndim (linearMulticlassClass Ψ) ≤ d := 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, §29.3.3 pp. 405-406, Theorem 29.7 with its proof
Human review

  • Endorsed by Shuze Chen · Sep 25, 2026

    Confirmed by the moderator at approval.

  • Endorsed by naimengye · Sep 25, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph