OAI/Probability/ProjectionMoments/BallMoments.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionMoments.rowMap_ac_iff line 16
2. lemma OAI.ProjectionMoments.measurableSet_projection_ac line 30
3. lemma OAI.ProjectionMoments.polar_ac_to_frame line 39
4. lemma OAI.ProjectionMoments.unitBallVolume_ne_zero line 49
5. lemma OAI.ProjectionMoments.unitBallVolume_ne_top line 52
6. instance OAI.ProjectionMoments.unitBallLaw_probability line 54
7. lemma OAI.ProjectionMoments.unitBallVolume_bound line 60
8. lemma OAI.ProjectionMoments.measurable_normalizedDensity line 65
9. lemma OAI.ProjectionMoments.normalizedDensity_support line 70
10. lemma OAI.ProjectionMoments.normalizedDensity_is_density line 77
11. lemma OAI.ProjectionMoments.normalizedMoment_le line 89
12. lemma OAI.ProjectionMoments.sphereWeightedRestriction_le line 116
13. lemma OAI.ProjectionMoments.sphereWeightedRestriction_finite line 125
14. lemma OAI.ProjectionMoments.sphereWeightedRestriction_support line 129
15. theorem OAI.ProjectionMoments.riesz_deterministic_offsets line 135
16. theorem OAI.ProjectionMoments.all_radii_sphere_moment line 194
17. lemma OAI.ProjectionMoments.normalized_cost line 241
18. theorem OAI.ProjectionMoments.normalized_unitBall_moment line 291