FacetCover.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite-halfspace geometry underlying the visible-facet projection formula.

def OAI.ProjectionCounterexample.halfspaceBody line 21
Source documentation
A finite intersection of closed halfspaces.
```
def halfspaceBody (a : ι → V →ₗ[ℝ] ℝ) (b : ι → ℝ) : Set V :=
…
```
def OAI.ProjectionCounterexample.boundingFace line 25
Source documentation
The part of the body on the bounding hyperplane of inequality i.
```
def boundingFace (a : ι → V →ₗ[ℝ] ℝ) (b : ι → ℝ) (i : ι) : Set V :=
…
```
theorem OAI.ProjectionCounterexample.ray_reaches_visible_face line 29
Source documentation
Moving in a direction with a positive halfspace slope reaches a visible face.
```
theorem ray_reaches_visible_face (a : ι → V →ₗ[ℝ] ℝ) (b : ι → ℝ)
    {y u : V} (hy : y ∈ halfspaceBody a b) (hu : ∃ i, 0 < a i u) :
    ∃ (t : ℝ) (i : ι), 0 ≤ t ∧ 0 < a i u ∧
      y + t • u ∈ boundingFace a b i := by
…
```
Mentions: OAI.ProjectionCounterexample.halfspaceBody, OAI.ProjectionCounterexample.boundingFace

theorem OAI.ProjectionCounterexample.image_halfspaceBody_eq_visible_faces line 59

Source documentation

The projected body is covered by the projections of its visible faces.

theorem image_halfspaceBody_eq_visible_faces
    (a : ι → V →ₗ[ℝ] ℝ) (b : ι → ℝ) (q : V →ₗ[ℝ] W)
    {u : V} (hqu : q u = 0) (hu : ∃ i, 0 < a i u) :
    q '' halfspaceBody a b =
      ⋃ i : {i : ι // 0 < a i u}, q '' boundingFace a b i.1 := by
…

Mentions: OAI.ProjectionCounterexample.halfspaceBody, OAI.ProjectionCounterexample.boundingFace

theorem OAI.ProjectionCounterexample.visible_face_line_unique line 78
Source documentation
Two visible boundary points on the same line parallel to the direction coincide. This will put overlaps of projected visible faces in their common lower-dimensional face.
```
theorem visible_face_line_unique
    (a : ι → V →ₗ[ℝ] ℝ) (b : ι → ℝ)
    {i j : ι} {y z u : V} {t : ℝ}
    (hy : y ∈ boundingFace a b i) (hz : z ∈ boundingFace a b j)
    (hi : 0 < a i u) (hj : 0 < a j u) (hline : z = y + t • u) : z = y := by
…
```
Mentions: OAI.ProjectionCounterexample.boundingFace

theorem OAI.ProjectionCounterexample.image_visible_faces_inter line 97

Source documentation

Overlaps of visible-face shadows are precisely shadows of the face intersections.

theorem image_visible_faces_inter
    (a : ι → V →ₗ[ℝ] ℝ) (b : ι → ℝ) (q : V →ₗ[ℝ] W)
    {u : V} (hker : LinearMap.ker q = Submodule.span ℝ {u})
    {i j : ι} (hi : 0 < a i u) (hj : 0 < a j u) :
    (q '' boundingFace a b i) ∩ (q '' boundingFace a b j) =
      q '' (boundingFace a b i ∩ boundingFace a b j) := by
…

Mentions: OAI.ProjectionCounterexample.boundingFace