Regularized Tartar Transform

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.mul_abs_le_half_mul_sq_add_sq_div {δ : ℝ} (hδ : 0 < δ) (a x : ℝ) : a * |x| ≤ δ / 2 * x ^ 2 + a ^ 2 / (2 * δ)

theorem NumberField.Odlyzko.exp_neg_mul_sq_add_mul_le {δ : ℝ} (hδ : 0 < δ) (a x : ℝ) : Real.exp (-δ * x ^ 2 + a * |x|) ≤ Real.exp (a ^ 2 / (2 * δ)) * Real.exp (-(δ / 2) * x ^ 2)

theorem NumberField.Odlyzko.continuous_regularizedScaledTartar (y δ : ℝ) : Continuous (regularizedScaledTartar y δ)

theorem NumberField.Odlyzko.continuous_poitouTransformIntegrand_regularizedScaledTartar (y δ : ℝ) (s : ℂ) : Continuous (poitouTransformIntegrand (regularizedScaledTartar y δ) s)

theorem NumberField.Odlyzko.norm_poitouTransformIntegrand_regularizedScaledTartar_le {y δ : ℝ} (hδ : 0 < δ) (s : ℂ) (x : ℝ) : ‖poitouTransformIntegrand (regularizedScaledTartar y δ) s x‖ ≤ Real.exp (|s.re - 1 / 2| ^ 2 / (2 * δ)) * Real.exp (-(δ / 2) * x ^ 2)

theorem NumberField.Odlyzko.poitouTransformIntegrand_regularizedScaledTartar_integrable {y δ : ℝ} (hδ : 0 < δ) (s : ℂ) : MeasureTheory.Integrable (poitouTransformIntegrand (regularizedScaledTartar y δ) s) MeasureTheory.volume

theorem NumberField.Odlyzko.norm_poitouTransformDerivativeIntegrand_regularizedScaledTartar_le {y δ : ℝ} (hδ : 0 < δ) (s : ℂ) (x : ℝ) : ‖poitouTransformDerivativeIntegrand (regularizedScaledTartar y δ) s x‖ ≤ Real.exp (|s.re - 1 / 2| ^ 2 / (2 * δ)) * (|x| * Real.exp (-(δ / 2) * x ^ 2))

theorem NumberField.Odlyzko.hasDerivAt_poitouTransform_regularizedScaledTartar {y δ : ℝ} (hδ : 0 < δ) (s : ℂ) : HasDerivAt (poitouTransform (regularizedScaledTartar y δ)) (∫ (x : ℝ), poitouTransformDerivativeIntegrand (regularizedScaledTartar y δ) s x) s

theorem NumberField.Odlyzko.analyticOnNhd_poitouTransform_regularizedScaledTartar {y δ : ℝ} (hδ : 0 < δ) : AnalyticOnNhd ℂ (poitouTransform (regularizedScaledTartar y δ)) Set.univ