Physlib

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Existence.GaussianKernelGrowth

Growth of the heat kernel's derivatives (Milestone 1′, Track A)

A **self-contained real-analysis fact**, with no dependence on the unitary group `U`, the Hilbert space `H`, or any operator machinery: a uniform factorial-type bound on the `L¹` norm of the `n`-th derivative of the normalized heat kernel `gaussianKernel ε` (`GardingVectors.lean`).

This is exactly the estimate needed to make `analyticGardingVector ε ψ` a genuine `LinearPMap.IsAnalyticVector` of `stoneCandidateGenerator` once combined with the (separately tracked) commutation identity `stoneCandidateGenerator_analyticGardingVector`: that identity turns `Aⁿ (analyticGardingVector ε ψ)` into (up to a unimodular scalar) `analyticGardingVector`-of-the- `n`-th-derivative-kernel smeared against `ψ`, whose norm is bounded by `(L¹ norm of the n-th kernel derivative) * ‖ψ‖` (since `‖U t ψ‖ = ‖ψ‖`); this file's bound is what then makes `∑ ‖Aⁿ (analyticGardingVector ε ψ)‖ tⁿ / n!` summable for suitable `t`.

Strategy (revised — thanks to a user suggestion pointing at the right Mathlib lemma)

Mathlib already has the exact structural identity needed, so there is no need to invent a polynomial recursion from scratch: `Polynomial.deriv_gaussian_eq_hermite_mul_gaussian`,

`deriv^[n] (fun y => exp (-(y^2/2))) x = (-1)^n * aeval x (hermite n) * exp (-(x^2/2))`,

where `hermite n` is the *probabilists'* Hermite polynomial. Combined with the scaling `x = √(2/ε) t` (which turns `gaussianKernel ε`'s `exp(-t²/ε)` into the standard-variance `exp(-x²/2)` this identity is stated for), this reduces `gaussianKernel_iteratedDeriv_L1_bound` to a single genuinely new fact:

**the weighted `L¹` growth of Hermite polynomials against the standard Gaussian**, `∫ |Hₙ(x)| exp(-x²/2) dx ≤ √(2π) · √(n!)`.

Rather than an `L^∞`-type Hermite bound (which Mathlib does not have, and which is arguably a harder classical fact than needed), this follows from **Cauchy–Schwarz** applied to `|Hₙ(x)| exp(-x²/2) = (|Hₙ(x)| exp(-x²/4)) · exp(-x²/4)`, reducing everything to the single **weighted `L²` norm identity** `∫ Hₙ(x)² exp(-x²/2) dx = √(2π) · n!` (the standard Hermite orthonormality fact, absent from Mathlib — checked directly, `Hermite/Basic.lean` has only algebraic/coefficient facts, `Hermite/Gaussian.lean` only the derivative identity above).

That `L²` identity is now **fully proved** (no `sorry`, no axioms beyond the standard `propext`/`Classical.choice`/`Quot.sound`), by a single-step recursion `Iₙ = n · Iₙ₋₁` rather than `n`-fold integration by parts:

* `hermite_derivative_succ`: the polynomial identity `Hₙ₊₁' = (n+1) · Hₙ` (absent from Mathlib; proved here by induction directly from the defining recursion `hermite_succ`, `Hₙ₊₁ = X·Hₙ - Hₙ'`). * `hermite_aeval_succ`/`hermite_aeval_deriv_succ`: the real-valued (`aeval`) specializations of `hermite_succ` and `hermite_derivative_succ`. * `integrable_aeval_mul_gaussian`: any polynomial times a Gaussian weight is integrable (proved by `Polynomial.induction_on'`, reducing to the monomial case via `integrable_rpow_mul_exp_neg_mul_sq`). * `hermite_gaussian_sq_integral_succ`: the recursion itself. With `u := Hₙ₊₁`, `v := Hₙ · exp(-x²/2)`, the defining recursion gives `v' = -u·exp(-x²/2)`, so integration by parts on `(-∞,∞)` (`integral_mul_deriv_eq_deriv_mul_of_integrable` — the "of_integrable" variant needs no explicit boundary-vanishing argument, only integrability of the three relevant products) turns `∫ Hₙ₊₁² exp(-x²/2)` into `∫ Hₙ₊₁' · Hₙ · exp(-x²/2)`, which `hermite_derivative_succ` identifies with `(n+1) · ∫ Hₙ² exp(-x²/2)`. * `hermite_gaussian_sq_integral`: assembled from the recursion by induction on `n`, with base case `∫ exp(-x²/2) = √(2π)` (`integral_gaussian` at `b = 1/2`).

An alternative strategy worth recording (suggested, not yet attempted): since `s ↦ g_ε(u - s)` is entire in a *complex* `s`, `analyticGardingVector`'s orbit `s ↦ U_s ψ_ε = ∫ g_ε(u-s) U_u ψ \, du` may extend to an entire `H`-valued function of a complex variable, from which analytic-vector status could follow via Taylor theory directly — potentially avoiding this whole Hermite apparatus. This would need a new general theorem ("entire orbit extension ⟹ `IsAnalyticVector`") that does not currently exist in the ported `AnalyticVector/*` files (checked: their API is purely series/growth-based), so it is not obviously smaller work; not pursued for now, and moot in any case now that the Hermite route is fully closed.

4 declarations

theorem

The function xne−cx2x^n e^{-cx^2} is integrable for c>0c > 0

For any natural number n∈Nn \in \mathbb{N} and any positive real number c>0c > 0, the function f:R→Rf: \mathbb{R} \to \mathbb{R} defined by f(x)=xne−cx2f(x) = x^n e^{-cx^2} is integrable.

theorem

Polynomials with Gaussian Weights are Integrable

For any polynomial qq with integer coefficients and any real constant c>0c > 0, the function x↦q(x)e−cx2x \mapsto q(x) e^{-cx^2} is integrable on R\mathbb{R}.

theorem

Closed-form expression for the nn-th derivative of the Gaussian kernel

For any real number ε>0\varepsilon > 0, the nn-th iterated derivative of the Gaussian kernel gε(t)=1πεe−t2/εg_\varepsilon(t) = \frac{1}{\sqrt{\pi \varepsilon}} e^{-t^2/\varepsilon} with respect to tt is given by dndtngε(t)=1πε(2ε)n(−1)nHn(2εt)exp⁡(−t2ε), \frac{d^n}{dt^n} g_\varepsilon(t) = \frac{1}{\sqrt{\pi \varepsilon}} \left( \sqrt{\frac{2}{\varepsilon}} \right)^n (-1)^n H_n\left( \sqrt{\frac{2}{\varepsilon}} t \right) \exp\left( -\frac{t^2}{\varepsilon} \right), where HnH_n denotes the nn-th probabilists' Hermite polynomial.

theorem

L1L^1 Norm Bound for Iterated Derivatives of the Gaussian Kernel

For any real number ε>0\varepsilon > 0, there exists a positive constant CC such that for every natural number nn, the nn-th iterated derivative of the Gaussian kernel Gε(t)=1πεexp⁡(−t2ε)G_\varepsilon(t) = \frac{1}{\sqrt{\pi \varepsilon}} \exp\left(-\frac{t^2}{\varepsilon}\right) is integrable on R\mathbb{R}, and its L1L^1 norm satisfies the bound ∫−∞∞∣dndtnGε(t)∣ dt≤Cn+1n!.\int_{-\infty}^{\infty} \left| \frac{d^n}{dt^n} G_\varepsilon(t) \right| \, dt \leq C^{n+1} \sqrt{n!}.