OAI/Combinatorics/BalancedRyser/Profiles/ProfileScheduledMarks.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.ProfileScheduledMarks.label line 16
  2. def OAI.Balanced.ProfileScheduledMarks.prefixD line 19
  3. def OAI.Balanced.ProfileScheduledMarks.prefixC line 22
  4. def OAI.Balanced.ProfileScheduledMarks.unexposedD line 25
  5. def OAI.Balanced.ProfileScheduledMarks.unexposedC line 28
  6. def OAI.Balanced.ProfileScheduledMarks.stepD line 31
  7. def OAI.Balanced.ProfileScheduledMarks.stepC line 34
  8. def OAI.Balanced.ProfileScheduledMarks.zD line 37
  9. def OAI.Balanced.ProfileScheduledMarks.zC line 39
  10. def OAI.Balanced.ProfileScheduledMarks.ID line 41
  11. def OAI.Balanced.ProfileScheduledMarks.JD line 42
  12. def OAI.Balanced.ProfileScheduledMarks.IC line 43
  13. def OAI.Balanced.ProfileScheduledMarks.JC line 44
  14. theorem OAI.Balanced.ProfileScheduledMarks.current_not_ID line 47
  15. theorem OAI.Balanced.ProfileScheduledMarks.current_not_IC line 51
  16. theorem OAI.Balanced.ProfileScheduledMarks.prefixD_complement line 55
  17. theorem OAI.Balanced.ProfileScheduledMarks.prefixC_complement line 61
  18. theorem OAI.Balanced.ProfileScheduledMarks.prefixD_add_unexposedD line 67
  19. theorem OAI.Balanced.ProfileScheduledMarks.prefixC_add_unexposedC line 73
  20. theorem OAI.Balanced.ProfileScheduledMarks.unexposed_fraction_bounds line 80
  21. theorem OAI.Balanced.ProfileScheduledMarks.unexposedC_empty line 89
  22. theorem OAI.Balanced.ProfileScheduledMarks.prefixC_empty line 95
  23. def OAI.Balanced.ProfileScheduledMarks.sourceMarkCount line 99
  24. theorem OAI.Balanced.ProfileScheduledMarks.sourceMarkCount_le line 102
  25. theorem OAI.Balanced.ProfileScheduledMarks.sourceMarkCount_antitone line 106
  26. def OAI.Balanced.ProfileScheduledMarks.normalizedMean line 112
  27. theorem OAI.Balanced.ProfileScheduledMarks.normalizedMean_antitone line 115
  28. theorem OAI.Balanced.ProfileScheduledMarks.sum_zD line 124
  29. theorem OAI.Balanced.ProfileScheduledMarks.sum_zC line 130