Finite patterns and rectangle complexity

Section 1 and the notation in Section 1.1 of paper/nivat.tex.

patterns is the range of the restriction map over every integer translation. The basic API proves finiteness, restriction surjectivity, monotonicity and invariance under translations and injective relabeling. Unique extension is the counting step used in Lemma 5.5 (lem:boundary-window).

def Nivat.rectangle (m n : ℕ) : Finset Lattice

The window Rₘ,ₙ = {0, …, m-1} × {0, …, n-1} from Section 1.

Equations

• Nivat.rectangle m n = (Finset.Ico 0 ↑m).product (Finset.Ico 0 ↑n)

@[simp]

theorem Nivat.mem_rectangle (z : Lattice) (m n : ℕ) : z ∈ rectangle m n ↔ 0 ≤ z.1 ∧ z.1 < ↑m ∧ 0 ≤ z.2 ∧ z.2 < ↑n

Coordinate inequalities describing the rectangle of Section 1.

@[simp]

theorem Nivat.card_rectangle (m n : ℕ) : (rectangle m n).card = m * n

The rectangle Rₘ,ₙ has m * n sites (Section 1).

def Nivat.patternAt {A : Type u_1} (c : Configuration A) (D : Finset Lattice) (u : Lattice) : ↥D → A

The restriction of Tᵘc to D, indexed by the sites of D (Section 1).

Equations

• Nivat.patternAt c D u z = c (↑z + u)

def Nivat.patterns {A : Type u_1} (c : Configuration A) (D : Finset Lattice) : Set (↥D → A)

The set Pat_c(D) of distinct restrictions over all lattice translations (Section 1).

Equations

• Nivat.patterns c D = Set.range (Nivat.patternAt c D)

noncomputable def Nivat.complexity {A : Type u_1} (c : Configuration A) (D : Finset Lattice) : ℕ

The pattern count P_c(D) from Section 1. For finite-range configurations, patterns_finite ensures that natural set cardinality counts this finite set; repeated occurrences contribute only one pattern.

Equations

• Nivat.complexity c D = (Nivat.patterns c D).ncard

noncomputable def Nivat.discrepancy {A : Type u_1} (c : Configuration A) (D : Finset Lattice) : ℤ

The signed discrepancy δ_c(D) = P_c(D) - |D| from Section 1.1.

Equations

• Nivat.discrepancy c D = ↑(Nivat.complexity c D) - ↑D.card

theorem Nivat.patterns_nonempty {A : Type u_1} (c : Configuration A) (D : Finset Lattice) : (patterns c D).Nonempty

The origin supplies an occurring pattern on every window (Section 1.1).

theorem Nivat.patterns_finite {A : Type u_1} {c : Configuration A} (hc : FiniteRange c) (D : Finset Lattice) : (patterns c D).Finite

A finite alphabet gives finitely many patterns on a finite window (Section 1.1).

theorem Nivat.complexity_pos {A : Type u_1} {c : Configuration A} (hc : FiniteRange c) (D : Finset Lattice) : 0 < complexity c D

Every finite window has at least one occurring pattern (Section 1.1).

@[simp]

theorem Nivat.complexity_empty {A : Type u_1} (c : Configuration A) : complexity c ∅ = 1

The empty window has exactly one pattern (Section 1.1).

theorem Nivat.patterns_shift {A : Type u_1} (c : Configuration A) (D : Finset Lattice) (h : Lattice) : patterns (shift h c) D = patterns c D

Translations of the configuration preserve its pattern sets (Section 1.1).

@[simp]

theorem Nivat.complexity_shift {A : Type u_1} (c : Configuration A) (D : Finset Lattice) (h : Lattice) : complexity (shift h c) D = complexity c D

Translations of the configuration preserve complexity (Section 1.1).

def Nivat.restrictPattern {A : Type u_1} {C D : Finset Lattice} (hCD : C ⊆ D) (p : ↥D → A) : ↥C → A

Restriction of a pattern to a smaller window (Section 1.1).

Equations

• Nivat.restrictPattern hCD p z = p ⟨↑z, ⋯⟩

theorem Nivat.restrict_patterns {A : Type u_1} (c : Configuration A) {C D : Finset Lattice} (hCD : C ⊆ D) : restrictPattern hCD '' patterns c D = patterns c C

Restriction maps onto all occurring patterns on the smaller window (Section 1.1).

theorem Nivat.complexity_mono {A : Type u_1} {c : Configuration A} (hc : FiniteRange c) {C D : Finset Lattice} (hCD : C ⊆ D) : complexity c C ≤ complexity c D

Pattern complexity is monotone under inclusion of windows (Section 1.1).

theorem Nivat.patterns_map {A : Type u_1} {B : Type u_2} (c : Configuration A) (f : A → B) (D : Finset Lattice) : patterns (f ∘ c) D = (fun (p : ↥D → A) => f ∘ p) '' patterns c D

The effect of relabeling symbols on the occurring patterns (Section 1.1).

theorem Nivat.complexity_map {A : Type u_1} {B : Type u_2} (c : Configuration A) {f : A → B} (hf : Function.Injective f) (D : Finset Lattice) : complexity (f ∘ c) D = complexity c D

Injective alphabet labeling preserves every finite-window complexity (Section 1.1).

theorem Nivat.equal_complexity_unique_extension {A : Type u_1} {c : Configuration A} (hc : FiniteRange c) {C D : Finset Lattice} (hCD : C ⊆ D) (hcard : complexity c C = complexity c D) {u v : Lattice} (huv : patternAt c C u = patternAt c C v) : patternAt c D u = patternAt c D v

Equal pattern counts imply unique extension between the two windows. This is the restriction-bijection step in Lemma 5.5 (lem:boundary-window).

theorem Nivat.patternAt_mem_of_language {A : Type u_1} {x c : Configuration A} (hx : ∀ (D : Finset Lattice), patternAt x D 0 ∈ patterns c D) (D : Finset Lattice) (u : Lattice) : patternAt x D u ∈ patterns c D

Occurrence of every finite origin pattern implies occurrence at every translate. This implements the finite-pattern inheritance used in Theorem 2.2 (thm:descent).

theorem Nivat.complexity_translate_window {A : Type u_1} (c : Configuration A) (D : Finset Lattice) (u : Lattice) : complexity c (Finset.image (fun (z : Lattice) => z + u) D) = complexity c D

Translating the window preserves its complexity (Section 1.1).