[Merged by Bors] - feat(ring_theory/polynomial): define the probabilist's Hermite polynomials #18739

lukemantle · 2023-04-04T21:50:16Z

Define the Hermite polynomials recursively, and show this is equivalent to the result of iterating the operation x - d/dx on the constant polynomial 1.

Future PRs will include several equivalent characterizations:

Recursive and explicit expressions for the coefficients
Definition based on the nth derivative of the Gaussian function

Co-authored-by: Jake Levinson levinson.jake@gmail.com

Currently, hermite n is defined as a polynomial over ℤ. Would it better to generalize this to a polynomial over comm_ring R?

define the Hermite polynomials

src/ring_theory/polynomial/hermite.lean

eric-wieser · 2023-04-04T23:00:30Z

Can you add the result that (hermite n).monic?

src/ring_theory/polynomial/hermite.lean

jakelev · 2023-04-05T05:25:51Z

Whoops - misclicked the "close" button. Sorry about that.

jakelev · 2023-04-06T19:46:50Z

@eric-wieser

Can you add the result that (hermite n).monic?

I think this will be easier once @lukemantle has PRed coeff.lean, which includes
https://github.com/lukemantle/hermite/blob/2e857f22b171febadbed9a9822e64c4b11446b04/src/coeff.lean#L39

lemma hermite_coeff_upper' (n k : ℕ) (hnk : n < k) : coeff (hermite n) k = 0

and
https://github.com/lukemantle/hermite/blob/2e857f22b171febadbed9a9822e64c4b11446b04/src/coeff.lean#L45

lemma hermite_coeff_top (n : ℕ) : coeff (hermite n) n = 1

eric-wieser · 2023-04-07T22:11:08Z

I left some comments at 7e00f85#comments, they seem not to be showing up here

src/ring_theory/polynomial/hermite.lean

eric-wieser

I recommend you add an entry to https://github.com/leanprover-community/mathlib4/wiki/port-comments/_edit asking people not to port this file yet; I imagine you will want to add to it in a future PR, and having someone port it immediately will just be unhelpful.

src/ring_theory/polynomial/hermite.lean

Co-authored-by: jakelev <levinson.jake@gmail.com>

lukemantle · 2023-04-10T18:03:03Z

I recommend you add an entry to https://github.com/leanprover-community/mathlib4/wiki/port-comments/_edit asking people not to port this file yet; I imagine you will want to add to it in a future PR, and having someone port it immediately will just be unhelpful.

Ok, that sounds like a good idea. How can I add an entry to that file?

src/ring_theory/polynomial/hermite.lean

mcdoll · 2023-04-18T01:33:46Z

Just merge master, that will solve the lint-style issue.

eric-wieser · 2023-04-18T08:16:06Z

src/ring_theory/polynomial/hermite.lean

