Legendre Upper Bound from a Bounded Domain and Real Floor

This bounds the actual extended-real Legendre transform using a bounded effective domain.

Let $\phi:E\to\overline{\mathbb R}$, let $L\in[0,\infty)$, and let $m\in\mathbb R$. Assume:

1. $\phi(y)\neq-\infty$ for every $y$;
2. if $\phi(y)\neq+\infty$, then $\|y\|\leq L$;
3. $m\leq\phi(y)$ for every $y$.

Then for every $x\in E$,

with the right-hand side coerced into EReal. The statement controls the full extended-real supremum and does not assume finite dimensionality.

Original Lean declaration header

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

theorem legendre_le_of_real_lower_bound
    (φ : E → EReal) (L : NNReal) (m : ℝ)
    (hbot : ∀ y, φ y ≠ ⊥)
    (hdom : ∀ y, φ y ≠ ⊤ → y ∈ closedBall (0 : E) (L : ℝ))
    (hfloor : ∀ y, (m : EReal) ≤ φ y) (x : E) :
    legendre φ x ≤ (((L : ℝ) * ‖x‖ - m : ℝ) : EReal)

Module navigation

Module: Analysis/Convex/BoundedConjugate.

Definition modules: Analysis/Convex/Legendre.

Previous: exists_real_global_minimum_of_bounded_domain · Next: real_convexOn_legendre.

Source excerpt, lines 107–112 · Frozen source 408915f.