OAI/Geometry/Relativity/CKS/CollarLapseJet.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSAngularGeometry.LapseInput line 11
  2. def OAI.CKSAngularGeometry.radicandJet line 13
  3. def OAI.CKSAngularGeometry.reconstructedLapse line 16
  4. def OAI.CKSAngularGeometry.lapseRegion line 19
  5. def OAI.CKSAngularGeometry.lapseReference line 21
  6. def OAI.CKSAngularGeometry.lapseReferenceFamily line 23
  7. lemma OAI.CKSAngularGeometry.radicandJet_smooth line 25
  8. lemma OAI.CKSAngularGeometry.reconstructedLapse_smooth line 37
  9. lemma OAI.CKSAngularGeometry.lapseRegion_open line 44
  10. lemma OAI.CKSAngularGeometry.radicand_reference line 49
  11. lemma OAI.CKSAngularGeometry.reconstructed_reference line 56
  12. lemma OAI.CKSAngularGeometry.lapseReferenceFamily_compact line 60
  13. lemma OAI.CKSAngularGeometry.lapseReferenceFamily_regular line 63
  14. theorem OAI.CKSAngularGeometry.lapse_uniform_lipschitz line 70
  15. lemma OAI.CKSAngularGeometry.actual_radicandJet line 83
  16. theorem OAI.CKSAngularGeometry.actual_reconstructedLapse line 96
  17. lemma OAI.CKSAngularGeometry.radial_normalization line 112