theorem ri_effectiveDomain_sum_eq_iInter {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : have e := EuclideanSpace.equiv (Fin n) ℝ; have fSum := fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x; (⋂ (i : Fin m), euclideanRelativeInterior n (⇑e.symm '' effectiveDomain Set.univ (f i))).Nonempty → euclideanRelativeInterior n (⇑e.symm '' effectiveDomain Set.univ fSum) = ⋂ (i : Fin m), euclideanRelativeInterior n (⇑e.symm '' effectiveDomain Set.univ (f i))

The relative interior of the effective domain of a finite sum is the intersection of the relative interiors.

theorem closedConvexFunction_sum_of_closed {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hclosed : ∀ (i : Fin m), ClosedConvexFunction (f i)) (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : ClosedConvexFunction fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x

A finite sum of closed proper convex functions is closed.

theorem properConvexFunctionOn_sum_of_exists_ne_top {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hexists : ∃ (x : Fin n → ℝ), ∑ i : Fin m, f i x ≠ ⊤) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x

A finite sum of proper convex functions is proper if it is finite somewhere.

theorem convexFunctionClosure_sum_eq_sum_closure {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : have e := EuclideanSpace.equiv (Fin n) ℝ; have fSum := fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x; (∃ (x : EuclideanSpace ℝ (Fin n)), ∀ (i : Fin m), x ∈ euclideanRelativeInterior n (⇑e.symm '' effectiveDomain Set.univ (f i))) → convexFunctionClosure fSum = fun (x : Fin n → ℝ) => ∑ i : Fin m, convexFunctionClosure (f i) x

Under a common relative-interior point, the closure of a finite sum is the sum of closures.

theorem sum_closed_proper_convex_recession_and_closure {n m : ℕ} {f f0_plus : Fin m → (Fin n → ℝ) → EReal} (hproper : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : have e := EuclideanSpace.equiv (Fin n) ℝ; have fSum := fun (x : Fin n → ℝ) => ∑ i : Fin m, f i x; have fSum0_plus := fun (y : Fin n → ℝ) => ∑ i : Fin m, f0_plus i y; ((∀ (i : Fin m), ClosedConvexFunction (f i)) → (∃ (x : Fin n → ℝ), fSum x ≠ ⊤) → ClosedConvexFunction fSum ∧ ProperConvexFunctionOn Set.univ fSum ∧ fSum0_plus = fun (y : Fin n → ℝ) => ∑ i : Fin m, f0_plus i y) ∧ ((∃ (x : EuclideanSpace ℝ (Fin n)), ∀ (i : Fin m), x ∈ euclideanRelativeInterior n (⇑e.symm '' effectiveDomain Set.univ (f i))) → convexFunctionClosure fSum = fun (x : Fin n → ℝ) => ∑ i : Fin m, convexFunctionClosure (f i) x)

Theorem 9.3. Let f₁, …, fₘ be proper convex functions on ℝ^n. If every f_i is closed and f₁ + ··· + fₘ is not identically +∞, then the sum is a closed proper convex function and (f₁ + ··· + fₘ)0^+ = f₁ 0^+ + ··· + fₘ 0^+. If the f_i are not all closed, but there exists a point common to every ri (dom f_i), then cl (f₁ + ··· + fₘ) = cl f₁ + ··· + cl fₘ.

theorem closedConvexFunction_iSup_of_closed {n : ℕ} {I : Type u_1} {f : I → (Fin n → ℝ) → EReal} (hclosed : ∀ (i : I), ClosedConvexFunction (f i)) : ClosedConvexFunction fun (x : Fin n → ℝ) => ⨆ (i : I), f i x

The pointwise supremum of closed convex functions is closed.

theorem properConvexFunctionOn_iSup_of_exists {n : ℕ} {I : Type u_1} {f : I → (Fin n → ℝ) → EReal} (hproper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) : have fSup := fun (x : Fin n → ℝ) => ⨆ (i : I), f i x; (∃ (x : Fin n → ℝ), fSup x ≠ ⊤ ∧ fSup x ≠ ⊥) → ProperConvexFunctionOn Set.univ fSup

A pointwise supremum of proper convex functions is proper if it is finite somewhere.

theorem mem_iInter_riEpigraph_of_common_ri_dom {n : ℕ} {I : Type u_1} {f : I → (Fin n → ℝ) → EReal} (hconv : ∀ (i : I), ConvexFunction (f i)) : have e := EuclideanSpace.equiv (Fin n) ℝ; have fSup := fun (x : Fin n → ℝ) => ⨆ (i : I), f i x; ∀ {x0 : EuclideanSpace ℝ (Fin n)}, (∀ (i : I), x0 ∈ euclideanRelativeInterior n (⇑e.symm '' effectiveDomain Set.univ (f i))) → fSup (e.symm x0.ofLp).ofLp ≠ ⊤ → fSup (e.symm x0.ofLp).ofLp ≠ ⊥ → (appendAffineEquiv n 1) ((EuclideanSpace.equiv (Fin n) ℝ).symm ((EuclideanSpace.equiv (Fin n) ℝ) x0), (EuclideanSpace.equiv (Fin 1) ℝ).symm fun (x : Fin 1) => (fSup (e.symm x0.ofLp).ofLp).toReal + 1) ∈ ⋂ (i : I), riEpigraph (f i)

A common relative-interior point yields a point in all ri (epi f i) above the supremum.

theorem iSup_closed_proper_convex_recession_and_closure {n : ℕ} {I : Type u_1} {f f0_plus : I → (Fin n → ℝ) → EReal} (hproper : ∀ (i : I), ProperConvexFunctionOn Set.univ (f i)) : have e := EuclideanSpace.equiv (Fin n) ℝ; have fSup := fun (x : Fin n → ℝ) => ⨆ (i : I), f i x; have fSup0_plus := fun (y : Fin n → ℝ) => ⨆ (i : I), f0_plus i y; ((∀ (i : I), ClosedConvexFunction (f i)) → (∃ (x : Fin n → ℝ), fSup x ≠ ⊤ ∧ fSup x ≠ ⊥) → ClosedConvexFunction fSup ∧ ProperConvexFunctionOn Set.univ fSup ∧ fSup0_plus = fun (y : Fin n → ℝ) => ⨆ (i : I), f0_plus i y) ∧ ((∃ (x : EuclideanSpace ℝ (Fin n)), (∀ (i : I), x ∈ euclideanRelativeInterior n (⇑e.symm '' effectiveDomain Set.univ (f i))) ∧ fSup (e.symm x.ofLp).ofLp ≠ ⊤ ∧ fSup (e.symm x.ofLp).ofLp ≠ ⊥) → convexFunctionClosure fSup = fun (x : Fin n → ℝ) => ⨆ (i : I), convexFunctionClosure (f i) x)

Theorem 9.4. Let f_i be a proper convex function on ℝ^n for i ∈ I, and let f = sup { f_i | i ∈ I }. If f is finite somewhere and every f_i is closed, then f is closed and proper and f0^+ = sup { f_i0^+ | i ∈ I }. If the f_i are not all closed, but there exists a point common to every ri (dom f_i) such that f is finite there, then cl f = sup { cl f_i | i ∈ I }.