OAI/Combinatorics/KMedianRecovery/Recovery/PhasesBounded.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedianRecovery.UniformDisablingEndpoint.phases_bounded line 11
  2. theorem OAI.MetricKMedianRecovery.UniformDisablingEndpoint.uniform_far line 33
  3. theorem OAI.MetricKMedianRecovery.UniformDisablingEndpoint.endpoint line 62
  4. def OAI.MetricKMedianRecovery.LeafMetric.parent line 105
  5. def OAI.MetricKMedianRecovery.LeafMetric.height line 107
  6. def OAI.MetricKMedianRecovery.LeafMetric.leafDist line 109
  7. lemma OAI.MetricKMedianRecovery.LeafMetric.height_nonneg line 114
  8. lemma OAI.MetricKMedianRecovery.LeafMetric.leafDist_self line 119
  9. lemma OAI.MetricKMedianRecovery.LeafMetric.leafDist_nonneg line 121
  10. lemma OAI.MetricKMedianRecovery.LeafMetric.leafDist_comm line 127
  11. lemma OAI.MetricKMedianRecovery.LeafMetric.leafDist_triangle line 134
  12. def OAI.MetricKMedianRecovery.LeafMetric.attachedMetric line 152
  13. lemma OAI.MetricKMedianRecovery.LeafMetric.original_distance line 159
  14. lemma OAI.MetricKMedianRecovery.LeafMetric.copy_distance line 164
  15. lemma OAI.MetricKMedianRecovery.LeafMetric.copies_distance line 167
  16. lemma OAI.MetricKMedianRecovery.LeafMetric.parent_nonexpansive line 171
  17. lemma OAI.MetricKMedianRecovery.LeafMetric.shorten_distance line 178
  18. lemma OAI.MetricKMedianRecovery.LeafMetric.shorten_distance_loss line 184