Insensitive word families and tilings

Boolean closure of insensitive families and the subspace-tiling results used in the density increment argument.

def DensityHalesJewett.InsensitiveEquiv {α : Type u_1} {ι : Type u_2} (i j : α) (x y : ι → α) : Prop

Two words are equivalent after freely interchanging the letters i and j.

Equations

• DensityHalesJewett.InsensitiveEquiv i j x y = ∀ (a : α), a ≠ i → a ≠ j → ∀ (c : ι), x c = a ↔ y c = a

def DensityHalesJewett.IsInsensitive {α : Type u_1} {ι : Type u_2} (i j : α) (D : Finset (ι → α)) : Prop

Membership in an (i,j)-insensitive family is constant on insensitive-equivalence classes.

Equations

• DensityHalesJewett.IsInsensitive i j D = ∀ ⦃x y : ι → α⦄, DensityHalesJewett.InsensitiveEquiv i j x y → (x ∈ D ↔ y ∈ D)

def DensityHalesJewett.transportWords {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} (e : ι ≃ ι') (D : Finset (ι → α)) : Finset (ι' → α)

Transport a word family along an equivalence of coordinate types.

Equations

• DensityHalesJewett.transportWords e D = Finset.map (e.arrowCongr (Equiv.refl α)).toEmbedding D

@[simp]

