SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 07:38:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

golfed delta_

Browse source
This commit is contained in:
Andre 2023-06-16 15:17:43 -04:00
parent c8797956ab
commit 3e8aafd23d
1 changed files with 3 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
CommAlg/final_poly_type.lean
View file

@ -53,8 +53,6 @@ noncomputable section
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 section
#check PolyType
example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by
unfold PolyType unfold PolyType
sorry sorry
@ -132,8 +130,8 @@ lemma PolyType_0 (f : ℤ → ℤ) : (PolyType f 0) ↔ (∃ (c : ℤ), ∃ (N :
-- Δ of 0 times preserves the function -- Δ of 0 times preserves the function
lemma Δ_0 (f : ℤ → ℤ) : (Δ f 0) = f := by rfl 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 lemma Δ_1 (f : ℤ → ℤ) (d : ℕ) : PolyType f (d + 1) → PolyType (Δ f 1) d := by
intro h intro h
simp only [PolyType, Δ, Int.cast_sub, exists_and_right] simp only [PolyType, Δ, Int.cast_sub, exists_and_right]
@ -186,20 +184,15 @@ lemma Δ_d_PolyType_d_to_PolyType_0 (f : ℤ → ℤ) (d : ℕ): PolyType f d
-- The "reverse" of Δ of 1 times increases the polynomial type by one -- 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 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] 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) let G := fun (q : ℤ) => f (N)
sorry sorry
lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → lemma foo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n →
(Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d) := by (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d) := by
induction' d with d hd induction' d with d hd
-- Base case
· rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩ · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩
-- Induction step
· exact fun f ⟨c, N, ⟨H, c0⟩⟩ => · 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⟩) Δ_1_ f d (hd (Δ f 1) ⟨c, N, fun n h => by rw [← H n h, Δ_1_s_equiv_Δ_s_1], c0⟩)