OAI/Geometry/BallPacking/Holder/BanachSpace.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.Pairs line 14
2. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.Ambient line 16
3. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.graph line 18
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.graph_closed line 34
5. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.Holder line 44
6. instance OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.(instance at line 46) line 46
7. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.valueCLM line 51
8. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.incrementCLM line 54
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.valueCLM_apply line 59
10. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.incrementCLM_apply line 62
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.increment_eq line 65
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.value_norm_le line 69
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.increment_norm_le line 72
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.norm_value_le line 75
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.norm_increment_le line 78
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.norm_sub_value_le line 82
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.value_ext line 95
18. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBound line 104
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBound_value line 128
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBound_norm_le line 133
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.norm_le_of_bounds line 150
22. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapCLM line 164
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapCLM_value line 172
24. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.const line 175
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.const_value line 178
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.const_norm_le line 180
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bilin_sub_bound line 191
28. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bilin line 216
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bilin_value line 225
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bilin_norm line 229
31. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bilinCLM line 237
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.bilinCLM_value line 268
33. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.JetAmbient line 276
34. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetGraph line 278
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetGraph_closed line 290
36. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.COneHolder line 301
37. instance OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.(instance at line 303) line 303
38. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetValueCLM line 308
39. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetDerivCLM line 311
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.hasFDerivAt line 314
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.contDiff_one line 318
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetValue_norm_le line 327
43. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jetDeriv_norm_le line 330
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jet_norm_value_le line 333
45. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.jet_norm_deriv_le line 337
46. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedJets line 341
47. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedJets_closed line 345
48. instance OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.(instance at line 354) line 354
49. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mem_markedJets line 358
50. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.norm_sub_le_of_deriv_bound line 373
51. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.taylor_remainder_quadratic line 379
52. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.hasFDerivAt_of_quadratic_remainder line 395
53. structure OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree line 409
54. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.boundedCThree_of_compactSupport line 416
55. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.add_const line 436
56. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.boundedCThree_of_compactPerturbation line 449
57. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.bound line 457
58. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.bound_nonneg line 459
59. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.norm_le line 462
60. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.norm_fderiv_le line 465
61. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.norm_fderiv₂_le line 468
62. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.norm_fderiv₃_le line 472
63. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.fderiv_smooth line 476
64. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.fderiv₂_smooth line 479
65. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.norm_sub_le line 482
66. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.norm_fderiv_sub_le line 486
67. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.norm_fderiv₂_sub_le line 490
68. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.remainder_bound line 494
69. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.BoundedCThree.fderiv_remainder_bound line 499
70. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.fderiv_composed_remainder line 510
71. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.norm_fderiv_composed_remainder line 537