theorem convexOn_exists_unique_continuousExtension_of_locallySimplicial {n : ℕ} {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hCloc : Set.LocallySimplicial n C) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ConvexOn ℝ (euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C)) f) (hf_bddAbove : ∀ s ⊆ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C), Bornology.IsBounded s → BddAbove (f '' s)) : ∃ (g : EuclideanSpace ℝ (Fin n) → ℝ), (ConvexOn ℝ ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C) g ∧ Function.ContinuousRelativeTo g ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C) ∧ ∀ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C), g x = f x) ∧ ∀ (g' : EuclideanSpace ℝ (Fin n) → ℝ), (ConvexOn ℝ ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C) g' ∧ Function.ContinuousRelativeTo g' ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C) ∧ ∀ x ∈ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C), g' x = f x) → ∀ x ∈ (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C, g' x = g x

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 in one and only one way to a continuous finite convex function on the whole of C.

theorem Section10.bddAbove_image_of_monotoneOn_of_isBounded_posOrthant {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hfmono : MonotoneOn f {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}) {s : Set (Fin n → ℝ)} (hs : s ⊆ {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}) (hsbdd : Bornology.IsBounded s) : BddAbove (f '' s)

Boundedness above on bounded subsets of the positive orthant, from coordinatewise monotonicity.

theorem Section10.euclideanRelativeInterior_preimage_nonnegOrthant {n : ℕ} : have C := {y : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ y i}; have CE := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C; euclideanRelativeInterior n CE = {x : EuclideanSpace ℝ (Fin n) | ∀ (i : Fin n), 0 < x.ofLp i}

The relative interior of the nonnegative orthant in EuclideanSpace is the positive orthant.

theorem Section10.linearIndependent_piSingle {n : ℕ} {M : ℝ} (hM : M ≠ 0) : LinearIndependent ℝ fun (i : Fin n) => Pi.single i M

The coordinate singleton vectors Pi.single i M are linearly independent when M ≠ 0.

theorem Section10.affineIndependent_zero_piSingle {n : ℕ} {M : ℝ} (hM : M ≠ 0) : have b := fun (i : Fin (n + 1)) => Fin.cases (motive := fun (x : Fin (n + 1)) => Fin n → ℝ) 0 (fun (i : Fin n) => Pi.single i M) i; AffineIndependent ℝ b

The family of vertices {0} ∪ {Pi.single i M} is affinely independent when M ≠ 0.

theorem Section10.isSimplex_convexHull_zero_piSingle {n : ℕ} {M : ℝ} (hM : M ≠ 0) : have b := fun (i : Fin (n + 1)) => Fin.cases (motive := fun (x : Fin (n + 1)) => Fin n → ℝ) 0 (fun (i : Fin n) => Pi.single i M) i; IsSimplex n n ((convexHull ℝ) (Set.range b))

The convex hull of {0} ∪ {Pi.single i M} is an n-simplex when M ≠ 0.

theorem Section10.mem_convexHull_zero_piSingle_of_nonneg_sum_le {n : ℕ} {M : ℝ} (hM : 0 < M) (y : Fin n → ℝ) (hy0 : ∀ (i : Fin n), 0 ≤ y i) (hysum : ∑ i : Fin n, y i ≤ M) : have b := fun (i : Fin (n + 1)) => Fin.cases (motive := fun (x : Fin (n + 1)) => Fin n → ℝ) 0 (fun (i : Fin n) => Pi.single i M) i; y ∈ (convexHull ℝ) (Set.range b)

A nonnegative vector with sum bounded by M lies in the simplex convexHull {0, M e_i}.

theorem Section10.locallySimplicial_nonnegOrthant {n : ℕ} : Set.LocallySimplicial n {y : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ y i}

The nonnegative orthant is locally simplicial.

theorem convexOn_bddAbove_and_exists_unique_extension_nonnegOrthant_of_monotoneOn {n : ℕ} (f : (Fin n → ℝ) → ℝ) (hfconv : ConvexOn ℝ {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i} f) (hfmono : MonotoneOn f {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}) : (∀ s ⊆ {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}, Bornology.IsBounded s → BddAbove (f '' s)) ∧ ∃ (g : (Fin n → ℝ) → ℝ), (ConvexOn ℝ {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i} g ∧ ContinuousOn g {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i} ∧ ∀ x ∈ {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}, g x = f x) ∧ ∀ (g' : (Fin n → ℝ) → ℝ), (ConvexOn ℝ {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i} g' ∧ ContinuousOn g' {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i} ∧ ∀ x ∈ {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}, g' x = f x) → ∀ x ∈ {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i}, g' x = g x

Theorem 10.3.1. Let C ⊆ ℝ^n be the nonnegative orthant, C = {x = (ξ₁, …, ξₙ) | ξⱼ ≥ 0, j = 1, …, n}. Assume f is a finite convex function on the positive orthant int C and is non-decreasing in each coordinate.

Then f is bounded above on every bounded subset of the positive orthant, and hence f admits a unique extension to a finite continuous convex function on the whole nonnegative orthant C.

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

Definition 10.3.2. Let S ⊆ ℝ^n. A real-valued function f defined on S is called Lipschitzian relative to S if there exists a real number α ≥ 0 such that |f(y) - f(x)| ≤ α |y - x| for all x ∈ S and y ∈ S.

Equations

• Function.LipschitzRelativeTo f S = ∃ (K : NNReal), LipschitzOnWith K f S

theorem Function.LipschitzRelativeTo.uniformContinuousOn {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {S : Set (EuclideanSpace ℝ (Fin n))} (hf : LipschitzRelativeTo f S) : UniformContinuousOn f S

A function that is Lipschitz on a set is uniformly continuous on that set.

theorem Function.uniformContinuousOn_of_lipschitzRelativeTo {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → ℝ} {S : Set (EuclideanSpace ℝ (Fin n))} (hf : LipschitzRelativeTo f S) : UniformContinuousOn f S

Theorem 10.3.3. Let S ⊆ ℝ^n. If a real-valued function f is Lipschitzian relative to S, then f is uniformly continuous relative to S.

theorem Section10.exists_pos_eps_uniform_ball_subset_ri {n : ℕ} {C S : Set (EuclideanSpace ℝ (Fin n))} (hS : IsCompact S) (hSsubset : S ⊆ euclideanRelativeInterior n C) : ∃ (ε : ℝ), 0 < ε ∧ ∀ x ∈ S, (fun (u : EuclideanSpace ℝ (Fin n)) => x + u) '' (ε • euclideanUnitBall n) ∩ ↑(affineSpan ℝ C) ⊆ euclideanRelativeInterior n C

A compact set included in the relative interior admits a uniform radius whose translated scaled unit ball (intersected with the affine span) stays in the relative interior.