Physicists Hermite Polynomial

This file may eventually be upstreamed to Mathlib.

noncomputable def PhysLean.physHermite : ℕ → Polynomial ℤ

The Physicists Hermite polynomial are defined as polynomials over ℤ in X recursively with physHermite 0 = 1 and

physHermite (n + 1) = 2 • X * physHermite n - derivative (physHermite n).

This polynomial will often be cast as a function ℝ → ℝ by evaluating the polynomial at X.

Equations

• PhysLean.physHermite 0 = 1
• PhysLean.physHermite n.succ = 2 • Polynomial.X * PhysLean.physHermite n - Polynomial.derivative (PhysLean.physHermite n)

theorem PhysLean.physHermite_succ (n : ℕ) : physHermite (n + 1) = 2 • Polynomial.X * physHermite n - Polynomial.derivative (physHermite n)

theorem PhysLean.physHermite_eq_iterate (n : ℕ) : physHermite n = (fun (p : Polynomial ℤ) => 2 * Polynomial.X * p - Polynomial.derivative p)^[n] 1

@[simp]

theorem PhysLean.physHermite_zero : physHermite 0 = Polynomial.C 1

theorem PhysLean.physHermite_one : physHermite 1 = 2 * Polynomial.X

theorem PhysLean.derivative_physHermite_succ (n : ℕ) : Polynomial.derivative (physHermite (n + 1)) = 2 * (n + 1) • physHermite n

theorem PhysLean.derivative_physHermite (n : ℕ) : Polynomial.derivative (physHermite n) = 2 * n • physHermite (n - 1)

theorem PhysLean.physHermite_succ' (n : ℕ) : physHermite (n + 1) = 2 • Polynomial.X * physHermite n - 2 * n • physHermite (n - 1)

theorem PhysLean.coeff_physHhermite_succ_zero (n : ℕ) : (physHermite (n + 1)).coeff 0 = -(physHermite n).coeff 1

theorem PhysLean.coeff_physHermite_succ_succ (n k : ℕ) : (physHermite (n + 1)).coeff (k + 1) = 2 * (physHermite n).coeff k - (↑k + 2) * (physHermite n).coeff (k + 2)

theorem PhysLean.coeff_physHermite_of_lt {n k : ℕ} (hnk : n < k) : (physHermite n).coeff k = 0

@[simp]

theorem PhysLean.coeff_physHermite_self_succ (n : ℕ) : (physHermite n).coeff n = 2 ^ n

@[simp]

theorem PhysLean.degree_physHermite (n : ℕ) : (physHermite n).degree = ↑n

@[simp]

theorem PhysLean.natDegree_physHermite {n : ℕ} : (physHermite n).natDegree = n

theorem PhysLean.iterate_derivative_physHermite_of_gt {n m : ℕ} (h : n < m) : (⇑Polynomial.derivative)^[m] (physHermite n) = 0

@[simp]

theorem PhysLean.iterate_derivative_physHermite_self {n : ℕ} : (⇑Polynomial.derivative)^[n] (physHermite n) = Polynomial.C (↑n.factorial * 2 ^ n)

@[simp]

theorem PhysLean.physHermite_leadingCoeff {n : ℕ} : (physHermite n).leadingCoeff = 2 ^ n

@[simp]

theorem PhysLean.physHermite_ne_zero {n : ℕ} : physHermite n ≠ 0

instance PhysLean.instCoeFunPolynomialIntForallReal_physLean : CoeFun (Polynomial ℤ) fun (x : Polynomial ℤ) => ℝ → ℝ

Equations

• PhysLean.instCoeFunPolynomialIntForallReal_physLean = { coe := fun (p : Polynomial ℤ) (x : ℝ) => (Polynomial.aeval x) p }

