def IsConvexWeights (m : ℕ) (w : Fin m → ℝ) : Prop

Definition 17.0.1 (Convex combination). Let x₁, …, xₘ ∈ ℝⁿ and let coefficients λ₁, …, λₘ satisfy λ i ≥ 0 for all i and ∑ i, λ i = 1. Then the vector ∑ i, λ i • x i is called a convex combination of the points x₁, …, xₘ.

Equations

• IsConvexWeights m w = ((∀ (i : Fin m), 0 ≤ w i) ∧ ∑ i : Fin m, w i = 1)

def convexCombination (n m : ℕ) (x : Fin m → Fin n → ℝ) (w : Fin m → ℝ) : Fin n → ℝ

The weighted sum ∑ i, w i • x i.

Equations

• convexCombination n m x w = ∑ i : Fin m, w i • x i

theorem isConvexCombination_of_isConvexWeights (n m : ℕ) (x : Fin m → Fin n → ℝ) (w : Fin m → ℝ) (hw : IsConvexWeights m w) : IsConvexCombination n m x (convexCombination n m x w)

If w are nonnegative and sum to 1, then ∑ i, w i • x i is a convex combination in the sense of IsConvexCombination.

@[reducible, inline]

abbrev conv {n : ℕ} (S : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Definition 17.0.2 (Convex hull). For S ⊆ ℝⁿ, the convex hull of S, denoted conv(S), is the set of all convex combinations of finitely many points of S; equivalently, it is the smallest convex set containing S.

Equations

• conv S = (convexHull ℝ) S

theorem caratheodory_aux_exists_affineIndependent_pos {n : ℕ} {S : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hx : x ∈ conv S) : ∃ (ι : Type) (x_1 : Fintype ι) (z : ι → Fin n → ℝ) (w : ι → ℝ), Set.range z ⊆ S ∧ AffineIndependent ℝ z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x

Helper: extract a finite affinely independent positive convex combination.

theorem caratheodory_aux_card_le_n_add_one {n : ℕ} {ι : Type u_1} [Fintype ι] {z : ι → Fin n → ℝ} (hz : AffineIndependent ℝ z) : Fintype.card ι ≤ n + 1

Helper: an affinely independent family in ℝⁿ has cardinality at most n + 1.

theorem caratheodory_aux_reindex_to_Fin {n : ℕ} {S : Set (Fin n → ℝ)} {x : Fin n → ℝ} {ι : Type u_1} [Fintype ι] (z : ι → Fin n → ℝ) (w : ι → ℝ) (hzS : Set.range z ⊆ S) (hw_pos : ∀ (i : ι), 0 < w i) (hw_sum : ∑ i : ι, w i = 1) (hw_x : ∑ i : ι, w i • z i = x) : ∃ (x' : Fin (Fintype.card ι) → Fin n → ℝ) (w' : Fin (Fintype.card ι) → ℝ), (∀ (i : Fin (Fintype.card ι)), x' i ∈ S) ∧ IsConvexWeights (Fintype.card ι) w' ∧ x = convexCombination n (Fintype.card ι) x' w'

Helper: reindex a finite convex combination to Fin m.

theorem caratheodory {n : ℕ} {S : Set (Fin n → ℝ)} {x : Fin n → ℝ} : x ∈ conv S → ∃ m ≤ n + 1, ∃ (x' : Fin m → Fin n → ℝ) (w : Fin m → ℝ), (∀ (i : Fin m), x' i ∈ S) ∧ IsConvexWeights m w ∧ x = convexCombination n m x' w

Theorem 17.0.3 (Carath'eodory). Let S ⊆ ℝⁿ. For every x ∈ conv(S), there exist x₁, …, xₘ ∈ S and coefficients λ₁, …, λₘ ≥ 0 such that x = ∑ i, λ i • x i, ∑ i, λ i = 1, and m ≤ n + 1.

def mixedConvexHull {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Definition 17.0.4 (Mixed convex hull). Let S = S₀ ∪ S₁, where S₀ ⊆ ℝⁿ is a set of points and S₁ is a set of directions. The (mixed) convex hull conv(S) is the smallest convex set C ⊆ ℝⁿ such that:

(1) C ⊇ S₀; (2) C recedes in all directions in S₁, i.e. for every d ∈ S₁, x ∈ C, and t ≥ 0, x + t • d ∈ C.

Equations

• mixedConvexHull S₀ S₁ = ⋂₀ {C : Set (Fin n → ℝ) | Convex ℝ C ∧ S₀ ⊆ C ∧ ∀ ⦃d : Fin n → ℝ⦄, d ∈ S₁ → ∀ ⦃x : Fin n → ℝ⦄, x ∈ C → ∀ (t : ℝ), 0 ≤ t → x + t • d ∈ C}

@[reducible, inline]

abbrev ray (n : ℕ) (S₁ : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Definition 17.0.5 (ray S₁ and cone S₁, LaTeX label def:ray-cone). Let ray S₁ be the set consisting of the origin and all vectors whose directions belong to S₁, i.e. all vectors of the form t • d with d ∈ S₁ and t ≥ 0. Define cone(S₁) := conv(ray S₁). Equivalently, cone(S₁) is the convex cone generated by all vectors whose directions belong to S₁.

Equations

• ray n S₁ = Set.insert 0 (rayNonneg n S₁)

@[reducible, inline]

abbrev cone (n : ℕ) (S₁ : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

The cone obtained as the convex hull of ray S₁.

Equations

• cone n S₁ = conv (ray n S₁)

theorem cone_eq_convexConeGenerated_aux_ray_subset_convexConeGenerated (n : ℕ) (S₁ : Set (Fin n → ℝ)) : ray n S₁ ⊆ convexConeGenerated n S₁

The ray lies in the generated cone.

theorem cone_eq_convexConeGenerated_aux_ray_smul_subset {n : ℕ} {S₁ : Set (Fin n → ℝ)} {c : ℝ} (hc : 0 < c) : c • ray n S₁ ⊆ ray n S₁

Positive scaling sends the ray into itself.

theorem cone_eq_convexConeGenerated_aux_pos_smul_mem_cone {n : ℕ} {S₁ : Set (Fin n → ℝ)} {c : ℝ} (hc : 0 < c) {x : Fin n → ℝ} (hx : x ∈ cone n S₁) : c • x ∈ cone n S₁

The cone is closed under positive scaling.

theorem cone_eq_convexConeGenerated_aux_hull_subset_cone {n : ℕ} {S₁ : Set (Fin n → ℝ)} : ↑(ConvexCone.hull ℝ S₁) ⊆ cone n S₁

The convex cone hull of S₁ lies in cone S₁.

theorem cone_eq_convexConeGenerated_aux_convexConeGenerated_subset_cone (n : ℕ) (S₁ : Set (Fin n → ℝ)) : convexConeGenerated n S₁ ⊆ cone n S₁

The generated cone is contained in cone.

theorem cone_eq_convexConeGenerated (n : ℕ) (S₁ : Set (Fin n → ℝ)) : cone n S₁ = convexConeGenerated n S₁

The cone defined as conv(ray S₁) agrees with the convex cone generated by S₁.

theorem convex_mixedConvexHull {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) : Convex ℝ (mixedConvexHull S₀ S₁)

The mixed convex hull is convex.

theorem add_ray_subset_mixedConvexHull {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) : S₀ + ray n S₁ ⊆ mixedConvexHull S₀ S₁

Elements of S₀ + ray S₁ lie in the mixed convex hull.

theorem isConvexCone_convexConeGenerated {n : ℕ} (S₁ : Set (Fin n → ℝ)) : IsConvexCone n (convexConeGenerated n S₁)

The generated cone is a convex cone.

theorem conv_add_cone_mem_mixedConvexHull_family {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) : Convex ℝ (conv S₀ + cone n S₁) ∧ S₀ ⊆ conv S₀ + cone n S₁ ∧ ∀ ⦃d : Fin n → ℝ⦄, d ∈ S₁ → ∀ ⦃x : Fin n → ℝ⦄, x ∈ conv S₀ + cone n S₁ → ∀ (t : ℝ), 0 ≤ t → x + t • d ∈ conv S₀ + cone n S₁

The set conv S₀ + cone S₁ satisfies the mixed convex hull properties.

theorem mixedConvexHull_eq_conv_add_ray_eq_conv_add_cone {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) : mixedConvexHull S₀ S₁ = conv (S₀ + ray n S₁) ∧ conv (S₀ + ray n S₁) = conv S₀ + cone n S₁

Proposition 17.0.6 (Representation of the mixed convex hull), LaTeX label prop:mixed-representation. With the notation above, the smallest mixed convex hull exists, and one has

mixedConvexHull S₀ S₁ = conv (S₀ + ray n S₁) = conv S₀ + cone n S₁.

def IsMixedConvexCombination (n m : ℕ) (S₀ S₁ : Set (Fin n → ℝ)) (x : Fin n → ℝ) : Prop

Definition 17.0.7 (Mixed convex combination), LaTeX label def:mixed-comb. Let S = S₀ ∪ S₁ be a mixed set of points S₀ ⊆ ℝⁿ and directions S₁ ⊆ ℝⁿ. A vector x ∈ ℝⁿ is a convex combination of m points and directions in S if it can be written as

x = λ₁ • x₁ + ··· + λₖ • xₖ + λₖ₊₁ • xₖ₊₁ + ··· + λₘ • xₘ,

where 1 ≤ k ≤ m, one has x₁, …, xₖ ∈ S₀, the vectors xₖ₊₁, …, xₘ have directions in S₁, all coefficients satisfy λ i ≥ 0, and λ₁ + ··· + λₖ = 1.

In this formalization, “has direction in S₁” is modeled as membership in ray n S₁.

Equations

• One or more equations did not get rendered due to their size.

theorem one_le_of_IsConvexWeights {m : ℕ} {w : Fin m → ℝ} (hw : IsConvexWeights m w) : 1 ≤ m

Convex weights force at least one summand.

theorem sum_smul_mem_cone_of_nonneg_mem_ray {n m : ℕ} {S₁ : Set (Fin n → ℝ)} (d : Fin m → Fin n → ℝ) (b : Fin m → ℝ) (hd : ∀ (j : Fin m), d j ∈ ray n S₁) (hb : ∀ (j : Fin m), 0 ≤ b j) : ∑ j : Fin m, b j • d j ∈ cone n S₁

A nonnegative linear combination of rays lies in the cone.

theorem exists_mixedConvexCombination_of_mem_mixedConvexHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {x : Fin n → ℝ} : x ∈ mixedConvexHull S₀ S₁ → ∃ (m : ℕ), IsMixedConvexCombination n m S₀ S₁ x

Membership in the mixed convex hull gives a mixed convex combination.

theorem mem_mixedConvexHull_of_IsMixedConvexCombination {n m : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {x : Fin n → ℝ} : IsMixedConvexCombination n m S₀ S₁ x → x ∈ mixedConvexHull S₀ S₁

A mixed convex combination lies in the mixed convex hull.

theorem mem_mixedConvexHull_iff_exists_mixedConvexCombination {n : ℕ} (S₀ S₁ : Set (Fin n → ℝ)) (x : Fin n → ℝ) : x ∈ mixedConvexHull S₀ S₁ ↔ ∃ (m : ℕ), IsMixedConvexCombination n m S₀ S₁ x

Proposition 17.0.8 (Algebraic characterization of conv S), LaTeX label prop:algebraic-char. With the notation above, a vector x ∈ ℝⁿ lies in the (mixed) convex hull if and only if x is a mixed convex combination in the sense of Definition 17.0.7.

def liftingHyperplane (n : ℕ) : Set (Fin (n + 1) → ℝ)

Definition 17.0.9 (Lifting data in ℝ^{n+1}), LaTeX label def:lifting. Let H := {(1, x) | x ∈ ℝⁿ} ⊆ ℝ^{n+1}.

Equations

• liftingHyperplane n = Set.range fun (x : Fin n → ℝ) (i : Fin (n + 1)) => Fin.cases 1 x i

def liftingSet {n : ℕ} (S₀ S₁' : Set (Fin n → ℝ)) : Set (Fin (n + 1) → ℝ)

Definition 17.0.9 (Lifting data in ℝ^{n+1}), continued. Given S₀ ⊆ ℝⁿ and a choice of S₁' ⊆ ℝⁿ whose set of directions is S₁, define

S' := {(1, x) | x ∈ S₀} ∪ {(0, x) | x ∈ S₁'} ⊆ ℝ^{n+1}.

Equations

• liftingSet S₀ S₁' = (fun (x : Fin n → ℝ) (i : Fin (n + 1)) => Fin.cases 1 x i) '' S₀ ∪ (fun (x : Fin n → ℝ) (i : Fin (n + 1)) => Fin.cases 0 x i) '' S₁'

def liftingCone {n : ℕ} (S₀ S₁' : Set (Fin n → ℝ)) : Set (Fin (n + 1) → ℝ)

Definition 17.0.9 (Lifting data in ℝ^{n+1}), continued. With S' as above, define K := cone(S').

Equations

• liftingCone S₀ S₁' = cone (n + 1) (liftingSet S₀ S₁')

theorem lift1_mem_liftingHyperplane {n : ℕ} (x : Fin n → ℝ) : (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ∈ liftingHyperplane n

The lifted point (1, x) lies in the lifting hyperplane.

theorem liftingSet_mem_ray_of_mem {n : ℕ} {S₀ S₁' : Set (Fin n → ℝ)} {v : Fin (n + 1) → ℝ} (hv : v ∈ liftingSet S₀ S₁') : v ∈ ray (n + 1) (liftingSet S₀ S₁')

Elements of the lifting set lie on the corresponding ray.

theorem lift0_mem_ray_of_mem_ray {n : ℕ} {S₀ S₁' : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hd : d ∈ ray n S₁') : (fun (i : Fin (n + 1)) => Fin.cases 0 d i) ∈ ray (n + 1) (liftingSet S₀ S₁')

A lifted direction from ray S₁' lies on the ray of the lifting set.

theorem lift_mem_liftingCone_of_IsMixedConvexCombination {n m : ℕ} {S₀ S₁' : Set (Fin n → ℝ)} {x : Fin n → ℝ} : IsMixedConvexCombination n m S₀ S₁' x → (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ∈ liftingCone S₀ S₁'

A mixed convex combination lifts into the lifting cone.

theorem mem_ray_of_mem {n : ℕ} {S : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hx : x ∈ S) : x ∈ ray n S

Elements of a set lie in its generated ray.

theorem ray_mem_decompose {n : ℕ} {S : Set (Fin n → ℝ)} {v : Fin n → ℝ} (hv : v ∈ ray n S) : v = 0 ∨ ∃ s ∈ S, ∃ (t : ℝ), 0 ≤ t ∧ v = t • s

Decompose membership in a ray into either 0 or a nonnegative multiple.

theorem liftingSet_mem_cases {n : ℕ} {S₀ S₁' : Set (Fin n → ℝ)} {v : Fin (n + 1) → ℝ} (hv : v ∈ liftingSet S₀ S₁') : (∃ p ∈ S₀, v = fun (i : Fin (n + 1)) => Fin.cases 1 p i) ∨ ∃ d ∈ S₁', v = fun (i : Fin (n + 1)) => Fin.cases 0 d i

Split membership in the lifting set into point-lifts or direction-lifts.

theorem fin_cases_zero_real {n : ℕ} (a : ℝ) (p : Fin n → ℝ) : Fin.cases a p 0 = a

Evaluate a lifted vector at coordinate 0.

theorem fin_cases_succ_real {n : ℕ} (a : ℝ) (p : Fin n → ℝ) (j : Fin n) : Fin.cases a p j.succ = p j

Evaluate a lifted vector at a successor coordinate.

theorem exists_nonneg_sum_smul_liftingSet_of_lift_mem_liftingCone {n : ℕ} {S₀ S₁' : Set (Fin n → ℝ)} {x : Fin n → ℝ} : (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ∈ liftingCone S₀ S₁' → ∃ (m : ℕ) (s : Fin m → Fin (n + 1) → ℝ) (c : Fin m → ℝ), (∀ (i : Fin m), s i ∈ liftingSet S₀ S₁') ∧ (∀ (i : Fin m), 0 ≤ c i) ∧ (fun (i : Fin (n + 1)) => Fin.cases 1 x i) = ∑ i : Fin m, c i • s i

Cone membership yields a finite nonnegative sum of lifting-set generators.

theorem split_liftingSet_sum_to_IsMixedConvexCombination {n m : ℕ} {S₀ S₁' : Set (Fin n → ℝ)} {x : Fin n → ℝ} (s : Fin m → Fin (n + 1) → ℝ) (c : Fin m → ℝ) (hs : ∀ (i : Fin m), s i ∈ liftingSet S₀ S₁') (hc : ∀ (i : Fin m), 0 ≤ c i) (hsum : (fun (i : Fin (n + 1)) => Fin.cases 1 x i) = ∑ i : Fin m, c i • s i) : ∃ (m' : ℕ), IsMixedConvexCombination n m' S₀ S₁' x

Split a lifting-set sum into a mixed convex combination.

theorem exists_IsMixedConvexCombination_of_lift_mem_liftingCone {n : ℕ} {S₀ S₁' : Set (Fin n → ℝ)} {x : Fin n → ℝ} : (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ∈ liftingCone S₀ S₁' → ∃ (m : ℕ), IsMixedConvexCombination n m S₀ S₁' x

Lifting cone membership yields a mixed convex combination.

theorem mem_mixedConvexHull_iff_lift_mem_liftingCone_inter_liftingHyperplane {n : ℕ} (S₀ S₁' : Set (Fin n → ℝ)) (x : Fin n → ℝ) : x ∈ mixedConvexHull S₀ S₁' ↔ (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ∈ liftingCone S₀ S₁' ∩ liftingHyperplane n

Proposition 17.0.10 (Cone slice representation), LaTeX label prop:lift-cone. With the notation in Definition 17.0.9, the (mixed) convex hull can be identified with the slice K ∩ H via the correspondence x ↦ (1, x). Equivalently, mixed convex combinations correspond to nonnegative linear combinations

λ₁ (1, x₁) + ··· + λₖ (1, xₖ) + λₖ₊₁ (0, xₖ₊₁) + ··· + λₘ (0, xₘ) in ℝ^{n+1}

which lie in the hyperplane H = {(1, x) | x ∈ ℝⁿ}.

theorem mixedConvexHull_singleton_zero_eq_cone {n : ℕ} (T : Set (Fin n → ℝ)) : mixedConvexHull {0} T = cone n T

Mixed convex hull with point-set {0} agrees with the cone.