OAI/Combinatorics/BalancedRyser/Selection/SelectionOccupancyTail.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Selection.Process.positive_snapshot_surviving_update line 16
  2. theorem OAI.Balanced.Selection.Process.recorded_seen_on_support_path line 34
  3. theorem OAI.Balanced.Selection.Process.ae_occupancyPrefix_avoids_recorded line 66
  4. theorem OAI.Balanced.Selection.Process.remaining_lines_loss_le line 80
  5. theorem OAI.Balanced.Selection.Process.finalTracked_loss_le_remaining line 106
  6. theorem OAI.Balanced.Selection.Process.ae_completed_occupancy_loss line 127
  7. def OAI.Balanced.Selection.Process.recordedTracked line 143
  8. theorem OAI.Balanced.Selection.Process.ae_occupancyPrefix_subset_recorded line 148
  9. theorem OAI.Balanced.Selection.Process.surviving_recorded_occupancy_bound line 158
  10. theorem OAI.Balanced.Selection.Process.recorded_finalTracked_loss_le line 177
  11. theorem OAI.Balanced.Selection.Process.completion_occupancyMass_le_bad_recorded line 187