at_infty.lean

import tactic
import data.polynomial.degree.basic

open polynomial

lemma finset_of_bounded {S : set ℕ} (N : ℕ) {nN : ∀ n ∈ S , 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 : ℕ | ∃ aa ∈ p.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