OAI/Geometry/Relativity/CKS/CollarNullMap.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSAngularGeometry.nullD line 12
  2. def OAI.CKSAngularGeometry.nullRatio line 14
  3. def OAI.CKSAngularGeometry.lapseResidual line 17
  4. def OAI.CKSAngularGeometry.nullQuadratic line 23
  5. def OAI.CKSAngularGeometry.nullMomentumRegion line 29
  6. lemma OAI.CKSAngularGeometry.nullD_smooth line 30
  7. lemma OAI.CKSAngularGeometry.nullMomentumRegion_open line 31
  8. lemma OAI.CKSAngularGeometry.nullRatio_smooth line 33
  9. lemma OAI.CKSAngularGeometry.lapseResidual_smooth line 38
  10. lemma OAI.CKSAngularGeometry.momentTensorPair_fields_smooth line 52
  11. lemma OAI.CKSAngularGeometry.momentCovectorPair_fields_smooth line 63
  12. lemma OAI.CKSAngularGeometry.nullQuadratic_smooth line 70
  13. abbrev OAI.CKSAngularGeometry.NullInput line 78
  14. abbrev OAI.CKSAngularGeometry.nP line 79
  15. abbrev OAI.CKSAngularGeometry.nF line 80
  16. abbrev OAI.CKSAngularGeometry.nFr line 81
  17. def OAI.CKSAngularGeometry.nullResidual line 83
  18. def OAI.CKSAngularGeometry.nullRegion line 91
  19. lemma OAI.CKSAngularGeometry.nullRegion_open line 92
  20. lemma OAI.CKSAngularGeometry.nullResidual_smooth line 93