OAI/Geometry/Zonotope/Halfspaces.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiagonalZonotope.abs_single_difference line 13
2. lemma OAI.DiagonalZonotope.coordinate_difference_support line 24
3. theorem OAI.DiagonalZonotope.centered_eq_support_halfspaces line 40

   Source documentation

   Explicit coordinate tests suffice to recover the body from all support bounds.

   theorem centered_eq_support_halfspaces :
       (centered : Set (ι → ℝ)) =
         {x | ∀ u : ι → ℝ, (∑ i, u i * x i) ≤
           ((∑ i, |u i|) + |∑ i, u i|) / 2} := by
   …

   Mentions: OAI.DiagonalZonotope.centered