polynomial.eval_sub rewrite fail

Stream: new members

[Luke Mantle]

I'm trying to show that the hermite polynomials are indeed each polynomials. I have them defined as real functions through their recursive definition, and I'm working on the last lemma in the code below. I'm wondering why rw polynomial.eval_sub is failing:

import analysis.calculus.mean_value
open polynomial

open set filter

noncomputable theory

@[simp]
def x_sub_dx (f : ℝ → ℝ) :=
id * f - (deriv f)

@[simp]
def hermite (n : ℕ) : ℝ → ℝ :=
nat.iterate x_sub_dx n (λ x, 1)

universe u
lemma iterate_assoc {α : Sort u} (op : α → α) (k : ℕ) :
∀ a : α, nat.iterate op k.succ a = op (nat.iterate op k a) :=
begin
  induction k with k ih;
  intro a,
  { refl, },
  { have test := (op^[k]) a,
    calc (op^[k + 2]) a = (op^[k + 1]) (op a)  : rfl
                  ... = op (op^[k] (op a))     : by apply ih
                  ... = op (op^[k + 1] a)      : rfl, },
end

lemma hermite_succ (n : ℕ) : hermite n.succ = x_sub_dx (hermite n) :=
begin
  apply iterate_assoc,
end

lemma x_sub_dx_def (f : ℝ → ℝ) : x_sub_dx f = id*f - deriv f :=
begin
  refl,
end

lemma x_sub_dx_apply (f : ℝ → ℝ) (x : ℝ) :
x_sub_dx f x = x*(f x) - (deriv f x) :=
begin
  refl,
end


lemma polynomial_deriv_eval (p : polynomial ℝ) :
(λ x, eval x (derivative p)) = (deriv (λ x, eval x p)) :=
begin
  ext,
  simp,
end

-- H_n is a polynomial
lemma is_polynomial_hermite :
∀ n : ℕ, ∃ p : polynomial ℝ, ∀ x : ℝ, p.eval(x) = hermite n x :=
begin
  intro n,
  induction n with n ih,
  { --unfold hermite,
    use 1,
    intro x,
    simp, },
  { --unfold hermite,
    cases ih with q hq,
    use X*q - q.derivative,
    rw hermite_succ,
    -- intro x,
    -- specialize hq x,
    rw x_sub_dx_def,
    rw polynomial.eval_sub,
  }
end

[Kevin Buzzard]

Why don't you just define them directly as polynomials?

[Kevin Buzzard]

Your theorem that you want to prove just involves redefining the Hermite polynomials as polynomials rather than functions, so you have to do it anyway, so why not make it the definition instead, and if you really want the function then just evaluate the polynomial

[Kevin Buzzard]

Let me reiterate that polynomials and functions in lean are totally different objects

[Jireh Loreaux]

import data.polynomial.derivative

open polynomial
open_locale polynomial

variables (R : Type*) [ring R]

noncomputable def hermite (n : ℕ) : polynomial R :=
((λ p, X * p) - derivative)^[n] (C 1)

lemma hermite_zero : hermite R 0 = C 1 := rfl

lemma hermite_succ (n : ℕ) : hermite R (n+1) = X * hermite R n - (hermite R n).derivative :=
by { rw [hermite, function.iterate_succ'], refl }

[Jireh Loreaux]

also, your iterate_assoc is just docs#function.iterate_succ'

[Jake Levinson]

Jireh Loreaux said:

also, your iterate_assoc is just docs#function.iterate_succ'

Strange that this isn’t in the same file or namespace as nat.iterate

[Yaël Dillies]

Yeah, most lemma names pretend it's called function.iterate

[Jireh Loreaux]

By the way, if you're feeling fancy, you might replace (λ p, X * p) with linear_map.mul R R[X] X (but it needs another import), which has the advantage of turning the function you are iterating into a linear map (since docs#polynomial.derivative is).

[Luke Mantle]

Kevin Buzzard said:

Why don't you just define them directly as polynomials?

Thanks, I gave it a go and it was much simpler!

[Luke Mantle]

Jireh Loreaux said:

also, your iterate_assoc is just docs#function.iterate_succ'

Ah, ok, thanks. I was suspecting it existed already, but couldn't find it