From c18d6fc2c3bc932e0f9ee10a521b873aa08a6c18 Mon Sep 17 00:00:00 2001
From: lukemantle <lukeomantle@gmail.com>
Date: Fri, 28 Apr 2023 10:23:34 -0700
Subject: [PATCH 01/29] feat(ring_theory/polynomial): show gaussian form of
 `hermite n`

---
 src/ring_theory/polynomial/hermite.lean | 65 +++++++++++++++++++++++++
 1 file changed, 65 insertions(+)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 92699c9b6594f..39659a9d31dd6 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/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
@@ -125,4 +127,67 @@ end
 
 end coeff
 
+/-! ### Lemmas about `polynomial.hermite_gauss` -/
+
+section gauss
+
+abbreviation gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2))
+
+abbreviation inv_gaussian : ℝ → ℝ := λ x, real.exp (x^2 / 2)
+
+lemma inv_gaussian_mul_gaussian (x : ℝ) : inv_gaussian x * gaussian x = 1 :=
+by rw [← real.exp_add, add_neg_self, real.exp_zero]
+
+lemma deriv_gaussian (x : ℝ) : deriv gaussian x = -x * gaussian x :=
+by simp [mul_comm]
+
+lemma deriv_inv_gaussian (x : ℝ) : deriv inv_gaussian x = x * inv_gaussian x :=
+by simp [mul_comm]
+
+lemma cont_diff_gaussian : cont_diff ℝ ⊤ gaussian :=
+((cont_diff_id.pow 2).div_const 2).neg.exp
+
+lemma cont_diff.iterated_deriv :
+∀ (n : ℕ) (f : ℝ → ℝ) (hf : cont_diff ℝ ⊤ f), cont_diff ℝ ⊤ (deriv^[n] f)
+| 0     f hf := hf
+| (n+1) f hf := cont_diff.iterated_deriv n (deriv f) (cont_diff_top_iff_deriv.mp hf).2
+
+
+def hermite_exp (n : ℕ) : ℝ → ℝ :=
+λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x)
+
+lemma hermite_exp_def (n : ℕ) :
+hermite_exp n = λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) := rfl
+
+lemma hermite_exp_succ (n : ℕ) : hermite_exp (n+1)
+= id * (hermite_exp n) - deriv (hermite_exp n):=
+begin
+  ext,
+  simp only [hermite_exp, 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 },
+  { simp },
+  { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterated_deriv _ _ cont_diff_gaussian)).1 }
+end
+
+lemma hermite_eq_exp (n : ℕ) :
+(λ x, eval x (map (algebra_map ℤ ℝ) (hermite n))) =
+λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) :=
+begin
+  induction n with n ih,
+  { simp [inv_gaussian_mul_gaussian] },
+  { rw [← hermite_exp_def, hermite_exp_succ, hermite_succ, hermite_exp_def, ← ih],
+    ext,
+    simp },
+end
+
+lemma hermite_eq_exp_apply :
+  ∀ (n : ℕ) (x : ℝ), eval x (map (algebra_map ℤ ℝ) (hermite n)) =
+    (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) :=
+λ n x, congr_fun (hermite_eq_exp n) x
+
+end gauss
+
 end polynomial

From 01395137522b81aec2d76534517a472f00e7a803 Mon Sep 17 00:00:00 2001
From: lukemantle <lukeomantle@gmail.com>
Date: Fri, 28 Apr 2023 10:37:57 -0700
Subject: [PATCH 02/29] modify docstring, rename lemmas

---
 src/ring_theory/polynomial/hermite.lean | 31 ++++++++++++++-----------
 1 file changed, 18 insertions(+), 13 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 39659a9d31dd6..511ec37a8a169 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -18,12 +18,18 @@ 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 ℤ`
+* `polynomial.hermite_gauss n`: the `n`th probabilist's Hermite polynomial,
+  defined as a real function involving the `n`th derivative of a gaussian
+  function. The `n`th derivative uses `nat.iterate`.
 
 ## 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_gauss`: the recursive polynomial definition is equivalent to the
+  definition involving gaussian functions. That is, for all `n` and `x`,
+  `(hermite n).eval x = hermite_gauss n x`
 
 ## References
 
@@ -129,7 +135,7 @@ end coeff
 
 /-! ### Lemmas about `polynomial.hermite_gauss` -/
 
-section gauss
+section gaussian
 
 abbreviation gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2))
 
@@ -152,18 +158,17 @@ lemma cont_diff.iterated_deriv :
 | 0     f hf := hf
 | (n+1) f hf := cont_diff.iterated_deriv n (deriv f) (cont_diff_top_iff_deriv.mp hf).2
 
-
-def hermite_exp (n : ℕ) : ℝ → ℝ :=
+def hermite_gauss (n : ℕ) : ℝ → ℝ :=
 λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x)
 
-lemma hermite_exp_def (n : ℕ) :
-hermite_exp n = λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) := rfl
+lemma hermite_gauss_def (n : ℕ) :
+hermite_gauss n = λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) := rfl
 
-lemma hermite_exp_succ (n : ℕ) : hermite_exp (n+1)
-= id * (hermite_exp n) - deriv (hermite_exp n):=
+lemma hermite_gauss_succ (n : ℕ) : hermite_gauss (n+1)
+= id * (hermite_gauss n) - deriv (hermite_gauss n):=
 begin
   ext,
-  simp only [hermite_exp, function.iterate_succ', function.comp_app,
+  simp only [hermite_gauss, 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,
@@ -172,22 +177,22 @@ begin
   { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterated_deriv _ _ cont_diff_gaussian)).1 }
 end
 
-lemma hermite_eq_exp (n : ℕ) :
+lemma hermite_eq_gauss (n : ℕ) :
 (λ x, eval x (map (algebra_map ℤ ℝ) (hermite n))) =
 λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) :=
 begin
   induction n with n ih,
   { simp [inv_gaussian_mul_gaussian] },
