OAI/MeasureTheory/FalconerCompletion/Sphere/SphereAxisIntegral2.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisIntegralND line 20
  2. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisIntegralND_rotate line 23
  3. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisReflectionND line 30
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAxisReflectionND_apply line 34
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphere_north_normND line 52
  6. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.sphere_rotated_stationaryND_uniform line 57
  7. instance OAI.GraphLiteralSupport.Attempt4PrefixShell.canonicalSphereMeasureND_finite line 105
  8. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.canonicalSphereMeasureND_ae_norm line 109
  9. def OAI.GraphLiteralSupport.Attempt4PrefixShell.skewFlowND line 116
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.skewFlowND_apply line 124
  11. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.skewFlowND_zero line 128
  12. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.skewFlowND_hasDerivAt line 132
  13. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.integral_sphere_skew_derivative_zero line 138
  14. def OAI.GraphLiteralSupport.Attempt4PrefixShell.angularDerivativeND line 199
  15. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.angularDerivativeND_contDiff line 203
  16. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.angularDerivativeND_mul line 208
  17. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphere_angular_integration_by_parts line 217
  18. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphere_angular_second_selfadjoint line 230
  19. def OAI.GraphLiteralSupport.Attempt4PrefixShell.angularGeneratorND line 238
  20. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.angularGeneratorND_skew line 242
  21. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.angularGeneratorND_apply line 247
  22. def OAI.GraphLiteralSupport.Attempt4PrefixShell.spherePlaneWaveND line 252
  23. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.spherePlaneWaveND_contDiff line 256
  24. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.angularDerivativeND_planeWave line 265
  25. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.angularDerivativeND_complexLinear line 282
  26. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.angularDerivativeND_planeWave_second line 290