OAI/Geometry/Relativity/CKS/HeatPotential.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSphericalHarmonics.inversePolynomials line 11
2. lemma OAI.CKSSphericalHarmonics.inversePolynomials_rapid line 14
3. lemma OAI.CKSSphericalHarmonics.inversePolynomials_harmonic line 20
4. lemma OAI.CKSSphericalHarmonics.heatTerm_inverse line 26
5. lemma OAI.CKSSphericalHarmonics.casimir_terms_summable line 32
6. theorem OAI.CKSSphericalHarmonics.spatialHeat_inverse_equation line 40
7. lemma OAI.CKSSphericalHarmonics.harmonic_sphereIntegral_zero line 61
8. lemma OAI.CKSSphericalHarmonics.sphereHeatJet_mean_zero line 70