ProductZonotopeBridge.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ProjectionCounterexample.blockSupport line 13
Source documentation
The sum of the two block support functions, with a common scale.
```
def blockSupport {n m : ℕ} (u : E (n + m)) : ℝ :=
…
```
Mentions: OAI.ProjectionCounterexample.E
lemma OAI.ProjectionCounterexample.blockSupport_zero line 17
lemma OAI.ProjectionCounterexample.blockSupport_smul line 20
theorem OAI.ProjectionCounterexample.projectionBody_eq_productZonotope line 28
Source documentation
A proved block brightness formula identifies the product projection zonotope.
```
theorem projectionBody_eq_productZonotope {n m : ℕ} (P : Set (E (n + m)))
    (c : ℝ) (hc : 0 < c)
    (hbrightness : ∀ u : E (n + m), ‖u‖ = 1 → projectionVolume P u = c * blockSupport u) :
    projectionBody P = DiagonalZonotope.euclideanProduct n m c := by
…
```
Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.projectionVolume, OAI.ProjectionCounterexample.blockSupport, OAI.ProjectionCounterexample.projectionBody, OAI.DiagonalZonotope.euclideanProduct
theorem OAI.ProjectionCounterexample.projection_productZonotope_is_body_and_attains line 53
Source documentation
Body structure and attained orthogonal-projection support values for a block formula.
```
theorem projection_productZonotope_is_body_and_attains {n m : ℕ}
    (P : Set (E (n + m))) (c : ℝ) (hc : 0 < c)
    (hbrightness : ∀ u : E (n + m), ‖u‖ = 1 → projectionVolume P u = c * blockSupport u) :
    IsConvexBody (projectionBody P) ∧
      ∀ u : E (n + m), ‖u‖ = 1 → ∃ x ∈ projectionBody P, ⟪u, x⟫ = projectionVolume P u := by
…
```
Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.projectionVolume, OAI.ProjectionCounterexample.blockSupport, OAI.ProjectionCounterexample.IsConvexBody, OAI.ProjectionCounterexample.projectionBody