OAI/Combinatorics/KMedianRecovery/Recovery/Iterate.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BirdRationalIteration.iterate line 11
  2. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.iterate_zero line 13
  3. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.iterate_succ line 14
  4. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.step_smul line 17
  5. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.iterate_smul line 29
  6. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.step_cast line 38
  7. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.iterate_cast line 44
  8. def OAI.MetricKMedianRecovery.BirdRationalIteration.flat line 51
  9. def OAI.MetricKMedianRecovery.BirdRationalIteration.integral line 52
  10. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.integral_cast line 54
  11. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.commonDen_height line 58
  12. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.iterate_height line 68
  13. def OAI.MetricKMedianRecovery.BirdRationalIteration.determinant line 89
  14. lemma OAI.MetricKMedianRecovery.BirdRationalIteration.determinant_eq line 92
  15. lemma OAI.MetricKMedianRecovery.RationalHeight.list_sum line 99