OAI/Combinatorics/HalvingLines/SpatialMass.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PlanarHalving.Spatial.UnitSphere line 11
2. instance OAI.PlanarHalving.Spatial.(instance at line 12) line 12
3. instance OAI.PlanarHalving.Spatial.(instance at line 13) line 13
4. def OAI.PlanarHalving.Spatial.radialU line 19
5. def OAI.PlanarHalving.Spatial.radialV line 21
6. lemma OAI.PlanarHalving.Spatial.unitSphere_param line 24
7. lemma OAI.PlanarHalving.Spatial.sphere_representation line 29
8. lemma OAI.PlanarHalving.Spatial.continuous_sphereValue line 36
9. lemma OAI.PlanarHalving.Spatial.radialU_attained line 43
10. lemma OAI.PlanarHalving.Spatial.radialV_attained line 57
11. lemma OAI.PlanarHalving.Spatial.radial_extrema_bounds line 71
12. lemma OAI.PlanarHalving.Spatial.radialV_pos line 80
13. lemma OAI.PlanarHalving.Spatial.continuousOn_radialU line 90
14. lemma OAI.PlanarHalving.Spatial.continuousOn_radialV line 105
15. def OAI.PlanarHalving.Spatial.rankCore line 126
16. lemma OAI.PlanarHalving.Spatial.rankCore_closed line 129
17. lemma OAI.PlanarHalving.Spatial.rankCore_ball line 131
18. lemma OAI.PlanarHalving.Spatial.rankCore_small line 142
19. lemma OAI.PlanarHalving.Spatial.radialCompare_extrema line 153
20. def OAI.PlanarHalving.Spatial.ScaleGood line 184
21. lemma OAI.PlanarHalving.Spatial.scaleGood_measurable line 189
22. lemma OAI.PlanarHalving.Spatial.exists_scaleGood line 238
23. lemma OAI.PlanarHalving.Spatial.exists_dyadicExponent_scaleGood line 266
24. lemma OAI.PlanarHalving.Spatial.positive_scaleGood line 284
25. lemma OAI.PlanarHalving.Spatial.radius_le_of_ball_subset_closedBall line 322
26. lemma OAI.PlanarHalving.Spatial.normalized_local_bounds line 328
27. lemma OAI.PlanarHalving.Spatial.scaleGood_iteration line 379