theorem PhysLean.physHermite_eq_aeval (n : ℕ) (x : ℝ) : (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x = (Polynomial.aeval x) (physHermite n)

theorem PhysLean.physHermite_zero_apply (x : ℝ) : (fun (x : ℝ) => (Polynomial.aeval x) (physHermite 0)) x = 1

theorem PhysLean.physHermite_pow (n m : ℕ) (x : ℝ) : (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x ^ m = (Polynomial.aeval x) (physHermite n ^ m)

theorem PhysLean.physHermite_succ_fun (n : ℕ) : (fun (x : ℝ) => (Polynomial.aeval x) (physHermite (n + 1))) = ((2 • fun (x : ℝ) => x) * fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) - (2 * ↑n) • fun (x : ℝ) => (Polynomial.aeval x) (physHermite (n - 1))

theorem PhysLean.physHermite_succ_fun' (n : ℕ) : (fun (x : ℝ) => (Polynomial.aeval x) (physHermite (n + 1))) = fun (x : ℝ) => 2 • x * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x - (2 * ↑n) • (fun (x : ℝ) => (Polynomial.aeval x) (physHermite (n - 1))) x

theorem PhysLean.iterated_deriv_physHermite_eq_aeval (n m : ℕ) : (deriv^[m] fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) = fun (x : ℝ) => (Polynomial.aeval x) ((⇑Polynomial.derivative)^[m] (physHermite n))

theorem PhysLean.physHermite_differentiableAt (n : ℕ) (x : ℝ) : DifferentiableAt ℝ (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x

theorem PhysLean.deriv_physHermite_differentiableAt (n m : ℕ) (x : ℝ) : DifferentiableAt ℝ (deriv^[m] fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x

theorem PhysLean.deriv_physHermite (n : ℕ) : (deriv fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) = 2 * ↑n * fun (x : ℝ) => (Polynomial.aeval x) (physHermite (n - 1))

theorem PhysLean.fderiv_physHermite {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) (f : E → ℝ) (hf : DifferentiableAt ℝ f x) (n : ℕ) : fderiv ℝ (fun (x : E) => (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) (f x)) x = (2 * ↑n * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite (n - 1))) (f x)) • fderiv ℝ f x

@[simp]

theorem PhysLean.deriv_physHermite' (x : ℝ) (f : ℝ → ℝ) (hf : DifferentiableAt ℝ f x) (n : ℕ) : deriv (fun (x : ℝ) => (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) (f x)) x = 2 * ↑n * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite (n - 1))) (f x) * deriv f x

theorem PhysLean.physHermite_parity (n : ℕ) (x : ℝ) : (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) (-x) = (-1) ^ n * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x

Relationship to Gaussians

theorem PhysLean.deriv_gaussian_eq_physHermite_mul_gaussian (n : ℕ) (x : ℝ) : deriv^[n] (fun (y : ℝ) => Real.exp (-y ^ 2)) x = (-1) ^ n * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * Real.exp (-x ^ 2)

theorem PhysLean.physHermite_eq_deriv_gaussian (n : ℕ) (x : ℝ) : (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x = (-1) ^ n * deriv^[n] (fun (y : ℝ) => Real.exp (-y ^ 2)) x / Real.exp (-x ^ 2)

theorem PhysLean.physHermite_eq_deriv_gaussian' (n : ℕ) (x : ℝ) : (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x = (-1) ^ n * deriv^[n] (fun (y : ℝ) => Real.exp (-y ^ 2)) x * Real.exp (x ^ 2)

theorem PhysLean.guassian_integrable_polynomial {b : ℝ} (hb : 0 < b) (P : Polynomial ℤ) : MeasureTheory.Integrable (fun (x : ℝ) => (Polynomial.aeval x) P * Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem PhysLean.guassian_integrable_polynomial_cons {b c : ℝ} (hb : 0 < b) (P : Polynomial ℤ) : MeasureTheory.Integrable (fun (x : ℝ) => (Polynomial.aeval (c * x)) P * Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem PhysLean.physHermite_gaussian_integrable (n p m : ℕ) : MeasureTheory.Integrable ((deriv^[m] fun (x : ℝ) => (Polynomial.aeval x) (physHermite p)) * deriv^[n] fun (x : ℝ) => Real.exp (-x ^ 2)) MeasureTheory.volume

theorem PhysLean.integral_physHermite_mul_physHermite_eq_integral_deriv_exp (n m : ℕ) : ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = (-1) ^ m * ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * deriv^[m] (fun (x : ℝ) => Real.exp (-x ^ 2)) x

theorem PhysLean.integral_physHermite_mul_physHermite_eq_integral_deriv_inductive (n m p : ℕ) (hpm : p ≤ m) : ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = (-1) ^ (m - p) * ∫ (x : ℝ), deriv^[p] (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * deriv^[m - p] (fun (x : ℝ) => Real.exp (-x ^ 2)) x

theorem PhysLean.integral_physHermite_mul_physHermite_eq_integral_deriv (n m : ℕ) : ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = ∫ (x : ℝ), deriv^[m] (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * Real.exp (-x ^ 2)

theorem PhysLean.physHermite_orthogonal_lt {n m : ℕ} (hnm : n < m) : ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = 0

theorem PhysLean.physHermite_orthogonal {n m : ℕ} (hnm : n ≠ m) : ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite m)) x * Real.exp (-x ^ 2) = 0

theorem PhysLean.physHermite_orthogonal_cons {n m : ℕ} (hnm : n ≠ m) (c : ℝ) : ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) (c * x) * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite m)) (c * x) * Real.exp (-c ^ 2 * x ^ 2) = 0

theorem PhysLean.physHermite_norm (n : ℕ) : ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) x * Real.exp (-x ^ 2) = ↑n.factorial * 2 ^ n * √Real.pi

theorem PhysLean.physHermite_norm_cons (n : ℕ) (c : ℝ) : ∫ (x : ℝ), (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) (c * x) * (fun (x : ℝ) => (Polynomial.aeval x) (physHermite n)) (c * x) * Real.exp (-c ^ 2 * x ^ 2) = |c⁻¹| • (↑n.factorial * 2 ^ n * √Real.pi)

@[irreducible]

theorem PhysLean.polynomial_mem_physHermite_span_induction (P : Polynomial ℤ) (n : ℕ) (hn : P.natDegree = n) : (fun (x : ℝ) => (Polynomial.aeval x) P) ∈ Submodule.span ℝ (Set.range fun (n : ℕ) (x : ℝ) => (Polynomial.aeval x) (physHermite n))

theorem PhysLean.polynomial_mem_physHermite_span (P : Polynomial ℤ) : (fun (x : ℝ) => (Polynomial.aeval x) P) ∈ Submodule.span ℝ (Set.range fun (n : ℕ) (x : ℝ) => (Polynomial.aeval x) (physHermite n))

theorem PhysLean.cos_mem_physHermite_span_topologicalClosure (c : ℝ) : (fun (x : ℝ) => Real.cos (c * x)) ∈ (Submodule.span ℝ (Set.range fun (n : ℕ) (x : ℝ) => (Polynomial.aeval x) (physHermite n))).topologicalClosure