OAI/Geometry/BallPacking/Holder/HolderTaylor.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HigherDimensionalBallPacking.Rigidity.holder_taylor_remainder line 17
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.hasFDerivAt_of_holder_remainder line 34
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.holder_continuous line 48
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.hasFDerivAt_limit_of_holder_derivative line 61
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyDerivative_holder line 84
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_hasFDerivAt line 96
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_contDiff_one line 120
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_fderiv_bound line 132
  9. def OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel line 166
  10. def OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyJet line 169
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel_smooth line 173
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel_eventually_zero line 177
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyJet_eq line 182
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel_zero line 193
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel_tendsto line 201
  16. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyJet_tendsto line 208
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel_uniform_bounds line 232
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel_hasFDerivAt line 271
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel_bounds line 292
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyKernel_contDiff_one line 317
  21. def OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyTransform line 330
  22. def OAI.HigherDimensionalBallPacking.Rigidity.tailIntegralJet line 333
  23. def OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyDerivative line 336
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyTransform_eq line 340
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchyJet_continuous line 344
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailIntegralJet_continuous line 349
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailIntegralJet_bound line 355
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchy_hasFDerivAt line 368
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchy_value_bound line 393
  30. lemma OAI.HigherDimensionalBallPacking.Rigidity.tailCauchy_derivative_bounds line 403
  31. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyKernel_integrable line 440
  32. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_convolution_integrable line 445
  33. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_value_bound line 458
  34. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchy_kernel_convolution_split line 471
  35. def OAI.HigherDimensionalBallPacking.Rigidity.globalCauchyDerivative line 494
  36. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_holder_hasFDerivAt line 497
  37. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_schauder_bounds line 505
  38. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_holder_contDiff_one line 573
  39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedHolder_hasCompactSupport line 600
  40. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedHolder_integrable line 606
  41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedHolder_integral_norm_le line 612
  42. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supported_cauchy_bounds line 621
  43. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.schauderConstant line 639
  44. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.schauderConstant_nonneg line 640
  45. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.schauderConstant_spec line 642
  46. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCauchy line 649
  47. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCauchy_value line 664
  48. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCauchy_deriv line 666
  49. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCauchy_norm_le line 669
  50. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supported_cauchy_integrable line 688
  51. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCauchy_add line 694
  52. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCauchy_smul line 704
  53. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCauchyCLM line 714
  54. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.supportedCauchyCLM_value line 721