OAI/Geometry/BallPacking/Necessity/FramedCompactness.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.HasFrame line 33
2. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.centeredFrame line 36
3. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.frozenCoefficient line 39
4. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.centeredFrame_smooth line 44
5. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.centeredFrame_fderiv line 50
6. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.frozenCoefficient_smooth line 57
7. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.frozen_CR_equation line 62
8. def OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.frameConjugation line 74
9. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.frameConjugation_apply line 79
10. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.frozenCoefficient_fderiv line 84
11. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.frozen_CR_no_gradient_loss line 90
12. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.field_CR_no_gradient_loss line 157
13. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.rescaleMap_CR_I line 207
14. theorem OAI.HigherDimensionalBallPacking.Rigidity.FramedCR.field_C0_gradient_bound line 218
15. theorem OAI.HigherDimensionalBallPacking.Rigidity.holder_gradient_limit_C1 line 302
16. theorem OAI.HigherDimensionalBallPacking.Rigidity.exists_principal_threshold line 387
17. theorem OAI.HigherDimensionalBallPacking.Rigidity.smallCR_local_modulus line 406
18. theorem OAI.HigherDimensionalBallPacking.Rigidity.smallCR_C1_closure_threshold line 457
19. theorem OAI.HigherDimensionalBallPacking.Rigidity.locally_uniform_small_ball line 509