OAI/Geometry/Relativity/CKS/HeatRegularity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSDifferentialSeries.series line 18
  2. lemma OAI.CKSDifferentialSeries.series_summable line 23
  3. lemma OAI.CKSDifferentialSeries.series_continuous line 30
  4. lemma OAI.CKSDifferentialSeries.series_hasFDerivAt line 36
  5. theorem OAI.CKSDifferentialSeries.series_contDiff line 75
  6. def OAI.CKSSphericalHarmonics.PolynomialRapid line 99
  7. def OAI.CKSSphericalHarmonics.heatPolynomials line 103
  8. lemma OAI.CKSSphericalHarmonics.heatPolynomials_rapid line 106
  9. lemma OAI.CKSSphericalHarmonics.heatTerm_bound line 113
  10. def OAI.CKSSphericalHarmonics.jointHeatSeries line 124
  11. lemma OAI.CKSSphericalHarmonics.jointHeatSeries_summable line 127
  12. theorem OAI.CKSSphericalHarmonics.jointHeatSeries_smooth line 131
  13. lemma OAI.CKSSphericalHarmonics.jointHeatSeries_hasFDerivAt line 136
  14. theorem OAI.CKSSphericalHarmonics.smoothSphere_joint_heat line 143
  15. lemma OAI.CKSSphericalHarmonics.jointHeatSeries_sphere_smooth line 149