Finite Real Minimum on a Bounded Effective Domain

Let $E$ be a finite-dimensional real inner-product normed space, let $\phi:E\to\overline{\mathbb R}$, and let $L\in[0,\infty)$. Assume $\phi(y)\ne-\infty$ for every $y$, some value of $\phi$ is finite, $\phi$ is lower semicontinuous, and every point where $\phi(y)\ne+\infty$ lies in the closed ball $\overline B(0,L)$. Then there exist $a\in\overline B(0,L)$ and $m\in\mathbb R$ such that

The conclusion explicitly produces a real-valued global minimum after excluding both extended-real infinities.

Original Lean declaration header

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

theorem exists_real_global_minimum_of_bounded_domain
    (φ : E → EReal) (L : NNReal)
    (hbot : ∀ y, φ y ≠ ⊥)
    (hfinite : ∃ y, φ y ≠ ⊤)
    (hlsc : LowerSemicontinuous φ)
    (hdom : ∀ y, φ y ≠ ⊤ → y ∈ closedBall (0 : E) (L : ℝ)) :
    ∃ a ∈ closedBall (0 : E) (L : ℝ), ∃ m : ℝ,
      φ a = (m : EReal) ∧ ∀ y, (m : EReal) ≤ φ y

Module navigation

Module: Analysis/Convex/BoundedConjugate.

Previous: closedBallCap_lowerSemicontinuous · Next: legendre_le_of_real_lower_bound.

Source excerpt, lines 72–79 · Frozen source 408915f.