Rockafellar, §10: Continuity of Convex Functions

The situations in which a convex function is automatically upper semicontinuous, hence continuous, together with the equi-Lipschitz and convergence theory that follows from them. All 13 numbered results of §10 are formalized. The section is entirely finite-dimensional: every result rests on Theorem 6.2 — a non-empty convex set has a non-empty relative interior — somewhere.

The section's definitions

• Continuity relative to S is ContinuousOn f S, identified with continuity of the restriction — the book's own phrasing — by continuousOn_iff_continuous_restrict_rn.
• Locally simplicial is the backbone's LocallySimplicial, transcribed without change.
• Lipschitzian relative to S is LipschitzianOn, with the bridge lipschitzianOn_iff; equi-Lipschitzian is EquiLipschitzianOn, with equiLipschitzianOn_iff giving a single K for the whole family.
• Pointwise bounded and uniformly bounded on S are PointwiseBoundedOn and UniformlyBoundedOn, with bridges pointwiseBoundedOn_iff and uniformlyBoundedOn_iff.

corollary_10_5_1 spells the book's liminf_{λ → ∞} f (λ y) / λ < ∞ as "for some c, f (a y) ≤ c a for arbitrarily large a", which avoids an EReal division convention; the two agree because the quotient is nondecreasing in λ (Theorem 8.5). Hypothesis (a) of theorem_10_6 is stated with cl C' where the book writes conv (cl C').

theorem_10_2 is unconditional. Rockafellar's proof triangulates a simplex around an interior point, a step he calls intuitively obvious and does not prove; upper semicontinuity relative to a simplex is instead obtained at every point of it by a direct barycentric estimate, so §20 inherits no obligation from §10.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §10.

The definitions of §10

theorem Rockafellar.continuousOn_iff_continuous_restrict_rn {n : ℕ} (f : TdafSurface.Rn n → EReal) (S : Set (TdafSurface.Rn n)) : ContinuousOn f S ↔ Continuous (S.domRestrict f)

Continuity relative to S (Rockafellar, §10, p. 82): the restriction of f to S is a continuous function. This is ContinuousOn, and the identification is Mathlib's.

def Rockafellar.LipschitzianOn {n : ℕ} (f : TdafSurface.Rn n → ℝ) (S : Set (TdafSurface.Rn n)) : Prop

Lipschitzian relative to S (Rockafellar, §10, p. 86): a real-valued function f on S ⊆ ℝⁿ for which there is a single α ≥ 0 with |f y - f x| ≤ α ‖y - x‖ for all x, y ∈ S.

Equations

• Rockafellar.LipschitzianOn f S = ∃ (α : ℝ), 0 ≤ α ∧ ∀ y ∈ S, ∀ x ∈ S, |f y - f x| ≤ α * ‖y - x‖

def Rockafellar.EquiLipschitzianOn {n : ℕ} {ι : Type u_1} (f : ι → TdafSurface.Rn n → ℝ) (S : Set (TdafSurface.Rn n)) : Prop

Equi-Lipschitzian relative to S (Rockafellar, §10, p. 88): one α ≥ 0 serves every member of the family.

Equations

• Rockafellar.EquiLipschitzianOn f S = ∃ (α : ℝ), 0 ≤ α ∧ ∀ (i : ι), ∀ y ∈ S, ∀ x ∈ S, |f i y - f i x| ≤ α * ‖y - x‖

def Rockafellar.PointwiseBoundedOn {n : ℕ} {ι : Type u_1} (f : ι → TdafSurface.Rn n → ℝ) (S : Set (TdafSurface.Rn n)) : Prop

Pointwise bounded on S (Rockafellar, §10, p. 88): the set of real numbers f i x, i ∈ I, is bounded for each x ∈ S.

Equations

• Rockafellar.PointwiseBoundedOn f S = ∀ x ∈ S, Bornology.IsBounded (Set.range fun (i : ι) => f i x)

def Rockafellar.UniformlyBoundedOn {n : ℕ} {ι : Type u_1} (f : ι → TdafSurface.Rn n → ℝ) (S : Set (TdafSurface.Rn n)) : Prop

Uniformly bounded on S (Rockafellar, §10, p. 88): α₁ ≤ f i x ≤ α₂ for all x ∈ S and all i ∈ I, with α₁ and α₂ independent of both.

Equations

• Rockafellar.UniformlyBoundedOn f S = ∃ (α₁ : ℝ) (α₂ : ℝ), ∀ x ∈ S, ∀ (i : ι), α₁ ≤ f i x ∧ f i x ≤ α₂

theorem Rockafellar.lipschitzianOn_iff {n : ℕ} {f : TdafSurface.Rn n → ℝ} {S : Set (TdafSurface.Rn n)} : LipschitzianOn f S ↔ ∃ (K : NNReal), LipschitzOnWith K f S

The bridge for LipschitzianOn: Rockafellar's Lipschitz condition is Mathlib's LipschitzOnWith with the constant left existentially quantified.

theorem Rockafellar.equiLipschitzianOn_iff {n : ℕ} {ι : Type u_1} {f : ι → TdafSurface.Rn n → ℝ} {S : Set (TdafSurface.Rn n)} : EquiLipschitzianOn f S ↔ ∃ (K : NNReal), ∀ (i : ι), LipschitzOnWith K (f i) S

The bridge for EquiLipschitzianOn: a single ℝ≥0 constant serving the whole family.

theorem Rockafellar.pointwiseBoundedOn_iff {n : ℕ} {ι : Type u_1} {f : ι → TdafSurface.Rn n → ℝ} {S : Set (TdafSurface.Rn n)} : PointwiseBoundedOn f S ↔ ∀ x ∈ S, BddBelow (Set.range fun (i : ι) => f i x) ∧ BddAbove (Set.range fun (i : ι) => f i x)

The bridge for PointwiseBoundedOn: boundedness of a set of reals is two-sided boundedness, which is the shape the backbone's hypotheses take.

theorem Rockafellar.uniformlyBoundedOn_iff {n : ℕ} {ι : Type u_1} {f : ι → TdafSurface.Rn n → ℝ} {S : Set (TdafSurface.Rn n)} : UniformlyBoundedOn f S ↔ ∃ (M : ℝ), 0 ≤ M ∧ ∀ (i : ι), ∀ x ∈ S, |f i x| ≤ M

The bridge for UniformlyBoundedOn: a two-sided uniform bound is a bound on |f i x|, which is the shape the backbone's conclusions take.

Theorem 10.1

theorem Rockafellar.theorem_10_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCro : intrinsicInterior ℝ C = C) (hCdom : C ⊆ Tdaf.ConvexAnalysis.dom f) : ContinuousOn f C

