OAI/Geometry/BallPacking/Compactness/FrozenCR.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenTargetCoefficient line 15
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenTargetCoefficient_zero line 19
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenTargetCoefficient_continuous line 24
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenTargetCoefficient_difference line 28
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenTargetCoefficient_lipschitz line 37
6. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenCurve line 56
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenCurve_smooth line 59
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenCurve_fderiv line 63
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frozenCurve_CR line 68
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_joint_contDiffAt line 96
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_slice_contDiff line 102
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_partial_deriv line 109
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.lineHomotopy_eventually_standard line 118
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.compatibleFrame_contDiffAt line 128
15. theorem OAI.HigherDimensionalBallPacking.Rigidity.exact_homotopy_target_bounds line 134
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.frozenHomotopy_joint_contDiffAt line 195
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.frozenHomotopy_tendstoUniformlyOn line 218
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.exact_frame_tendsto line 240
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.weighted_gradient_selection line 258
20. def OAI.HigherDimensionalBallPacking.Rigidity.rescaledCurve line 303
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.rescaledCurve_smooth line 305
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.rescaledCurve_fderiv line 308
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.rescaledCurve_CR line 317
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.rescaledCurve_source_dist line 327
25. theorem OAI.HigherDimensionalBallPacking.Rigidity.equicontinuous_CR_derivative_bound line 330
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.uniform_values_cauchy_on line 434
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.uniform_clm_cauchy_on line 444
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.centered_rescaled_cauchy line 469