-  { rw [← hermite_exp_def, hermite_exp_succ, hermite_succ, hermite_exp_def, ← ih],
+  { rw [← hermite_gauss_def, hermite_gauss_succ, hermite_succ, hermite_gauss_def, ← ih],
     ext,
     simp },
 end
 
-lemma hermite_eq_exp_apply :
+lemma hermite_eq_gauss_apply :
   ∀ (n : ℕ) (x : ℝ), eval x (map (algebra_map ℤ ℝ) (hermite n)) =
     (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) :=
-λ n x, congr_fun (hermite_eq_exp n) x
+λ n x, congr_fun (hermite_eq_gauss n) x
 
-end gauss
+end gaussian
 
 end polynomial

From 3eb686ba907849d3ff837b48d43639b110cfa92c Mon Sep 17 00:00:00 2001
From: lukemantle <lukeomantle@gmail.com>
Date: Fri, 28 Apr 2023 11:06:55 -0700
Subject: [PATCH 03/29] remove inv_gaussian, modify docstring

---
 src/ring_theory/polynomial/hermite.lean | 48 ++++++++++++++-----------
 1 file changed, 27 insertions(+), 21 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 511ec37a8a169..f334209f320fd 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -18,9 +18,7 @@ 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 ℤ`
-* `polynomial.hermite_gauss n`: the `n`th probabilist's Hermite polynomial,
-  defined as a real function involving the `n`th derivative of a gaussian
-  function. The `n`th derivative uses `nat.iterate`.
+* `gaussian`: the real Gaussian function
 
 ## Results
 
@@ -28,8 +26,13 @@ This file defines `polynomial.hermite n`, the nth probabilist's Hermite polynomi
   zero.
 * `polynomial.monic_hermite`: for all `n`, `hermite n` is monic.
 * `polynomial.hermite_eq_gauss`: the recursive polynomial definition is equivalent to the
-  definition involving gaussian functions. That is, for all `n` and `x`,
-  `(hermite n).eval x = hermite_gauss n x`
+  definition of the Hermite polynomial as the polynomial factor occurring in the `n`-th derivative
+  of a gaussian. That is, for all `n` and `x`,
+
+## Implementation details
+
+We proceed by defining an auxiliary function `polynomial.hermite_gauss n` directly in terms of the `n`th derivative of a gaussian function. We show that it satisfies the same recurrence relation as the polynomial definition of `hermite n`, and hence that the two definitions are equivalent. This
+definition is not intended to be used outside of this file.
 
 ## References
 
@@ -132,23 +135,25 @@ begin
 end
 
 end coeff
+end polynomial
 
 /-! ### Lemmas about `polynomial.hermite_gauss` -/
 
 section gaussian
 
-abbreviation gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2))
+def gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2))
 
-abbreviation inv_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 : ℝ) : inv_gaussian x * gaussian x = 1 :=
-by rw [← real.exp_add, add_neg_self, real.exp_zero]
+lemma inv_gaussian_mul_gaussian (x : ℝ) : gaussian⁻¹ x * gaussian x = 1 :=
+by rw [inv_gaussian_eq, gaussian, ← real.exp_add, add_neg_self, real.exp_zero]
 
 lemma deriv_gaussian (x : ℝ) : deriv gaussian x = -x * gaussian x :=
-by simp [mul_comm]
+by simp [gaussian, mul_comm]
 
-lemma deriv_inv_gaussian (x : ℝ) : deriv inv_gaussian x = x * inv_gaussian x :=
-by simp [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
@@ -159,10 +164,10 @@ lemma cont_diff.iterated_deriv :
 | (n+1) f hf := cont_diff.iterated_deriv n (deriv f) (cont_diff_top_iff_deriv.mp hf).2
 
 def hermite_gauss (n : ℕ) : ℝ → ℝ :=
-λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x)
+λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x)
 
 lemma hermite_gauss_def (n : ℕ) :
-hermite_gauss n = λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) := rfl
+hermite_gauss n = λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) := rfl
 
 lemma hermite_gauss_succ (n : ℕ) : hermite_gauss (n+1)
 = id * (hermite_gauss n) - deriv (hermite_gauss n):=
@@ -172,17 +177,19 @@ begin
              id.def, pi.mul_apply, pi.sub_apply, pow_succ],
   rw [deriv_mul, deriv_const_mul, deriv_inv_gaussian],
   ring,
-  { simp },
-  { simp },
+  { simp [inv_gaussian_eq] },
+  { simp [inv_gaussian_eq] },
   { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterated_deriv _ _ cont_diff_gaussian)).1 }
 end
 
+namespace polynomial
+
 lemma hermite_eq_gauss (n : ℕ) :
 (λ x, eval x (map (algebra_map ℤ ℝ) (hermite n))) =
-λ x, (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) :=
+λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
 begin
   induction n with n ih,
-  { simp [inv_gaussian_mul_gaussian] },
+  { simp [-pi.inv_apply, inv_gaussian_mul_gaussian] },
   { rw [← hermite_gauss_def, hermite_gauss_succ, hermite_succ, hermite_gauss_def, ← ih],
     ext,
     simp },
@@ -190,9 +197,8 @@ end
 
 lemma hermite_eq_gauss_apply :
   ∀ (n : ℕ) (x : ℝ), eval x (map (algebra_map ℤ ℝ) (hermite n)) =
-    (-1)^n * (inv_gaussian x) * (deriv^[n] gaussian x) :=
+    (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
 λ n x, congr_fun (hermite_eq_gauss n) x
 
-end gaussian
-
 end polynomial
+end gaussian

From e3c4d85a56816f3945d5cf43d992987a985de865 Mon Sep 17 00:00:00 2001
From: lukemantle <lukeomantle@gmail.com>
Date: Fri, 28 Apr 2023 11:10:55 -0700
Subject: [PATCH 04/29] add docstrings to definitions

---
 src/ring_theory/polynomial/hermite.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index f334209f320fd..03b440ac51d2b 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -141,6 +141,7 @@ end polynomial
 
 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) :=
@@ -163,6 +164,7 @@ lemma cont_diff.iterated_deriv :
 | 0     f hf := hf
 | (n+1) f hf := cont_diff.iterated_deriv n (deriv f) (cont_diff_top_iff_deriv.mp hf).2
 
+/-- The Gaussian form of `hermite n` -/
 def hermite_gauss (n : ℕ) : ℝ → ℝ :=
 λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x)
 

From 44763e4d632a69fb3d6139ac0dc7cd77e7f0be0b Mon Sep 17 00:00:00 2001
From: lukemantle <lukeomantle@gmail.com>
Date: Fri, 28 Apr 2023 11:11:32 -0700
Subject: [PATCH 05/29] split oversized line

---
 src/ring_theory/polynomial/hermite.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 03b440ac51d2b..9b05278a280a9 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -31,7 +31,9 @@ This file defines `polynomial.hermite n`, the nth probabilist's Hermite polynomi
 
 ## Implementation details
 
-We proceed by defining an auxiliary function `polynomial.hermite_gauss n` directly in terms of the `n`th derivative of a gaussian function. We show that it satisfies the same recurrence relation as the polynomial definition of `hermite n`, and hence that the two definitions are equivalent. This
+We proceed by defining an auxiliary function `polynomial.hermite_gauss n` directly in terms of the
+`n`th derivative of a gaussian function. We show that it satisfies the same recurrence relation as
+the polynomial definition of `hermite n`, and hence that the two definitions are equivalent. This
 definition is not intended to be used outside of this file.
 
 ## References

From 9d6e6eccce654adc233fe18840e5e1aa144c6d68 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Sat, 29 Apr 2023 12:19:50 -0700
Subject: [PATCH 06/29] move cont_diff.iterate_deriv to cont_diff.lean, correct
 proof of inv_gaussian_mul_gaussian, remove hermite_gauss def, change eval to
 aeval

---
 src/analysis/calculus/cont_diff.lean    |  5 +++
 src/ring_theory/polynomial/hermite.lean | 50 +++++++++----------------
 2 files changed, 22 insertions(+), 33 deletions(-)

diff --git a/src/analysis/calculus/cont_diff.lean b/src/analysis/calculus/cont_diff.lean
index 45b377d3401ec..d70b3c5ad5e7b 100644
--- a/src/analysis/calculus/cont_diff.lean
+++ b/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
diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 9b05278a280a9..89e51617df00f 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -25,16 +25,8 @@ This file defines `polynomial.hermite n`, the nth probabilist's Hermite polynomi
 * `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_gauss`: the recursive polynomial definition is equivalent to the
-  definition of the Hermite polynomial as the polynomial factor occurring in the `n`-th derivative
-  of a gaussian. That is, for all `n` and `x`,
-
-## Implementation details
-
-We proceed by defining an auxiliary function `polynomial.hermite_gauss n` directly in terms of the
-`n`th derivative of a gaussian function. We show that it satisfies the same recurrence relation as
-the polynomial definition of `hermite n`, and hence that the two definitions are equivalent. This
-definition is not intended to be used outside of this file.
+* `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
 
@@ -150,7 +142,7 @@ 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 :=
-by rw [inv_gaussian_eq, gaussian, ← real.exp_add, add_neg_self, real.exp_zero]
+inv_mul_cancel (real.exp_pos _).ne.symm
 
 lemma deriv_gaussian (x : ℝ) : deriv gaussian x = -x * gaussian x :=
 by simp [gaussian, mul_comm]
@@ -161,48 +153,40 @@ by simp [inv_gaussian_eq, mul_comm]
 lemma cont_diff_gaussian : cont_diff ℝ ⊤ gaussian :=
 ((cont_diff_id.pow 2).div_const 2).neg.exp
 
-lemma cont_diff.iterated_deriv :
-∀ (n : ℕ) (f : ℝ → ℝ) (hf : cont_diff ℝ ⊤ f), cont_diff ℝ ⊤ (deriv^[n] f)
-| 0     f hf := hf
-| (n+1) f hf := cont_diff.iterated_deriv n (deriv f) (cont_diff_top_iff_deriv.mp hf).2
-
-/-- The Gaussian form of `hermite n` -/
-def hermite_gauss (n : ℕ) : ℝ → ℝ :=
-λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x)
-
-lemma hermite_gauss_def (n : ℕ) :
-hermite_gauss n = λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) := rfl
-
-lemma hermite_gauss_succ (n : ℕ) : hermite_gauss (n+1)
-= id * (hermite_gauss n) - deriv (hermite_gauss n):=
+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 [hermite_gauss, function.iterate_succ', function.comp_app,
+  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.iterated_deriv _ _ cont_diff_gaussian)).1 }
+  { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterate_deriv _ _ cont_diff_gaussian)).1 }
 end
 
 namespace polynomial
 
