theorem exists_strict_mixedConvexCombination_of_mem_mixedConvexHull {n : ℕ} {S₀ S₁ : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hx : x ∈ mixedConvexHull S₀ S₁) : ∃ (k : ℕ) (m : ℕ) (p : Fin k → Fin n → ℝ) (d : Fin m → Fin n → ℝ) (a : Fin k → ℝ) (b : Fin m → ℝ), (∀ (i : Fin k), p i ∈ S₀) ∧ (∀ (j : Fin m), d j ∈ S₁) ∧ (∀ (i : Fin k), 0 < a i) ∧ (∀ (j : Fin m), 0 < b j) ∧ ∑ i : Fin k, a i = 1 ∧ x = ∑ i : Fin k, a i • p i + ∑ j : Fin m, b j • d j

Extract a strict mixed convex combination from membership in a mixed convex hull.

theorem mem_mixedConvexHull_range_of_exists_coeffs {n k m : ℕ} (p : Fin k → Fin n → ℝ) (d : Fin m → Fin n → ℝ) {y : Fin n → ℝ} (a : Fin k → ℝ) (b : Fin m → ℝ) (ha : ∀ (i : Fin k), 0 ≤ a i) (hb : ∀ (j : Fin m), 0 ≤ b j) (hsum : ∑ i : Fin k, a i = 1) (hy : y = ∑ i : Fin k, a i • p i + ∑ j : Fin m, b j • d j) : y ∈ mixedConvexHull (Set.range p) (Set.range d)

A mixed convex combination over fixed finite families lies in their mixed convex hull.

def euclideanRelativeInterior_fin (n : ℕ) (C : Set (Fin n → ℝ)) : Set (Fin n → ℝ)

Relative interior in Fin n → ℝ, transported via EuclideanSpace.equiv.

Equations

• euclideanRelativeInterior_fin n C = ⇑(EuclideanSpace.equiv (Fin n) ℝ) '' euclideanRelativeInterior n (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C)

theorem mem_euclideanRelativeInterior_fin_iff {n : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} : x ∈ euclideanRelativeInterior_fin n C ↔ (EuclideanSpace.equiv (Fin n) ℝ).symm x ∈ euclideanRelativeInterior n (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C)

theorem euclideanRelativeInterior_fin_singleton (n : ℕ) (x : Fin n → ℝ) : euclideanRelativeInterior_fin n {x} = {x}

theorem mem_euclideanRelativeInterior_convexHull_of_strict_combination {n k : ℕ} (p : Fin k → Fin n → ℝ) (a : Fin k → ℝ) (ha : ∀ (i : Fin k), 0 < a i) (hsum : ∑ i : Fin k, a i = 1) : ∑ i : Fin k, a i • p i ∈ euclideanRelativeInterior_fin n ((convexHull ℝ) (Set.range p))

A strict convex combination of finitely many points lies in the relative interior.

theorem euclideanEquiv_symm_image_add {n : ℕ} (C1 C2 : Set (Fin n → ℝ)) : ⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' (C1 + C2) = ⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C1 + ⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' C2

Image of a Minkowski sum under the EuclideanSpace equivalence.

theorem convexConeHull_image_equiv_fin {n : ℕ} (S : Set (Fin n → ℝ)) : ↑(ConvexCone.hull ℝ (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' S)) = ⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' ↑(ConvexCone.hull ℝ S)

Convex cone hull commutes with the EuclideanSpace equivalence.

theorem euclideanRelativeInterior_fin_convexConeGenerated_eq_smul {n : ℕ} {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hCne : C.Nonempty) : euclideanRelativeInterior_fin n ↑(ConvexCone.hull ℝ C) = {v : Fin n → ℝ | ∃ (r : ℝ), 0 < r ∧ ∃ x ∈ euclideanRelativeInterior_fin n C, v = r • x}

Relative interior of a convex cone in Fin n → ℝ.

theorem euclideanRelativeInterior_fin_add_eq_and_closure_add_superset {n : ℕ} {C1 C2 : Set (Fin n → ℝ)} (hC1 : Convex ℝ C1) (hC2 : Convex ℝ C2) : euclideanRelativeInterior_fin n (C1 + C2) = euclideanRelativeInterior_fin n C1 + euclideanRelativeInterior_fin n C2

Relative interior of a Minkowski sum in Fin n → ℝ.

theorem convexConeHull_convexHull_eq {n : ℕ} (S : Set (Fin n → ℝ)) : ↑(ConvexCone.hull ℝ ((convexHull ℝ) S)) = ↑(ConvexCone.hull ℝ S)

The convex cone hull of a convex hull equals the convex cone hull of the set.

theorem mem_euclideanRelativeInterior_cone_of_strict_positive_combination {n m : ℕ} (d : Fin m → Fin n → ℝ) (b : Fin m → ℝ) (hb : ∀ (j : Fin m), 0 < b j) : ∑ j : Fin m, b j • d j ∈ euclideanRelativeInterior_fin n (cone n (Set.range d))

A strictly positive linear combination of directions lies in the relative interior of the cone.