theorem properConvexFunctionOn_lipschitzRelativeTo_of_isClosed_isBounded_subset_ri_effectiveDomain {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {S : Set (EuclideanSpace ℝ (Fin n))} (hSclosed : IsClosed S) (hSbdd : Bornology.IsBounded S) (hSsubset : S ⊆ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ f)) : Function.LipschitzRelativeTo (fun (x : EuclideanSpace ℝ (Fin n)) => (f x.ofLp).toReal) S

Theorem 10.4. Let f be a proper convex function, and let S be any closed bounded subset of ri (dom f). Then f is Lipschitzian relative to S.

theorem Section10.toLp_coeFn_eq {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) : WithLp.toLp 2 x.ofLp = x

WithLp.toLp is a two-sided coercion between Fin n → ℝ and the Euclidean space ℝ^n = EuclideanSpace ℝ (Fin n); converting to a function and back gives the same point.

theorem Function.LipschitzRelativeTo.mono {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {S T : Set (EuclideanSpace ℝ (Fin n))} (hT : LipschitzRelativeTo f T) (hST : S ⊆ T) : LipschitzRelativeTo f S

A Lipschitz function on a set remains Lipschitz when restricting to a subset.

theorem Section10.euclideanRelativeInterior_univ (n : ℕ) : euclideanRelativeInterior n Set.univ = Set.univ

The relative interior of the whole Euclidean space is the whole space.

theorem Section10.properConvexFunctionOn_univ_coe_comp_toLp_of_convexOn {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ Set.univ f) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(f (WithLp.toLp 2 x))

A finite convex function on ℝ^n yields a proper convex EReal-valued function on univ by coercing to EReal (after viewing Fin n → ℝ as ℝ^n via WithLp.toLp).

theorem convexOn_uniformContinuousOn_and_lipschitzRelativeTo_of_isBounded {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ Set.univ f) (S : Set (EuclideanSpace ℝ (Fin n))) : Bornology.IsBounded S → UniformContinuousOn f S ∧ Function.LipschitzRelativeTo f S

Theorem 10.4.1. Let f : ℝ^n → ℝ be a finite convex function. Then f is uniformly continuous, and even Lipschitzian, relative to every bounded subset of ℝ^n.

noncomputable def Function.recessionFunction {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) : EuclideanSpace ℝ (Fin n) → EReal

The recession function f₀⁺ of a real-valued function f on ℝ^n, defined by f₀⁺(y) = sup_x (f(x + y) - f(x)) (as an extended real).

Equations

• Function.recessionFunction f y = sSup {r : EReal | ∃ (x : EuclideanSpace ℝ (Fin n)), r = ↑(f (x + y) - f x)}

def Function.RecessionFunctionFiniteEverywhere {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) : Prop

The recession function f₀⁺ is finite everywhere (i.e. takes values in ℝ).

Equations

• Function.RecessionFunctionFiniteEverywhere f = ∀ (y : EuclideanSpace ℝ (Fin n)), ∃ (r : ℝ), Function.recessionFunction f y = ↑r

theorem Section10.recessionFunction_diff_le {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (x y : EuclideanSpace ℝ (Fin n)) : ↑(f (x + y) - f x) ≤ Function.recessionFunction f y

Any increment f(x+y)-f x is bounded above by the recession function f₀⁺(y).

theorem Section10.recessionFunction_zero {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} : Function.recessionFunction f 0 = 0

The recession function f₀⁺ is zero at the origin.

theorem Section10.recessionFunction_ne_bot {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (y : EuclideanSpace ℝ (Fin n)) : Function.recessionFunction f y ≠ ⊥

The recession function never takes the value ⊥.

theorem Section10.recessionFunctionFiniteEverywhere_of_uniformContinuousOn_univ {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hu : UniformContinuousOn f Set.univ) : Function.RecessionFunctionFiniteEverywhere f

Uniform continuity of f on univ forces its recession function to be finite everywhere.

theorem Section10.lipschitzRelativeTo_univ_of_recessionFunctionFiniteEverywhere {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ Set.univ f) (hfin : Function.RecessionFunctionFiniteEverywhere f) : Function.LipschitzRelativeTo f Set.univ

If the recession function is finite everywhere, a convex function is Lipschitz on univ.

theorem convexOn_uniformContinuousOn_univ_iff_recessionFunctionFiniteEverywhere {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ Set.univ f) : (UniformContinuousOn f Set.univ ↔ Function.RecessionFunctionFiniteEverywhere f) ∧ (Function.RecessionFunctionFiniteEverywhere f → Function.LipschitzRelativeTo f Set.univ)

Theorem 10.5. Let f be a finite convex function on ℝ^n. In order that f be uniformly continuous relative to ℝ^n, it is necessary and sufficient that the recession function f₀⁺ of f be finite everywhere. In this event, f is actually Lipschitzian relative to ℝ^n.

theorem Section10.closedConvexFunction_coe_comp_toLp_of_convexOn {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ Set.univ f) : ClosedConvexFunction fun (x : Fin n → ℝ) => ↑(f (WithLp.toLp 2 x))

A finite convex function on ℝ^n yields a closed convex EReal-valued function on univ after composing with WithLp.toLp and coercing to EReal.

theorem Section10.tendsto_div_sub_to_recessionFunction {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ Set.univ f) (y : EuclideanSpace ℝ (Fin n)) : Filter.Tendsto (fun (t : ℝ) => ↑((f (t • y) - f 0) / t)) Filter.atTop (nhds (Function.recessionFunction f y))

Along a ray, the difference quotient (f(t•y) - f(0))/t converges to the recession function.

This is Theorem 8.5 specialized to x = 0 and rewritten in terms of Function.recessionFunction.

theorem Section10.recessionFunctionFiniteEverywhere_of_liminf_div_lt_top {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ Set.univ f) (hlim : ∀ (y : EuclideanSpace ℝ (Fin n)), Filter.liminf (fun (t : ℝ) => ↑(f (t • y) / t)) Filter.atTop < ⊤) : Function.RecessionFunctionFiniteEverywhere f

If liminf_{t→∞} f(t•y)/t is finite for all y, then the recession function is finite everywhere.

theorem convexOn_lipschitzRelativeTo_univ_of_liminf_div_lt_top {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ Set.univ f) (hlim : ∀ (y : EuclideanSpace ℝ (Fin n)), Filter.liminf (fun (t : ℝ) => ↑(f (t • y) / t)) Filter.atTop < ⊤) : Function.LipschitzRelativeTo f Set.univ

Corollary 10.5.1. A finite convex function f is Lipschitzian relative to ℝ^n if liminf_{λ → ∞} f(λ • y) / λ < ∞ for all y.

theorem Section10.liminf_le_liminf_of_eventually_le {α : Type u_1} {l : Filter α} {u v : α → EReal} (h : ∀ᶠ (a : α) in l, u a ≤ v a) : Filter.liminf u l ≤ Filter.liminf v l

If u ≤ v eventually along a filter, then liminf u ≤ liminf v.