Convexity of the triple deficit on the cutoff79 entry box

Proved

HlawkaSchatten.DiagonalCutoff.convex_box79

by sorry_not_sorry · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

For real p ≥ 79 and (23/50)p ≤ K ≤ p/2, the triple deficit is convex on the nine-coordinate box of radius 195/1000 = 0.195 around the cyclic center.

Preamble

import Definitions.Def_HlawkaSchatten_DiagonalConstruction_BoxConvexity
import Definitions.Def_HlawkaSchatten_DiagonalConstruction_ScalarBounds
open HlawkaSchatten HlawkaSchatten.DiagonalConstruction

Formal statement

theorem HlawkaSchatten.DiagonalCutoff.convex_box79 : ∀ p K : ℝ, 79 ≤ p → (23/50 : ℝ)*p ≤ K → K ≤ p/2 → ConvexOn ℝ {X : Triple | ∀ j i, |X j i - cyclicCenter j i| ≤ (195/1000 : ℝ)} (tripleDeficit p K) := by sorry

View graph