OAI/Probability/Subsphere/Geometry/MassBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubsphereCurrent.Weighted.weightedOnTest line 14
2. lemma OAI.SubsphereCurrent.Weighted.measurable_weightedOnTest line 18
3. lemma OAI.SubsphereCurrent.Weighted.weighted_control line 22
4. lemma OAI.SubsphereCurrent.Weighted.subspace_perpendicular line 46
5. lemma OAI.SubsphereCurrent.Weighted.weighted_cap line 59
6. lemma OAI.SubsphereCurrent.Weighted.radial_sphere line 71
7. lemma OAI.SubsphereCurrent.Weighted.weightedOnTest_le_one line 77
8. lemma OAI.SubsphereCurrent.Weighted.weighted_norm_le_one line 83
9. def OAI.SubsphereCurrent.Weighted.sphereDensity line 97
10. lemma OAI.SubsphereCurrent.Weighted.sphereDensity_integral line 100
11. lemma OAI.SubsphereCurrent.Weighted.sphereDensity_cap line 110
12. lemma OAI.SubsphereCurrent.Weighted.sphereDensity_le line 122
13. lemma OAI.SubsphereCurrent.Weighted.sphereDensity_finite line 131
14. lemma OAI.SubsphereCurrent.Weighted.sphereDensity_restrict_ball line 135
15. lemma OAI.SubsphereCurrent.Weighted.polynomialMass_weighted line 145
16. def OAI.SubsphereCurrent.Weighted.completeRoute line 156
17. lemma OAI.SubsphereCurrent.Weighted.completeRoute_ge line 167
18. lemma OAI.SubsphereCurrent.Weighted.measurable_completeRoute line 173
19. lemma OAI.SubsphereCurrent.Weighted.sample_mass_identity line 183
20. lemma OAI.SubsphereCurrent.Weighted.measurable_sample_mass line 205
21. lemma OAI.SubsphereCurrent.Weighted.routing_mixture_bound line 224
22. lemma OAI.SubsphereCurrent.Weighted.projection_sphere_integral line 253
23. lemma OAI.SubsphereCurrent.Weighted.sphereDensity_zero_of_mass_zero line 266
24. lemma OAI.SubsphereCurrent.Weighted.deterministic_sphere_routing line 278
25. lemma OAI.SubsphereCurrent.Weighted.sphere_routing_bound line 297