OAI/Geometry/Relativity/CKS/CollarExpansionJet.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSAngularGeometry.ExpansionInput line 11
  2. def OAI.CKSAngularGeometry.normalizedLieJet line 14
  3. def OAI.CKSAngularGeometry.normalizedExpansionJet line 18
  4. def OAI.CKSAngularGeometry.expansionRegion line 22
  5. def OAI.CKSAngularGeometry.expansionReference line 24
  6. lemma OAI.CKSAngularGeometry.productJet_zero_right line 27
  7. lemma OAI.CKSAngularGeometry.productJet_zero_left line 29
  8. lemma OAI.CKSAngularGeometry.normalizedExpansion_reference line 32
  9. lemma OAI.CKSAngularGeometry.normalizedLieJet_smooth line 37
  10. lemma OAI.CKSAngularGeometry.normalizedExpansionJet_smooth line 48
  11. lemma OAI.CKSAngularGeometry.expansionRegion_open line 63
  12. theorem OAI.CKSAngularGeometry.expansion_uniform_lipschitz line 66
  13. def OAI.CKSAngularGeometry.actualExpansionInput line 83
  14. def OAI.CKSAngularGeometry.normalizedLie line 90
  15. def OAI.CKSAngularGeometry.normalizedExpansion line 94
  16. lemma OAI.CKSAngularGeometry.component_three line 97
  17. lemma OAI.CKSAngularGeometry.normalizedLie_diff line 101
  18. lemma OAI.CKSAngularGeometry.actual_normalizedLieJet line 113
  19. theorem OAI.CKSAngularGeometry.actual_normalizedExpansionJet line 142