# UV-compressions #

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`

is`a`

compressed along`u`

and`v`

.`UV.compression`

:`compression u v s`

is the compression of the set family`s`

along`u`

and`v`

. It is the compressions of the elements of`s`

whose compression is not already in`s`

along with the element whose compression is already in`s`

. This way of splitting into what moves and what does not ensures the compression doesn't squash the set family, which is proved by`UV.card_compression`

.`UV.card_shadow_compression_le`

: Compressing reduces the size of the shadow. This is a key fact in the proof of Kruskal-Katona.

## Notation #

`𝓒`

(typed with `\MCC`

) is notation for `UV.compression`

in locale `FinsetFamily`

.

## 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 α`

.

## References #

## Tags #

compression, UV-compression, shadow

UV-compression is injective on the elements it moves. See `UV.compress`

.

### UV-compression in generalized boolean algebras #

UV-compressing `a`

means removing `v`

from it and adding `u`

if `a`

and `u`

are disjoint and
`v ≤ a`

(it replaces the `v`

part of `a`

by the `u`

part). Else, UV-compressing `a`

doesn't do
anything. This is most useful when `u`

and `v`

are disjoint finsets of the same size.

## Instances For

An element can be compressed to any other element by removing/adding the differences.

Compressing an element is idempotent.

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 (fun (x : α) => UV.compress u v x ∈ s) s ∪ Finset.filter (fun (x : α) => x ∉ s) (Finset.image (UV.compress u v) s)

## Instances For

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

- FinsetFamily.term𝓒 = Lean.ParserDescr.node `FinsetFamily.term𝓒 1024 (Lean.ParserDescr.symbol "𝓒 ")

## Instances For

`IsCompressed u v s`

expresses that `s`

is UV-compressed.

## Equations

- UV.IsCompressed u v s = (UV.compression u v s = s)

## Instances For

UV-compression is injective on the sets that are not UV-compressed.

`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 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.

UV-compression reduces the size of the shadow of `𝒜`

if, for all `x ∈ u`

there is `y ∈ v`

such
that `𝒜`

is `(u.erase x, v.erase y)`

-compressed. This is the key fact about compression for
Kruskal-Katona.

UV-compression reduces the size of the shadow of `𝒜`

if, for all `x ∈ u`

there is `y ∈ v`

such that `𝒜`

is `(u.erase x, v.erase y)`

-compressed. This is the key UV-compression fact needed for
Kruskal-Katona.