OAI/Geometry/ProjectionBodies/Normalization.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.smul_body line 11
2. lemma OAI.PettyProjection.translate_body line 17
3. lemma OAI.PettyProjection.isEllipsoid_linear_image line 24
4. lemma OAI.PettyProjection.isEllipsoid_translate line 33
5. lemma OAI.PettyProjection.isEllipsoid_smul line 42
6. lemma OAI.PettyProjection.ellipsoid_homothety line 46
7. def OAI.PettyProjection.normalizeBody line 53
8. lemma OAI.PettyProjection.normalizeBody_body line 55
9. lemma OAI.PettyProjection.normalizeBody_nhds line 58
10. lemma OAI.PettyProjection.normalizeBody_volume line 62
11. lemma OAI.PettyProjection.normalizeBody_ellipsoid line 67
12. lemma OAI.PettyProjection.measurePair_comm line 81
13. theorem OAI.PettyProjection.normalized_projection line 93

    Source documentation

    Main geometric estimate and equality rigidity at the natural volume normalization; both the input and the projection body remain nonsmooth.

    theorem normalized_projection {n : ℕ} (hn : 4≤ n) [NeZero n] {K : Set (Space n)}
        (hK : IsCompact K) (hc : Convex ℝ K) (h0 : K∈𝓝 (0:Space n))
        (hv : volume.real K=kappa n) :
        kappa (n-1)≤ normalizedVolume (projectionBody K) ∧
          (normalizedVolume (projectionBody K)=kappa (n-1) → IsEllipsoid K) := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.kappa, OAI.PettyProjection.normalizedVolume, OAI.PettyProjection.projectionBody, OAI.PettyProjection.IsEllipsoid

14. lemma OAI.PettyProjection.volumeReal_translate line 159
15. lemma OAI.PettyProjection.normalizedVolume_translate line 164
16. lemma OAI.PettyProjection.shadowVolume_translate line 168
17. lemma OAI.PettyProjection.projectionBody_translate line 180
18. lemma OAI.PettyProjection.projectionRatio_translate line 185
19. lemma OAI.PettyProjection.shadowVolume_smul line 189
20. lemma OAI.PettyProjection.projectionBody_smul line 202
21. lemma OAI.PettyProjection.projectionRatio_smul line 219
22. lemma OAI.PettyProjection.projectionRatio_normalized line 236
23. lemma OAI.PettyProjection.normalized_projection_ratio line 246
24. lemma OAI.PettyProjection.centered_projection_lower_bound line 261
25. theorem OAI.PettyProjection.projection_lower_bound line 274

    Source documentation

    No origin, symmetry, localness, or boundary smoothness hypothesis is used.

    theorem projection_lower_bound {n : ℕ} (hn : 4≤n) {K : Set (Space n)}
        (hK : IsConvexBody K) :
        pettyConstant n≤projectionRatio K ∧ (projectionRatio K=pettyConstant n → IsEllipsoid K) := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.IsConvexBody, OAI.PettyProjection.pettyConstant, OAI.PettyProjection.projectionRatio, OAI.PettyProjection.IsEllipsoid