theorem epigraph_subset_convexHull_union {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) (i : ι) : epigraph Set.univ (f i) ⊆ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i))

Each epigraph sits inside the convex hull of the union of epigraphs.

theorem convexHull_union_subset_epigraph_of_le {n : ℕ} {ι : Sort u_1} {f : ι → (Fin n → ℝ) → EReal} {h : (Fin n → ℝ) → EReal} (hh : ConvexFunctionOn Set.univ h) (h_le_f : ∀ (i : ι), h ≤ f i) : (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i)) ⊆ epigraph Set.univ h

If a convex function lies below each member, then the convex hull of the union of their epigraphs lies in its epigraph.

theorem sInf_coe_image_eq_sInf_real {A : Set ℝ} (hne : A.Nonempty) (hbdd : BddBelow A) : sInf ((fun (μ : ℝ) => ↑μ) '' A) = ↑(sInf A)

The EReal infimum of a coerced real set matches the coerced real infimum under nonemptiness and bounded-below hypotheses.

theorem mem_convexHull_union_epigraph_iff_fin_combo {n : ℕ} {ι : Sort u_1} {f : ι → (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} : (x, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i)) ↔ ∃ (m : ℕ) (idx : Fin m → ι) (lam : Fin m → ℝ) (x' : Fin m → Fin n → ℝ) (μ' : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ ∑ i : Fin m, lam i • x' i = x ∧ ∑ i : Fin m, lam i * μ' i = μ ∧ ∀ (i : Fin m), f (idx i) (x' i) ≤ ↑(μ' i)

Membership in the convex hull of a union of epigraphs gives a finite convex combination of epigraph points with explicit indices.

theorem exists_point_ne_top_of_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} (hproper : ProperConvexFunctionOn Set.univ f) : ∃ (x : Fin n → ℝ), f x ≠ ⊤

From properness, there exists a point where the value is not ⊤.

theorem merge_epigraph_combo_finset {n : ℕ} {ι : Type u_1} {f : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) {m : ℕ} {idx : Fin m → ι} {lam : Fin m → ℝ} {x' : Fin m → Fin n → ℝ} {μ' : Fin m → ℝ} {x : Fin n → ℝ} {μ : ℝ} (h0 : ∀ (i : Fin m), 0 ≤ lam i) (hsum1 : ∑ i : Fin m, lam i = 1) (hsumx : ∑ i : Fin m, lam i • x' i = x) (hsumμ : ∑ i : Fin m, lam i * μ' i = μ) (hle : ∀ (i : Fin m), f (idx i) (x' i) ≤ ↑(μ' i)) : ∃ (s : Finset ι) (lam' : ι → ℝ) (x'' : ι → Fin n → ℝ) (μ'' : ι → ℝ), (∀ (i : ι), 0 ≤ lam' i) ∧ (∀ i ∉ s, lam' i = 0) ∧ ∑ i ∈ s, lam' i = 1 ∧ ∑ i ∈ s, lam' i • x'' i = x ∧ ∑ i ∈ s, lam' i * μ'' i = μ ∧ ∀ (i : ι), f i (x'' i) ≤ ↑(μ'' i)

Merge a finite convex combination indexed by Fin m into a Finset-indexed form.

theorem mem_convexHull_union_epigraph_of_finset_combo {n : ℕ} {ι : Type u_1} {f : ι → (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {s : Finset ι} {lam : ι → ℝ} {x' : ι → Fin n → ℝ} {μ' : ι → ℝ} (h0 : ∀ (i : ι), 0 ≤ lam i) (hsum1 : ∑ i ∈ s, lam i = 1) (hsumx : ∑ i ∈ s, lam i • x' i = x) (hle : ∀ (i : ι), f i (x' i) ≤ ↑(μ' i)) : (x, ∑ i ∈ s, lam i * μ' i) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i))

Finset-indexed convex combinations give points in the convex hull of the union of epigraphs.

theorem convexHullFunctionFamily_eq_inf_section_ereal {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) : convexHullFunctionFamily f = fun (x : Fin n → ℝ) => sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i))})

The convex-hull function family is the EReal inf-section for the convex hull of the union of epigraphs.

