Documentation

Mathlib.Combinatorics.SetFamily.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 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

theorem sup_sdiff_injOn {α : Type u_1} [GeneralizedBooleanAlgebra α] (u : α) (v : α) :
Set.InjOn (fun (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} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] (u : α) (v : α) (a : α) :
α

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
Instances For
    theorem UV.compress_of_disjoint_of_le {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {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} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {u : α} {v : α} {a : α} (hva : Disjoint v a) (hua : u a) :
    UV.compress u v ((a v) \ u) = a
    @[simp]
    theorem UV.compress_self {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] (u : α) (a : α) :
    UV.compress u u a = a
    @[simp]
    theorem UV.compress_sdiff_sdiff {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
    UV.compress (a \ b) (b \ a) b = a

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

    @[simp]
    theorem UV.compress_idem {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] (u : α) (v : α) (a : α) :

    Compressing an element is idempotent.

    def UV.compression {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableEq α] (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
    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
      Instances For
        def UV.IsCompressed {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableEq α] (u : α) (v : α) (s : Finset α) :

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

        Equations
        Instances For
          theorem UV.compress_injOn {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} [DecidableEq α] :
          Set.InjOn (UV.compress u v) (Finset.filter (fun (x : α) => UV.compress u v xs) s)

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

          theorem UV.mem_compression {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} {a : α} [DecidableEq α] :
          a UV.compression u v s a s UV.compress u v a s as bs, 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.

          theorem UV.IsCompressed.eq {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} [DecidableEq α] (h : UV.IsCompressed u v s) :
          @[simp]
          theorem UV.compression_self {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableEq α] (u : α) (s : Finset α) :
          theorem UV.isCompressed_self {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableEq α] (u : α) (s : Finset α) :

          Any family is compressed along two identical elements.

          theorem UV.compress_disjoint {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} [DecidableEq α] :
          Disjoint (Finset.filter (fun (x : α) => UV.compress u v x s) s) (Finset.filter (fun (x : α) => xs) (Finset.image (UV.compress u v) s))
          theorem UV.compress_mem_compression {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} {a : α} [DecidableEq α] (ha : a s) :
          theorem UV.compress_mem_compression_of_mem_compression {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} {a : α} [DecidableEq α] (ha : a UV.compression u v s) :
          @[simp]
          theorem UV.compression_idem {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableEq α] (u : α) (v : α) (s : Finset α) :

          Compressing a family is idempotent.

          @[simp]
          theorem UV.card_compression {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] [DecidableEq α] (u : α) (v : α) (s : Finset α) :
          (UV.compression u v s).card = s.card

          Compressing a family doesn't change its size.

          theorem UV.le_of_mem_compression_of_not_mem {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} {a : α} [DecidableEq α] (h : a UV.compression u v s) (ha : as) :
          u a
          theorem UV.disjoint_of_mem_compression_of_not_mem {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} {a : α} [DecidableEq α] (h : a UV.compression u v s) (ha : as) :
          theorem UV.sup_sdiff_mem_of_mem_compression_of_not_mem {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} {a : α} [DecidableEq α] (h : a UV.compression u v s) (ha : as) :
          (a v) \ u s
          theorem UV.sup_sdiff_mem_of_mem_compression {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} {a : α} [DecidableEq α] (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} [GeneralizedBooleanAlgebra α] [DecidableRel Disjoint] [DecidableRel fun (x1 x2 : α) => x1 x2] {s : Finset α} {u : α} {v : α} {a : α} [DecidableEq α] (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} [DecidableEq α] {u : Finset α} {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.

          theorem Set.Sized.uvCompression {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} {u : Finset α} {v : Finset α} {r : } (huv : u.card = v.card) (h𝒜 : Set.Sized r 𝒜) :
          Set.Sized r (UV.compression u v 𝒜)
          theorem UV.shadow_compression_subset_compression_shadow {α : Type u_1} [DecidableEq α] {𝒜 : Finset (Finset α)} (u : Finset α) (v : Finset α) (huv : xu, yv, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) :
          (UV.compression u v 𝒜).shadow UV.compression u v 𝒜.shadow

          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} [DecidableEq α] {𝒜 : Finset (Finset α)} (u : Finset α) (v : Finset α) (huv : xu, yv, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) :
          (UV.compression u v 𝒜).shadow.card 𝒜.shadow.card

          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.