OAI/Geometry/BallPacking/Necessity/CauchyDuality.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HigherDimensionalBallPacking.Rigidity.annularPotential_difference line 32
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffPotential_scale_zero line 50
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernel_cutoff_identity line 60
  4. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_contDiff_oneNecessity line 84
  5. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_hasFDerivAtNecessity line 93
  6. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_fderiv_holder line 103
  7. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_cauchy_supported_eq line 130
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_eventually_cutoff line 160
  9. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_holder_contDiff_oneNecessity line 170
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_fderiv_holder_on line 188
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.compactKernel_convolution_tendsto_bounded line 228
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.scaledKernelDerivative_tendsto line 256
  13. lemma OAI.HigherDimensionalBallPacking.Rigidity.dyadicKernelDerivative_tendsto line 274
  14. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchy_fderiv_tendsto line 288
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_fderiv_tendsto line 305
  16. def OAI.HigherDimensionalBallPacking.Rigidity.holderMollify line 342
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderMollify_smooth line 346
  18. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderMollify_bound line 352
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderMollify_holder line 363
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderMollify_support line 384
  21. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderMollify_compactSupport line 402
  22. def OAI.HigherDimensionalBallPacking.Rigidity.shrinkingHolderBump line 406
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.shrinkingHolderBump_radius_le line 411
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.holderMollify_tendsto line 414
  25. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyCurl_subLeft line 470
  26. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchy_integral_curl_translate line 478
  27. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_curl line 489
  28. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_holder_curlNecessity line 523
  29. def OAI.HigherDimensionalBallPacking.Rigidity.complexCauchyCurl line 556
  30. theorem OAI.HigherDimensionalBallPacking.Rigidity.complexCauchyCurl_smooth line 559
  31. theorem OAI.HigherDimensionalBallPacking.Rigidity.complexCauchyCurl_compactSupport line 564
  32. theorem OAI.HigherDimensionalBallPacking.Rigidity.complexCauchyCurl_dual line 569
  33. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_dual line 577