Prove2Me

Proposition 2.1(ii) — solutions of (8) satisfy ∥(x1,x2)∥2≤(1+δ(ν))x3\|(x_1,x_2)\|_2\le(1+\delta(\nu))x_3

Proved
PolyhedralSOC.UpperBound.planar_approx_quality

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

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

Let ν\nu be a positive integer and suppose (x1,x2,x3)(x_1,x_2,x_3) can be extended, by some ξj,ηj\xi^j,\eta^j (j=0,…,νj=0,\dots,\nu), to a solution of system (8). Then

∥(x1,x2)∥2=x12+x22≤(1+δ(ν)) x3,δ(ν)=1cos⁡(π2ν+1)−1.\|(x_1,x_2)\|_2=\sqrt{x_1^2+x_2^2}\le(1+\delta(\nu))\,x_3,\qquad \delta(\nu)=\frac{1}{\cos\big(\frac{\pi}{2^{\nu+1}}\big)}-1.

Together with part (i) this says that system (8) is a polyhedral δ(ν)\delta(\nu)-approximation of L2L^2.

Formalization Note The conclusion holds for every solution of (8), not only for the one constructed in part (i).

Preamble
import Mathlib
import Definitions.Def_PolyhedralSOC_UpperBound_System8
Formal statement
namespace PolyhedralSOC.UpperBound

/-- Ben-Tal & Nemirovski, *On Polyhedral Approximations of the Second-Order Cone*,
Math. Oper. Res. 26(2):193–205 (2001), Proposition 2.1, part (ii), p. 199 (PDF p. 7;
proof p. 200): for every positive integer `ν`, if `(x₁, x₂, x₃)` can be extended to a
solution of (8), then `‖(x₁, x₂)‖₂ ≤ (1 + δ(ν)) x₃` with `δ(ν) = 1/cos(π/2^{ν+1}) − 1`. -/
theorem planar_approx_quality (ν : ℕ) (hν : 1 ≤ ν) (x₁ x₂ x₃ : ℝ) (ξ η : ℕ → ℝ)
    (h : System8 ν x₁ x₂ x₃ ξ η) :
    Real.sqrt (x₁ ^ 2 + x₂ ^ 2) ≤ (1 + delta ν) * x₃ := by sorry

end PolyhedralSOC.UpperBound
Source
Ben-Tal & Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Math. Oper. Res. 26(2):193–205 (2001), p. 199, Proposition 2.1, part (ii) of the proof statement, Eq. (9)
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

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

View graph