TrueLevelBasis #

An element G belongs to Hk k when its canonical Hermite-coefficient expansion converges pointwise to G and its weighted square norm is integrable. Equivalently, Hk k is the weighted-L² closure of span {Φₖ,ₙ} together with the pointwise Hermite expansion data.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def HermitekLEAN.finiteHermiteSum (k : ℕ) {D : ℕ} (a : Fin D → ℂ) :

ℂ → ℂ

A finite Hermite sum sum_{n < D} a_n Phi_{k,n}.

Equations

HermitekLEAN.finiteHermiteSum k a z = ∑ n : Fin D, a n * HermitekLEAN.Phi k (↑n) z

Instances For

source

def HermitekLEAN.topCoeff {d : ℕ} (a : Fin (d + 1) → ℂ) :

ℂ

The top coefficient of a degree-d finite Hermite sum.

Equations

HermitekLEAN.topCoeff a = a ⟨d, ⋯⟩

Instances For

source

noncomputable def HermitekLEAN.hermiteCoeff (k : ℕ) (G : ℂ → ℂ) (n : ℕ) :

ℂ

The canonical coefficient extractor for the true level basis.

Equations

HermitekLEAN.hermiteCoeff k G n = HermitekLEAN.weightedInner G (HermitekLEAN.Phi k n)

Instances For

source

noncomputable def HermitekLEAN.truncate (k J : ℕ) (G : ℂ → ℂ) :

ℂ → ℂ

The partial Hermite sum with the first J + 1 canonical coefficients of G.

Equations

HermitekLEAN.truncate k J G = HermitekLEAN.finiteHermiteSum k fun (n : Fin (J + 1)) => HermitekLEAN.hermiteCoeff k G ↑n

Instances For

source

noncomputable def HermitekLEAN.qkn :

ℕ → ℕ → ℝ → ℝ

The real radial coefficient in the polar decomposition of Phi k n.

Equations

HermitekLEAN.qkn k n r = 1 / √↑n.factorial * ∑ j ∈ Finset.range (min k n + 1), (-1) ^ j * ↑(k.choose j) * (↑n.factorial / ↑(n - j).factorial) * r ^ (↑n - 2 * ↑j)

Instances For

source

noncomputable def HermitekLEAN.circleLeadingFactor (k : ℕ) (r : ℝ) :

ℂ

The scalar front factor in the polar representation.

Equations

HermitekLEAN.circleLeadingFactor k r = ↑(r ^ k / √↑k.factorial)

Instances For

source

noncomputable def HermitekLEAN.finiteCircleCoeff (k : ℕ) (r : ℝ) {D : ℕ} (a : Fin D → ℂ) :

ℕ → ℂ

The finitely supported circle coefficient map attached to finite Hermite data.

Equations

HermitekLEAN.finiteCircleCoeff k r a n = if h : n < D then a ⟨n, h⟩ * ↑(HermitekLEAN.qkn k n r) else 0

Instances For

source

noncomputable def HermitekLEAN.finiteCirclePoly (k : ℕ) (r : ℝ) {D : ℕ} (a : Fin D → ℂ) :

Circle → ℂ

The finite Fourier polynomial on the circle attached to a finite Hermite sum.

Equations

HermitekLEAN.finiteCirclePoly k r a = HermitekLEAN.positiveTrigonometricPolynomial (HermitekLEAN.frequencyBand 0 D) (HermitekLEAN.finiteCircleCoeff k r a)

Instances For

source

noncomputable def HermitekLEAN.truncCirclePoly (k : ℕ) (r : ℝ) (J : ℕ) (G : ℂ → ℂ) :

Circle → ℂ

The finite circle polynomial built from the truncated coefficient vector of G.

Equations

HermitekLEAN.truncCirclePoly k r J G = HermitekLEAN.finiteCirclePoly k r fun (n : Fin (J + 1)) => HermitekLEAN.hermiteCoeff k G ↑n

Instances For

source

noncomputable def HermitekLEAN.tailAnnulusMass (F : ℂ → ℂ) (j0 : ℕ) :

ℝ

The total mass of F on annuli A_j with j >= j0.

Equations

