LeanPool.FriezePatterns.Chapter3

Imported Lean Pool material for LeanPool.FriezePatterns.Chapter3.

class arith_fp (f : ℕ × ℕ → ℚ) (n : ℕ) : Prop

An arithmetic frieze pattern of height n: a rational-valued frieze pattern with all denominators equal to one and positive interior entries.

• 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)
• integral (i m : ℕ) : (f (i, m)).den = 1
• positive (i m : ℕ) : 1 ≤ i → i ≤ n → f (i, m) > 0

instance instNzPattern_nRatOfArith_fp {f : ℕ × ℕ → ℚ} {n : ℕ} [arith_fp f n] : nzPattern_n ℚ f n

def fluteF (f : ℕ × ℕ → ℚ) (n m i : ℕ) : ℕ

The flute underlying sequence extracted from an arithmetic frieze pattern.

Equations

• fluteF f n m i = (f (i % (n - 1) + 1, m)).num.toNat

def friezeToFlute (f : ℕ × ℕ → ℚ) (n m : ℕ) (hn : 2 ≤ n) [arith_fp f n] : flute n

The flute associated to an arithmetic frieze pattern of height n ≥ 2.

Equations

• friezeToFlute f n m hn = { a := fluteF f n m, pos := ⋯, hd := ⋯, period := ⋯, div := ⋯ }

@[irreducible]

def friezeF {n : ℕ} (g : flute n) : ℕ × ℕ → ℚ

The arithmetic frieze pattern associated to a flute, defined recursively over the second coordinate m (and as a tie-breaker the first coordinate i).

Equations

• friezeF g (i, m) = if i = 0 then 0 else if i ≥ n + 1 then 0 else if m = 0 then ↑(g.a (i - 1)) else (friezeF g (i + 1, m - 1) * friezeF g (i - 1, m) + 1) / friezeF g (i, m - 1)

theorem fluteToFrieze {n : ℕ} (g : flute n) (hn : n ≠ 0) : arith_fp (friezeF g) n

The frieze pattern built from a flute is in fact an arithmetic frieze pattern.

def arithFriezePatSet (n : ℕ) : Set (ℕ × ℕ → ℚ)

The set of arithmetic frieze patterns of height n.

Equations

• arithFriezePatSet n = {f : ℕ × ℕ → ℚ | arith_fp f n}

theorem arithFriezePatSetNonEmpty {n : ℕ} (h : n ≠ 0) : (arithFriezePatSet n).Nonempty

theorem main1 (n : ℕ) (h : n ≠ 0) (f : ℕ × ℕ → ℚ) : arith_fp f n → ∀ (a : ℕ × ℕ), f a ≤ ↑(Nat.fib n)

theorem main2 (n : ℕ) (hn : n ≠ 0) : ∃ (f : ℕ × ℕ → ℚ) (_ : arith_fp f n) (a : ℕ × ℕ), f a = ↑(Nat.fib n)

theorem main3 (n : ℕ) (hn : n ≠ 0) : ∃ (g : ℕ × ℕ → ℚ) (_ : arith_fp g n) (b : ℕ × ℕ), (∀ (f : ℕ × ℕ → ℚ), arith_fp f n → ∀ (a : ℕ × ℕ), f a ≥ g b → f a = g b) ∧ g b = ↑(Nat.fib n)