OAI/Geometry/Relativity/CKS/SphereHeat.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSSphericalHarmonics.smooth_harmonicCoefficients_summable line 11
  2. theorem OAI.CKSSphericalHarmonics.smooth_harmonicCoefficients_tsum line 18
  3. lemma OAI.CKSSphericalHarmonics.sphereEval_C line 26
  4. lemma OAI.CKSSphericalHarmonics.sphereIntegral_constant line 30
  5. lemma OAI.CKSSphericalHarmonics.harmonicProjection_zero_of_mean_zero line 34
  6. lemma OAI.CKSSphericalHarmonics.first_moments_pairing_zero line 46
  7. lemma OAI.CKSSphericalHarmonics.harmonicProjection_one_of_first_moments line 59
  8. lemma OAI.CKSSphericalHarmonics.harmonicCoefficient_zero_of_mean line 70
  9. lemma OAI.CKSSphericalHarmonics.harmonicCoefficient_one_of_first_moments line 83
  10. def OAI.CKSSphericalHarmonics.Balanced line 90
  11. lemma OAI.CKSSphericalHarmonics.smooth_high_harmonics_initial line 93
  12. def OAI.CKSSphericalHarmonics.sphereHeatJet line 103
  13. lemma OAI.CKSSphericalHarmonics.sphereHeatJet_eq line 106
  14. lemma OAI.CKSSphericalHarmonics.sphereHeatJet_decay line 120
  15. lemma OAI.CKSSphericalHarmonics.sphereHeatJet_smooth line 126
  16. lemma OAI.CKSSphericalHarmonics.sphereHeatJet_initial line 131
  17. lemma OAI.CKSSphericalHarmonics.jointHeatSeries_fderiv_tsum line 139
  18. lemma OAI.CKSSphericalHarmonics.heatTerm_directional_rotation line 151
  19. def OAI.CKSSphericalHarmonics.spatialHeat line 166
  20. lemma OAI.CKSSphericalHarmonics.spatialHeat_smooth line 169
  21. lemma OAI.CKSSphericalHarmonics.spatialHeat_rotation line 173
  22. lemma OAI.CKSSphericalHarmonics.spatialHeat_time_derivative line 187