Commit 2024-01-09 07:03 bb297ad1

View on Github →

feat: The Ahlswede-Zhang identity (#8171) The Ahlswede-Zhang identity is a sharpening of the Lubell-Yamamoto-Meshalkin inequality, by expliciting the correction term. This PR defines Finset.truncatedSup/Finset.truncatedInf, whose cardinalities show up in the correction term, and subsequently proves the Ahlswede-Zhang identity itself.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

added theorem AhlswedeZhang.IsAntichain.le_infSum

added def AhlswedeZhang.infSum

added theorem AhlswedeZhang.infSum_compls_add_supSum

added theorem AhlswedeZhang.infSum_eq_one

added theorem AhlswedeZhang.infSum_union_add_infSum_sups

added def AhlswedeZhang.supSum

added theorem AhlswedeZhang.supSum_of_not_univ_mem

added theorem AhlswedeZhang.supSum_singleton

added theorem AhlswedeZhang.supSum_union_add_supSum_infs

added theorem Finset.card_truncatedInf_union_add_card_truncatedInf_sups

added theorem Finset.card_truncatedSup_union_add_card_truncatedSup_infs

added theorem Finset.compl_truncatedInf

added theorem Finset.compl_truncatedSup

added theorem Finset.le_truncatedSup

added theorem Finset.map_truncatedInf

added theorem Finset.map_truncatedSup

added def Finset.truncatedInf

added theorem Finset.truncatedInf_empty

added theorem Finset.truncatedInf_le

added theorem Finset.truncatedInf_of_isAntichain

added theorem Finset.truncatedInf_of_mem

added theorem Finset.truncatedInf_of_not_mem

added theorem Finset.truncatedInf_singleton

added theorem Finset.truncatedInf_sups

added theorem Finset.truncatedInf_sups_of_not_mem

added theorem Finset.truncatedInf_union

added theorem Finset.truncatedInf_union_left

added theorem Finset.truncatedInf_union_of_not_mem

added theorem Finset.truncatedInf_union_right

added def Finset.truncatedSup

added theorem Finset.truncatedSup_empty

added theorem Finset.truncatedSup_infs

added theorem Finset.truncatedSup_infs_of_not_mem

added theorem Finset.truncatedSup_of_isAntichain

added theorem Finset.truncatedSup_of_mem

added theorem Finset.truncatedSup_of_not_mem

added theorem Finset.truncatedSup_singleton

added theorem Finset.truncatedSup_union

added theorem Finset.truncatedSup_union_left

added theorem Finset.truncatedSup_union_of_not_mem

added theorem Finset.truncatedSup_union_right