OAI/Geometry/BallPacking/Fredholm/PointwiseMarkedCR.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedDerivEval line 27
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedDerivEval_value line 32
3. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedVariation line 35
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedVariation_value line 39
5. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedDerivativeVariation line 42
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedDerivativeVariation_value line 46
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_variation line 50
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_derivative_variation line 56
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_model_hasFDerivAt line 72
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_derivative_model_hasFDerivAt line 85
11. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.pointMarkedCR line 99
12. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.pointMarkedCRDeriv line 104
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.pointMarkedCR_hasFDerivAt line 111
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.pointMarkedCRDeriv_value line 126
15. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedDStructure line 158
16. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedDX line 163
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedDX_value line 166
18. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedQ line 172
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedQ_value line 177
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedQ_zero_outside line 190
21. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedMarkHolder line 202
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedMarkHolder_value line 209
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedMarkHolder_zero_outside line 225
24. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedZeroOrder line 237
25. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedMarkCorrection line 240
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedZeroOrder_compact line 245
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedMarkCorrection_compact line 248
28. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedLinearized line 251
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedLinearized_value line 255
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedLinearized_fredholm line 279
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fredholm_from_coordinates line 298
32. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freePrincipal line 335
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freePrincipal_value line 338
34. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeZeroOrder line 344
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeZeroOrder_value line 352
36. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.constantZeroOrder line 355
37. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeLinearized line 362
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeLinearized_coords line 365
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeLinearized_fredholm line 390
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freePrincipal_fredholm line 400
41. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedEval line 422
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedEval_value line 427
43. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactJPerturbation line 434
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactJPerturbation_smooth line 436
45. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactJPerturbation_compact line 439
46. theorem OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactJPerturbationBound line 452
47. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactJPerturbation_outside line 456
48. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedChart line 473
49. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedChart_contDiff line 475
50. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedChart_value line 478
51. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.actualMarkedChart_fderiv_eval line 492
52. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeChart line 534
53. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeChart_contDiff line 540
54. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeChart_value line 551
55. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.crSection_value_of_standard line 558
56. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoff_residual_algebra line 568
57. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeChart_true_value line 574
58. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.freeChart_hasFDerivAt_eval line 588