Tartar Derivative Bounds

Supporting definitions and lemmas for the Odlyzko-bound formalization.

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

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

Equations

• NumberField.Odlyzko.tartarAmplitudeDerivativeIntegrand x t = -t * NumberField.Odlyzko.Tartar.weight t * Real.sin (x * t)

theorem NumberField.Odlyzko.hasDerivAt_tartarWeight_mul_cos (x t : ℝ) : HasDerivAt (fun (z : ℝ) => Tartar.weight t * Real.cos (z * t)) (tartarAmplitudeDerivativeIntegrand x t) x

theorem NumberField.Odlyzko.abs_mul_tartarWeight_integrable : MeasureTheory.Integrable (fun (t : ℝ) => |t| * Tartar.weight t) MeasureTheory.volume

theorem NumberField.Odlyzko.norm_tartarAmplitudeDerivativeIntegrand_le (x t : ℝ) : ‖tartarAmplitudeDerivativeIntegrand x t‖ ≤ |t| * Tartar.weight t

theorem NumberField.Odlyzko.hasDerivAt_integral_tartarWeight_mul_cos (x : ℝ) : HasDerivAt (fun (z : ℝ) => ∫ (t : ℝ), Tartar.weight t * Real.cos (z * t)) (∫ (t : ℝ), tartarAmplitudeDerivativeIntegrand x t) x

theorem NumberField.Odlyzko.hasDerivAt_tartarAmplitude (x : ℝ) : HasDerivAt Tartar.amplitude (3 / 4 * ∫ (t : ℝ), tartarAmplitudeDerivativeIntegrand x t) x

theorem NumberField.Odlyzko.differentiable_tartarAmplitude : Differentiable ℝ Tartar.amplitude

theorem NumberField.Odlyzko.continuous_integral_tartarAmplitudeDerivativeIntegrand : Continuous fun (x : ℝ) => ∫ (t : ℝ), tartarAmplitudeDerivativeIntegrand x t

theorem NumberField.Odlyzko.deriv_tartarAmplitude (x : ℝ) : deriv Tartar.amplitude x = 3 / 4 * ∫ (t : ℝ), tartarAmplitudeDerivativeIntegrand x t

theorem NumberField.Odlyzko.continuous_deriv_tartarAmplitude : Continuous (deriv Tartar.amplitude)

noncomputable def NumberField.Odlyzko.tartarAmplitudeDerivativeBound : ℝ

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

Equations

• NumberField.Odlyzko.tartarAmplitudeDerivativeBound = 3 / 4 * ∫ (t : ℝ), |t| * NumberField.Odlyzko.Tartar.weight t

theorem NumberField.Odlyzko.tartarAmplitudeDerivativeBound_nonneg : 0 ≤ tartarAmplitudeDerivativeBound

theorem NumberField.Odlyzko.abs_deriv_tartarAmplitude_le (x : ℝ) : |deriv Tartar.amplitude x| ≤ tartarAmplitudeDerivativeBound

theorem NumberField.Odlyzko.hasDerivAt_tartarTestFunction (x : ℝ) : HasDerivAt Tartar.testFunction (2 * Tartar.amplitude x * deriv Tartar.amplitude x) x

theorem NumberField.Odlyzko.deriv_tartarTestFunction (x : ℝ) : deriv Tartar.testFunction x = 2 * Tartar.amplitude x * deriv Tartar.amplitude x

theorem NumberField.Odlyzko.abs_deriv_tartarTestFunction_le (x : ℝ) : |deriv Tartar.testFunction x| ≤ 2 * tartarAmplitudeDerivativeBound

theorem NumberField.Odlyzko.hasDerivAt_scaledTartarTestFunction (y x : ℝ) : HasDerivAt (scaledTartarTestFunction y) (y * deriv Tartar.testFunction (y * x)) x

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

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

Equations

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

theorem NumberField.Odlyzko.hasDerivAt_regularizedScaledTartar (y δ x : ℝ) : HasDerivAt (regularizedScaledTartar y δ) (regularizedScaledTartarDerivative y δ x) x

theorem NumberField.Odlyzko.continuous_regularizedScaledTartarDerivative (y δ : ℝ) : Continuous (regularizedScaledTartarDerivative y δ)

theorem NumberField.Odlyzko.abs_regularizedScaledTartarDerivative_le {δ : ℝ} (hδ : 0 ≤ δ) (y x : ℝ) : |regularizedScaledTartarDerivative y δ x| ≤ (2 * |y| * tartarAmplitudeDerivativeBound + 2 * δ * |x|) * Real.exp (-δ * x ^ 2)