OAI/Geometry/Relativity/CKS/CKSFoliationJet.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSMixedGeometry.foliationDen line 13
  2. def OAI.CKSMixedGeometry.lapseCorrection line 15
  3. def OAI.CKSMixedGeometry.uCorrection line 18
  4. def OAI.CKSMixedGeometry.foliationCoefficients line 21
  5. def OAI.CKSMixedGeometry.foliationRegion line 24
  6. lemma OAI.CKSMixedGeometry.foliationRegion_open line 26
  7. lemma OAI.CKSMixedGeometry.foliationRegion_zero line 28
  8. lemma OAI.CKSMixedGeometry.foliationDen_smooth line 33
  9. lemma OAI.CKSMixedGeometry.lapseCorrection_smooth line 38
  10. lemma OAI.CKSMixedGeometry.uCorrection_smooth line 50
  11. lemma OAI.CKSMixedGeometry.foliationCoefficients_smooth line 56
  12. lemma OAI.CKSMixedGeometry.foliation_family_bound line 61
  13. theorem OAI.CKSMixedGeometry.cks_foliation_coefficients_bounded line 88