Orthogonality of the Hermite polynomials

Stream: new members

[Luke Mantle]

I've been working on the Hermite polynomials (see #18739, this post). While that PR is under review, I've been working on showing their orthogonality. I was wondering if I could get any advice on the best way to do that in Lean. Here's my current idea (with some non-Lean notation) :

For n<m,

lemma integral_polynomial_mul_deriv_gaussian_of_deg_lt
  (p : polynomial ℝ) (n m : ℕ) (hp : n = p.nat_degree) (hnm : n < m) :
∫ dx p(x) * (d/dx^m exp (-x^2 / 2)) = 0 := sorry

and for n=m,

lemma integral_polynomial_mul_deriv_gaussian_of_deg_eq
  (p : polynomial ℝ) (n : ℕ) (hp : n = p.nat_degree) :
∫ dx p(x) * (d/dx^n exp (-x^2 / 2)) = n! * p.coeff n * sqrt (2 * π) := sorry

and show each of these by induction. Then, I would apply these lemmas to the Hermite polynomials.

[Jake Levinson]

I think you want integration by parts in some form, though I'm not sure how to do that in Lean. Both of those statements can be proven from

lemma integral_polynomial_mul_deriv_gaussian
  (p : polynomial ℝ) (m : ℕ) :
∫ (x : ℝ), p.eval x * (deriv^[m+1] (λ y, real.exp (-y^2 / 2)) x) =
∫ (x : ℝ), p.derivative.eval x * (deriv^[m] (λ y, real.exp (-y^2 / 2)) x) := sorry

which is integration by parts plus a statement about decay at infinity. You might also want to use p.degree instead of p.nat_degree since that's more precise.

For instance here's a proof of the first one assuming this integration by parts lemma:

import measure_theory.integral.interval_integral

noncomputable theory

lemma integral_polynomial_mul_deriv_gaussian
  (p : polynomial ℝ) (m : ℕ) :
∫ (x : ℝ), p.eval x * (deriv^[m+1] (λ y, real.exp (-y^2 / 2)) x) =
∫ (x : ℝ), p.derivative.eval x * (deriv^[m] (λ y, real.exp (-y^2 / 2)) x) := sorry

lemma integral_polynomial_mul_deriv_gaussian_of_deg_lt
  (p : polynomial ℝ) (n m : ℕ) (hp : p.degree = n) (hnm : n < m) :
∫ (x : ℝ), p.eval x * (deriv^[m] (λ y, real.exp (-y^2 / 2)) x) = 0 :=
begin
  obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_lt hnm,
  clear hnm,
  rw integral_polynomial_mul_deriv_gaussian, -- integration by parts
  induction n with n ih generalizing p,
  { rw [polynomial.eq_C_of_degree_eq_zero hp, polynomial.derivative_C],
    simp, },
  { rw [n.succ_add k, integral_polynomial_mul_deriv_gaussian, ih],
    rw polynomial.degree_derivative_eq;
    simp [polynomial.nat_degree_eq_of_degree_eq_some hp] },
end

[Eric Wieser]

Guessing based on the wording in the original link, should we be integrating with respect to a measure that includes the weight function?

[Moritz Doll]

I don't think that has any advantages over just carrying around the exponential.

[Jake Levinson]

Is there even a statement of integration by parts for integrals over all of ℝ? There's integral_mul_deriv_eq_deriv_mul in measure_theory.integral.interval_integral, but it is for finite intervals. And there's measure_theory.integral.integral_eq_improper with some statements about improper integrals. I'm not sure how to combine these.

[Jake Levinson]

Apparently analysis.special_functions.gamma proves Γ(s+1) = s * Γ(s) using integration by parts:

/-! Now we establish the recurrence relation `Γ(s + 1) = s * Γ(s)` using integration by parts. -/

...
/-- The recurrence relation for the indefinite version of the `Γ` function. -/
lemma partial_Gamma_add_one {s : ℂ} (hs: 0 < s.re) {X : ℝ} (hX : 0 ≤ X) :
  partial_Gamma (s + 1) X = s * partial_Gamma s X - (-X).exp * X ^ s := sorry

But looking through the proof, I can't understand where integration by parts is used.

[Moritz Doll]

it looks to me that it uses the fundamental theorem of calculus (on line 243), not integration by parts.
Generally, I think you want to imitate the argument in some sense: define the finite integral, show that converges to the real thing (here you need that the improper integral equals the integral) and then do calculations with the finite integral and in the end observe that all boundary terms vanish in the limit.

[Moritz Doll]

I don't know what your final goal is, but if you want low-hanging fruit, then I think other properties of the Hermite function are better suited.

[Jireh Loreaux]

Moritz, one reason to bundle the weight into a measure μ is to get terms of docs#measure_theory.Lp ℝ 2 μ and where you can actually state orthogonality properly. However, I agree that this is not necessarily the first thing you want to do, and having unbundled versions is fine also.

[Moritz Doll]

that is true, but I think you want to have the unbundled version to prove that the Hermite functions are an ONS in the usual L^2.

[Moritz Doll]

I don't know any applications of the Hermite polynomials other than that, but probably the probability people want to use L^2 with an exponentially decaying weight (but I would expect that they want to normalize it as well).

[Jake Levinson]

Moritz Doll said:

I don't know what your final goal is, but if you want low-hanging fruit, then I think other properties of the Hermite function are better suited.

@Luke Mantle has already done a bunch of the other basic properties :)