HermitekLEAN.tailAnnulusMass F j0 = ∑' (j : ℕ), if j0 ≤ j then HermitekLEAN.annulusIntegralSq F j else 0

Instances For

Explicit and Polar Formulas #

source

theorem HermitekLEAN.gaussian_monomial_moments (a b : ℕ) :

1 / Real.pi * ∫ (z : ℂ), (z ^ a * star z ^ b).re * Real.exp (-‖z‖ ^ 2) = if a = b then ↑a.factorial else 0

Gaussian monomial moments in the weighted plane.

source

theorem HermitekLEAN.phi_explicit {k n : ℕ} {z : ℂ} :

Phi k n z = 1 / ↑√(↑k.factorial * ↑n.factorial) * ∑ j ∈ Finset.range (min k n + 1), (-1) ^ j * ↑(k.choose j) * (↑n.factorial / ↑(n - j).factorial) * z ^ (n - j) * star z ^ (k - j)

Explicit finite expansion for the true Hermite basis vector Phi k n.

source

theorem HermitekLEAN.phi_polar {k n : ℕ} {r : ℝ} :

0 < r → ∀ (t : Circle), Phi k n (circlePoint r t) = circleLeadingFactor k r * (fourier (-↑k)) t * (↑(qkn k n r) * (fourier ↑n) t)

Polar formula for Phi k n.

source

theorem HermitekLEAN.qkn_explicit {k n : ℕ} {r : ℝ} :

0 < r → qkn k n r = 1 / √↑n.factorial * ∑ j ∈ Finset.range (min k n + 1), (-1) ^ j * ↑(k.choose j) * (↑n.factorial / ↑(n - j).factorial) * r ^ (↑n - 2 * ↑j)

Explicit finite Laurent expansion for the radial coefficient qkn.

source

theorem HermitekLEAN.qkn_structure {k n : ℕ} {r : ℝ} :

0 < r → qkn k n r = 1 / √↑n.factorial * ∑ j ∈ Finset.range (min k n + 1), (-1) ^ j * ↑(k.choose j) * (↑n.factorial / ↑(n - j).factorial) * r ^ (↑n - 2 * ↑j)

Backward-compatible alias for the explicit Laurent expansion of qkn.

source

@[simp]

theorem HermitekLEAN.qkn_real {k n : ℕ} {r : ℝ} :

star ↑(qkn k n r) = ↑(qkn k n r)

The circle coefficients qkn remain fixed by complex conjugation.

source

theorem HermitekLEAN.qkn_top_term_asymptotic (k n : ℕ) :

∃ (c : ℝ), c ≠ 0 ∧ ∀ (ε : ℝ), 0 < ε → ∃ (R0 : ℝ), ∀ r ≥ R0, ‖↑(qkn k n r) / ↑r ^ n - ↑c‖ ≤ ε

source

theorem HermitekLEAN.qkn_top_term_limit (k n : ℕ) (ε : ℝ) :

0 < ε → ∃ (R0 : ℝ), 1 ≤ R0 ∧ ∀ (r : ℝ), R0 ≤ r → ‖↑(qkn k n r) / ↑r ^ n - ↑(1 / √↑n.factorial)‖ ≤ ε

After dividing by r^n, qkn k n r converges to its explicit top term.

source

theorem HermitekLEAN.qkn_eventual_lower_bound (k n : ℕ) :

∃ (R : ℝ) (c : ℝ), 1 ≤ R ∧ 0 < c ∧ ∀ r ≥ R, c * r ^ n ≤ ‖↑(qkn k n r)‖

Each qkn k n eventually dominates a positive multiple of r^n.

source

theorem HermitekLEAN.qkn_eventually_nonzero (k n : ℕ) :

∃ (R0 : ℝ), 1 ≤ R0 ∧ ∀ r ≥ R0, qkn k n r ≠ 0

The radial coefficient qkn k n is eventually nonvanishing on large radii.

source

theorem HermitekLEAN.qkn_ratio_control {k n d : ℕ} :

n < d → ∃ (C : ℝ) (R0 : ℝ), 0 < C ∧ 1 ≤ R0 ∧ ∀ (r : ℝ), R0 ≤ r → ‖↑(qkn k n r) / ↑(qkn k d r)‖ ≤ C / r

