OAI/Geometry/BallPacking/Fredholm/TranslationContinuity.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bilinear_tendsto_zero_of_bounded line 15
2. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationError line 37
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationError_value line 43
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translation_second_factor_bound line 48
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationError_tendsto line 55
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translation_CR_algebra line 65
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeTranslation_principal_near line 85
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeTranslation_principal_tendsto line 102
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.elliptic_freeTranslation_continuous line 113
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineCurve_translation line 140
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineCurve_translation_fderiv line 147
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineCurve_translation_CR line 155
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeChart_zero_of_CR line 173
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeChart_translation_zero_near line 189
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.source_smooth_of_translation line 204
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affine_free_norm_lower line 244
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.exists_free_escape_radius line 259
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeModel_mono line 275
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeModel_of_elliptic line 282
20. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.FreeEscapeNeighborhood line 305
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeEscape_of_radius line 310
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.nonlinear_stabilized_regularity line 327
23. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.regularityTranslation line 390
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.regularityTranslation_zero line 393
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.regularityTranslation_near line 396
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.regularityTranslation_continuous line 401
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.regularityTranslation_smooth line 415
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completed_free_source_contDiff line 436
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.marked_escape_base line 469
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedChart_derivative_eq_linearized line 477
31. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedDerivative line 490
32. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.IsIndexZeroFredholm line 492
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedChart_derivative_fredholm line 497
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedHolder_mono line 526
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedModel_mono line 533
36. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.widenMarked line 538
37. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.MarkedEscapeNeighborhood line 541
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedEscape_of_uniform line 547
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.exists_chart_escape_neighborhood line 556
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.realCR_axis_implies_all line 575
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedChart_zero_pseudoholomorphic line 606
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedMarkedCurve_contDiff_one line 619
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedMarkedCurve_marks line 624
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedMarkedCurve_asymptote line 633
45. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completed_markedCurve_contDiff line 651
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedChart_zero_affineLine line 678
47. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricResidual line 706
48. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricResidual_smooth line 709
49. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricResidual_compact line 717
50. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.inverse_correction_holomorphic line 730
51. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.inverse_correction_asymptote line 752
52. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affine_reconstruction_from_correction line 762
53. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.marked_reconstruction_from_correction line 772
54. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.affineLineCurve_completed_representation line 790