-lemma hermite_eq_gauss (n : ℕ) :
-(λ x, eval x (map (algebra_map ℤ ℝ) (hermite n))) =
+lemma hermite_eq_deriv_gaussian (n : ℕ) :
+(λ (x : ℝ), aeval x (hermite n)) =
 λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
 begin
+  convert_to (λ x, eval x (map (algebra_map ℤ ℝ) (hermite n))) = _,
+  simp [aeval_def, eval, eval₂_map],
   induction n with n ih,
   { simp [-pi.inv_apply, inv_gaussian_mul_gaussian] },
-  { rw [← hermite_gauss_def, hermite_gauss_succ, hermite_succ, hermite_gauss_def, ← ih],
+  { rw [hermite_gauss_succ, hermite_succ, ← ih],
     ext,
     simp },
 end
 
-lemma hermite_eq_gauss_apply :
-  ∀ (n : ℕ) (x : ℝ), eval x (map (algebra_map ℤ ℝ) (hermite n)) =
+lemma hermite_eq_deriv_gaussian_apply :
+  ∀ (n : ℕ) (x : ℝ), aeval x (hermite n) =
     (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
-λ n x, congr_fun (hermite_eq_gauss n) x
+λ n x, congr_fun (hermite_eq_deriv_gaussian n) x
 
 end polynomial
 end gaussian

From 930aead5468f818dd78ac0c6edc900b3d6867045 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Sat, 29 Apr 2023 12:29:03 -0700
Subject: [PATCH 07/29] fix proof using aeval rw lemma

---
 src/ring_theory/polynomial/hermite.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 89e51617df00f..683f736e40a7f 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -174,13 +174,11 @@ lemma hermite_eq_deriv_gaussian (n : ℕ) :
 (λ (x : ℝ), aeval x (hermite n)) =
 λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
 begin
-  convert_to (λ x, eval x (map (algebra_map ℤ ℝ) (hermite n))) = _,
-  simp [aeval_def, eval, eval₂_map],
   induction n with n ih,
   { simp [-pi.inv_apply, inv_gaussian_mul_gaussian] },
   { rw [hermite_gauss_succ, hermite_succ, ← ih],
     ext,
-    simp },
+    simp [aeval_def, eval₂_eq_eval_map] },
 end
 
 lemma hermite_eq_deriv_gaussian_apply :

From 1ae19cfcb46ed300cc6bf7a29397438fde785af1 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Sat, 29 Apr 2023 12:42:14 -0700
Subject: [PATCH 08/29] remove separate equality of lambdas

---
 src/ring_theory/polynomial/hermite.lean | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 683f736e40a7f..41b3cc9f7d5f8 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -153,6 +153,8 @@ 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)) -
@@ -168,12 +170,10 @@ begin
   { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterate_deriv _ _ cont_diff_gaussian)).1 }
 end
 
-namespace polynomial
-
-lemma hermite_eq_deriv_gaussian (n : ℕ) :
-(λ (x : ℝ), aeval x (hermite n)) =
-λ x, (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
+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],
@@ -181,10 +181,5 @@ begin
     simp [aeval_def, eval₂_eq_eval_map] },
 end
 
