OAI/Geometry/Zonotope/Scaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiagonalZonotope.coordinate_pairing_smul line 13
2. lemma OAI.DiagonalZonotope.support_value_smul line 23
3. theorem OAI.DiagonalZonotope.scaled_centered_eq_support_halfspaces line 30

   Source documentation

   Positive scalar images of the centered zonotope have the scaled support inequalities.

   theorem scaled_centered_eq_support_halfspaces (c : ℝ) (hc : 0 < c) :
       (fun y : ι → ℝ => c • y) '' centered =
         {x | ∀ u : ι → ℝ, (∑ i, u i * x i) ≤
           c * (((∑ i, |u i|) + |∑ i, u i|) / 2)} := by
   …

   Mentions: OAI.DiagonalZonotope.centered

4. lemma OAI.DiagonalZonotope.scaled_centered_support_attained line 51