OAI/Geometry/Relativity/CKS/CollarMetricCoefficient.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSAngularGeometry.normalizedFoliationMetric line 12
  2. def OAI.CKSAngularGeometry.metricCorrection line 16
  3. lemma OAI.CKSAngularGeometry.metric_correction_identity line 20
  4. def OAI.CKSAngularGeometry.rawNormalizedSpeed line 32
  5. def OAI.CKSAngularGeometry.rawMetricDomain line 33
  6. def OAI.CKSAngularGeometry.rawMetricCorrection line 34
  7. def OAI.CKSAngularGeometry.rawNormalizedMetric line 38
  8. def OAI.CKSAngularGeometry.rawBackgroundMetric line 41
  9. lemma OAI.CKSAngularGeometry.rawNormalizedSpeed_smooth line 44
  10. lemma OAI.CKSAngularGeometry.rawMetricDomain_open line 50
  11. lemma OAI.CKSAngularGeometry.rawMetricFamily_regular line 58
  12. lemma OAI.CKSAngularGeometry.rawMetricCorrection_continuousAt line 67
  13. lemma OAI.CKSAngularGeometry.raw_metric_correction line 93
  14. theorem OAI.CKSAngularGeometry.bounded_raw_collar_metric line 104