OAI/Geometry/Relativity/CKS/HeatTensor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSInducedSphere.sphereGradient_rotations line 13
2. lemma OAI.CKSInducedSphere.smoothRotation_congr_sphere line 24
3. lemma OAI.CKSInducedSphere.sphereGradient_congr_sphere line 43
4. def OAI.CKSInducedSphere.heatTensor line 52
5. lemma OAI.CKSInducedSphere.heatTensor_symmetric line 55
6. lemma OAI.CKSInducedSphere.heatTensor_tangent line 62
7. lemma OAI.CKSInducedSphere.heatTensor_trace_zero line 66
8. theorem OAI.CKSInducedSphere.heatTensor_divergence line 70