OAI/Geometry/BallPacking/Necessity/GlobalArea.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_one line 37
2. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_le_one line 45
3. theorem OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_mono line 53
4. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffCurl line 64
5. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCurl_integrable line 67
6. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCurl_stokes line 73
7. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCurl_bounds line 84
8. theorem OAI.HigherDimensionalBallPacking.Rigidity.tendsto_integral_cutoffCurl line 124
9. theorem OAI.HigherDimensionalBallPacking.Rigidity.integral_planarCurl_of_nonneg_of_angular_limit line 156
10. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.total_radial_area line 207
11. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_primitive_angular_limit_zero line 226
12. theorem OAI.HigherDimensionalBallPacking.Rigidity.affine_sphere_constant line 272
13. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_common_radial_interval line 321
14. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_lines_have_common_unit_area line 347
15. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_pole_infinity_curve line 363
16. theorem OAI.HigherDimensionalBallPacking.Rigidity.normalizedPrimitive_pole_angular_limit line 386
17. theorem OAI.HigherDimensionalBallPacking.Rigidity.pole_norm_tendsto line 427
18. theorem OAI.HigherDimensionalBallPacking.Rigidity.pole_radial_area line 449