Adapted orthonormal bases and the Bessel coefficients

An orthonormal basis of W whose initial segments span U and V, and the coefficients of the two-variable kernel against its tensor squares.

The three subspaces are finite-dimensional — each is spanned by a finite family — which is what makes Module.finrank the right index bound and Gram–Schmidt applicable.

instance ZetaZeros.finiteDimensional_subspaceU {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) : FiniteDimensional ℂ ↥(subspaceU h Z m)

instance ZetaZeros.finiteDimensional_subspaceW {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) : FiniteDimensional ℂ ↥(subspaceW h Z m)

instance ZetaZeros.finiteDimensional_subspaceV {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) : FiniteDimensional ℂ ↥(subspaceV h Z m)

structure ZetaZeros.IsAdaptedBasis {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) (psi : Fin (Module.finrank ℂ ↥(subspaceW h Z m)) → ↥(L2Interval lam)) : Prop

A tuple is an adapted orthonormal basis: orthonormal, spanning W, and with the initial segments of lengths dim U and dim V spanning U and V. The nesting proved in subspaceU_le_subspaceV is what makes such a tuple possible.

• orthonormal : Orthonormal ℂ psi

  The tuple is orthonormal.

• span_W : Submodule.span ℂ (Set.range psi) = subspaceW h Z m

  It spans W.

• span_U : Submodule.span ℂ (psi '' {j : Fin (Module.finrank ℂ ↥(subspaceW h Z m)) | ↑j < Module.finrank ℂ ↥(subspaceU h Z m)}) = subspaceU h Z m

  Its first dim U members span U.

• span_V : Submodule.span ℂ (psi '' {j : Fin (Module.finrank ℂ ↥(subspaceW h Z m)) | ↑j < Module.finrank ℂ ↥(subspaceV h Z m)}) = subspaceV h Z m

  Its first dim V members span V.

noncomputable def ZetaZeros.alphaOf (eta : ℝ → ℝ) (lam : ℝ) (Z : Finset ℂ) (m : ℂ → ℕ) (psi : ↥(L2Interval lam)) : ℂ

The Bessel coefficient of a single L² element: the coefficient of the two-variable kernel against its tensor square.

Equations

• ZetaZeros.alphaOf eta lam Z m psi = ∫ (u : ℝ) (v : ℝ) in Set.Ioo (-lam) lam, ZetaZeros.bigF eta Z m u v * (starRingEnd ℂ) (↑↑psi u * ↑↑psi v)

noncomputable def ZetaZeros.alphaCoeff (eta : ℝ → ℝ) (lam : ℝ) (Z : Finset ℂ) (m : ℂ → ℕ) (psi : ℕ → ↥(L2Interval lam)) (j : ℕ) : ℂ

The indexed form of alphaOf.

Equations

• ZetaZeros.alphaCoeff eta lam Z m psi j = ZetaZeros.alphaOf eta lam Z m (psi j)