Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

DefinitionThe Hermite functions are a Hilbert basis of L²(ℝ)#

Orthonormality comes from the weighted-measure machinery and completeness from moment determinacy (TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot), applied to the exact-degree family Hₙ(x√2) against the Gaussian weight e^{-x²}.

TauCeti.hermiteHilbertBasis.{u_1} (𝕜 : Type u_1) [RCLike 𝕜] :
  HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)

Lean

Formalized in Tau Ceti as TauCeti.hermiteHilbertBasis.

Sources

• Tau Ceti documentation: TauCeti.hermiteHilbertBasis
• Source of TauCeti.hermiteHilbertBasis in TauCeti/Analysis/SpecialFunctions/Hermite/Function/HilbertBasis.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.hermiteHilbertBasis

Uses 3 · Used by 1

Statement usesThe weight ↔ measure isometry · The weighted-measure basis

Proof usesMoment determinacy, exponential-moment form (the roadmap's B1 hypothesis)

Used byParseval's identity for the Hermite basis (norm-square form)

TheoremParseval's identity for the Hermite basis (norm-square form)#

the squared Hermite coordinates of f sum to ‖f‖².

TauCeti.tsum_norm_sq_inner_hermiteFunctionLp.{u_1} {𝕜 : Type u_1} [RCLike 𝕜]
  (f : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)) :
  ∑' (n : ℕ), ‖inner 𝕜 (TauCeti.hermiteFunctionLp 𝕜 n) f‖ ^ 2 = ‖f‖ ^ 2

Lean

Formalized in Tau Ceti as TauCeti.tsum_norm_sq_inner_hermiteFunctionLp.

Other forms

Parseval's identity for the Chebyshev basis. Formalized in Tau Ceti as TauCeti.tsum_norm_sq_integral_normalizedChebyshevT_mul_measureT.

TauCeti.tsum_norm_sq_integral_normalizedChebyshevT_mul_measureT.{u_1} {𝕜 : Type u_1} [RCLike 𝕜]
  (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) :
  ∑' (n : ℕ),
      ‖∫ (x : ℝ),
            (algebraMap ℝ 𝕜) (TauCeti.normalizedChebyshevT n x) *
              ↑↑f x ∂Polynomial.Chebyshev.measureT‖ ^
        2 =
    ‖f‖ ^ 2

Parseval's identity for the Chebyshev cosine basis (norm-square form). Formalized in Tau Ceti as TauCeti.tsum_norm_sq_integral_normalizedChebyshevCosine_mul.

TauCeti.tsum_norm_sq_integral_normalizedChebyshevCosine_mul.{u_1} {𝕜 : Type u_1} [RCLike 𝕜]
  (f : ↥(MeasureTheory.Lp 𝕜 2 TauCeti.chebyshevAngleMeasure)) :
  ∑' (n : ℕ),
      ‖∫ (θ : ℝ),
            (algebraMap ℝ 𝕜) (TauCeti.normalizedChebyshevCosine n θ) *
              ↑↑f θ ∂TauCeti.chebyshevAngleMeasure‖ ^
        2 =
    ‖f‖ ^ 2

Parseval's identity for the Chebyshev cosine basis (interval-integral form). Formalized in Tau Ceti as TauCeti.tsum_norm_sq_intervalIntegral_normalizedChebyshevCosine_mul.

TauCeti.tsum_norm_sq_intervalIntegral_normalizedChebyshevCosine_mul.{u_1} {𝕜 : Type u_1} [RCLike 𝕜]
  (f : ↥(MeasureTheory.Lp 𝕜 2 TauCeti.chebyshevAngleMeasure)) :
  ∑' (n : ℕ),
      ‖∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (TauCeti.normalizedChebyshevCosine n θ) * ↑↑f θ‖ ^
        2 =
    ‖f‖ ^ 2

Parseval's identity for the Chebyshev cosine basis (polarized form). Formalized in Tau Ceti as TauCeti.tsum_star_integral_normalizedChebyshevCosine_mul_mul_integral.

