Roadmap area: OrthogonalL2Bases
Items in scope
What & why. One orthogonal family gives two bases depending on where the weight sits: the bare polynomials Hₙ/√(n!) as an ONB of the weighted / probability L² (e.g. N(0,1) — expansions, moment problems, chaos), or the Hₙ·√w functions as an ONB of Lebesgue L²(dx) (e.g. Hermite functions / QHO states, PDE, signal processing). They are the same object times √w, and √w is an isometry L²(w·μ) ≅ L²(μ). The roadmap builds only the Lebesgue side; this adds the isometry (plus a missing one-line HilbertBasis transport) so both sides come from one construction — neither normalization privileged, no per-consumer re-derivation.
Targets (narrow):
- Part 0:
weightL2Isometry, HilbertBasis.mapₗᵢ (+ mapₗᵢ_apply).
- A1:
derivative_hermite_succ, integrable_aeval_mul_gaussian, hermite_generating_function, orthogonality (integral_hermite_mul_hermite_mul_gaussian Lebesgue + integral_hermite_mul_hermite_gaussianReal measure).
- B2:
barePolyLp, orthonormal_barePolyLp, barePolyLp_ortho_eq_bot, hilbertBasisOfWeightedMeasure, hilbertBasisOfOrthogonalSystem (+ coe_*).
- A3′:
gaussianHermiteHilbertBasis (+ coe_*), memLp_hermite_gaussianReal.
Not claiming (open): B1 completeness, the Hermite-function object API (A2), B3 product/pi, Chebyshev (C).
Notes
A1 is implemented in TauCetiProject/TauCeti#499 (draft). Roadmap README + Targets.lean change is #45.
Roadmap area:
OrthogonalL2BasesItems in scope
What & why. One orthogonal family gives two bases depending on where the weight sits: the bare polynomials
Hₙ/√(n!)as an ONB of the weighted / probabilityL²(e.g.N(0,1)— expansions, moment problems, chaos), or theHₙ·√wfunctions as an ONB of LebesgueL²(dx)(e.g. Hermite functions / QHO states, PDE, signal processing). They are the same object times√w, and√wis an isometryL²(w·μ) ≅ L²(μ). The roadmap builds only the Lebesgue side; this adds the isometry (plus a missing one-lineHilbertBasistransport) so both sides come from one construction — neither normalization privileged, no per-consumer re-derivation.Targets (narrow):
weightL2Isometry,HilbertBasis.mapₗᵢ(+mapₗᵢ_apply).derivative_hermite_succ,integrable_aeval_mul_gaussian,hermite_generating_function, orthogonality (integral_hermite_mul_hermite_mul_gaussianLebesgue +integral_hermite_mul_hermite_gaussianRealmeasure).barePolyLp,orthonormal_barePolyLp,barePolyLp_ortho_eq_bot,hilbertBasisOfWeightedMeasure,hilbertBasisOfOrthogonalSystem(+coe_*).gaussianHermiteHilbertBasis(+coe_*),memLp_hermite_gaussianReal.Not claiming (open): B1 completeness, the Hermite-function object API (A2), B3 product/
pi, Chebyshev (C).Notes
A1 is implemented in TauCetiProject/TauCeti#499 (draft). Roadmap README +
Targets.leanchange is #45.