-lemma hermite_eq_deriv_gaussian_apply :
-  ∀ (n : ℕ) (x : ℝ), aeval x (hermite n) =
-    (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
-λ n x, congr_fun (hermite_eq_deriv_gaussian n) x
-
 end polynomial
 end gaussian

From 22a9add50c2cf5e4108f4891894d671408899ded Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Sun, 30 Apr 2023 13:28:12 -0700
Subject: [PATCH 09/29] remove gaussian definition, simplify all proofs

---
 src/ring_theory/polynomial/hermite.lean | 65 +++++++++----------------
 1 file changed, 22 insertions(+), 43 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 41b3cc9f7d5f8..eb936c368d88b 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -129,57 +129,36 @@ begin
 end
 
 end coeff
-end polynomial
-
-/-! ### Lemmas about `polynomial.hermite_gauss` -/
 
+/-! ### Lemmas about `hermite n` and gaussians -/
 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)) :=
+lemma hermite_gauss_succ (n : ℕ) (x : ℝ) :
+(-1 : ℝ)^(n+1) * real.exp (x^2 / 2) * (deriv^[n+1] (λ y, real.exp (-(y^2 / 2))) x)
+= x * ((-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) -
+  deriv (λ x, (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) 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 }
+             id.def, pi.mul_apply, pi.sub_apply],
+  rw [deriv_mul, deriv_const_mul,
+      (by simp [mul_comm] : deriv (λ y, real.exp (y^2 / 2)) x = x * real.exp (x^2 / 2))],
+  ring_exp,
+  { simp },
+  { simp },
+  { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterate_deriv _ _ _)).1,
+    exact ((cont_diff_id.pow 2).div_const 2).neg.exp },
 end
 
-lemma hermite_eq_deriv_gaussian (n : ℕ) (x : ℝ) :
-  aeval x (hermite n) = (-1)^n * (gaussian⁻¹ x) * (deriv^[n] gaussian x) :=
+/- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a gaussian -/
+lemma hermite_eq_deriv_gaussian : ∀ (n) (x),
+aeval x (hermite n) = (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)
+| 0       _ := by simp [← real.exp_add]
+| (n + 1) _ :=
 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] },
+  simp_rw [hermite_gauss_succ, hermite_succ, ← hermite_eq_deriv_gaussian],
+  simp [aeval_def, eval₂_eq_eval_map],
 end
 
-end polynomial
 end gaussian
+
+end polynomial

From 9fb7f4c5b06f220269820f71ac6765f6e214cd32 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Sun, 30 Apr 2023 13:29:01 -0700
Subject: [PATCH 10/29] add finite-level version of cont_diff.iterate_deriv

---
 src/analysis/calculus/cont_diff.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/analysis/calculus/cont_diff.lean b/src/analysis/calculus/cont_diff.lean
index d70b3c5ad5e7b..66e3e0762230c 100644
--- a/src/analysis/calculus/cont_diff.lean
+++ b/src/analysis/calculus/cont_diff.lean
@@ -2298,8 +2298,13 @@ lemma cont_diff.continuous_deriv (h : cont_diff 𝕜 n f₂) (hn : 1 ≤ n) :
 
 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
