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

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

source
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 #

source
def uv.compress {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u v a : α) :
α

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 = ∅.

Equations
source
def uv.compression {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u v : α) (s : finset α) :
finset α

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
source
def uv.is_compressed {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u v : α) (s : finset α) :
Prop

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

Equations
source
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
source
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.

source
@[simp]
theorem uv.compress_self {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u a : α) :
uv.compress u u a = a
source
@[simp]
theorem uv.compression_self {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u : α) (s : finset α) :
uv.compression u u s = s
source
theorem uv.is_compressed_self {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u : α) (s : finset α) :
uv.is_compressed u u s

Any family is compressed along two identical elements.

source
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))
source
@[simp]
theorem uv.compress_idem {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u v a : α) :
uv.compress u v (uv.compress u v a) = uv.compress u v a

Compressing an element is idempotent.

source
theorem uv.compress_mem_compression {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] {s : finset α} {u v a : α} (ha : a ∈ s) :
uv.compress u v a ∈ uv.compression u v s
source
theorem uv.compress_mem_compression_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) :
uv.compress u v a ∈ uv.compression u v s
source
@[simp]
theorem uv.compression_idem {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u v : α) (s : finset α) :
uv.compression u v (uv.compression u v s) = uv.compression u v s

Compressing a family is idempotent.

source
theorem uv.card_compression {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u v : α) (s : finset α) :
(uv.compression u v s).card = s.card

Compressing a family doesn't change its size.

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

source
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 #

source
theorem uv.card_compress {α : Type u_1} [decidable_eq α] {U V : finset α} (hUV : U.card = V.card) (A : finset α) :
(uv.compress U V A).card = A.card

Compressing a finset doesn't change its size.