Regularized Poitou Quadratic Decay

Supporting definitions and lemmas for the Odlyzko-bound formalization.

noncomputable def NumberField.Odlyzko.tartarAmplitudeSecondDerivativeIntegrand (x t : ℝ) : ℝ

A tartar amplitude second derivative integrand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.tartarAmplitudeSecondDerivativeIntegrand x t = -t ^ 2 * NumberField.Odlyzko.Tartar.weight t * Real.cos (x * t)

theorem NumberField.Odlyzko.hasDerivAt_tartarAmplitudeDerivativeIntegrand (x t : ℝ) : HasDerivAt (fun (z : ℝ) => tartarAmplitudeDerivativeIntegrand z t) (tartarAmplitudeSecondDerivativeIntegrand x t) x

theorem NumberField.Odlyzko.sq_mul_tartarWeight_integrable : MeasureTheory.Integrable (fun (t : ℝ) => t ^ 2 * Tartar.weight t) MeasureTheory.volume

theorem NumberField.Odlyzko.norm_tartarAmplitudeSecondDerivativeIntegrand_le (x t : ℝ) : ‖tartarAmplitudeSecondDerivativeIntegrand x t‖ ≤ t ^ 2 * Tartar.weight t

theorem NumberField.Odlyzko.hasDerivAt_integral_tartarAmplitudeDerivativeIntegrand (x : ℝ) : HasDerivAt (fun (z : ℝ) => ∫ (t : ℝ), tartarAmplitudeDerivativeIntegrand z t) (∫ (t : ℝ), tartarAmplitudeSecondDerivativeIntegrand x t) x

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

A tartar amplitude second derivative used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.tartarAmplitudeSecondDerivative x = 3 / 4 * ∫ (t : ℝ), NumberField.Odlyzko.tartarAmplitudeSecondDerivativeIntegrand x t

theorem NumberField.Odlyzko.hasDerivAt_deriv_tartarAmplitude (x : ℝ) : HasDerivAt (deriv Tartar.amplitude) (tartarAmplitudeSecondDerivative x) x

theorem NumberField.Odlyzko.abs_tartarAmplitudeSecondDerivative_le (x : ℝ) : |tartarAmplitudeSecondDerivative x| ≤ 3 / 4 * ∫ (t : ℝ), t ^ 2 * Tartar.weight t

noncomputable def NumberField.Odlyzko.tartarTestFunctionSecondDerivativeBound : ℝ

A tartar test function second derivative bound used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.tartarTestFunctionSecondDerivativeBound = 2 * NumberField.Odlyzko.tartarAmplitudeDerivativeBound ^ 2 + 2 * (3 / 4 * ∫ (t : ℝ), t ^ 2 * NumberField.Odlyzko.Tartar.weight t)

theorem NumberField.Odlyzko.tartarTestFunctionSecondDerivativeBound_nonneg : 0 ≤ tartarTestFunctionSecondDerivativeBound

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

A tartar test function second derivative used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.hasDerivAt_deriv_tartarTestFunction (x : ℝ) : HasDerivAt (deriv Tartar.testFunction) (tartarTestFunctionSecondDerivative x) x

theorem NumberField.Odlyzko.abs_tartarTestFunctionSecondDerivative_le (x : ℝ) : |tartarTestFunctionSecondDerivative x| ≤ tartarTestFunctionSecondDerivativeBound

theorem NumberField.Odlyzko.abs_sinh_le_cosh (x : ℝ) : |Real.sinh x| ≤ Real.cosh x

