OAI/Geometry/ProjectionBodies/AffineCovariance.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PettyProjection.unitSegment_smul line 11
2. lemma OAI.PettyProjection.unitSegment_image line 17
3. lemma OAI.PettyProjection.unitSegment_zero line 24
4. lemma OAI.PettyProjection.segment_volume_support line 31
5. lemma OAI.PettyProjection.linearEquiv_nhds line 49
6. lemma OAI.PettyProjection.projection_support_linearEquiv line 55
7. lemma OAI.PettyProjection.adjoint_inverse_comp line 78
8. def OAI.PettyProjection.adjointEquiv line 89

   Source documentation

   Invertibility of the transpose uses the transpose of the inverse.

   def adjointEquiv (T : Space n ≃L[ℝ] Space n) : Space n ≃L[ℝ] Space n :=
   …

   Mentions: OAI.PettyProjection.Space

9. lemma OAI.PettyProjection.adjointEquiv_clm line 94
10. lemma OAI.PettyProjection.det_adjoint line 97
11. lemma OAI.PettyProjection.adjointEquiv_det line 104
12. theorem OAI.PettyProjection.projectionBody_linearEquiv line 118

    Source documentation

    The actual unpolarized projection body transforms by the determinant and inverse transpose, proved from orthogonal shadow volumes via segment addition.

    theorem projectionBody_linearEquiv (T : Space n ≃L[ℝ] Space n)
        {K : Set (Space n)} (hK : IsCompact K) (hc : Convex ℝ K) (h0 : K∈𝓝 (0:Space n)) :
        projectionBody (T '' K)=|LinearMap.det T.toLinearMap| • (adjointEquiv T.symm '' projectionBody K) := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.projectionBody, OAI.PettyProjection.adjointEquiv

13. lemma OAI.PettyProjection.projection_volume_linearEquiv line 139
14. lemma OAI.PettyProjection.projectionRatio_linearEquiv line 153
15. lemma OAI.PettyProjection.projectionBody_unitBall line 170
16. lemma OAI.PettyProjection.projectionRatio_unitBall line 189
17. theorem OAI.PettyProjection.ellipsoid_projectionRatio line 196

    Source documentation

    All affine ellipsoids, including arbitrary translates, attain equality.

    theorem ellipsoid_projectionRatio {n : ℕ} (hn : 2≤n) {K : Set (Space n)}
        (hK : IsEllipsoid K) : projectionRatio K=pettyConstant n := by
    …

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