LeanPool.Polytopes.Polytope

Definitions and basic properties of V-polytopes and H-polytopes.

def Vpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set E} (hS : S.Finite) :

The V-polytope of a finite point set S: its convex hull.

The finiteness witness is recorded as it characterises the polytope and is used by the surrounding API, even though the convex hull itself does not depend on it.

Equations

Vpolytope hS = (fun (x : S.Finite) => (convexHull ℝ) S) hS

Instances For

source

@[simp]

theorem Vpolytope_def {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set E} (hS : S.Finite) :

Vpolytope hS = (convexHull ℝ) S

source

theorem Convex_Vpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set E} (hS : S.Finite) :

Convex ℝ (Vpolytope hS)

source

theorem Closed_Vpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set E} (hS : S.Finite) :

IsClosed (Vpolytope hS)

source

theorem Compact_Vpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set E} (hS : S.Finite) :

IsCompact (Vpolytope hS)

source

def Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (hH_ : H_.Finite) :

Set E

The H-polytope of a finite set of halfspaces H_: the intersection of those halfspaces.

The finiteness witness is recorded as it characterises the polytope and is used by the surrounding API, even though the intersection itself does not depend on it.

Equations

Hpolytope hH_ = (fun (x : H_.Finite) => ⋂₀ (SetLike.coe '' H_)) hH_

Instances For

source

@[simp]

theorem Hpolytope_def {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (hH_ : H_.Finite) :

Hpolytope hH_ = ⋂₀ (SetLike.coe '' H_)

source

theorem Convex_Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (hH_ : H_.Finite) :

Convex ℝ (Hpolytope hH_)

source

theorem Closed_Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H : Set (Halfspace E)} (hH_ : H.Finite) :

IsClosed (Hpolytope hH_)

source

theorem Hpolytope_same {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (hH_1 hH_2 : H_.Finite) :

Hpolytope hH_1 = Hpolytope hH_2

source

theorem mem_Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (hH_ : H_.Finite) (x : E) :

x ∈ Hpolytope hH_ ↔ ∀ Hi ∈ H_, ↑Hi.f x ≤ Hi.α

source

theorem empty_Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Nontrivial E] :

∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite), Hpolytope hH_ = ∅

source

theorem origin_Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] :

∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite), Hpolytope hH_ = {0}

source

theorem hyperplane_Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : { f : StrongDual ℝ E // ‖f‖ = 1 }) (c : ℝ) :

∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite), Hpolytope hH_ = {x : E | ↑f x = c}

source

theorem inter_Hpolytope {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H_1 H_2 : Set (Halfspace E)) (hH_1 : H_1.Finite) (hH_2 : H_2.Finite) :

Hpolytope ⋯ = Hpolytope hH_1 ∩ Hpolytope hH_2

source

theorem Vpolytope_translation {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set E} (hS : S.Finite) (x : E) :

Vpolytope ⋯ = Vpolytope hS + {x}

source

theorem Hpolytope_translation {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H_ : Set (Halfspace E)} (hH_ : H_.Finite) (x : E) :

Hpolytope ⋯ = Hpolytope hH_ + {x}