noncomputable def NumberField.Odlyzko.poitouKernelDerivative (f f' : ℝ → ℝ) (x : ℝ) : ℝ

A poitou kernel derivative used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.poitouKernelDerivative f f' x = f' x / Real.cosh (x / 2) - f x * Real.sinh (x / 2) / (2 * Real.cosh (x / 2) ^ 2)

theorem NumberField.Odlyzko.hasDerivAt_poitouKernel {f f' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (x : ℝ) : HasDerivAt (poitouKernel f) (poitouKernelDerivative f f' x) x

theorem NumberField.Odlyzko.abs_poitouKernelDerivative_le (f f' : ℝ → ℝ) (x : ℝ) : |poitouKernelDerivative f f' x| ≤ |f' x| + |f x| / 2

noncomputable def NumberField.Odlyzko.poitouVerticalProfileDerivative (f f' : ℝ → ℝ) (σ x : ℝ) : ℂ

A poitou vertical profile derivative used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.hasDerivAt_poitouVerticalProfile {f f' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (σ x : ℝ) : HasDerivAt (fun (z : ℝ) => ↑(poitouKernel f z) * Complex.exp ((↑σ - 1 / 2) * ↑z)) (poitouVerticalProfileDerivative f f' σ x) x

theorem NumberField.Odlyzko.abs_regularizedScaledTartar_le_gaussian (y δ x : ℝ) : |regularizedScaledTartar y δ x| ≤ Real.exp (-δ * x ^ 2)

theorem NumberField.Odlyzko.abs_poitouKernel_regularizedScaledTartar_le_gaussian (y δ x : ℝ) : |poitouKernel (regularizedScaledTartar y δ) x| ≤ Real.exp (-δ * x ^ 2)

theorem NumberField.Odlyzko.norm_poitouVerticalProfileDerivative_regularized_le {δ : ℝ} (hδ : 0 < δ) (y σ x : ℝ) : ‖poitouVerticalProfileDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) σ x‖ ≤ Real.exp (|σ - 1 / 2| ^ 2 / (2 * δ)) * ((2 * |y| * tartarAmplitudeDerivativeBound + 2 * δ * |x| + 1 / 2 + |σ - 1 / 2|) * Real.exp (-(δ / 2) * x ^ 2))

theorem NumberField.Odlyzko.poitouVerticalProfileDerivative_regularized_integrable {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : MeasureTheory.Integrable (poitouVerticalProfileDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) σ) MeasureTheory.volume

noncomputable def NumberField.Odlyzko.regularizedPoitouVerticalProfile (y δ σ x : ℝ) : ℂ

A regularized poitou vertical profile used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.regularizedPoitouVerticalProfile y δ σ x = ↑(NumberField.Odlyzko.poitouKernel (NumberField.Odlyzko.regularizedScaledTartar y δ) x) * Complex.exp ((↑σ - 1 / 2) * ↑x)

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

theorem NumberField.Odlyzko.poitouTransform_regularizedScaledTartar_eq_fourier (y δ σ t : ℝ) : poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I) = FourierTransform.fourier (regularizedPoitouVerticalProfile y δ σ) (-t / (2 * Real.pi))

theorem NumberField.Odlyzko.differentiable_regularizedPoitouVerticalProfile (y δ σ : ℝ) : Differentiable ℝ (regularizedPoitouVerticalProfile y δ σ)

theorem NumberField.Odlyzko.deriv_regularizedPoitouVerticalProfile (y δ σ x : ℝ) : deriv (regularizedPoitouVerticalProfile y δ σ) x = poitouVerticalProfileDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) σ x

theorem NumberField.Odlyzko.fourier_poitouVerticalProfileDerivative_regularized {δ : ℝ} (hδ : 0 < δ) (y σ w : ℝ) : FourierTransform.fourier (poitouVerticalProfileDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) σ) w = (2 * ↑Real.pi * Complex.I * ↑w) • FourierTransform.fourier (regularizedPoitouVerticalProfile y δ σ) w

