Commit 2023-11-03 16:13 5db1ef31

View on Github →

feat: The four functions theorem (#7551) Prove the four functions theorem, aka Ahlswede-Daykin inequality, and derive the Holley, Fortuin-Kastelyn-Ginibre and Marica-Schönheim inequalities.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/FourFunctions.lean

added theorem Finset.card_le_card_diffs

added theorem Finset.le_card_diffs_mul_card_diffs

added theorem Finset.le_card_infs_mul_card_sups

added theorem collapse_eq

added theorem collapse_modular

added theorem collapse_nonneg

added theorem collapse_of_mem

added theorem fkg

added theorem four_functions_theorem

added theorem four_functions_theorem_univ

added theorem holley

added theorem le_collapse_of_insert_mem

added theorem le_collapse_of_mem

added theorem sum_collapse

Modified Mathlib/Data/Finset/Sups.lean

added theorem Finset.inter_mem_infs

added theorem Finset.powerset_infs_powerset_self

added theorem Finset.powerset_sups_powerset_self

added theorem Finset.union_mem_sups

added theorem Finset.univ_infs_univ

added theorem Finset.univ_sups_univ