OAI/MeasureTheory/FalconerCompletion/Sphere/SphereAmbient.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. abbrev OAI.GraphLiteralSupport.Attempt4FullFar.SphereAmbientND line 20
  2. structure OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND line 22
  3. instance OAI.GraphLiteralSupport.Attempt4FullFar.(instance at line 27) line 27
  4. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereBasisND line 29
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.finrank_sphereAmbientND line 31
  6. def OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.casimir line 35
  7. lemma OAI.GraphLiteralSupport.Attempt4FullFar.northAmplitudeND_vanish line 40
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sqrt_seven_halves_lt_two line 50
  9. def OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.chart line 53
  10. def OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.profile line 58
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.profile_smooth line 61
  12. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereLeadingND line 65
  13. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereLeadingND_ne_zero line 68
  14. lemma OAI.GraphLiteralSupport.Attempt4FullFar.fresnelCoefficientND_half line 72
  15. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.integral_profile line 82
  16. lemma OAI.GraphLiteralSupport.Attempt4FullFar.outgoingPowerND_ne_zero line 100
  17. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.profile_zero line 105
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.profile_helmholtz line 115
  19. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.profile_jets line 148
  20. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereJetPolynomialND line 155
  21. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.profile_jets_polynomial line 160
  22. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.profile_jets_moments line 171
  23. lemma OAI.GraphLiteralSupport.Attempt4FullFar.NorthAmplitudeND.quadratic_series_global line 184