OAI/MeasureTheory/FalconerCompletion/Sphere/SphereAxisIntegralConj.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereAxisIntegralND_conj line 18
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.radial_sphere_integrableND line 30
  3. theorem OAI.GraphLiteralSupport.Attempt4FullFar.noncomparable_conj_sphereND line 48
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.pole_exact_sphere_integralND line 62
  5. theorem OAI.GraphLiteralSupport.Attempt4FullFar.pole_noncomparable_kernelND line 92
  6. theorem OAI.GraphLiteralSupport.Attempt4FullFar.sphere_noncomparable_kernelND line 140