1. Physlib
  2. Mathematics
  3. SpecialFunctions
  4. PhysHermite
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomas Skrivan, Joseph Tooby-Smith -/ module public import Mathlib.Analysis.Calculus.Deriv.Polynomial public import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series public import Mathlib.Tactic.Cases

Physicists Hermite Polynomial

This file may eventually be upstreamed to Mathlib.

@[expose] public sectionlemma physHermite_succ (n : ℕ) : physHermite (n + 1) = 2 • X * physHermite n - derivative (physHermite n) := n:ℕ⊢ physHermite (n + 1) = 2 • X * physHermite n - derivative (physHermite n) All goals completed! 🐙lemma physHermite_eq_iterate (n : ℕ) : physHermite n = (fun p => 2 * X * p - derivative p)^[n] 1 := n:ℕ⊢ physHermite n = (fun p => 2 * X * p - derivative p)^[n] 1 induction n with ⊢ physHermite 0 = (fun p => 2 * X * p - derivative p)^[0] 1 All goals completed! 🐙 n:ℕih:physHermite n = (fun p => 2 * X * p - derivative p)^[n] 1⊢ physHermite (n + 1) = (fun p => 2 * X * p - derivative p)^[n + 1] 1 All goals completed! 🐙@[simp] lemma physHermite_zero : physHermite 0 = C 1 := rfllemma physHermite_one : physHermite 1 = 2 * X := ⊢ physHermite 1 = 2 * X All goals completed! 🐙n:ℕ⊢ derivative (2 • X * physHermite (n + 1) - derivative (physHermite (n + 1))) = 2 * (n + 1 + 1) • physHermite (n + 1) n:ℕ⊢ 2 * physHermite (n + 1) + 2 * X * (2 * ((↑n + 1) * physHermite n)) - 2 * ((↑n + 1) * derivative (physHermite n)) = 2 * ((↑n + 1 + 1) * physHermite (n + 1)) n:ℕ⊢ 2 * (↑2 * X * physHermite n - derivative (physHermite n)) + 2 * X * (2 * ((↑n + 1) * physHermite n)) - 2 * ((↑n + 1) * derivative (physHermite n)) = 2 * ((↑n + 1 + 1) * (↑2 * X * physHermite n - derivative (physHermite n))) All goals completed! 🐙lemma derivative_physHermite : (n : ℕ) → derivative (physHermite n) = 2 * n • physHermite (n - 1) ⊢ derivative (physHermite 0) = 2 * 0 • physHermite (0 - 1) ⊢ derivative (physHermite 0) = 2 * 0 • physHermite (0 - 1) All goals completed! 🐙 n:ℕ⊢ derivative (physHermite (n + 1)) = 2 * (n + 1) • physHermite (n + 1 - 1) n:ℕ⊢ derivative (physHermite (n + 1)) = 2 * (n + 1) • physHermite (n + 1 - 1) All goals completed! 🐙All goals completed! 🐙lemma coeff_physHhermite_succ_zero (n : ℕ) : coeff (physHermite (n + 1)) 0 = - coeff (physHermite n) 1 := n:ℕ⊢ (physHermite (n + 1)).coeff 0 = -(physHermite n).coeff 1 All goals completed! 🐙n:ℕk:ℕ⊢ 2 • (physHermite n).coeff k - (↑(k + 1) + 1) * (physHermite n).coeff (k + 1 + 1) = 2 * (physHermite n).coeff k - (↑k + 2) * (physHermite n).coeff (k + 2) All goals completed! 🐙n:ℕih:∀ (k : ℕ), (physHermite n).coeff (n + k + 1) = 0k:ℕ⊢ 2 * 0 - (↑(n + k + 1) + 2) * 0 = 0 All goals completed! 🐙All goals completed! 🐙@[simp] lemma degree_physHermite (n : ℕ) : degree (physHermite n) = n := n:ℕ⊢ (physHermite n).degree = ↑n refine degree_eq_of_le_of_coeff_ne_zero ?_ (n:ℕ⊢ (physHermite n).coeff n ≠ 0 All goals completed! 🐙) simp_rw n:ℕ⊢ (physHermite n).degree ≤ ↑nn:ℕ⊢ ∀ (m : ℕ), ↑n < ↑m → (physHermite n).coeff m = 0 n:ℕ⊢ ∀ (m : ℕ), n < m → (physHermite n).coeff m = 0] All goals completed! 🐙@[simp] lemma natDegree_physHermite {n : ℕ} : (physHermite n).natDegree = n := natDegree_eq_of_degree_eq_some (degree_physHermite n)lemma iterate_derivative_physHermite_of_gt {n m : ℕ} (h : n < m) : derivative^[m] (physHermite n) = 0 := iterate_derivative_eq_zero (n:ℕm:ℕh:n < m⊢ (physHermite n).natDegree < m All goals completed! 🐙)n:ℕm✝:ℕm:ℕ⊢ (m + 1 + n).descFactorial n • 0 = 0 All goals completed! 🐙@[simp] lemma physHermite_leadingCoeff {n : ℕ} : (physHermite n).leadingCoeff = 2 ^ n := n:ℕ⊢ (physHermite n).leadingCoeff = 2 ^ n All goals completed! 🐙@[simp] lemma physHermite_ne_zero {n : ℕ} : physHermite n ≠ 0 := leadingCoeff_ne_zero.mp (n:ℕ⊢ (physHermite n).leadingCoeff ≠ 0 All goals completed! 🐙)lemma physHermite_eq_aeval (n : ℕ) (x : ℝ) : physHermite n x = (physHermite n).aeval x := rfllemma physHermite_zero_apply (x : ℝ) : physHermite 0 x = 1 := x:ℝ⊢ (fun x => (aeval x) (physHermite 0)) x = 1 All goals completed! 🐙lemma physHermite_pow (n m : ℕ) (x : ℝ) : physHermite n x ^ m = aeval x (physHermite n ^ m) := n:ℕm:ℕx:ℝ⊢ (fun x => (aeval x) (physHermite n)) x ^ m = (aeval x) (physHermite n ^ m) All goals completed! 🐙lemma physHermite_succ_fun (n : ℕ) : (physHermite (n + 1) : ℝ → ℝ) = 2 • (fun x => x) * (physHermite n : ℝ → ℝ)- (2 * n : ℝ) • (physHermite (n - 1) : ℝ → ℝ) := n:ℕ⊢ (fun x => (aeval x) (physHermite (n + 1))) = ((2 • fun x => x) * fun x => (aeval x) (physHermite n)) - (2 * ↑n) • fun x => (aeval x) (physHermite (n - 1)) n:ℕx:ℝ⊢ (aeval x) (physHermite (n + 1)) = (((2 • fun x => x) * fun x => (aeval x) (physHermite n)) - (2 * ↑n) • fun x => (aeval x) (physHermite (n - 1))) x All goals completed! 🐙n:ℕ⊢ (((2 • fun x => x) * fun x => (aeval x) (physHermite n)) - (2 * ↑n) • fun x => (aeval x) (physHermite (n - 1))) = fun x => 2 • x * (fun x => (aeval x) (physHermite n)) x - (2 * ↑n) • (fun x => (aeval x) (physHermite (n - 1))) x All goals completed! 🐙All goals completed! 🐙@[fun_prop] lemma physHermite_differentiableAt (n : ℕ) (x : ℝ) : DifferentiableAt ℝ (physHermite n) x := Polynomial.differentiableAt_aeval (physHermite n)@[fun_prop] lemma deriv_physHermite_differentiableAt (n m : ℕ) (x : ℝ) : DifferentiableAt ℝ (deriv^[m] (physHermite n)) x := iterated_deriv_physHermite_eq_aeval n m ▸ Polynomial.differentiableAt_aeval _n:ℕx:ℝ⊢ (aeval x) (2 * n • physHermite (n - 1)) = (2 * ↑n * fun x => (aeval x) (physHermite (n - 1))) x All goals completed! 🐙E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Ex:Ef:E → ℝhf:DifferentiableAt ℝ f xn:ℕ⊢ fderiv ℝ (fun x => (aeval x) (physHermite n)) (f x) ∘SL fderiv ℝ f x = (2 * ↑n * (fun x => (aeval x) (physHermite (n - 1))) (f x)) • fderiv ℝ f x E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Ex:Ef:E → ℝhf:DifferentiableAt ℝ f xn:ℕdx:E⊢ (fderiv ℝ (fun x => (aeval x) (physHermite n)) (f x) ∘SL fderiv ℝ f x) dx = ((2 * ↑n * (fun x => (aeval x) (physHermite (n - 1))) (f x)) • fderiv ℝ f x) dx E:Type u_1inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ Ex:Ef:E → ℝhf:DifferentiableAt ℝ f xn:ℕdx:E⊢ (fderiv ℝ f x) dx * (2 * (↑n * (aeval (f x)) (physHermite (n - 1)))) = 2 * ↑n * (aeval (f x)) (physHermite (n - 1)) * (fderiv ℝ f x) dx All goals completed! 🐙x:ℝf:ℝ → ℝhf:DifferentiableAt ℝ f xn:ℕ⊢ ((2 * ↑n * (fun x => (aeval x) (physHermite (n - 1))) (f x)) • fderiv ℝ f x) 1 = 2 * ↑n * (fun x => (aeval x) (physHermite (n - 1))) (f x) * (fderiv ℝ f x) 1 All goals completed! 🐙n:ℕx:ℝ⊢ (fun x => 2 • x * (fun x => (aeval x) (physHermite (n + 1))) x - (2 * ↑(n + 1)) • (fun x => (aeval x) (physHermite (n + 1 - 1))) x) (-x) = (-1) ^ (n + 2) * (fun x => 2 • x * (fun x => (aeval x) (physHermite (n + 1))) x - (2 * ↑(n + 1)) • (fun x => (aeval x) (physHermite (n + 1 - 1))) x) x n:ℕx:ℝ⊢ -(2 * x * ((-1) ^ (n + 1) * (aeval x) (physHermite (n + 1)))) - 2 * (↑n + 1) * ((-1) ^ n * (aeval x) (physHermite n)) = (-1) ^ (n + 2) * (2 * x * (aeval x) (physHermite (n + 1)) - 2 * (↑n + 1) * (aeval x) (physHermite n)) All goals completed! 🐙

