[GOAL]
n : ℕ
x : ℝ
⊢ deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * ↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
n : ℕ
x : ℝ
⊢ deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
induction' n with n ih generalizing x
[GOAL]
case zero
x✝ x : ℝ
⊢ deriv^[Nat.zero] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ Nat.zero * (↑(aeval x) (hermite Nat.zero) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
rw [Function.iterate_zero_apply, pow_zero, one_mul, hermite_zero, C_1, map_one, one_mul]
[GOAL]
case succ
x✝ : ℝ
n : ℕ
ih :
  ∀ (x : ℝ),
    deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x = (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
x : ℝ
⊢ deriv^[Nat.succ n] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ Nat.succ n * (↑(aeval x) (hermite (Nat.succ n)) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
replace ih : deriv^[n] _ = _ := _root_.funext ih
[GOAL]
case succ
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ deriv^[Nat.succ n] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ Nat.succ n * (↑(aeval x) (hermite (Nat.succ n)) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
have deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2)) := by
  rw [deriv_exp (by simp)]; simp;
  ring
    -- Porting note: was `simp [mul_comm, ← neg_mul]`
[GOAL]
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
rw [deriv_exp (by simp)]
[GOAL]
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ DifferentiableAt ℝ (fun y => -(y ^ 2 / 2)) x
[PROOFSTEP]
simp
[GOAL]
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ Real.exp (-(x ^ 2 / 2)) * deriv (fun y => -(y ^ 2 / 2)) x = -x * Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
simp
[GOAL]
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ Real.exp (-(x ^ 2 / 2)) * (2 * x / 2) = x * Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
ring
  -- Porting note: was `simp [mul_comm, ← neg_mul]`
[GOAL]
case succ
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ deriv^[Nat.succ n] (fun y => Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ Nat.succ n * (↑(aeval x) (hermite (Nat.succ n)) * Real.exp (-(x ^ 2 / 2)))
[PROOFSTEP]
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]
[GOAL]
case succ
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ (-1) ^ n *
      (↑(aeval x) (↑derivative (hermite n)) * Real.exp (-(x ^ 2 / 2)) +
        ↑(aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    -1 * (-1) ^ n * ((x * ↑(aeval x) (hermite n) - ↑(aeval x) (↑derivative (hermite n))) * Real.exp (-(x ^ 2 / 2)))
case succ.hc
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => ↑(aeval x) (hermite n)) x
case succ.hd
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => Real.exp (-(x ^ 2 / 2))) x
[PROOFSTEP]
ring
[GOAL]
case succ.hc
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => ↑(aeval x) (hermite n)) x
[PROOFSTEP]
apply Polynomial.differentiable_aeval
[GOAL]
case succ.hd
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => Real.exp (-(x ^ 2 / 2))) x
[PROOFSTEP]
apply DifferentiableAt.exp
[GOAL]
case succ.hd.hc
x✝ : ℝ
n : ℕ
x : ℝ
ih :
  (deriv^[n] fun y => Real.exp (-(y ^ 2 / 2))) = fun x => (-1) ^ n * (↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x => -(x ^ 2 / 2)) x
[PROOFSTEP]
simp
  -- Porting note: was just `simp`
[GOAL]
n : ℕ
x : ℝ
⊢ ↑(aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
rw [deriv_gaussian_eq_hermite_mul_gaussian]
[GOAL]
n : ℕ
x : ℝ
⊢ ↑(aeval x) (hermite n) =
    (-1) ^ n * ((-1) ^ n * ↑(aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))) / Real.exp (-(x ^ 2 / 2))
[PROOFSTEP]
field_simp [Real.exp_ne_zero]
[GOAL]
n : ℕ
x : ℝ
⊢ ↑(aeval x) (hermite n) * Real.exp (-x ^ 2 / 2) =
    (-1) ^ n * ((-1) ^ n * ↑(aeval x) (hermite n) * Real.exp (-x ^ 2 / 2))
[PROOFSTEP]
rw [← @smul_eq_mul ℝ _ ((-1) ^ n), ← inv_smul_eq_iff₀, mul_assoc, smul_eq_mul, ← inv_pow, ← neg_inv, inv_one]
[GOAL]
case ha
n : ℕ
x : ℝ
⊢ (-1) ^ n ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ (by norm_num)
[GOAL]
n : ℕ
x : ℝ
⊢ -1 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
x : ℝ
⊢ ↑(aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)
[PROOFSTEP]
rw [hermite_eq_deriv_gaussian, Real.exp_neg]
[GOAL]
n : ℕ
x : ℝ
⊢ (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / (Real.exp (x ^ 2 / 2))⁻¹ =
    (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x * Real.exp (x ^ 2 / 2)
[PROOFSTEP]
field_simp [Real.exp_ne_zero]
