TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.Poitou.cosineTransform (f : ℝ → ℝ) (t : ℝ) : ℝ

A cosine transform used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.Poitou.cosineTransform f t = ∫ (x : ℝ), f x * Real.cos (t * x)

structure NumberField.Odlyzko.Poitou.Admissible (f : ℝ → ℝ) : Prop

Conditions on a test function used in Poitou's explicit formula.

• continuous : Continuous f
• even (x : ℝ) : f (-x) = f x
• value_zero : f 0 = 1
• nonnegative (x : ℝ) : 0 ≤ f x
• integrable : MeasureTheory.Integrable f MeasureTheory.volume
• cosineTransform_nonnegative (t : ℝ) : 0 ≤ cosineTransform f t

theorem NumberField.Odlyzko.tendsto_sin_sub_mul_cos_div_pow_three : Filter.Tendsto (fun (x : ℝ) => (Real.sin x - x * Real.cos x) / x ^ 3) (nhdsWithin 0 {0}ᶜ) (nhds (1 / 3))

theorem NumberField.Odlyzko.tendsto_tartarAmplitude_punctured_zero : Filter.Tendsto Tartar.amplitude (nhdsWithin 0 {0}ᶜ) (nhds 1)

theorem NumberField.Odlyzko.tartarAmplitude_continuousAt_zero : ContinuousAt Tartar.amplitude 0

theorem NumberField.Odlyzko.tartarAmplitude_continuous : Continuous Tartar.amplitude

theorem NumberField.Odlyzko.tartarTestFunction_continuous : Continuous Tartar.testFunction

noncomputable def NumberField.Odlyzko.complexTartarWeight (x : ℝ) : ℂ

A complex tartar weight used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.complexTartarWeight x = ↑(NumberField.Odlyzko.Tartar.weight x)

theorem NumberField.Odlyzko.complexTartarWeight_integrable : MeasureTheory.Integrable complexTartarWeight MeasureTheory.volume

theorem NumberField.Odlyzko.integral_tartarWeight_mul_sin (a : ℝ) : ∫ (x : ℝ), Tartar.weight x * Real.sin (a * x) = 0

theorem NumberField.Odlyzko.fourier_complexTartarWeight (ξ : ℝ) : FourierTransform.fourier complexTartarWeight ξ = ↑(4 / 3) * ↑(Tartar.amplitude (2 * Real.pi * ξ))

noncomputable def NumberField.Odlyzko.tartarWeightConvolution (x : ℝ) : ℝ

A tartar weight convolution used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.tartarWeightConvolution x = ∫ (t : ℝ), NumberField.Odlyzko.Tartar.weight t * NumberField.Odlyzko.Tartar.weight (x - t)

theorem NumberField.Odlyzko.tartarWeightConvolution_nonneg (x : ℝ) : 0 ≤ tartarWeightConvolution x

theorem NumberField.Odlyzko.complexTartarWeight_convolution_eq (x : ℝ) : MeasureTheory.convolution complexTartarWeight complexTartarWeight (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume x = ↑(tartarWeightConvolution x)

theorem NumberField.Odlyzko.complexTartarWeight_convolution_integrable : MeasureTheory.Integrable (MeasureTheory.convolution complexTartarWeight complexTartarWeight (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume) MeasureTheory.volume

theorem NumberField.Odlyzko.complexTartarWeight_convolution_continuous : Continuous (MeasureTheory.convolution complexTartarWeight complexTartarWeight (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume)

theorem NumberField.Odlyzko.fourier_complexTartarWeight_convolution (ξ : ℝ) : FourierTransform.fourier (MeasureTheory.convolution complexTartarWeight complexTartarWeight (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume) ξ = ↑(16 / 9) * ↑(Tartar.testFunction (2 * Real.pi * ξ))

theorem NumberField.Odlyzko.fourier_complexTartarWeight_convolution_integrable : MeasureTheory.Integrable (FourierTransform.fourier (MeasureTheory.convolution complexTartarWeight complexTartarWeight (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume)) MeasureTheory.volume

theorem NumberField.Odlyzko.fourierInv_fourier_complexTartarWeight_convolution : FourierTransformInv.fourierInv (FourierTransform.fourier (MeasureTheory.convolution complexTartarWeight complexTartarWeight (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume)) = MeasureTheory.convolution complexTartarWeight complexTartarWeight (ContinuousLinearMap.mul ℂ ℂ) MeasureTheory.volume

theorem NumberField.Odlyzko.cosineTransform_tartarTestFunction (t : ℝ) : Poitou.cosineTransform Tartar.testFunction t = 9 * Real.pi / 8 * tartarWeightConvolution t

theorem NumberField.Odlyzko.integral_tartarWeight_sq : ∫ (x : ℝ), Tartar.weight x ^ 2 = 16 / 15

@[simp]

theorem NumberField.Odlyzko.tartarWeightConvolution_zero : tartarWeightConvolution 0 = 16 / 15

theorem NumberField.Odlyzko.integral_tartarTestFunction : ∫ (x : ℝ), Tartar.testFunction x = 6 * Real.pi / 5