OAI/Geometry/Relativity/CKS/CollarMetricComparison.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSAngularGeometry.quadratic3 line 12
  2. lemma OAI.CKSAngularGeometry.quadratic3_eq_dot line 14
  3. lemma OAI.CKSAngularGeometry.quadratic3_sub line 23
  4. lemma OAI.CKSAngularGeometry.quadratic3_smul line 27
  5. lemma OAI.CKSAngularGeometry.quadratic3_bound line 31
  6. lemma OAI.CKSAngularGeometry.quadratic3_error line 55
  7. lemma OAI.CKSAngularGeometry.round_background_lower line 60
  8. theorem OAI.CKSAngularGeometry.metric_lower_from_coefficients line 67
  9. lemma OAI.CKSAngularGeometry.metric_upper_from_coefficients line 81
  10. theorem OAI.CKSAngularGeometry.metric_comparison_from_background line 95
  11. lemma OAI.CKSAngularGeometry.comparison_posSemidef line 111