OAI/Combinatorics/Ryser/Selection/Chunk.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Selection.equationLoss line 17
  2. def OAI.RyserCoveringCounterexample.Selection.lossByDirections line 20
  3. def OAI.RyserCoveringCounterexample.Selection.targetLoss line 26
  4. def OAI.RyserCoveringCounterexample.Selection.sourceLoss line 30
  5. def OAI.RyserCoveringCounterexample.Selection.entryLoss line 34
  6. def OAI.RyserCoveringCounterexample.Selection.frozenMass line 38
  7. def OAI.RyserCoveringCounterexample.Selection.sourceEnergy line 41
  8. theorem OAI.RyserCoveringCounterexample.Selection.equationLoss_nonneg line 45
  9. theorem OAI.RyserCoveringCounterexample.Selection.equationLoss_le line 49
  10. theorem OAI.RyserCoveringCounterexample.Selection.expectation_equationLoss line 54
  11. theorem OAI.RyserCoveringCounterexample.Selection.variance_equationLoss line 60
  12. theorem OAI.RyserCoveringCounterexample.Selection.sum_le_of_card_le line 66
  13. theorem OAI.RyserCoveringCounterexample.Selection.triple_sum_le line 74
  14. theorem OAI.RyserCoveringCounterexample.Selection.variance_sum_le_of_card_le line 88
  15. theorem OAI.RyserCoveringCounterexample.Selection.variance_triple_sum_le line 97
  16. theorem OAI.RyserCoveringCounterexample.Selection.lossByDirections_nonneg line 119
  17. theorem OAI.RyserCoveringCounterexample.Selection.lossByDirections_le line 127
  18. theorem OAI.RyserCoveringCounterexample.Selection.expectation_lossByDirections_le line 143
  19. theorem OAI.RyserCoveringCounterexample.Selection.entryLoss_nonneg line 162
  20. theorem OAI.RyserCoveringCounterexample.Selection.entryLoss_le line 168
  21. theorem OAI.RyserCoveringCounterexample.Selection.expectation_entryLoss_le line 178
  22. theorem OAI.RyserCoveringCounterexample.Selection.sourceEnergy_nonneg line 196
  23. theorem OAI.RyserCoveringCounterexample.Selection.variance_sourceLoss_le line 202
  24. def OAI.RyserCoveringCounterexample.Selection.targetDirectionGroup line 239
  25. theorem OAI.RyserCoveringCounterexample.Selection.targetDirectionGroup_nonneg line 244
  26. theorem OAI.RyserCoveringCounterexample.Selection.targetDirectionGroup_le line 250
  27. theorem OAI.RyserCoveringCounterexample.Selection.targetLoss_eq_sum_groups line 269
  28. theorem OAI.RyserCoveringCounterexample.Selection.variance_targetLoss_le line 288
  29. theorem OAI.RyserCoveringCounterexample.Selection.variance_entryLoss_le line 323