OAI/Combinatorics/KMedianRecovery/Recovery/Freeze.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BirdInteger.sumFrom_eq_sum_Ico line 11
  2. lemma OAI.MetricKMedianRecovery.BirdInteger.sumFrom_fin_tail line 17
  3. lemma OAI.MetricKMedianRecovery.BirdInteger.iterate_get_eq_spec line 25
  4. lemma OAI.MetricKMedianRecovery.BirdInteger.bird_eq_spec line 35
  5. lemma OAI.MetricKMedianRecovery.BirdInteger.spec_eq_det line 41
  6. def OAI.MetricKMedianRecovery.BirdInteger.freeze line 48
  7. lemma OAI.MetricKMedianRecovery.BirdInteger.freeze_eq line 52
  8. def OAI.MetricKMedianRecovery.BirdInteger.iterate line 55
  9. lemma OAI.MetricKMedianRecovery.BirdInteger.iterate_eq line 59
  10. def OAI.MetricKMedianRecovery.BirdInteger.determinant line 65
  11. lemma OAI.MetricKMedianRecovery.BirdInteger.determinant_eq line 69
  12. lemma OAI.MetricKMedianRecovery.BirdInteger.sum_natAbs_bound line 75
  13. lemma OAI.MetricKMedianRecovery.BirdInteger.step_height line 83
  14. theorem OAI.MetricKMedianRecovery.BirdInteger.iterate_height line 99
  15. theorem OAI.MetricKMedianRecovery.BirdInteger.determinant_height line 110