@[reducible, inline]

abbrev nonnegOrthant (m : ℕ) : Set (Fin m → ℝ)

Definition 17.0.14 ($m$-dimensional (skew) orthant), LaTeX label def:orthant. A generalized m-dimensional simplex with one ordinary vertex and m - 1 vertices at infinity is called an m-dimensional (skew) orthant. The m-dimensional orthants in ℝⁿ are exactly the images of the nonnegative orthant ℝ^m_{≥ 0} under one-to-one affine transformations from ℝ^m into ℝⁿ.

Equations

• nonnegOrthant m = Set.Ici 0

def IsSkewOrthant (n m : ℕ) (O : Set (Fin n → ℝ)) : Prop

A set O ⊆ ℝⁿ is an m-dimensional (skew) orthant if it is the image of the nonnegative orthant ℝ^m_{≥ 0} under an injective affine map ℝ^m → ℝⁿ.

Equations

• IsSkewOrthant n m O = ∃ (f : (Fin m → ℝ) →ᵃ[ℝ] Fin n → ℝ), Function.Injective ⇑f ∧ O = ⇑f '' nonnegOrthant m

theorem isClosed_nonnegOrthant (m : ℕ) : IsClosed (nonnegOrthant m)

The nonnegative orthant is closed.

theorem isClosedEmbedding_of_injective_affineMap {n m : ℕ} (f : (Fin m → ℝ) →ᵃ[ℝ] Fin n → ℝ) (hf : Function.Injective ⇑f) : Topology.IsClosedEmbedding fun (x : Fin m → ℝ) => f x

An injective affine map between finite-dimensional real vector spaces is a closed embedding.

theorem isClosed_of_isSkewOrthant {n m : ℕ} {O : Set (Fin n → ℝ)} : IsSkewOrthant n m O → IsClosed O

Propositon 17.0.15 (Closedness), LaTeX label prop:closedness. Every m-dimensional (skew) orthant in ℝⁿ is closed.

def IsGeneralizedSimplex (n m : ℕ) (S : Set (Fin n → ℝ)) : Prop

A generalized m-dimensional simplex in ℝⁿ, modeled via the identification x ↦ (1, x) ∈ H = {(1, x) | x ∈ ℝⁿ} as a slice of an (m+1)-dimensional skew orthant in ℝ^{n+1}.

Equations

• IsGeneralizedSimplex n m S = ∃ (O : Set (Fin (n + 1) → ℝ)), IsSkewOrthant (n + 1) (m + 1) O ∧ S = (fun (x : Fin n → ℝ) (i : Fin (n + 1)) => Fin.cases 1 x i) ⁻¹' (O ∩ liftingHyperplane n)

theorem continuous_lift1 (n : ℕ) : Continuous fun (x : Fin n → ℝ) (i : Fin (n + 1)) => Fin.cases 1 x i

The lift map x ↦ (1, x) is continuous.

theorem liftingHyperplane_eq (n : ℕ) : liftingHyperplane n = {y : Fin (n + 1) → ℝ | y 0 = 1}

The lifting hyperplane is given by the equation y 0 = 1.

theorem isClosed_liftingHyperplane (n : ℕ) : IsClosed (liftingHyperplane n)

The lifting hyperplane is closed.

theorem isClosed_of_isGeneralizedSimplex {n m : ℕ} {S : Set (Fin n → ℝ)} : IsGeneralizedSimplex n m S → IsClosed S

Propositon 17.0.15 (Closedness), generalized simplex version: every generalized m-dimensional simplex in ℝⁿ is closed.

theorem isClosed_of_isGeneralizedSimplex_via_orthant_slicing {n m : ℕ} {S : Set (Fin n → ℝ)} : IsGeneralizedSimplex n m S → IsClosed S

Propositon 17.0.16 (Closedness via orthant slicing), LaTeX label prop:gen-simplex-closed.

Every generalized m-dimensional simplex in ℝⁿ is closed. More precisely, such a set can be identified with the intersection of an (m+1)-dimensional orthant in ℝ^{n+1} and the hyperplane H = {(1, x) | x ∈ ℝⁿ}.

In this file, a “generalized simplex” is represented by IsGeneralizedSimplex n m S, which models the “orthant slicing” description.

theorem split_liftingSet_sum_to_IsMixedConvexCombination_fixed_length {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) : IsMixedConvexCombination n m S₀ S₁' x

Split a lifting-set sum into a mixed convex combination, preserving the length.