theorem convexHullFunctionFamily_greatest_convex_minorant_of_nonempty_bddBelow {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) : have g := convexHullFunctionFamily f; ConvexFunctionOn Set.univ g ∧ (∀ (i : ι), g ≤ f i) ∧ ∀ (h : (Fin n → ℝ) → EReal), ConvexFunctionOn Set.univ h → (∀ (i : ι), h ≤ f i) → h ≤ g

The convex-hull function family is the greatest convex minorant.

theorem fiber_nonempty_convexHull_union_of_exists_ne_top {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) {x : Fin n → ℝ} (h : ∃ (i : ι), f i x ≠ ⊤) : {μ : ℝ | (x, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i))}.Nonempty

If some member of the family is finite at x, then the fiber over x in the convex hull of the union of epigraphs is nonempty.

theorem fiber_nonempty_convexHull_union_or_all_top {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) (x : Fin n → ℝ) : {μ : ℝ | (x, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i))}.Nonempty ∨ ∀ (i : ι), f i x = ⊤

For each x, either some f i x is finite (yielding a nonempty fiber), or all values are ⊤.

theorem not_bddBelow_fiber_convexHull_union_of_exists_bot {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) {x : Fin n → ℝ} (h : ∃ (i : ι), f i x = ⊥) : ¬BddBelow {μ : ℝ | (x, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i))}

If some member takes the value ⊥ at x, then the fiber is unbounded below.

theorem convexHullFunctionFamily_greatest_convex_minorant {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) : have g := convexHullFunctionFamily f; ConvexFunctionOn Set.univ g ∧ (∀ (i : ι), g ≤ f i) ∧ ∀ (h : (Fin n → ℝ) → EReal), ConvexFunctionOn Set.univ h → (∀ (i : ι), h ≤ f i) → h ≤ g

Text 5.5.6: conv { f_i | i ∈ I } is the greatest convex function f (not necessarily proper) on R^n such that f(x) ≤ f_i(x) for every x ∈ R^n and every i ∈ I.

theorem convexHullFunctionFamily_eq_sInf_convexCombination {n : ℕ} {ι : Type u_1} {f : ι → (Fin n → ℝ) → EReal} (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) (x : Fin n → ℝ) : convexHullFunctionFamily f x = sInf {z : EReal | ∃ (s : Finset ι) (lam : ι → ℝ) (x' : ι → Fin n → ℝ), (∀ (i : ι), 0 ≤ lam i) ∧ (∀ i ∉ s, lam i = 0) ∧ ∑ i ∈ s, lam i = 1 ∧ ∑ i ∈ s, lam i • x' i = x ∧ z = ∑ i ∈ s, ↑(lam i) * f i (x' i)}

Theorem 5.6: Let {f_i | i ∈ I} be a collection of proper convex functions on R^n, and let f be the convex hull of the collection. Then f(x) = inf { ∑_{i∈I} λ_i f_i(x_i) | ∑_{i∈I} λ_i x_i = x }, where the infimum is taken over all representations of x as a convex combination of points x_i with only finitely many nonzero coefficients λ_i. (The formula is also valid if one restricts x_i to lie in dom f_i.)

theorem indicator_add_const_at_point {n : ℕ} (a : Fin n → ℝ) (c : ℝ) : indicatorFunction {a} a + ↑c = ↑c

The singleton indicator plus a constant equals the constant at the point.

theorem le_indicator_add_const_of_le_at {n : ℕ} {h : (Fin n → ℝ) → EReal} (a : Fin n → ℝ) (c : ℝ) (ha : h a ≤ ↑c) : h ≤ fun (x : Fin n → ℝ) => indicatorFunction {a} x + ↑c

A bound at a implies a global bound by the singleton indicator plus a constant.

theorem properConvexFunctionOn_indicator_add_const_singleton {n : ℕ} (a : Fin n → ℝ) (c : ℝ) : ProperConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => indicatorFunction {a} x + ↑c

The singleton indicator plus a constant is a proper convex function on Set.univ.

theorem sum_eq_top_of_term_top {ι : Type u_1} (s : Finset ι) (f : ι → EReal) {i : ι} (hi : i ∈ s) (htop : f i = ⊤) (hbot : ∀ j ∈ s, f j ≠ ⊥) : s.sum f = ⊤

A finite sum is ⊤ if one term is ⊤ and all terms are not ⊥.