OAI/Geometry/Zonotope/EuclideanVolume.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiagonalZonotope.volume_scaled_centered line 14
2. theorem OAI.DiagonalZonotope.volume_euclidean line 21

   Source documentation

   The coordinate calculation gives actual Euclidean Lebesgue volume.

   theorem volume_euclidean (c : ℝ) (hc : 0 ≤ c) :
       volume (euclidean c : Set (EuclideanSpace ℝ ι)) =
         ENNReal.ofReal (c ^ Fintype.card ι) * ((Fintype.card ι : ℝ≥0∞) + 1) := by
   …

   Mentions: OAI.DiagonalZonotope.euclidean

3. lemma OAI.DiagonalZonotope.finAdd_measurePreserving line 32
4. theorem OAI.DiagonalZonotope.volume_euclideanProduct line 40

   Source documentation

   The block product has the product of its two Euclidean volumes.

   theorem volume_euclideanProduct (n m : ℕ) (c : ℝ) (hc : 0 ≤ c) :
       volume (euclideanProduct n m c) =
         (ENNReal.ofReal (c ^ n) * ((n : ℝ≥0∞) + 1)) *
         (ENNReal.ofReal (c ^ m) * ((m : ℝ≥0∞) + 1)) := by
   …

   Mentions: OAI.DiagonalZonotope.euclideanProduct

5. theorem OAI.DiagonalZonotope.volume_euclidean_toReal line 52

   Source documentation

   Real-valued Euclidean volume for the normalized-ratio calculation.

   theorem volume_euclidean_toReal (c : ℝ) (hc : 0 ≤ c) :
       (volume (euclidean c : Set (EuclideanSpace ℝ ι))).toReal =
         c ^ Fintype.card ι * ((Fintype.card ι : ℝ) + 1) := by
   …

   Mentions: OAI.DiagonalZonotope.euclidean

6. theorem OAI.DiagonalZonotope.volume_euclideanProduct_toReal line 59

   Source documentation

   Real-valued volume of the two-block product.

   theorem volume_euclideanProduct_toReal (n m : ℕ) (c : ℝ) (hc : 0 ≤ c) :
       (volume (euclideanProduct n m c)).toReal =
         c ^ (n + m) * (((n : ℝ) + 1) * ((m : ℝ) + 1)) := by
   …

   Mentions: OAI.DiagonalZonotope.euclideanProduct