Regularized Tartar

Supporting definitions and lemmas for the Odlyzko-bound formalization.

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

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

Equations

• NumberField.Odlyzko.regularizedScaledTartar y δ x = NumberField.Odlyzko.scaledTartarTestFunction y x * Real.exp (-δ * x ^ 2)

@[simp]

theorem NumberField.Odlyzko.regularizedScaledTartar_zero (y δ : ℝ) : regularizedScaledTartar y δ 0 = 1

theorem NumberField.Odlyzko.regularizedScaledTartar_even (y δ x : ℝ) : regularizedScaledTartar y δ (-x) = regularizedScaledTartar y δ x

theorem NumberField.Odlyzko.regularizedScaledTartar_nonneg (y δ x : ℝ) : 0 ≤ regularizedScaledTartar y δ x

theorem NumberField.Odlyzko.regularizedScaledTartar_le_scaledTartar {y δ x : ℝ} (hδ : 0 ≤ δ) : regularizedScaledTartar y δ x ≤ scaledTartarTestFunction y x

theorem NumberField.Odlyzko.regularizedScaledTartar_le_one {y δ x : ℝ} (hδ : 0 ≤ δ) : regularizedScaledTartar y δ x ≤ 1

theorem NumberField.Odlyzko.tendsto_regularizedScaledTartar_nhds_zero (y x : ℝ) : Filter.Tendsto (fun (δ : ℝ) => regularizedScaledTartar y δ x) (nhds 0) (nhds (scaledTartarTestFunction y x))