ProductBasisAndAnnuli

ProductBasisAndAnnuli

Finite several-variable basis infrastructure. Scaffolding notes: ScaffoldingNotes/Basis/product_basis_and_annuli.md.

theorem Hermite1DimdLEAN.productBasisOrthonormal {d : ℕ} (κ α β : MultiIndex d) : gaussianInner (PhiKappaAlpha κ α) (PhiKappaAlpha κ β) = if α = β then 1 else 0

Product basis orthonormality at fixed multi-index κ.

theorem Hermite1DimdLEAN.nuKappa_norm_one {d : ℕ} (κ : MultiIndex d) : gaussianL2Norm (nuKappa κ) = 1

The distinguished basis vector has Gaussian norm one.

theorem Hermite1DimdLEAN.finiteParseval {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : hermiteNormSq κ G = ∑ α ∈ G.support, ‖G.coeff α‖ ^ 2

Finite Parseval for a finite several-variable Hermite sum.

theorem Hermite1DimdLEAN.coefficientAtZero {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : hermiteInnerNu κ G = G.coeff 0

Coefficient extraction against the distinguished vector ν_κ.

theorem Hermite1DimdLEAN.orthogonalToNu_iff_coeff_zero {d : ℕ} (κ : MultiIndex d) (G : FiniteHermiteSum d) : hermiteInnerNu κ G = 0 ↔ G.coeff 0 = 0

Orthogonality to ν_κ is equivalent to vanishing zero coefficient.

theorem Hermite1DimdLEAN.productBasisPhaseLaw {d : ℕ} (κ α : MultiIndex d) (t : ℝ) (z : CSpace d) : (PhiKappaAlpha κ α fun (q : Fin d) => Complex.exp (Complex.I * ↑t) * z q) = Complex.exp (Complex.I * ((↑↑(totalDegree α) - ↑↑(totalDegree κ)) * ↑t)) * PhiKappaAlpha κ α z

Global phase law on the product basis.

theorem Hermite1DimdLEAN.totalDegreePiecePhaseLaw {d : ℕ} (κ : MultiIndex d) (n : ℕ) (G : FiniteHermiteSum d) (t : ℝ) (z : CSpace d) : (evalHermiteSum κ (totalDegreePiece n G) fun (q : Fin d) => Complex.exp (Complex.I * ↑t) * z q) = Complex.exp (Complex.I * ((↑↑n - ↑↑(totalDegree κ)) * ↑t)) * evalHermiteSum κ (totalDegreePiece n G) z

The same phase law for a fixed total-degree piece.

theorem Hermite1DimdLEAN.partitionOfGaussianNorm {d : ℕ} (F : CSpace d → ℂ) (hF : MeasureTheory.Integrable (fun (z : CSpace d) => ‖F z‖ ^ 2) (gaussianMeasure d)) : gaussianL2NormSq F = ∑' (j : MultiIndex d), annulusMass j F

Partition of the Gaussian norm by product annuli.

theorem Hermite1DimdLEAN.annulusIntegrablePolynomial {d : ℕ} (j κ : MultiIndex d) (G H : FiniteHermiteSum d) : MeasureTheory.Integrable (indicatorMul (productAnnulus j) fun (z : CSpace d) => evalHermiteSum κ G z * (starRingEnd ℂ) (evalHermiteSum κ H z)) (gaussianMeasure d)

Finite-Hermite annulus integrability wrapper on a fixed annulus.

theorem Hermite1DimdLEAN.annulusRotationInvariant {d : ℕ} (j : MultiIndex d) (t : ℝ) (z : CSpace d) : z ∈ productAnnulus j ↔ (fun (q : Fin d) => Complex.exp (Complex.I * ↑t) * z q) ∈ productAnnulus j

Rotation preserves a product annulus.

theorem Hermite1DimdLEAN.annulusRotationAveraging {d : ℕ} (j : MultiIndex d) (F : CSpace d → ENNReal) (hF : Measurable F) : ∫⁻ (z : CSpace d), if _h : z ∈ productAnnulus j then ∫⁻ (t : Circle), F fun (q : Fin d) => (fourier 1) t * z q ∂AddCircle.haarAddCircle else 0 ∂gaussianMeasure d = ∫⁻ (z : CSpace d), if _h : z ∈ productAnnulus j then F z else 0 ∂gaussianMeasure d

Rotation averaging on a product annulus for nonnegative measurable functions.

theorem Hermite1DimdLEAN.annulusOrthogonality {d : ℕ} (κ j α β : MultiIndex d) (hαβ : α ≠ β) : annulusInner j (PhiKappaAlpha κ α) (PhiKappaAlpha κ β) = 0

Annulus orthogonality of distinct basis vectors.

theorem Hermite1DimdLEAN.annulusParseval {d : ℕ} (κ j : MultiIndex d) (G : FiniteHermiteSum d) : annulusMass j (evalHermiteSum κ G) = ∑ α ∈ G.support, ‖G.coeff α‖ ^ 2 * annulusMass j (PhiKappaAlpha κ α)

Annulus Parseval for finite Hermite sums.