OAI/Probability/ProjectionMoments/Caps.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ProjectionMoments.sphere_packing_annulus line 15
2. lemma OAI.ProjectionMoments.sphere_packing_bound line 75
3. lemma OAI.ProjectionMoments.sphere_cap_mass_center line 115
4. lemma OAI.ProjectionMoments.sphere_finite_net line 132
5. lemma OAI.ProjectionMoments.sphere_cap_lower_one line 146
6. lemma OAI.ProjectionMoments.sphere_cap_lower line 184
7. lemma OAI.ProjectionMoments.cap_mass_pos line 217
8. lemma OAI.ProjectionMoments.capMeasure_probability line 224
9. lemma OAI.ProjectionMoments.capMeasure_ac line 230
10. lemma OAI.ProjectionMoments.capMeasure_support line 233
11. lemma OAI.ProjectionMoments.reciprocal_scale line 239
12. lemma OAI.ProjectionMoments.exists_capDictionary line 257