OAI/Geometry/BallPacking/Holder/NonlinearCR.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.ThirdHolderOn line 13
2. theorem OAI.HigherDimensionalBallPacking.Rigidity.thirdHolderOn_of_bounded_lipschitz line 17
3. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.HMap line 37
4. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.COne line 40
5. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBoundedDeriv line 43
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBoundedDeriv_value line 52
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBoundedDeriv_norm_le line 57
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.holder_norm_le_of_deriv_bounds line 65
9. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cValue line 76
10. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cDeriv line 77
11. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.c_hasFDerivAt line 79
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.c_differentiable line 82
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.c_fderiv line 85
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.c_value_bound line 88
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.c_deriv_bound line 89
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cValue_add line 91
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cValue_smul line 92
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.base_fderiv_bound line 100
19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose_differentiable line 108
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose_fderiv_bound line 113
21. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose line 124
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose_value line 130
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficient_differentiable line 134
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficient_fderiv_bound line 139
25. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficient line 151
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficient_value line 157
27. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superposeDeriv line 160
28. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superposeDeriv_value line 164
29. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.variation_differentiable line 169
30. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose_remainder_norm line 173
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.superpose_hasFDerivAt line 218
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapCLM_norm_le line 241
33. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapJet line 256
34. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapJet_value line 262
35. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapJet_deriv line 265
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.cValue_ext line 268
37. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapJet_norm_le line 279
38. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapJetBilinear line 298
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mapJetBilinear_value line 324
40. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBoundedCThree line 327
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBoundedCThree_value line 335
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.ofBoundedCThree_deriv line 338
43. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedHolder line 341
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedHolder_closed line 345
45. instance OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.(instance at line 353) line 353
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.mem_supportedHolder line 357
47. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficientValueAction line 389
48. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficientDerivAction line 393
49. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficientAction line 400
50. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficientAction_value line 408
51. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficientAction_deriv line 411
52. def OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel line 422
53. theorem OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_smooth line 424
54. theorem OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_norm line 430
55. theorem OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_fderiv line 442
56. theorem OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_fderiv_norm line 457
57. theorem OAI.HigherDimensionalBallPacking.Rigidity.smoothCauchyKernel_tendsto line 482
58. theorem OAI.HigherDimensionalBallPacking.Rigidity.compact_kernel_derivative_integral_zero line 506
59. theorem OAI.HigherDimensionalBallPacking.Rigidity.compact_kernel_convolution_fderiv line 525
60. theorem OAI.HigherDimensionalBallPacking.Rigidity.compact_kernel_convolution_cancel line 540
61. theorem OAI.HigherDimensionalBallPacking.Rigidity.compact_kernel_convolution_derivative_bound line 557