Lower modes are eventually suppressed by at least one power of r.

Finite-First Basis API #

Helpers for the diagonal case of phi_orthonormal #

Double-sum identity for phi_orthonormal diagonal case #

source

theorem HermitekLEAN.phi_orthonormal {k m n : ℕ} :

weightedInner (Phi k m) (Phi k n) = if m = n then 1 else 0

The level-k basis is orthonormal for the weighted inner product.

source

theorem HermitekLEAN.continuous_Phi (k n : ℕ) :

Continuous (Phi k n)

source

theorem HermitekLEAN.integrable_weightedDiag (k n : ℕ) :

MeasureTheory.Integrable (fun (z : ℂ) => ‖Phi k n z‖ ^ 2 * Real.exp (-‖z‖ ^ 2)) MeasureTheory.volume

source

theorem HermitekLEAN.integrable_weightedCross (k m n : ℕ) :

MeasureTheory.Integrable (fun (z : ℂ) => Phi k m z * (starRingEnd ℂ) (Phi k n z) * ↑(Real.exp (-‖z‖ ^ 2))) MeasureTheory.volume

source

theorem HermitekLEAN.finiteHermiteSum_inner {k D : ℕ} (a b : Fin D → ℂ) :

weightedInner (finiteHermiteSum k a) (finiteHermiteSum k b) = ∑ n : Fin D, a n * star (b n)

Inner products of finite Hermite sums are finite coefficient inner products.

source

theorem HermitekLEAN.finiteHermiteSum_normSq {k D : ℕ} (a : Fin D → ℂ) :

weightedNormSq (finiteHermiteSum k a) = ∑ n : Fin D, ‖a n‖ ^ 2

The weighted norm square of a finite Hermite sum is the coefficient ℓ² norm square.

source

theorem HermitekLEAN.Phi_mem_Hk (k n : ℕ) :

Phi k n ∈ Hk k

Every basis vector belongs to the true level space.

source

theorem HermitekLEAN.weightedNorm_smul (c : ℂ) (G : ℂ → ℂ) :

weightedNorm (c • G) = ‖c‖ * weightedNorm G

Weighted norms are homogeneous under scalar multiplication.

source

theorem HermitekLEAN.weightedDefectNorm_smul (c : ℂ) (F0 G : ℂ → ℂ) :

weightedDefectNorm (c • F0) (c • G) = ‖c‖ * weightedDefectNorm F0 G

Weighted defect norms are homogeneous under scalar multiplication.

source

theorem HermitekLEAN.finiteHermiteSum_mem_Hk (k : ℕ) {D : ℕ} (a : Fin D → ℂ) :

finiteHermiteSum k a ∈ Hk k

Every finite Hermite sum belongs to the true level space.

source

theorem HermitekLEAN.hermiteCoeff_finiteHermiteSum {k D : ℕ} (a : Fin D → ℂ) (n : ℕ) :

hermiteCoeff k (finiteHermiteSum k a) n = if h : n < D then a ⟨n, h⟩ else 0

The canonical coefficient extractor recovers the coefficients of a finite Hermite sum.

source

@[simp]

theorem HermitekLEAN.hermiteCoeff_phi0 {k : ℕ} {G : ℂ → ℂ} :

hermiteCoeff k G 0 = weightedInner G (phi0 k)

The zeroth coefficient is the inner product against the lowest basis vector.

source

theorem HermitekLEAN.orthogonal_phi0_iff_hermiteCoeff_zero {k : ℕ} {G : ℂ → ℂ} :

weightedInner G (phi0 k) = 0 ↔ hermiteCoeff k G 0 = 0

Orthogonality to Phi k 0 is equivalent to vanishing zeroth Hermite coefficient.

source

theorem HermitekLEAN.truncate_eq_finiteHermiteSum {k J : ℕ} {G : ℂ → ℂ} :

truncate k J G = finiteHermiteSum k fun (n : Fin (J + 1)) => hermiteCoeff k G ↑n

The truncation operator is the explicit finite Hermite sum of the first coefficients.

source

