[Merged by Bors] - feat(ring_theory/polynomial): show gaussian form of hermite n

src/analysis/calculus/cont_diff.lean

@@ -2296,6 +2296,16 @@ lemma cont_diff.continuous_deriv (h : cont_diff 𝕜 n f₂) (hn : 1 ≤ n) :
   continuous (deriv f₂) :=
 (cont_diff_succ_iff_deriv.mp (h.of_le hn)).2.continuous
 
+lemma cont_diff.iterate_deriv :
+∀ (n : ℕ) {f₂ : 𝕜 → F} (hf : cont_diff 𝕜 ∞ f₂), cont_diff 𝕜 ∞ (deriv^[n] f₂)
+| 0       f₂ hf := hf
+| (n + 1) f₂ hf := cont_diff.iterate_deriv n (cont_diff_top_iff_deriv.mp hf).2
+
+lemma cont_diff.iterate_deriv' (n : ℕ) :
+∀ (k : ℕ) {f₂ : 𝕜 → F} (hf : cont_diff 𝕜 (n + k : ℕ) f₂), cont_diff 𝕜 n (deriv^[k] f₂)
+| 0       f₂ hf := hf
+| (n + 1) f₂ hf := cont_diff.iterate_deriv' n (cont_diff_succ_iff_deriv.mp hf).2
+
 end deriv
 
 section restrict_scalars

src/analysis/calculus/deriv.lean

@@ -5,6 +5,7 @@ Authors: Gabriel Ebner, Sébastien Gouëzel
 -/
 import analysis.calculus.fderiv
 import data.polynomial.derivative
+import data.polynomial.algebra_map
 import linear_algebra.affine_space.slope
 
 /-!
@@ -1880,6 +1881,10 @@ p.differentiable.differentiable_on
 @[simp] protected lemma deriv : deriv (λx, p.eval x) x = p.derivative.eval x :=
 (p.has_deriv_at x).deriv
 
+@[simp] protected lemma deriv_aeval {R : Type*} [comm_semiring R] [algebra R 𝕜] (p : polynomial R) :
+  deriv (λ (x : 𝕜), aeval x p) x = aeval x (derivative p) :=
+by simp [aeval_def, eval₂_eq_eval_map]
+
 protected lemma deriv_within (hxs : unique_diff_within_at 𝕜 s x) :
   deriv_within (λx, p.eval x) s x = p.derivative.eval x :=
 begin

src/ring_theory/polynomial/hermite.lean → src/ring_theory/polynomial/hermite/basic.lean

@@ -19,6 +19,7 @@ This file defines `polynomial.hermite n`, the nth probabilist's Hermite polynomi
 
 ## Results
 
+* `polynomial.hermite_succ`: the recursion `hermite (n+1) = (x - d/dx) (hermite n)`
 * `polynomial.coeff_hermite_of_odd_add`: for `n`,`k` where `n+k` is odd, `(hermite n).coeff k` is
   zero.
 * `polynomial.monic_hermite`: for all `n`, `hermite n` is monic.
@@ -39,6 +40,7 @@ noncomputable def hermite : ℕ → polynomial ℤ
 | 0     := 1
 | (n+1) := X * (hermite n) - (hermite n).derivative
 
+/-- The recursion `hermite (n+1) = (x - d/dx) (hermite n)` -/
 @[simp] lemma hermite_succ (n : ℕ) : hermite (n+1) = X * (hermite n) - (hermite n).derivative :=
 by rw hermite
 

src/ring_theory/polynomial/hermite/gaussian.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2023 Luke Mantle. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Luke Mantle, Jake Levinson
+-/
+
+import ring_theory.polynomial.hermite.basic
+import analysis.special_functions.exp
+import analysis.special_functions.exp_deriv
+
+/-!
+# Hermite polynomials and Gaussians
+
+This file shows that the Hermite polynomial `hermite n` is (up to sign) the
+polynomial factor occurring in the `n`th derivative of a gaussian.
+
+## Results
+
+* `polynomial.deriv_gaussian_eq_hermite_mul_gaussian`:
+  The Hermite polynomial is (up to sign) the polynomial factor occurring in the
+  `n`th derivative of a gaussian.
+
+## References
+
+* [Hermite Polynomials](https://en.wikipedia.org/wiki/Hermite_polynomials)
+
+-/
+
+noncomputable theory
+open polynomial
+
+namespace polynomial
+
+/-- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a gaussian -/
+lemma deriv_gaussian_eq_hermite_mul_gaussian (n : ℕ) (x : ℝ) :
+  deriv^[n] (λ y, real.exp (-(y^2 / 2))) x =
+  (-1 : ℝ)^n * aeval x (hermite n) * real.exp (-(x^2 / 2)) :=
+begin
+  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 deriv_gaussian : deriv (λ y, real.exp (-(y^2 / 2))) x = (-x) * real.exp (-(x^2 / 2)),
+    { simp [mul_comm, ← neg_mul] },
+    rw [function.iterate_succ_apply', ih, deriv_mul, deriv_const_mul, pow_succ (-1 : ℝ),
+        deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, polynomial.deriv_aeval],
+    ring,
+    { 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 } }
+end
+
+lemma hermite_eq_deriv_gaussian (n : ℕ) (x : ℝ) :
+  aeval x (hermite n) =
+  (-1 : ℝ)^n * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x) / real.exp (-(x^2 / 2)) :=
+begin
+  rw deriv_gaussian_eq_hermite_mul_gaussian,
+  field_simp [real.exp_ne_zero],
+  rw [← @smul_eq_mul ℝ _ ((-1)^n), ← inv_smul_eq_iff₀, mul_assoc, smul_eq_mul,
+      ← inv_pow, ← neg_inv, inv_one],
+  exact pow_ne_zero _ (by norm_num),
+end
+
+lemma hermite_eq_deriv_gaussian' (n : ℕ) (x : ℝ) :
+  aeval x (hermite n) =
+  (-1 : ℝ)^n * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x) * real.exp (x^2 / 2) :=
+begin
+  rw [hermite_eq_deriv_gaussian, real.exp_neg],
+  field_simp [real.exp_ne_zero],
+end
+
+end polynomial