§30.2.1: axis-aligned rectangles in ℝ^d have a compression scheme of size 2d (extremal positive examples per dimension, minimal enclosing rectangle)

Proved

UnderstandingML.box_compression

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

compression-schemesrectangles

§30.2.1 (Axis Aligned Rectangles). Consider the algorithm $A$ that works as follows: for each dimension, choose the two positive examples with extremal values at this dimension. Define $B$ to be the function that returns the minimal enclosing rectangle. Then, for $k = 2d$ , we have that in the realizable case, $L_S(B(A(S))) = 0$ .

Formally: the class of closed axis-aligned boxes in $\mathbb{R}^d$ has a compression scheme of size $2d$ .

Preamble

import Definitions.Def_UnderstandingML_Compression

open MeasureTheory
open scoped InnerProductSpace

Formal statement

namespace UnderstandingML

/-- **§30.2.1** (p. 412). The class of axis-aligned rectangles in `ℝ^d` has a compression scheme
of size `k = 2d`: for each dimension `A` selects the two positive examples with extremal values,
and `B` returns the minimal enclosing rectangle. -/
theorem box_compression (d : ℕ) : HasCompressionScheme (boxClass d) (2 * 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, §30.2.1 p. 412

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