Limits and continuous extensions of convex functions

A pointwise limit, on a set s, of functions that are eventually convex on s is convex on s. This is the closedness of the set of convex functions (isClosed_setOfPred_convexOn) applied to functions that are only known to converge on s.

A function convex on s and continuous on closure s remains convex on that closure (ConvexOn.closure_of_continuousOn).

A convex function on (0, ∞) bounded above by L stays convex when extended by the value L at 0 (ConvexOn.apply_mul_le_of_forall_le), as the limit of convex combinations approaching 0.

On a set with compact closure, a convex function v continuous on the closure can be rescaled and shifted to (1 + ε) v + b so that it passes from above to below an arbitrary function u (TauCeti.exists_convexOn_lt_frontier_of_lt).

theorem TauCeti.convexOn_of_tendsto {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [PartialOrder β] [TopologicalSpace β] [OrderClosedTopology β] [AddCommMonoid α] [AddCommMonoid β] [SMul 𝕜 α] [SMul 𝕜 β] [ContinuousConstSMul 𝕜 β] [ContinuousAdd β] {l : Filter ι} [l.NeBot] {F : ι → α → β} {f : α → β} {s : Set α} (hF : ∀ᶠ (i : ι) in l, ConvexOn 𝕜 s (F i)) (hf : ∀ x ∈ s, Filter.Tendsto (fun (i : ι) => F i x) l (nhds (f x))) : ConvexOn 𝕜 s f

A pointwise limit of convex functions is convex. If the functions F i are eventually convex on s and converge to f at every point of s, then f is convex on s.

theorem TauCeti.exists_convexOn_lt_frontier_of_lt {E : Type u_5} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] {Ω : Set E} {u v : E → ℝ} (hΩ : IsCompact (closure Ω)) (hv : ConvexOn ℝ Ω v) (hvc : ContinuousOn v (closure Ω)) (hfr : ∀ x ∈ frontier Ω, v x ≤ u x) {x₀ : E} (hx₀ : x₀ ∈ Ω) (hlt : u x₀ < v x₀) : ∃ ε > 0, ∃ (b : ℝ), ContinuousOn (fun (y : E) => (1 + ε) * v y + b) (closure Ω) ∧ (ConvexOn ℝ Ω fun (y : E) => (1 + ε) * v y + b) ∧ (∀ y ∈ frontier Ω, (1 + ε) * v y + b < u y) ∧ u x₀ < (1 + ε) * v x₀ + b

If v ≤ u on the frontier of a set Ω with compact closure and u x₀ < v x₀ at some x₀ ∈ Ω, with v convex on Ω and continuous on its closure (nothing is assumed of u), then for a small ε > 0 and a constant b the function (1 + ε) v + b is convex on Ω and continuous on its closure, lies below u on the frontier, and lies above u at x₀.

theorem ConvexOn.apply_mul_le_of_forall_le {φ : ℝ → ℝ} (hφ : ConvexOn ℝ (Set.Ioi 0) φ) {L : ℝ} (hL : ∀ s ∈ Set.Ioi 0, φ s ≤ L) {x b : ℝ} (hx : 0 < x) (hb₀ : 0 < b) (hb₁ : b ≤ 1) : φ (b * x) ≤ b * φ x + (1 - b) * L

A convex function φ on (0, ∞) bounded above by L satisfies φ (b x) ≤ b φ x + (1 - b) L for x > 0 and 0 < b ≤ 1: extending φ by the value L at 0 keeps it convex on [0, ∞). For φ(s) = sⁿ U(s⁻ⁿ) nonincreasing, the best such bound is the recession constant of U, since U(r) / r = φ(r^{-1/n}).

theorem ConvexOn.closure_of_continuousOn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [PartialOrder F] [SMul 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [OrderClosedTopology F] {s : Set E} {f : E → F} (hf : ConvexOn 𝕜 s f) (hc : ContinuousOn f (closure s)) : ConvexOn 𝕜 (closure s) f

A convex function that is continuous on the closure remains convex on that closure.