TauCeti.tsum_star_integral_normalizedChebyshevCosine_mul_mul_integral.{u_1} {𝕜 : Type u_1}
  [RCLike 𝕜] (f g : ↥(MeasureTheory.Lp 𝕜 2 TauCeti.chebyshevAngleMeasure)) :
  ∑' (n : ℕ),
      star
          (∫ (θ : ℝ),
            (algebraMap ℝ 𝕜) (TauCeti.normalizedChebyshevCosine n θ) *
              ↑↑f θ ∂TauCeti.chebyshevAngleMeasure) *
        ∫ (θ : ℝ),
          (algebraMap ℝ 𝕜) (TauCeti.normalizedChebyshevCosine n θ) *
            ↑↑g θ ∂TauCeti.chebyshevAngleMeasure =
    inner 𝕜 f g

Parseval's identity for the Chebyshev cosine basis (polarized interval-integral form). Formalized in Tau Ceti as TauCeti.tsum_star_intervalIntegral_normalizedChebyshevCosine_mul_mul_intervalIntegral.

TauCeti.tsum_star_intervalIntegral_normalizedChebyshevCosine_mul_mul_intervalIntegral.{u_1}
  {𝕜 : Type u_1} [RCLike 𝕜] (f g : ↥(MeasureTheory.Lp 𝕜 2 TauCeti.chebyshevAngleMeasure)) :
  ∑' (n : ℕ),
      star
          (∫ (θ : ℝ) in 0..Real.pi,
            (algebraMap ℝ 𝕜) (TauCeti.normalizedChebyshevCosine n θ) * ↑↑f θ) *
        ∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (TauCeti.normalizedChebyshevCosine n θ) * ↑↑g θ =
    inner 𝕜 f g

Parseval's identity for the Hermite basis (polarized form). Formalized in Tau Ceti as TauCeti.tsum_inner_mul_inner_hermiteFunctionLp.

TauCeti.tsum_inner_mul_inner_hermiteFunctionLp.{u_1} {𝕜 : Type u_1} [RCLike 𝕜]
  (f g : ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)) :
  ∑' (n : ℕ),
      inner 𝕜 f (TauCeti.hermiteFunctionLp 𝕜 n) * inner 𝕜 (TauCeti.hermiteFunctionLp 𝕜 n) g =
    inner 𝕜 f g

Parseval's identity for the multi-index Hermite basis (polarized form). Formalized in Tau Ceti as TauCeti.tsum_inner_mul_inner_L2piMul_hermiteFunctionLp.

TauCeti.tsum_inner_mul_inner_L2piMul_hermiteFunctionLp.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜]
  {ι : Type u_2} [Fintype ι]
  (f g : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun x => MeasureTheory.volume))) :
  ∑' (a : ι → ℕ),
      inner 𝕜 f (TauCeti.L2piMul fun i => TauCeti.hermiteFunctionLp 𝕜 (a i)) *
        inner 𝕜 (TauCeti.L2piMul fun i => TauCeti.hermiteFunctionLp 𝕜 (a i)) g =
    inner 𝕜 f g

Parseval's identity for the multi-index Hermite basis (norm-square form). Formalized in Tau Ceti as TauCeti.tsum_norm_sq_inner_L2piMul_hermiteFunctionLp.

TauCeti.tsum_norm_sq_inner_L2piMul_hermiteFunctionLp.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜]
  {ι : Type u_2} [Fintype ι]
  (f : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi fun x => MeasureTheory.volume))) :
  ∑' (a : ι → ℕ), ‖inner 𝕜 (TauCeti.L2piMul fun i => TauCeti.hermiteFunctionLp 𝕜 (a i)) f‖ ^ 2 =
    ‖f‖ ^ 2

Sources

• Tau Ceti documentation: TauCeti.tsum_norm_sq_inner_hermiteFunctionLp
• Source of TauCeti.tsum_norm_sq_inner_hermiteFunctionLp in TauCeti/Analysis/SpecialFunctions/Hermite/Function/Parseval.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.tsum_norm_sq_inner_hermiteFunctionLp · TauCeti.tsum_norm_sq_integral_normalizedChebyshevT_mul_measureT · TauCeti.tsum_norm_sq_integral_normalizedChebyshevCosine_mul · TauCeti.tsum_norm_sq_intervalIntegral_normalizedChebyshevCosine_mul · TauCeti.tsum_star_integral_normalizedChebyshevCosine_mul_mul_integral · TauCeti.tsum_star_intervalIntegral_normalizedChebyshevCosine_mul_mul_intervalIntegral · TauCeti.tsum_inner_mul_inner_hermiteFunctionLp · TauCeti.tsum_inner_mul_inner_L2piMul_hermiteFunctionLp · TauCeti.tsum_norm_sq_inner_L2piMul_hermiteFunctionLp

