# Zulip Chat Archive

## 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