## Stream: new members

### Topic: polynomial.eval_sub rewrite fail

#### Luke Mantle (Feb 09 2023 at 00:43):

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 (Feb 09 2023 at 00:46):

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

#### Kevin Buzzard (Feb 09 2023 at 00:48):

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 (Feb 09 2023 at 00:49):

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

#### Jireh Loreaux (Feb 09 2023 at 03:49):

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 (Feb 09 2023 at 04:00):

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

#### Jake Levinson (Feb 09 2023 at 08:13):

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 (Feb 09 2023 at 08:25):

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

#### Jireh Loreaux (Feb 09 2023 at 13:22):

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 (Feb 09 2023 at 21:26):

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 (Feb 09 2023 at 21:27):

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

Last updated: Dec 20 2023 at 11:08 UTC