Prove2Me

Simplex Ball Inclusion and Box Ball Inclusion

Proved
FunctionalInequalities.Analysis.closedBall_subset_stdSimplex_and_box_subset_closedBall_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This establishes two elementary geometric inclusions for the standard simplex and a coordinate box.

Let n≥1n\ge1 and work in Rn=EuclideanSpace⁡ R (Fin⁡n)\mathbb R^n=\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n). Let

c=1n+1∑iei,ρ=12(n+1)n.c=\frac1{n+1}\sum_i e_i, \qquad \rho=\frac1{2(n+1)\sqrt n}.

Then

B‾(c,ρ)⊆{y:yi≥0 ∀i, ∑iyi≤1},\overline B(c,\rho)\subseteq\left\{y: y_i\ge0\ \forall i,\ \sum_i y_i\le1\right\},

and

{y:∣yi∣≤1 ∀i, ∣1−∑iyi∣≤1}⊆B‾(0,n).\left\{y: |y_i|\le1\ \forall i,\ \left|1-\sum_i y_i\right|\le1\right\} \subseteq\overline B(0,\sqrt n).

The declaration is closedBall_subset_stdSimplex_and_box_subset_closedBall_readable. The dimension restriction is strictly 0<n0<n.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem closedBall_subset_stdSimplex_and_box_subset_closedBall {n : ℕ} (hn : 0 < n) :
    closedBall ((1 / ((n : ℝ) + 1)) • ∑ i, EuclideanSpace.single i (1 : ℝ))
        (1 / (2 * ((n : ℝ) + 1) * Real.sqrt n)) ⊆
      {y : EuclideanSpace ℝ (Fin n) | (∀ i, 0 ≤ y i) ∧ ∑ i, y i ≤ 1} ∧
    {y : EuclideanSpace ℝ (Fin n) | (∀ i, |y i| ≤ 1) ∧ |1 - ∑ i, y i| ≤ 1} ⊆
      closedBall (0 : EuclideanSpace ℝ (Fin n)) (Real.sqrt n)

Module navigation

Module: Analysis/Convex/Normalization.

Previous: abs_simplexCoord_le_one_of_max · Next: exists_affine_normalization.

Source excerpt, lines 348–353 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Normalization

open Set Metric
Formal statement

theorem FunctionalInequalities.Analysis.closedBall_subset_stdSimplex_and_box_subset_closedBall_readable {n : ℕ} (hn : 0 < n) :
    closedBall ((1 / ((n : ℝ) + 1)) • ∑ i, EuclideanSpace.single i (1 : ℝ))
        (1 / (2 * ((n : ℝ) + 1) * Real.sqrt n)) ⊆
      {y : EuclideanSpace ℝ (Fin n) | (∀ i, 0 ≤ y i) ∧ ∑ i, y i ≤ 1} ∧
    {y : EuclideanSpace ℝ (Fin n) | (∀ i, |y i| ≤ 1) ∧ |1 - ∑ i, y i| ≤ 1} ⊆
      closedBall (0 : EuclideanSpace ℝ (Fin n)) (Real.sqrt n) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Normalization.lean#L346-L501 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Normalization`, declaration `FunctionalInequalities.Analysis.closedBall_subset_stdSimplex_and_box_subset_closedBall`; the repository is private at upload time).

View graph