OAI/Geometry/Relativity/CKS/SchwarzschildMetric.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSSchwarzschild.radialUnit_smoothAt line 17
  2. lemma OAI.CKSSchwarzschild.radialForm_smoothAt line 19
  3. lemma OAI.CKSSchwarzschild.cartMetric_smoothAt line 24
  4. lemma OAI.CKSSchwarzschild.velocity_deriv_smooth line 31
  5. lemma OAI.CKSSchwarzschild.cartTensor_smoothAt line 33
  6. lemma OAI.CKSSchwarzschild.euclideanForm_apply line 43
  7. lemma OAI.CKSSchwarzschild.radialForm_apply line 44
  8. lemma OAI.CKSSchwarzschild.cartMetric_apply line 46
  9. lemma OAI.CKSSchwarzschild.cartMetric_symm line 49
  10. lemma OAI.CKSSchwarzschild.cartTensor_symm line 51
  11. lemma OAI.CKSSchwarzschild.norm_radialUnit line 58
  12. lemma OAI.CKSSchwarzschild.cartMetric_pos line 61
  13. lemma OAI.CKSSchwarzschild.metricInner_smooth line 75
  14. lemma OAI.CKSSchwarzschild.tensorInner_smooth line 82
  15. lemma OAI.CKSSchwarzschild.metricInner_symm line 89
  16. lemma OAI.CKSSchwarzschild.tensorInner_symm line 92
  17. lemma OAI.CKSSchwarzschild.metricInner_pos line 95
  18. def OAI.CKSSchwarzschild.smoothMetric line 105
  19. theorem OAI.CKSSchwarzschild.exists_schwarzschild_smooth_data line 112