OAI/Combinatorics/BalancedRyser/Probability/ExposureInterleaving.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.ExposureInterleaving.grid line 14
  2. def OAI.Balanced.ExposureInterleaving.countLE line 16
  3. def OAI.Balanced.ExposureInterleaving.countLT line 19
  4. theorem OAI.Balanced.ExposureInterleaving.grid_pos line 22
  5. theorem OAI.Balanced.ExposureInterleaving.grid_le_one line 27
  6. theorem OAI.Balanced.ExposureInterleaving.grid_strictMono line 32
  7. theorem OAI.Balanced.ExposureInterleaving.countLE_eq_floor line 39
  8. theorem OAI.Balanced.ExposureInterleaving.countLT_eq_ceil_sub_one line 61
  9. theorem OAI.Balanced.ExposureInterleaving.countLE_fraction_error line 83
  10. theorem OAI.Balanced.ExposureInterleaving.countLT_fraction_error line 93
  11. def OAI.Balanced.ExposureInterleaving.coverGrid line 116
  12. theorem OAI.Balanced.ExposureInterleaving.coverGrid_pos line 118
  13. theorem OAI.Balanced.ExposureInterleaving.coverGrid_le_one line 121
  14. theorem OAI.Balanced.ExposureInterleaving.coverGrid_rpow line 125
  15. theorem OAI.Balanced.ExposureInterleaving.coverGrid_strictMono line 129
  16. abbrev OAI.Balanced.ExposureInterleaving.Step line 135
  17. def OAI.Balanced.ExposureInterleaving.parameter line 137
  18. def OAI.Balanced.ExposureInterleaving.Before line 141
  19. def OAI.Balanced.ExposureInterleaving.remainingD line 147
  20. def OAI.Balanced.ExposureInterleaving.remainingC line 150
  21. theorem OAI.Balanced.ExposureInterleaving.remainingD_at_D line 153
  22. theorem OAI.Balanced.ExposureInterleaving.remainingC_at_C line 166
  23. theorem OAI.Balanced.ExposureInterleaving.remainingD_at_C line 179
  24. theorem OAI.Balanced.ExposureInterleaving.remainingC_at_D line 183
  25. theorem OAI.Balanced.ExposureInterleaving.parameter_pos line 191
  26. theorem OAI.Balanced.ExposureInterleaving.parameter_le_one line 197
  27. theorem OAI.Balanced.ExposureInterleaving.remainingD_fraction_error line 203
  28. theorem OAI.Balanced.ExposureInterleaving.remainingC_fraction_error line 215
  29. theorem OAI.Balanced.ExposureInterleaving.remainingC_zero line 230
  30. def OAI.Balanced.ExposureInterleaving.typeRank line 234
  31. theorem OAI.Balanced.ExposureInterleaving.before_iff line 238
  32. theorem OAI.Balanced.ExposureInterleaving.before_irrefl line 254
  33. theorem OAI.Balanced.ExposureInterleaving.before_trans line 257
  34. theorem OAI.Balanced.ExposureInterleaving.before_trichotomy line 267
  35. def OAI.Balanced.ExposureInterleaving.previousD line 293
  36. def OAI.Balanced.ExposureInterleaving.previousC line 296
  37. theorem OAI.Balanced.ExposureInterleaving.currentD_not_previousD line 299
  38. theorem OAI.Balanced.ExposureInterleaving.currentC_not_previousC line 303
  39. theorem OAI.Balanced.ExposureInterleaving.previousD_add_remainingD line 307
  40. theorem OAI.Balanced.ExposureInterleaving.previousC_add_remainingC line 313
  41. theorem OAI.Balanced.ExposureInterleaving.source_remaining_fraction_bounds line 319