The three nested subspaces

U ⊆ V ⊆ W inside L²((-lam, lam)), spanned by the twisted functions attached to the three parts of the support. These are the spaces the Gram–Schmidt process is run on, and the nesting is what makes an adapted orthonormal basis possible.

Each family is indexed by the whole of nonRealPart Z rather than by a choice of one point from each conjugate pair. That is legitimate because gz is conjugation-invariant and hz is conjugation-anti-invariant, so the span is unchanged — and it removes the enumeration z₁, conj z₁, …, z_k, conj z_k that the source has to carry.

@[reducible, inline]

noncomputable abbrev ZetaZeros.L2Interval (lam : ℝ) : AddSubgroup (ℝ →ₘ[MeasureTheory.volume.restrict (Set.Ioo (-lam) lam)] ℂ)

The ambient Hilbert space: square-integrable functions on the interval.

Equations

• ZetaZeros.L2Interval lam = MeasureTheory.Lp ℂ 2 (MeasureTheory.volume.restrict (Set.Ioo (-lam) lam))

noncomputable def ZetaZeros.fzL2 {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z : ℂ) : ↥(L2Interval lam)

The twisted function as an element of L².

Equations

• ZetaZeros.fzL2 h z = MeasureTheory.MemLp.toLp (ZetaZeros.fz eta z) ⋯

noncomputable def ZetaZeros.gzL2 {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z : ℂ) : ↥(L2Interval lam)

The even part as an element of L².

Equations

• ZetaZeros.gzL2 h z = MeasureTheory.MemLp.toLp (ZetaZeros.gz eta z) ⋯

noncomputable def ZetaZeros.hzL2 {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z : ℂ) : ↥(L2Interval lam)

The odd part as an element of L².

Equations

• ZetaZeros.hzL2 h z = MeasureTheory.MemLp.toLp (ZetaZeros.hz eta z) ⋯

noncomputable def ZetaZeros.subspaceU {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) : Submodule ℂ ↥(L2Interval lam)

The first subspace, spanned by the twisted functions at the multiple real points together with the even parts at the non-real points.

Equations

• ZetaZeros.subspaceU h Z m = Submodule.span ℂ (ZetaZeros.fzL2 h '' ↑(ZetaZeros.multipleRealPart Z m) ∪ ZetaZeros.gzL2 h '' ↑(ZetaZeros.nonRealPart Z))

noncomputable def ZetaZeros.subspaceV {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) : Submodule ℂ ↥(L2Interval lam)

The second subspace, adding the twisted functions at the simple real points.

Equations

• ZetaZeros.subspaceV h Z m = Submodule.span ℂ (ZetaZeros.fzL2 h '' ↑(ZetaZeros.simpleRealPart Z m ∪ ZetaZeros.multipleRealPart Z m) ∪ ZetaZeros.gzL2 h '' ↑(ZetaZeros.nonRealPart Z))

noncomputable def ZetaZeros.subspaceW {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) : Submodule ℂ ↥(L2Interval lam)

The third subspace, adding the odd parts at the non-real points.

Equations

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

theorem ZetaZeros.subspaceU_le_subspaceV {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) : subspaceU h Z m ≤ subspaceV h Z m

The subspaces are nested: U ≤ V.

theorem ZetaZeros.subspaceV_le_subspaceW {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (Z : Finset ℂ) (m : ℂ → ℕ) : subspaceV h Z m ≤ subspaceW h Z m

The subspaces are nested: V ≤ W.