Uses 7

Proof usesThe Fintype-indexed product Hilbert basis · The Chebyshev T polynomials are a Hilbert basis of L²(measureT) · The Hermite functions are a Hilbert basis of L²(ℝ) · Moment determinacy, exponential-moment form (the roadmap's B1 hypothesis) · Parseval's identity for a functional · The weight ↔ measure isometry · The weighted-measure basis

DefinitionThe Chebyshev T polynomials are a Hilbert basis of L²(measureT)#

Orthonormality is orthonormal_normalizedChebyshevTLp; completeness is orthogonal_span_normalizedChebyshevTLp_eq_bot.

TauCeti.chebyshevTHilbertBasis.{u_1} (𝕜 : Type u_1) [RCLike 𝕜] :
  HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)

Lean

Formalized in Tau Ceti as TauCeti.chebyshevTHilbertBasis.

Sources

• Tau Ceti documentation: TauCeti.chebyshevTHilbertBasis
• Source of TauCeti.chebyshevTHilbertBasis in TauCeti/Analysis/SpecialFunctions/Trigonometric/Chebyshev/HilbertBasis.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.chebyshevTHilbertBasis

Uses 1 · Used by 2

Proof usesMoment determinacy, exponential-moment form (the roadmap's B1 hypothesis)

Used byParseval's identity for the Hermite basis (norm-square form) · The Chebyshev expansion

TheoremThe Chebyshev expansion#

Every f ∈ L²(measureT) is the sum of its normalized Chebyshev-polynomial series.

TauCeti.hasSum_chebyshevT_expansion.{u_1} {𝕜 : Type u_1} [RCLike 𝕜]
  (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) :
  HasSum
    (fun n =>
      (∫ (x : ℝ),
          (algebraMap ℝ 𝕜) (TauCeti.normalizedChebyshevT n x) *
            ↑↑f x ∂Polynomial.Chebyshev.measureT) •
        TauCeti.normalizedChebyshevTLp 𝕜 n)
    f

Lean

Formalized in Tau Ceti as TauCeti.hasSum_chebyshevT_expansion.

Sources

• Tau Ceti documentation: TauCeti.hasSum_chebyshevT_expansion
• Source of TauCeti.hasSum_chebyshevT_expansion in TauCeti/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Parseval.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.hasSum_chebyshevT_expansion

Uses 2

Proof usesThe Chebyshev T polynomials are a Hilbert basis of L²(measureT) · Moment determinacy, exponential-moment form (the roadmap's B1 hypothesis)

TheoremMoment determinacy, exponential-moment form (the roadmap's B1 hypothesis)#

A finite measure on ℝ for which some exponential moment ∫ e^{a|x|} dμ with a > 0 is finite is determined by its polynomial moments. This is the form the completeness argument consumes: the hypothesis holds for Gaussian decay and automatically for compactly supported measures.

TauCeti.Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp
  {μ ν : MeasureTheory.Measure ℝ}
  (hμ : ∃ a, 0 < a ∧ MeasureTheory.Integrable (fun x => Real.exp (a * |x|)) μ)
  (hν : ∃ a, 0 < a ∧ MeasureTheory.Integrable (fun x => Real.exp (a * |x|)) ν)
  (hmom : ∀ (n : ℕ), ∫ (x : ℝ), x ^ n ∂μ = ∫ (x : ℝ), x ^ n ∂ν) : μ = ν

Lean

Formalized in Tau Ceti as TauCeti.Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp.

Sources

• Tau Ceti documentation: TauCeti.Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp
• Source of TauCeti.Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp in TauCeti/Probability/Moments/Determinacy.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.Measure.ext_of_forall_integral_pow_eq_of_exists_integrable_exp

Used by 12

Used byHausdorff--Bernstein--Widder theorem, finite-measure version on ℝ≥0 · The Berg--Christensen--Ressel representation theorem (Berg--Christensen--Ressel 4.1.13) · Parseval's identity for the Hermite basis (norm-square form) · The Chebyshev envelope functions are a Hilbert basis of L²((-1, 1]; dx) · The Chebyshev expansion · The Chebyshev T polynomials are a Hilbert basis of L²(measureT) · The Hermite functions are a Hilbert basis of L²(ℝ) · The rescaled Hermite functions are a Hilbert basis of L²(ℝ) · The complete Bernstein representation theorem, uniqueness form · The Stieltjes representation theorem, uniqueness form · The zero-spatial BCR theorem is the Hausdorff--Bernstein--Widder theorem · Parseval's identity for the Gaussian Hermite basis

DefinitionThe rescaled Hermite functions are a Hilbert basis of L²(ℝ)#

This is the Hermite basis in the normalization Mathlib's e^{-2πixξ} Fourier convention forces: the same bridge TauCeti.hilbertBasisOfOrthogonalSystem, run at the weight e^{-2πx²} and the polynomials Hₙ(2√π·x).

TauCeti.twoPiHermiteHilbertBasis.{u_1} (𝕜 : Type u_1) [RCLike 𝕜] :
  HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 MeasureTheory.volume)

Lean

Formalized in Tau Ceti as TauCeti.twoPiHermiteHilbertBasis.

Sources

• Tau Ceti documentation: TauCeti.twoPiHermiteHilbertBasis
• Source of TauCeti.twoPiHermiteHilbertBasis in TauCeti/Analysis/SpecialFunctions/Hermite/Function/Fourier/HilbertBasis.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.twoPiHermiteHilbertBasis

Uses 3

Statement usesThe weight ↔ measure isometry · The weighted-measure basis

Proof usesMoment determinacy, exponential-moment form (the roadmap's B1 hypothesis)

TheoremThe Fourier eigenrelation for the unitary Fourier transform of L²(ℝ; ℂ)#

The n-th rescaled Hermite function is an eigenvector of MeasureTheory.Lp.fourierTransformₗᵢ with eigenvalue (-i)ⁿ.

TauCeti.fourier_twoPiHermiteFunctionLp (n : ℕ) :
  FourierTransform.fourier (TauCeti.twoPiHermiteFunctionLp ℂ n) =
    (-Complex.I) ^ n • TauCeti.twoPiHermiteFunctionLp ℂ n

Lean

Formalized in Tau Ceti as TauCeti.fourier_twoPiHermiteFunctionLp.

Sources

• Tau Ceti documentation: TauCeti.fourier_twoPiHermiteFunctionLp
• Source of TauCeti.fourier_twoPiHermiteFunctionLp in TauCeti/Analysis/SpecialFunctions/Hermite/Function/Fourier/HilbertBasis.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.fourier_twoPiHermiteFunctionLp

Uses 1

Proof usesFourier eigenfunction theorem

TheoremCanonical Commutation Relation (CCR) for the Hermite ladder operators#

[a, a†] = a ∘L a† - a† ∘L a = id.

TauCeti.hermiteAnnihilationCLM_comp_hermiteCreationCLM_sub_hermiteCreationCLM_comp_hermiteAnnihilationCLM :
  TauCeti.hermiteAnnihilationCLM ∘SL TauCeti.hermiteCreationCLM -
      TauCeti.hermiteCreationCLM ∘SL TauCeti.hermiteAnnihilationCLM =
    ContinuousLinearMap.id ℝ (SchwartzMap ℝ ℝ)

Lean

Formalized in Tau Ceti as TauCeti.hermiteAnnihilationCLM_comp_hermiteCreationCLM_sub_hermiteCreationCLM_comp_hermiteAnnihilationCLM.

Sources

• Tau Ceti documentation: TauCeti.hermiteAnnihilationCLM_comp_hermiteCreationCLM_sub_hermiteCreationCLM_comp_hermiteAnnihilationCLM
• Source of TauCeti.hermiteAnnihilationCLM_comp_hermiteCreationCLM_sub_hermiteCreationCLM_comp_hermiteAnnihilationCLM in TauCeti/Analysis/SpecialFunctions/Hermite/Function/Operator.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.hermiteAnnihilationCLM_comp_hermiteCreationCLM_sub_hermiteCreationCLM_comp_hermiteAnnihilationCLM

DefinitionThe weight ↔ measure isometry#

For an almost-everywhere-positive weight w, multiplication by √w is a linear isometric equivalence L²(w·μ; E) ≃ₗᵢ[𝕜] L²(μ; E).

TauCeti.weightL2Isometry.{u_1, u_2, u_3} (𝕜 : Type u_1) {E : Type u_2} {α : Type u_3} [NormedRing 𝕜]
  [NormedAddCommGroup E] [NormedSpace ℝ E] [_root_.Module 𝕜 E] [IsBoundedSMul 𝕜 E]
  [SMulCommClass ℝ 𝕜 E] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (w : α → ℝ)
  (hwpos : ∀ᵐ (x : α) ∂μ, 0 < w x) (hwm : AEMeasurable w μ) :
  ↥(MeasureTheory.Lp E 2 (μ.withDensity fun x => ENNReal.ofReal (w x))) ≃ₗᵢ[𝕜]
    ↥(MeasureTheory.Lp E 2 μ)

Lean

Formalized in Tau Ceti as TauCeti.weightL2Isometry.

Sources

• Tau Ceti documentation: TauCeti.weightL2Isometry
• Source of TauCeti.weightL2Isometry in TauCeti/MeasureTheory/Function/WeightL2Isometry.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.weightL2Isometry

Used by 4

Used byParseval's identity for the Hermite basis (norm-square form) · The Chebyshev envelope functions are a Hilbert basis of L²((-1, 1]; dx) · The Hermite functions are a Hilbert basis of L²(ℝ) · The rescaled Hermite functions are a Hilbert basis of L²(ℝ)

DefinitionThe Chebyshev envelope functions are a Hilbert basis of L²((-1, 1]; dx)#

It is the weight-in-the-function normalization, assembled from the same bridge as the weight-in-the-measure basis TauCeti.chebyshevTHilbertBasis: orthonormality from the Chebyshev orthogonality relation, completeness from moment determinacy applied to the exact-degree family Tₙ.

TauCeti.chebyshevTEnvelopeHilbertBasis.{u_1} (𝕜 : Type u_1) [RCLike 𝕜] :
  HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.volume.restrict (Set.Ioc (-1) 1)))

Lean

Formalized in Tau Ceti as TauCeti.chebyshevTEnvelopeHilbertBasis.

Sources

• Tau Ceti documentation: TauCeti.chebyshevTEnvelopeHilbertBasis
• Source of TauCeti.chebyshevTEnvelopeHilbertBasis in TauCeti/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Envelope.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.chebyshevTEnvelopeHilbertBasis

Uses 3

Statement usesThe weight ↔ measure isometry · The weighted-measure basis

Proof usesMoment determinacy, exponential-moment form (the roadmap's B1 hypothesis)

DefinitionThe weighted-measure basis#

The normalized bare functions, orthonormal by the orthogonality relation and complete by hypothesis, form a Hilbert basis of L²(w·μ) — the textbook statement that a family of orthogonal functions is an orthonormal basis of its own weighted L² space.

TauCeti.hilbertBasisOfWeightedMeasure.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2}
  [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α}
  (hwnn : ∀ᵐ (x : α) ∂μ, 0 ≤ w x) (hwm : AEMeasurable w μ) (hc : ∀ (n : ℕ), 0 < c n)
  (horth : ∀ (m n : ℕ), ∫ (x : α), f m x * f n x * w x ∂μ = if m = n then c n else 0)
  (hmem :
    ∀ (n : ℕ),
      MeasureTheory.MemLp (fun x => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2
        (μ.withDensity fun x => ENNReal.ofReal (w x)))
  (hcomplete : (Submodule.span 𝕜 (Set.range (TauCeti.bareNormalizedLp f w c hmem)))ᗮ = ⊥) :
  HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (μ.withDensity fun x => ENNReal.ofReal (w x)))

Lean

Formalized in Tau Ceti as TauCeti.hilbertBasisOfWeightedMeasure.

Sources

• Tau Ceti documentation: TauCeti.hilbertBasisOfWeightedMeasure
• Source of TauCeti.hilbertBasisOfWeightedMeasure in TauCeti/Analysis/InnerProductSpace/WeightedOrthogonalBasis.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.hilbertBasisOfWeightedMeasure

Used by 5

Used byParseval's identity for the Hermite basis (norm-square form) · The Chebyshev envelope functions are a Hilbert basis of L²((-1, 1]; dx) · The Hermite functions are a Hilbert basis of L²(ℝ) · The rescaled Hermite functions are a Hilbert basis of L²(ℝ) · Parseval's identity for the Gaussian Hermite basis

DefinitionThe product Hilbert basis#

Pointwise products of two Hilbert bases form a Hilbert basis of L²(μ ⊗ ν), indexed by the product of the index types.

HilbertBasis.prod.{u_1, u_2, u_3, u_4, u_5} {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [RCLike 𝕜]
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν]
  {ι₁ : Type u_4} {ι₂ : Type u_5} (b₁ : HilbertBasis ι₁ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 μ))
  (b₂ : HilbertBasis ι₂ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 ν)) :
  HilbertBasis (ι₁ × ι₂) 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (μ.prod ν))

