Regularity and Coercive Decay of the Tilted Objective

This is a technical attainment lemma for a Legendre transform.

Let $E$ be a finite-dimensional real inner-product normed space, let $\phi:E\to\overline{\mathbb R}$ be a ProperPotential, and assume that $\phi$ is lower semicontinuous. If $y$ lies in the interior of $\{q:\phi^*(q)\ne+\infty\}$, define $G(z)=\langle z,y\rangle-\phi(z)$. Then:

1. $G$ is upper semicontinuous;
2. $G(z)\ne+\infty$ for every $z$;
3. $G(z)\ne-\infty$ for at least one $z$; and
4. there exist $a,b\in\mathbb R$ with $a>0$ such that, for every $z$,

The conclusion supplies the hypotheses for a separate upper-semicontinuous maximum theorem; it does not itself assert existence of a maximizer.

Original Lean declaration header

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

theorem tiltedObjective_data
    (φ : E → EReal) (hφ : ProperPotential φ)
    (hlsc : LowerSemicontinuous φ) (y : E)
    (hy : y ∈ interior {q : E | legendre φ q ≠ ⊤}) :
    let G : E → EReal := fun z => (inner ℝ z y : EReal) - φ z
    UpperSemicontinuous G ∧
      (∀ z, G z ≠ ⊤) ∧
      (∃ z, G z ≠ ⊥) ∧
      ∃ (a b : ℝ), 0 < a ∧ ∀ z,
        G z ≤ ((b - a * ‖z‖ : ℝ) : EReal)

Module navigation

Module: Analysis/Convex/LegendreVariation/Attainment.

Definition modules: Analysis/Convex/Legendre.

Supporting theorems: exists_coercive_tilt_of_mem_interior_legendre_domain.

Previous: exists_coercive_tilt_of_mem_interior_legendre_domain · Next: exists_legendre_maximizer_with_gradient_identity.

Source excerpt, lines 280–289 · Frozen source 408915f.