-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(ring_theory/polynomial): show gaussian form of hermite n
#18896
Conversation
…gaussian_mul_gaussian, remove hermite_gauss def, change eval to aeval
{ simp_rw [aeval_def, eval₂_eq_eval_map], | ||
apply polynomial.differentiable }, | ||
{ simp_rw [aeval_def, eval₂_eq_eval_map], | ||
apply differentiable.const_mul, | ||
apply polynomial.differentiable }, | ||
{ simp } } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These side goals go away if you work with has_deriv_at
instead of deriv
:
induction n with n ih generalizing x,
{ rw [function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul] },
{ replace ih : (deriv^[n] _) = _ := _root_.funext ih,
have has_deriv_at_gaussian : ∀ x,
has_deriv_at (λ y, real.exp (-(y^2 / 2))) ((-x) * real.exp (-(x^2 / 2))) x,
{ intro x,
simpa [mul_div_cancel_left x (two_ne_zero), neg_mul, mul_comm]
using (((has_deriv_at_id' x).pow 2).div_const 2).neg.exp },
rw [function.iterate_succ_apply', ih],
have := ((polynomial.has_deriv_at_aeval _ _).const_mul ((-1 : ℝ) ^ n)).mul (has_deriv_at_gaussian x),
refine this.deriv.trans _,
sorry },
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually also deriv_const_mul_field
doesn't generate a side goal, I didn't notice it before (versus deriv_const_mul
).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The new version is pretty close to this, let's just go with it.
Is this PR ready to merge? |
My hope was to get #18945 in first since I think that golfs a few proofs slightly here. |
This duplicates every lemma about differentiation of `polynomial.eval` for `polynomial.aeval` too. Some of these turned out to be needed in #18896.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ lukemantle can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Show the equivalence of the polynomial form of the Hermite polynomials to the explicit form involving derivatives of the gaussian function. Co-authored-by: Jake Levinson <levinson.jake@gmail.com> Co-authored-by: Jake Levinson <levinson.jake@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: jakelev <levinson.jake@gmail.com>
Build failed: |
Thanks 🎉 bors merge |
Show the equivalence of the polynomial form of the Hermite polynomials to the explicit form involving derivatives of the gaussian function. Co-authored-by: Jake Levinson <levinson.jake@gmail.com> Co-authored-by: lukemantle <lukeomantle@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
hermite n
hermite n
Show the equivalence of the polynomial form of the Hermite polynomials to the explicit form involving derivatives of the gaussian function.
Co-authored-by: Jake Levinson levinson.jake@gmail.com
We are interested in feedback about two parts of this PR:
- Should the definition(removed)gaussian
be removed and replaced with its definition written out explicitly? Or ifgaussian
is kept, should it be placed somewhere else in mathlib?- Should the auxiliary definition(removed)hermite_gauss
also be removed the same way? If not, should it be hidden usingprotected def
or something along these lines?