OAI/Geometry/BallPacking/Holder/SchauderSplit.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HigherDimensionalBallPacking.Rigidity.SchauderSplit line 17
  2. lemma OAI.HigherDimensionalBallPacking.Rigidity.norm_second_const_sub line 30
  3. lemma OAI.HigherDimensionalBallPacking.Rigidity.first_near_bound line 37
  4. lemma OAI.HigherDimensionalBallPacking.Rigidity.second_far_bound line 51
  5. lemma OAI.HigherDimensionalBallPacking.Rigidity.schauderSplit_exists_uniform line 76
  6. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smoothCauchyKernel_splits line 120
  7. lemma OAI.HigherDimensionalBallPacking.Rigidity.inv_sq_mul_third line 135
  8. lemma OAI.HigherDimensionalBallPacking.Rigidity.inv_cube_mul_third line 140
  9. lemma OAI.HigherDimensionalBallPacking.Rigidity.SchauderSplit.near_weight_bound line 146
  10. lemma OAI.HigherDimensionalBallPacking.Rigidity.SchauderSplit.far_weight_bound line 174
  11. lemma OAI.HigherDimensionalBallPacking.Rigidity.SchauderSplit.holder_bound line 205
  12. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smoothCauchyKernel_full_schauder line 235
  13. def OAI.HigherDimensionalBallPacking.Rigidity.cauchySchauderWeight line 260
  14. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchy_holder_power_locallyIntegrable line 264
  15. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchySchauderWeight_integrable line 271
  16. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smoothCauchyKernel_bound line 281
  17. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smoothCauchyKernel_schauder_bound line 316
  18. theorem OAI.HigherDimensionalBallPacking.Rigidity.locallyIntegrable_complex_inv line 368
  19. def OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform line 375
  20. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_apply line 378
  21. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_smooth line 381
  22. theorem OAI.HigherDimensionalBallPacking.Rigidity.cauchyTransform_hasFDerivAt line 386
  23. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smoothCauchyKernel_convolution_tendsto line 402
  24. theorem OAI.HigherDimensionalBallPacking.Rigidity.cutoff_cauchy_holder_lipschitz line 428
  25. def OAI.HigherDimensionalBallPacking.Rigidity.regularizedCauchyJet line 474
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.regularizedCauchyJet_eq line 478
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.regularizedCauchyJet_continuousAt line 488
  28. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyJet line 498
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyJet_eq line 501
  30. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyJet_continuousAt line 507
  31. def OAI.HigherDimensionalBallPacking.Rigidity.cancellationJetIntegrand line 523
  32. def OAI.HigherDimensionalBallPacking.Rigidity.cutoffCauchyDerivative line 527
  33. lemma OAI.HigherDimensionalBallPacking.Rigidity.cancellationJetIntegrand_apply line 531
  34. lemma OAI.HigherDimensionalBallPacking.Rigidity.cancellationJetIntegrand_continuous line 536
  35. lemma OAI.HigherDimensionalBallPacking.Rigidity.cancellationJetIntegrand_bound line 548
  36. lemma OAI.HigherDimensionalBallPacking.Rigidity.cancellationJetIntegrand_tendsto line 566
  37. lemma OAI.HigherDimensionalBallPacking.Rigidity.cutoff_smoothCauchyKernel_derivative_tendsto line 579