Proposition 3.1, proof — $B\subseteq G\subseteq(1+\varepsilon)B$

Proved

PolyhedralSOC.LowerBound.ball_sandwich

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

p2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1polyhedral-approximationsecond-order-cone

Let $\varepsilon>0$ and let $\Pi:\mathbb R^k\times\mathbb R\times\mathbb R^p\to\mathbb R^q$ be a polyhedral $\varepsilon$ -approximation of $L^k$ . Let

G=\{y\in\mathbb R^k\mid \Pi(y,1,u)\ge0\ \text{for some } u\}

and let $B=\{y\mid \|y\|_2\le 1\}$ be the closed unit Euclidean ball of $\mathbb R^k$ . Then

B\subseteq G\subseteq (1+\varepsilon)B=\{y\mid \|y\|_2\le 1+\varepsilon\}.

This is the entry point of the lower-bound argument: the slice $G$ of the approximating polyhedral cone is squeezed between two concentric Euclidean balls whose radii differ by the factor $1+\varepsilon$ .

Formalization Note The page writes "polyhedral $\alpha$ approximation" at this point, a misprint for $\varepsilon$ .

Preamble

import Mathlib
import Definitions.Def_PolyhedralSOC_Shared_LorentzCone
import Definitions.Def_PolyhedralSOC_Shared_IsPolyhedralApprox
import Definitions.Def_PolyhedralSOC_LowerBound_ProofObjects

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):
"Since Π(·) is a polyhedral ε approximation of L^k, the set G contains the unit k-dimensional
Euclidean ball B and is contained in the ball (1+ε)B" (the page prints "α" for "ε"), where
`G = {y | Π(y, 1, u) ≥ 0 for some u}`. -/
theorem ball_sandwich {k p q : ℕ} {ε : ℝ} (hε : 0 < ε)
    (P : (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ))
    (hP : Shared.IsPolyhedralApprox k p q ε P) :
    {y : Fin k → ℝ | Shared.eucNorm y ≤ 1} ⊆ sliceG P ∧
      sliceG P ⊆ {y : Fin k → ℝ | Shared.eucNorm y ≤ 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 ("the set G contains the unit k-dimensional Euclidean ball B and is contained in the ball (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

Proposition 3.1, proof — B⊆G⊆(1+ε)BB\subseteq G\subseteq(1+\varepsilon)BB⊆G⊆(1+ε)B

Proposition 3.1, proof — $B\subseteq G\subseteq(1+\varepsilon)B$