Skip to content

Instantly share code, notes, and snippets.

@adomani

adomani/at_infty.lean Secret

Created Sep 3, 2020
Embed
What would you like to do?
import tactic
import data.polynomial.degree.basic
open polynomial
lemma finset_of_bounded {S : set ℕ} (N : ℕ) {nN : ∀ nS , n ≤ N} : S.finite :=
begin
refine set.finite.subset _ _,
{use {n : ℕ | n ≤ N}},
{exact set.finite_le_nat N,},
{intros s,refine nN s,},
end
lemma le_degree_of_mem_supp {R : Type*} [comm_ring R] {p : polynomial R} : ∀ a : ℕ , a ∈ p.1 → a ≤ nat_degree p :=
begin
intros a,
contrapose,
push_neg,
intros ah,
rw (p.3 a),
push_neg,
apply coeff_eq_zero_of_nat_degree_lt,
exact ah,
end
def rev_at (N : ℕ) : ℕ → ℕ := λ i : ℕ , (N-i) + i*min 1 (i-N)
lemma rev_invol {N i : ℕ} : rev_at N (rev_at N i) = i :=
begin
unfold rev_at,
by_cases i ≤ N,
{have iN : (i - N) = 0, by exact nat.sub_eq_zero_of_le h,
rw iN,
have min10 : min 1 0 = 0, by exact nat.min_zero 1,
have NiN : N - i - N = 0,
refine nat.sub_eq_zero_of_le _,
exact nat.sub_le N i,
rw min10,rw mul_zero,rw add_zero,rw NiN,
rw min10,rw mul_zero,rw add_zero,
exact nat.sub_sub_self h,},
{rw not_le at h,
have iN : 1 ≤ i - N,
apply nat.succ_le_of_lt,
exact nat.sub_pos_of_lt h,
have min1iN : min 1 (i-N) = 1, by exact min_eq_left iN,
rw min1iN,rw mul_one,
have Nile0 : (N-i : int) ≤ 0,
apply le_of_lt,
finish,
have Ni0 : (N-i)=0, by omega,
rw Ni0,rw zero_add,rw min1iN,rw mul_one,rw Ni0,rw zero_add,},
end
lemma rev_support {R : Type*} [comm_ring R] (p : polynomial R) : {a : ℕ | ∃ aap.1 , a = rev_at (nat_degree p) aa}.finite :=
begin
refine finset_of_bounded (nat_degree p),
intros n nH,
cases nH with rn rH,
cases rH,
rw rH_h,
unfold rev_at,
have zerr : 0 ≤ rn, exact zero_le rn,
have rle : rn ≤ nat_degree p,
apply le_degree_of_mem_supp rn,
assumption,
have rneq : (rn - p.nat_degree) = 0,
refine nat.sub_eq_zero_of_le rle,
have : min 1 (rn - p.nat_degree) = 0,
{rw rneq,exact nat.min_zero 1,},
rw this,rw mul_zero,rw add_zero,
refine (nat_degree p).sub_le rn,
end
noncomputable def at_infty {R : Type*} [comm_ring R] : polynomial R → polynomial R := λ p : polynomial R , begin
refine ⟨ (rev_support p).to_finset , λ i : ℕ , p.2 (rev_at (nat_degree p) i) , _ ⟩,
--members
tidy,
{apply a_1_h_left,rw a_1_h_right at a_2,rw ← a_2,apply congr_arg p.2,symmetry,exact rev_invol,},
{symmetry,exact rev_invol,},
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment