OAI/Geometry/Relativity/CKS/CKSFoliationLeading.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSMixedGeometry.leadingD line 13
  2. def OAI.CKSMixedGeometry.leadingT line 15
  3. def OAI.CKSMixedGeometry.leadingLapse line 17
  4. def OAI.CKSMixedGeometry.leadingU line 18
  5. lemma OAI.CKSMixedGeometry.coefficientD_zero line 20
  6. lemma OAI.CKSMixedGeometry.coefficientT_zero line 27
  7. lemma OAI.CKSMixedGeometry.coefficientV_zero line 29
  8. lemma OAI.CKSMixedGeometry.sqrtJet_one line 31
  9. lemma OAI.CKSMixedGeometry.reciprocalJet_constant line 33
  10. lemma OAI.CKSMixedGeometry.lapseCorrection_zero line 35
  11. lemma OAI.CKSMixedGeometry.uCorrection_zero line 43
  12. lemma OAI.CKSMixedGeometry.foliation_uniform_lipschitz line 47
  13. theorem OAI.CKSMixedGeometry.cks_foliation_leading_bounded line 75