OAI/Combinatorics/KMedianRecovery/Recovery/CommonDen.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BirdRational.commonDen line 13
  2. def OAI.MetricKMedianRecovery.BirdRational.scaled line 14
  3. lemma OAI.MetricKMedianRecovery.BirdRational.commonDen_pos line 18
  4. lemma OAI.MetricKMedianRecovery.BirdRational.scaled_cast line 21
  5. lemma OAI.MetricKMedianRecovery.BirdRational.scaled_height line 34
  6. lemma OAI.MetricKMedianRecovery.BirdRational.intCast_height line 51
  7. def OAI.MetricKMedianRecovery.BirdRational.data line 56
  8. def OAI.MetricKMedianRecovery.BirdRational.integerMatrix line 61
  9. def OAI.MetricKMedianRecovery.BirdRational.integerVector line 64
  10. lemma OAI.MetricKMedianRecovery.BirdRational.integerMatrix_cast line 68
  11. lemma OAI.MetricKMedianRecovery.BirdRational.integerVector_cast line 74
  12. def OAI.MetricKMedianRecovery.BirdRational.solve line 79
  13. lemma OAI.MetricKMedianRecovery.BirdRational.solve_as_cramer line 87
  14. theorem OAI.MetricKMedianRecovery.BirdRational.solve_correct line 97
  15. def OAI.MetricKMedianRecovery.BirdRational.clearedHeight line 111
  16. def OAI.MetricKMedianRecovery.BirdRational.detHeight line 112
  17. lemma OAI.MetricKMedianRecovery.BirdRational.data_height line 114
  18. lemma OAI.MetricKMedianRecovery.BirdRational.integerMatrix_height line 122
  19. lemma OAI.MetricKMedianRecovery.BirdRational.integerVector_height line 130
  20. lemma OAI.MetricKMedianRecovery.BirdRational.updated_height line 136
  21. theorem OAI.MetricKMedianRecovery.BirdRational.solve_height line 144