OAI/Combinatorics/KMedian/Process/CopyState.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.CopyState.Copy line 13
  2. def OAI.MetricKMedian.CopyState.slots line 15
  3. theorem OAI.MetricKMedian.CopyState.mem_slots line 17
  4. theorem OAI.MetricKMedian.CopyState.card_slots line 25
  5. theorem OAI.MetricKMedian.CopyState.slots_disjoint line 29
  6. def OAI.MetricKMedian.CopyState.resets line 34
  7. theorem OAI.MetricKMedian.CopyState.mem_resets line 36
  8. theorem OAI.MetricKMedian.CopyState.card_resets line 39
  9. def OAI.MetricKMedian.CopyState.integral line 45
  10. theorem OAI.MetricKMedian.CopyState.mem_integral line 47
  11. def OAI.MetricKMedian.CopyState.next line 50
  12. theorem OAI.MetricKMedian.CopyState.reset_integral line 52
  13. theorem OAI.MetricKMedian.CopyState.integral_persists line 59
  14. theorem OAI.MetricKMedian.CopyState.reset_mass line 74
  15. theorem OAI.MetricKMedian.CopyState.integral_count line 79
  16. theorem OAI.MetricKMedian.CopyState.next_mass_le line 88
  17. theorem OAI.MetricKMedian.CopyState.next_mass_at_least_one line 100