OAI/Combinatorics/HalvingLines/MassEstimates.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Spatial.radial_extrema_scale line 11
2. def OAI.PlanarHalving.Spatial.normalizeChart line 32
3. lemma OAI.PlanarHalving.Spatial.normalizeChart_symm line 36
4. lemma OAI.PlanarHalving.Spatial.normalizeChart_source line 40
5. lemma OAI.PlanarHalving.Spatial.normalizeChart_target line 46
6. lemma OAI.PlanarHalving.Spatial.normalizeChart_radial line 49
7. lemma OAI.PlanarHalving.Spatial.normalizeChart_scaleGood line 64
8. lemma OAI.PlanarHalving.Spatial.normalized_spatial_limit line 94
9. lemma OAI.PlanarHalving.Limits.exists_bounded_density_piece line 161
10. lemma OAI.PlanarHalving.Limits.positive_bounded_projection line 195
11. lemma OAI.PlanarHalving.Spatial.joint_of_asymptotic_continuity line 223
12. lemma OAI.PlanarHalving.Spatial.scaleGood_joint line 238
13. lemma OAI.PlanarHalving.Spatial.positive_localization line 273
14. lemma OAI.PlanarHalving.Spatial.integer_scale_parameters line 295
15. lemma OAI.PlanarHalving.Spatial.positive_spatial_witness line 316
16. abbrev OAI.PlanarHalving.Spatial.Cube line 394
17. def OAI.PlanarHalving.Spatial.encode line 395
18. def OAI.PlanarHalving.Spatial.decode line 396
19. lemma OAI.PlanarHalving.Spatial.continuous_encode line 399
20. lemma OAI.PlanarHalving.Spatial.measurable_decode line 403
21. lemma OAI.PlanarHalving.Spatial.decode_encode line 407
22. lemma OAI.PlanarHalving.Spatial.encode_injective line 413
23. lemma OAI.PlanarHalving.Spatial.support_spatial_graph line 417
24. lemma OAI.PlanarHalving.Spatial.volume_closedBall_point line 437
25. lemma OAI.PlanarHalving.Spatial.disk_bound_of_inverse_holder line 445