theorem Section10.upperSemicontinuousWithinAt_of_isSimplex_vertex {n m : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) {b : Fin (m + 1) → Fin n → ℝ} (hb : AffineIndependent ℝ b) (hdom : (convexHull ℝ) (Set.range b) ⊆ effectiveDomain Set.univ f) (j : Fin (m + 1)) : UpperSemicontinuousWithinAt f ((convexHull ℝ) (Set.range b)) (b j)

Upper semicontinuity at a vertex of an m-simplex contained in dom f.

theorem Section10.upperSemicontinuousWithinAt_of_isSimplex {n m : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) {P : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hP : IsSimplex n m P) (hxP : x ∈ P) (hPdom : P ⊆ effectiveDomain Set.univ f) : UpperSemicontinuousWithinAt f P x

Upper semicontinuity within an m-simplex contained in dom f.

theorem convexFunctionOn_upperSemicontinuousOn_of_locallySimplicial {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) {S : Set (Fin n → ℝ)} (hS : Set.LocallySimplicial n S) (hSdom : S ⊆ effectiveDomain Set.univ f) : UpperSemicontinuousOn f S ∧ (ClosedConvexFunction f → ContinuousOn f S)

Theorem 10.2. Let f be a convex function on ℝ^n, and let S be any locally simplicial subset of dom f. Then f is upper semicontinuous relative to S, so that if f is closed, then f is continuous relative to S.

theorem Section10.properConvexFunctionOn_univ_extendTopOutside_ri {n : ℕ} {riCE : Set (EuclideanSpace ℝ (Fin n))} (hri : riCE.Nonempty) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hfconv : ConvexOn ℝ riCE f) (e : EuclideanSpace ℝ (Fin n) ≃L[ℝ] Fin n → ℝ := EuclideanSpace.equiv (Fin n) ℝ) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => if e.symm x ∈ riCE then ↑(f (e.symm x)) else ⊤

Extending a finite convex function by ⊤ outside a nonempty set yields a proper convex function on Set.univ.

theorem Section10.preimage_effectiveDomain_extendTopOutside_ri {n : ℕ} {C : Set (Fin n → ℝ)} (f : EuclideanSpace ℝ (Fin n) → ℝ) : have CE := (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' C; have riCE := euclideanRelativeInterior n CE; have e := EuclideanSpace.equiv (Fin n) ℝ; have F := fun (x : Fin n → ℝ) => if e.symm x ∈ riCE then ↑(f (e.symm x)) else ⊤; (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ F = riCE ∧ euclideanRelativeInterior n ((fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ F) = riCE

For the ⊤-extension F outside the relative interior riCE, the effective domain of F pulled back to EuclideanSpace is exactly riCE; hence its relative interior is riCE.

theorem Section10.convexFunctionClosure_ne_top_of_mem_closure_ri_of_bddAbove {n : ℕ} {riCE : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf_bddAbove : ∀ s ⊆ riCE, Bornology.IsBounded s → BddAbove (f '' s)) (e : EuclideanSpace ℝ (Fin n) ≃L[ℝ] Fin n → ℝ := EuclideanSpace.equiv (Fin n) ℝ) (y : Fin n → ℝ) (hy : e.symm y ∈ closure riCE) : convexFunctionClosure (fun (x : Fin n → ℝ) => if e.symm x ∈ riCE then ↑(f (e.symm x)) else ⊤) y ≠ ⊤

Boundedness above on bounded subsets of riCE forces the convex closure of the ⊤-extension to be finite at any point in the closure of riCE.

theorem Section10.unique_extension_on_C_of_continuous_eqOn_ri {n : ℕ} {CE riCE : Set (EuclideanSpace ℝ (Fin n))} (hri : riCE ⊆ CE) (hclosure : CE ⊆ closure riCE) {g g' : EuclideanSpace ℝ (Fin n) → ℝ} (hg : Function.ContinuousRelativeTo g CE) (hg' : Function.ContinuousRelativeTo g' CE) (hEq : ∀ x ∈ riCE, g x = g' x) (x : EuclideanSpace ℝ (Fin n)) : x ∈ CE → g x = g' x

If two functions are continuous relative to CE and agree on riCE, then they agree on CE provided riCE ⊆ CE and CE ⊆ closure riCE.