theorem HermitekLEAN.truncCirclePoly_eq_finiteCirclePoly {k J : ℕ} {G : ℂ → ℂ} {r : ℝ} :

truncCirclePoly k r J G = finiteCirclePoly k r fun (n : Fin (J + 1)) => hermiteCoeff k G ↑n

The truncated circle polynomial is the finite circle polynomial of the truncated vector.

source

theorem HermitekLEAN.hermiteCoeff_truncate {k J : ℕ} {G : ℂ → ℂ} (n : ℕ) :

hermiteCoeff k (truncate k J G) n = if _h : n < J + 1 then hermiteCoeff k G n else 0

The truncation keeps exactly the first J + 1 Hermite coefficients.

source

theorem HermitekLEAN.truncate_mem_Hk (k J : ℕ) (G : ℂ → ℂ) :

truncate k J G ∈ Hk k

Every truncation lies in the true level space.

source

theorem HermitekLEAN.truncate_normSq (k J : ℕ) (G : ℂ → ℂ) :

weightedNormSq (truncate k J G) = ∑ n : Fin (J + 1), ‖hermiteCoeff k G ↑n‖ ^ 2

Exact finite Parseval identity for Hermite truncations.

source

theorem HermitekLEAN.finiteHermiteSum_circle {k D : ℕ} (a : Fin D → ℂ) {r : ℝ} :

0 < r → ∀ (t : Circle), finiteHermiteSum k a (circlePoint r t) = circleLeadingFactor k r * (fourier (-↑k)) t * finiteCirclePoly k r a t

Finite Hermite sums admit a finite circle representation.

source

theorem HermitekLEAN.finiteCircleCoeff_eq_zero_outside {k D : ℕ} (r : ℝ) (a : Fin D → ℂ) {n : ℕ} :

D ≤ n → finiteCircleCoeff k r a n = 0

The finite circle coefficient map vanishes outside the finite frequency range.

source

theorem HermitekLEAN.finiteCirclePoly_support {k D : ℕ} (r : ℝ) (a : Fin D → ℂ) :

finiteCirclePoly k r a = positiveTrigonometricPolynomial (frequencyBand 0 D) (finiteCircleCoeff k r a)

The finite circle polynomial is supported in frequencies {0, ..., D - 1}.

source

theorem HermitekLEAN.finiteCirclePoly_support_pos {k D : ℕ} (r : ℝ) (a : Fin (D + 1) → ℂ) :

a 0 = 0 → finiteCirclePoly k r a = positiveTrigonometricPolynomial (frequencyBand 1 D) (finiteCircleCoeff k r a)

If the zeroth coefficient vanishes, the finite circle polynomial has positive-frequency support.

source

theorem HermitekLEAN.finiteCirclePoly_l2_identity {k D : ℕ} (r : ℝ) (a : Fin D → ℂ) :

circleL2Sq (finiteCirclePoly k r a) = ∑ n : Fin D, ‖a n‖ ^ 2 * |qkn k (↑n) r| ^ 2

Circle Parseval identity for finite Hermite sums.

source

theorem HermitekLEAN.truncate_circle (k J : ℕ) (G : ℂ → ℂ) {r : ℝ} :

0 < r → ∀ (t : Circle), truncate k J G (circlePoint r t) = circleLeadingFactor k r * (fourier (-↑k)) t * truncCirclePoly k r J G t

Truncations admit the corresponding finite circle representation.

source

theorem HermitekLEAN.truncCirclePoly_support {k J : ℕ} (r : ℝ) (G : ℂ → ℂ) :

truncCirclePoly k r J G = positiveTrigonometricPolynomial (frequencyBand 0 (J + 1)) (finiteCircleCoeff k r fun (n : Fin (J + 1)) => hermiteCoeff k G ↑n)

The truncation circle polynomial is supported in {0, ..., J}.

source

theorem HermitekLEAN.truncCirclePoly_support_pos {k J : ℕ} (r : ℝ) (G : ℂ → ℂ) :

weightedInner G (phi0 k) = 0 → truncCirclePoly k r J G = positiveTrigonometricPolynomial (frequencyBand 1 J) (finiteCircleCoeff k r fun (n : Fin (J + 1)) => hermiteCoeff k G ↑n)