Theorem 10.1. A convex function f on ℝⁿ is continuous relative to any relatively open convex set C in its effective domain — in particular relative to ri (dom f), which is corollary_10_1_1's and Theorem 10.4's form. The improper case is not excluded.

Corollary 10.1.1

theorem Rockafellar.corollary_10_1_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) (hdom : Tdaf.ConvexAnalysis.dom f = Set.univ) : Continuous f

Corollary 10.1.1. A convex function finite on all of ℝⁿ is necessarily continuous. "finite on all of ℝⁿ" is dom f = univ together with properness, which is the ≠ -∞ half.

Theorem 10.2

theorem Rockafellar.theorem_10_2 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) {S : Set (TdafSurface.Rn n)} (hS : Tdaf.ConvexAnalysis.LocallySimplicial S) (hSdom : S ⊆ Tdaf.ConvexAnalysis.dom f) : UpperSemicontinuousOn f S

Theorem 10.2. Let f be a convex function on ℝⁿ, and let S be any locally simplicial subset of dom f. Then f is upper semicontinuous relative to S. Improperness is not excluded; see the module docstring on the triangulation step the book leaves unproved.

theorem Rockafellar.theorem_10_2_closed {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hcl : Tdaf.ConvexAnalysis.ClosedFn f) {S : Set (TdafSurface.Rn n)} (hS : Tdaf.ConvexAnalysis.LocallySimplicial S) (hSdom : S ⊆ Tdaf.ConvexAnalysis.dom f) : ContinuousOn f S

Theorem 10.2, second assertion: if f is closed then f is continuous relative to S.

Theorem 10.3

