feat: The Ahlswede-Zhang identity (#8171)

The Ahlswede-Zhang identity is a sharpening of the [Lubell-Yamamoto-Meshalkin inequality](https://leanprover-community.github.io/mathlib_docs/combinatorics/set_family/lym.html#finset.sum_card_slice_div_choose_le_one), 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. Co-authored-by: Vladimir Ivanov <[email protected]>
leanprover-community · Jan 9, 2024 · bb297ad · bb297ad
1 parent ef72bdb
commit bb297ad
Show file tree

Hide file tree

Showing 2 changed files with 426 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1355,6 +1355,7 @@ import Mathlib.Combinatorics.Quiver.SingleObj
 import Mathlib.Combinatorics.Quiver.Subquiver
 import Mathlib.Combinatorics.Quiver.Symmetric
 import Mathlib.Combinatorics.Schnirelmann
+import Mathlib.Combinatorics.SetFamily.AhlswedeZhang
 import Mathlib.Combinatorics.SetFamily.CauchyDavenport
 import Mathlib.Combinatorics.SetFamily.Compression.Down
 import Mathlib.Combinatorics.SetFamily.Compression.UV