The probabilists' Hermite polynomials over ℝ

Mathlib defines Polynomial.hermite in ℤ[X]. Every analytic consumer in this library wants the same family in ℝ[X], and each of them was spelling the cast out inline as (hermite n).map (Int.castRingHom ℝ), re-deriving eval and degree facts about it at the point of use. This file gives that cast a name and states those two facts once.

It deliberately sits beside TauCeti/RingTheory/Polynomial/Hermite/Derivative.lean rather than in any analysis or probability file: the definition mentions no measure, no inner product space, and no Gaussian, so putting it here is what lets the earlier function-side files import it. A copy living in a Gaussian leaf file would be unreachable from exactly the places that need it.

Main definitions

• TauCeti.hermiteℝ — Hₙ cast into ℝ[X].

Main statements

• TauCeti.eval_hermiteℝ — evaluation agrees with aeval against the integer polynomial.
• TauCeti.degree_hermiteℝ — the cast preserves degrees, so Hₙ has degree exactly n. This is the exact-degree hypothesis that the polynomial-completeness machinery consumes.

noncomputable def TauCeti.hermiteℝ (n : ℕ) : Polynomial ℝ

Hₙ over ℝ: Mathlib's Polynomial.hermite n lives in ℤ[X], and the analytic consumers in this library take a real polynomial family.

Equations

• TauCeti.hermiteℝ n = Polynomial.map (Int.castRingHom ℝ) (Polynomial.hermite n)

@[simp]

theorem TauCeti.eval_hermiteℝ (n : ℕ) (x : ℝ) : Polynomial.eval x (hermiteℝ n) = (Polynomial.aeval x) (Polynomial.hermite n)

@[simp]

theorem TauCeti.degree_hermiteℝ (n : ℕ) : (hermiteℝ n).degree = ↑n

The cast to ℝ[X] preserves degrees: Hₙ has degree exactly n.

Marked @[simp], matching Mathlib's own Polynomial.degree_hermite.