OAI/Geometry/Relativity/CKS/MixedJetPolynomial.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSMixedGeometry.productJet_add_left line 13
  2. lemma OAI.CKSMixedGeometry.productJet_add_right line 25
  3. lemma OAI.CKSMixedGeometry.productJet_smul_left line 37
  4. lemma OAI.CKSMixedGeometry.productJet_smul_right line 49
  5. lemma OAI.CKSMixedGeometry.productJet_sub_left line 61
  6. lemma OAI.CKSMixedGeometry.productJet_sub_right line 73
  7. lemma OAI.CKSMixedGeometry.productJet_constant_right line 84
  8. lemma OAI.CKSMixedGeometry.productJet_constant_left line 86
  9. lemma OAI.CKSMixedGeometry.constantJet_smul line 88
  10. lemma OAI.CKSMixedGeometry.constantJet_add line 90
  11. lemma OAI.CKSMixedGeometry.reciprocalJet_one line 92
  12. lemma OAI.CKSMixedGeometry.productJet_zero_right line 95
  13. lemma OAI.CKSMixedGeometry.productJet_zero_left line 97
  14. lemma OAI.CKSMixedGeometry.productThreeJet_zero_right line 99
  15. lemma OAI.CKSMixedGeometry.productThreeJet_zero_left line 103
  16. def OAI.CKSMixedGeometry.powJet line 108
  17. def OAI.CKSMixedGeometry.powThreeJet line 112
  18. lemma OAI.CKSMixedGeometry.powJet_zero_succ line 116
  19. lemma OAI.CKSMixedGeometry.powThreeJet_zero_succ line 117
  20. lemma OAI.CKSMixedGeometry.powJet_fst line 118
  21. lemma OAI.CKSMixedGeometry.powThreeJet_fst line 122
  22. lemma OAI.CKSMixedGeometry.powJet_smooth line 129
  23. lemma OAI.CKSMixedGeometry.powThreeJet_smooth line 133
  24. lemma OAI.CKSMixedGeometry.actualScalarJet_pow line 138
  25. lemma OAI.CKSMixedGeometry.actualThreeJet_pow line 143
  26. lemma OAI.CKSMixedGeometry.productJet_contDiff line 151
  27. lemma OAI.CKSMixedGeometry.productJet_contDiffAt line 153
  28. lemma OAI.CKSMixedGeometry.powJet_contDiff line 155
  29. lemma OAI.CKSMixedGeometry.powJet_contDiffAt line 157
  30. lemma OAI.CKSMixedGeometry.productThreeJet_contDiff line 159
  31. lemma OAI.CKSMixedGeometry.productThreeJet_contDiffAt line 161
  32. lemma OAI.CKSMixedGeometry.powThreeJet_contDiff line 163
  33. lemma OAI.CKSMixedGeometry.powThreeJet_contDiffAt line 165
  34. def OAI.CKSMixedGeometry.massNumeratorJet line 169
  35. def OAI.CKSMixedGeometry.normalizedMassJet line 175
  36. lemma OAI.CKSMixedGeometry.massNumeratorJet_smooth line 179
  37. lemma OAI.CKSMixedGeometry.normalizedMassJet_smooth line 183
  38. lemma OAI.CKSMixedGeometry.normalizedMassJet_zero line 191