OAI/Combinatorics/KMedianRecovery/Sampling/PrefixData.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.PhaseMergeInvariant.PrefixData line 13
  2. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.after_append line 21
  3. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.history_exact_eta line 27
  4. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.PrefixData.after_subset line 35
  5. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.PrefixData.mono_free line 39
  6. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.PrefixData.append_phase line 45
  7. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.PrefixData.append_exact line 61
  8. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.PrefixData.map line 78
  9. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.Attains.split line 101
  10. def OAI.MetricKMedianRecovery.PhaseMergeInvariant.Finished line 116
  11. def OAI.MetricKMedianRecovery.PhaseMergeInvariant.Solved line 120
  12. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.Solved.of_finished line 127
  13. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.Solved.pullback line 136
  14. lemma OAI.MetricKMedianRecovery.PhaseMergeInvariant.PrefixData.finish line 151