noncomputable def NumberField.Odlyzko.poitouKernelSecondDerivative (f f' f'' : ℝ → ℝ) (x : ℝ) : ℝ

A poitou kernel second derivative used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.hasDerivAt_poitouKernelDerivative {f f' f'' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (f'' x) x) (x : ℝ) : HasDerivAt (poitouKernelDerivative f f') (poitouKernelSecondDerivative f f' f'' x) x

theorem NumberField.Odlyzko.abs_poitouKernelSecondDerivative_le (f f' f'' : ℝ → ℝ) (x : ℝ) : |poitouKernelSecondDerivative f f' f'' x| ≤ |f'' x| + |f' x| + 3 * |f x| / 4

noncomputable def NumberField.Odlyzko.poitouVerticalProfileSecondDerivative (f f' f'' : ℝ → ℝ) (σ x : ℝ) : ℂ

A poitou vertical profile second derivative used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.hasDerivAt_poitouVerticalProfileDerivative {f f' f'' : ℝ → ℝ} (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (f'' x) x) (σ x : ℝ) : HasDerivAt (poitouVerticalProfileDerivative f f' σ) (poitouVerticalProfileSecondDerivative f f' f'' σ x) x

noncomputable def NumberField.Odlyzko.regularizedScaledTartarSecondDerivative (y δ x : ℝ) : ℝ

A regularized scaled tartar second derivative used in the Odlyzko-bound argument.

Equations

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

theorem NumberField.Odlyzko.hasDerivAt_regularizedScaledTartarDerivative (y δ x : ℝ) : HasDerivAt (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ x) x

theorem NumberField.Odlyzko.abs_regularizedScaledTartarSecondDerivative_le {δ : ℝ} (hδ : 0 ≤ δ) (y x : ℝ) : |regularizedScaledTartarSecondDerivative y δ x| ≤ (y ^ 2 * tartarTestFunctionSecondDerivativeBound + 2 * δ + 8 * δ * |y| * tartarAmplitudeDerivativeBound * |x| + 4 * δ ^ 2 * x ^ 2) * Real.exp (-δ * x ^ 2)

theorem NumberField.Odlyzko.hasDerivAt_regularizedPoitouVerticalProfileDerivative (y δ σ x : ℝ) : HasDerivAt (poitouVerticalProfileDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) σ) (poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ x) x

theorem NumberField.Odlyzko.differentiable_regularizedPoitouVerticalProfileDerivative (y δ σ : ℝ) : Differentiable ℝ (poitouVerticalProfileDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) σ)

theorem NumberField.Odlyzko.deriv_regularizedPoitouVerticalProfileDerivative (y δ σ x : ℝ) : deriv (poitouVerticalProfileDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) σ) x = poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ x

theorem NumberField.Odlyzko.integrable_quadratic_abs_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) (A B C : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => (A + B * |x| + C * x ^ 2) * Real.exp (-b * x ^ 2)) MeasureTheory.volume

theorem NumberField.Odlyzko.norm_poitouVerticalProfileSecondDerivative_regularized_le {δ : ℝ} (hδ : 0 < δ) (y σ x : ℝ) : ‖poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ x‖ ≤ Real.exp (|σ - 1 / 2| ^ 2 / (2 * δ)) * ((y ^ 2 * tartarTestFunctionSecondDerivativeBound + 2 * δ + 2 * |y| * tartarAmplitudeDerivativeBound + 3 / 4 + 2 * |σ - 1 / 2| * (2 * |y| * tartarAmplitudeDerivativeBound + 1 / 2) + |σ - 1 / 2| ^ 2 + (8 * δ * |y| * tartarAmplitudeDerivativeBound + 2 * δ + 4 * |σ - 1 / 2| * δ) * |x| + 4 * δ ^ 2 * x ^ 2) * Real.exp (-(δ / 2) * x ^ 2))

theorem NumberField.Odlyzko.poitouVerticalProfileSecondDerivative_regularized_integrable {δ : ℝ} (hδ : 0 < δ) (y σ : ℝ) : MeasureTheory.Integrable (poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ) MeasureTheory.volume

theorem NumberField.Odlyzko.fourier_poitouVerticalProfileSecondDerivative_regularized {δ : ℝ} (hδ : 0 < δ) (y σ w : ℝ) : FourierTransform.fourier (poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ) w = (2 * ↑Real.pi * Complex.I * ↑w) • FourierTransform.fourier (poitouVerticalProfileDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) σ) w

theorem NumberField.Odlyzko.fourier_poitouVerticalProfileSecondDerivative_regularized_eq_sq {δ : ℝ} (hδ : 0 < δ) (y σ w : ℝ) : FourierTransform.fourier (poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ) w = (2 * ↑Real.pi * Complex.I * ↑w) ^ 2 • FourierTransform.fourier (regularizedPoitouVerticalProfile y δ σ) w

theorem NumberField.Odlyzko.sq_abs_mul_norm_poitouTransform_regularized_le {δ : ℝ} (hδ : 0 < δ) (y σ t : ℝ) : |t| ^ 2 * ‖poitouTransform (regularizedScaledTartar y δ) (↑σ + ↑t * Complex.I)‖ ≤ ∫ (x : ℝ), ‖poitouVerticalProfileSecondDerivative (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ) (regularizedScaledTartarSecondDerivative y δ) σ x‖