Prove2Me

Frontier Distance Bounded by Directional Width

Proved
FunctionalInequalities.Analysis.infDist_frontier_le_of_forall_inner_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This proves that the distance to the frontier is bounded by a one-sided width.

Let EE be a normed real inner-product space, let S⊆ES\subseteq E be open and bounded, let x∈Sx\in S, and let θ\theta be a unit vector. If for some t∈Rt\in\mathbb R,

⟨y−x,θ⟩≤tfor every y∈S,\langle y-x,\theta\rangle\le t\qquad\text{for every }y\in S,

then

infDist⁡(x,∂S)≤t.\operatorname{infDist}(x,\partial S)\le t.

The declaration is infDist_frontier_le_of_forall_inner_le_readable. No finite-dimensionality or convexity assumption appears in the statement.

Original Lean declaration header

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

theorem infDist_frontier_le_of_forall_inner_le {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] {S : Set E} (hS : IsOpen S) (hb : Bornology.IsBounded S)
    {x : E} (hx : x ∈ S) {θ : E} (hθ : ‖θ‖ = 1) {t : ℝ} (ht : ∀ y ∈ S, ⟪y - x, θ⟫ ≤ t) :
    infDist x (frontier S) ≤ t

Module navigation

Module: Analysis/Convex/Alexandrov.

Previous: volume_subgradientImage_quadraticAt_aux · Next: subgradientImage_comp_affineEquiv_symm.

Source excerpt, lines 1687–1690 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Alexandrov

open Set Metric
open scoped RealInnerProductSpace
Formal statement

theorem FunctionalInequalities.Analysis.infDist_frontier_le_of_forall_inner_le_readable {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] {S : Set E} (hS : IsOpen S) (hb : Bornology.IsBounded S)
    {x : E} (hx : x ∈ S) {θ : E} (hθ : ‖θ‖ = 1) {t : ℝ} (ht : ∀ y ∈ S, ⟪y - x, θ⟫ ≤ t) :
    infDist x (frontier S) ≤ t := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Alexandrov.lean#L1685-L1740 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Alexandrov`, declaration `FunctionalInequalities.Analysis.infDist_frontier_le_of_forall_inner_le`; the repository is private at upload time).

View graph