Relationship to Gaussians

n:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * ((fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ (-1) ^ n * (deriv (fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2) + (aeval x) (physHermite n) * (-2 * x * Real.exp (-x ^ 2))) = (-1) ^ n * -1 * ((fun x => (aeval x) (2 • X * physHermite n - 2 * n • physHermite (n - 1))) x * Real.exp (-x ^ 2))n:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * ((fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ DifferentiableAt ℝ (fun x => (aeval x) (physHermite n)) xn:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * ((fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ DifferentiableAt ℝ (fun x => Real.exp (-x ^ 2)) x n:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * ((fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ (-1) ^ n * (deriv (fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2) + (aeval x) (physHermite n) * (-2 * x * Real.exp (-x ^ 2))) = (-1) ^ n * -1 * ((fun x => (aeval x) (2 • X * physHermite n - 2 * n • physHermite (n - 1))) x * Real.exp (-x ^ 2)) n:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * ((fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ (-1) ^ n * (2 * (↑n * (aeval x) (physHermite (n - 1))) * Real.exp (-x ^ 2) + (aeval x) (physHermite n) * (-2 * x * Real.exp (-x ^ 2))) = (-1) ^ n * -1 * ((↑2 * x * (aeval x) (physHermite n) - 2 * (↑n * (aeval x) (physHermite (n - 1)))) * Real.exp (-x ^ 2)) All goals completed! 🐙 n:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * ((fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ DifferentiableAt ℝ (fun x => (aeval x) (physHermite n)) x All goals completed! 🐙 n:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * ((fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ DifferentiableAt ℝ (fun x => Real.exp (-x ^ 2)) x All goals completed! 🐙n:ℕx:ℝ⊢ (fun x => (aeval x) (physHermite n)) x = (-1) ^ n * ((-1) ^ n * (fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2)) / Real.exp (-x ^ 2) All goals completed! 🐙n:ℕx:ℝ⊢ (-1) ^ n * deriv^[n] (fun y => Real.exp (-y ^ 2)) x / (Real.exp (x ^ 2))⁻¹ = (-1) ^ n * deriv^[n] (fun y => Real.exp (-y ^ 2)) x * Real.exp (x ^ 2) All goals completed! 🐙b:ℝc:ℝhb:0 < bP:ℤ[X]i:ℕx✝:i ∈ Finset.range (P.natDegree + 1)h2:(fun a => P.coeff i • (c * a) ^ i * Real.exp (-b * a ^ 2)) = (c ^ i * ↑(P.coeff i)) • fun x => x ^ ↑i * Real.exp (-b * x ^ 2)⊢ MeasureTheory.Integrable (fun x => P.coeff i • (c * x) ^ i * Real.exp (-b * x ^ 2)) MeasureTheory.volume All goals completed! 🐙@[fun_prop] lemma guassian_integrable_polynomial {b : ℝ} (hb : 0 < b) (P : Polynomial ℤ) : MeasureTheory.Integrable fun x : ℝ => (P.aeval x) * Real.exp (-b * x ^ 2) := b:ℝhb:0 < bP:ℤ[X]⊢ MeasureTheory.Integrable (fun x => (aeval x) P * Real.exp (-b * x ^ 2)) MeasureTheory.volume All goals completed! 🐙n:ℕp:ℕm:ℕprod_eq_smul_aeval_mul_gaussian:((deriv^[m] fun x => (aeval x) (physHermite p)) * deriv^[n] fun x => Real.exp (-x ^ 2)) = (-1) ^ n • fun x => (aeval x) ((⇑derivative)^[m] (physHermite p) * physHermite n) * Real.exp (-1 * x ^ 2)⊢ MeasureTheory.Integrable ((deriv^[m] fun x => (aeval x) (physHermite p)) * deriv^[n] fun x => Real.exp (-x ^ 2)) MeasureTheory.volume All goals completed! 🐙n:ℕm:ℕh1:∀ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * (fun x => (aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = (-1) ^ m * ((fun x => (aeval x) (physHermite n)) x * deriv^[m] (fun x => Real.exp (-x ^ 2)) x)⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * (fun x => (aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = (-1) ^ m * ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * deriv^[m] (fun x => Real.exp (-x ^ 2)) x All goals completed! 🐙n:ℕm:ℕp:ℕh:p + 1 ≤ mhl:∫ (x : ℝ), deriv^[p] (fun x => (aeval x) (physHermite n)) x * deriv (deriv^[m - (p + 1)] fun x => Real.exp (-x ^ 2)) x = -∫ (x : ℝ), deriv (deriv^[p] fun x => (aeval x) (physHermite n)) x * deriv^[m - (p + 1)] (fun x => Real.exp (-x ^ 2)) x⊢ -1 * ∫ (x : ℝ), deriv^[p] (fun x => (aeval x) (physHermite n)) x * deriv (deriv^[m - (p + 1)] fun x => Real.exp (-x ^ 2)) x = ∫ (x : ℝ), deriv (deriv^[p] fun x => (aeval x) (physHermite n)) x * deriv^[m - (p + 1)] (fun x => Real.exp (-x ^ 2)) x All goals completed! 🐙lemma integral_physHermite_mul_physHermite_eq_integral_deriv (n m : ℕ) : ∫ x : ℝ, (physHermite n x * physHermite m x) * Real.exp (- x ^ 2) = ∫ x : ℝ, (deriv^[m] (physHermite n) x * (Real.exp (-x ^ 2))) := n:ℕm:ℕ⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * (fun x => (aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = ∫ (x : ℝ), deriv^[m] (fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2) All goals completed! 🐙n:ℕm:ℕhnm:n < m⊢ ∫ (x : ℝ), deriv^[m] (fun x => (aeval x) (physHermite n)) x * Real.exp (-x ^ 2) = 0 All goals completed! 🐙theorem physHermite_orthogonal {n m : ℕ} (hnm : n ≠ m) : ∫ x : ℝ, (physHermite n x * physHermite m x) * Real.exp (- x ^ 2) = 0 := n:ℕm:ℕhnm:n ≠ m⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * (fun x => (aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = 0 n:ℕm:ℕhnm:n ≠ mh:n < m⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * (fun x => (aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = 0n:ℕm:ℕhnm:n ≠ mh:m < n⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * (fun x => (aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = 0 n:ℕm:ℕhnm:n ≠ mh:n < m⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * (fun x => (aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = 0 All goals completed! 🐙 n:ℕm:ℕhnm:n ≠ mh:m < n⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) x * (fun x => (aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = 0 All goals completed! 🐙n:ℕm:ℕhnm:n ≠ mc:ℝh:∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) (c * x) * (fun x => (aeval x) (physHermite m)) (c * x) * Real.exp (-(c * x) ^ 2) = 0⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) (c * x) * (fun x => (aeval x) (physHermite m)) (c * x) * Real.exp (-c ^ 2 * x ^ 2) = 0 All goals completed! 🐙n:ℕ⊢ ∫ (x : ℝ), (fun x => (aeval x) ((⇑derivative)^[n] (physHermite n))) x * Real.exp (-x ^ 2) = ↑n ! * 2 ^ n * √Real.pi All goals completed! 🐙n:ℕc:ℝh:∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) (c * x) * (fun x => (aeval x) (physHermite n)) (c * x) * Real.exp (-(c * x) ^ 2) = |c⁻¹| • (↑n ! * 2 ^ n * √Real.pi)⊢ ∫ (x : ℝ), (fun x => (aeval x) (physHermite n)) (c * x) * (fun x => (aeval x) (physHermite n)) (c * x) * Real.exp (-c ^ 2 * x ^ 2) = |c⁻¹| • (↑n ! * 2 ^ n * √Real.pi) All goals completed! 🐙P:ℤ[X]n✝¹:(x : ℕ) ×' P.natDegree = xa✝¹:∀ (y : (P : ℤ[X]) ×' (n : ℕ) ×' P.natDegree = n), InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun P n => PSigma.casesOn n fun n hn => n) y ⟨P, n✝¹⟩ → (fun x => (aeval x) y.1) ∈ Submodule.span ℝ (Set.range fun n x => (aeval x) (physHermite n))n✝:ℕhn:P.natDegree = n✝a✝:∀ (y : (P : ℤ[X]) ×' (n : ℕ) ×' P.natDegree = n), InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun P n => PSigma.casesOn n fun n hn => n) y ⟨P, ⟨n✝, hn⟩⟩ → (fun x => (aeval x) y.1) ∈ Submodule.span ℝ (Set.range fun n x => (aeval x) (physHermite n))n:ℕh:P.natDegree = n + 1x✝:∀ (y : (P : ℤ[X]) ×' (n : ℕ) ×' P.natDegree = n), InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun P n => PSigma.casesOn n fun n hn => n) y ⟨P, ⟨n.succ, h⟩⟩ → (fun x => (aeval x) y.1) ∈ Submodule.span ℝ (Set.range fun n x => (aeval x) (physHermite n))hP0:¬P = 0P':ℤ[X] := (physHermite (n + 1)).coeff (n + 1) • P - P.coeff (n + 1) • physHermite (n + 1)hP':¬P' = 0m:ℕhm':n + 1 ≤ mhm:¬m = n + 1⊢ 2 ^ (n + 1) • 0 - P.coeff (n + 1) • 0 = 0 All goals completed! 🐙 P:ℤ[X]n✝¹:(x : ℕ) ×' P.natDegree = xa✝¹:∀ (y : (P : ℤ[X]) ×' (n : ℕ) ×' P.natDegree = n), InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun P n => PSigma.casesOn n fun n hn => n) y ⟨P, n✝¹⟩ → (fun x => (aeval x) y.1) ∈ Submodule.span ℝ (Set.range fun n x => (aeval x) (physHermite n))n✝:ℕhn:P.natDegree = n✝a✝:∀ (y : (P : ℤ[X]) ×' (n : ℕ) ×' P.natDegree = n), InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun P n => PSigma.casesOn n fun n hn => n) y ⟨P, ⟨n✝, hn⟩⟩ → (fun x => (aeval x) y.1) ∈ Submodule.span ℝ (Set.range fun n x => (aeval x) (physHermite n))n:ℕh:P.natDegree = n + 1x✝:∀ (y : (P : ℤ[X]) ×' (n : ℕ) ×' P.natDegree = n), InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun P n => PSigma.casesOn n fun n hn => n) y ⟨P, ⟨n.succ, h⟩⟩ → (fun x => (aeval x) y.1) ∈ Submodule.span ℝ (Set.range fun n x => (aeval x) (physHermite n))hP0:¬P = 0P':ℤ[X] := (physHermite (n + 1)).coeff (n + 1) • P - P.coeff (n + 1) • physHermite (n + 1)hP':¬P' = 0⊢ (physHermite (n + 1)).coeff (n + 1) • P - P.coeff (n + 1) • physHermite (n + 1) ≠ 0 All goals completed! 🐙lemma polynomial_mem_physHermite_span (P : Polynomial ℤ) : (P : ℝ → ℝ) ∈ Submodule.span ℝ (Set.range (fun n => (physHermite n : ℝ → ℝ))) := polynomial_mem_physHermite_span_induction P P.natDegree rflc:ℝh1:Filter.Tendsto (fun s y => ∑ x ∈ s, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) Filter.atTop (nhds fun x => Real.cos (c * x))h2:∀ (z : Finset ℕ), (fun y => ∑ x ∈ z, (-1) ^ x * (c * y) ^ (2 * x) / ↑(2 * x)!) ∈ Submodule.span ℝ (Set.range fun n x => (aeval x) (physHermite n))⊢ (fun x => Real.cos (c * x)) ∈ (Submodule.span ℝ (Set.range fun n x => (aeval x) (physHermite n))).topologicalClosure All goals completed! 🐙