UV-compressions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines UV-compression. It is an operation on a set family that reduces its shadow.
UV-compressing a : α
along u v : α
means replacing a
by (a ⊔ u) \ v
if a
and u
are
disjoint and v ≤ a
. In some sense, it's moving a
from v
to u
.
UV-compressions are immensely useful to prove the Kruskal-Katona theorem. The idea is that compressing a set family might decrease the size of its shadow, so iterated compressions hopefully minimise the shadow.
Main declarations #
uv.compress
:compress u v a
isa
compressed alongu
andv
.uv.compression
:compression u v s
is the compression of the set familys
alongu
andv
. It is the compressions of the elements ofs
whose compression is not already ins
along with the element whose compression is already ins
. This way of splitting into what moves and what does not ensures the compression doesn't squash the set family, which is proved byuv.card_compress
.
Notation #
𝓒
(typed with \MCC
) is notation for uv.compression
in locale finset_family
.
Notes #
Even though our emphasis is on finset α
, we define UV-compressions more generally in a generalized
boolean algebra, so that one can use it for set α
.
TODO #
Prove that compressing reduces the size of shadow. This result and some more already exist on the
branch combinatorics
.
References #
Tags #
compression, UV-compression, shadow
UV-compression is injective on the elements it moves. See uv.compress
.
UV-compression in generalized boolean algebras #
To UV-compress a
, if it doesn't touch U
and does contain V
, we remove V
and
put U
in. We'll only really use this when |U| = |V|
and U ∩ V = ∅
.
To UV-compress a set family, we compress each of its elements, except that we don't want to reduce the cardinality, so we keep all elements whose compression is already present.
Equations
- uv.compression u v s = finset.filter (λ (a : α), uv.compress u v a ∈ s) s ∪ finset.filter (λ (a : α), a ∉ s) (finset.image (uv.compress u v) s)
is_compressed u v s
expresses that s
is UV-compressed.
Equations
- uv.is_compressed u v s = (uv.compression u v s = s)
a
is in the UV-compressed family iff it's in the original and its compression is in the
original, or it's not in the original but it's the compression of something in the original.
Any family is compressed along two identical elements.
Compressing an element is idempotent.
Compressing a family is idempotent.
Compressing a family doesn't change its size.
If a
is in the family compression and can be compressed, then its compression is in the
original family.
If a
is in the u, v
-compression but v ≤ a
, then a
must have been in the original
family.
UV-compression on finsets #
Compressing a finset doesn't change its size.