OAI/Geometry/BallPacking/Compactness/JetCauchy.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cauchy_coefficient_action line 22
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoff_forcing_holder_cauchy line 33
3. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoff_jet_cauchy line 44
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.common_small_value_scale line 97
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCurveJet_deriv_zero line 108
6. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bounded_cutoff_gradient_small line 115
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.smooth_cutoff_local_bounds line 175
8. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.local_nonlinear_gradient_small line 217
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.uniform_cauchy_comp_lipschitz line 273
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoff_uniform_cauchy line 297
11. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.smallDiskBump line 313
12. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.largerDiskBump line 314
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.double_disk_cutoff line 317
14. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.disk_nonlinear_jet_cauchy line 335
15. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame line 417
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_apply line 419
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_intertwine line 423
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_invertible line 428
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_standard line 431
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_smooth line 438
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_inverse_smooth line 444
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_inverse_left line 452
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_inverse_right line 459
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_inverse_standard line 466
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_compactPerturbation line 483
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrame_inverse_compactPerturbation line 493
27. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrameJet line 502
28. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleInverseJet line 506
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrameJet_value line 510
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleInverseJet_value line 513
31. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleMarkedEquiv line 516
32. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleResidualEquiv line 524