OAI/Combinatorics/ListHadwiger/FractionalSampling.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.Fractional.Dual.extend line 9
  2. theorem OAI.LinearListHadwiger.Fractional.induced_duality line 44
  3. lemma OAI.LinearListHadwiger.Fractional.Dual.restrict_sum line 63
  4. lemma OAI.LinearListHadwiger.Fractional.induced_number_le line 74
  5. lemma OAI.LinearListHadwiger.Fractional.induced_number_abs_sub_le line 98
  6. def OAI.LinearListHadwiger.Sampling.productMass line 113
  7. def OAI.LinearListHadwiger.Sampling.expectation line 114
  8. def OAI.LinearListHadwiger.Sampling.probability line 115
  9. lemma OAI.LinearListHadwiger.Sampling.productMass_nonneg line 118
  10. lemma OAI.LinearListHadwiger.Sampling.productMass_sum line 121
  11. lemma OAI.LinearListHadwiger.Sampling.expectation_product line 128
  12. lemma OAI.LinearListHadwiger.Sampling.expectation_coordinate line 135
  13. lemma OAI.LinearListHadwiger.Sampling.expectation_pair line 154
  14. lemma OAI.LinearListHadwiger.Sampling.expectation_nonneg line 182
  15. lemma OAI.LinearListHadwiger.Sampling.expectation_mono line 185
  16. lemma OAI.LinearListHadwiger.Sampling.expectation_sum line 189
  17. lemma OAI.LinearListHadwiger.Sampling.probability_eq_expectation line 194
  18. lemma OAI.LinearListHadwiger.Sampling.probability_nonneg line 202
  19. lemma OAI.LinearListHadwiger.Sampling.probability_mono line 207
  20. lemma OAI.LinearListHadwiger.Sampling.probability_coordinate line 217
  21. lemma OAI.LinearListHadwiger.Sampling.probability_union_le line 224
  22. lemma OAI.LinearListHadwiger.Sampling.probability_or_le line 242
  23. lemma OAI.LinearListHadwiger.Sampling.markov line 250
  24. lemma OAI.LinearListHadwiger.Sampling.exists_positive_avoiding line 264
  25. lemma OAI.LinearListHadwiger.Sampling.expectation_const line 288
  26. def OAI.LinearListHadwiger.Sampling.otherCopies line 291
  27. def OAI.LinearListHadwiger.Sampling.privateCopy line 294
  28. def OAI.LinearListHadwiger.Sampling.collision line 297
  29. lemma OAI.LinearListHadwiger.Sampling.collision_nonneg line 301
  30. lemma OAI.LinearListHadwiger.Sampling.expectation_collision line 309
  31. lemma OAI.LinearListHadwiger.Sampling.sum_on_eq line 343
  32. lemma OAI.LinearListHadwiger.Sampling.private_weight_loss line 351
  33. lemma OAI.LinearListHadwiger.Sampling.privateCopies_disjoint line 386
  34. theorem OAI.LinearListHadwiger.Sampling.private_fractional_failure line 396