@[reducible, inline]

abbrev euclideanEquiv (n : ℕ) : EuclideanSpace ℝ (Fin n) ≃L[ℝ] Fin n → ℝ

The EuclideanSpace equivalence for Fin n.

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

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

theorem mem_euclideanRelativeBoundary_fin_iff {n : ℕ} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} : x ∈ euclideanRelativeBoundary_fin n C ↔ (euclideanEquiv n).symm x ∈ euclideanRelativeBoundary n (⇑(euclideanEquiv n).symm '' C)

theorem euclideanRelativeInterior_fin_subset_closure {n : ℕ} {C : Set (Fin n → ℝ)} : euclideanRelativeInterior_fin n C ⊆ closure C

theorem euclideanRelativeBoundary_fin_eq_diff_of_isClosed {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) : euclideanRelativeBoundary_fin n C = C \ euclideanRelativeInterior_fin n C

theorem isFace_image_equiv_fin_symm {n : ℕ} {C C' : Set (EuclideanSpace ℝ (Fin n))} (hC' : IsFace C C') : IsFace (⇑(euclideanEquiv n) '' C) (⇑(euclideanEquiv n) '' C')

Transport a face along EuclideanSpace.equiv back to Fin n → ℝ.

theorem isClosed_of_isFace_fin {n : ℕ} {C C' : Set (Fin n → ℝ)} (hC' : IsFace C C') (hC'conv : Convex ℝ C') (hCclosed : IsClosed C) : IsClosed C'

theorem finrank_direction_affineSpan_equiv {n : ℕ} (C : Set (Fin n → ℝ)) : Module.finrank ℝ ↥(affineSpan ℝ (⇑(euclideanEquiv n).symm '' C)).direction = Module.finrank ℝ ↥(affineSpan ℝ C).direction

Finrank of the affine span direction is invariant under the Euclidean equivalence.

theorem noLines_equiv_fin {n : ℕ} {C : Set (Fin n → ℝ)} (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) : ¬∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ 0 ∧ y ∈ -(⇑(euclideanEquiv n).symm '' C).recessionCone ∩ (⇑(euclideanEquiv n).symm '' C).recessionCone

No-lineality is preserved under the Euclidean equivalence.

theorem mem_recessionCone_of_isExtremeDirection_fin {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) {d : Fin n → ℝ} (hd : IsExtremeDirection C d) : d ∈ C.recessionCone

Transfer the recession-cone lemma for extreme directions to Fin n → ℝ.

theorem isExtremeDirection_of_isFace {n : ℕ} {C F : Set (Fin n → ℝ)} {d : Fin n → ℝ} (hF : IsFace C F) (hd : IsExtremeDirection F d) : IsExtremeDirection C d

Extreme directions of a face are extreme directions of the ambient set.

theorem exists_proper_face_with_mem_ri_of_mem_euclideanRelativeBoundary {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) {x : Fin n → ℝ} (hx : x ∈ euclideanRelativeBoundary_fin n C) : ∃ (F : Set (Fin n → ℝ)), IsFace C F ∧ F ≠ C ∧ F.Nonempty ∧ Convex ℝ F ∧ x ∈ euclideanRelativeInterior_fin n F

A relative boundary point lies in the relative interior of a proper face.

theorem noLines_of_isFace {n : ℕ} {C F : Set (Fin n → ℝ)} (hF : IsFace C F) (hFne : F.Nonempty) (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hNoLinesC : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -F.recessionCone ∩ F.recessionCone

A face of a closed convex set with no nonzero lineality direction also has none.

theorem mem_mixedConvexHull_of_mem_euclideanRelativeBoundary_under_IH {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hNoLines : ¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -C.recessionCone ∩ C.recessionCone) (IH : ∀ ⦃F : Set (Fin n → ℝ)⦄, IsClosed F → Convex ℝ F → (¬∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ -F.recessionCone ∩ F.recessionCone) → Module.finrank ℝ ↥(affineSpan ℝ F).direction < Module.finrank ℝ ↥(affineSpan ℝ C).direction → F ⊆ mixedConvexHull (Set.extremePoints ℝ F) {d : Fin n → ℝ | IsExtremeDirection F d}) {x : Fin n → ℝ} (hx : x ∈ euclideanRelativeBoundary_fin n C) : x ∈ mixedConvexHull (Set.extremePoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}

Boundary points belong to the mixed convex hull under the finrank induction hypothesis.

theorem mem_mixedConvexHull_of_mem_euclideanRelativeInterior_of_boundary_in_hull {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hC_not_affine : ¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))), ↑A = ⇑(euclideanEquiv n).symm '' C) (hC_not_closedHalf_affine : ¬∃ (A : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) (f : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ) (a : ℝ), f ≠ 0 ∧ ⇑(euclideanEquiv n).symm '' C = ↑A ∩ {x : EuclideanSpace ℝ (Fin n) | f x ≤ a}) (hbdy : ∀ y ∈ euclideanRelativeBoundary_fin n C, y ∈ mixedConvexHull (Set.extremePoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}) ⦃x : Fin n → ℝ⦄ : x ∈ euclideanRelativeInterior_fin n C → x ∈ mixedConvexHull (Set.extremePoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}

Relative interior points belong to the mixed convex hull once boundary points do.

theorem closedConvex_eq_mixedConvexHull_of_finrank_direction_eq_zero {n : ℕ} {C : Set (Fin n → ℝ)} (hCclosed : IsClosed C) (hCconv : Convex ℝ C) (hfin : Module.finrank ℝ ↥(affineSpan ℝ C).direction = 0) : C = mixedConvexHull (Set.extremePoints ℝ C) {d : Fin n → ℝ | IsExtremeDirection C d}

Base case: if the affine span has direction of finrank 0, then C is a singleton and is generated by its extreme points/directions.

theorem mem_extremePoints_endpoint_of_eq_image_add_smul_Ici {n : ℕ} {C : Set (Fin n → ℝ)} {x0 d : Fin n → ℝ} (hd : d ≠ 0) (hC : C = (fun (t : ℝ) => x0 + t • d) '' Set.Ici 0) : x0 ∈ Set.extremePoints ℝ C

The endpoint of a ray is an extreme point of the ray.

theorem isExtremeDirection_of_eq_image_add_smul_Ici {n : ℕ} {C : Set (Fin n → ℝ)} {x0 d : Fin n → ℝ} (hd : d ≠ 0) (hC : C = (fun (t : ℝ) => x0 + t • d) '' Set.Ici 0) (hCconv : Convex ℝ C) : IsExtremeDirection C d

A ray is an extreme direction of itself.