Lean

Formalized in Tau Ceti as HilbertBasis.prod.

Sources

• Tau Ceti documentation: HilbertBasis.prod
• Source of HilbertBasis.prod in TauCeti/Analysis/InnerProductSpace/L2/Product.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanHilbertBasis.prod

Uses 1

Proof usesThe tensor as a bounded bilinear map

DefinitionThe Fintype-indexed product Hilbert basis#

Pointwise products of coordinatewise Hilbert bases form a Hilbert basis of L²(Measure.pi μ), indexed by the dependent function type.

TauCeti.piHilbertBasis.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {ι : Type u_2} [Fintype ι]
  {α : ι → Type u_3} [(i : ι) → MeasurableSpace (α i)] {μ : (i : ι) → MeasureTheory.Measure (α i)}
  [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] [RCLike 𝕜] {κ : ι → Type u_4}
  (b : (i : ι) → HilbertBasis (κ i) 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (μ i))) :
  HilbertBasis ((i : ι) → κ i) 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.Measure.pi μ))

Lean

Formalized in Tau Ceti as TauCeti.piHilbertBasis.

Sources

• Tau Ceti documentation: TauCeti.piHilbertBasis
• Source of TauCeti.piHilbertBasis in TauCeti/Analysis/InnerProductSpace/L2/Pi.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanTauCeti.piHilbertBasis