theorem Rockafellar.theorem_10_3 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCls : Tdaf.ConvexAnalysis.LocallySimplicial C) (hne : C.Nonempty) {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hbot : ∀ (x : TdafSurface.Rn n), f x ≠ ⊥) (hdom : Tdaf.ConvexAnalysis.dom f = intrinsicInterior ℝ C) (hbdd : ∀ S ⊆ intrinsicInterior ℝ C, Bornology.IsBounded S → ∃ (c : ℝ), ∀ x ∈ S, f x ≤ ↑c) : ∃ (g : TdafSurface.Rn n → EReal), Tdaf.ConvexAnalysis.ConvexFn g ∧ Tdaf.ConvexAnalysis.ClosedFn g ∧ Tdaf.ConvexAnalysis.Proper g ∧ Set.EqOn g f (intrinsicInterior ℝ C) ∧ C ⊆ Tdaf.ConvexAnalysis.dom g ∧ ContinuousOn g C

Theorem 10.3. Let C be a locally simplicial convex set, and let f be a finite convex function on ri C which is bounded above on every bounded subset of ri C. Then f can be extended to a continuous finite convex function on the whole of C.

"A finite convex function on ri C" is a convex f : ℝⁿ → (-∞, +∞] with dom f = ri C, which is how §4 reads a function given only on a set. The extension produced is cl f.

theorem Rockafellar.theorem_10_3_unique {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) {g₁ g₂ : TdafSurface.Rn n → EReal} (h₁ : ContinuousOn g₁ C) (h₂ : ContinuousOn g₂ C) (h : Set.EqOn g₁ g₂ (intrinsicInterior ℝ C)) : Set.EqOn g₁ g₂ C

Theorem 10.3, uniqueness: there can be only one such extension, since C ⊆ cl (ri C). Neither local simpliciality of C nor convexity of the two functions is needed.

Theorem 10.4

theorem Rockafellar.theorem_10_4 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) {S : Set (TdafSurface.Rn n)} (hScl : IsClosed S) (hSb : Bornology.IsBounded S) (hSri : S ⊆ intrinsicInterior ℝ (Tdaf.ConvexAnalysis.dom f)) : LipschitzianOn (fun (x : TdafSurface.Rn n) => (f x).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. The Lipschitz condition is about real values, so the statement is about (f ·).toReal, faithful on dom f by properness.

Theorem 10.5

theorem Rockafellar.theorem_10_5 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) (hdom : Tdaf.ConvexAnalysis.dom f = Set.univ) : (UniformContinuous fun (x : TdafSurface.Rn n) => (f x).toReal) ↔ ∀ (y : TdafSurface.Rn n), Tdaf.ConvexAnalysis.recessionFn f y ≠ ⊤

Theorem 10.5. Let f be a finite convex function on ℝⁿ. In order that f be uniformly continuous relative to ℝⁿ, it is necessary and sufficient that the recession function f0⁺ be finite everywhere. "Finite everywhere" is spelled ≠ ⊤; the other half, f0⁺ ≠ -∞, is automatic from properness of f.

theorem Rockafellar.theorem_10_5_lipschitzian {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) (hdom : Tdaf.ConvexAnalysis.dom f = Set.univ) (hrec : ∀ (y : TdafSurface.Rn n), Tdaf.ConvexAnalysis.recessionFn f y ≠ ⊤) : LipschitzianOn (fun (x : TdafSurface.Rn n) => (f x).toReal) Set.univ

Theorem 10.5, second assertion: in that event f is Lipschitzian relative to ℝⁿ, with Rockafellar's constant α = sup {(f0⁺) z | ‖z‖ = 1}.

Corollary 10.5.1

theorem Rockafellar.corollary_10_5_1 {n : ℕ} {f : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) (hdom : Tdaf.ConvexAnalysis.dom f = Set.univ) (h : ∀ (y : TdafSurface.Rn n), ∃ (c : ℝ), ∃ᶠ (a : ℝ) in Filter.atTop, f (a • y) ≤ ↑(c * a)) : LipschitzianOn (fun (x : TdafSurface.Rn n) => (f x).toReal) Set.univ

Corollary 10.5.1. A finite convex function f is Lipschitzian relative to ℝⁿ if liminf_{λ → ∞} f (λ y) / λ < ∞ for every y. The liminf is spelled "for some c, f (a y) ≤ c a for arbitrarily large a", avoiding the EReal quotient; the two agree because the quotient is nondecreasing in λ (Theorem 8.5).

Corollary 10.5.2

