theorem convexFunctionOn_coord {n : ℕ} (j : Fin n) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(x j)

Coordinate projections are convex on ℝ^n.

theorem convexFunctionOn_maxComponent {n : ℕ} : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ⨆ (j : Fin n), ↑(x j)

Text 5.5.0.1: The function f which assigns to each x = (xi_1, ..., xi_n) the greatest of the components xi_j of x is convex.

theorem iSup_mul_of_pos {n : ℕ} (a : Fin n → EReal) {t : ℝ} (ht : 0 < t) : ⨆ (j : Fin n), ↑t * a j = ↑t * ⨆ (j : Fin n), a j

Pulling out a positive scalar from a finite supremum in EReal.

theorem maxComponent_smul_rewrite {n : ℕ} (x : Fin n → ℝ) (t : ℝ) : ⨆ (j : Fin n), ↑((t • x) j) = ⨆ (j : Fin n), ↑t * ↑(x j)

Rewrite the max-component after scaling as EReal multiplication.

theorem positivelyHomogeneous_maxComponent {n : ℕ} : PositivelyHomogeneous fun (x : Fin n → ℝ) => ⨆ (j : Fin n), ↑(x j)

Text 5.5.0.2: The function f which assigns to each x = (xi_1, ..., xi_n) the greatest of the components xi_j of x is positively homogeneous.

theorem bddAbove_components {n : ℕ} (x : Fin n → ℝ) : BddAbove {r : ℝ | ∃ (j : Fin n), r = x j}

Components of a vector form a bounded-above set.

theorem simplex_stdBasis_mem {n : ℕ} (j : Fin n) : (∀ (i : Fin n), 0 ≤ Pi.single j 1 i) ∧ ∑ i : Fin n, Pi.single j 1 i = 1

The standard basis vector lies in the simplex.

theorem dotProduct_le_sSup_components_of_simplex {n : ℕ} (x y : Fin n → ℝ) (hy0 : ∀ (j : Fin n), 0 ≤ y j) (hysum : ∑ j : Fin n, y j = 1) : x ⬝ᵥ y ≤ sSup {r : ℝ | ∃ (j : Fin n), r = x j}

A convex combination of components is bounded by their supremum.

theorem component_le_supportFunction_simplex {n : ℕ} (x : Fin n → ℝ) (j : Fin n) : x j ≤ supportFunction {y : Fin n → ℝ | (∀ (j : Fin n), 0 ≤ y j) ∧ ∑ j : Fin n, y j = 1} x

Each component is bounded by the support function of the simplex.

theorem supportFunction_simplex_eq_maxComponent {n : ℕ} : have C := {y : Fin n → ℝ | (∀ (j : Fin n), 0 ≤ y j) ∧ ∑ j : Fin n, y j = 1}; supportFunction C = fun (x : Fin n → ℝ) => sSup {r : ℝ | ∃ (j : Fin n), r = x j}

Text 5.5.0.3: The function f which assigns to each x = (xi_1, ..., xi_n) the greatest of the components xi_j of x is the support function of the simplex C = { y = (eta_1, ..., eta_n) | eta_j ≥ 0, eta_1 + ... + eta_n = 1 }.

theorem bddAbove_abs_components {n : ℕ} (x : Fin n → ℝ) : BddAbove {r : ℝ | ∃ (j : Fin n), r = |x j|}

Absolute values of components form a bounded-above set.

theorem abs_component_le_convexCombo {n : ℕ} (x y : Fin n → ℝ) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (j : Fin n) : |(a • x + b • y) j| ≤ a * |x j| + b * |y j|

Componentwise absolute value bound for convex combinations.

theorem abs_components_nonempty_succ {n : ℕ} (x : Fin n.succ → ℝ) : {r : ℝ | ∃ (j : Fin n.succ), r = |x j|}.Nonempty

The set of absolute component values is nonempty in positive dimension.

theorem dotProduct_le_sSup_abs_components_of_l1Ball {n : ℕ} (x y : Fin n → ℝ) (hy : ∑ j : Fin n, |y j| ≤ 1) : x ⬝ᵥ y ≤ sSup {r : ℝ | ∃ (j : Fin n), r = |x j|}

