OAI/Geometry/BallPacking/Necessity/DensityLimits.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentCurveDir line 38
2. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentCurveDir_smooth line 41
3. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentCurveDir_fderiv line 46
4. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.tangentCurveDir_CR line 55
5. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.directional_second_convergence line 102
6. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.standardCurl line 131
7. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.standardCurl_smooth line 135
8. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.curlLinear line 141
9. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.curlLinear_apply line 147
10. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.standardCurl_convergence line 151
11. theorem OAI.HigherDimensionalBallPacking.Rigidity.density_tsupport_subset line 196
12. theorem OAI.HigherDimensionalBallPacking.Rigidity.density_compact_support line 204
13. def OAI.HigherDimensionalBallPacking.Rigidity.smoothCompactDensity line 208
14. theorem OAI.HigherDimensionalBallPacking.Rigidity.smoothCompactDensity_apply line 213
15. theorem OAI.HigherDimensionalBallPacking.Rigidity.density_fderiv_zero_exterior line 217
16. theorem OAI.HigherDimensionalBallPacking.Rigidity.density_locally_uniform_to_uniform line 226
17. theorem OAI.HigherDimensionalBallPacking.Rigidity.smoothCompactDensity_tendsto line 240
18. def OAI.HigherDimensionalBallPacking.Rigidity.affineHolderModuli line 288
19. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_density_common_support line 294
20. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineHolderModuli_isCompact line 310
21. theorem OAI.HigherDimensionalBallPacking.Rigidity.homotopy_affine_Holder_compactness line 353
22. def OAI.HigherDimensionalBallPacking.Rigidity.affineHomotopyModuli line 377
23. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineHomotopyModuli_isCompact line 381
24. def OAI.HigherDimensionalBallPacking.Rigidity.affineSolvableTimes line 397
25. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineSolvableTimes_eq_image line 400
26. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineSolvableTimes_isCompact line 409
27. theorem OAI.HigherDimensionalBallPacking.Rigidity.zero_mem_affineSolvableTimes line 419
28. theorem OAI.HigherDimensionalBallPacking.Rigidity.standard_affine_line_unique line 437
29. theorem OAI.HigherDimensionalBallPacking.Rigidity.affineHomotopyModuli_zero_fiber line 467