OAI/Geometry/Relativity/CKS/FoliationCurvatureOperator.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSAngularGeometry.foliationMetric_contDiffAt line 11
  2. lemma OAI.CKSAngularGeometry.adaptedFrame_contDiffAt line 41
  3. theorem OAI.CKSAngularGeometry.foliation_scalar_curvature_trace line 70
  4. abbrev OAI.CKSAngularGeometry.CovectorJet line 95
  5. abbrev OAI.CKSAngularGeometry.CovariantTensorJet line 96
  6. def OAI.CKSAngularGeometry.covectorDiv line 98
  7. def OAI.CKSAngularGeometry.tensorDiv line 100
  8. def OAI.CKSAngularGeometry.covectorLie line 103
  9. def OAI.CKSAngularGeometry.covectorPair line 105
  10. def OAI.CKSAngularGeometry.tensorPair line 107
  11. def OAI.CKSAngularGeometry.normalMomentum line 110
  12. def OAI.CKSAngularGeometry.angularMomentum line 114
  13. abbrev OAI.CKSAngularGeometry.MomentumInput line 120
  14. abbrev OAI.CKSAngularGeometry.mz line 123
  15. abbrev OAI.CKSAngularGeometry.mw line 124
  16. abbrev OAI.CKSAngularGeometry.mq line 125
  17. abbrev OAI.CKSAngularGeometry.mc line 126
  18. abbrev OAI.CKSAngularGeometry.mS line 127
  19. abbrev OAI.CKSAngularGeometry.mE line 128
  20. abbrev OAI.CKSAngularGeometry.mT line 129
  21. abbrev OAI.CKSAngularGeometry.mX line 130
  22. abbrev OAI.CKSAngularGeometry.mEr line 131
  23. def OAI.CKSAngularGeometry.normalizedSpeed line 133
  24. def OAI.CKSAngularGeometry.normalizedMean line 135
  25. def OAI.CKSAngularGeometry.accelerationCoefficient line 137
  26. def OAI.CKSAngularGeometry.normalResidual line 140
  27. def OAI.CKSAngularGeometry.angularResidual line 147
  28. def OAI.CKSAngularGeometry.momentumResidual line 155
  29. def OAI.CKSAngularGeometry.momentumRegion line 157
  30. lemma OAI.CKSAngularGeometry.momentumRegion_open line 160
  31. lemma OAI.CKSAngularGeometry.momentInverse_smooth line 165
  32. lemma OAI.CKSAngularGeometry.momentChristoffel_smooth line 169
  33. lemma OAI.CKSAngularGeometry.normalizedSpeed_smooth line 173
  34. lemma OAI.CKSAngularGeometry.normalizedMean_smooth line 177
  35. lemma OAI.CKSAngularGeometry.accelerationCoefficient_smooth line 179
  36. lemma OAI.CKSAngularGeometry.momentCovectorDiv_smooth line 183
  37. lemma OAI.CKSAngularGeometry.momentTensorDiv_smooth line 192
  38. lemma OAI.CKSAngularGeometry.momentTensorPair_smooth line 202
  39. lemma OAI.CKSAngularGeometry.momentCovectorPair_smooth line 210
  40. lemma OAI.CKSAngularGeometry.momentumResidual_smooth line 217