Dot product bound for vectors in the l1-ball.

theorem l1Ball_single_mem {n : ℕ} (j : Fin n) (s : ℝ) (hs : |s| ≤ 1) : Pi.single j s ∈ {y : Fin n → ℝ | ∑ i : Fin n, |y i| ≤ 1}

A single-coordinate vector with bounded absolute value lies in the l1-ball.

theorem abs_component_le_supportFunction_l1Ball {n : ℕ} (x : Fin n → ℝ) (j : Fin n) : |x j| ≤ supportFunction {y : Fin n → ℝ | ∑ j : Fin n, |y j| ≤ 1} x

Each absolute component is bounded by the support function of the l1-ball.

theorem convexOn_maxAbsComponent {n : ℕ} : ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => sSup {r : ℝ | ∃ (j : Fin n), r = |x j|}

Text 5.5.0.4: The function k(x) = max { |xi_j| | j = 1, ..., n } is convex in ℝ^n.

theorem supportFunction_l1Ball_eq_maxAbsComponent {n : ℕ} : have D := {y : Fin n → ℝ | ∑ j : Fin n, |y j| ≤ 1}; supportFunction D = fun (x : Fin n → ℝ) => sSup {r : ℝ | ∃ (j : Fin n), r = |x j|}

Text 5.5.0.5: The function k(x) = max { |xi_j| | j = 1, ..., n } is the support function of the convex set D = { y = (eta_1, ..., eta_n) | |eta_1| + ... + |eta_n| ≤ 1 }.

theorem cube_mem_iff_abs_le_one {n : ℕ} {x : Fin n → ℝ} : x ∈ {x : Fin n → ℝ | ∀ (j : Fin n), -1 ≤ x j ∧ x j ≤ 1} ↔ ∀ (j : Fin n), |x j| ≤ 1

Membership in the cube is equivalent to an absolute-value bound.

theorem mem_scaling_cube_of_abs_le {n : ℕ} {x : Fin n → ℝ} {t : ℝ} (ht : 0 < t) (hxt : ∀ (j : Fin n), |x j| ≤ t) : x ∈ (fun (y : Fin n → ℝ) => t • y) '' {x : Fin n → ℝ | ∀ (j : Fin n), -1 ≤ x j ∧ x j ≤ 1}

If all components of x are bounded by t > 0, then x lies in the scaled cube.

theorem abs_le_of_mem_scaling_cube {n : ℕ} {x : Fin n → ℝ} {t : ℝ} (ht : 0 ≤ t) (hx : x ∈ (fun (y : Fin n → ℝ) => t • y) '' {x : Fin n → ℝ | ∀ (j : Fin n), -1 ≤ x j ∧ x j ≤ 1}) (j : Fin n) : |x j| ≤ t

Membership in a scaled cube bounds each component in absolute value.

theorem gaugeOfCube_eq_maxAbsComponent {n : ℕ} : have E := {x : Fin n → ℝ | ∀ (j : Fin n), -1 ≤ x j ∧ x j ≤ 1}; gaugeOfConvexSet E = fun (x : Fin n → ℝ) => sSup {r : ℝ | ∃ (j : Fin n), r = |x j|}

Text 5.5.0.6: The function k(x) = max { |xi_j| | j = 1, ..., n } is the gauge of the n-dimensional cube E = { x = (xi_1, ..., xi_n) | -1 ≤ xi_j ≤ 1, j = 1, ..., n }.

noncomputable def convexHullFunction {n : ℕ} (g : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 5.5.1: For a function g, define f x = inf { μ | (x, μ) ∈ conv (epi g) }. Then f is called the convex hull of g, and is denoted f = conv(g).

Equations

• convexHullFunction g x = sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ (convexHull ℝ) (epigraph Set.univ g)})

theorem convex_convexHull_epigraph {n : ℕ} (g : (Fin n → ℝ) → EReal) : Convex ℝ ((convexHull ℝ) (epigraph Set.univ g))

