OAI/Geometry/Relativity/CKS/HeatChart.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSSphericalChart.positiveChart line 14
  2. lemma OAI.CKSSphericalChart.positiveChart_open line 15
  3. lemma OAI.CKSSphericalChart.joint_slice line 17
  4. lemma OAI.CKSSphericalChart.joint_time line 21
  5. def OAI.CKSSphericalChart.chartMass line 26
  6. def OAI.CKSSphericalChart.chartTensorA line 28
  7. def OAI.CKSSphericalChart.chartTensorPhi line 30
  8. lemma OAI.CKSSphericalChart.radius_comp_smooth line 33
  9. lemma OAI.CKSSphericalChart.joint_chart_smooth line 37
  10. lemma OAI.CKSSphericalChart.chartMass_smooth line 44
  11. lemma OAI.CKSSphericalChart.chartTensorA_smooth line 50
  12. lemma OAI.CKSSphericalChart.chartTensorPhi_smooth line 63
  13. lemma OAI.CKSSphericalChart.chartMass_laplace line 77
  14. lemma OAI.CKSSphericalChart.chartMass_first line 106