OAI/Geometry/BallPacking/Compactness/AffineCorrectionInfinity.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.analyticAt_dslope_zero line 14
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.infinityGerm_affine_reconstruction line 19
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.analytic_inverse_angular_fderiv_limit line 26
4. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.affine_correction_at_infinity line 54
5. def OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection line 63
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection_smooth line 65
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection_locally_inverse line 68
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection_limit line 75
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection_angular_fderiv_limit line 84
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.affineCorrection_primitive_flux_zero line 92
11. def OAI.HigherDimensionalBallPacking.Rigidity.defectEnergy line 114
12. def OAI.HigherDimensionalBallPacking.Rigidity.symplecticEnergy line 117
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.defectEnergy_nonneg line 119
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.defectEnergy_standard line 121
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.defectEnergy_smul line 124
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.symplecticEnergy_smul line 129
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.symplecticEnergy_pos line 134
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.defectEnergy_continuous line 139
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.symplecticEnergy_continuous line 144
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.energyRatio_continuousOn line 147
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.energyRatio_bounded_on_sphere line 162
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.energyRatio_extend_from_sphere line 180
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.exists_defectEnergy_bound line 198
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.outerProfile_one_before line 215
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.radiusSq_pos_bound_of_compact line 222
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.integral_compact_le_infinity_flux line 231
27. theorem OAI.HigherDimensionalBallPacking.Rigidity.AffineLineCurve.compact_density_mass_le_one line 287
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.entire_affine_of_asymptote line 311
29. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holderTranslate line 344
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holderTranslate_value line 352
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holderTranslate_norm_le line 356
32. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTranslate line 362
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTranslate_value line 369
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTranslate_deriv line 372
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTranslate_norm_le line 375
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cValue_norm_diff_le line 380
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translate_value_norm line 386
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translate_value_lipschitz line 391
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetValue_translate_tendsto line 401