+| 0       f₂ hf := hf
+| (n + 1) f₂ hf := cont_diff.iterate_deriv n (deriv f₂) (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
 

From 257a8f0fcdf7e55cae07b59204a09cd6cedcaf38 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Sun, 30 Apr 2023 13:32:14 -0700
Subject: [PATCH 11/29] correct docstring

---
 src/ring_theory/polynomial/hermite.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index eb936c368d88b..8710a63eaf9ae 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -18,7 +18,6 @@ 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
 
@@ -26,7 +25,7 @@ This file defines `polynomial.hermite n`, the nth probabilist's Hermite polynomi
   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.
+  definition as (up to sign) the polynomial factor occurring in the `n`th derivative of a gaussian.
 
 ## References
 

From ed9218547e27c421236330e6c0c55982059c0ce1 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 30 Apr 2023 21:09:03 +0000
Subject: [PATCH 12/29] golf and format

---
 src/ring_theory/polynomial/hermite.lean | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 8710a63eaf9ae..e95d55d49c827 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -133,13 +133,11 @@ end coeff
 section gaussian
 
 lemma hermite_gauss_succ (n : ℕ) (x : ℝ) :
-(-1 : ℝ)^(n+1) * real.exp (x^2 / 2) * (deriv^[n+1] (λ y, real.exp (-(y^2 / 2))) x)
-= x * ((-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) -
-  deriv (λ x, (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) x :=
+  (-1 : ℝ)^(n+1) * real.exp (x^2 / 2) * (deriv^[n+1] (λ y, real.exp (-(y^2 / 2))) x)
+  = x * ((-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) -
+    deriv (λ x, (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) x :=
 begin
-  simp only [function.iterate_succ', function.comp_app,
-             id.def, pi.mul_apply, pi.sub_apply],
-  rw [deriv_mul, deriv_const_mul,
+  rw [function.iterate_succ_apply', deriv_mul, deriv_const_mul,
       (by simp [mul_comm] : deriv (λ y, real.exp (y^2 / 2)) x = x * real.exp (x^2 / 2))],
   ring_exp,
   { simp },
@@ -149,11 +147,10 @@ begin
 end
 
 /- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a gaussian -/
-lemma hermite_eq_deriv_gaussian : ∀ (n) (x),
-aeval x (hermite n) = (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)
-| 0       _ := by simp [← real.exp_add]
-| (n + 1) _ :=
-begin
+lemma hermite_eq_deriv_gaussian : ∀ (x : ℝ) (n : ℕ),
+  aeval x (hermite n) = (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)
+| _ 0       := by simp [← real.exp_add]
+| _ (n + 1) := begin
   simp_rw [hermite_gauss_succ, hermite_succ, ← hermite_eq_deriv_gaussian],
   simp [aeval_def, eval₂_eq_eval_map],
 end

From 0248c18b878046a535719e94c6d62ee66f64f3cc Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Sun, 30 Apr 2023 15:49:17 -0700
Subject: [PATCH 13/29] inline proof of recurrence

---
 src/ring_theory/polynomial/hermite.lean | 32 ++++++++++++-------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index e95d55d49c827..9c06658f37df5 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -132,29 +132,29 @@ end coeff
 /-! ### Lemmas about `hermite n` and gaussians -/
 section gaussian
 
-lemma hermite_gauss_succ (n : ℕ) (x : ℝ) :
-  (-1 : ℝ)^(n+1) * real.exp (x^2 / 2) * (deriv^[n+1] (λ y, real.exp (-(y^2 / 2))) x)
-  = x * ((-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) -
-    deriv (λ x, (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) x :=
-begin
-  rw [function.iterate_succ_apply', deriv_mul, deriv_const_mul,
-      (by simp [mul_comm] : deriv (λ y, real.exp (y^2 / 2)) x = x * real.exp (x^2 / 2))],
-  ring_exp,
-  { simp },
-  { simp },
-  { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterate_deriv _ _ _)).1,
-    exact ((cont_diff_id.pow 2).div_const 2).neg.exp },
-end
-
 /- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a gaussian -/
 lemma hermite_eq_deriv_gaussian : ∀ (x : ℝ) (n : ℕ),
   aeval x (hermite n) = (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)
 | _ 0       := by simp [← real.exp_add]
-| _ (n + 1) := begin
-  simp_rw [hermite_gauss_succ, hermite_succ, ← hermite_eq_deriv_gaussian],
+| _ (_ + 1) :=
+begin
+  have : ∀ n x,
+    (-1 : ℝ)^(n+1) * real.exp (x^2 / 2) * (deriv^[n+1] (λ y, real.exp (-(y^2 / 2))) x)
+    = x * ((-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) -
+      deriv (λ x, (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) x,
+  { intros n x,
+    rw [function.iterate_succ_apply', deriv_mul, deriv_const_mul,
+        (by simp [mul_comm] : deriv (λ y, real.exp (y^2 / 2)) x = x * real.exp (x^2 / 2))],
+    ring_exp,
+    { simp },
+    { simp },
+    { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterate_deriv _ _ _)).1,
+      exact ((cont_diff_id.pow 2).div_const 2).neg.exp } },
+  simp_rw [this, hermite_succ, ← hermite_eq_deriv_gaussian],
   simp [aeval_def, eval₂_eq_eval_map],
 end
 
 end gaussian
 
 end polynomial
+-- ⁻¹

From 04fafe53678166fb6855f93384b4b050bc1ebff3 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Mon, 1 May 2023 20:29:13 -0700
Subject: [PATCH 14/29] modified proof to use division

---
 src/analysis/calculus/cont_diff.lean    |  8 ++---
 src/ring_theory/polynomial/hermite.lean | 42 ++++++++++++++-----------
 2 files changed, 27 insertions(+), 23 deletions(-)

diff --git a/src/analysis/calculus/cont_diff.lean b/src/analysis/calculus/cont_diff.lean
index 66e3e0762230c..ec4f3351c2548 100644
--- a/src/analysis/calculus/cont_diff.lean
+++ b/src/analysis/calculus/cont_diff.lean
@@ -2297,14 +2297,14 @@ lemma cont_diff.continuous_deriv (h : cont_diff 𝕜 n f₂) (hn : 1 ≤ n) :
 (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₂)
+∀ (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
+| (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₂)
+∀ (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
+| (n + 1) f₂ hf := cont_diff.iterate_deriv' n (cont_diff_succ_iff_deriv.mp hf).2
 
 end deriv
 
diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 9c06658f37df5..a4847dc8e55b8 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -133,28 +133,32 @@ end coeff
 section gaussian
 
 /- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a gaussian -/
-lemma hermite_eq_deriv_gaussian : ∀ (x : ℝ) (n : ℕ),
-  aeval x (hermite n) = (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)
-| _ 0       := by simp [← real.exp_add]
-| _ (_ + 1) :=
+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
-  have : ∀ n x,
-    (-1 : ℝ)^(n+1) * real.exp (x^2 / 2) * (deriv^[n+1] (λ y, real.exp (-(y^2 / 2))) x)
-    = x * ((-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) -
-      deriv (λ x, (-1 : ℝ)^n * real.exp (x^2 / 2) * (deriv^[n] (λ y, real.exp (-(y^2 / 2))) x)) x,
-  { intros n x,
-    rw [function.iterate_succ_apply', deriv_mul, deriv_const_mul,
-        (by simp [mul_comm] : deriv (λ y, real.exp (y^2 / 2)) x = x * real.exp (x^2 / 2))],
-    ring_exp,
-    { simp },
-    { simp },
-    { apply (cont_diff_top_iff_deriv.mp (cont_diff.iterate_deriv _ _ _)).1,
-      exact ((cont_diff_id.pow 2).div_const 2).neg.exp } },
-  simp_rw [this, hermite_succ, ← hermite_eq_deriv_gaussian],
-  simp [aeval_def, eval₂_eq_eval_map],
+  induction n with n ih generalizing x,
+  { simp [← real.exp_sub] },
+  { let gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2)),
+    have gaussian_ne_zero : ∀ x, gaussian x ≠ 0 := by simp [gaussian, real.exp_ne_zero],
+    have cont_diff_gaussian : cont_diff ℝ ⊤ gaussian := ((cont_diff_id.pow 2).div_const 2).neg.exp,
+    have : ∀ x n,
+      (-1 : ℝ)^(n+1) * (deriv^[n+1] gaussian x) / gaussian x
+      = x * ((-1 : ℝ)^n * (deriv^[n] gaussian x)) / gaussian x -
+        deriv (λ z, (-1 : ℝ)^n * (deriv^[n] gaussian z) / gaussian z) x,
+    { intros x n,
+      rw [function.iterate_succ_apply', deriv_div _ _ (gaussian_ne_zero _), deriv_const_mul,
+          (by simp [gaussian, mul_comm] : deriv gaussian x = (-x) * gaussian x)],
+      field_simp [gaussian_ne_zero],
+      ring_exp,
+      { apply (cont_diff_top_iff_deriv.mp (cont_diff_gaussian.iterate_deriv _)).1, },
+      { apply (cont_diff_top_iff_deriv.mp _).1,
+        exact (cont_diff_gaussian.iterate_deriv _).const_smul ((-1 : ℝ)^n) },
+      { simp } },
+    simp_rw [this, hermite_succ, ← mul_div x, ← ih],
+    simp [aeval_def, eval₂_eq_eval_map] }
 end
 
 end gaussian
 
 end polynomial
--- ⁻¹

From ac5025ad8f2468179e33daefa7369ef2351dbba5 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Mon, 1 May 2023 20:32:34 -0700
Subject: [PATCH 15/29] correct typo

---
 src/ring_theory/polynomial/hermite.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index a4847dc8e55b8..42c3a389899bf 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -133,7 +133,7 @@ end coeff
 section gaussian
 
 /- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a gaussian -/
-lemma hermite_eq_deriv_gaussian' (n : ℕ) (x : ℝ) :
+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

From 5ab5fb969b632268bc9359091c824535ed2f8c80 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Thu, 4 May 2023 16:46:50 -0700
Subject: [PATCH 16/29] modify docstring

---
 src/ring_theory/polynomial/hermite.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 42c3a389899bf..4d9d2d8e67452 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -21,11 +21,12 @@ 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.hermite_eq_deriv_gaussian`: the Hermite polynomial is (up to sign) the polynomial
+factor occurring in the `n`th derivative of a gaussian.
 * `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 (up to sign) the polynomial factor occurring in the `n`th derivative of a gaussian.
 
 ## References
 
@@ -38,7 +39,7 @@ open polynomial
 
 namespace polynomial
 
-/-- the nth probabilist's Hermite polynomial -/
+/-- the nth probabilist's Hermite polynomial H_(n+1) = (x - d/dx) H_n -/
 noncomputable def hermite : ℕ → polynomial ℤ
 | 0     := 1
 | (n+1) := X * (hermite n) - (hermite n).derivative

From 086953e80abe5309fc5a9e4937cceb56c0240b78 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Thu, 4 May 2023 17:13:28 -0700
Subject: [PATCH 17/29] add polynomial.deriv_aeval

---
 src/analysis/calculus/deriv.lean        | 5 +++++
 src/ring_theory/polynomial/hermite.lean | 5 ++---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/analysis/calculus/deriv.lean b/src/analysis/calculus/deriv.lean
index d3f5f5e96cce2..2043c0835d735 100644
--- a/src/analysis/calculus/deriv.lean
+++ b/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
diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite.lean
index 4d9d2d8e67452..ab0428b1ab207 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite.lean
@@ -145,7 +145,7 @@ begin
     have cont_diff_gaussian : cont_diff ℝ ⊤ gaussian := ((cont_diff_id.pow 2).div_const 2).neg.exp,
     have : ∀ x n,
       (-1 : ℝ)^(n+1) * (deriv^[n+1] gaussian x) / gaussian x
-      = x * ((-1 : ℝ)^n * (deriv^[n] gaussian x)) / gaussian x -
+      = x * ((-1 : ℝ)^n * (deriv^[n] gaussian x) / gaussian x) -
         deriv (λ z, (-1 : ℝ)^n * (deriv^[n] gaussian z) / gaussian z) x,
     { intros x n,
       rw [function.iterate_succ_apply', deriv_div _ _ (gaussian_ne_zero _), deriv_const_mul,
@@ -156,8 +156,7 @@ begin
       { apply (cont_diff_top_iff_deriv.mp _).1,
         exact (cont_diff_gaussian.iterate_deriv _).const_smul ((-1 : ℝ)^n) },
       { simp } },
-    simp_rw [this, hermite_succ, ← mul_div x, ← ih],
-    simp [aeval_def, eval₂_eq_eval_map] }
+    simp_rw [this, hermite_succ, ← ih, polynomial.deriv_aeval, map_sub, map_mul, aeval_X] }
 end
 
 end gaussian

From 07044aa8e632b3af4307ebe6c51b8d7e5d902b11 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Thu, 4 May 2023 17:21:15 -0700
Subject: [PATCH 18/29] move PR to ring_theory/polynomial/hermite/

---
 .../{hermite.lean => hermite/basic.lean}      | 35 -----------
 .../polynomial/hermite/gaussian.lean          | 59 +++++++++++++++++++
 2 files changed, 59 insertions(+), 35 deletions(-)
 rename src/ring_theory/polynomial/{hermite.lean => hermite/basic.lean} (69%)
 create mode 100644 src/ring_theory/polynomial/hermite/gaussian.lean

diff --git a/src/ring_theory/polynomial/hermite.lean b/src/ring_theory/polynomial/hermite/basic.lean
similarity index 69%
rename from src/ring_theory/polynomial/hermite.lean
rename to src/ring_theory/polynomial/hermite/basic.lean
index ab0428b1ab207..84c1160d6fcaf 100644
--- a/src/ring_theory/polynomial/hermite.lean
+++ b/src/ring_theory/polynomial/hermite/basic.lean
@@ -6,8 +6,6 @@ Authors: Luke Mantle
 
 import data.polynomial.derivative
 import data.nat.parity
-import analysis.special_functions.exp
-import analysis.special_functions.exp_deriv
 
 /-!
 # Hermite polynomials
@@ -22,8 +20,6 @@ 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.hermite_eq_deriv_gaussian`: the Hermite polynomial is (up to sign) the polynomial
-factor occurring in the `n`th derivative of a gaussian.
 * `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.
@@ -130,35 +126,4 @@ end
 
 end coeff
 
-/-! ### Lemmas about `hermite n` and gaussians -/
-section gaussian
-
-/- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a gaussian -/
-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
-  induction n with n ih generalizing x,
-  { simp [← real.exp_sub] },
-  { let gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2)),
-    have gaussian_ne_zero : ∀ x, gaussian x ≠ 0 := by simp [gaussian, real.exp_ne_zero],
-    have cont_diff_gaussian : cont_diff ℝ ⊤ gaussian := ((cont_diff_id.pow 2).div_const 2).neg.exp,
-    have : ∀ x n,
-      (-1 : ℝ)^(n+1) * (deriv^[n+1] gaussian x) / gaussian x
-      = x * ((-1 : ℝ)^n * (deriv^[n] gaussian x) / gaussian x) -
-        deriv (λ z, (-1 : ℝ)^n * (deriv^[n] gaussian z) / gaussian z) x,
-    { intros x n,
-      rw [function.iterate_succ_apply', deriv_div _ _ (gaussian_ne_zero _), deriv_const_mul,
-          (by simp [gaussian, mul_comm] : deriv gaussian x = (-x) * gaussian x)],
-      field_simp [gaussian_ne_zero],
-      ring_exp,
-      { apply (cont_diff_top_iff_deriv.mp (cont_diff_gaussian.iterate_deriv _)).1, },
-      { apply (cont_diff_top_iff_deriv.mp _).1,
-        exact (cont_diff_gaussian.iterate_deriv _).const_smul ((-1 : ℝ)^n) },
-      { simp } },
-    simp_rw [this, hermite_succ, ← ih, polynomial.deriv_aeval, map_sub, map_mul, aeval_X] }
-end
-
-end gaussian
-
 end polynomial
diff --git a/src/ring_theory/polynomial/hermite/gaussian.lean b/src/ring_theory/polynomial/hermite/gaussian.lean
new file mode 100644
index 0000000000000..4792a1c159d0d
--- /dev/null
+++ b/src/ring_theory/polynomial/hermite/gaussian.lean
@@ -0,0 +1,59 @@
+/-
+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.hermite_eq_deriv_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 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
+  induction n with n ih generalizing x,
+  { simp [← real.exp_sub] },
+  { let gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2)),
+    have gaussian_ne_zero : ∀ x, gaussian x ≠ 0 := by simp [gaussian, real.exp_ne_zero],
+    have cont_diff_gaussian : cont_diff ℝ ⊤ gaussian := ((cont_diff_id.pow 2).div_const 2).neg.exp,
+    have : ∀ x n,
+      (-1 : ℝ)^(n+1) * (deriv^[n+1] gaussian x) / gaussian x
+      = x * ((-1 : ℝ)^n * (deriv^[n] gaussian x) / gaussian x) -
+        deriv (λ z, (-1 : ℝ)^n * (deriv^[n] gaussian z) / gaussian z) x,
+    { intros x n,
+      rw [function.iterate_succ_apply', deriv_div _ _ (gaussian_ne_zero _), deriv_const_mul,
+          (by simp [gaussian, mul_comm] : deriv gaussian x = (-x) * gaussian x)],
+      field_simp [gaussian_ne_zero],
+      ring_exp,
+      { apply (cont_diff_top_iff_deriv.mp (cont_diff_gaussian.iterate_deriv _)).1, },
+      { apply (cont_diff_top_iff_deriv.mp _).1,
+        exact (cont_diff_gaussian.iterate_deriv _).const_smul ((-1 : ℝ)^n) },
+      { simp } },
+    simp_rw [this, hermite_succ, ← ih, polynomial.deriv_aeval, map_sub, map_mul, aeval_X] }
+end
+
+end polynomial

From e19873794c8ace0cbd3f13607350a396aa51fd86 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Thu, 4 May 2023 17:25:18 -0700
Subject: [PATCH 19/29] modify docstring

---
 src/ring_theory/polynomial/hermite/basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ring_theory/polynomial/hermite/basic.lean b/src/ring_theory/polynomial/hermite/basic.lean
index 84c1160d6fcaf..4a6d951db090c 100644
--- a/src/ring_theory/polynomial/hermite/basic.lean
+++ b/src/ring_theory/polynomial/hermite/basic.lean
@@ -35,11 +35,12 @@ open polynomial
 
 namespace polynomial
 
-/-- the nth probabilist's Hermite polynomial H_(n+1) = (x - d/dx) H_n -/
+/-- the nth probabilist's Hermite polynomial -/
 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
 

From c2e742f8c81c5e03495746b213e50ed39ea97278 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Thu, 4 May 2023 23:58:09 -0700
Subject: [PATCH 20/29] added variant lemma statements

---
 .../polynomial/hermite/gaussian.lean          | 57 ++++++++++++-------
 1 file changed, 36 insertions(+), 21 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite/gaussian.lean b/src/ring_theory/polynomial/hermite/gaussian.lean
index 4792a1c159d0d..daa6ca7ce220a 100644
--- a/src/ring_theory/polynomial/hermite/gaussian.lean
+++ b/src/ring_theory/polynomial/hermite/gaussian.lean
@@ -16,8 +16,9 @@ polynomial factor occurring in the `n`th derivative of a gaussian.
 
 ## Results
 
-* `polynomial.hermite_eq_deriv_gaussian`: the Hermite polynomial is (up to sign) the polynomial
-factor occurring in the `n`th derivative of a gaussian.
+* `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
 
@@ -31,29 +32,43 @@ 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,
+  { by simp },
+  { replace ih : (deriv^[n] _) = _ := function.funext_iff.mpr ih,
+    have deriv_gaussian : deriv (λ y, real.exp (-(y^2 / 2))) x = (-x) * real.exp (-(x^2 / 2)) :=
+      by 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
-  induction n with n ih generalizing x,
-  { simp [← real.exp_sub] },
-  { let gaussian : ℝ → ℝ := λ x, real.exp (-(x^2 / 2)),
-    have gaussian_ne_zero : ∀ x, gaussian x ≠ 0 := by simp [gaussian, real.exp_ne_zero],
-    have cont_diff_gaussian : cont_diff ℝ ⊤ gaussian := ((cont_diff_id.pow 2).div_const 2).neg.exp,
-    have : ∀ x n,
-      (-1 : ℝ)^(n+1) * (deriv^[n+1] gaussian x) / gaussian x
-      = x * ((-1 : ℝ)^n * (deriv^[n] gaussian x) / gaussian x) -
-        deriv (λ z, (-1 : ℝ)^n * (deriv^[n] gaussian z) / gaussian z) x,
-    { intros x n,
-      rw [function.iterate_succ_apply', deriv_div _ _ (gaussian_ne_zero _), deriv_const_mul,
-          (by simp [gaussian, mul_comm] : deriv gaussian x = (-x) * gaussian x)],
-      field_simp [gaussian_ne_zero],
-      ring_exp,
-      { apply (cont_diff_top_iff_deriv.mp (cont_diff_gaussian.iterate_deriv _)).1, },
-      { apply (cont_diff_top_iff_deriv.mp _).1,
-        exact (cont_diff_gaussian.iterate_deriv _).const_smul ((-1 : ℝ)^n) },
-      { simp } },
-    simp_rw [this, hermite_succ, ← ih, polynomial.deriv_aeval, map_sub, map_mul, aeval_X] }
+  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

From 3a28d9a155b7998a3820039baa80f3ae12f83f67 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Fri, 5 May 2023 08:17:42 +0000
Subject: [PATCH 21/29] Update src/ring_theory/polynomial/hermite/gaussian.lean

---
 src/ring_theory/polynomial/hermite/gaussian.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite/gaussian.lean b/src/ring_theory/polynomial/hermite/gaussian.lean
index daa6ca7ce220a..fb3d0845acbb1 100644
--- a/src/ring_theory/polynomial/hermite/gaussian.lean
+++ b/src/ring_theory/polynomial/hermite/gaussian.lean
@@ -33,8 +33,8 @@ 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)) :=
+  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,
   { by simp },

From 549d5d25095d9e2c323ba053ebc7fa94360a1e1e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 5 May 2023 09:28:22 +0100
Subject: [PATCH 22/29] Update src/ring_theory/polynomial/hermite/gaussian.lean

---
 src/ring_theory/polynomial/hermite/gaussian.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ring_theory/polynomial/hermite/gaussian.lean b/src/ring_theory/polynomial/hermite/gaussian.lean
index fb3d0845acbb1..9afaa8b3dae4c 100644
--- a/src/ring_theory/polynomial/hermite/gaussian.lean
+++ b/src/ring_theory/polynomial/hermite/gaussian.lean
@@ -31,7 +31,7 @@ open polynomial
 
 namespace polynomial
 
-/- `hermite n` is (up to sign) the factor appearing in `deriv^[n]` of a gaussian -/
+/-- `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)) :=

