Documentation

LeanPool.Polytopes.Halfspace

Halfspaces in inner product spaces and their basic geometric operations.

structure Halfspace (E : Type) [NormedAddCommGroup E] [InnerProductSpace ℝ E] :

A halfspace of E. For convenience it is described by a continuous linear functional of norm 1 together with a real number bound.

f : { f : StrongDual ℝ E // ‖f‖ = 1 }
The bounding functional, of norm 1.
α : ℝ
The real bound defining the halfspace.

Instances For

@[implicit_reducible]

noncomputable instance NegUnitSphereDual {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :

Neg { f : StrongDual ℝ E // ‖f‖ = 1 }

Equations

NegUnitSphereDual = { neg := fun (f : { f : StrongDual ℝ E // ‖f‖ = 1 }) => ⟨-↑f, ⋯⟩ }

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

↑(-f) = -↑f

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

Function.Surjective ⇑↑f

def Halfspace.S {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (H_ : Halfspace E) :

The underlying set of points of a halfspace H_.

Equations

H_.S = ⇑↑H_.f ⁻¹' {x : ℝ | x ≤ H_.α}

Instances For

@[implicit_reducible]

instance Halfspace.SetLike {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] :

_root_.SetLike (Halfspace E) E

Equations

Halfspace.SetLike = { coe := Halfspace.S, coe_injective := ⋯ }

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

↑H_ = ⇑↑H_.f ⁻¹' {x : ℝ | x ≤ H_.α}

The coercion of a halfspace to a set equals the sublevel preimage of its functional.

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

x ∈ ↑H_ ↔ ↑H_.f x ≤ H_.α

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

Convex ℝ ↑H_

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

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

affineSpan ℝ ↑H_ = ⊤

noncomputable def halfspaceTranslation {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) (H_ : Halfspace E) :

The halfspace H_ translated by the vector x.

Equations

halfspaceTranslation x H_ = { f := H_.f, α := H_.α + ↑H_.f x }

Instances For

theorem halfspaceTranslation.S {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : E) (H_ : Halfspace E) :

↑(halfspaceTranslation x H_) = (fun (x_1 : E) => x_1 + x) '' ↑H_

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

y ∈ ↑(halfspaceTranslation x H_) ↔ y - x ∈ ↑H_

theorem halfspaceTranslation.injective {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (x : E) :

Function.Injective fun (x_1 : Halfspace E) => halfspaceTranslation x x_1

theorem frontierHalfspace_Hyperplane {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {Hi_ : Halfspace E} :

frontier ↑Hi_ = {x : E | ↑Hi_.f x = Hi_.α}

theorem Hyperplane_convex {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Hi_ : Halfspace E) :

Convex ℝ {x : E | ↑Hi_.f x = Hi_.α}

theorem Hyperplane_affineClosed {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (Hi_ : Halfspace E) (s : Fin n → E) :

Set.range s ⊆ {x : E | ↑Hi_.f x = Hi_.α} → ∀ (a : Fin n → ℝ), Finset.univ.sum a = 1 → (Finset.affineCombination ℝ Finset.univ s) a ∈ {x : E | ↑Hi_.f x = Hi_.α}

theorem Halfspace.val_raw {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : Subspace ℝ E) [CompleteSpace ↥p] (H_' : Halfspace ↥p) :

∃ (H_ : Halfspace E), ((∀ (x : ↥p), ↑H_.f ↑x = ↑H_'.f x) ∧ ‖↑H_.f‖ = ‖↑H_'.f‖) ∧ H_.α = H_'.α

noncomputable def Halfspace.val {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : Subspace ℝ E) [CompleteSpace ↥p] (H_' : Halfspace ↥p) :

A halfspace of the subspace p extended to a halfspace of the whole space E.

Equations

Halfspace.val p H_' = (fun (H_ : Halfspace E) (x : ((∀ (x : ↥p), ↑H_.f ↑x = ↑H_'.f x) ∧ ‖↑H_.f‖ = ‖↑H_'.f‖) ∧ H_.α = H_'.α) => H_) (Classical.choose ⋯) ⋯

Instances For

theorem Halfspace.val_f {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : Subspace ℝ E) [CompleteSpace ↥p] (H_' : Halfspace ↥p) (x : ↥p) :

↑(val p H_').f ↑x = ↑H_'.f x

theorem Halfspace.val_C {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : Subspace ℝ E) [CompleteSpace ↥p] (H_' : Halfspace ↥p) :

(val p H_').α = H_'.α

theorem Halfspace.val_eq {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : Subspace ℝ E) [CompleteSpace ↥p] (H_' : Halfspace ↥p) :

↑(val p H_') ∩ ↑p = Subtype.val '' ↑H_'

theorem Halfspace.val_eq' {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (p : Subspace ℝ E) [CompleteSpace ↥p] (H_' : Halfspace ↥p) :

(fun (H_ : Halfspace ↥p) => ↑(val p H_) ∩ ↑p) H_' = (fun (H_ : Set ↥p) => Subtype.val '' H_) ↑H_'