OAI/MeasureTheory/FalconerCompletion/Sphere/SphereShift.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereShiftND line 18
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereJetPolynomialND_eq line 21
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereJetPolynomialND_comp_isometry line 30
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereJetPolynomialND_eventuallyEq line 40
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthPartND_tsupport line 46
  6. def OAI.GraphLiteralSupport.Attempt4FullFar.northPartAmplitudeND line 56
  7. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthPartND_eventuallyEq line 59
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthPartND_polynomial line 69
  9. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereLND line 74
  10. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.expansion_global line 77
  11. theorem OAI.GraphLiteralSupport.Attempt4FullFar.northAmplitude_stationary_globalND line 89
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereJetPolynomialND_star line 105
  13. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereReflectedSouthPartND_tsupport line 126
  14. def OAI.GraphLiteralSupport.Attempt4FullFar.southPartAmplitudeND line 138
  15. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereReflectedSouthPartND_eventuallyEq line 142
  16. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereReflectedSouthPartND_polynomial line 155
  17. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereLMinusND line 164
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereLND_comp_isometry line 167
  19. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereLMinusND_comp_isometry line 173
  20. lemma OAI.GraphLiteralSupport.Attempt4FullFar.northPartAmplitudeND_L line 182
  21. lemma OAI.GraphLiteralSupport.Attempt4FullFar.southPartAmplitudeND_L line 189
  22. theorem OAI.GraphLiteralSupport.Attempt4FullFar.sphere_global_two_poleND line 197
  23. theorem OAI.GraphLiteralSupport.Attempt4FullFar.sphere_global_rotatedND line 232
  24. lemma OAI.GraphLiteralSupport.Attempt4FullFar.casimirPolynomialND_const_mul line 272
  25. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereLND_const_mul line 285
  26. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereAxisIntegralND_const_mul line 292
  27. def OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.const_mul line 298
  28. def OAI.GraphLiteralSupport.Attempt4FullFar.northRemainderND line 303
  29. lemma OAI.GraphLiteralSupport.Attempt4FullFar.northRemainderND_const_mul line 308
  30. theorem OAI.GraphLiteralSupport.Attempt4FullFar.northAmplitude_stationary_shiftND line 315