LeanPool.Polytopes.Cutspace

Cut spaces obtained by intersecting collections of halfspaces.

source

def cutSpace {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H_ : Set (Halfspace E)) :

Set E

The cut space of a set of halfspaces: the intersection of all of them.

Equations

cutSpace H_ = ⋂₀ (SetLike.coe '' H_)

Instances For

source

theorem Convex_cutSpace {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H_ : Set (Halfspace E)) :

Convex ℝ (cutSpace H_)

source

theorem Closed_cutSpace {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H_ : Set (Halfspace E)) :

IsClosed (cutSpace H_)

source

theorem mem_cutSpace {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H_ : Set (Halfspace E)) (x : E) :

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

source

theorem empty_cutSpace {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (h : ∃ (x : E), x ≠ 0) :

∃ (H_ : Set (Halfspace E)), cutSpace H_ = ∅

source

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

∃ (H_ : Set (Halfspace E)), cutSpace H_ = {x : E | ↑f x = c}

source

theorem inter_cutSpace {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H_1 H_2 : Set (Halfspace E)) :

cutSpace (H_1 ∪ H_2) = cutSpace H_1 ∩ cutSpace H_2

source

def orthoHyperplane {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : { x : E // x ≠ 0 }) :

Set (Halfspace E)

The pair of halfspaces whose intersection is the hyperplane orthogonal to x.

Equations

orthoHyperplane x = {{ f := pointDualLin x, α := 0 }, { f := pointDualLin ⟨-↑x, ⋯⟩, α := 0 }}

Instances For

source

theorem orthoHyperplane.Finite {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : { x : E // x ≠ 0 }) :

(orthoHyperplane x).Finite

source

theorem orthoHyperplane_mem {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : { x : E // x ≠ 0 }) (y : E) :

y ∈ cutSpace (orthoHyperplane x) ↔ inner ℝ (↑x) y = 0

source

theorem cutSpace_sUnion_orthoHyperplane {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (X : Set { x : E // x ≠ 0 }) (y : E) :

y ∈ cutSpace (⋃₀ (orthoHyperplane '' X)) ↔ ∀ (i : ↑(orthoHyperplane '' X)), y ∈ cutSpace ↑i

source

theorem orthoHyperplanes_mem {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (X : Set { x : E // x ≠ 0 }) (y : E) :

y ∈ cutSpace (⋃₀ (orthoHyperplane '' X)) ↔ ∀ x ∈ X, inner ℝ (↑x) y = 0

source

def submoduleCut {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (p : Subspace ℝ E) :

Set (Halfspace E)

A finite set of halfspaces whose cut space is the subspace p, built from a basis of pᗮ.

Equations

submoduleCut p = ⋃₀ (orthoHyperplane '' Subtype.val ⁻¹' Set.range (Subtype.val ∘ ⇑(Module.finBasis ℝ ↥pᗮ)))

Instances For

source

theorem Submodule_cut_finite {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (p : Subspace ℝ E) :

(submoduleCut p).Finite

source

theorem Submodule_cutspace {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (p : Subspace ℝ E) :

∃ (H_ : Set (Halfspace E)), H_.Finite ∧ ↑p = cutSpace H_