OAI/Geometry/BallPacking/Fredholm/FreeLinearization.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedFreePrincipal line 37
2. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedFreeLinearized line 41
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedFreePrincipal_fredholm line 46
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedFreeLinearized_fredholm line 54
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedFreeLinearized_value line 63
6. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualStructureBound line 75
7. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualFreeChart line 91
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualFreeChart_contDiff line 93
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.free_escape_base line 98
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualFreeChart_crSection_fderiv_eval line 107
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedFreeLinearized_crSection line 118
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualFreeChart_fderiv_eval line 133
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualFreeChart_fderiv_eq line 141
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualFreeChart_fderiv_fredholm line 152
15. theorem OAI.HigherDimensionalBallPacking.Rigidity.compact_test_translation_smooth line 164
16. theorem OAI.HigherDimensionalBallPacking.Rigidity.finite_separating_family line 186
17. theorem OAI.HigherDimensionalBallPacking.Rigidity.fredholm_stabilized_leftInverse line 221
18. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.PlaneTest line 252
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.planeTest_integrable line 255
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.planeTest_norm_bound line 260
21. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.planeTestCLM line 273
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.planeTest_separates line 285
23. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTestCLM line 299
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTest_value line 302
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTest_separates line 305
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTest_translation_smooth line 311
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetTest_translation_difference_smooth line 316
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.finite_jet_tests line 321
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.observed_fredholm_leftInverse line 342
30. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetObservations line 369
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetObservations_translation_smooth line 373
32. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.subspaceObservations line 383
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.exists_jet_fredholm_observations line 386
34. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationVariation line 411
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationVariation_value line 415
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationVariation_deriv line 419
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationVariation_zero line 425
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationVariation_CR line 431
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationVariation_mem line 437
40. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeTranslation line 461
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeTranslation_near line 464
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeTranslation_zero line 469
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.translationVariation_observation_smooth line 475
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeTranslation_observation_smoothAt line 489