OAI/MeasureTheory/FalconerCompletion/Sphere/AngularDerivativeEventuallyEq.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_eventuallyEq line 19
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereCasimirND_eventuallyEq line 25
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_add line 38
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_const_mul line 47
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereCasimirND_add line 56
  6. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereCasimirND_const_mul line 65
  7. def OAI.GraphLiteralSupport.Attempt4FullFar.casimirPolynomialND line 73
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.casimirPolynomialND_contDiff line 80
  9. lemma OAI.GraphLiteralSupport.Attempt4FullFar.casimirPolynomialND_commute line 88
  10. lemma OAI.GraphLiteralSupport.Attempt4FullFar.casimirPolynomialND_factor line 103
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.casimirPolynomialND_eventuallyEq line 112
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.tsupport_casimirPolynomialND_subset line 122
  13. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_second line 138
  14. lemma OAI.GraphLiteralSupport.Attempt4FullFar.bilinearND_basis_expansion line 148
  15. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularGeneratorND_sum_bilinear line 163
  16. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularGeneratorND_sum_second_vector line 200
  17. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereCasimirND_eq_intrinsic line 221
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereCasimirND_basis_independent line 244
  19. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularGeneratorND_isometry line 251
  20. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_comp_isometry line 256
  21. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereCasimirND_comp_isometry line 269