Affine Normalization of Compact Convex Sets

Proved

FunctionalInequalities.Analysis.exists_affine_normalization_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the affine normalization statement used in the weak Letwin route.

Let $E$ be a finite-dimensional real inner-product space. There exists a constant $C>0$ , depending only on $E$ , such that for every compact convex set $K\subseteq E$ with nonempty interior, there is an affine equivalence $e:E\simeq_A E$ satisfying

\overline B(0,1)\subseteq e(K)\subseteq\overline B(0,C).

The declaration is exists_affine_normalization_readable. The result is existential in both $C$ and the affine equivalence and does not provide a uniform constant across different ambient spaces.

Original Lean declaration header

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

theorem exists_affine_normalization {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] :
    ∃ C : ℝ, 0 < C ∧ ∀ K : Set E, IsCompact K → Convex ℝ K → (interior K).Nonempty →
      ∃ e : E ≃ᵃ[ℝ] E, closedBall (0 : E) 1 ⊆ e '' K ∧ e '' K ⊆ closedBall (0 : E) C

Module navigation

Module: Analysis/Convex/Normalization.

Supporting theorems: abs_simplexCoord_le_one_of_max, closedBall_subset_stdSimplex_and_box_subset_closedBall, exists_max_simplexEdgeMatrix_det.

Previous: closedBall_subset_stdSimplex_and_box_subset_closedBall.

Source excerpt, lines 520–523 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Normalization

open Set Metric
set_option maxHeartbeats 4000000

Formal statement


theorem FunctionalInequalities.Analysis.exists_affine_normalization_readable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] :
    ∃ C : ℝ, 0 < C ∧ ∀ K : Set E, IsCompact K → Convex ℝ K → (interior K).Nonempty →
      ∃ e : E ≃ᵃ[ℝ] E, closedBall (0 : E) 1 ⊆ e '' K ∧ e '' K ⊆ closedBall (0 : E) C := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Normalization.lean#L515-L736 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Normalization`, declaration `FunctionalInequalities.Analysis.exists_affine_normalization`; the repository is private at upload time).

View graph