OAI/Geometry/BallPacking/Necessity/KernelMoments.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HigherDimensionalBallPacking.Rigidity.kernelMomentOne line 23
2. def OAI.HigherDimensionalBallPacking.Rigidity.kernelMomentTwo line 25
3. lemma OAI.HigherDimensionalBallPacking.Rigidity.weightedKernel_integrable line 28
4. lemma OAI.HigherDimensionalBallPacking.Rigidity.kernelMomentOne_nonneg line 34
5. lemma OAI.HigherDimensionalBallPacking.Rigidity.kernelMomentTwo_nonneg line 36
6. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactKernel_schauder_first line 39
7. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactKernel_directional_eq line 61
8. lemma OAI.HigherDimensionalBallPacking.Rigidity.kernelMomentOne_directional_le line 68
9. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactKernel_schauder_second line 97
10. def OAI.HigherDimensionalBallPacking.Rigidity.scaledKernelPotential line 130
11. def OAI.HigherDimensionalBallPacking.Rigidity.scaledKernelDerivative line 133
12. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledKernel_hasFDerivAt line 137
13. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaled_holder_bound line 156
14. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledKernel_derivative_bound line 163
15. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledKernel_derivative_lipschitz line 173
16. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledKernel_value_bound line 186
17. lemma OAI.HigherDimensionalBallPacking.Rigidity.eighth_rpow_third line 202
18. lemma OAI.HigherDimensionalBallPacking.Rigidity.eighth_scale_lipschitz line 208
19. def OAI.HigherDimensionalBallPacking.Rigidity.annularCauchyKernel line 219
20. lemma OAI.HigherDimensionalBallPacking.Rigidity.annularCauchyKernel_smooth line 222
21. lemma OAI.HigherDimensionalBallPacking.Rigidity.annularCauchyKernel_compactSupport line 239
22. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadic_summable line 260
23. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadic_tsum line 263
24. lemma OAI.HigherDimensionalBallPacking.Rigidity.four_pow_sum_le line 267
25. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadicSeries_summable line 275
26. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadicSeries_split_bound line 279
27. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadic_cubic_scale line 309
28. theorem OAI.HigherDimensionalBallPacking.Rigidity.dyadicSeries_holder line 334
29. def OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernelPotential line 373
30. def OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernelDerivative line 376
31. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernel_value_summable line 379
32. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernel_derivative_bound line 387
33. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernel_derivative_lipschitz line 393
34. theorem OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernel_hasFDerivAt line 401
35. theorem OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernel_derivative_holder line 412
36. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernel_derivative_continuous line 424
37. theorem OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernel_contDiff_one line 436
38. def OAI.HigherDimensionalBallPacking.Rigidity.physicalScaledKernel line 452
39. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledKernel_asConvolution line 456
40. lemma OAI.HigherDimensionalBallPacking.Rigidity.physicalScaledKernel_integrable line 483
41. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledKernel_value_bound_integrable line 488
42. lemma OAI.HigherDimensionalBallPacking.Rigidity.locallyIntegrable_complex_inv_series line 504
43. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyKernel line 509
44. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyKernel_integrableNecessity line 511
45. lemma OAI.HigherDimensionalBallPacking.Rigidity.physicalScaled_cutoff line 516
46. lemma OAI.HigherDimensionalBallPacking.Rigidity.physicalScaled_annular line 523