[Merged by Bors] - feat: The Ahlswede-Zhang identity #8171
Conversation
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.
| /-- The infimum of the elements of `s` less than `a` if there are some, otherwise `⊥`. -/ | ||
| def truncatedInf (s : Finset α) (a : α) : α := | ||
| if h : a ∈ upperClosure s then (s.filter (· ≤ a)).inf' (inf_aux h) id else ⊥ |
There was a problem hiding this comment.
Can you explain why you add ⊥? The natural choice would seem to be top, since that's the inf of an empty set.
There was a problem hiding this comment.
This is why it's called "truncated". The theorem is not true otherwise.
Note this was already PRed to mathlib.
There was a problem hiding this comment.
Wait, so is this a forward-port PR?
There was a problem hiding this comment.
If the intent is not to actually forward-port it, we should just revert it in mathlib3 to get it off the dashboard
There was a problem hiding this comment.
I'm happy to make this a forward-port. But note that the second half of the file is not a forward-port
There was a problem hiding this comment.
In fact, it doesn't show up on the dashboard right now. So I'd be in favor of waiting for this PR to be merged before adding the aligns.
Co-authored-by: Eric Wieser <[email protected]>
leanprover-community-mathlib4-bot
added
the
merge-conflict
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
leanprover-community-mathlib4-bot
removed
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
|
bors merge |
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]>
|
Build failed (retrying...): |
|
Please merge |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Canceled. |
|
bors merge |
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]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
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.Co-authored-by: Vladimir Ivanov [email protected]
This is a rehash of leanprover-community/mathlib3#18612 and leanprover-community/mathlib3#18618.