OAI/Geometry/BallPacking/Fredholm/FrameFredholm.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.framedJetPrincipal_add_compact_fredholm line 34
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compactPerturbation_of_outside_constant line 67
3. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedStructureJet line 92
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedStructureJet_value line 96
5. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedFrameJet line 99
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedFrameJet_value line 105
7. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedInverseJet line 108
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedInverseJet_value line 114
9. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedPrincipal line 123
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedPrincipal_value line 127
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.completedPrincipal_add_compact_fredholm line 132
12. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedFieldAction line 167
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedFieldAction_value line 176
14. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedEval line 180
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedEval_value line 184
16. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedFiniteCorrection line 187
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedFiniteCorrection_value line 192
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedFiniteCorrection_isCompact line 197
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fderiv_standard_outside line 221
20. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveZeroOrder line 230
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveZeroOrder_apply line 233
22. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveMarkCoefficient line 236
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveMarkCoefficient_apply line 239
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveZeroOrder_smooth line 243
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveMarkCoefficient_smooth line 251
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveZeroOrder_zero_outside line 267
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveMarkCoefficient_zero_outside line 275
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveZeroOrder_compact line 281
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveMarkCoefficient_compact line 288
30. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveZeroOrderHolder line 294
31. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveMarkCoefficientHolder line 298
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveZeroOrderHolder_value line 302
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.curveMarkCoefficientHolder_value line 305
34. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricZeroOrder line 308
35. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricMarkCorrection line 312
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricZeroOrder_compact line 316
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricMarkCorrection_compact line 319
38. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricLinearized line 322
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricLinearized_value line 326
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.geometricLinearized_fredholm line 339
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.exists_escape_radii line 357
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.exists_uniform_escape line 375
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compact_coefficient_truncated line 390
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compact_coefficient_zero_outside line 404
45. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedDX line 432
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedDX_value line 436
47. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedDX_contDiff line 443
48. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncatedCoefficient line 453
49. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncatedCoefficient_value line 457
50. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncatedCoefficient_contDiff line 461
51. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.chartNonlinearity line 469
52. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.chartNonlinearity_value line 473
53. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.chartNonlinearity_contDiff line 479
54. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedChart line 489
55. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedChart_contDiff line 493
56. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedChart_value line 502
57. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoff_action_eq line 511
58. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedChart_actual_value line 525