Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges, Tomas Skrivan, Joseph Tooby-Smith
-/
module
public import Mathlib.Analysis.Calculus.Deriv.Polynomial
public import Mathlib.Analysis.Calculus.ContDiff.Polynomial
public import Mathlib.Analysis.Distribution.TemperateGrowth
public import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
public import Mathlib.Tactic.Cases
public import Mathlib.Topology.Algebra.PolynomialPhysicist's Hermite Polynomials
This file may eventually be upstreamed to Mathlib.
i. Overview
The physicist's Hermite polynomials are a family of orthogonal polynomials defined by the recursion
$H_0(x) = 1$ and $H_{n+1}(x) = 2x,H_n(x) - H_n'(x)$.
These are a rescaling of the so-called probabalist's Hermite polynomials (Polynomial.hermite)
and, up to numerical factors, satisfy all of the same properties.
ii. Key results
iii. Table of contents
A. Recursive definition
B. Coefficients & degree
C. Iterated derivatives
D. As functions ℝ → ℝ
D.1. Recursion
D.2. Parity
D.3. Differentiability
D.4. Temperate growth
E. Relationship to Gaussians
iv. References
@[expose] public sectionA. Recursive definition
The defining recursion physHermite (n + 1) = (2x - d/dx) (physHermite n).
lemma 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! 🐙
The Rodrigues formula physHermite n = (2x - d/dx)ⁿ 1.
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 := rfl@[simp]
lemma 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! 🐙B. Coefficients & degree
lemma coeff_physHermite_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)@[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! 🐙)C. Iterated derivatives
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! 🐙)All goals completed! 🐙
D. As functions ℝ → ℝ
Cast an integer polynomial to a function ℝ → ℝ by evaluation of the indeterminant.
@[coe]
noncomputable abbrev realEval (p : Polynomial ℤ) : ℝ → ℝ := fun x ↦ p.aeval xD.1. Recursion
lemma physHermite_zero_coe : (physHermite 0 : ℝ → ℝ) = fun _ ↦ 1 := ⊢ ↑(physHermite 0) = fun x => 1 x✝:ℝ⊢ ↑(physHermite 0) x✝ = 1; All goals completed! 🐙
The defining recursion for physHermite as functions ℝ → ℝ (c.f. physHermite_succ).
lemma physHermite_succ_coe (n : ℕ) :
(physHermite (n + 1) : ℝ → ℝ) =
2 • (fun x => x) * (physHermite n : ℝ → ℝ) - deriv (physHermite n) := n:ℕ⊢ ↑(physHermite (n + 1)) = (2 • fun x => x) * ↑(physHermite n) - deriv ↑(physHermite n)
n:ℕx✝:ℝ⊢ ↑(physHermite (n + 1)) x✝ = ((2 • fun x => x) * ↑(physHermite n) - deriv ↑(physHermite n)) x✝
All goals completed! 🐙lemma physHermite_succ_apply (n : ℕ) (x : ℝ) :
physHermite (n + 1) x = 2 * x * physHermite n x - deriv (physHermite n) x := n:ℕx:ℝ⊢ ↑(physHermite (n + 1)) x = 2 * x * ↑(physHermite n) x - deriv (↑(physHermite n)) x
All goals completed! 🐙
The two-term recursion for physHermite as functions ℝ → ℝ (c.f. physHermite_succ').
lemma physHermite_succ_coe' (n : ℕ) :
(physHermite (n + 1) : ℝ → ℝ) =
2 • (fun x => x) * (physHermite n : ℝ → ℝ) - (2 * n) • (physHermite (n - 1) : ℝ → ℝ) := n:ℕ⊢ ↑(physHermite (n + 1)) = (2 • fun x => x) * ↑(physHermite n) - (2 * n) • ↑(physHermite (n - 1))
n:ℕx✝:ℝ⊢ ↑(physHermite (n + 1)) x✝ = ((2 • fun x => x) * ↑(physHermite n) - (2 * n) • ↑(physHermite (n - 1))) x✝
All goals completed! 🐙lemma physHermite_succ_apply' (n : ℕ) (x : ℝ) :
physHermite (n + 1) x = 2 * x * physHermite n x - 2 * n * physHermite (n - 1) x := n:ℕx:ℝ⊢ ↑(physHermite (n + 1)) x = 2 * x * ↑(physHermite n) x - 2 * ↑n * ↑(physHermite (n - 1)) x
All goals completed! 🐙lemma deriv_physHermite (n : ℕ) : deriv (physHermite n) = 2 * n * physHermite (n - 1) := n:ℕ⊢ deriv ↑(physHermite n) = 2 * ↑n * ↑(physHermite (n - 1))
n:ℕx✝:ℝ⊢ deriv (↑(physHermite n)) x✝ = (2 * ↑n * ↑(physHermite (n - 1))) x✝
All goals completed! 🐙lemma iterate_deriv_physHermite_eq_iterate_derivative (n m : ℕ) :
deriv^[m] (physHermite n) = derivative^[m] (physHermite n) := n:ℕm:ℕ⊢ deriv^[m] ↑(physHermite n) = ↑((⇑derivative)^[m] (physHermite n))
match m with
n:ℕm:ℕ⊢ deriv^[0] ↑(physHermite n) = ↑((⇑derivative)^[0] (physHermite n)) All goals completed! 🐙
n:ℕm✝:ℕm:ℕ⊢ deriv^[m + 1] ↑(physHermite n) = ↑((⇑derivative)^[m + 1] (physHermite n))
n:ℕm✝:ℕm:ℕx✝:ℝ⊢ deriv^[m + 1] (↑(physHermite n)) x✝ = ↑((⇑derivative)^[m + 1] (physHermite n)) x✝
All goals completed! 🐙lemma fderiv_physHermite (n : ℕ) (x : ℝ) :
fderiv ℝ (physHermite n) x = (1 : ℝ →L[ℝ] ℝ).smulRight (deriv (physHermite n) x) := n:ℕx:ℝ⊢ fderiv ℝ (↑(physHermite n)) x = ContinuousLinearMap.smulRight 1 (deriv (↑(physHermite n)) x)
All goals completed! 🐙D.2. Parity
The physHermite polynomials are alternately even and odd.
@[simp]
lemma physHermite_neg (n : ℕ) (x : ℝ) : physHermite n (-x) = (-1) ^ n * physHermite n x := n:ℕx:ℝ⊢ ↑(physHermite n) (-x) = (-1) ^ n * ↑(physHermite n) x
match n with
n:ℕx:ℝ⊢ ↑(physHermite 0) (-x) = (-1) ^ 0 * ↑(physHermite 0) x All goals completed! 🐙
n:ℕx:ℝ⊢ ↑(physHermite 1) (-x) = (-1) ^ 1 * ↑(physHermite 1) x All goals completed! 🐙
n✝:ℕx:ℝn:ℕ⊢ ↑(physHermite (n + 2)) (-x) = (-1) ^ (n + 2) * ↑(physHermite (n + 2)) x All goals completed! 🐙lemma physHermite_even {n : ℕ} (hn : Even n) : Function.Even (physHermite n) := n:ℕhn:Even n⊢ Function.Even ↑(physHermite n) n:ℕhn:Even na✝:ℝ⊢ ↑(physHermite n) (-a✝) = ↑(physHermite n) a✝; All goals completed! 🐙lemma physHermite_odd {n : ℕ} (hn : Odd n) : Function.Odd (physHermite n) := n:ℕhn:Odd n⊢ Function.Odd ↑(physHermite n) n:ℕhn:Odd na✝:ℝ⊢ ↑(physHermite n) (-a✝) = -↑(physHermite n) a✝; All goals completed! 🐙D.3. Differentiability
@[fun_prop]
lemma physHermite_differentiable (n : ℕ) : Differentiable ℝ (physHermite n) :=
Polynomial.differentiable_aeval _@[fun_prop]
lemma deriv_physHermite_differentiable (n m : ℕ) : Differentiable ℝ (deriv^[m] (physHermite n)) :=
iterate_deriv_physHermite_eq_iterate_derivative n m ▸ Polynomial.differentiable_aeval _@[fun_prop]
lemma physHermite_continuous (n : ℕ) : Continuous (physHermite n) := Polynomial.continuous_aeval _@[fun_prop]
lemma physHermite_contDiff (n : ℕ) (m : WithTop ℕ∞) : ContDiff ℝ m (physHermite n) :=
Polynomial.contDiff_aeval _ _D.4. Temperate growth
E. Relationship to Gaussians
n:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * (↑(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 (↑(physHermite n)) x * Real.exp (-x ^ 2) + ↑(physHermite n) x * (-2 * x * Real.exp (-x ^ 2))) =
(-1) ^ n * -1 * (↑(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 * (↑(physHermite n) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ DifferentiableAt ℝ (↑(physHermite n)) xn:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * (↑(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 * (↑(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 (↑(physHermite n)) x * Real.exp (-x ^ 2) + ↑(physHermite n) x * (-2 * x * Real.exp (-x ^ 2))) =
(-1) ^ n * -1 * (↑(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 * (↑(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) +
↑(physHermite n) x * (-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 * (↑(physHermite n) x * Real.exp (-x ^ 2))deriv_gaussian:deriv (fun y => Real.exp (-y ^ 2)) x = -2 * x * Real.exp (-x ^ 2)⊢ DifferentiableAt ℝ (↑(physHermite n)) x All goals completed! 🐙
n:ℕx:ℝih:(deriv^[n] fun y => Real.exp (-y ^ 2)) = fun x => (-1) ^ n * (↑(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:ℝ⊢ ↑(physHermite n) x = (-1) ^ n * ((-1) ^ n * ↑(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] ↑(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] ↑(physHermite p) * deriv^[n] fun x => Real.exp (-x ^ 2)) MeasureTheory.volume
All goals completed! 🐙n:ℕm:ℕh1:∀ (x : ℝ),
↑(physHermite n) x * ↑(physHermite m) x * Real.exp (-x ^ 2) =
(-1) ^ m * (↑(physHermite n) x * deriv^[m] (fun x => Real.exp (-x ^ 2)) x)⊢ ∫ (x : ℝ), ↑(physHermite n) x * ↑(physHermite m) x * Real.exp (-x ^ 2) =
(-1) ^ m * ∫ (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] (↑(physHermite n)) x * deriv (deriv^[m - (p + 1)] fun x => Real.exp (-x ^ 2)) x =
-∫ (x : ℝ), deriv (deriv^[p] ↑(physHermite n)) x * deriv^[m - (p + 1)] (fun x => Real.exp (-x ^ 2)) x⊢ -1 * ∫ (x : ℝ), deriv^[p] (↑(physHermite n)) x * deriv (deriv^[m - (p + 1)] fun x => Real.exp (-x ^ 2)) x =
∫ (x : ℝ), deriv (deriv^[p] ↑(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 : ℝ), ↑(physHermite n) x * ↑(physHermite m) x * Real.exp (-x ^ 2) =
∫ (x : ℝ), deriv^[m] (↑(physHermite n)) x * Real.exp (-x ^ 2)
All goals completed! 🐙n:ℕm:ℕhnm:n < m⊢ ∫ (x : ℝ), deriv^[m] (↑(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 : ℝ), ↑(physHermite n) x * ↑(physHermite m) x * Real.exp (-x ^ 2) = 0
n:ℕm:ℕhnm:n ≠ mh:n < m⊢ ∫ (x : ℝ), ↑(physHermite n) x * ↑(physHermite m) x * Real.exp (-x ^ 2) = 0n:ℕm:ℕhnm:n ≠ mh:m < n⊢ ∫ (x : ℝ), ↑(physHermite n) x * ↑(physHermite m) x * Real.exp (-x ^ 2) = 0
n:ℕm:ℕhnm:n ≠ mh:n < m⊢ ∫ (x : ℝ), ↑(physHermite n) x * ↑(physHermite m) x * Real.exp (-x ^ 2) = 0 All goals completed! 🐙
n:ℕm:ℕhnm:n ≠ mh:m < n⊢ ∫ (x : ℝ), ↑(physHermite n) x * ↑(physHermite m) x * Real.exp (-x ^ 2) = 0 All goals completed! 🐙n:ℕm:ℕhnm:n ≠ mc:ℝh:∫ (x : ℝ), ↑(physHermite n) (c * x) * ↑(physHermite m) (c * x) * Real.exp (-(c * x) ^ 2) = 0⊢ ∫ (x : ℝ), ↑(physHermite n) (c * x) * ↑(physHermite m) (c * x) * Real.exp (-c ^ 2 * x ^ 2) = 0
All goals completed! 🐙n:ℕ⊢ ∫ (x : ℝ), ↑((⇑derivative)^[n] (physHermite n)) x * Real.exp (-x ^ 2) = ↑n ! * 2 ^ n * √Real.pi
All goals completed! 🐙n:ℕc:ℝh:∫ (x : ℝ), ↑(physHermite n) (c * x) * ↑(physHermite n) (c * x) * Real.exp (-(c * x) ^ 2) =
|c⁻¹| • (↑n ! * 2 ^ n * √Real.pi)⊢ ∫ (x : ℝ), ↑(physHermite n) (c * 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✝¹⟩ →
↑y.1 ∈ Submodule.span ℝ (Set.range fun n => ↑(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⟩⟩ →
↑y.1 ∈ Submodule.span ℝ (Set.range fun n => ↑(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⟩⟩ →
↑y.1 ∈ Submodule.span ℝ (Set.range fun n => ↑(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✝¹⟩ →
↑y.1 ∈ Submodule.span ℝ (Set.range fun n => ↑(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⟩⟩ →
↑y.1 ∈ Submodule.span ℝ (Set.range fun n => ↑(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⟩⟩ →
↑y.1 ∈ Submodule.span ℝ (Set.range fun n => ↑(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 => ↑(physHermite n))⊢ (fun x => Real.cos (c * x)) ∈ (Submodule.span ℝ (Set.range fun n => ↑(physHermite n))).topologicalClosure
All goals completed! 🐙