Pattern complexity under a Laurent operator

Section 2 of paper/nivat.tex.

• multiplierMap_injective completes the dimension calculation in Lemma 2.1.
• localFilter_transpose identifies the transpose with Laurent multiplication.
• translatedSpan_eq_ker proves equation eq:full-kernel.
• exact_complexity_descent is Theorem 2.2 (thm:descent).
• exists_smaller_low_complexity_rectangle is Corollary 2.3 (cor:line-descent).

The geometry of supported multiples is in Nivat.Algebra.RectangleSupport; the finite fiber-counting argument is in Nivat.Descent.FiberBudget.

noncomputable def Nivat.Descent.translatedSpan (d : Configuration ℚ) (R : Finset Lattice) : Submodule ℚ (↥R → ℚ)

The space V_R(d) spanned by all translated restrictions of d. Defined in the proof of Theorem 2.2 (thm:descent).

Equations

• Nivat.Descent.translatedSpan d R = Submodule.span ℚ (Nivat.patterns d R)

theorem Nivat.Descent.dotProduct_mem_dualAnnihilator_iff (d : Configuration ℚ) (R : Finset Lattice) (b : ↥R → ℚ) : (dotProductEquiv ℚ ↥R) b ∈ (translatedSpan d R).dualAnnihilator ↔ Algebra.act (Algebra.windowPolynomial R b) d = 0

A coefficient vector annihilates V_R(d) exactly when its polynomial annihilates d. This is the perpendicular-space identification in Theorem 2.2 (thm:descent).

def Nivat.Descent.coefficientRestriction (R : Finset Lattice) : Laurent →ₗ[ℚ] ↥R → ℚ

Restrict Laurent coefficients to a finite window. This implements the identification with ℚ^R at the start of Section 2.

Equations

