Regularized Prime Power Series Integral

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.norm_fourier_regularizedPoitouVerticalProfile_le_integral {δ : ℝ} (_hδ : 0 < δ) (y σ w : ℝ) : ‖FourierTransform.fourier (regularizedPoitouVerticalProfile y δ σ) w‖ ≤ ∫ (x : ℝ), ‖regularizedPoitouVerticalProfile y δ σ x‖

theorem NumberField.Odlyzko.sq_mul_norm_fourier_regularizedPoitouVerticalProfile_le_integral {δ : ℝ} (hδ : 0 < δ) (y σ w : ℝ) : w ^ 2 * ‖FourierTransform.fourier (regularizedPoitouVerticalProfile y δ σ) w‖ ≤ ∫ (x : ℝ), ‖poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ x‖

theorem NumberField.Odlyzko.fourier_regularizedPoitouVerticalProfile_integrable {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : MeasureTheory.Integrable (FourierTransform.fourier (regularizedPoitouVerticalProfile y δ σ)) MeasureTheory.volume

theorem NumberField.Odlyzko.poitouTransform_regularizedScaledTartar_vertical_integrable {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I)) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_fourier_regularizedPoitouVerticalProfile {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : ∫ (w : ℝ), FourierTransform.fourier (regularizedPoitouVerticalProfile y δ σ) w = regularizedPoitouVerticalProfile y δ σ 0

theorem NumberField.Odlyzko.integral_poitouTransform_regularized_vertical {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) = 2 * ↑Real.pi

theorem NumberField.Odlyzko.integral_fourier_mul_cexp_regularizedPoitouVerticalProfile {δ : ℝ} (hδ : 0 < δ) (y σ a : ℝ) : ∫ (w : ℝ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑w * ↑a) * FourierTransform.fourier (regularizedPoitouVerticalProfile y δ σ) w = regularizedPoitouVerticalProfile y δ σ a

theorem NumberField.Odlyzko.integral_poitouTransform_regularized_mul_exp_neg {δ : ℝ} (hδ : 0 < δ) (y σ a : ℝ) : ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * Complex.exp (-↑a * (↑σ + ↑t * Complex.I)) = 2 * ↑Real.pi * ↑(poitouKernel (regularizedScaledTartar y δ) a) * Complex.exp (-↑a / 2)

noncomputable def NumberField.Odlyzko.primePowerLocation (K : Type u_1) [Field K] [NumberField K] (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (e : ℕ) : ℝ

A prime power location used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.primePowerLocation K P e = ↑(e + 1) * Real.log ↑(NumberField.Odlyzko.primeIdealNorm K P)

noncomputable def NumberField.Odlyzko.regularizedPrimePowerPoitouWeight (K : Type u_1) [Field K] [NumberField K] (y δ : ℝ) (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (e : ℕ) : ℝ

A regularized prime power poitou weight used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.regularizedPrimePowerPoitouWeight_nonneg (K : Type u_1) [Field K] [NumberField K] (y δ : ℝ) (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (e : ℕ) : 0 ≤ regularizedPrimePowerPoitouWeight K y δ P e

theorem NumberField.Odlyzko.integral_poitouTransform_regularized_mul_primePowerLogTerm (K : Type u_1) [Field K] [NumberField K] {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) (P : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (e : ℕ) : ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * primePowerLogTerm K P e (↑σ + ↑t * Complex.I) = ↑(2 * Real.pi * regularizedPrimePowerPoitouWeight K y δ P e)

theorem NumberField.Odlyzko.hasSum_integral_poitouTransform_regularized_mul_primePowerLogTerm (K : Type u_1) [Field K] [NumberField K] {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 1 < σ) : HasSum (fun (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ) => ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * primePowerLogTerm K pe.1 pe.2 (↑σ + ↑t * Complex.I)) (∫ (t : ℝ), ∑' (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * primePowerLogTerm K pe.1 pe.2 (↑σ + ↑t * Complex.I))

theorem NumberField.Odlyzko.integral_poitouTransform_regularized_mul_neg_logDeriv_dedekindZeta_eq_tsum (K : Type u_1) [Field K] [NumberField K] {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 1 < σ) : ∫ (t : ℝ), poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) * -logDeriv (dedekindZeta K) (↑σ + ↑t * Complex.I) = ∑' (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ), ↑(2 * Real.pi * regularizedPrimePowerPoitouWeight K y δ pe.1 pe.2)

theorem NumberField.Odlyzko.summable_regularizedPrimePowerPoitouWeight (K : Type u_1) [Field K] [NumberField K] {δ : ℝ} (hδ : 0 < δ) (y : ℝ) {σ : ℝ} (hσ : 1 < σ) : Summable fun (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ) => regularizedPrimePowerPoitouWeight K y δ pe.1 pe.2

theorem NumberField.Odlyzko.tsum_regularizedPrimePowerPoitouWeight_nonneg (K : Type u_1) [Field K] [NumberField K] (y δ : ℝ) : 0 ≤ ∑' (pe : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) × ℕ), regularizedPrimePowerPoitouWeight K y δ pe.1 pe.2