def Function.UniformlyEquicontinuousRelativeTo {n : ℕ} {I : Type u_1} (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (S : Set (EuclideanSpace ℝ (Fin n))) : Prop

Definition 10.5.4. Let S ⊆ ℝ^n and let {f i | i ∈ I} be a family of real-valued functions defined on S. The family is uniformly equicontinuous relative to S if for every ε > 0 there exists δ > 0 such that for all x ∈ S, y ∈ S, and all indices i, if ‖y - x‖ ≤ δ then |f i y - f i x| ≤ ε.

Equations

• Function.UniformlyEquicontinuousRelativeTo f S = UniformEquicontinuousOn f S

theorem Function.uniformlyEquicontinuousRelativeTo_of_equiLipschitzRelativeTo {n : ℕ} {I : Type u_1} {f : I → EuclideanSpace ℝ (Fin n) → ℝ} {S : Set (EuclideanSpace ℝ (Fin n))} (hf : EquiLipschitzRelativeTo f S) : UniformlyEquicontinuousRelativeTo f S

Theorem 10.5.5. Let S ⊆ ℝ^n and let {f i | i ∈ I} be a collection of real-valued functions on S. If the family is equi-Lipschitzian relative to S, then it is uniformly equicontinuous relative to S.

def Function.PointwiseBoundedOn {n : ℕ} {I : Type u_1} (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (S : Set (EuclideanSpace ℝ (Fin n))) : Prop

Definition 10.5.6. Let S ⊆ ℝ^n and let {f i | i ∈ I} be a collection of real-valued functions on S. The collection {f i | i ∈ I} is pointwise bounded on S if for each x ∈ S the set of real numbers {f i x | i ∈ I} is bounded.

Equations

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

def Function.UniformlyBoundedOn {n : ℕ} {I : Type u_1} (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (S : Set (EuclideanSpace ℝ (Fin n))) : Prop

Definition 10.5.7. Let S ⊆ ℝ^n and let {f i | i ∈ I} be a collection of real-valued functions on S. The collection {f i | i ∈ I} is uniformly bounded on S if there exist real numbers α₁ and α₂ such that α₁ ≤ f i x ≤ α₂ for all x ∈ S and all indices i.

Equations

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

theorem Section10.isCompact_of_isClosed_isBounded {n : ℕ} {S : Set (EuclideanSpace ℝ (Fin n))} (hSclosed : IsClosed S) (hSbdd : Bornology.IsBounded S) : IsCompact S

A closed and bounded subset of ℝ^n is compact.

theorem Section10.exists_abs_le_of_uniformlyBoundedOn {n : ℕ} {I : Type u_1} {f : I → EuclideanSpace ℝ (Fin n) → ℝ} {S : Set (EuclideanSpace ℝ (Fin n))} (h : Function.UniformlyBoundedOn f S) : ∃ (M : ℝ), ∀ (i : I), ∀ x ∈ S, |f i x| ≤ M

A uniform two-sided bound implies a uniform absolute bound.

theorem Section10.uniformlyBoundedOn_and_equiLipschitzRelativeTo_of_abs_le_cthickening {n : ℕ} {I : Type u_1} {C S : Set (EuclideanSpace ℝ (Fin n))} {f : I → EuclideanSpace ℝ (Fin n) → ℝ} (hfconv : ∀ (i : I), ConvexOn ℝ C (f i)) {δ M : ℝ} (hδ : 0 < δ) (hcthick : Metric.cthickening δ S ⊆ C) (hM : ∀ (i : I), ∀ x ∈ Metric.cthickening δ S, |f i x| ≤ M) : Function.UniformlyBoundedOn f S ∧ Function.EquiLipschitzRelativeTo f S

If all functions in a convex family are uniformly bounded by M on a closed thickening of S contained in C, then the family is uniformly bounded on S and equi-Lipschitzian relative to S.

theorem Section10.interior_closure_subset_of_convex {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) (hS : Convex ℝ S) : interior (closure S) ⊆ S

For a convex set S in ℝ^n, taking the closure does not create new interior points: interior (closure S) ⊆ S.

theorem Section10.exists_uniform_upper_bound_on_compact_of_exists_subset {n : ℕ} {I : Type u_1} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ∀ (i : I), ConvexOn ℝ C (f i)) {C' : Set (EuclideanSpace ℝ (Fin n))} (hC'sub : C' ⊆ C) (hC'hull : C ⊆ (convexHull ℝ) (closure C')) (hC'bdAbove : ∀ x ∈ C', BddAbove (Set.range fun (i : I) => f i x)) {K : Set (EuclideanSpace ℝ (Fin n))} (hKcomp : IsCompact K) (hKsubset : K ⊆ C) : ∃ (M : ℝ), ∀ (i : I), ∀ x ∈ K, f i x ≤ M

Under hypothesis (a) from Theorem 10.6, the family is uniformly bounded above on any compact subset K ⊆ C.

theorem Section10.exists_uniform_lower_bound_on_compact_of_point_bddBelow {n : ℕ} {I : Type u_1} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ∀ (i : I), ConvexOn ℝ C (f i)) (hexists_bddBelow : ∃ x₀ ∈ C, BddBelow (Set.range fun (i : I) => f i x₀)) (hUpper : ∀ {K : Set (EuclideanSpace ℝ (Fin n))}, IsCompact K → K ⊆ C → ∃ (M : ℝ), ∀ (i : I), ∀ x ∈ K, f i x ≤ M) {K : Set (EuclideanSpace ℝ (Fin n))} (hKcomp : IsCompact K) (hKsubset : K ⊆ C) : ∃ (m : ℝ), ∀ (i : I), ∀ x ∈ K, m ≤ f i x

Under hypothesis (b) from Theorem 10.6 and the uniform upper bound on a compact neighborhood of x₀, the family is uniformly bounded below on any compact subset K ⊆ C.

theorem Section10.uniformlyBoundedOn_on_compact_of_exists_subset {n : ℕ} {I : Type u_1} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ∀ (i : I), ConvexOn ℝ C (f i)) {C' : Set (EuclideanSpace ℝ (Fin n))} (hC'sub : C' ⊆ C) (hC'hull : C ⊆ (convexHull ℝ) (closure C')) (hC'bdAbove : ∀ x ∈ C', BddAbove (Set.range fun (i : I) => f i x)) (hexists_bddBelow : ∃ x ∈ C, BddBelow (Set.range fun (i : I) => f i x)) {K : Set (EuclideanSpace ℝ (Fin n))} (hKcomp : IsCompact K) (hKsubset : K ⊆ C) : Function.UniformlyBoundedOn f K

Under hypotheses (a) and (b) from Theorem 10.6, the family is uniformly bounded on any compact subset K ⊆ C.

theorem Section10.convexOn_family_uniformlyBoundedOn_and_equiLipschitzRelativeTo_of_exists_subset_aux {n : ℕ} {I : Type u_1} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ∀ (i : I), ConvexOn ℝ C (f i)) {C' : Set (EuclideanSpace ℝ (Fin n))} (hC'sub : C' ⊆ C) (hC'hull : C ⊆ (convexHull ℝ) (closure C')) (hC'bdAbove : ∀ x ∈ C', BddAbove (Set.range fun (i : I) => f i x)) (hexists_bddBelow : ∃ x ∈ C, BddBelow (Set.range fun (i : I) => f i x)) {S : Set (EuclideanSpace ℝ (Fin n))} (hSclosed : IsClosed S) (hSbdd : Bornology.IsBounded S) (hSsubset : S ⊆ C) : Function.UniformlyBoundedOn f S ∧ Function.EquiLipschitzRelativeTo f S

Theorem 10.6 (variant, auxiliary proof): reduce uniform boundedness + equi-Lipschitz to uniform boundedness on a compact thickening of S.

theorem convexOn_family_uniformlyBoundedOn_and_equiLipschitzRelativeTo_of_pointwiseBoundedOn {n : ℕ} {I : Type u_1} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ∀ (i : I), ConvexOn ℝ C (f i)) (hfpt : Function.PointwiseBoundedOn f C) {S : Set (EuclideanSpace ℝ (Fin n))} (hSclosed : IsClosed S) (hSbdd : Bornology.IsBounded S) (hSsubset : S ⊆ C) : Function.UniformlyBoundedOn f S ∧ Function.EquiLipschitzRelativeTo 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 | i ∈ I} is uniformly bounded on S and equi-Lipschitzian relative to S.

The conclusion remains valid if the pointwise boundedness assumption is weakened to the following pair of assumptions:

(a) There exists a subset C' of C such that conv (cl C') ⊇ C and sup {f i x | i ∈ I} is finite for every x ∈ C';

(b) There exists at least one x ∈ C such that inf {f i x | i ∈ I} is finite.

theorem convexOn_family_uniformlyBoundedOn_and_equiLipschitzRelativeTo_of_exists_subset {n : ℕ} {I : Type u_1} {C : Set (EuclideanSpace ℝ (Fin n))} (hCopen : IsOpen C) (hCconv : Convex ℝ C) (f : I → EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ∀ (i : I), ConvexOn ℝ C (f i)) {C' : Set (EuclideanSpace ℝ (Fin n))} (hC'sub : C' ⊆ C) (hC'hull : C ⊆ (convexHull ℝ) (closure C')) (hC'bdAbove : ∀ x ∈ C', BddAbove (Set.range fun (i : I) => f i x)) (hexists_bddBelow : ∃ x ∈ C, BddBelow (Set.range fun (i : I) => f i x)) {S : Set (EuclideanSpace ℝ (Fin n))} (hSclosed : IsClosed S) (hSbdd : Bornology.IsBounded S) (hSsubset : S ⊆ C) : Function.UniformlyBoundedOn f S ∧ Function.EquiLipschitzRelativeTo f S

Theorem 10.6 (variant). The same conclusion under the weaker assumptions (a) and (b) stated in Theorem 10.6.