From 150bf4684a26c41bc7f7f0155bf83beef33c589e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 5 May 2023 09:25:56 +0000
Subject: [PATCH 23/29] fix style, squeeze a slow simp

---
 src/ring_theory/polynomial/hermite/gaussian.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite/gaussian.lean b/src/ring_theory/polynomial/hermite/gaussian.lean
index 9afaa8b3dae4c..f0f24943a8342 100644
--- a/src/ring_theory/polynomial/hermite/gaussian.lean
+++ b/src/ring_theory/polynomial/hermite/gaussian.lean
@@ -37,10 +37,10 @@ lemma deriv_gaussian_eq_hermite_mul_gaussian (n : ℕ) (x : ℝ) :
   (-1 : ℝ)^n * aeval x (hermite n) * real.exp (-(x^2 / 2)) :=
 begin
   induction n with n ih generalizing x,
-  { by simp },
-  { replace ih : (deriv^[n] _) = _ := function.funext_iff.mpr ih,
-    have deriv_gaussian : deriv (λ y, real.exp (-(y^2 / 2))) x = (-x) * real.exp (-(x^2 / 2)) :=
-      by simp [mul_comm, ← neg_mul],
+  { 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,

From a7b25eb87afb4e9d5ccacc9666fd3f714f44df33 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 5 May 2023 10:38:01 +0100
Subject: [PATCH 24/29] Update src/analysis/calculus/deriv.lean

---
 src/analysis/calculus/deriv.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analysis/calculus/deriv.lean b/src/analysis/calculus/deriv.lean
index 2043c0835d735..ab2fcd6e790b1 100644
--- a/src/analysis/calculus/deriv.lean
+++ b/src/analysis/calculus/deriv.lean
@@ -1882,7 +1882,7 @@ p.differentiable.differentiable_on
 (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) :=
+  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) :

From f3a41d2e3c519d6ead3320cfc222f302642d1a31 Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Fri, 5 May 2023 10:00:33 -0700
Subject: [PATCH 25/29] avoid side goal

---
 src/ring_theory/polynomial/hermite/gaussian.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite/gaussian.lean b/src/ring_theory/polynomial/hermite/gaussian.lean
index daa6ca7ce220a..0b3336b716ebd 100644
--- a/src/ring_theory/polynomial/hermite/gaussian.lean
+++ b/src/ring_theory/polynomial/hermite/gaussian.lean
@@ -36,19 +36,17 @@ 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
+  rw mul_assoc,
   induction n with n ih generalizing x,
   { by simp },
   { replace ih : (deriv^[n] _) = _ := function.funext_iff.mpr ih,
     have deriv_gaussian : deriv (λ y, real.exp (-(y^2 / 2))) x = (-x) * real.exp (-(x^2 / 2)) :=
       by simp [mul_comm, ← neg_mul],
-    rw [function.iterate_succ_apply', ih, deriv_mul, deriv_const_mul, pow_succ (-1 : ℝ),
+    rw [function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_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
 

From bdde5114ef7413e324b950a85bd28baee60b4da6 Mon Sep 17 00:00:00 2001
From: jakelev <levinson.jake@gmail.com>
Date: Fri, 5 May 2023 11:04:59 -0700
Subject: [PATCH 26/29] Apply suggestions from code review

---
 src/analysis/calculus/cont_diff.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analysis/calculus/cont_diff.lean b/src/analysis/calculus/cont_diff.lean
index ec4f3351c2548..2a8cced40e013 100644
--- a/src/analysis/calculus/cont_diff.lean
+++ b/src/analysis/calculus/cont_diff.lean
@@ -2297,12 +2297,12 @@ lemma cont_diff.continuous_deriv (h : cont_diff 𝕜 n f₂) (hn : 1 ≤ n) :
 (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₂)
+  ∀ (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₂)
+  ∀ (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
 

From b6c1adc20b13d9783b1a6747b764a6f7c95ff153 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 11 May 2023 20:32:48 +0100
Subject: [PATCH 27/29] Delete duplicate import from bad merge

---
 src/analysis/calculus/deriv.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/analysis/calculus/deriv.lean b/src/analysis/calculus/deriv.lean
index 30e3c0a6c2c43..20327a2f4cc7b 100644
--- a/src/analysis/calculus/deriv.lean
+++ b/src/analysis/calculus/deriv.lean
@@ -6,7 +6,6 @@ Authors: Gabriel Ebner, Sébastien Gouëzel
 import analysis.calculus.fderiv
 import data.polynomial.algebra_map
 import data.polynomial.derivative
-import data.polynomial.algebra_map
 import linear_algebra.affine_space.slope
 
 /-!

From a39abab8722b55e08195e6b91031edb93c5bbc35 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 11 May 2023 19:47:23 +0000
Subject: [PATCH 28/29] use the new lemma in the proof

---
 src/ring_theory/polynomial/hermite/gaussian.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/ring_theory/polynomial/hermite/gaussian.lean b/src/ring_theory/polynomial/hermite/gaussian.lean
index 4d1c57cf89ffc..4c42aa338feac 100644
--- a/src/ring_theory/polynomial/hermite/gaussian.lean
+++ b/src/ring_theory/polynomial/hermite/gaussian.lean
@@ -45,8 +45,7 @@ begin
     rw [function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_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 },
+    { exact polynomial.differentiable_aeval },
     { simp } }
 end
 

From 8c65b7391fcb1a40804f60bb5c55649dd1ddf36d Mon Sep 17 00:00:00 2001
From: Jake Levinson <levinson.jake@gmail.com>
Date: Thu, 11 May 2023 21:58:36 -0700
Subject: [PATCH 29/29] correct failing proof

---
 src/ring_theory/polynomial/hermite/gaussian.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ring_theory/polynomial/hermite/gaussian.lean b/src/ring_theory/polynomial/hermite/gaussian.lean
index 4c42aa338feac..0dc26ea76c07f 100644
--- a/src/ring_theory/polynomial/hermite/gaussian.lean
+++ b/src/ring_theory/polynomial/hermite/gaussian.lean
@@ -45,7 +45,7 @@ begin
     rw [function.iterate_succ_apply', ih, deriv_const_mul_field, deriv_mul, pow_succ (-1 : ℝ),
         deriv_gaussian, hermite_succ, map_sub, map_mul, aeval_X, polynomial.deriv_aeval],
     ring,
-    { exact polynomial.differentiable_aeval },
+    { apply polynomial.differentiable_aeval },
     { simp } }
 end