theorem ereal_bot_mul_add_of_no_forbidden {x1 x2 : EReal} (h : ¬ERealForbiddenSum (⊥ * x1) (⊥ * x2)) : ⊥ * (x1 + x2) = ⊥ * x1 + ⊥ * x2

Left distributivity for multiplication by ⊥ under a non-forbidden sum.

theorem ereal_mul_add_of_no_forbidden {α x1 x2 : EReal} (hα : ¬ERealForbiddenSum (α * x1) (α * x2)) : α * (x1 + x2) = α * x1 + α * x2

Left distributivity under a non-forbidden sum.

theorem ereal_arithmetic_laws_of_no_forbidden {x1 x2 x3 α : EReal} (_h12 : ¬ERealForbiddenSum x1 x2) (_h23 : ¬ERealForbiddenSum x2 x3) (_h123 : ¬ERealForbiddenSum (x1 + x2) x3) (_h123' : ¬ERealForbiddenSum x1 (x2 + x3)) (hα : ¬ERealForbiddenSum (α * x1) (α * x2)) : x1 + x2 = x2 + x1 ∧ x1 + x2 + x3 = x1 + (x2 + x3) ∧ x1 * x2 = x2 * x1 ∧ x1 * x2 * x3 = x1 * (x2 * x3) ∧ α * (x1 + x2) = α * x1 + α * x2

Defintion 4.4.6: Under these conventions, the usual arithmetic laws remain valid as long as none of the indicated binary sums is forbidden.

def ConvexFunction {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop

Remark 4.4.7: In this book, a “convex function” means an EReal-valued convex function defined on all of ℝ^n, unless otherwise specified; this convention lets the effective domain be determined implicitly by where f x is or is not ⊤.

Equations

• ConvexFunction f = ConvexFunctionOn Set.univ f

theorem inner_add_const_combo_eq {n : ℕ} (a : Fin n → ℝ) (α t : ℝ) (x y : Fin n → ℝ) : ↑(∑ i : Fin n, ((1 - t) • x + t • y) i * a i + α) = ↑(1 - t) * ↑(∑ i : Fin n, x i * a i + α) + ↑t * ↑(∑ i : Fin n, y i * a i + α)

Convex combinations preserve linear-plus-constant forms.

theorem affineFunctionOn_univ_inner_add_const {n : ℕ} (a : Fin n → ℝ) (α : ℝ) : AffineFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(∑ i : Fin n, x i * a i + α)

theorem affineFunctionOn_univ_eq_combo {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : AffineFunctionOn Set.univ f) (x y : Fin n → ℝ) (t : ℝ) : 0 ≤ t → t ≤ 1 → f ((1 - t) • x + t • y) = ↑(1 - t) * f x + ↑t * f y

Affine functions on Set.univ agree with convex combinations.

theorem affineFunctionOn_univ_toReal_linearMap {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : AffineFunctionOn Set.univ f) : ∃ (A : (Fin n → ℝ) →ₗ[ℝ] ℝ), ∀ (x : Fin n → ℝ), (f x).toReal = A x + (f 0).toReal

Subtracting the value at 0 gives a linear map for an affine function.

theorem linearMap_apply_eq_sum_mul_basis {n : ℕ} (A : (Fin n → ℝ) →ₗ[ℝ] ℝ) (x : Fin n → ℝ) : A x = ∑ i : Fin n, x i * A fun (j : Fin n) => if j = i then 1 else 0

A linear functional on Fin n → ℝ is determined by its values on the standard basis.

theorem affineFunctionOn_univ_exists_inner_add_const {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : AffineFunctionOn Set.univ f) : ∃ (a : Fin n → ℝ) (α : ℝ), ∀ (x : Fin n → ℝ), f x = ↑(∑ i : Fin n, x i * a i + α)

Remark 4.5.0: Every affine function on ℝ^n is of the form x ↦ ⟪x, a⟫ + α for some a ∈ ℝ^n and α ∈ ℝ (Theorem 1.5).

noncomputable def functionDimension {n : ℕ} (S : Set (Fin n → ℝ)) (f : (Fin n → ℝ) → EReal) : ℕ

Definition 4.5: The dimension of the effective domain of f is called the dimension of f.

Equations

• functionDimension S f = Module.finrank ℝ ↥(affineSpan ℝ (effectiveDomain S f)).direction

theorem epigraph_mem_of_le {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ : ℝ} (hx : x ∈ S) (hμ : f x ≤ ↑μ) : (x, μ) ∈ epigraph S f

If x ∈ S and f x ≤ μ, then (x, μ) is in the epigraph.

theorem convex_combo_mem_epigraph {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {μ v t : ℝ} (hconv : Convex ℝ (epigraph S f)) (hx : (x, μ) ∈ epigraph S f) (hy : (y, v) ∈ epigraph S f) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (1 - t) • (x, μ) + t • (y, v) ∈ epigraph S f

Convexity of the epigraph yields convex combinations of points in it.

theorem epigraph_combo_proj {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {μ v t : ℝ} : (1 - t) • (x, μ) + t • (y, v) ∈ epigraph S f → (1 - t) • x + t • y ∈ S ∧ f ((1 - t) • x + t • y) ≤ ↑((1 - t) * μ + t * v)

Unpack epigraph membership of a convex combination.

theorem convexFunctionOn_epigraph_condition {n : ℕ} {S : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn S f) (x : Fin n → ℝ) : x ∈ S → ∀ y ∈ S, ∀ (μ v : ℝ), f x ≤ ↑μ → f y ≤ ↑v → ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → (1 - t) • x + t • y ∈ S ∧ f ((1 - t) • x + t • y) ≤ ↑((1 - t) * μ + t * v)

Remark 4.5.1: For convexity of the epigraph, one requires that for any x, y ∈ S, any μ, v ∈ ℝ with f x ≤ μ and f y ≤ v, and any 0 ≤ λ ≤ 1, the point (1 - λ) x + λ y lies in S and satisfies f ((1 - λ) x + λ y) ≤ (1 - λ) μ + λ v; this condition admits several equivalent formulations.

theorem quadratic_combo_expansion {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℝ} (x y : Fin n → ℝ) (t u : ℝ) : (t • x + u • y) ⬝ᵥ Q.mulVec (t • x + u • y) = t ^ 2 * x ⬝ᵥ Q.mulVec x + u ^ 2 * y ⬝ᵥ Q.mulVec y + t * u * (x ⬝ᵥ Q.mulVec y + y ⬝ᵥ Q.mulVec x)

Expansion of the quadratic form on a linear combination.

theorem quadratic_sub_cross {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℝ} (x y : Fin n → ℝ) : (x - y) ⬝ᵥ Q.mulVec (x - y) = x ⬝ᵥ Q.mulVec x + y ⬝ᵥ Q.mulVec y - (x ⬝ᵥ Q.mulVec y + y ⬝ᵥ Q.mulVec x)

Quadratic form of a difference expressed via cross terms.

theorem convexity_implies_quadratic_nonneg {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℝ} {a : Fin n → ℝ} {α : ℝ} (hconv : ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => 1 / 2 * x ⬝ᵥ Q.mulVec x + x ⬝ᵥ a + α) (x : Fin n → ℝ) : 0 ≤ x ⬝ᵥ Q.mulVec x

Convexity of the quadratic function forces its quadratic form to be nonnegative.

theorem posSemidef_implies_convexity_quadratic {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℝ} {a : Fin n → ℝ} {α : ℝ} (hpos : Q.PosSemidef) : ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => 1 / 2 * x ⬝ᵥ Q.mulVec x + x ⬝ᵥ a + α

Positive semidefinite quadratic form yields convexity of the quadratic function.

theorem convexOn_quadratic_iff_posSemidef {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℝ} {a : Fin n → ℝ} {α : ℝ} (hQ : Q.IsSymm) : (ConvexOn ℝ Set.univ fun (x : Fin n → ℝ) => 1 / 2 * x ⬝ᵥ Q.mulVec x + x ⬝ᵥ a + α) ↔ Q.PosSemidef

Remark 4.5.1: A quadratic function f x = (1/2) ⟪x, Q x⟫ + ⟪x, a⟫ + α, where Q is a symmetric n × n matrix, is convex on ℝ^n iff Q is positive semidefinite, i.e. ⟪z, Q z⟫ ≥ 0 for every z ∈ ℝ^n.

theorem sum_sq_le_n_mul_sum_sq {n : ℕ} (u : Fin n → ℝ) : Finset.univ.sum u ^ 2 ≤ ↑n * ∑ i : Fin n, u i ^ 2

Cauchy-Schwarz for Fin n: the square of the sum is bounded by n times the sum of squares.

theorem closure_posOrthant_eq_nonneg {n : ℕ} : closure {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i} = {x : Fin n → ℝ | ∀ (i : Fin n), 0 ≤ x i}

The closure of the positive orthant is the nonnegative orthant.

theorem isOpen_posOrthant {n : ℕ} : IsOpen {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}

The positive orthant is open.

theorem convex_posOrthant {n : ℕ} : Convex ℝ {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}

The positive orthant is convex.

theorem contDiffOn_prod_coord {n : ℕ} {C : Set (Fin n → ℝ)} : ContDiffOn ℝ 2 (fun (x : Fin n → ℝ) => ∏ i : Fin n, x i) C

The coordinate product is C^2 on any set.

theorem prod_ne_zero_of_pos {n : ℕ} {x : Fin n → ℝ} (hx : ∀ (i : Fin n), 0 < x i) : ∏ i : Fin n, x i ≠ 0

The coordinate product is nonzero on the positive orthant.

theorem contDiffOn_negGeomMean_pos {n : ℕ} : ContDiffOn ℝ 2 (fun (x : Fin n → ℝ) => -(∏ i : Fin n, x i).rpow (1 / ↑n)) {x : Fin n → ℝ | ∀ (i : Fin n), 0 < x i}

The negative geometric mean is C^2 on the positive orthant.

theorem prod_erase_erase_eq_div {n : ℕ} (x : Fin n → ℝ) (hx : ∀ (i : Fin n), x i ≠ 0) {i j : Fin n} (hj : j ∈ Finset.univ.erase i) : ∏ k ∈ (Finset.univ.erase i).erase j, x k = (∏ k : Fin n, x k) / x i / x j

Product over Finset.univ with two entries removed.

theorem sum_erase_mul_sum_eq_sum_sq_sub_sum_sq {n : ℕ} (u : Fin n → ℝ) : ∑ i : Fin n, ∑ j ∈ Finset.univ.erase i, u i * u j = Finset.univ.sum u ^ 2 - ∑ i : Fin n, u i ^ 2

Off-diagonal double sum identity.