+/-- the nth probabilist's Hermite polynomial -/
+noncomputable def hermite : ℕ → polynomial ℤ
+| 0     := 1
+| (n+1) := X * (hermite n) - (hermite n).derivative
+
+@[simp] lemma hermite_succ {n : ℕ} : hermite (n+1) =  X * (hermite n) - (hermite n).derivative :=
+by rw hermite
+
+lemma hermite_eq_iter {n : ℕ} : hermite n = nat.iterate (λp, X*p - p.derivative) n 1 :=
+begin
+  induction n with n ih,
+  { refl },
+  { rw [function.iterate_succ_apply', ← ih, hermite_succ] }
+end
+
+@[simp] lemma hermite_zero : hermite 0 = C 1 := rfl
+
+@[simp] lemma hermite_one : hermite 1 = X :=
+begin
+  rw [hermite_succ, hermite_zero],
+  simp only [map_one, mul_one, derivative_one, sub_zero]
+end


I think this should all be wrapped in namespace polynomial

eric-wieser · 2023-04-18T08:16:23Z

src/ring_theory/polynomial/hermite.lean

+| 0     := 1
+| (n+1) := X * (hermite n) - (hermite n).derivative
+
+@[simp] lemma hermite_succ {n : ℕ} : hermite (n+1) =  X * (hermite n) - (hermite n).derivative :=


n should be explicit (() not {}) here and below

eric-wieser · 2023-04-18T08:17:22Z

src/ring_theory/polynomial/hermite.lean

+@[simp] lemma hermite_succ {n : ℕ} : hermite (n+1) =  X * (hermite n) - (hermite n).derivative :=
+by rw hermite
+
+lemma hermite_eq_iter {n : ℕ} : hermite n = nat.iterate (λp, X*p - p.derivative) n 1 :=


Lean has notation for nat.iterate, I think it's

Suggested change

lemma hermite_eq_iter {n : ℕ} : hermite n = nat.iterate (λp, X*p - p.derivative) n 1 :=

lemma hermite_eq_iterate {n : ℕ} : hermite n = (λ p, X*p - p.derivative)^[n] 1 :=

I also changed the name; we rarely abbreviate function names unless they're really really long.

src/ring_theory/polynomial/hermite.lean

eric-wieser · 2023-04-18T21:50:56Z

bors d+

Please merge once CI passes! Make sure you've done this first

Ok, that sounds like a good idea. How can I add an entry to that file?

I've done it for you; maybe you don't have permission to edit the page?

bors · 2023-04-18T21:50:57Z

✌️ lukemantle can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

lukemantle · 2023-04-18T21:58:44Z

bors d+

Please merge once CI passes! Make sure you've done this first

I recommend you add an entry to https://github.com/leanprover-community/mathlib4/wiki/port-comments/_edit asking people not to port this file yet; I imagine you will want to add to it in a future PR, and having someone port it immediately will just be unhelpful.

Ok, that sounds like a good idea. How can I add an entry to that file?

Just click "edit" and add a line in the style of the existing lines, referring to your file name.

Huh, I don't see the edit icon on the wiki sidebar. Maybe I'm missing some permission? I see you've already added an entry about ring_theory.polynomial.hermite

src/ring_theory/polynomial/hermite.lean

mcdoll · 2023-04-19T02:25:40Z

You probably need non-master write access to mathlib4.

eric-wieser · 2023-04-19T08:40:11Z

bors merge

Thanks!

…mials (#18739) Define the Hermite polynomials recursively, and show this is equivalent to the result of iterating the operation `x - d/dx` on the constant polynomial `1`. Future PRs will include several equivalent characterizations: - Recursive and explicit expressions for the coefficients - Definition based on the nth derivative of the Gaussian function Co-authored-by: Jake Levinson <levinson.jake@gmail.com> Co-authored-by: lukemantle <62187700+lukemantle@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bors · 2023-04-19T09:44:46Z

Pull request successfully merged into master.

Build succeeded:

Create hermite.lean

f6ae090

define the Hermite polynomials

lukemantle added the awaiting-review The author would like community review of the PR label Apr 4, 2023

lukemantle added 2 commits April 4, 2023 14:57

fix author line in hermite.lean

7ef85a4

move open line in hermite.lean

28f7736

eric-wieser reviewed Apr 4, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 4, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Outdated Show resolved Hide resolved

mcdoll reviewed Apr 5, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Outdated Show resolved Hide resolved

jakelev closed this Apr 5, 2023

jakelev reopened this Apr 5, 2023

eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 6, 2023

mcdoll mentioned this pull request Apr 7, 2023

Define Hermite polynomials #15566

Closed

change definition of hermite n, remove x_sub_dx

7e00f85

lukemantle added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 7, 2023

lukemantle added 2 commits April 8, 2023 12:16

move open polynomial below docstring

6a33fc7

restore hermite_eq_iter

3bea4f0

eric-wieser reviewed Apr 8, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Show resolved Hide resolved

eric-wieser reviewed Apr 8, 2023

View reviewed changes

jakelev reviewed Apr 8, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Outdated Show resolved Hide resolved

shorten proof of hermite_eq_iter

5a69342

Co-authored-by: jakelev <levinson.jake@gmail.com>

mcdoll reviewed Apr 14, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Outdated Show resolved Hide resolved

sgouezel reviewed Apr 14, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Outdated Show resolved Hide resolved

sgouezel reviewed Apr 14, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Outdated Show resolved Hide resolved

sgouezel removed the awaiting-review The author would like community review of the PR label Apr 16, 2023

Merge branch 'master' into hermite

61c4eea

eric-wieser reviewed Apr 18, 2023

View reviewed changes

lukemantle added 3 commits April 18, 2023 12:23

Update hermite.lean

9a4f789

make n in hermite_succ and hermite_eq_iter explicit

e3aceb9

rename to hermite_eq_iterate and change notation

edc778e

eric-wieser reviewed Apr 18, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Outdated Show resolved Hide resolved

eric-wieser added 3 commits April 18, 2023 22:48

Update src/ring_theory/polynomial/hermite.lean

c4bdf2b

whtiespace

d9a8e01

Tweak docs

4863470

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 18, 2023

split oversized line

1fe6ee9

eric-wieser added the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 18, 2023

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 18, 2023

mcdoll reviewed Apr 19, 2023

View reviewed changes

src/ring_theory/polynomial/hermite.lean Show resolved Hide resolved

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Apr 19, 2023

bors bot changed the title ~~feat(ring_theory/polynomial): define the probabilist's Hermite polynomials~~ [Merged by Bors] - feat(ring_theory/polynomial): define the probabilist's Hermite polynomials Apr 19, 2023

bors bot closed this Apr 19, 2023

bors bot deleted the hermite branch April 19, 2023 09:44

eric-wieser mentioned this pull request May 14, 2023

[Merged by Bors] - feat(nat/factorial): add double factorials #18994

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(ring_theory/polynomial): define the probabilist's Hermite polynomials #18739

[Merged by Bors] - feat(ring_theory/polynomial): define the probabilist's Hermite polynomials #18739

lukemantle commented Apr 4, 2023 •

edited by eric-wieser

eric-wieser commented Apr 4, 2023

jakelev commented Apr 5, 2023

jakelev commented Apr 6, 2023 •

edited

eric-wieser commented Apr 7, 2023

eric-wieser left a comment

lukemantle commented Apr 10, 2023

mcdoll commented Apr 18, 2023

eric-wieser Apr 18, 2023

eric-wieser Apr 18, 2023

eric-wieser Apr 18, 2023

eric-wieser commented Apr 18, 2023 •

edited

bors bot commented Apr 18, 2023

lukemantle commented Apr 18, 2023

mcdoll commented Apr 19, 2023

eric-wieser commented Apr 19, 2023

bors bot commented Apr 19, 2023

	lemma hermite_eq_iter {n : ℕ} : hermite n = nat.iterate (λp, X*p - p.derivative) n 1 :=
	lemma hermite_eq_iterate {n : ℕ} : hermite n = (λ p, X*p - p.derivative)^[n] 1 :=

[Merged by Bors] - feat(ring_theory/polynomial): define the probabilist's Hermite polynomials #18739

[Merged by Bors] - feat(ring_theory/polynomial): define the probabilist's Hermite polynomials #18739

Conversation

lukemantle commented Apr 4, 2023 • edited by eric-wieser

eric-wieser commented Apr 4, 2023

jakelev commented Apr 5, 2023

jakelev commented Apr 6, 2023 • edited

eric-wieser commented Apr 7, 2023

eric-wieser left a comment

Choose a reason for hiding this comment

lukemantle commented Apr 10, 2023

mcdoll commented Apr 18, 2023

eric-wieser Apr 18, 2023

Choose a reason for hiding this comment

eric-wieser Apr 18, 2023

Choose a reason for hiding this comment

eric-wieser Apr 18, 2023

Choose a reason for hiding this comment

eric-wieser commented Apr 18, 2023 • edited

bors bot commented Apr 18, 2023

lukemantle commented Apr 18, 2023

mcdoll commented Apr 19, 2023

eric-wieser commented Apr 19, 2023

bors bot commented Apr 19, 2023

lukemantle commented Apr 4, 2023 •

edited by eric-wieser

jakelev commented Apr 6, 2023 •

edited

eric-wieser commented Apr 18, 2023 •

edited