OAI/Combinatorics/KMedian/Analysis/ComparisonCertificates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Certificates.T1_compat line 13
  2. theorem OAI.MetricKMedian.Certificates.T2_compat line 16
  3. theorem OAI.MetricKMedian.Certificates.Q0_compat line 19
  4. theorem OAI.MetricKMedian.Certificates.Q1_compat line 21
  5. theorem OAI.MetricKMedian.Certificates.Y_compat line 23
  6. theorem OAI.MetricKMedian.Certificates.Yprime_compat line 25
  7. theorem OAI.MetricKMedian.Certificates.p_bounds line 30
  8. theorem OAI.MetricKMedian.Certificates.T1_error_actual line 36
  9. theorem OAI.MetricKMedian.Certificates.T2_error_actual line 45
  10. theorem OAI.MetricKMedian.Certificates.Q0_error_actual line 54
  11. theorem OAI.MetricKMedian.Certificates.Q1_error_actual line 61
  12. theorem OAI.MetricKMedian.Certificates.Y_error_actual line 71
  13. theorem OAI.MetricKMedian.Certificates.Yprime_error_actual line 78
  14. theorem OAI.MetricKMedian.Certificates.T1_actual_pos line 85
  15. theorem OAI.MetricKMedian.Certificates.T2_actual_pos line 91
  16. theorem OAI.MetricKMedian.Certificates.Q1_actual_pos line 97
  17. theorem OAI.MetricKMedian.Certificates.Q0_actual_pos line 108
  18. theorem OAI.MetricKMedian.Certificates.Y_actual_bounds line 135
  19. theorem OAI.MetricKMedian.Certificates.Yprime_actual_bounds line 151