OAI/MeasureTheory/FalconerCompletion/Graphs/SpherePairRadialCoefficient.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.Attempt4FullFar.spherePairRadialCoefficientND line 21
  2. theorem OAI.GraphLiteralSupport.Attempt4FullFar.spherePairRadialCoefficientND_bound line 28
  3. theorem OAI.GraphLiteralSupport.Attempt4FullFar.spherePairRadialCoefficientND_kernel line 65
  4. abbrev OAI.GraphLiteralSupport.Attempt4FullFar.PoleIndexND line 103
  5. def OAI.GraphLiteralSupport.Attempt4FullFar.poleSignND line 105
  6. lemma OAI.GraphLiteralSupport.Attempt4FullFar.poleSignND_cases line 106
  7. lemma OAI.GraphLiteralSupport.Attempt4FullFar.poleSignND_neg_cases line 108
  8. def OAI.GraphLiteralSupport.Attempt4FullFar.radialPoleSumND line 111
  9. lemma OAI.GraphLiteralSupport.Attempt4FullFar.radialPhaseIntegral_integrable line 116
  10. lemma OAI.GraphLiteralSupport.Attempt4FullFar.pole_pair_integrand_identityND line 125
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.pole_pair_integral_identityND line 164
  12. theorem OAI.GraphLiteralSupport.Attempt4FullFar.pole_pair_kernelND line 189