OAI/Combinatorics/BalancedRyser/Probability/CountingExposureKernel.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CountingExposureKernel.uniformSetWeight line 16
  2. theorem OAI.Balanced.CountingExposureKernel.uniformSetWeight_nonneg line 20
  3. theorem OAI.Balanced.CountingExposureKernel.sum_uniformSetWeight line 25
  4. theorem OAI.Balanced.CountingExposureKernel.uniformSetWeight_le line 31
  5. def OAI.Balanced.CountingExposureKernel.available line 40
  6. theorem OAI.Balanced.CountingExposureKernel.card_available line 42
  7. def OAI.Balanced.CountingExposureKernel.tokenWeight line 47
  8. theorem OAI.Balanced.CountingExposureKernel.tokenWeight_nonneg line 51
  9. theorem OAI.Balanced.CountingExposureKernel.sum_tokenWeight line 56
  10. def OAI.Balanced.CountingExposureKernel.tokenPMF line 64
  11. theorem OAI.Balanced.CountingExposureKernel.tokenPMF_real line 71
  12. theorem OAI.Balanced.CountingExposureKernel.tokenWeight_le_two_div line 77
  13. def OAI.Balanced.CountingExposureKernel.coverWeight line 116
  14. theorem OAI.Balanced.CountingExposureKernel.coverWeight_le_one_div_sq line 119
  15. theorem OAI.Balanced.CountingExposureKernel.cover_available_nonempty line 135
  16. theorem OAI.Balanced.CountingExposureKernel.sum_coverWeight line 144
  17. def OAI.Balanced.CountingExposureKernel.markedLines line 151
  18. theorem OAI.Balanced.CountingExposureKernel.markedLines_eq line 156
  19. theorem OAI.Balanced.CountingExposureKernel.marked_mass_le line 165
  20. theorem OAI.Balanced.CountingExposureKernel.token_marked_mass_le line 176
  21. theorem OAI.Balanced.CountingExposureKernel.cover_marked_mass_le line 190