OAI/Geometry/Relativity/CKS/FullSphereHeat.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSInducedSphere.pd_const_add line 12
2. lemma OAI.CKSInducedSphere.pd_const_add_fun line 16
3. lemma OAI.CKSInducedSphere.roundLaplacian_const_add line 21
4. lemma OAI.CKSInducedSphere.sphereGradient_const_add line 25
5. lemma OAI.CKSInducedSphere.radial_restriction line 29
6. lemma OAI.CKSInducedSphere.smoothDatum_rapid line 34
7. structure OAI.CKSInducedSphere.AngularHeatSolution line 39
8. theorem OAI.CKSInducedSphere.sphere_heat_full line 58
9. theorem OAI.CKSInducedSphere.sphere_heat_every_smooth line 114