OAI/Probability/ProjectionMoments/SphereDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionMoments.measurable_coordinateMap line 14
2. def OAI.ProjectionMoments.projectionKernel line 21
3. instance OAI.ProjectionMoments.projectionKernel_finite line 34
4. lemma OAI.ProjectionMoments.projectionKernel_compProd line 41
5. lemma OAI.ProjectionMoments.ae_projection_ac line 57
6. lemma OAI.ProjectionMoments.sphere_ae_projection_ac line 69
7. lemma OAI.ProjectionMoments.linearEquiv_preserves_ac line 83
8. lemma OAI.ProjectionMoments.sphere_projection_rotation line 89
9. theorem OAI.ProjectionMoments.sphere_frame_ac line 98
10. theorem OAI.ProjectionMoments.sphere_fullRank_ac line 117