Part of the base case of \Delta lemma

This commit is contained in:
chelseaandmadrid 2023-06-15 17:51:32 -07:00
parent 300007621a
commit d5b2e4d431

View file

@ -65,7 +65,13 @@ example : Polynomial.eval (100 : ) F = (2 : ) := by
end section end section
-- @[BH, 4.1.2] -- @[BH, 4.1.2]
-- All the polynomials are in [X], all the functions are considered as -- All the polynomials are in [X], all the functions are considered as
noncomputable section noncomputable section
-- Polynomial type of degree d -- Polynomial type of degree d
@ -107,6 +113,10 @@ def f (n : ) := n
end section end section
-- (NO need to prove another direction) Constant polynomial function = constant function -- (NO need to prove another direction) Constant polynomial function = constant function
lemma Poly_constant (F : Polynomial ) (c : ) : lemma Poly_constant (F : Polynomial ) (c : ) :
(F = Polynomial.C (c : )) ↔ (∀ r : , (Polynomial.eval r F) = (c : )) := by (F = Polynomial.C (c : )) ↔ (∀ r : , (Polynomial.eval r F) = (c : )) := by
@ -133,7 +143,6 @@ lemma Poly_shifting (f : ) (g : ) (hf : PolyType f d) (s :
-- set_option pp.all true in -- set_option pp.all true in
-- PolyType 0 = constant function -- PolyType 0 = constant function
lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N : ), ∀ (n : ), (N ≤ n → f n = c) ∧ (c ≠ 0)) := by lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N : ), ∀ (n : ), (N ≤ n → f n = c) ∧ (c ≠ 0)) := by
@ -212,7 +221,6 @@ lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N :
exact this3 n exact this3 n
exact this2.symm exact this2.symm
· have this : Polynomial.degree Poly = 0 := by · have this : Polynomial.degree Poly = 0 := by
simp only [map_intCast] simp only [map_intCast]
exact Polynomial.degree_C H2 exact Polynomial.degree_C H2
@ -221,23 +229,54 @@ lemma PolyType_0 (f : ) : (PolyType f 0) ↔ (∃ (c : ), ∃ (N :
-- Δ of 0 times preserve the function -- Δ of 0 times preserve the function
lemma Δ_0 (f : ) : (Δ f 0) = f := by lemma Δ_0 (f : ) : (Δ f 0) = f := by
tauto tauto
-- Δ 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
lemma Δ_PolyType_d_to_PolyType_0 (f : ) (d : ): PolyType f d → PolyType (Δ f d) 0 := by lemma Δ_d_PolyType_d_to_PolyType_0 (f : ) (d : ): PolyType f d → PolyType (Δ f d) 0 := by
intro h intro h
rcases h with ⟨Poly, hN⟩ rcases h with ⟨Poly, hN⟩
rcases hN with ⟨N, hh⟩ rcases hN with ⟨N, hh⟩
rcases hh with ⟨H1, H2⟩ rcases hh with ⟨H1, H2⟩
have HH2 : d = Polynomial.degree Poly := by have HH2 : d = Polynomial.degree Poly := by
sorry tauto
have HH3 : Polynomial.degree Poly = d := by
tauto
induction' d with d hd induction' d with d hd
-- Base case
· rw [PolyType_0] · rw [PolyType_0]
sorry have this : Poly = Polynomial.C (Polynomial.coeff Poly 0) := by
exact Polynomial.eq_C_of_degree_eq_zero HH3
let d := Polynomial.coeff Poly 0
have this11 : ∃ (c : ), c = d := by
sorry
rcases this11 with ⟨c, this1⟩
have this1 : c = Polynomial.coeff Poly 0 := by
tauto
use c; use N; intro n
constructor
· specialize H1 n
rw [Δ_0]
intro h
have this2 : f n = Polynomial.eval (n : ) Poly := by
tauto
have this3 : f n = (c : ) := by
rw [this2, this1]
let HHH := (Poly_constant Poly c).mp
sorry
exact Iff.mp (Rat.coe_int_inj (f n) c) this3
· intro c0
have this2 : (c : ) = 0 := by
exact congrArg Int.cast c0
have this3 : Polynomial.coeff Poly 0 = 0 := by
rw [←this1, this2]
sorry
-- Induction step
· sorry · sorry
@ -260,12 +299,14 @@ lemma a_to_b (f : ) (d : ) : (∃ (c : ), ∃ (N : ), ∀ (n
tauto tauto
· sorry · 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 : ) : PolyType f d → (∃ (c : ), ∃ (N : ), ∀ (n : ), ((N ≤ n → (Δ f d) (n) = c) ∧ c ≠ 0)) := by
intro h intro h
have : PolyType (Δ f d) 0 := by have : PolyType (Δ f d) 0 := by
apply Δ_PolyType_d_to_PolyType_0 apply Δ_d_PolyType_d_to_PolyType_0
exact h exact h
have this1 : (∃ (c : ), ∃ (N : ), ∀ (n : ), ((N ≤ n → (Δ f d) n = c) ∧ c ≠ 0)) := by have this1 : (∃ (c : ), ∃ (N : ), ∀ (n : ), ((N ≤ n → (Δ f d) n = c) ∧ c ≠ 0)) := by
rw [←PolyType_0] rw [←PolyType_0]
@ -277,6 +318,9 @@ 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