OAI/MeasureTheory/FalconerCompletion/Sphere/SphereCasimir2.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereCasimirND line 20
  2. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereCasimirND_contDiff line 25
  3. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereCasimirND_selfadjoint line 32
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereCasimirND_planeWave line 64
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.spherePlaneWaveND_norm line 99
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.spherePlaneWaveND_hasDerivAt line 103
  7. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisIntegralND_hasDerivAt line 110
  8. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisIntegralND_casimir line 146
  9. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisIntegralND_deriv line 200
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisIntegralND_deriv2 line 206
  11. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisIntegralND_helmholtz line 216
  12. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.tsupport_angularDerivativeND_subset line 241
  13. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.tsupport_sphereCasimirND_subset line 250