OAI/MeasureTheory/FalconerCompletion/Sphere/SphereAmbient2.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

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