Finite Maximum Under Upper Semicontinuity and Linear Decay

This is a general finite-dimensional attainment lemma for extended-real functions.

Let $E$ be a finite-dimensional real inner-product normed space and $G:E\to\overline{\mathbb R}$. Assume:

1. $G$ is upper semicontinuous;
2. $G(x)\ne+\infty$ for every $x$;
3. $G$ is not identically $-\infty$;
4. there are $a,b\in\mathbb R$ with $a>0$ and

for every $x\in E$.

Then there is $x\in E$ such that $G(x)$ is neither $-\infty$ nor $+\infty$, and

Values equal to $-\infty$ are allowed away from the maximizing point. The lemma is a reusable attainment principle for extended-real objectives with positive linear decay.

Original Lean declaration header

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

theorem exists_finite_maximum_of_upperSemicontinuous_linear_decay
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E]
    (G : E → EReal) (husc : UpperSemicontinuous G)
    (hnotTop : ∀ x : E, G x ≠ ⊤) (hfinite : ∃ x : E, G x ≠ ⊥)
    (a b : ℝ) (ha : 0 < a)
    (hdecay : ∀ x : E, G x ≤ ((b - a * ‖x‖ : ℝ) : EReal)) :
    ∃ x : E, G x ≠ ⊥ ∧ G x ≠ ⊤ ∧ ∀ z : E, G z ≤ G x

Module navigation

Module: Analysis/Extremum.

Source excerpt, lines 23–30 · Frozen source 408915f.