OAI/Geometry/BallPacking/Continuation/CompatibleHomotopy.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.compatible_interpolateJ_initial line 16
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.interpolateJ_standard_initial line 35
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.contDiffAt_interpolateJ_initial line 51
4. def OAI.HigherDimensionalBallPacking.Rigidity.initialTime line 70
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialTime_range line 71
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialTime_smooth line 73
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialTime_zero line 74
8. def OAI.HigherDimensionalBallPacking.Rigidity.initialTimeBump line 76
9. def OAI.HigherDimensionalBallPacking.Rigidity.initialCoefficient line 78
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialCoefficient_smooth line 84
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialCoefficient_zero line 92
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialCoefficient_compact line 95
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialCoefficient_outside line 112
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialCoefficient_near line 117
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.initialCoefficient_compatible_near line 127
16. def OAI.HigherDimensionalBallPacking.Rigidity.fullTime line 140
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullTime_range line 141
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullTime_smooth line 143
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullTime_zero line 147
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullTime_one line 148
21. def OAI.HigherDimensionalBallPacking.Rigidity.fullTimeBump line 150
22. def OAI.HigherDimensionalBallPacking.Rigidity.fullCoefficient line 151
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullCoefficient_smooth line 156
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullCoefficient_zero line 166
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullCoefficient_compact line 169
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullCoefficient_outside line 188
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullCoefficient_exact line 194
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.fullCoefficient_compatible line 204
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compact_marked_bounds line 219
30. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedBoundedDomain line 232
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedBoundedDomain_open line 236
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedBoundedDomain_slope line 241
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bounded_marked_uniform_escape line 246
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bounded_marked_escape_neighborhood line 271
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.marked_escape_neighborhood_base line 280
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.normed_t2 line 294
37. def OAI.HigherDimensionalBallPacking.Rigidity.fullMarkedZeroSet line 303
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.full_marked_compact_of_exact line 306
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.full_marked_zeroSet_compact line 323
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.exact_marked_common_neighborhood line 327
41. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.realConstantJet line 382
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.realConstantJet_value line 384
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.realConstantJet_norm line 385
44. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.realConstantJetCLM line 390
45. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.parameterJet line 417
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.parameterJet_value line 425
47. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.parameterSlope line 430
48. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.parameterCoefficient line 435
49. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.parameterCoefficient_value line 439
50. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.parameterCoefficient_contDiff line 450
51. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalMarkedJet line 467
52. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalMarkedJet_contDiff line 471
53. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalMarkedJet_value line 477
54. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalMarkedJet_eq_marked line 482
55. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalParameterJet line 488
56. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalParameterJet_contDiff line 493
57. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalParameterJet_value line 506
58. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.global_zero_derivative_bound line 512
59. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalCoefficient line 516
60. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalCoefficient_value line 520
61. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.globalCoefficient_contDiff line 525