noncomputable def Frourio.Kzeta [ZetaLineAPI] (τ : ℝ) : ℝ

Zeta kernel on the critical line: Kζ(τ) = ‖ζ(1/2 + iτ)‖².

Equations

• Frourio.Kzeta τ = ‖Frourio.ZetaLineAPI.zeta_on_line τ‖ ^ 2

theorem Frourio.measurable_Kzeta [ZetaLineAPI] : Measurable Kzeta

theorem Frourio.Kzeta_nonneg [ZetaLineAPI] (τ : ℝ) : 0 ≤ Kzeta τ

noncomputable def Frourio.Qζℝ [ZetaLineAPI] (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ℝ

Continuous quadratic form with the zeta kernel on L²(ℝ).

Equations

• Frourio.Qζℝ g = Frourio.Qℝ (fun (τ : ℝ) => Frourio.Kzeta τ) g

noncomputable def Frourio.Qζσ [ZetaLineAPI] (σ : ℝ) (f : ↥(Hσ σ)) : ℝ

Pullback to Hσ: zeta-kernel quadratic form on Hσ via Uσ.

Equations

• Frourio.Qζσ σ f = Qσ[fun (τ : ℝ) => Frourio.Kzeta τ] f

theorem Frourio.Qζ_pos [ZetaLineAPI] (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : 0 ≤ Qζℝ g

Positivity: Qζℝ ≥ 0.

theorem Frourio.Qζσ_pos [ZetaLineAPI] (σ : ℝ) (f : ↥(Hσ σ)) : 0 ≤ Qζσ σ f

Positivity on Hσ: Qζσ ≥ 0.

def Frourio.Qζ_kernelPred [ZetaLineAPI] (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Prop

Kernel predicate for Qζ on L²: vanishing a.e. on the support of Kζ (design-level).

Equations

• Frourio.Qζ_kernelPred g = (↑↑g =ᵐ[MeasureTheory.volume.restrict (Frourio.supp_K fun (τ : ℝ) => ↑(Frourio.Kzeta τ))] 0)

theorem Frourio.Qζ_eq_zero_of_ae_zero [ZetaLineAPI] (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑g =ᵐ[MeasureTheory.volume] 0 → Qζℝ g = 0

Trivial direction used in this phase: if g = 0 a.e. (globally), then Qζℝ g = 0.