OAI/Geometry/Relativity/CKS/ConeSupport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSEnd.mass line 9
  2. def OAI.CKSEnd.normalMass line 11
  3. structure OAI.CKSEnd.ConstraintJet line 14
  4. def OAI.CKSEnd.ConstraintJet.H line 33
  5. def OAI.CKSEnd.ConstraintJet.p line 34
  6. def OAI.CKSEnd.ConstraintJet.NH line 36
  7. def OAI.CKSEnd.ConstraintJet.Np line 39
  8. def OAI.CKSEnd.ConstraintJet.C line 42
  9. def OAI.CKSEnd.ConstraintJet.Q line 47
  10. def OAI.CKSEnd.ConstraintJet.massIdentityRHS line 51
  11. theorem OAI.CKSEnd.ConstraintJet.mass_identity line 59
  12. def OAI.CKSEnd.DEC line 72
  13. lemma OAI.CKSEnd.momentum_norm line 75
  14. lemma OAI.CKSEnd.DEC.add line 80
  15. lemma OAI.CKSEnd.DEC.of_null_margins line 92
  16. lemma OAI.CKSEnd.DEC.after_common_norm line 102
  17. def OAI.CKSEnd.smallMargin line 113
  18. def OAI.CKSEnd.largeMargin line 115
  19. lemma OAI.CKSEnd.smallMargin_eq_rpow line 117
  20. theorem OAI.CKSEnd.collar_DEC_of_weighted_errors line 126