OAI/Geometry/BallPacking/Holder/MarkedFrame.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficientDeriv_zero_outside line 21
2. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficientAction_mem_marked line 32
3. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCoefficientAction line 60
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCoefficientAction_value line 66
5. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holderCoefficientAction line 71
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holderCoefficientAction_value line 75
7. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCoefficientAction line 78
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCoefficientAction_value line 86
9. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCoefficientEquiv line 90
10. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCoefficientEquiv line 105
11. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.complexSlopeCLM line 126
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.complexSlopeCLM_apply line 130
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCoordinate_smooth line 134
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCoordinate_compact line 136
15. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCoordinate line 139
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffCoordinate_value line 142
17. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffSlope line 144
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cutoffSlope_value line 148
19. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncateShift line 153
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncateShift_value line 157
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedSlope_add line 163
22. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncatedCurve line 168
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncatedCurve_value line 172
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncatedCurve_eq_marked line 179
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cValue_norm_le line 187
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.truncatedCurve_norm_lower line 191
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedCurve_norm_lower line 216
28. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.constHolderCLM line 244
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.constHolderCLM_value line 251
30. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bumpHolder line 255
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bumpHolder_value line 258
32. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.sourceCutoff line 260
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.sourceCutoff_value line 263
34. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedSourceCutoff line 269
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedSourceCutoff_value line 277
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.third_interpolation line 289
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.exists_small_third_scale line 314
38. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holder_small_of_small_value line 325
39. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.lipHolderSet line 341
40. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.restrictedValue line 346
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.restrictedValue_apply line 349
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.restrictedValue_uniformInducing line 352
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.lipHolderSet_totallyBounded line 383
44. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.localizedJetValue line 418
45. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.localizedJetValue_apply line 421
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.localizedJetValue_bounds line 424
47. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.localizedJetValue_isCompact line 463