From 3e8aafd23d5e659f989faa2f8acc167fa78dd913 Mon Sep 17 00:00:00 2001 From: Andre Date: Fri, 16 Jun 2023 15:17:43 -0400 Subject: [PATCH] golfed delta_ --- CommAlg/final_poly_type.lean | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean index 07b7bf4..8bc6b9e 100644 --- a/CommAlg/final_poly_type.lean +++ b/CommAlg/final_poly_type.lean @@ -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 section -#check PolyType - example (f : ℤ → ℤ) (hf : ∀ x, f x = x ^ 2) : PolyType f 2 := by unfold PolyType sorry @@ -132,8 +130,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,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 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 induction' d with d hd - -- Base case · rintro f ⟨c, N, hh⟩; rw [PolyType_0 f]; exact ⟨c, N, hh⟩ - -- Induction step · 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⟩)