Lower Semicontinuity After Closed-Ball Capping

This proves preservation of lower semicontinuity under the closed-ball cap operation.

Let $E$ be a normed additive commutative group, let $\varphi:E\to[-\infty,\infty]$ be extended-real valued, and let $L\in[0,\infty)$. If $\varphi$ is lower semicontinuous, then closedBallCap φ L is lower semicontinuous:

The operation agrees with $\varphi$ on the closed ball of radius $L$ centered at $0$ and takes the value $+\infty$ outside it. The declaration is closedBallCap_lowerSemicontinuous_readable; no inner-product, finite-dimensional, or measurable-space assumptions are present in the statement.

Original Lean declaration header

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

theorem closedBallCap_lowerSemicontinuous
 (φ : E → EReal) (L : NNReal)
    (hφ : LowerSemicontinuous φ) : LowerSemicontinuous (closedBallCap φ L)

Module navigation

Module: Analysis/Convex/BoundedConjugate.

Next: exists_real_global_minimum_of_bounded_domain.

Source excerpt, lines 43–45 · Frozen source 408915f.