OAI/Geometry/Zonotope/Product.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DiagonalZonotope.euclideanProduct line 12

   Source documentation

   The two-block product of explicit Euclidean zonotopes.

   def euclideanProduct (n m : ℕ) (c : ℝ) : Set (EuclideanSpace ℝ (Fin (n + m))) :=
   …

2. lemma OAI.DiagonalZonotope.finAddEquivProd_apply line 16
3. lemma OAI.DiagonalZonotope.inner_finAdd line 22
4. lemma OAI.DiagonalZonotope.isCompact_euclideanProduct line 29
5. lemma OAI.DiagonalZonotope.convex_euclideanProduct line 35
6. lemma OAI.DiagonalZonotope.euclideanProduct_interior_nonempty line 39
7. theorem OAI.DiagonalZonotope.euclideanProduct_eq_halfspaces line 48

   Source documentation

   Product support is the sum of the two independently attainable supports.

   theorem euclideanProduct_eq_halfspaces (n m : ℕ) (c : ℝ) (hc : 0 < c) :
       euclideanProduct n m c =
         {x | ∀ u : EuclideanSpace ℝ (Fin (n + m)), ⟪u, x⟫ ≤ c *
           (support (WithLp.ofLp (EuclideanSpace.finAddEquivProd u).1) +
            support (WithLp.ofLp (EuclideanSpace.finAddEquivProd u).2))} := by
   …

   Mentions: OAI.DiagonalZonotope.euclideanProduct, OAI.DiagonalZonotope.support

8. theorem OAI.DiagonalZonotope.euclideanProduct_support_attained line 77