The convex hull of an epigraph is convex.

theorem convexHullFunction_eq_inf_section {n : ℕ} (g : (Fin n → ℝ) → EReal) : convexHullFunction g = fun (x : Fin n → ℝ) => sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ (convexHull ℝ) (epigraph Set.univ g)})

Rewrite the convex hull function as an EReal inf-section.

theorem convexFunctionOn_convexHullFunction {n : ℕ} (g : (Fin n → ℝ) → EReal) : ConvexFunctionOn Set.univ (convexHullFunction g)

Text 5.5.2: If f = conv(g) is the convex hull of g, then f is a convex function.

theorem epigraph_subset_epigraph_of_le {n : ℕ} {h g : (Fin n → ℝ) → EReal} (h_le_g : h ≤ g) : epigraph Set.univ g ⊆ epigraph Set.univ h

If h ≤ g, then epi g ⊆ epi h.

theorem convexHull_epigraph_subset_of_convex {n : ℕ} {h g : (Fin n → ℝ) → EReal} (hh : ConvexFunctionOn Set.univ h) (h_le_g : h ≤ g) : (convexHull ℝ) (epigraph Set.univ g) ⊆ epigraph Set.univ h

Convex hull of epi g lies in epi h when h is convex and h ≤ g.

theorem le_inf_section_of_subset_epigraph {n : ℕ} {h : (Fin n → ℝ) → EReal} {F : Set ((Fin n → ℝ) × ℝ)} (hF : F ⊆ epigraph Set.univ h) : h ≤ fun (x : Fin n → ℝ) => sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ F})

Inclusion in an epigraph gives a pointwise lower bound on the inf-section.

theorem convexHullFunction_greatest_convex_minorant {n : ℕ} (g : (Fin n → ℝ) → EReal) : have f := convexHullFunction g; ConvexFunctionOn Set.univ f ∧ f ≤ g ∧ ∀ (h : (Fin n → ℝ) → EReal), ConvexFunctionOn Set.univ h → h ≤ g → h ≤ f

Text 5.5.3: f = conv(g) is the greatest convex function majorized by g.

theorem fst_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Finset ι) (f : ι → α × β) : (s.sum f).1 = ∑ i ∈ s, (f i).1

The first projection of a finite sum of pairs is the sum of first projections.

theorem snd_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Finset ι) (f : ι → α × β) : (s.sum f).2 = ∑ i ∈ s, (f i).2

The second projection of a finite sum of pairs is the sum of second projections.

theorem mem_convexHull_epigraph_iff_fin_combo {n : ℕ} {g : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} : (x, μ) ∈ (convexHull ℝ) (epigraph Set.univ g) ↔ ∃ (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), g (x' i) ≤ ↑(μ' i)

Membership in the convex hull of an epigraph is a finite convex combination.

theorem sum_ereal_mul_le_sum_of_le {n m : ℕ} {g : (Fin n → ℝ) → EReal} (lam : Fin m → ℝ) (x' : Fin m → Fin n → ℝ) (μ' : Fin m → ℝ) (h0 : ∀ (i : Fin m), 0 ≤ lam i) (hμ : ∀ (i : Fin m), g (x' i) ≤ ↑(μ' i)) : ∑ i : Fin m, ↑(lam i) * g (x' i) ≤ ∑ i : Fin m, ↑(lam i) * ↑(μ' i)

Compare finite EReal sums using pointwise bounds and nonnegative weights.

theorem ereal_coe_sum {ι : Type u_1} (s : Finset ι) (f : ι → ℝ) : ∑ i ∈ s, ↑(f i) = ↑(s.sum f)

Coercion from ℝ to EReal commutes with finite sums.

theorem sum_ne_bot_of_ne_bot {ι : Type u_1} (s : Finset ι) (f : ι → EReal) (h : ∀ i ∈ s, f i ≠ ⊥) : s.sum f ≠ ⊥

A finite sum of EReal terms is not ⊥ if each term is not ⊥.