diff --git a/FriezePatterns/chapter1.lean b/FriezePatterns/chapter1.lean index 790f901..88c5ef4 100644 --- a/FriezePatterns/chapter1.lean +++ b/FriezePatterns/chapter1.lean @@ -115,56 +115,56 @@ rw[i_eq_zero, n_eq_zero] simp rw[@pattern_n.topBordZeros F _ f n _ (m+2), @pattern_n.botBordZeros_n F _ f n _ (2) m (by linarith),zero_mul, sub_zero] +theorem glideSymm (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀ i, i ≤ n+1 → ∀ m, f (n+1-i, m+i) = f (i,m) := by +-- we need glideSymm in chapter 3 + intros i ileq + induction' i using Nat.strong_induction_on with i ih -- strong induction on i + match i with + | 0 => -- P₀ + simp + intro m + rw [@pattern_n.botBordZeros_n F _ f n _ (n+1) m (by linarith), @pattern_n.topBordZeros F _ f n _ m] + | 1 => -- P₁ + simp at * + intro m + rw [@pattern_n.botBordOnes_n F _ f n _ (m+1), @pattern_n.topBordOnes F _ f n _ m] + | i+2 => + simp at * + intro m + rw [Nat.sub_add_eq, ← add_assoc m i 2] + have h₁ : i ≤ n-1 := by omega + have h₂ : f (2,m+i) = f (n-1,m+i+2) := by -- we first prove P₂ + have key := pattern_nContinuant2 F f n 0 (by linarith) (m+i) + simp at key + rw [@pattern_n.topBordZeros F _ f n _ (m+i+2), @pattern_n.topBordOnes F _ f n _ (m+i+1)] at key + simp at key + exact (sub_eq_zero.mp key.symm).symm + have h₃ : f (i+1,m) = f (n-i,m+i+1) := by + have := ih (i+1) (by linarith) (by linarith) + simp at this + rw [← this, add_assoc] + have h₄ : f (i,m) = f (n+1-i,m+i) := by + have := ih i (by linarith) (by linarith) + simp at this + rw [← this] + have h₅ : f (n-i-1,m+i+2) = f (n-1,m+i+2) * f (n-i,m+i+1) - f (n+1-i,m+i) := by + have key := pattern_nContinuant2 F f n (n-i-1) (by omega) (m+i) + rw [key, Nat.sub_sub n i 1, ← Nat.sub_add_comm ileq, ← Nat.sub_add_comm ileq] + simp + symm + calc + f (i+2,m) = f (2,m+i) * f (i+1,m) - f (i,m) := by rw [pattern_nContinuant1 F f n i h₁ m] + _ = f (n-1,m+i+2) * f (n-i,m+i+1) - f (n+1-i,m+i) := by rw [h₂, h₃, h₄] + _ = f (n-i-1,m+i+2) := by rw [h₅] theorem trsltInv (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀ i, i ≤ n+1 → ∀m, f (i,m) = f (i,m+n+1) := by - -- it suffices to prove glide symmetry - suffices glideSymm : ∀ i, i ≤ n+1 → ∀ m, f (n+1-i, m+i) = f (i,m) - · intros i ileq m - have key := glideSymm i ileq m - have key2 := glideSymm (n+1-i) (Nat.sub_le (n+1) i) (m+i) - simp [Nat.sub_sub_eq_min, ileq, add_assoc] at key2 - rw [←key, ←key2, add_assoc] - - -- proof of glide symmetry - · intros i ileq - induction' i using Nat.strong_induction_on with i ih -- strong induction on i - match i with - | 0 => -- P₀ - simp - intro m - rw [@pattern_n.botBordZeros_n F _ f n _ (n+1) m (by linarith), @pattern_n.topBordZeros F _ f n _ m] - | 1 => -- P₁ - simp at * - intro m - rw [@pattern_n.botBordOnes_n F _ f n _ (m+1), @pattern_n.topBordOnes F _ f n _ m] - | i+2 => - simp at * - intro m - rw [Nat.sub_add_eq, ← add_assoc m i 2] - have h₁ : i ≤ n-1 := by omega - have h₂ : f (2,m+i) = f (n-1,m+i+2) := by -- we first prove P₂ - have key := pattern_nContinuant2 F f n 0 (by linarith) (m+i) - simp at key - rw [@pattern_n.topBordZeros F _ f n _ (m+i+2), @pattern_n.topBordOnes F _ f n _ (m+i+1)] at key - simp at key - exact (sub_eq_zero.mp key.symm).symm - have h₃ : f (i+1,m) = f (n-i,m+i+1) := by - have := ih (i+1) (by linarith) (by linarith) - simp at this - rw [← this, add_assoc] - have h₄ : f (i,m) = f (n+1-i,m+i) := by - have := ih i (by linarith) (by linarith) - simp at this - rw [← this] - have h₅ : f (n-i-1,m+i+2) = f (n-1,m+i+2) * f (n-i,m+i+1) - f (n+1-i,m+i) := by - have key := pattern_nContinuant2 F f n (n-i-1) (by omega) (m+i) - rw [key, Nat.sub_sub n i 1, ← Nat.sub_add_comm ileq, ← Nat.sub_add_comm ileq] - simp - symm - calc - f (i+2,m) = f (2,m+i) * f (i+1,m) - f (i,m) := by rw [pattern_nContinuant1 F f n i h₁ m] - _ = f (n-1,m+i+2) * f (n-i,m+i+1) - f (n+1-i,m+i) := by rw [h₂, h₃, h₄] - _ = f (n-i-1,m+i+2) := by rw [h₅] + intros i ileq m + have key := glideSymm F f n i ileq m + have key2 := glideSymm F f n (n+1-i) (Nat.sub_le (n+1) i) (m+i) + simp [Nat.sub_sub_eq_min, ileq, add_assoc] at key2 + rw [←key, ←key2, add_assoc] + + -- A stronger version of the translation invariance - may be useful lemma strongTrsltInv (F : Type*) [Field F] (f : ℕ×ℕ → F) (n: ℕ) [nzPattern_n F f n] : ∀ i, i ≤ n+1 → ∀m, f (i,m) = f (i,m%(n+1)) := by diff --git a/FriezePatterns/chapter2.lean b/FriezePatterns/chapter2.lean index 7831943..91985f9 100644 --- a/FriezePatterns/chapter2.lean +++ b/FriezePatterns/chapter2.lean @@ -173,7 +173,11 @@ def fib_flute_odd (k : ℕ) : flute (2*k+1) := by rw [hi₁₀, ← Nat.fib_add_two, hi₁₁] omega · push_neg at hi₅ - by_cases hi₆ : ¬ 2*k ≤ i+1 + by_cases hi₆ : 2*k ≤ i+1 + have hi₇ : i+1-2*k = 0 := by omega + have hi₈ : i+2-2*k = 1 := by omega + unfold a_odd ; simp [hk, hi, hi₂, hi₃, hi₄, hi₅, hi₆, hi₇, hi₇, hi₈] + unfold a_odd ; simp [hk] unfold a_odd ; simp [hk, hi, hi₂, hi₃, hi₄, hi₅, hi₆] have hi₇ : 1+4*k-2*(i+1) = 3 := by omega have hi₈ : 1+4*k-2*i = 5 := by omega @@ -182,14 +186,8 @@ def fib_flute_odd (k : ℕ) : flute (2*k+1) := by unfold a_odd simp [hi₇, hi₈, hi₉, hk, hk₂] use 3 ; simp [Nat.fib_add_two] - push_neg at hi₆ - have hi₇ : i+1-2*k = 0 := by omega - have hi₈ : i+2-2*k = 1 := by omega - unfold a_odd ; simp [hk, hi, hi₂, hi₃, hi₄, hi₅, hi₆, hi₇, hi₇, hi₈] - unfold a_odd ; simp [hk] exact ⟨a_odd k, pos, hd, period, div⟩ - def a_even (k i : ℕ) : ℕ := if i ≥ 2*k+1 then a_even k (i-2*k-1) @@ -476,14 +474,56 @@ def a_2 (n : ℕ) (f : flute (n+3)) (h : f.a (n+1) = 1) (k : ℕ) : ℕ := f.a k def aux_2 (n : ℕ) (f : flute (n+3)) (h : f.a (n+1) = 1) : flute (n+2) := by - have pos : ∀ i, a_2 n f h i > 0 := by sorry + have pos : ∀ i, a_2 n f h i > 0 := by + intro i + induction' i using Nat.strong_induction_on with i ih + by_cases hi : i ≥ n+1 + unfold a_2 ; simp [hi] + exact ih (i-(n+1)) (by omega) + simp [a_2, hi] + exact f.pos i have hd : a_2 n f h 0 = 1 := by simp [a_2, f.hd] have period : ∀ i, a_2 n f h i = a_2 n f h (i+(n+2)-1) := by intro i nth_rw 2 [a_2] simp - have div : ∀ i, a_2 n f h (i+1) ∣ (a_2 n f h i + a_2 n f h (i+2)) := by sorry + have div : ∀ i, a_2 n f h (i+1) ∣ (a_2 n f h i + a_2 n f h (i+2)) := by + intro i + induction' i using Nat.strong_induction_on with i ih + by_cases hi : i ≥ n+1 + have hi₂ : n ≤ i := by omega + have hi₃ : n ≤ i+1 := by omega + unfold a_2 ; simp [hi, hi₂, hi₃] + specialize ih (i-(n+1)) (by omega) + have hi₄ : i-(n+1)+1 = i-n := by omega + have hi₅ : i-(n+1)+2 = i+1-n := by omega + rw [hi₄, hi₅] at ih ; exact ih + by_cases hi₂ : i = 0 + unfold a_2 ; simp [hi, hi₂] + match n with + | 0 => simp [hd] + | 1 => + simp ; simp at h + rw [hd, f.hd] + nth_rw 2 [←h] + nth_rw 2 [←f.hd] + simp [f.div 0, add_comm] + | n+2 => + simp [f.hd] + nth_rw 2 [←f.hd] + exact f.div 0 + unfold a_2 ; simp [hi, hi₂] + by_cases hi₃ : n ≤ i + have hi₄ : i = n := by omega + simp [hi₃, hi₄, hd] + by_cases hi₄ : n ≤ i+1 + have hi₅ : i+1 = n := by omega + simp [hi₃, hi₄, hi₅, hd] + have key := f.div i + rw [hi₅, ←one_add_one_eq_two, ←add_assoc, hi₅, h] at key + exact key + simp [hi₃, hi₄, f.div i] exact ⟨a_2 n f h, pos, hd, period, div⟩ def a_3 (n : ℕ) (f : flute (n+3)) (i : ℕ) (hi : i ≤ n ∧ f.a (i+1) = f.a i + f.a (i+2)) (k : ℕ) : ℕ := @@ -494,11 +534,104 @@ def a_3 (n : ℕ) (f : flute (n+3)) (i : ℕ) (hi : i ≤ n ∧ f.a (i+1) = f.a else f.a (k+1) def aux_3 (n : ℕ) (f : flute (n+3)) (j : ℕ) (hj : j ≤ n ∧ f.a (j+1) = f.a j + f.a (j+2)) : flute (n+2) := by - -- the proof of this will probably be more complicated than the previous two - have pos : ∀ i, a_3 n f j hj i > 0 := by sorry - have hd : a_3 n f j hj 0 = 1 := by sorry - have period : ∀ i, a_3 n f j hj i = a_3 n f j hj (i+(n+2)-1) := by sorry - have div : ∀ i, a_3 n f j hj (i+1) ∣ (a_3 n f j hj i + a_3 n f j hj (i+2)) := by sorry + have pos : ∀ i, a_3 n f j hj i > 0 := by + intro i + induction' i using Nat.strong_induction_on with i ih + by_cases hi : i ≥ n+1 + unfold a_3 ; simp [hi] + exact ih (i-(n+1)) (by omega) + by_cases hi₂ : i ≤ j + unfold a_3 ; simp [hi, hi₂] + exact f.pos i + unfold a_3 ; simp [hi, hi₂] + exact f.pos (i+1) + have hd : a_3 n f j hj 0 = 1 := by simp [a_3, f.hd] + have period : ∀ i, a_3 n f j hj i = a_3 n f j hj (i+(n+2)-1) := by + intro i + nth_rw 2 [a_3] + simp + have div : ∀ i, a_3 n f j hj (i+1) ∣ (a_3 n f j hj i + a_3 n f j hj (i+2)) := by + have f.tl : f.a (n+2) = 1 := by + have := f.period 0 + simpa [f.hd] using this.symm + intro i + induction' i using Nat.strong_induction_on with i ih + by_cases hi : i ≥ n+1 + have hi₂ : n ≤ i := by omega + have hi₃ : n ≤ i+1 := by omega + unfold a_3 ; simp [hi, hi₂, hi₃] + specialize ih (i-(n+1)) (by omega) + have hi₄ : i-(n+1)+1 = i-n := by omega + have hi₅ : i-(n+1)+2 = i+1-n := by omega + rw [hi₄, hi₅] at ih ; exact ih + by_cases hi₂ : n ≤ i + have hi₂ : i = n := by omega + simp [hi, hi₂, a_3, f.hd] + by_cases hi₃ : n ≤ i+1 + have hi₃ : i = n-1 := by omega + have hn : ¬ n ≤ n-1 := by omega + have hn₂ : n-1+1 = n := by omega + have hn₃ : ¬ n+1 ≤ n-1 := by omega + unfold a_3 ; simp [hi, hi₂, hi₃, hn, hn₂, hn₃] + simp [hd] + by_cases hn₄ : n ≤ j + have hn₅ : j = n := by omega + simp [hn₄, hn₅] + have key := f.div (n-1) + have hn₆ : n-1+2 = n+1 := by omega + simp [hn₂, hn₆] at key + simp [hn₅ ▸ hj.2] at key + rw [f.tl] at key + rcases key with ⟨k, hk⟩ + use k-1 + calc + f.a (n-1) +1 = f.a (n-1) + (f.a n +1) - f.a n := by omega + _ = f.a n * k - f.a n := by rw [hk] + _ = f.a n * (k-1) := by exact (Nat.mul_sub_one (f.a n) k).symm + simp [hn₄] + by_cases hn₅ : n ≤ j+1 + have hn₆ : j = n-1 := by omega + have hn₇ : n ≤ n-1+1 := by omega + simp [hn₄, hn₅, hn₆, hn₇] + have key := hn₆ ▸ hj.2 + have hn₈ : n-1+2 = n+1 := by omega + simp [hn₂, hn₈] at key + have key₂ := f.div n + simp [hn₂, hn₈, f.tl] at key₂ + rcases key₂ with ⟨k, hk⟩ + use k-1 + calc + f.a (n-1) + 1 = f.a (n+1)*k - f.a (n+1) := by omega + _ = f.a (n+1) * (k-1) := by exact (Nat.mul_sub_one (f.a (n+1)) k).symm + simp [hn₅] + simpa [f.tl] using f.div n + unfold a_3 ; simp [hi, hi₂, hi₃, add_assoc] + by_cases hij : i+2 ≤ j + have hij₂ : i+1 ≤ j := by omega + have hij₃ : i ≤ j := by omega + simp [hij, hij₂, hij₃, f.div i] + by_cases hij₂ : i+1 ≤ j + have hij₃ : i ≤ j := by omega + have hij₄ : i+1 = j := by omega + simp [hij, hij₂, hij₃, ←hij₄] + have key := hij₄ ▸ hj.2 + simp [add_assoc] at key + rcases f.div i with ⟨k, hk⟩ + use k-1 + calc + f.a i + f.a (i+3) = f.a (i+1) * k - f.a (i+1) := by omega + _ = f.a (i+1) * (k-1) := by exact (Nat.mul_sub_one (f.a (i+1)) k).symm + by_cases hij₃ : i ≤ j + have hij₄ : i = j := by omega + simp [hij, hij₂, hij₃, hij₄] + have key := hj.2 + rcases f.div (j+1) with ⟨k, hk⟩ + simp [add_assoc] at hk + use k-1 + calc + f.a j + f.a (j+3) = f.a (j+2) * k - f.a (j+2) := by omega + _ = f.a (j+2) * (k-1) := by exact (Nat.mul_sub_one (f.a (j+2)) k).symm + simp [hij, hij₂, hij₃, f.div (i+1)] exact ⟨a_3 n f j hj, pos, hd, period, div⟩ theorem FluteBounded (n : ℕ) (hn: n>0) (f : flute n) : ∀ i ≤ n-1, f.a i ≤ Nat.fib n := by diff --git a/FriezePatterns/chapter3.lean b/FriezePatterns/chapter3.lean index 5cf81d8..5fa024e 100644 --- a/FriezePatterns/chapter3.lean +++ b/FriezePatterns/chapter3.lean @@ -8,7 +8,7 @@ class arith_fp (f : ℕ × ℕ → ℚ) (n : ℕ) : Prop where 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 + integral: ∀ i, ∀ m, (f (i,m)).den = 1 positive: ∀ i, ∀ m, 1 ≤ i → i ≤ n → f (i,m) > 0 instance [arith_fp f n] : nzPattern_n ℚ f n := { @@ -26,7 +26,7 @@ def flute_f (f : ℕ×ℕ → ℚ) (n m: ℕ) [arith_fp f n] (i:ℕ) : ℕ := def friezeToFlute (f : ℕ×ℕ → ℚ) (n m: ℕ) (hn : 2 ≤ n) [arith_fp f n] : flute n := by - have pos : ∀ i, flute_f f n m (i) > 0 := by + have pos : ∀ i, flute_f f n m i > 0 := by intro i have zero_lt_n_sub_one : 0 < n - 1 := @@ -78,11 +78,15 @@ def friezeToFlute (f : ℕ×ℕ → ℚ) (n m: ℕ) (hn : 2 ≤ n) [arith_fp f n _= 1 * 1 + 1 := by rw[@pattern_n.botBordOnes_n ℚ _ f n _ (m)] _= 2 := by ring - have this.num : (f (2, m)).num * (f (2, m + 1)).num = 2 := by sorry - --use theorem Rat.mul_num (q₁ : ℚ) (q₂ : ℚ) : (q₁ * q₂).num = q₁.num * q₂.num / ↑(Nat.gcd (Int.natAbs (q₁.num * q₂.num)) (q₁.den * q₂.den)) + have this.num : (f (2, m)).num * (f (2, m + 1)).num = 2 := by + have key : (f (2, m)).num * (f (2, m + 1)).num = (f (2, m) * f (2, m + 1)).num := by + simp [Rat.mul_num, arith_fp.integral n, arith_fp.integral n] + simp [key, this] - - have this.num.toNat : (f (2, m)).num.toNat * (f (2, m + 1)).num.toNat = 2 := by sorry + have this.num.toNat : (f (2, m)).num.toNat * (f (2, m + 1)).num.toNat = 2 := by + have h₃ : 0 ≤ (f (2,m)).num := by linarith [Rat.num_pos.mpr (@arith_fp.positive f n _ 2 m (by omega) (by omega))] + have h₄ : 0 ≤ (f (2,m+1)).num := by linarith [Rat.num_pos.mpr (@arith_fp.positive f n _ 2 (m+1) (by omega) (by omega))] + zify ; rw [Int.toNat_of_nonneg h₃, Int.toNat_of_nonneg h₄, this.num] nth_rewrite 2 [← this.num.toNat] simp --finish if n=3, i_even @@ -127,10 +131,21 @@ def friezeToFlute (f : ℕ×ℕ → ℚ) (n m: ℕ) (hn : 2 ≤ n) [arith_fp f n rw[pattern_nContinuant1 ℚ f n (i % (n - 1) + 1) h₁ m] simp - have continuant.num : (f (i % (n - 1) + 1, m)).num + (f (i % (n - 1) + 1 + 1 + 1, m)).num = (f (2, m + (i % (n - 1) + 1))).num * (f (i % (n - 1) + 1 + 1,m)).num := by sorry - - have continuant.num.toNat : (f (i % (n - 1) + 1, m)).num.toNat + (f (i % (n - 1) + 1 + 1 + 1, m)).num.toNat = (f (2, m + (i % (n - 1) + 1))).num.toNat * (f (i % (n - 1) + 1 + 1,m)).num.toNat := by sorry - -- Need to use theorem Int.toNat_add {a : Int} {b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : Int.toNat (a + b) = Int.toNat a + Int.toNat b + have continuant.num : (f (i % (n - 1) + 1, m)).num + (f (i % (n - 1) + 1 + 1 + 1, m)).num = (f (2, m + (i % (n - 1) + 1))).num * (f (i % (n - 1) + 1 + 1,m)).num := by + have key₁ : (f (i % (n - 1) + 1, m)).num + (f (i % (n - 1) + 1 + 1 + 1, m)).num = (f (i % (n - 1) + 1, m) + f (i % (n - 1) + 1 + 1 + 1, m)).num := by + simp [Rat.add_num_den, arith_fp.integral n (i % (n - 1) + 1) m] + simp [arith_fp.integral n (i % (n - 1) + 1 + 1 + 1) m] + norm_cast + have key₂ : (f (2, m + (i % (n - 1) + 1))).num * (f (i % (n - 1) + 1 + 1,m)).num = (f (2, m + (i % (n - 1) + 1)) * f (i % (n - 1) + 1 + 1,m)).num := by + simp [Rat.mul_num, arith_fp.integral n 2 (m + (i % (n - 1) + 1)), arith_fp.integral n (i % (n - 1) + 1 + 1) m] + simp [key₁, key₂, continuant] + + have continuant.num.toNat : (f (i % (n - 1) + 1, m)).num.toNat + (f (i % (n - 1) + 1 + 1 + 1, m)).num.toNat = (f (2, m + (i % (n - 1) + 1))).num.toNat * (f (i % (n - 1) + 1 + 1,m)).num.toNat := by + have h₂ : 0 ≤ (f (i % (n - 1) + 1, m)).num := by linarith [Rat.num_pos.mpr (@arith_fp.positive f n _ (i % (n - 1) + 1) m (by omega) (by omega))] + have h₃ : 0 ≤ (f (i % (n - 1) + 1 + 1 + 1, m)).num := by linarith [Rat.num_pos.mpr (@arith_fp.positive f n _ (i % (n - 1) + 1 + 1 + 1) m (by omega) (by omega))] + have h₄ : 0 ≤ (f (2, m + (i % (n - 1) + 1))).num := by linarith [Rat.num_pos.mpr (@arith_fp.positive f n _ 2 (m + (i % (n - 1) + 1)) (by omega) (by omega))] + have h₅ : 0 ≤ (f (i % (n - 1) + 1 + 1,m)).num := by linarith [Rat.num_pos.mpr (@arith_fp.positive f n _ (i % (n - 1) + 1 + 1) m (by omega) (by omega))] + zify ; rw [Int.toNat_of_nonneg h₂, Int.toNat_of_nonneg h₃, Int.toNat_of_nonneg h₄, Int.toNat_of_nonneg h₅, continuant.num] simp[continuant.num.toNat] @@ -140,16 +155,146 @@ def friezeToFlute (f : ℕ×ℕ → ℚ) (n m: ℕ) (hn : 2 ≤ n) [arith_fp f n -- The following two definitions turn a flute to a frieze. -def f {n : ℕ} (g : flute n): ℕ × ℕ → ℚ := +def frieze_f {n : ℕ} (g : flute n): ℕ × ℕ → ℚ := λ ⟨i, m⟩ => if i = 0 then 0 else if i ≥ n+1 then 0 else if m = 0 then g.a (i-1) - else (f g (i+1,m-1) * f g (i-1, m) + 1) / f g (i,m-1) + else (frieze_f g (i+1,m-1) * frieze_f g (i-1, m) + 1) / frieze_f g (i,m-1) termination_by x => (x.2, x.1) - -def fluteToFrieze {n : ℕ} (g : flute n) (h: n ≠ 0): arith_fp (f g) n := by sorry +def fluteToFrieze {n : ℕ} (g : flute n) (hn : n ≠ 0) : arith_fp (frieze_f g) n := by + have topBordZeros : ∀ m, frieze_f g (0,m) = 0 := λ m => (by simp [frieze_f]) + have botBordZeros_n : ∀ i, ∀ m, i ≥ n+1 → (frieze_f g (i,m) = 0) := λ i m h => by simp [frieze_f, h] + have topBordOnes : ∀ m, frieze_f g (1,m) = 1 := by + intro m + induction' m with m ih + simp [frieze_f, hn, g.hd] + have : ¬ 1 ≥ n+1 := by omega + unfold frieze_f ; simp [this, ih] + right + exact topBordZeros (m+1) + have botBordOnes_n : ∀ m, frieze_f g (n, m) = 1 := by + intro m + induction' m with m ih + simp [frieze_f, hn] + have := g.period 0 + simp [g.hd] at this + exact this.symm + have : ¬ n ≥ n+1 := by omega + unfold frieze_f ; simp [this, ih, hn] + left + exact botBordZeros_n (n+1) m (by rfl) + have positive: ∀ i, ∀ m, 1 ≤ i → i ≤ n → frieze_f g (i,m) > 0 := by + intro i m + induction' m with m ih₁ generalizing i + intro hi₁ hi₂ + have hi₃ : ¬ i = 0 := by omega + have hi₄ : ¬ i ≥ n+1 := by omega + unfold frieze_f ; simp [hi₃, hi₄] + exact g.pos (i-1) + induction' i with i ih₂ + omega + intro hi₁ hi₂ + by_cases hi : i = 0 + simp [hi, topBordOnes] + by_cases hi' : i = n-1 + have : n-1+1 = n := by omega + simp [this, hi', botBordOnes_n] + specialize ih₂ (by omega) (by omega) + have : ¬ n ≤ i := by omega + unfold frieze_f ; simp [this, add_assoc] + have h₁ := ih₁ (i+1) (by omega) (by omega) + have h₂ := ih₁ (i+2) (by omega) (by omega) + field_simp [h₁, h₂, ih₂] + have diamond : ∀ i, ∀ m, i ≤ n-1 → frieze_f g (i+1,m) * frieze_f g (i+1,m+1)-1 = frieze_f g (i+2,m) * frieze_f g (i,m+1) := by + intro i m hi + conv => + enter [1,1,2] + unfold frieze_f + have : ¬ n ≤ i := by omega + simp [this, add_assoc] + have : frieze_f g (i+1, m) > 0 := by linarith [positive (i+1) m (by omega) (by omega)] + field_simp [this] + have non_zero : ∀ i m, 1 ≤ i ∧ i ≤ n → frieze_f g (i,m) ≠ 0 := λ i m ⟨hi₁, hi₂⟩ => by linarith [positive i m hi₁ hi₂] + have : nzPattern_n ℚ (frieze_f g) n := by + exact {topBordZeros, topBordOnes, botBordOnes_n, botBordZeros_n, diamond, non_zero} + have integral: ∀ i, ∀ m, (frieze_f g (i,m)).den = 1 := by + have key : ∀ m, (frieze_f g (2, m)).den = 1 := by + intro m + induction' m using Nat.strong_induction_on with m ih + by_cases hm : m = 0 + simp [hm, frieze_f] + norm_cast + by_cases hm₂ : m ≤ n-2 + have key := pattern_nContinuant1 ℚ (frieze_f g) n m (by omega) 0 + have div : ∃ k : ℕ, (frieze_f g (m,0) + frieze_f g (m+2,0)) = frieze_f g (m+1,0)*k := by + have hm₃ : ¬ n ≤ m := by omega + have hm₄ : ¬ n ≤ m+1 := by omega + have hm₅ : ¬ n+1 ≤ m := by omega + unfold frieze_f ; simp [hm, hm₃, hm₄, hm₅] + norm_cast + have := g.div (m-1) + have hm₆ : m-1+1 = m := by omega + have hm₇ : m-1+2 = m+1 := by omega + simp [hm₆, hm₇] at this + exact this + rcases div with ⟨k, hk⟩ + simp at key + have : frieze_f g (m+1, 0) ≠ 0 := by linarith [positive (m+1) 0 (by omega) (by omega)] + have : frieze_f g (2,m) = k := by + calc frieze_f g (2,m) = (frieze_f g (m,0) + frieze_f g (m+2,0)) / frieze_f g (m+1,0) := by field_simp [hm, hm₂, this, key] + _ = k := by field_simp [hk] + field_simp [this] + have : n+1-(n-1)=2 := by omega + by_cases hm₃ : m = n-1 + have key := glideSymm ℚ (frieze_f g) n (n-1) (by omega) 0 + simp [this] at key + simp [hm₃, key, frieze_f] + norm_cast + by_cases hm₄ : m = n + have key := glideSymm ℚ (frieze_f g) n (n-1) (by omega) 1 + have hm₅ : 1+(n-1)=n := by omega + simp [this, hm₅] at key + rw [hm₄, key] ; rw [hm₄] at ih + suffices : ∀ i ≤ n-1, (frieze_f g (i,1)).den = 1 + · exact this (n-1) (by omega) + intro i hi + induction' i using Nat.twoStepInduction with i ih₁ ih₂ + simp [frieze_f] + simp [frieze_f, hn, g.hd] + simp [add_assoc] at ih₁ ih₂ hi + specialize ih₁ (by omega) + specialize ih₂ (by omega) + have := pattern_nContinuant1 ℚ (frieze_f g) n i (by omega) 1 + rw [this] + have := ih (1+i) (by omega) + -- there should be a tactic to do the following two steps? + rw [Rat.sub_eq_add_neg, Rat.add_num_den, Rat.neg_den, Rat.mul_den, ih₁, ih₂, this] + simp ; norm_cast + have h := trsltInv ℚ (frieze_f g) n 2 (by omega) (m-(n+1)) + have : m-(n+1)+n+1 = m := by omega + rw [this] at h + exact h ▸ ih (m-(n+1)) (by omega) + intro i + induction' i using Nat.strong_induction_on with i ih + match i with + | 0 => intro ; simp [topBordZeros] + | 1 => intro ; simp [topBordOnes] + | 2 => exact key + | i+3 => + by_cases hi : i+2 ≥ n + intro ; simp [botBordZeros_n (i+3) _ (by omega)] + intro m + have key₂ := pattern_nContinuant1 ℚ (frieze_f g) n (i+1) (by omega) m + simp [add_assoc] at key₂ + rw [key₂] + have h₁ := key (m+(i+1)) + have h₂ := ih (i+1) (by omega) m + have h₃ := ih (i+2) (by omega) m + rw [Rat.sub_eq_add_neg, Rat.add_num_den, Rat.neg_den, Rat.mul_den, h₁, h₂, h₃] + simp ; norm_cast + exact {topBordZeros, topBordOnes, botBordOnes_n, botBordZeros_n, diamond, integral, positive} def arithFriezePatSet (n: ℕ) : Set (ℕ × ℕ → ℚ) := { f | arith_fp f n} @@ -158,7 +303,7 @@ def arithFriezePatSet (n: ℕ) : Set (ℕ × ℕ → ℚ) := -- Now we can use the nonemptyness of Flute n to prove the nonemptyness of arithFriezePatSet n. lemma arithFriezePatSetNonEmpty {n : ℕ} (h : n ≠ 0) : (arithFriezePatSet n).Nonempty := by rcases csteFlute n with ⟨a⟩ - exact ⟨f a, fluteToFrieze a h⟩ + exact ⟨frieze_f a, fluteToFrieze a h⟩