theorem DensityHalesJewett.mem_transportWords {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {e : ι ≃ ι'} {D : Finset (ι → α)} {w : ι' → α} : w ∈ transportWords e D ↔ w ∘ ⇑e ∈ D

@[simp]

theorem DensityHalesJewett.dens_transportWords {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Fintype (ι → α)] [Fintype (ι' → α)] (e : ι ≃ ι') (D : Finset (ι → α)) : (transportWords e D).dens = D.dens

theorem DensityHalesJewett.IsInsensitive.reindex {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {i j : α} {D : Finset (ι → α)} (e : ι ≃ ι') (hD : IsInsensitive i j D) : IsInsensitive i j (transportWords e D)

Reindexing coordinates preserves insensitivity.

theorem DensityHalesJewett.IsInsensitive.fiberSection {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [Fintype (κ → α)] [DecidableEq (ι ⊕ κ → α)] {i j : α} {D : Finset (ι ⊕ κ → α)} (hD : IsInsensitive i j D) (v : ι → α) : IsInsensitive i j (fiber D v)

Fixing a prefix of coordinates preserves insensitivity of the remaining section.

theorem DensityHalesJewett.IsInsensitive.compl {α : Type u_1} {ι : Type u_2} [Fintype (ι → α)] [DecidableEq (ι → α)] {i j : α} {D : Finset (ι → α)} (hD : IsInsensitive i j D) : IsInsensitive i j Dᶜ

Complements preserve insensitivity.

noncomputable def DensityHalesJewett.IsInsensitive.uncovered {η : Type u_1} {α : Type u_2} {ι : Type u_3} [Fintype (η → α)] [DecidableEq (ι → α)] (D : Finset (ι → α)) (𝒱 : Set (Combinatorics.Subspace η α ι)) : Finset (ι → α)

The part of D left uncovered by a set of subspaces.

Equations

• DensityHalesJewett.IsInsensitive.uncovered D 𝒱 = {w ∈ D | ∀ V ∈ 𝒱, w ∉ DensityHalesJewett.Subspace.range V}

noncomputable def DensityHalesJewett.IsInsensitive.intersection {r : ℕ} {X : Type u_1} [Fintype X] (D : Fin r → Finset X) : Finset X

The intersection of a finite indexed family of finite sets.

Equations

• DensityHalesJewett.IsInsensitive.intersection D = Finset.univ.inf D

@[simp]

theorem DensityHalesJewett.IsInsensitive.mem_intersection {r : ℕ} {X : Type u_1} [Fintype X] {D : Fin r → Finset X} {x : X} : x ∈ intersection D ↔ ∀ (i : Fin r), x ∈ D i

def DensityHalesJewett.IsInsensitive.TilingSufficient (k m : ℕ) (β : ℝ) (n : ℕ) : Prop

An ambient dimension is sufficient for tiling every dense one-pair insensitive family.

Equations

• One or more equations did not get rendered due to their size.

theorem DensityHalesJewett.IsInsensitive.sdiff {α : Type u_1} {ι : Type u_2} [DecidableEq (ι → α)] {i j : α} {D E : Finset (ι → α)} (hD : IsInsensitive i j D) (hE : IsInsensitive i j E) : IsInsensitive i j (D \ E)

Differences preserve insensitivity.

theorem DensityHalesJewett.IsInsensitive.fiber_congr {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [Fintype (κ → α)] [DecidableEq (ι ⊕ κ → α)] {i j : α} {D : Finset (ι ⊕ κ → α)} (hD : IsInsensitive i j D) {v w : ι → α} (hvw : InsensitiveEquiv i j v w) : fiber D v = fiber D w

Insensitive-equivalent prefixes have the same section.

theorem DensityHalesJewett.exists_isContained_of_insensitive {k m b : ℕ} (hDHJ : HasDensityHJ k) (hm : 1 ≤ m) (i : Fin k) {β : ℝ} (hβ : 0 < β) (hb : Subspace.restrictAlphabetBound k m β ≤ b) (E : Finset (Fin b → Fin (k + 1))) (hE : IsInsensitive i.castSucc (Fin.last k) E) (hdens : β ≤ ↑E.dens) : ∃ (V : Combinatorics.Subspace (Fin m) (Fin (k + 1)) (Fin b)), Subspace.IsContained V E

An insensitive family that is dense in a large enough block contains a full subspace: the restricted-alphabet subspace lemma supplies the Fin k-restricted range, and insensitivity upgrades containment to the whole parameter cube.

noncomputable def DensityHalesJewett.pickSubspace {k m b : ℕ} (hm : 1 ≤ m) (hmb : m ≤ b) (E : Finset (Fin b → Fin (k + 1))) : Combinatorics.Subspace (Fin m) (Fin (k + 1)) (Fin b)

A canonical subspace contained in a family, depending on nothing but the family.

Equations

• One or more equations did not get rendered due to their size.

theorem DensityHalesJewett.pickSubspace_isContained {k m b : ℕ} (hm : 1 ≤ m) (hmb : m ≤ b) {E : Finset (Fin b → Fin (k + 1))} (h : ∃ (V : Combinatorics.Subspace (Fin m) (Fin (k + 1)) (Fin b)), Subspace.IsContained V E) : Subspace.IsContained (pickSubspace hm hmb E) E

theorem DensityHalesJewett.IsInsensitive.exists_tilingSufficient_dimension (k m : ℕ) (hDHJ : HasDensityHJ k) (hm : 1 ≤ m) {β : ℝ} (hβ₀ : 0 < β) : ∃ (N : ℕ), TilingSufficient k m β N

Finite-stage block packing gives one exact sufficient dimension for one-family tiling.

theorem DensityHalesJewett.IsInsensitive.exists_eventually_tilingSufficient (k m : ℕ) (hDHJ : HasDensityHJ k) (hm : 1 ≤ m) {β : ℝ} (hβ₀ : 0 < β) : ∃ (N : ℕ), ∀ n ≥ N, TilingSufficient k m β n

One-family tiling sufficiency is upward closed after padding with unused final coordinates.

noncomputable def DensityHalesJewett.IsInsensitive.tilingBound (k m : ℕ) (β : ℝ) : ℕ

A sufficient ambient dimension for tiling one insensitive family. The tiling argument needs density Hales--Jewett for the smaller alphabet, so the witness is selected under HasDensityHJ k.

Equations

• DensityHalesJewett.IsInsensitive.tilingBound k m β = if h : DensityHalesJewett.HasDensityHJ k ∧ 1 ≤ m ∧ 0 < β then Nat.find ⋯ else 0

theorem DensityHalesJewett.IsInsensitive.tilingBound_spec (k m n : ℕ) (hDHJ : HasDensityHJ k) (hm : 1 ≤ m) {β : ℝ} (hβ₀ : 0 < β) (hn : tilingBound k m β ≤ n) : TilingSufficient k m β n

The selected one-family tiling bound satisfies the tiling predicate in every larger dimension.

theorem DensityHalesJewett.IsInsensitive.parameterPreimage_isInsensitive {α : Type u_1} {η : Type u_2} {ι : Type u_3} [Fintype (η → α)] {a b : α} (V : Combinatorics.Subspace η α ι) (D : Finset (ι → α)) (hD : IsInsensitive a b D) : IsInsensitive a b (parameterPreimage V D)

Pulling an insensitive family back through a subspace preserves its sensitivity pair.

theorem DensityHalesJewett.IsInsensitive.composed_inner_tiles_facts {k d M n : ℕ} (D : Finset (Fin n → Fin (k + 1))) (V : Combinatorics.Subspace (Fin M) (Fin (k + 1)) (Fin n)) (𝒲 : Set (Combinatorics.Subspace (Fin d) (Fin (k + 1)) (Fin M))) (h𝒲 : 𝒲.Finite) (hcontained : ∀ W ∈ 𝒲, Subspace.IsContained W (parameterPreimage V D)) (hpairwise : 𝒲.PairwiseDisjoint fun (W : Combinatorics.Subspace (Fin d) (Fin (k + 1)) (Fin M)) => ↑(Subspace.range W)) : have 𝒰 := Subspace.compose V '' 𝒲; 𝒰.Finite ∧ (∀ U ∈ 𝒰, Subspace.IsContained U D) ∧ 𝒰.PairwiseDisjoint fun (U : Combinatorics.Subspace (Fin d) (Fin (k + 1)) (Fin n)) => ↑(Subspace.range U)

Composing a finite disjoint family of inner tiles with one outer tile preserves finiteness, containment, and pairwise-disjointness.

def DensityHalesJewett.IsInsensitive.IntersectionTilingSufficient (k r m : ℕ) (β : ℝ) (n : ℕ) : Prop

An ambient dimension is sufficient for tiling every dense intersection of r insensitive families.

Equations

• One or more equations did not get rendered due to their size.

theorem DensityHalesJewett.IsInsensitive.exists_intersectionTilingSufficient_dimension (k r m : ℕ) (hDHJ : HasDensityHJ k) (hr₀ : 1 ≤ r) (hrk : r ≤ k) (hm : 1 ≤ m) {β : ℝ} (hβ₀ : 0 < β) : ∃ (N : ℕ), IntersectionTilingSufficient k r m β N

Induction on the number of insensitive families gives one exact sufficient intersection-tiling dimension.

theorem DensityHalesJewett.IsInsensitive.exists_eventually_intersectionTilingSufficient (k r m : ℕ) (hDHJ : HasDensityHJ k) (hr₀ : 1 ≤ r) (hrk : r ≤ k) (hm : 1 ≤ m) {β : ℝ} (hβ₀ : 0 < β) : ∃ (N : ℕ), ∀ n ≥ N, IntersectionTilingSufficient k r m β n

Intersection-tiling sufficiency is upward closed after padding with unused final coordinates.

noncomputable def DensityHalesJewett.IsInsensitive.intersectionTilingBound (k r m : ℕ) (β : ℝ) : ℕ

A sufficient ambient dimension for tiling an intersection of insensitive families, again selected under HasDensityHJ k.

Equations

• DensityHalesJewett.IsInsensitive.intersectionTilingBound k r m β = if h : DensityHalesJewett.HasDensityHJ k ∧ 1 ≤ r ∧ r ≤ k ∧ 1 ≤ m ∧ 0 < β then Nat.find ⋯ else 0

theorem DensityHalesJewett.IsInsensitive.intersectionTilingBound_spec (k r m n : ℕ) (hDHJ : HasDensityHJ k) (hr₀ : 1 ≤ r) (hrk : r ≤ k) (hm : 1 ≤ m) {β : ℝ} (hβ₀ : 0 < β) (hn : intersectionTilingBound k r m β ≤ n) : IntersectionTilingSufficient k r m β n

The selected intersection-tiling bound satisfies the tiling predicate in every larger dimension.

theorem DensityHalesJewett.IsInsensitive.exists_disjoint_subspaces_iInter {k : ℕ} (r m n : ℕ) (hDHJ : HasDensityHJ k) (hr₀ : 1 ≤ r) (hrk : r ≤ k) (hm : 1 ≤ m) (β : ℝ) (hβ₀ : 0 < β) (hn : intersectionTilingBound k r m β ≤ n) (D : Fin r → Finset (Fin n → Fin (k + 1))) (hD : ∀ (i : Fin r), IsInsensitive (Fin.castLE hrk i).castSucc (Fin.last k) (D i)) (hDβ : 2 * ↑r * β ≤ ↑(intersection D).dens) : ∃ (𝒱 : Set (Combinatorics.Subspace (Fin m) (Fin (k + 1)) (Fin n))), 𝒱.Finite ∧ (∀ V ∈ 𝒱, Subspace.IsContained V (intersection D)) ∧ (𝒱.PairwiseDisjoint fun (V : Combinatorics.Subspace (Fin m) (Fin (k + 1)) (Fin n)) => ↑(Subspace.range V)) ∧ ↑(uncovered (intersection D) 𝒱).dens < 2 * ↑r * β

An intersection of insensitive families can be tiled by disjoint subspaces.