theorem Rockafellar.corollary_10_5_2 {n : ℕ} {f g : TdafSurface.Rn n → EReal} (hf : Tdaf.ConvexAnalysis.ConvexFn f) (hp : Tdaf.ConvexAnalysis.Proper f) (hdom : Tdaf.ConvexAnalysis.dom f = Set.univ) (_hg : Tdaf.ConvexAnalysis.ConvexFn g) (hgp : Tdaf.ConvexAnalysis.Proper g) (hgdom : Tdaf.ConvexAnalysis.dom g = Set.univ) (hglip : LipschitzianOn (fun (x : TdafSurface.Rn n) => (g x).toReal) Set.univ) (hle : ∀ (x : TdafSurface.Rn n), f x ≤ g x) : LipschitzianOn (fun (x : TdafSurface.Rn n) => (f x).toReal) Set.univ

Corollary 10.5.2. Every finite convex f below a finite convex g that is Lipschitzian relative to ℝⁿ is itself Lipschitzian relative to ℝⁿ. Convexity of g is carried so that the statement is the book's; the estimate needs only that g is Lipschitz.

Theorem 10.6

theorem Rockafellar.theorem_10_6 {n : ℕ} {ι : Type u_1} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCro : intrinsicInterior ℝ C = C) {f : ι → TdafSurface.Rn n → ℝ} (hf : ∀ (i : ι), ConvexOn ℝ C (f i)) (hbdd : PointwiseBoundedOn f C) {S : Set (TdafSurface.Rn n)} (hScl : IsClosed S) (hSb : Bornology.IsBounded S) (hSC : S ⊆ C) : UniformlyBoundedOn f S ∧ EquiLipschitzianOn f S

Theorem 10.6. Let C be a relatively open convex set, and let {f i | i ∈ I} be an arbitrary collection of convex functions finite and pointwise bounded on C. Let S be any closed bounded subset of C. Then {f i} is uniformly bounded on S and equi-Lipschitzian relative to S.

"Relatively open" is ri C = C; "finite and convex on C" is Mathlib's real-valued ConvexOn ℝ C, exactly as the book's collection is. I may be empty.

theorem Rockafellar.theorem_10_6_ab {n : ℕ} {ι : Type u_1} {C C' : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCro : intrinsicInterior ℝ C = C) {f : ι → TdafSurface.Rn n → ℝ} (hf : ∀ (i : ι), ConvexOn ℝ C (f i)) (hC'sub : C' ⊆ C) (hdense : C ⊆ closure C') (hab : ∀ x ∈ C', BddAbove (Set.range fun (i : ι) => f i x)) (hbe : ∃ z ∈ C, BddBelow (Set.range fun (i : ι) => f i z)) {S : Set (TdafSurface.Rn n)} (hScl : IsClosed S) (hSb : Bornology.IsBounded S) (hSC : S ⊆ C) : UniformlyBoundedOn f S ∧ EquiLipschitzianOn f S

Theorem 10.6, weakened hypotheses: the conclusion survives if pointwise boundedness is replaced by

(a) a subset C' of C with cl C' ⊇ C on which sup {f i x | i ∈ I} is finite, and (b) at least one x ∈ C at which inf {f i x | i ∈ I} is finite.

The book's (a) reads conv (cl C') ⊇ C, which is weaker than the cl C' ⊇ C used here.

Theorem 10.7

theorem Rockafellar.theorem_10_7 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCro : intrinsicInterior ℝ C = C) {T : Type u_1} [TopologicalSpace T] [LocallyCompactSpace T] {F : TdafSurface.Rn n × T → ℝ} (hconv : ∀ (t : T), ConvexOn ℝ C fun (x : TdafSurface.Rn n) => F (x, t)) (hcont : ∀ x ∈ C, Continuous fun (t : T) => F (x, t)) : ContinuousOn F (C ×ˢ Set.univ)

Theorem 10.7. Let C be a relatively open convex set in ℝⁿ, and let T be any locally compact topological space. Let f be a real-valued function on C × T such that f (x, t) is convex in x for each t and continuous in t for each x. Then f is jointly continuous on C × T. T is a type, so the conclusion is ContinuousOn F (C ×ˢ univ).

