Merge branch 'main' of github.com:GTBarkley/comm_alg into main

2024-12-26 07:38:36 -06:00 · 2023-06-16 10:12:11 -07:00 · 2023-06-16 10:12:11 -07:00 · c9d02bbf59
commit c9d02bbf59
parent d0a6d8605e 17f6d2ab85
1 changed files with 21 additions and 101 deletions
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@ -22,34 +22,20 @@ macro "obviously" : tactic =>
        -- | nlinarith; done
        | fail "No, this is not obvious."))

-
 -- Testing of Polynomial
 section Polynomial
 noncomputable section
-#check Polynomial 
-#check Polynomial (ℚ)
-#check Polynomial.eval
-

 example (f : Polynomial ℚ) (hf : f = Polynomial.C (1 : ℚ)) : Polynomial.eval 2 f = 1 := by
  have : ∀ (q : ℚ), Polynomial.eval q f = 1 := by
    sorry
-  obviously
-
-- example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : Polynomial.eval 2 f = 4 := by
--   sorry

 -- degree of a constant function is ⊥ (is this same as -1 ???)
 #print Polynomial.degree_zero

 def F : Polynomial ℚ := Polynomial.C (2 : ℚ)
-#print F
-#check F
-#check Polynomial.degree F
-#check Polynomial.degree 0
-#check WithBot ℕ
+
 -- #eval Polynomial.degree F
-#check Polynomial.eval 1 F
 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]
@ -57,41 +43,21 @@ example : Polynomial.eval (100 : ℚ) F = (2 : ℚ) := by
  simp

 -- Treat polynomial f ∈ ℚ[X] as a function f : ℚ → ℚ
-#check CoeFun
-
-
-

 end section

-
-
-
-
-- @[BH, 4.1.2]
-
-
-
 -- All the polynomials are in ℚ[X], all the functions are considered as ℤ → ℤ
 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
 section
-- structure PolyType (f : ℤ → ℤ) where
--   Poly : Polynomial ℤ
--   d : 
--   N : ℤ
--   Poly_equal : ∀ n ∈ ℤ → f n = Polynomial.eval n : ℤ Poly

 #check PolyType

 example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
  unfold PolyType
  sorry
-  -- use Polynomial.monomial (2 : ℤ) (1 : ℤ)
-  -- have' := hf 0; ring_nf at this
-  -- exact this
 
 end section

@ -101,22 +67,13 @@ def Δ : (ℤ → ℤ) → ℕ → (ℤ → ℤ)
  | f, 0 => f
  | f, d + 1 => fun (n : ℤ) ↦ (Δ f d) (n + 1) - (Δ f d) (n)  
 section
-- def Δ (f : ℤ → ℤ) (d : ℕ) := fun (n : ℤ) ↦ f (n + 1) - f n
-- def add' : ℕ → ℕ → ℕ
--   | 0, m => m 
--   | n+1, m => (add' n m) + 1
-- #eval add' 5 10
+
 #check Δ
 def f (n : ℤ) := n
 #eval (Δ f 1) 100
 -- #check (by (show_term unfold Δ) : Δ f 0=0)
 end section

-
-
-
-
-
 -- (NO need to prove another direction) Constant polynomial function = constant function
 lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) : 
  (F = Polynomial.C (c : ℚ)) ↔ (∀ r : ℚ, (Polynomial.eval r F) = (c : ℚ)) := by
@ -129,9 +86,6 @@ lemma Poly_constant (F : Polynomial ℚ) (c : ℚ) :
    simp
  · 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]
@ -153,25 +107,25 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
        ⟨f N, by simp [(Poly_constant Poly c).mp HHH N, H1 N (le_refl N)]⟩
      cases' HHHH with d H5; exact ⟨d, by rw[← H5] at HHH; exact HHH⟩
    rcases this2 with ⟨c, hthis2⟩ 
