Linear Coercivity of an Interior Legendre Tilt

Proved

FunctionalInequalities.Analysis.exists_coercive_tilt_of_mem_interior_legendre_domain_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a pointwise coercivity result for a proper extended-real potential.

Let $E$ be a finite-dimensional real inner-product normed space, let $\phi:E\to\overline{\mathbb R}$ be a ProperPotential, and let $y$ lie in the interior of the finite domain

\{q:E\mid \operatorname{legendre}(\phi)(q)\ne+\infty\}.

Then there exist real numbers $a,b$ with $a>0$ such that, for every $z\in E$ ,

\bigl(a\|z\|-b\bigr)\le \phi(z)-\langle z,y\rangle,

where the real affine expression is embedded into EReal and the inner product is likewise coerced.

No convexity, differentiability, nonnegativity, or global finiteness of $\phi$ is assumed. The result supplies the linear decay needed to establish attainment of a Legendre supremum.

Original Lean declaration header

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

theorem exists_coercive_tilt_of_mem_interior_legendre_domain
    (φ : E → EReal) (hφ : ProperPotential φ) (y : E)
    (hy : y ∈ interior {q : E | legendre φ q ≠ ⊤}) :
    ∃ (a b : ℝ), 0 < a ∧ ∀ z : E,
      ((a * ‖z‖ - b : ℝ) : EReal) ≤ φ z - (inner ℝ z y : EReal)

Module navigation

Module: Analysis/Convex/LegendreVariation/Attainment.

Definition modules: Analysis/Convex/Legendre.

Supporting theorems: affineMaximum_coercive.

Previous: conjugate_maximizer_eq_gradient · Next: tiltedObjective_data.

Source excerpt, lines 210–214 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_LegendreVariation_Attainment

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.exists_coercive_tilt_of_mem_interior_legendre_domain_readable
    (φ : E → EReal) (hφ : ProperPotential φ) (y : E)
    (hy : y ∈ interior {q : E | legendre φ q ≠ ⊤}) :
    ∃ (a b : ℝ), 0 < a ∧ ∀ z : E,
      ((a * ‖z‖ - b : ℝ) : EReal) ≤ φ z - (inner ℝ z y : EReal) := by sorry

Source

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

View graph