The twisted functions live in L²((-lam, lam))

The twisted functions and their even and odd parts are square-integrable on the interval, so they are genuine elements of the ambient Hilbert space and Submodule.span may be taken of them.

The bound is the only analytic content. ‖fz eta z u‖ = |eta u| · exp(2π u · im z), and on a bounded interval the exponential is bounded by exp(2π · lam · |im z|), so fz is dominated by a constant multiple of eta, which is square-integrable by admissibility. Note the twist is not bounded by 1 unless z is real — that is exactly why the interval has to be bounded.

Also here: the passage from the rescaled zeros as a Set to the Finset that IsConjInvariant requires.

theorem ZetaZeros.memLp_fz {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z : ℂ) : MeasureTheory.MemLp (fz eta z) 2 (MeasureTheory.volume.restrict (Set.Ioo (-lam) lam))

The twisted function is square-integrable on the interval.

theorem ZetaZeros.memLp_gz {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z : ℂ) : MeasureTheory.MemLp (gz eta z) 2 (MeasureTheory.volume.restrict (Set.Ioo (-lam) lam))

The even part is square-integrable on the interval.

theorem ZetaZeros.memLp_hz {lam : ℝ} {eta : ℝ → ℝ} (h : IsAdmissible lam eta) (z : ℂ) : MeasureTheory.MemLp (hz eta z) 2 (MeasureTheory.volume.restrict (Set.Ioo (-lam) lam))

The odd part is square-integrable on the interval.

From the rescaled zeros as a set to the finite set the propositions need

noncomputable def ZetaZeros.rescaledZerosFinset (T : ℝ) : Finset ℂ

The rescaled zeros as a Finset, which is what IsConjInvariant and the key proposition take. The rescaled zeros are defined as a Set; finiteness of the zero set is what bridges the two.

Equations

• ZetaZeros.rescaledZerosFinset T = Finset.image (ZetaZeros.rescale T) ⋯.toFinset

@[simp]

theorem ZetaZeros.coe_rescaledZerosFinset (T : ℝ) : ↑(rescaledZerosFinset T) = rescaledZeros T