OAI/MeasureTheory/FalconerCompletion/Sphere/SphereAxisIntegral.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereAxisIntegralND line 19
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereAxisIntegralND_rotate line 22
  3. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereAxisReflectionND line 29
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereAxisReflectionND_apply line 33
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphere_north_normND line 51
  6. theorem OAI.GraphLiteralSupport.Attempt4FullFar.sphere_rotated_stationaryND_uniform line 56
  7. instance OAI.GraphLiteralSupport.Attempt4FullFar.canonicalSphereMeasureND_finite line 104
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.canonicalSphereMeasureND_ae_norm line 108
  9. def OAI.GraphLiteralSupport.Attempt4FullFar.skewFlowND line 115
  10. lemma OAI.GraphLiteralSupport.Attempt4FullFar.skewFlowND_apply line 123
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.skewFlowND_zero line 127
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.skewFlowND_hasDerivAt line 131
  13. theorem OAI.GraphLiteralSupport.Attempt4FullFar.integral_sphere_skew_derivative_zero line 137
  14. def OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND line 198
  15. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_contDiff line 202
  16. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_mul line 207
  17. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphere_angular_integration_by_parts line 216
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphere_angular_second_selfadjoint line 229
  19. def OAI.GraphLiteralSupport.Attempt4FullFar.angularGeneratorND line 237
  20. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularGeneratorND_skew line 241
  21. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularGeneratorND_apply line 246
  22. def OAI.GraphLiteralSupport.Attempt4FullFar.spherePlaneWaveND line 251
  23. lemma OAI.GraphLiteralSupport.Attempt4FullFar.spherePlaneWaveND_contDiff line 255
  24. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_planeWave line 264
  25. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_complexLinear line 281
  26. lemma OAI.GraphLiteralSupport.Attempt4FullFar.angularDerivativeND_planeWave_second line 289