-    use c; use N; intro n
-    constructor
-    · have this4 : Polynomial.eval (n : ℚ) Poly = c := by
+    use c; use N; constructor
+    · intro n
+      have this4 : Polynomial.eval (n : ℚ) Poly = c := by
        rw [hthis2]; simp only [map_intCast, Polynomial.eval_int_cast]
      exact fun HH1 => Iff.mp (Rat.coe_int_inj (f n) c) (by rw [←this4, H1 n HH1])
    · intro c0
      simp only [hthis2, c0, Int.cast_zero, map_zero, Polynomial.degree_zero] 
        at this1
  · rintro ⟨c, N, hh⟩
-    have H2 : (c : ℚ) ≠ 0 := by simp only [ne_eq, Int.cast_eq_zero]; exact (hh 0).2 
+    have H2 : (c : ℚ) ≠ 0 := by simp only [ne_eq, Int.cast_eq_zero, hh]
    exact ⟨Polynomial.C (c : ℚ), N, fun n Nn 
-      => by rw [(hh n).1 Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ)) 
+      => by rw [hh.1 n Nn]; exact (((Poly_constant (Polynomial.C (c : ℚ)) 
      (c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩

 -- Δ of 0 times preserves the function
-lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by tauto
-
+lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by rfl
+  --simp only [Δ]
 -- Δ of 1 times decreaes the polynomial type by one
-lemma Δ_1 (f : ℤ → ℤ) (d : ℕ): d > 0 → PolyType f d → PolyType (Δ f 1) (d - 1) := by
+lemma Δ_1 (f : ℤ → ℤ) (d : ℕ): PolyType f (d + 1) → PolyType (Δ f 1) d := by
  sorry

 -- Δ of d times maps polynomial of degree d to polynomial of degree 0
@ -181,22 +135,13 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
  induction' d with d hd
  · intro f h
    rw [Δ_0]
-    tauto
+    exact h
  · intro f hf
-    have this1 : PolyType f (d + 1) := by tauto
-    have this2 : PolyType (Δ f (d + 1)) 0 := by
-      have this3 : PolyType (Δ f 1) d := by
-        have this4 : d + 1 > 0 := by positivity
-        have this5 : (d + 1) > 0 → PolyType f (d + 1) → PolyType (Δ f 1) d := Δ_1 f (d + 1)
-        exact this5 this4 this1
-      clear hf
-      specialize hd (Δ f 1)
-      have this4 : PolyType (Δ (Δ f 1) d) 0 := by tauto
-      rw [Δ_1_s_equiv_Δ_s_1] at this4
-      tauto
-    tauto
+    have this4 := hd (Δ f 1) $ (Δ_1 f d) hf
+    rwa [Δ_1_s_equiv_Δ_s_1] at this4

-lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := fun h => (foofoo d f) h
+lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d → PolyType (Δ f d) 0 := 
+  fun h => (foofoo d f) h

 lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d)  := by
  induction' d with d hd
@ -218,43 +163,18 @@ lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ),
      sorry
    tauto

-
-
 -- [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
-  -- intro h
-  -- rcases h with ⟨c, N, hh⟩
-  -- have H1 := λ n => (hh n).left
-  -- have H2 := λ n => (hh n).right
-  -- clear hh
-  -- have H2 : c ≠ 0 := by
-  --   tauto
-  -- induction' d with d hd
-
-  -- -- Base case
-  -- · rw [PolyType_0]
-  --   use c
-  --   use N
-  --   tauto
-
-  -- -- Induction step
-  -- · sorry

 -- [BH, 4.1.2] (a) <= (b)
 -- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0
-lemma b_to_a (f : ℤ → ℤ) (d : ℕ) : PolyType f d → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) := by
-  intro h
-  have : PolyType (Δ f d) 0 := by
-    apply Δ_d_PolyType_d_to_PolyType_0
-    exact h
-  have this1 : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), (N ≤ n → (Δ f d) n = c)) ∧ c ≠ 0) := by
-    rw [←PolyType_0]
-    exact this
-  exact this1
-end
+lemma b_to_a (f : ℤ → ℤ) (d : ℕ) (poly : PolyType f d) : 
+    (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) := by
+  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