Orthogonality to Phi k 0 removes the zero frequency from every truncation circle polynomial.

source

theorem HermitekLEAN.truncCirclePoly_l2_identity (k J : ℕ) (r : ℝ) (G : ℂ → ℂ) :

circleL2Sq (truncCirclePoly k r J G) = ∑ n : Fin (J + 1), ‖hermiteCoeff k G ↑n‖ ^ 2 * |qkn k (↑n) r| ^ 2

Circle Parseval identity for truncated Hermite sums.

Basis Bridge #

source

noncomputable def HermitekLEAN.hermiteSeries (k : ℕ) (g : ℕ → ℂ) :

ℂ → ℂ

The formal Hermite expansion attached to a coefficient sequence.

Equations

HermitekLEAN.hermiteSeries k g z = ∑' (n : ℕ), g n * HermitekLEAN.Phi k n z

Instances For

source

noncomputable def HermitekLEAN.circleSeries (k : ℕ) (g : ℕ → ℂ) (r : ℝ) :

Circle → ℂ

The circle series associated to Hermite coefficients at radius r.

Equations

HermitekLEAN.circleSeries k g r t = ∑' (n : ℕ), g n * ↑(HermitekLEAN.qkn k n r) * (fourier ↑n) t

Instances For

source

theorem HermitekLEAN.hermiteCoeff_expansion {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → G = hermiteSeries k (hermiteCoeff k G)

The canonical coefficient extractor recovers the Hermite expansion of any G ∈ H_k.

source

theorem HermitekLEAN.truncate_unique {k J : ℕ} {G H : ℂ → ℂ} :

H ∈ Hk k → (∀ (n : ℕ), hermiteCoeff k H n = if _h : n < J + 1 then hermiteCoeff k G n else 0) → H = truncate k J G

The truncation is the unique degree-≤ J element with the prescribed first coefficients.

source

theorem HermitekLEAN.integrable_truncate_normSq_exp (k J : ℕ) (G : ℂ → ℂ) :

MeasureTheory.Integrable (fun (z : ℂ) => ‖truncate k J G z‖ ^ 2 * Real.exp (-‖z‖ ^ 2)) MeasureTheory.volume

Integrability of truncation norm squared with Gaussian weight.

source

theorem HermitekLEAN.hermiteCoeff_parseval {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → weightedNormSq G = ∑' (n : ℕ), ‖hermiteCoeff k G n‖ ^ 2

Parseval identity for the canonical Hermite coefficients.

source

theorem HermitekLEAN.h_k_expansion {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∃ (g : ℕ → ℂ), G = hermiteSeries k g ∧ weightedNormSq G = ∑' (n : ℕ), ‖g n‖ ^ 2

Every G ∈ H_k admits a Hermite expansion with Parseval.

source

theorem HermitekLEAN.circle_representation {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∃ (g : ℕ → ℂ), G = hermiteSeries k g ∧ ∀ (r : ℝ), 0 < r → ∀ (t : Circle), G (circlePoint r t) = circleLeadingFactor k r * (fourier (-↑k)) t * circleSeries k g r t

Compatibility statement: polar/circle representation of an element of H_k.

source

theorem HermitekLEAN.circle_representation_hermiteCoeff {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∀ (r : ℝ), 0 < r → ∀ (t : Circle), G (circlePoint r t) = circleLeadingFactor k r * (fourier (-↑k)) t * circleSeries k (hermiteCoeff k G) r t

Canonical circle representation in terms of hermiteCoeff.

source

theorem HermitekLEAN.point_eval_bounded {k : ℕ} (z : ℂ) :

∃ (C : ℝ), 0 ≤ C ∧ ∀ {G : ℂ → ℂ}, G ∈ Hk k → ‖G z‖ ≤ C * weightedNorm G

Point evaluations are bounded on H_k.

source

theorem HermitekLEAN.circleSeries_l2_identity {k : ℕ} {G : ℂ → ℂ} {g : ℕ → ℂ} :

G ∈ Hk k → G = hermiteSeries k g → (Summable fun (n : ℕ) => ‖g n‖ ^ 2) → ∀ (r : ℝ), 0 < r → circleL2Sq (circleSeries k g r) = ∑' (n : ℕ), ‖g n‖ ^ 2 * |qkn k n r| ^ 2

Compatibility statement: circle Parseval identity for an H_k expansion.

source

theorem HermitekLEAN.circleSeries_l2_identity_hermiteCoeff {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∀ (r : ℝ), 0 < r → circleL2Sq (circleSeries k (hermiteCoeff k G) r) = ∑' (n : ℕ), ‖hermiteCoeff k G n‖ ^ 2 * |qkn k n r| ^ 2

Circle Parseval identity for the canonical coefficient sequence.

source

theorem HermitekLEAN.circleSeries_fourierCoeff_hermiteCoeff {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∀ {r : ℝ}, 0 < r → ∀ (n : ℕ), fourierCoeff (circleSeries k (hermiteCoeff k G) r) ↑n = hermiteCoeff k G n * ↑(qkn k n r)

The canonical circle series has the expected Fourier coefficients.

source

theorem HermitekLEAN.h_k_expansion_perp_phi0 {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → weightedInner G (Phi k 0) = 0 → ∃ (g : ℕ → ℂ), G = hermiteSeries k g ∧ g 0 = 0

Orthogonality to Phi k 0 yields an expansion with vanishing zero mode.

source

theorem HermitekLEAN.truncate_tendsto {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∀ (ε : ℝ), 0 < ε → ∃ (J0 : ℕ), ∀ J ≥ J0, weightedNorm (truncate k J G - G) ≤ ε

Truncations converge to G in the weighted norm.

source

theorem HermitekLEAN.truncate_locally_uniform {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∀ (R ε : ℝ), 0 < R → 0 < ε → ∃ (J0 : ℕ), ∀ J ≥ J0, ∀ (z : ℂ), ‖z‖ ≤ R → ‖truncate k J G z - G z‖ ≤ ε

Truncations converge locally uniformly on bounded sets.

source

theorem HermitekLEAN.truncCirclePoly_tendsto_circleSeries {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∀ (r : ℝ), 0 < r → ∀ (ε : ℝ), 0 < ε → ∃ (J0 : ℕ), ∀ J ≥ J0, circleL2Sq (truncCirclePoly k r J G - circleSeries k (hermiteCoeff k G) r) ≤ ε

The finite circle polynomials of G converge in circle L² to the Hermite circle series.

source

theorem HermitekLEAN.hermite_series_locally_uniform {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → ∃ (g : ℕ → ℂ), G = hermiteSeries k g ∧ Continuous G

Hermite expansions converge locally uniformly, hence are continuous.

source

theorem HermitekLEAN.continuous_of_mem_Hk {k : ℕ} {G : ℂ → ℂ} :

G ∈ Hk k → Continuous G

Every element of H_k is continuous.

source

theorem HermitekLEAN.hermiteCoeff_hermiteSeries {k : ℕ} {G : ℂ → ℂ} (h : ℕ → ℂ) :

G ∈ Hk k → G = hermiteSeries k h → (Summable fun (n : ℕ) => ‖h n‖ ^ 2) → ∀ (n : ℕ), hermiteCoeff k G n = h n

Fourier inversion: the canonical coefficients of a Hermite series recover the original coefficient sequence.

source

theorem HermitekLEAN.hermiteSeries_mem_Hk {k : ℕ} (h : ℕ → ℂ) :

(∀ (n : ℕ), ‖h n‖ ≤ 1) → (Summable fun (n : ℕ) => ‖h n‖ ^ 2) → hermiteSeries k h ∈ Hk k

A square-summable Hermite series defines an element of H_k.

source

theorem HermitekLEAN.modulusDefect_le_norm (F0 G : ℂ → ℂ) (z : ℂ) :

modulusDefect F0 G z ≤ ‖G z‖

The modulus defect is bounded by the perturbation norm.

Documentation

LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermitek.TrueLevelBasis

TrueLevelBasis #

Core Basis Objects #

Explicit and Polar Formulas #

Finite-First Basis API #

Helpers for the diagonal case of phi_orthonormal #

Double-sum identity for phi_orthonormal diagonal case #

Basis Bridge #