mathlib3 documentation

combinatorics.set_family.compression.uv

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 #

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

References #

Tags #

compression, UV-compression, shadow

theorem sup_sdiff_inj_on {α : Type u_1} [generalized_boolean_algebra α] (u v : α) :
set.inj_on (λ (x : α), (x u) \ v) {x : α | disjoint u x v x}

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.

Equations

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

is_compressed u v s expresses that s is UV-compressed.

Equations
theorem uv.compress_of_disjoint_of_le {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] {u v a : α} (hua : disjoint u a) (hva : v a) :
uv.compress u v a = (a u) \ v
theorem uv.compress_of_disjoint_of_le' {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] {u v a : α} (hva : disjoint v a) (hua : u a) :
uv.compress u v ((a v) \ u) = a
theorem uv.mem_compression {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] {s : finset α} {u v a : α} :
a uv.compression u v s a s uv.compress u v a s a s (b : α) (H : b s), uv.compress u v b = a

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.

@[protected]

Any family is compressed along two identical elements.

@[simp]

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

theorem uv.compress_disjoint {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] {s : finset α} (u v : α) :
disjoint (finset.filter (λ (a : α), uv.compress u v a s) s) (finset.filter (λ (a : α), a s) (finset.image (uv.compress u v) s))
@[simp]

Compressing an element is idempotent.

@[simp]

Compressing a family is idempotent.

@[simp]

Compressing a family doesn't change its size.

theorem uv.le_of_mem_compression_of_not_mem {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] {s : finset α} {u v a : α} (h : a uv.compression u v s) (ha : a s) :
u a
theorem uv.sup_sdiff_mem_of_mem_compression {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] {s : finset α} {u v a : α} (ha : a uv.compression u v s) (hva : v a) (hua : disjoint u a) :
(a u) \ v s

If a is in the family compression and can be compressed, then its compression is in the original family.

theorem uv.mem_of_mem_compression {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] {s : finset α} {u v a : α} (ha : a uv.compression u v s) (hva : v a) (hvu : v = u = ) :
a s

If a is in the u, v-compression but v ≤ a, then a must have been in the original family.

UV-compression on finsets #

theorem uv.card_compress {α : Type u_1} [decidable_eq α] {u v : finset α} (hUV : u.card = v.card) (A : finset α) :

Compressing a finset doesn't change its size.

theorem uv.shadow_compression_subset_compression_shadow {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} (u v : finset α) (huv : (x : α), x u ( (y : α) (H : y v), uv.is_compressed (u.erase x) (v.erase y) 𝒜)) :

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.

theorem uv.card_shadow_compression_le {α : Type u_1} [decidable_eq α] {𝒜 : finset (finset α)} (u v : finset α) (huv : (x : α), x u ( (y : α) (H : y v), uv.is_compressed (u.erase x) (v.erase y) 𝒜)) :

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.