Half-plane agreement from compactness

This module proves Lemma 3.1 (lem:halfplane-pair) of paper/nivat.tex. Nearest disagreements are chosen by minimizing their squared integer norms. A simultaneous compact subsequence of the translated configurations and their unit normals gives agreement on an open half-plane while retaining a fixed origin disagreement.

The main results are exists_halfPlane_pair for a closed shift-invariant space and exists_halfPlane_pair_coordinates with the normal written as a coordinate pair.

@[reducible, inline]

abbrev Nivat.Dynamics.RealPlane : Type

The Euclidean plane in which the unit normals of Lemma 3.1 (lem:halfplane-pair) converge.

Equations

• Nivat.Dynamics.RealPlane = EuclideanSpace ℝ (Fin 2)

def Nivat.Dynamics.latticeReal (z : Lattice) : RealPlane

The real embedding of a lattice site used in the distance estimates of Lemma 3.1 (lem:halfplane-pair).

Equations

• Nivat.Dynamics.latticeReal z = !₂[↑z.1, ↑z.2]

def Nivat.Dynamics.latticeSqNorm (z : Lattice) : ℕ

The natural-number squared norm used to select a nearest disagreement in Lemma 3.1 (lem:halfplane-pair).

Equations

• Nivat.Dynamics.latticeSqNorm z = (z.1 ^ 2 + z.2 ^ 2).toNat

@[simp]

theorem Nivat.Dynamics.latticeReal_add (z w : Lattice) : latticeReal (z + w) = latticeReal z + latticeReal w

The lattice embedding preserves addition, as used when translating agreement balls in Lemma 3.1 (lem:halfplane-pair).

@[simp]

theorem Nivat.Dynamics.latticeReal_zero : latticeReal 0 = 0

The lattice origin embeds as the real origin in the geometry of Lemma 3.1 (lem:halfplane-pair).

@[simp]

theorem Nivat.Dynamics.latticeReal_norm_sq (z : Lattice) : ‖latticeReal z‖ ^ 2 = ↑z.1 ^ 2 + ↑z.2 ^ 2

The squared Euclidean norm is the sum of the two squared coordinates, as in the nearest-disagreement argument of Lemma 3.1 (lem:halfplane-pair).

@[simp]

theorem Nivat.Dynamics.latticeSqNorm_cast (z : Lattice) : ↑(latticeSqNorm z) = ‖latticeReal z‖ ^ 2

The integer measure of a disagreement equals its squared Euclidean distance. This connects well-ordering to the geometry in Lemma 3.1 (lem:halfplane-pair).

theorem Nivat.Dynamics.exists_ne_agree_on_finite {A : Type u_1} [Finite A] (X : Set (Configuration A)) (hX : X.Infinite) (D : Finset Lattice) : ∃ x ∈ X, ∃ y ∈ X, x ≠ y ∧ ∀ z ∈ D, x z = y z

An infinite family over a finite alphabet contains distinct configurations agreeing on any finite window. This is the initial pigeonhole step of Lemma 3.1 (lem:halfplane-pair).

theorem Nivat.Dynamics.exists_nearest_disagreement {A : Type u_1} (x y : Configuration A) (hxy : x ≠ y) : ∃ (p : Lattice), x p ≠ y p ∧ ∀ (z : Lattice), ‖latticeReal z‖ < ‖latticeReal p‖ → x z = y z

Distinct configurations have a disagreement of least Euclidean distance from the origin, by minimizing a natural-number squared norm. This is the nearest-disagreement step of Lemma 3.1 (lem:halfplane-pair).

theorem Nivat.Dynamics.exists_far_nearest_disagreement {A : Type u_1} [Finite A] (X : Set (Configuration A)) (hX : X.Infinite) (n : ℕ) : ∃ x ∈ X, ∃ y ∈ X, ∃ (p : Lattice), x p ≠ y p ∧ ↑n < ‖latticeReal p‖ ∧ ∀ (z : Lattice), ‖latticeReal z‖ < ‖latticeReal p‖ → x z = y z

A finite alphabet and infinitely many configurations give nearest disagreements arbitrarily far from the origin. This implements the escaping agreement balls in Lemma 3.1 (lem:halfplane-pair).

theorem Nivat.Dynamics.eventually_norm_add_lt_of_normal_tendsto (p : ℕ → RealPlane) (ν z : RealPlane) (hp : ∀ (n : ℕ), p n ≠ 0) (hr : Filter.Tendsto (fun (n : ℕ) => ‖p n‖) Filter.atTop Filter.atTop) (hν : Filter.Tendsto (fun (n : ℕ) => ‖p n‖⁻¹ • p n) Filter.atTop (nhds ν)) (hz : inner ℝ ν z < 0) : ∀ᶠ (n : ℕ) in Filter.atTop, ‖p n + z‖ < ‖p n‖

A displacement strictly inside the limiting negative half-plane eventually shortens an escaping radius. This is the displayed squared-distance estimate in the proof of Lemma 3.1 (lem:halfplane-pair).

theorem Nivat.Dynamics.eventually_eq_at_of_tendsto {A : Type u_1} [TopologicalSpace A] [DiscreteTopology A] {x : ℕ → Configuration A} {c : Configuration A} (h : Filter.Tendsto x Filter.atTop (nhds c)) (z : Lattice) : ∀ᶠ (n : ℕ) in Filter.atTop, x n z = c z

Convergence in a product of discrete alphabets implies eventual equality at each fixed coordinate. Lemma 3.1 (lem:halfplane-pair) uses this to preserve disagreement at the origin and agreement inside the half-plane.

theorem Nivat.Dynamics.exists_halfPlane_pair {A : Type u_1} [TopologicalSpace A] [DiscreteTopology A] [Finite A] (X : Set (Configuration A)) (hX : X.Infinite) (hclosed : IsClosed X) (hshift : ∀ (h : Lattice), ∀ c ∈ X, shift h c ∈ X) : ∃ x ∈ X, ∃ y ∈ X, ∃ (ν : RealPlane), ‖ν‖ = 1 ∧ x 0 ≠ y 0 ∧ ∀ (z : Lattice), inner ℝ ν (latticeReal z) < 0 → x z = y z

An infinite closed shift-invariant space over a finite discrete alphabet contains two configurations disagreeing at the origin and agreeing on an open half-plane with a unit normal. This is the compact-space form of Lemma 3.1 (lem:halfplane-pair).

@[simp]

theorem Nivat.Dynamics.inner_latticeReal (ν : RealPlane) (z : Lattice) : inner ℝ ν (latticeReal z) = ν.ofLp 0 * ↑z.1 + ν.ofLp 1 * ↑z.2

The Euclidean inner product gives the coordinate formula for the normal functional in Lemma 3.1 (lem:halfplane-pair).

theorem Nivat.Dynamics.exists_halfPlane_pair_coordinates {A : Type u_1} [TopologicalSpace A] [DiscreteTopology A] [Finite A] (X : Set (Configuration A)) (hX : X.Infinite) (hclosed : IsClosed X) (hshift : ∀ (h : Lattice), ∀ c ∈ X, shift h c ∈ X) : ∃ x ∈ X, ∃ y ∈ X, ∃ (ν : ℝ × ℝ), ν.1 ^ 2 + ν.2 ^ 2 = 1 ∧ x 0 ≠ y 0 ∧ ∀ (z : Lattice), ν.1 * ↑z.1 + ν.2 * ↑z.2 < 0 → x z = y z

Coordinate form of Lemma 3.1 (lem:halfplane-pair), with the unit-normal equation and strict half-plane inequality written explicitly.