Strictly Exposed Contact Below a Level

Proved

FunctionalInequalities.Analysis.exists_exposed_contact_of_lt_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This establishes the existence of a strictly exposed contact point below a prescribed level.

Let $E$ be a finite-dimensional real inner-product space and let $u:E\to\mathbb R$ be convex. Let $x,p\in E$ satisfy

u(x)+\langle p,y-x\rangle\le u(y)\quad\text{for all }y\in E.

For $R\in\mathbb R$ , assume $u(x)<R$ and that the sublevel set $\{y:u(y)\le R\}$ is compact. Then there exist $z,\theta\in E$ such that

u(z)=u(x)+\langle p,z-x\rangle,\qquad u(z)<R,

and every other contact point in the sublevel set is strictly separated:

u(y)=u(x)+\langle p,y-x\rangle\ \land\ u(y)\le R\ \land\ y\ne z \ \Longrightarrow\ \langle y-z,\theta\rangle<0.

The result supplies an exposed point for later contact-set arguments; it does not assert uniqueness of all contacts without the additional local volume hypotheses.

Original Lean declaration header

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

theorem exists_exposed_contact_of_lt {u : E → ℝ} (hconv : ConvexOn ℝ univ u) {x p : E}
    (hp : ∀ y, u x + ⟪p, y - x⟫ ≤ u y) {R : ℝ} (hR : u x < R) (hK : IsCompact {y | u y ≤ R}) :
    ∃ z θ : E, u z = u x + ⟪p, z - x⟫ ∧ u z < R ∧
      ∀ y, u y = u x + ⟪p, y - x⟫ → u y ≤ R → y ≠ z → ⟪y - z, θ⟫ < 0

Module navigation

Module: Analysis/Convex/Caffarelli.

Previous: subgradient_mem_interior_of_strictConvexOn · Next: exists_truncatedConjugate_eq.

Source excerpt, lines 1206–1209 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Caffarelli

open scoped RealInnerProductSpace
open Set
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
variable [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.exists_exposed_contact_of_lt_readable {u : E → ℝ} (hconv : ConvexOn ℝ univ u) {x p : E}
    (hp : ∀ y, u x + ⟪p, y - x⟫ ≤ u y) {R : ℝ} (hR : u x < R) (hK : IsCompact {y | u y ≤ R}) :
    ∃ z θ : E, u z = u x + ⟪p, z - x⟫ ∧ u z < R ∧
      ∀ y, u y = u x + ⟪p, y - x⟫ → u y ≤ R → y ≠ z → ⟪y - z, θ⟫ < 0 := by sorry

Source

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

View graph