theorem Rockafellar.theorem_10_7_dense {n : ℕ} {C C' : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCro : intrinsicInterior ℝ C = C) {T : Type u_1} [TopologicalSpace T] [LocallyCompactSpace T] {F : TdafSurface.Rn n × T → ℝ} (hconv : ∀ (t : T), ConvexOn ℝ C fun (x : TdafSurface.Rn n) => F (x, t)) (hC'sub : C' ⊆ C) (hdense : C ⊆ closure C') (hcont : ∀ x ∈ C', Continuous fun (t : T) => F (x, t)) : ContinuousOn F (C ×ˢ Set.univ)

Theorem 10.7, weakened hypothesis: it is enough that f (x, ·) be continuous for each x in some subset C' of C with cl C' ⊇ C. Specialises continuousOn_prod_of_convexOn_relint directly.

Theorem 10.8

theorem Rockafellar.theorem_10_8 {n : ℕ} {C C' : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCro : intrinsicInterior ℝ C = C) {f : ℕ → TdafSurface.Rn n → ℝ} (hf : ∀ (i : ℕ), ConvexOn ℝ C (f i)) (hC'sub : C' ⊆ C) (hdense : C ⊆ closure C') (hcv : ∀ x ∈ C', ∃ (L : ℝ), Filter.Tendsto (fun (i : ℕ) => f i x) Filter.atTop (nhds L)) : ∃ (g : TdafSurface.Rn n → ℝ), ConvexOn ℝ C g ∧ (∀ x ∈ C, Filter.Tendsto (fun (i : ℕ) => f i x) Filter.atTop (nhds (g x))) ∧ ∀ ⦃S : Set (TdafSurface.Rn n)⦄, IsClosed S → Bornology.IsBounded S → S ⊆ C → TendstoUniformlyOn f g Filter.atTop S

Theorem 10.8. Let C be a relatively open convex set and f 1, f 2, … a sequence of finite convex functions on C converging pointwise on a subset C' of C with cl C' ⊇ C. The limit then exists for every x ∈ C, is finite and convex, and the convergence is uniform on each closed bounded subset of C.

Corollary 10.8.1

theorem Rockafellar.corollary_10_8_1 {n : ℕ} {C : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCro : intrinsicInterior ℝ C = C) {f : ℕ → TdafSurface.Rn n → ℝ} (hf : ∀ (i : ℕ), ConvexOn ℝ C (f i)) {g : TdafSurface.Rn n → ℝ} (hg : ConvexOn ℝ C g) (hle : ∀ x ∈ C, ∀ δ > 0, ∀ᶠ (i : ℕ) in Filter.atTop, f i x ≤ g x + δ) {S : Set (TdafSurface.Rn n)} (hScl : IsClosed S) (hSb : Bornology.IsBounded S) (hSC : S ⊆ C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ℕ) in Filter.atTop, ∀ x ∈ S, f i x ≤ g x + ε

Corollary 10.8.1. Let f be a finite convex function on a relatively open convex set C, and f 1, f 2, … finite convex functions on C with limsup_i f i x ≤ f x for every x ∈ C. Then for each closed bounded S ⊆ C and each ε > 0 there is an i₀ with f i x ≤ f x + ε for all i ≥ i₀ and all x ∈ S. The limsup hypothesis is spelled "for every δ > 0, eventually f i x ≤ f x + δ", which is what it means for a real sequence.

Theorem 10.9

theorem Rockafellar.theorem_10_9 {n : ℕ} {C C' : Set (TdafSurface.Rn n)} (hC : Convex ℝ C) (hCro : intrinsicInterior ℝ C = C) {f : ℕ → TdafSurface.Rn n → ℝ} (hf : ∀ (i : ℕ), ConvexOn ℝ C (f i)) (hC'sub : C' ⊆ C) (hdense : C ⊆ closure C') (hbdd : PointwiseBoundedOn f C') : ∃ (φ : ℕ → ℕ) (g : TdafSurface.Rn n → ℝ), StrictMono φ ∧ ConvexOn ℝ C g ∧ (∀ x ∈ C, Filter.Tendsto (fun (i : ℕ) => f (φ i) x) Filter.atTop (nhds (g x))) ∧ ∀ ⦃S : Set (TdafSurface.Rn n)⦄, IsClosed S → Bornology.IsBounded S → S ⊆ C → TendstoUniformlyOn (fun (i : ℕ) => f (φ i)) g Filter.atTop S

Theorem 10.9. Let C be a relatively open convex set and f 1, f 2, … a sequence of finite convex functions on C whose values are bounded at each point of a dense subset C' of C. It is then possible to select a subsequence converging uniformly on closed bounded subsets of C to some finite convex function f.