OAI/Geometry/Zonotope/Volume.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DiagonalZonotope.cube_eq_pi line 15
2. lemma OAI.DiagonalZonotope.isCompact_cube line 20
3. lemma OAI.DiagonalZonotope.continuous_extrusionMap line 25
4. lemma OAI.DiagonalZonotope.isCompact_cell line 35
5. theorem OAI.DiagonalZonotope.volume_cube line 40
6. theorem OAI.DiagonalZonotope.volume_cell line 44
7. lemma OAI.DiagonalZonotope.volume_coordinate_hyperplane line 55
8. lemma OAI.DiagonalZonotope.volume_coordinate_diagonal line 59
9. lemma OAI.DiagonalZonotope.cell_pairwise_aedisjoint line 79
10. lemma OAI.DiagonalZonotope.cube_aedisjoint_cells line 85
11. theorem OAI.DiagonalZonotope.volume_zonotope line 93

    Source documentation

    Lebesgue volume of the actual cube-plus-diagonal zonotope.

    theorem volume_zonotope :
        volume (zonotope : Set (ι → ℝ)) = (Fintype.card ι : ℝ≥0∞) + 1 := by
    …

    Mentions: OAI.DiagonalZonotope.zonotope

12. theorem OAI.DiagonalZonotope.volume_centered line 103

    Source documentation

    Translation to the center does not change the computed volume.

    theorem volume_centered :
        volume (centered : Set (ι → ℝ)) = (Fintype.card ι : ℝ≥0∞) + 1 := by
    …

    Mentions: OAI.DiagonalZonotope.centered

13. theorem OAI.DiagonalZonotope.volume_zonotope_fin line 108