Stage 8: attainment of the Euclidean solution radius

The public radius is defined as an sInf. In the Euclidean branch that infimum is attained: the minimizer set is closed because the objective is differentiable, and the literal finite-sum lpNorm 2 is the norm transported to the finite-dimensional PiLp 2 space. A closest point in that proper space therefore gives an actual optimizer at the exact frozen radius.

@[reducible, inline]

abbrev O3.Stage8EuclideanRadius.EuclideanLpSpace (d : ℕ) : Type

Finite-dimensional Euclidean space with the PiLp 2 norm.

Equations

• O3.Stage8EuclideanRadius.EuclideanLpSpace d = PiLp (ENNReal.ofReal 2) fun (x : Fin d) => ℝ

theorem O3.Stage8EuclideanRadius.minimizerSet_isClosed {d : ℕ} (P : AdmissibleInstance d 2) : IsClosed (MinimizerSet P.f)

The minimizer set of an admissible Euclidean instance is closed.

theorem O3.Stage8EuclideanRadius.lpNorm_two_eq_transport_dist {d : ℕ} (x y : Vec d) : lpNorm 2 (x - y) = dist (WithLp.toLp (ENNReal.ofReal 2) x) (WithLp.toLp (ENNReal.ofReal 2) y)

The literal lpNorm 2 is exactly distance after transport to PiLp 2.

theorem O3.Stage8EuclideanRadius.exists_minimizer_at_radius {d : ℕ} (P : AdmissibleInstance d 2) : ∃ xstar ∈ MinimizerSet P.f, lpNorm 2 (xstar - P.x0) = P.radius

The source sInf radius is attained by a genuine optimizer.

theorem O3.Stage8EuclideanRadius.exists_minimizer_within {d : ℕ} (P : AdmissibleInstance d 2) {D : ℝ} (hDR : P.radius ≤ D) : ∃ xstar ∈ MinimizerSet P.f, lpNorm 2 (xstar - P.x0) ≤ D

Exact optimizer interface consumed by the Euclidean estimate-sequence evaluation: no closest optimizer is added to the public instance data.