Merge pull request #98 from GTBarkley/monalisa

Monalisa

CommAlg/final_poly_type.lean

@@ -5,7 +5,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 set_option maxHeartbeats 0
 macro "ls" : tactic => `(tactic|library_search)
 
--- New tactic "obviously"
+-- From Kyle : New tactic "obviously"
 macro "obviously" : tactic =>
   `(tactic| (
       first
@@ -15,6 +15,7 @@ macro "obviously" : tactic =>
         | simp; tauto; done; dbg_trace "it was simp tauto"
         | rfl; done; dbg_trace "it was rfl"
         | norm_num; done; dbg_trace "it was norm_num"
+        | norm_cast; done; dbg_trace "it was norm_cast"
         | /-change (@Eq ℝ _ _);-/ linarith; done; dbg_trace "it was linarith"
         -- | gcongr; done
         | ring; done; dbg_trace "it was ring"
@@ -40,7 +41,7 @@ example : Polynomial.eval (100 : ℚ) F = (2 : ℚ) := by
   refine Iff.mpr (Rat.ext_iff (Polynomial.eval 100 F) 2) ?_
   simp only [Rat.ofNat_num, Rat.ofNat_den]
   rw [F]
-  simp
+  simp [simp]
 
 -- Treat polynomial f ∈ ℚ[X] as a function f : ℚ → ℚ
 
@@ -50,11 +51,11 @@ end section
 noncomputable section
 -- Polynomial type of degree d
 @[simp]
-def PolyType (f : ℤ → ℤ) (d : ℕ) := ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ d = Polynomial.degree Poly
+def PolyType (f : ℤ → ℤ) (d : ℕ) := 
+  ∃ Poly : Polynomial ℚ, ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → f n = Polynomial.eval (n : ℚ) Poly) ∧ 
+    d = Polynomial.degree Poly
 section
 
-#check PolyType
-
 example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
   unfold PolyType
   sorry
@@ -71,12 +72,10 @@ def Δ : (ℤ → ℤ) → ℕ → (ℤ → ℤ)
 lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) : 
     (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
   constructor
-  · intro h
-    rintro r
+  · intro h r
     refine Iff.mpr (Rat.ext_iff (Polynomial.eval r F) c) ?_
     simp only [Rat.ofNat_num, Rat.ofNat_den]
-    rw [h]
-    simp
+    simp [h]
   · sorry
 
 -- Get the polynomial G (X) = F (X + s) from the polynomial F(X)
@@ -84,22 +83,15 @@ lemma Polynomial_shifting (F : Polynomial ℚ) (s : ℚ) : ∃ (G : Polynomial
   sorry
 
 -- Shifting doesn't change the polynomial type
-lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℤ) (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
-  simp only [PolyType]
-  rcases hf with ⟨F, hh⟩
-  rcases hh with ⟨N,s1, s2⟩
-  have this : ∃ (G : Polynomial ℚ), (∀ (x : ℚ), Polynomial.eval x G = Polynomial.eval (x + s) F) ∧ (Polynomial.degree G = Polynomial.degree F) := by
-    exact Polynomial_shifting F s
-  rcases this with ⟨Poly, h1, h2⟩
-  use Poly
-  use N
-  constructor
-  · intro n
-    specialize s1 (n + s)
-    intro hN
-    have this1 : f (n + s) = Polynomial.eval (n + s : ℚ) F := by
-      sorry
-    sorry
+lemma Poly_shifting (f : ℤ → ℤ) (g : ℤ → ℤ) (hf : PolyType f d) (s : ℕ) 
+    (hfg : ∀ (n : ℤ), f (n + s) = g (n)) : PolyType g d := by
+  rcases hf with ⟨F, ⟨N, s1, s2⟩⟩
+  rcases (Polynomial_shifting F s) with ⟨Poly, h1, h2⟩
+  use Poly, N; constructor
+  · intro n hN
+    have this1 : f (n + s) = Polynomial.eval (n + (s : ℚ)) F := by
+      rw [s1 (n + s) (by linarith)]; norm_cast
+    rw [←hfg n, this1]; exact (h1 n).symm
   · rw [h2, s2]
 
 -- PolyType 0 = constant function
@@ -132,8 +124,8 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
 
 -- Δ of 0 times preserves the function
 lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by rfl
-  --simp only [Δ]
--- Δ of 1 times decreaes the polynomial type by one
+
+-- Δ of 1 times decreaes the polynomial type by one --can be golfed
 lemma Δ_1 (f : ℤ → ℤ) (d : ℕ) : PolyType f (d + 1) → PolyType (Δ f 1) d := by
   intro h
   simp only [PolyType, Δ, Int.cast_sub, exists_and_right]
@@ -186,53 +178,21 @@ lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d
 
 -- The "reverse" of Δ of 1 times increases the polynomial type by one
 lemma Δ_1_ (f : ℤ → ℤ) (d : ℕ) : PolyType (Δ f 1) d → PolyType f (d + 1) := by
-  intro h
+  rintro ⟨P, N, ⟨h1, h2⟩⟩ 
   simp only [PolyType, Nat.cast_add, Nat.cast_one, exists_and_right]
-  rcases h with ⟨P, N, h⟩
-  rcases h with ⟨h1, h2⟩
   let G := fun (q : ℤ) => f (N)
   sorry
 
-
-lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
+lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → 
+    (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
   induction' d with d hd
-
-  -- Base case
-  · intro f
-    intro h
-    rcases h with ⟨c, N, hh⟩
-    rw [PolyType_0]
-    use c
-    use N
-    tauto
-
-  -- Induction step
-  · intro f
-    intro h
-    rcases h with ⟨c, N, h⟩
-    have this : PolyType f (d + 1) := by
-      rcases h with ⟨H,c0⟩
-      let g := (Δ f 1)
-      have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ g d) (n) = c) ∧ c ≠ 0) := by
-        use c; use N
-        constructor
-        · intro n
-          specialize H n
-          intro h
-          have this : Δ f (d + 1) n = c := by tauto
-          rw [←this]
-          rw [Δ_1_s_equiv_Δ_s_1] 
-        · tauto 
-      have this2 : PolyType g d := by
-        apply hd
-        tauto
-      exact Δ_1_ f d this2
-    exact this
+  · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩
+  · exact fun f ⟨c, N, ⟨H, c0⟩⟩ =>
+      Δ_1_ f d (hd (Δ f 1) ⟨c, N, fun n h => by rw [← H n h, Δ_1_s_equiv_Δ_s_1], c0⟩)
 
 -- [BH, 4.1.2] (a) => (b)
 -- Δ^d f (n) = c for some nonzero integer c for n >> 0 → f is of polynomial type d
-lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := by
-  sorry
+lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → PolyType f d := fun h => (foo d f) h
 
 -- [BH, 4.1.2] (a) <= (b)
 -- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0
@@ -241,6 +201,7 @@ lemma b_to_a (f : ℤ → ℤ) (d : ℕ) (poly : PolyType f d) :
   rw [←PolyType_0]; exact Δ_d_PolyType_d_to_PolyType_0 f d poly
 
 end
+
 -- @Additive lemma of length for a SES
 -- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 
 section