LeanPool.FriezePatterns.Chapter1

Imported Lean Pool material for LeanPool.FriezePatterns.Chapter1.

class pattern_n (F : Type u_1) [Field F] (f : ℕ × ℕ → F) (n : ℕ) : Prop

A field-valued frieze pattern of height n: a function f : ℕ × ℕ → F with 0s on the row i = 0, 1s on rows i = 1 and i = n, 0s on rows i ≥ n + 1, satisfying the diamond (or unimodular) relation f (i + 1, m) * f (i + 1, m + 1) - 1 = f (i + 2, m) * f (i, m + 1) for i ≤ n - 1.

• topBordZeros (m : ℕ) : f (0, m) = 0
• topBordOnes (m : ℕ) : f (1, m) = 1
• botBordOnes_n (m : ℕ) : f (n, m) = 1
• botBordZeros_n (i m : ℕ) : i ≥ n + 1 → f (i, m) = 0
• diamond (i m : ℕ) : i ≤ n - 1 → f (i + 1, m) * f (i + 1, m + 1) - 1 = f (i + 2, m) * f (i, m + 1)

class nzPattern_n (F : Type u_1) [Field F] (f : ℕ × ℕ → F) (n : ℕ) extends pattern_n F f n : Prop

A frieze pattern is non-zero if it never vanishes on the interior rows 1 ≤ i ≤ n.

• topBordZeros (m : ℕ) : f (0, m) = 0
• topBordOnes (m : ℕ) : f (1, m) = 1
• botBordOnes_n (m : ℕ) : f (n, m) = 1
• botBordZeros_n (i m : ℕ) : i ≥ n + 1 → f (i, m) = 0
• diamond (i m : ℕ) : i ≤ n - 1 → f (i + 1, m) * f (i + 1, m + 1) - 1 = f (i + 2, m) * f (i, m + 1)
• non_zero (i m : ℕ) : 1 ≤ i ∧ i ≤ n → f (i, m) ≠ 0

theorem pattern_nContinuant1 (F : Type u_1) [Field F] (f : ℕ × ℕ → F) (n : ℕ) [nzPattern_n F f n] (i : ℕ) : i ≤ n - 1 → ∀ (m : ℕ), f (i + 2, m) = f (2, m + i) * f (i + 1, m) - f (i, m)

theorem pattern_nContinuant2 (F : Type u_1) [Field F] (f : ℕ × ℕ → F) (n : ℕ) [nzPattern_n F f n] (i : ℕ) : i ≤ n - 1 → ∀ (m : ℕ), f (i, m + 2) = f (n - 1, m + 2) * f (i + 1, m + 1) - f (i + 2, m)

theorem glideSymm (F : Type u_1) [Field F] (f : ℕ × ℕ → F) (n : ℕ) [nzPattern_n F f n] (i : ℕ) : i ≤ n + 1 → ∀ (m : ℕ), f (n + 1 - i, m + i) = f (i, m)

theorem translationInvariance (F : Type u_1) [Field F] (f : ℕ × ℕ → F) (n : ℕ) [nzPattern_n F f n] (i : ℕ) : i ≤ n + 1 → ∀ (m : ℕ), f (i, m) = f (i, m + n + 1)

theorem strongTranslationInvariance (F : Type u_1) [Field F] (f : ℕ × ℕ → F) (n : ℕ) [nzPattern_n F f n] (i : ℕ) : i ≤ n + 1 → ∀ (m : ℕ), f (i, m) = f (i, m % (n + 1))

theorem imageFinite (F : Type u_1) [Field F] (f : ℕ × ℕ → F) (n : ℕ) [nzPattern_n F f n] : Finite ↑(Set.range f)