OAI/Combinatorics/ExpectationThreshold/Basic.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TalagrandThreshold.cost_empty line 14
  2. theorem OAI.TalagrandThreshold.cost_singleton line 18
  3. theorem OAI.TalagrandThreshold.cost_nonneg line 22
  4. theorem OAI.TalagrandThreshold.cost_mono line 26
  5. theorem OAI.TalagrandThreshold.cost_union_le line 31
  6. theorem OAI.TalagrandThreshold.cost_biUnion_le line 39
  7. theorem OAI.TalagrandThreshold.cost_image_le line 49
  8. theorem OAI.TalagrandThreshold.cost_mono_density line 55
  9. theorem OAI.TalagrandThreshold.covers_self line 60
  10. theorem OAI.TalagrandThreshold.covers_empty line 64
  11. theorem OAI.TalagrandThreshold.Covers.mono_target line 69
  12. theorem OAI.TalagrandThreshold.Covers.mono_cover line 73
  13. theorem OAI.TalagrandThreshold.Covers.union line 80
  14. theorem OAI.TalagrandThreshold.small_empty line 90
  15. theorem OAI.TalagrandThreshold.Small.mono line 95
  16. theorem OAI.TalagrandThreshold.cost_gt_of_not_small line 101
  17. theorem OAI.TalagrandThreshold.members_nonempty line 106
  18. theorem OAI.TalagrandThreshold.cost_zero_of_empty_not_mem line 113
  19. theorem OAI.TalagrandThreshold.small_zero line 120
  20. theorem OAI.TalagrandThreshold.Increasing.empty_not_mem line 126
  21. def OAI.TalagrandThreshold.coverIndicator line 134
  22. theorem OAI.TalagrandThreshold.coverIndicator_nonneg line 137
  23. theorem OAI.TalagrandThreshold.coverIndicator_le_one line 143
  24. theorem OAI.TalagrandThreshold.Covers.fractionalCover line 149
  25. theorem OAI.TalagrandThreshold.fracCost_coverIndicator line 160
  26. theorem OAI.TalagrandThreshold.Small.fractionalSmall line 172
  27. theorem OAI.TalagrandThreshold.fractionalSmall_zero line 177
  28. theorem OAI.TalagrandThreshold.FractionalCover.nonneg line 181
  29. theorem OAI.TalagrandThreshold.FractionalCover.le_one line 185
  30. theorem OAI.TalagrandThreshold.fracCost_nonneg line 189
  31. theorem OAI.TalagrandThreshold.fracCost_mono_density line 194
  32. theorem OAI.TalagrandThreshold.FractionalSmall.mono line 201
  33. theorem OAI.TalagrandThreshold.empty_weight_le_fracCost line 207