OAI/Combinatorics/DiscreteConvexity/Basic.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TalagrandDiscreteConvexity.bernoulliMass_nonneg line 13
2. theorem OAI.TalagrandDiscreteConvexity.familyMeasure_nonneg line 17
3. theorem OAI.TalagrandDiscreteConvexity.familyMeasure_empty line 21
4. theorem OAI.TalagrandDiscreteConvexity.familyMeasure_mono line 24
5. theorem OAI.TalagrandDiscreteConvexity.cost_empty line 30
6. theorem OAI.TalagrandDiscreteConvexity.cost_singleton line 34
7. theorem OAI.TalagrandDiscreteConvexity.cost_nonneg line 38
8. theorem OAI.TalagrandDiscreteConvexity.cost_mono line 42
9. theorem OAI.TalagrandDiscreteConvexity.cost_union_le line 47
10. theorem OAI.TalagrandDiscreteConvexity.cost_biUnion_le line 56
11. theorem OAI.TalagrandDiscreteConvexity.cost_image_le line 66
12. theorem OAI.TalagrandDiscreteConvexity.covers_self line 72
13. theorem OAI.TalagrandDiscreteConvexity.covers_empty line 76
14. theorem OAI.TalagrandDiscreteConvexity.Covers.mono_target line 81
15. theorem OAI.TalagrandDiscreteConvexity.Covers.mono_cover line 85
16. theorem OAI.TalagrandDiscreteConvexity.Covers.union line 92
17. theorem OAI.TalagrandDiscreteConvexity.small_empty line 102
18. theorem OAI.TalagrandDiscreteConvexity.mem_unionTuple line 107
19. theorem OAI.TalagrandDiscreteConvexity.subset_unionTuple line 112
20. theorem OAI.TalagrandDiscreteConvexity.unionTuple_subset_iff line 116
21. theorem OAI.TalagrandDiscreteConvexity.mem_unionFamily line 125
22. theorem OAI.TalagrandDiscreteConvexity.mem_exceptional line 131
23. theorem OAI.TalagrandDiscreteConvexity.mem_exceptional_iff_unionFamily line 137
24. theorem OAI.TalagrandDiscreteConvexity.exceptional_tuple_misses line 148
25. theorem OAI.TalagrandDiscreteConvexity.exceptional_antitone line 154
26. theorem OAI.TalagrandDiscreteConvexity.exceptional_eq_empty_of_full_union line 161
27. theorem OAI.TalagrandDiscreteConvexity.mem_cubeSet line 169
28. theorem OAI.TalagrandDiscreteConvexity.cubeSet_decide line 172
29. theorem OAI.TalagrandDiscreteConvexity.familyIndicator_nonneg line 177
30. theorem OAI.TalagrandDiscreteConvexity.familyIndicator_le_one line 182
31. theorem OAI.TalagrandDiscreteConvexity.familyIndicator_sq line 187