• Nivat.Descent.coefficientRestriction R = { toFun := fun (f : Nivat.Laurent) (z : ↥R) => f.coeff ↑z, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Nivat.Descent.multiplierMap (Φ : Laurent) (R S : Finset Lattice) : (↥S → ℚ) →ₗ[ℚ] ↥R → ℚ

Multiplication by Φ on polynomials supported in S, with coefficients read on R. This is the map Φ : ℚ^S → ℚ^R in Lemma 2.1 (lem:supported).

Equations

• Nivat.Descent.multiplierMap Φ R S = Nivat.Descent.coefficientRestriction R ∘ₗ LinearMap.mulLeft ℚ Φ ∘ₗ Nivat.Algebra.windowPolynomialLinear S

theorem Nivat.Descent.multiplierMap_apply (Φ : Laurent) (R S : Finset Lattice) (b : ↥S → ℚ) (z : ↥R) : (multiplierMap Φ R S) b z = (Φ * Algebra.windowPolynomial S b).coeff ↑z

The coefficient formula for multiplication in Lemma 2.1 (lem:supported).

theorem Nivat.Descent.multiplierMap_injective (Φ : Laurent) (hΦ : Φ ≠ 0) (R S : Finset Lattice) (hfit : ∀ (g : Laurent), (Φ * g).coeff.support ⊆ R ↔ g.coeff.support ⊆ S) : Function.Injective ⇑(multiplierMap Φ R S)

Multiplication by a nonzero Laurent polynomial is injective. This gives the dimension |S| in Lemma 2.1 (lem:supported).

theorem Nivat.Descent.dualAnnihilator_eq_multiplier_range (d : Configuration ℚ) (Φ : Laurent) (R S : Finset Lattice) (hexact : ∀ (f : Laurent), Algebra.act f d = 0 ↔ Φ ∣ f) (hfit : ∀ (g : Laurent), (Φ * g).coeff.support ⊆ R ↔ g.coeff.support ⊆ S) : (translatedSpan d R).dualAnnihilator = (↑(dotProductEquiv ℚ ↥R) ∘ₗ multiplierMap Φ R S).range

The perpendicular space of V_R(d) is the image of multiplication by Φ. This is the chain of equalities preceding eq:full-kernel in Theorem 2.2.

theorem Nivat.Descent.translatedSpan_finrank_add (d : Configuration ℚ) (Φ : Laurent) (hΦ : Φ ≠ 0) (R S : Finset Lattice) (hexact : ∀ (f : Laurent), Algebra.act f d = 0 ↔ Φ ∣ f) (hfit : ∀ (g : Laurent), (Φ * g).coeff.support ⊆ R ↔ g.coeff.support ⊆ S) : Module.finrank ℚ ↥(translatedSpan d R) + S.card = R.card

The dimension identity dim V_R(d) + |S| = |R| in Theorem 2.2 (thm:descent). Together with translatedSpan_eq_ker, this is equation eq:filter-dimension. The additive form also covers an empty eroded window.

noncomputable def Nivat.Descent.localFilter (Φ : Laurent) (R S : Finset Lattice) (hS : ∀ z ∈ S, ∀ a ∈ Φ.coeff.support, z + a ∈ R) : (↥R → ℚ) →ₗ[ℚ] ↥S → ℚ

The map F : ℚ^R → ℚ^S induced by the Laurent operator. Defined in Theorem 2.2 (thm:descent); hS ensures every sampled input lies in R.

Equations

• Nivat.Descent.localFilter Φ R S hS = { toFun := fun (p : ↥R → ℚ) (z : ↥S) => ∑ a : ↥Φ.coeff.support, Φ.coeff ↑a * p ⟨↑z + ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem Nivat.Descent.localFilter_patternAt (Φ : Laurent) (R S : Finset Lattice) (hS : ∀ z ∈ S, ∀ a ∈ Φ.coeff.support, z + a ∈ R) (c : Configuration ℚ) (u : Lattice) : (localFilter Φ R S hS) (patternAt c R u) = patternAt (Algebra.act Φ c) S u

Filtering an occurring input pattern gives the corresponding output pattern. This is shift commutation in the proof of Theorem 2.2 (thm:descent).

theorem Nivat.Descent.localFilter_patterns_image (Φ : Laurent) (R S : Finset Lattice) (hS : ∀ z ∈ S, ∀ a ∈ Φ.coeff.support, z + a ∈ R) (c : Configuration ℚ) : ⇑(localFilter Φ R S hS) '' patterns c R = patterns (Algebra.act Φ c) S

The image of all occurring input patterns is exactly the output pattern set. This is F(Pat_c(R)) = Pat_{Φ(T)c}(S) in Theorem 2.2 (thm:descent).

theorem Nivat.Descent.localFilter_transpose (Φ : Laurent) (R S : Finset Lattice) (hfit : ∀ (g : Laurent), (Φ * g).coeff.support ⊆ R ↔ g.coeff.support ⊆ S) (hS : ∀ z ∈ S, ∀ a ∈ Φ.coeff.support, z + a ∈ R) : (localFilter Φ R S hS).dualMap ∘ₗ ↑(dotProductEquiv ℚ ↥S) = ↑(dotProductEquiv ℚ ↥R) ∘ₗ multiplierMap Φ R S

The transpose of the local filter is multiplication by Φ, after identifying coefficient vectors with their dot-product functionals. This is the transpose identity in the proof of Theorem 2.2 (thm:descent).

theorem Nivat.Descent.translatedSpan_eq_ker (d : Configuration ℚ) (Φ : Laurent) (R S : Finset Lattice) (hexact : ∀ (f : Laurent), Algebra.act f d = 0 ↔ Φ ∣ f) (hfit : ∀ (g : Laurent), (Φ * g).coeff.support ⊆ R ↔ g.coeff.support ⊆ S) (hS : ∀ z ∈ S, ∀ a ∈ Φ.coeff.support, z + a ∈ R) : translatedSpan d R = (localFilter Φ R S hS).ker

The translated restrictions of d span the full kernel of the local filter. This is equation eq:full-kernel in Theorem 2.2 (thm:descent).

theorem Nivat.Descent.exact_complexity_descent (c : Configuration ℚ) (hc : FiniteRange c) (x y : Configuration ℚ) (hx : ∀ (D : Finset Lattice), patternAt x D 0 ∈ patterns c D) (hy : ∀ (D : Finset Lattice), patternAt y D 0 ∈ patterns c D) (Φ : Laurent) (hΦ : Φ ≠ 0) (hexact : ∀ (f : Laurent), Algebra.act f (x - y) = 0 ↔ Φ ∣ f) (m n : ℕ) : complexity (Algebra.act Φ c) (Algebra.erodedWindow Φ hΦ (rectangle m n)) + (rectangle m n).card ≤ complexity c (rectangle m n) + (Algebra.erodedWindow Φ hΦ (rectangle m n)).card

Theorem 2.2 (thm:descent): exact complexity descent on a rectangle. The orbit-closure hypotheses are expressed by their finite-pattern language inclusion. The additive inequality avoids truncated subtraction and also handles an empty rectangle or eroded window.

theorem Nivat.Descent.exists_smaller_low_complexity_rectangle (c : Configuration ℚ) (hc : FiniteRange c) (x y : Configuration ℚ) (hx : ∀ (D : Finset Lattice), patternAt x D 0 ∈ patterns c D) (hy : ∀ (D : Finset Lattice), patternAt y D 0 ∈ patterns c D) (hd : x - y ≠ 0) (Φ : Laurent) (hΦ : Φ ≠ 0) (hexact : ∀ (f : Laurent), Algebra.act f (x - y) = 0 ↔ Φ ∣ f) (m n : ℕ) (hlow : complexity c (rectangle m n) ≤ m * n) : ∃ (m' : ℕ) (n' : ℕ), 0 < m' ∧ 0 < n' ∧ m' * n' < m * n ∧ complexity (Algebra.act Φ c) (rectangle m' n') ≤ m' * n'

Corollary 2.3 (cor:line-descent): an exact annihilator gives a positive rectangle of smaller area on which the filtered configuration has low complexity.

The support-width argument applies to any nonzero exact filter of a nonzero difference; in the paper it is used for the line polynomial of Theorem 4.1.