HermiteL2: Gaussian-weighted orthogonality of the Hermite polynomials (Route B foundation) - #16
Merged
Conversation
First increment of the Hermite L²(ℝ) orthonormal-basis build (Route B of the T² operator-index bridge, docs/INDEX_PAIRING.md). Mathlib has the three-term recursion `hermite_succ` and Rodrigues, but not the derivative form Hₙ' = n·Hₙ₋₁, which is load-bearing for the diagonal value ⟨Hₙ,Hₙ⟩ = n!·√(2π). Proved here by induction from `hermite_succ`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…)·δₘₙ
The load-bearing analytic result for Route B of the T² operator-index bridge
(docs/INDEX_PAIRING.md). Sorry-free and axiom-clean (standard-three only).
Architecture (avoids n-fold integration by parts):
- `hasDerivAt_hermite_mul_gaussian`: Rodrigues recursion (Hₙ·w)' = -(Hₙ₊₁·w),
w = e^{-x²/2}, from `hermite_succ` + the Gaussian derivative.
- `integrable_aeval_mul_gaussian`: polynomial × Gaussian is integrable, via
`induction_on'` to monomials + `integrable_rpow_mul_exp_neg_mul_sq`.
- the one-IBP pairing recursion ∫ p·Hₙ₊₁·w = ∫ p'·Hₙ·w
(`integral_mul_deriv_eq_deriv_mul_of_integrable`),
- `hermite_integral_eq_zero_of_ne`: off-diagonal = 0 by degree induction,
- `hermite_integral_self`: diagonal = n!·√(2π) via `derivative_hermite` +
`integral_gaussian`,
- `hermite_orthogonality`: the combined δₘₙ statement.
Mathlib (v4.30.0) had only the Hermite polynomials + Rodrigues + `integral_gaussian`;
the orthogonality, integrability, and L²-function layers were absent. (The L²
HilbertBasis / completeness layer is the next, separate phase.)
Golden axiom report extended with the five Hermite headlines (all standard-three).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
mrdouglasny
force-pushed
the
hermite-l2-basis
branch
from
June 21, 2026 14:54
3ef4f37 to
bf3395c
Compare
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
First analytic foundation for Route B of the T² operator-index bridge (issue #14, settled with Jon: Landau/Hermite, not Weyl's lemma). New file
SpectralTriples/HermiteL2.lean, sorry-free and axiom-clean (standard-three only).What this is
Mathlib (v4.30.0) has the probabilists' Hermite polynomials + Rodrigues +
integral_gaussian, but not the Gaussian-weighted orthogonality, the polynomial×Gaussian integrability, or any Hermite L²-function layer. This PR builds the orthogonality layer:∫ Hₘ(x) Hₙ(x) e^{−x²/2} dx = n!·√(2π)·δₘₙ(hermite_orthogonality)Architecture (avoids n-fold integration by parts)
derivative_hermite—Hₙ₊₁' = (n+1)·Hₙ(probabilists' identity; not in Mathlib), pure-algebra induction fromhermite_succ.hasDerivAt_hermite_mul_gaussian— Rodrigues recursion(Hₙ·w)' = −(Hₙ₊₁·w),w = e^{−x²/2}.integrable_aeval_mul_gaussian— any polynomial ×e^{−x²/2}is integrable (induction_on'→ monomials →integrable_rpow_mul_exp_neg_mul_sq).∫ p·Hₙ₊₁·w = ∫ p'·Hₙ·wviaintegral_mul_deriv_eq_deriv_mul_of_integrable.hermite_integral_eq_zero_of_ne— off-diagonal= 0by degree induction.hermite_integral_self— diagonal= n!·√(2π)viaderivative_hermite+integral_gaussian (1/2).Assurance
lake build SpectralTriplesgreen; zerosorry, zero projectaxiom.audit/axiom-report.txtextended with the five Hermite headlines — all[propext, Classical.choice, Quot.sound], CI-diffed.Scope / next
This is only the orthogonality layer. The next (separate, harder) phase is completeness/density → an actual
HilbertBasis ℕofL²(ℝ), then M1 (weightedL²(L_k)) and the guiding-center reductionD⁺ ≅ magneticDirac k. Tracked indocs/INDEX_PAIRING.mdand issue #14.🤖 Generated with Claude Code