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

golfed foofoo

Browse source
This commit is contained in:
Andre 2023-06-16 02:29:33 -04:00
parent 04849a931f
commit 95ddb3c1ff
1 changed files with 25 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
CommAlg/final_poly_type.lean
View file

@ -153,25 +153,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)]⟩ ⟨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⟩ cases' HHHH with d H5; exact ⟨d, by rw[← H5] at HHH; exact HHH⟩
rcases this2 with ⟨c, hthis2⟩ rcases this2 with ⟨c, hthis2⟩
use c; use N; intro n use c; use N; constructor
constructor · intro n
· have this4 : Polynomial.eval (n : ℚ) Poly = c := by have this4 : Polynomial.eval (n : ℚ) Poly = c := by
rw [hthis2]; simp only [map_intCast, Polynomial.eval_int_cast] 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]) exact fun HH1 => Iff.mp (Rat.coe_int_inj (f n) c) (by rw [←this4, H1 n HH1])
· intro c0 · intro c0
simp only [hthis2, c0, Int.cast_zero, map_zero, Polynomial.degree_zero] simp only [hthis2, c0, Int.cast_zero, map_zero, Polynomial.degree_zero]
at this1 at this1
· rintro ⟨c, N, hh⟩ · 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 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⟩ (c : ℚ)).mp rfl) n).symm, by rw [Polynomial.degree_C H2]; rfl⟩
-- Δ of 0 times preserves the function -- Δ 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 -- Δ 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 sorry
-- Δ of d times maps polynomial of degree d to polynomial of degree 0 -- Δ of d times maps polynomial of degree d to polynomial of degree 0
@ -181,22 +181,13 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
induction' d with d hd induction' d with d hd
· intro f h · intro f h
rw [Δ_0] rw [Δ_0]
tauto exact h
· intro f hf · intro f hf
have this1 : PolyType f (d + 1) := by tauto have this4 := hd (Δ f 1) $ (Δ_1 f d) hf
have this2 : PolyType (Δ f (d + 1)) 0 := by rwa [Δ_1_s_equiv_Δ_s_1] at this4
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
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 lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) → (PolyType f d) := by
induction' d with d hd induction' d with d hd
@ -218,12 +209,6 @@ lemma foofoofoo (d : ℕ) : (f : ℤ → ℤ) → (∃ (c : ℤ), ∃ (N : ℤ),
sorry sorry
tauto 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 -- intro h
-- rcases h with ⟨c, N, hh⟩ -- rcases h with ⟨c, N, hh⟩
-- have H1 := λ n => (hh n).left -- have H1 := λ n => (hh n).left
@ -242,19 +227,19 @@ lemma a_to_b (f : ℤ → ℤ) (d : ℕ) : (∃ (c : ℤ), ∃ (N : ℤ), (∀ (
-- -- Induction step -- -- Induction step
-- · sorry -- · sorry
-- [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
-- [BH, 4.1.2] (a) <= (b) -- [BH, 4.1.2] (a) <= (b)
-- f is of polynomial type d → Δ^d f (n) = c for some nonzero integer c for n >> 0 -- 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 lemma b_to_a (f : ℤ → ℤ) (d : ℕ) (poly : PolyType f d) :
intro h (∃ (c : ℤ), ∃ (N : ℤ), (∀ (n : ℤ), N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0) := by
have : PolyType (Δ f d) 0 := by rw [←PolyType_0]; exact Δ_d_PolyType_d_to_PolyType_0 f d poly
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
end
-- @Additive lemma of length for a SES -- @Additive lemma of length for a SES
-- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0 -- Given a SES 0 → A → B → C → 0, then length (A) - length (B) + length (C) = 0
section section