theorem Section10.exists_closedBall_subset_of_isOpen {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) {x0 : EuclideanSpace ℝ (Fin n)} (hx0 : x0 ∈ C) : ∃ (r : ℝ), 0 < r ∧ Metric.closedBall x0 r ⊆ C

If C is open and x₀ ∈ C, then some closed ball around x₀ is contained in C.

theorem Section10.exists_compact_mem_nhds_of_locallyCompact {T : Type u_1} [TopologicalSpace T] [LocallyCompactSpace T] (t0 : T) : ∃ (K : Set T), IsCompact K ∧ K ∈ nhds t0

In a locally compact space, every point admits a compact neighborhood.

theorem Section10.isBounded_range_subtype_of_continuous_compact {T : Type u_1} [TopologicalSpace T] {K : Set T} (hK : IsCompact K) {g : T → ℝ} (hg : Continuous g) : Bornology.IsBounded (Set.range fun (t : { t : T // t ∈ K }) => g ↑t)

A continuous real-valued function is bounded on a compact set (rephrased over a subtype).

theorem convexOn_continuousOn_prod_of_locallyCompact {n : ℕ} {T : Type u_1} [TopologicalSpace T] [LocallyCompactSpace T] {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : EuclideanSpace ℝ (Fin n) × T → ℝ) (hfconv : ∀ (t : T), ConvexOn ℝ C fun (x : EuclideanSpace ℝ (Fin n)) => f (x, t)) (hfcont : ∀ 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 ℝ^n, and let T be a locally compact topological space. Let f : ℝ^n × T → ℝ be such that:

• for each t ∈ T, the function x ↦ f (x,t) is convex on C;
• for each x ∈ C, the function t ↦ f (x,t) is continuous on T.

Then f is continuous on C × T (i.e. jointly continuous in x and t).

theorem convexOn_continuousOn_prod_of_locallyCompact_of_exists_subset_closure {n : ℕ} {T : Type u_1} [TopologicalSpace T] [LocallyCompactSpace T] {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : EuclideanSpace ℝ (Fin n) × T → ℝ) (hfconv : ∀ (t : T), ConvexOn ℝ C fun (x : EuclideanSpace ℝ (Fin n)) => f (x, t)) {C' : Set (EuclideanSpace ℝ (Fin n))} (hC'sub : C' ⊆ C) (hCclosure : C ⊆ closure C') (hfcont : ∀ x ∈ C', Continuous fun (t : T) => f (x, t)) : ContinuousOn f (C ×ˢ Set.univ)

Theorem 10.7 (variant). The same conclusion holds if the continuity-in-t assumption is weakened as follows: there exists C' ⊆ C with closure C' ⊇ C such that t ↦ f (x,t) is continuous for each x ∈ C'.

theorem Section10.exists_point_mem_C'_mem_S'_dist_lt_of_mem_interior_of_mem_closure {n : ℕ} {C' S' : Set (EuclideanSpace ℝ (Fin n))} {x : EuclideanSpace ℝ (Fin n)} (hxS' : x ∈ interior S') (hxC' : x ∈ closure C') (δ : ℝ) : 0 < δ → ∃ z ∈ C', z ∈ S' ∧ dist z x < δ

If x ∈ interior S' and x ∈ closure C', then for every δ > 0 there exists a point z ∈ C' ∩ S' within distance δ of x.

theorem Section10.exists_finset_net_in_C'_inter_S'_cover {n : ℕ} {C' S S' : Set (EuclideanSpace ℝ (Fin n))} (hScomp : IsCompact S) (hSint : S ⊆ interior S') (hSclosure : S ⊆ closure C') (δ : ℝ) : 0 < δ → ∃ (t : Finset (EuclideanSpace ℝ (Fin n))), (∀ z ∈ t, z ∈ C' ∧ z ∈ S') ∧ ∀ x ∈ S, ∃ z ∈ t, dist x z < δ

A compact set admits a finite δ-net with points in C' ∩ S', provided C' is dense around points of S and S sits inside interior S'.

theorem Section10.exists_tail_cauchy_on_finset_of_pointwise_tendsto {n : ℕ} {f : ℕ → EuclideanSpace ℝ (Fin n) → ℝ} (t : Finset (EuclideanSpace ℝ (Fin n))) (hpoint : ∀ z ∈ t, ∃ (l : ℝ), Filter.Tendsto (fun (i : ℕ) => f i z) Filter.atTop (nhds l)) (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ i ≥ N, ∀ j ≥ N, ∀ z ∈ t, ‖f i z - f j z‖ < ε

A finite family of convergent real sequences is uniformly Cauchy on the index set.

theorem Section10.uniformCauchyOn_of_equiLipschitz_and_finset_net {n : ℕ} {f : ℕ → EuclideanSpace ℝ (Fin n) → ℝ} {S S' : Set (EuclideanSpace ℝ (Fin n))} {t : Finset (EuclideanSpace ℝ (Fin n))} {L : NNReal} (hL : ∀ (i : ℕ), LipschitzOnWith L (f i) S') (hSsub : S ⊆ S') (htsub : ∀ z ∈ t, z ∈ S') {ε δ : ℝ} (hδbound : (↑L + 1) * δ ≤ ε / 3) {N : ℕ} (hfin : ∀ i ≥ N, ∀ j ≥ N, ∀ z ∈ t, dist (f i z) (f j z) < ε / 3) (hcover : ∀ x ∈ S, ∃ z ∈ t, dist x z < δ) (i : ℕ) : i ≥ N → ∀ j ≥ N, ∀ x ∈ S, dist (f i x) (f j x) < ε

Triangle inequality estimate upgrading control on a finite δ-net to control on all of S under an equi-Lipschitz hypothesis.

theorem Section10.convexOn_lim_of_pointwise_tendsto {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCconv : Convex ℝ C) {f : ℕ → EuclideanSpace ℝ (Fin n) → ℝ} {g : EuclideanSpace ℝ (Fin n) → ℝ} (hg : ∀ x ∈ C, Filter.Tendsto (fun (i : ℕ) => f i x) Filter.atTop (nhds (g x))) (hfconv : ∀ (i : ℕ), ConvexOn ℝ C (f i)) : ConvexOn ℝ C g

If convex functions converge pointwise on a convex set, the pointwise limit is convex.

theorem convexOn_seq_exists_convex_limit_of_tendstoOn_dense {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : ℕ → EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ∀ (i : ℕ), ConvexOn ℝ C (f i)) {C' : Set (EuclideanSpace ℝ (Fin n))} (hC'sub : C' ⊆ C) (hCclosure : C ⊆ closure C') (hpoint : ∀ x ∈ C', ∃ (l : ℝ), Filter.Tendsto (fun (i : ℕ) => f i x) Filter.atTop (nhds l)) : ∃ (f_lim : EuclideanSpace ℝ (Fin n) → ℝ), (∀ x ∈ C, Filter.Tendsto (fun (i : ℕ) => f i x) Filter.atTop (nhds (f_lim x))) ∧ ConvexOn ℝ C f_lim ∧ ∀ (S : Set (EuclideanSpace ℝ (Fin n))), IsClosed S → Bornology.IsBounded S → S ⊆ C → ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ i ≥ N, ∀ x ∈ S, ‖f i x - f_lim x‖ < ε

Theorem 10.8. Let C be a relatively open convex set, and let f 0, f 1, … be a sequence of finite convex functions on C. Suppose that there exists C' ⊆ C with closure C' ⊇ C such that for each x ∈ C' the limit lim_{i → ∞} f i x exists (as a finite real number). Then the limit exists for every x ∈ C, the resulting pointwise limit function f is finite and convex on C, and the sequence f 0, f 1, … converges to f uniformly on each closed bounded subset of C.

theorem Section10.convexOn_max {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} {f g : EuclideanSpace ℝ (Fin n) → ℝ} (hf : ConvexOn ℝ C f) (hg : ConvexOn ℝ C g) : ConvexOn ℝ C fun (x : EuclideanSpace ℝ (Fin n)) => max (f x) (g x)

The pointwise maximum of two convex functions is convex.

theorem Section10.tendsto_max_of_limsup_le {u : ℕ → ℝ} {a : ℝ} (h : Filter.limsup (fun (i : ℕ) => ↑(u i)) Filter.atTop ≤ ↑a) : Filter.Tendsto (fun (i : ℕ) => max (u i) a) Filter.atTop (nhds a)

If limsup (u i) ≤ a, then max (u i) a tends to a.

theorem Section10.le_add_of_uniform_norm_sub_lt_of_le {X : Type u_1} {g : ℕ → X → ℝ} {f : X → ℝ} {S : Set X} {ε : ℝ} {N : ℕ} (hU : ∀ i ≥ N, ∀ x ∈ S, ‖g i x - f x‖ < ε) (hle : ∀ (i : ℕ) (x : X), f x ≤ g i x) (i : ℕ) : i ≥ N → ∀ x ∈ S, g i x ≤ f x + ε

If g is uniformly within ε of f on S, and f ≤ g, then g ≤ f + ε on S.

theorem convexOn_eventually_le_add_of_limsup_le {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) {f : EuclideanSpace ℝ (Fin n) → ℝ} (hfconv : ConvexOn ℝ C f) (fseq : ℕ → EuclideanSpace ℝ (Fin n) → ℝ) (hfseqconv : ∀ (i : ℕ), ConvexOn ℝ C (fseq i)) (hlimsup : ∀ x ∈ C, Filter.limsup (fun (i : ℕ) => ↑(fseq i x)) Filter.atTop ≤ ↑(f x)) (S : Set (EuclideanSpace ℝ (Fin n))) : IsClosed S → Bornology.IsBounded S → S ⊆ C → ∀ (ε : ℝ), 0 < ε → ∃ (i0 : ℕ), ∀ i ≥ i0, ∀ x ∈ S, fseq i x ≤ f x + ε

Corollary 10.8.1. Let f be a finite convex function on a relatively open convex set C. Let f₁, f₂, … be a sequence of finite convex functions on C such that limsup_{i → ∞} fᵢ(x) ≤ f(x) for all x ∈ C. Then for each closed bounded subset S of C and each ε > 0, there exists i₀ such that fᵢ(x) ≤ f(x) + ε for all i ≥ i₀ and all x ∈ S.

theorem Section10.exists_countable_subset_closure_superset {n : ℕ} (C' : Set (EuclideanSpace ℝ (Fin n))) : ∃ C'' ⊆ C', C''.Countable ∧ C' ⊆ closure C''

Any subset of a separable space contains a countable subset with closure containing the set.

theorem Section10.exists_strictMono_subseq_pointwise_tendsto_on_countable_range {α : Type u_1} (x : ℕ → α) (f : ℕ → α → ℝ) (hbounded : ∀ (j : ℕ), Bornology.IsBounded (Set.range fun (i : ℕ) => f i (x j))) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (j : ℕ), ∃ (l : ℝ), Filter.Tendsto (fun (i : ℕ) => f (φ i) (x j)) Filter.atTop (nhds l)

A diagonal compactness argument: if each coordinate sequence i ↦ f i (x j) is bounded in ℝ, then some subsequence converges at every point in the countable range {x j}.

theorem Section10.pointwise_tendsto_on_countable_subset_from_range {α : Type u_1} {f : ℕ → α → ℝ} {x : ℕ → α} {φ : ℕ → ℕ} (hpoint : ∀ (j : ℕ), ∃ (l : ℝ), Filter.Tendsto (fun (i : ℕ) => f (φ i) (x j)) Filter.atTop (nhds l)) (z : α) : z ∈ Set.range x → ∃ (l : ℝ), Filter.Tendsto (fun (i : ℕ) => f (φ i) z) Filter.atTop (nhds l)

Turn convergence along an enumeration x : ℕ → α into convergence on Set.range x.

theorem convexOn_seq_exists_subseq_uniformlyConvergentOn_of_boundedOn_dense {n : ℕ} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : ℕ → EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ∀ (i : ℕ), ConvexOn ℝ C (f i)) (hbounded : ∃ C' ⊆ C, C ⊆ closure C' ∧ ∀ x ∈ C', Bornology.IsBounded (Set.range fun (i : ℕ) => f i x)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (f_lim : EuclideanSpace ℝ (Fin n) → ℝ), ConvexOn ℝ C f_lim ∧ ∀ (S : Set (EuclideanSpace ℝ (Fin n))), IsClosed S → Bornology.IsBounded S → S ⊆ C → ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ i ≥ N, ∀ x ∈ S, ‖f (φ i) x - f_lim x‖ < ε

Theorem 10.9. Let C be a relatively open convex set, and let f₁, f₂, … be a sequence of finite convex functions on C. Suppose that for each x ∈ C the real sequence f₁ x, f₂ x, … is bounded (or merely for each x in some dense subset C' of C). Then there exists a subsequence of f₁, f₂, … which converges uniformly on each closed bounded subset of C to a finite convex function f.