mathlib documentation

combinatorics.set_family.compression.uv

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 #

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

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 #

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

@[simp]
@[simp]
theorem uv.compression_self {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u : α) (s : finset α) :
𝓒 u u s = s

Any family is compressed along two identical elements.

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.

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 𝓒 u v s
@[simp]
theorem uv.compression_idem {α : Type u_1} [generalized_boolean_algebra α] [decidable_rel disjoint] [decidable_rel has_le.le] (u v : α) (s : finset α) :
𝓒 u v (𝓒 u v s) = 𝓒 u v s

Compressing a family is idempotent.

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

Compressing a family doesn't change its size.

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