OAI/Geometry/Relativity/CKS/JetPolynomial.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSAngularGeometry.productJet_add_left line 11
  2. lemma OAI.CKSAngularGeometry.productJet_add_right line 23
  3. lemma OAI.CKSAngularGeometry.productJet_smul_left line 35
  4. lemma OAI.CKSAngularGeometry.productJet_smul_right line 47
  5. lemma OAI.CKSAngularGeometry.productJet_sub_left line 59
  6. lemma OAI.CKSAngularGeometry.productJet_sub_right line 71
  7. lemma OAI.CKSAngularGeometry.productJet_constant_right line 82
  8. lemma OAI.CKSAngularGeometry.productJet_constant_left line 85
  9. lemma OAI.CKSAngularGeometry.constantJet_smul line 87
  10. lemma OAI.CKSAngularGeometry.constantJet_add line 89
  11. lemma OAI.CKSAngularGeometry.reciprocalJet_one line 91
  12. def OAI.CKSAngularGeometry.massNumeratorJet line 94
  13. def OAI.CKSAngularGeometry.normalizedMassJet line 99
  14. lemma OAI.CKSAngularGeometry.massNumeratorJet_smooth line 103
  15. lemma OAI.CKSAngularGeometry.normalizedMassJet_smooth line 116
  16. lemma OAI.CKSAngularGeometry.normalizedMassJet_zero line 124
  17. theorem OAI.CKSAngularGeometry.exact_mass_cancellation line 130