theorem trim_nonneg_sum_smul_drop_zero_coeffs {n m : ℕ} {S : Set (Fin (n + 1) → ℝ)} {y : Fin (n + 1) → ℝ} (s : Fin m → Fin (n + 1) → ℝ) (c : Fin m → ℝ) (hs : ∀ (i : Fin m), s i ∈ S) (hc : ∀ (i : Fin m), 0 ≤ c i) (hsum : y = ∑ i : Fin m, c i • s i) : ∃ (m' : ℕ) (s' : Fin m' → Fin (n + 1) → ℝ) (c' : Fin m' → ℝ), (∀ (i : Fin m'), s' i ∈ S) ∧ (∀ (i : Fin m'), 0 < c' i) ∧ y = ∑ i : Fin m', c' i • s' i

Drop zero coefficients from a nonnegative sum and reindex to obtain positive coefficients.

theorem exists_linear_relation_sum_smul_eq_zero_exists_pos {m : ℕ} {V : Type u_1} [AddCommGroup V] [Module ℝ V] (s : Fin m → V) (hlin : ¬LinearIndependent ℝ s) : ∃ (μ : Fin m → ℝ), ∑ i : Fin m, μ i • s i = 0 ∧ ∃ (i : Fin m), 0 < μ i

A linear dependence yields a relation with a positive coefficient.

theorem drop_zero_coeff_sum_smul_to_shorter {n m : ℕ} {T : Set (Fin (n + 1) → ℝ)} {y : Fin (n + 1) → ℝ} (s : Fin (m + 1) → Fin (n + 1) → ℝ) (c : Fin (m + 1) → ℝ) (hs : ∀ (i : Fin (m + 1)), s i ∈ T) (hc : ∀ (i : Fin (m + 1)), 0 ≤ c i) (hsum : y = ∑ i : Fin (m + 1), c i • s i) (i0 : Fin (m + 1)) (hci0 : c i0 = 0) : ∃ (s' : Fin m → Fin (n + 1) → ℝ) (c' : Fin m → ℝ), (∀ (j : Fin m), s' j ∈ T) ∧ (∀ (j : Fin m), 0 ≤ c' j) ∧ y = ∑ j : Fin m, c' j • s' j

Remove a zero coefficient from a nonnegative sum and shorten the index set.

theorem conic_elim_one_generator_pos_to_shorter {n m : ℕ} {T : Set (Fin (n + 1) → ℝ)} {y : Fin (n + 1) → ℝ} (s : Fin (m + 1) → Fin (n + 1) → ℝ) (c : Fin (m + 1) → ℝ) (hs : ∀ (i : Fin (m + 1)), s i ∈ T) (hc : ∀ (i : Fin (m + 1)), 0 < c i) (hsum : y = ∑ i : Fin (m + 1), c i • s i) (hlin : ¬LinearIndependent ℝ s) : ∃ (s' : Fin m → Fin (n + 1) → ℝ) (c' : Fin m → ℝ), (∀ (j : Fin m), s' j ∈ T) ∧ (∀ (j : Fin m), 0 ≤ c' j) ∧ y = ∑ j : Fin m, c' j • s' j

Eliminate one generator from a positive conic combination under linear dependence.

theorem exists_nonneg_sum_smul_liftingSet_le_add_one {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {x : Fin n → ℝ} : (fun (i : Fin (n + 1)) => Fin.cases 1 x i) ∈ liftingCone S₀ S₁ → ∃ m ≤ n + 1, ∃ (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

Reduce a lifting-set representation to at most n + 1 generators.

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

Theorem 17.1 (Caratheodory's Theorem). Let S be a set of points and directions in ℝⁿ, modeled as a pair (S₀, S₁) with point-set S₀ ⊆ ℝⁿ and direction-set S₁ ⊆ ℝⁿ, and let C := conv S be the resulting mixed convex hull (here: C := mixedConvexHull S₀ S₁).

Then x ∈ C if and only if x can be expressed as a convex combination of n + 1 of the points and directions in S (not necessarily distinct); in this file, this is represented as existence of a mixed convex combination of size m ≤ n + 1.

theorem conv_mem_range_of_convexCombination {n k : ℕ} {p : Fin k → Fin n → ℝ} {w : Fin k → ℝ} {x : Fin n → ℝ} (hw : IsConvexWeights k w) (hx : x = convexCombination n k p w) : x ∈ conv (Set.range p)

A convex combination lies in the convex hull of its range.

theorem exists_injective_indexed_convexCombination_of_mem_conv_iUnion {n : ℕ} {I : Type u_1} (Cᵢ : I → Set (Fin n → ℝ)) (hconv : ∀ (i : I), Convex ℝ (Cᵢ i)) {x : Fin n → ℝ} (hx : x ∈ conv (⋃ (i : I), Cᵢ i)) : ∃ (k : ℕ) (idx : Fin k → I) (p : Fin k → Fin n → ℝ) (w : Fin k → ℝ), Function.Injective idx ∧ (∀ (j : Fin k), p j ∈ Cᵢ (idx j)) ∧ IsConvexWeights k w ∧ x = convexCombination n k p w

Coalesce a convex combination in a union into one indexed by distinct sets.