Used by 2

Used byParseval's identity for the Hermite basis (norm-square form) · Parseval's identity for the Gaussian Hermite basis

DefinitionThe tensor as a bounded bilinear map#

prodMulL F G = prodMul F G, packaged so that either operand can be fixed: prodMulL F fixes the left factor, prodMulL.flip G the right. Its operator norm is at most 1; neither measure needs to be s-finite.

MeasureTheory.Lp.prodMulL.{u_1, u_2, u_3} {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NontriviallyNormedField 𝕜] :
  ↥(MeasureTheory.Lp 𝕜 2 μ) →L[𝕜] ↥(MeasureTheory.Lp 𝕜 2 ν) →L[𝕜] ↥(MeasureTheory.Lp 𝕜 2 (μ.prod ν))

Lean

Formalized in Tau Ceti as MeasureTheory.Lp.prodMulL.

Sources

• Tau Ceti documentation: MeasureTheory.Lp.prodMulL
• Source of MeasureTheory.Lp.prodMulL in TauCeti/MeasureTheory/Function/Lp/Product.lean
• Tau Ceti roadmap status: Weighted orthogonal L² bases — completeness, Hilbert-basis structure, and product bases of orthogonal systems

LeanMeasureTheory.Lp.prodMulL

Used by 1

Used byThe product Hilbert basis

TheoremFourier eigenfunction theorem#

For Mathlib's exp (-2πixξ) convention, the rescaled Hermite function Φₙ(x) = √(√(2π)) ψₙ(√(2π)x) has eigenvalue (-i)ⁿ.

TauCeti.fourier_twoPiHermiteFunction (n : ℕ) :
  (FourierTransform.fourier fun x => ↑(TauCeti.twoPiHermiteFunction n x)) = fun x =>
    (-Complex.I) ^ n * ↑(TauCeti.twoPiHermiteFunction n x)

Lean

Formalized in Tau Ceti as TauCeti.fourier_twoPiHermiteFunction.

Sources

• Tau Ceti documentation: TauCeti.fourier_twoPiHermiteFunction
• Source of TauCeti.fourier_twoPiHermiteFunction in TauCeti/Analysis/SpecialFunctions/Hermite/Function/Fourier/Basic.lean

LeanTauCeti.fourier_twoPiHermiteFunction

Used by 1

Used byThe Fourier eigenrelation for the unitary Fourier transform of L²(ℝ; ℂ)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.