OAI/MeasureTheory/FalconerCompletion/Sphere/SphereCasimir.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

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