OAI/MeasureTheory/FalconerCompletion/Sphere/AngularDerivative.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.angularDerivativeND line 19
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularDerivativeND_contDiff line 23
  3. def OAI.GraphLiteralSupport.CurrentFalconer.angularGeneratorND line 28
  4. def OAI.GraphLiteralSupport.CurrentFalconer.sphereCasimirND line 32
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.sphereCasimirND_contDiff line 37
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.tsupport_angularDerivativeND_subset line 45
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.tsupport_sphereCasimirND_subset line 54
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularDerivativeND_eventuallyEq line 67
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.sphereCasimirND_eventuallyEq line 73
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularDerivativeND_add line 86
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.angularDerivativeND_const_mul line 95
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.sphereCasimirND_add line 104
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.sphereCasimirND_const_mul line 113
  14. def OAI.GraphLiteralSupport.CurrentFalconer.casimirPolynomialND line 121
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.casimirPolynomialND_contDiff line 128
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.casimirPolynomialND_commute line 136
  17. lemma OAI.GraphLiteralSupport.CurrentFalconer.casimirPolynomialND_factor line 151
  18. lemma OAI.GraphLiteralSupport.CurrentFalconer.casimirPolynomialND_eventuallyEq line 160
  19. lemma OAI.GraphLiteralSupport.CurrentFalconer.tsupport_casimirPolynomialND_subset line 170