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

src/analysis/calculus/cont_diff.lean

@@ -2296,6 +2296,11 @@ 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 (deriv f₂) (cont_diff_top_iff_deriv.mp hf).2
+
 end deriv
 
 section restrict_scalars

src/ring_theory/polynomial/hermite.lean

@@ -6,6 +6,8 @@ Authors: Luke Mantle
 
 import data.polynomial.derivative
 import data.nat.parity
+import analysis.special_functions.exp
+import analysis.special_functions.exp_deriv
 
 /-!
 # Hermite polynomials
@@ -16,12 +18,15 @@ This file defines `polynomial.hermite n`, the nth probabilist's Hermite polynomi
 
 * `polynomial.hermite n`: the `n`th probabilist's Hermite polynomial,
   defined recursively as a `polynomial ℤ`
+* `gaussian`: the real Gaussian function
 
 ## Results
 
 * `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.
+* `polynomial.hermite_eq_deriv_gaussian`: the recursive polynomial definition is equivalent to the
+  definition as the polynomial factor occurring in the `n`-th derivative of a gaussian.
 
 ## References
 
@@ -124,5 +129,57 @@ begin
 end
 
 end coeff
+end polynomial
+
+/-! ### Lemmas about `polynomial.hermite_gauss` -/
+
+section gaussian
+
+/-- The real Gaussian function -/
+def gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2))
+
+lemma inv_gaussian_eq : gaussian⁻¹ = λ x, real.exp (x^2 / 2) :=
+by { ext, simp [gaussian, real.exp_neg] }
+
+lemma inv_gaussian_mul_gaussian (x : ℝ) : gaussian⁻¹ x * gaussian x = 1 :=
+inv_mul_cancel (real.exp_pos _).ne.symm
+
+lemma deriv_gaussian (x : ℝ) : deriv gaussian x = -x * gaussian x :=
+by simp [gaussian, mul_comm]
+
+lemma deriv_inv_gaussian (x : ℝ) : deriv gaussian⁻¹ x = x * gaussian⁻¹ x :=
+by simp [inv_gaussian_eq, mul_comm]
+
+lemma cont_diff_gaussian : cont_diff ℝ ⊤ gaussian :=
+((cont_diff_id.pow 2).div_const 2).neg.exp
+
+namespace polynomial
+
+lemma hermite_gauss_succ (n : ℕ) :
+(λ x, (-1)^(n+1) * (gaussian⁻¹ x) * (deriv^[n+1] gaussian x))
+= id * (λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x)) -
+  deriv (λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x)) :=
+begin
+  ext,
+  simp only [function.iterate_succ', function.comp_app,
+             id.def, pi.mul_apply, pi.sub_apply, pow_succ],
+  rw [deriv_mul, deriv_const_mul, deriv_inv_gaussian],
+  ring,
+  { simp [inv_gaussian_eq] },
+  { simp [inv_gaussian_eq] },
+  { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterate_deriv _ _ cont_diff_gaussian)).1 }
+end
+
+lemma hermite_eq_deriv_gaussian (n : ℕ) (x : ℝ) :
+  aeval x (hermite n) = (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
+begin
+  apply function.funext_iff.mp _ x,
+  induction n with n ih,
+  { simp [-pi.inv_apply, inv_gaussian_mul_gaussian] },
+  { rw [hermite_gauss_succ, hermite_succ, ← ih],
+    ext,
+    simp [aeval_def, eval₂_eq_eval_map] },
+end
 
 end polynomial
+end gaussian