Lower Semicontinuity Of The Secant Supremum

This lemma establishes lower semicontinuity of each fixed-radius secant supremum.

Let $X$ be a metric space, let $f:X\to\mathbb R$ be continuous, and let $r\in\mathbb R$. Define secant f r at $x$ as the supremum, over points $y$ with $d(y,x)<r$, of the extended quotient

Then the map $x\mapsto\operatorname{secant}(f,r)(x)$ is lower semicontinuous:

The Lean declaration is lowerSemicontinuous_secant_readable. The secant values are ENNReal values, so the conclusion allows the value $\top$.

Original Lean declaration header

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

theorem lowerSemicontinuous_secant {f : X → ℝ} (hf : Continuous f) (r : ℝ) :
    LowerSemicontinuous (secant f r)

Module navigation

Module: Energy/Euclidean/Slope/Density.

Definition modules: Energy/Euclidean/Slope/Recovery.

Next: exists_thickening_pairwise_disjoint.

Source excerpt, lines 64–65 · Frozen source 408915f.