Prove2Me

Proposition 3.1, proof — balls of radius 2ε(1+ε)\sqrt{2\varepsilon(1+\varepsilon)} about the yiy_i cover ∂((1+ε)B)\partial((1+\varepsilon)B)

Proved
PolyhedralSOC.LowerBound.covering_claim

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-geometrycovering-numbersp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let ε>0\varepsilon>0 and let S={y1,…,yN}⊆RkS=\{y_1,\dots,y_N\}\subseteq\mathbb R^k be a finite set such that

  1. the convex hull of SS contains the closed unit Euclidean ball BB, and
  2. every yiy_i satisfies ∥yi∥2≤1+ε\|y_i\|_2\le 1+\varepsilon.

Then the closed Euclidean balls BiB_i of radius 2ε(1+ε)\sqrt{2\varepsilon(1+\varepsilon)} centred at the yiy_i cover the sphere ∂((1+ε)B)\partial((1+\varepsilon)B): for every yy with ∥y∥2=1+ε\|y\|_2=1+\varepsilon there is an ii with

∥y−yi∥2≤2ε(1+ε).\|y-y_i\|_2\le\sqrt{2\varepsilon(1+\varepsilon)}.

Applied to the vertices yiy_i of the slice GG (which satisfies B⊆G⊆(1+ε)BB\subseteq G\subseteq(1+\varepsilon)B), this is the geometric heart of the lower bound: a polytope sandwiched between two nearby balls must have vertices close to every point of the outer sphere.

Preamble
import Mathlib
import Definitions.Def_PolyhedralSOC_Shared_LorentzCone
Formal statement
namespace PolyhedralSOC.LowerBound

/-- Ben-Tal & Nemirovski, *On Polyhedral Approximations of the Second-Order Cone*,
Math. Oper. Res. 26(2):193–205 (2001), Proposition 3.1, proof, p. 202 (PDF p. 10):
"We claim that the N Euclidean balls B_i centered at y_i of the radius √(2ε(1+ε)) cover the
boundary of (1+ε)B." Stated for the points `y_i` as a finite set `S ⊆ ℝ^k` whose convex hull
contains the unit Euclidean ball `B` and which lies in `(1 + ε)B` (the two properties of `G`
the proof uses): every `y` with `‖y‖₂ = 1 + ε` lies in the closed Euclidean ball of radius
`√(2ε(1+ε))` about some point of `S`. -/
theorem covering_claim {k : ℕ} {ε : ℝ} (hε : 0 < ε) (S : Finset (Fin k → ℝ))
    (hB : {y : Fin k → ℝ | Shared.eucNorm y ≤ 1} ⊆ convexHull ℝ (S : Set (Fin k → ℝ)))
    (hS : ∀ s ∈ S, Shared.eucNorm s ≤ 1 + ε) :
    ∀ y : Fin k → ℝ, Shared.eucNorm y = 1 + ε →
      ∃ s ∈ S, Shared.eucNorm (y - s) ≤ Real.sqrt (2 * ε * (1 + ε)) := by sorry

end PolyhedralSOC.LowerBound
Source
Ben-Tal & Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Math. Oper. Res. 26(2):193–205 (2001), p. 202, Proposition 3.1, proof ("We claim that the N Euclidean balls B_i centered at y_i of the radius √(2ε(1+ε)) cover the boundary of (1+ε)B")
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

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

View graph