Radial Extension Has Its Radial Limit

This auxiliary lemma establishes radial continuity of a convex radial extension.

Let $E$ be finite-dimensional over $\mathbb R$, let $K\subseteq E$ be open with $0\in K$, and let $g:E\to\mathbb R$ be convex on $K$. Assume:

1. $g(x)\ge0$ for every $x\in K$.
2. $g(0)=0$.

For every $x\in E$, the radial extension radialExtension K g satisfies

as $t\to1$ from below.

This is an internal continuity property used in constructing extended-real convex limits.

Original Lean declaration header

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

private lemma radialExtension_radial_limit {K : Set E} (hK : IsOpen K) (h0K : (0 : E) ∈ K)
    {g : E → ℝ} (hg : ConvexOn ℝ K g) (hnn : ∀ x ∈ K, 0 ≤ g x) (hg0 : g 0 = 0) (x : E) :
    Tendsto (fun t : ℝ => radialExtension K g (t • x)) (nhdsWithin 1 (Set.Iio 1))
      (nhds (radialExtension K g x))

Module navigation

Module: Analysis/Convex/RadialExtension.

Source excerpt, lines 208–211 · Frozen source 408915f.