Tartar Poitou Transform

Supporting definitions and lemmas for the Odlyzko-bound formalization.

noncomputable def NumberField.Odlyzko.scaledTartarTestFunction (y x : ℝ) : ℝ

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

Equations

• NumberField.Odlyzko.scaledTartarTestFunction y x = NumberField.Odlyzko.Tartar.testFunction (y * x)

theorem NumberField.Odlyzko.scaledTartarTestFunction_nonneg (y x : ℝ) : 0 ≤ scaledTartarTestFunction y x

theorem NumberField.Odlyzko.scaledTartarTestFunction_even (y x : ℝ) : scaledTartarTestFunction y (-x) = scaledTartarTestFunction y x

theorem NumberField.Odlyzko.scaledTartarTestFunction_integrable {y : ℝ} (hy : y ≠ 0) : MeasureTheory.Integrable (scaledTartarTestFunction y) MeasureTheory.volume

theorem NumberField.Odlyzko.exp_sub_half_mul_div_cosh_le_two {σ x : ℝ} (hσ : σ ∈ Set.Icc 0 1) : Real.exp ((σ - 1 / 2) * x) / Real.cosh (x / 2) ≤ 2

theorem NumberField.Odlyzko.norm_poitouTransformIntegrand_scaledTartar_le {y : ℝ} {s : ℂ} (hs : s.re ∈ Set.Icc 0 1) (x : ℝ) : ‖poitouTransformIntegrand (scaledTartarTestFunction y) s x‖ ≤ 2 * scaledTartarTestFunction y x

theorem NumberField.Odlyzko.continuous_poitouTransformIntegrand_scaledTartar (y : ℝ) (s : ℂ) : Continuous (poitouTransformIntegrand (scaledTartarTestFunction y) s)

theorem NumberField.Odlyzko.poitouTransformIntegrand_scaledTartar_integrable {y : ℝ} (hy : y ≠ 0) {s : ℂ} (hs : s.re ∈ Set.Icc 0 1) : MeasureTheory.Integrable (poitouTransformIntegrand (scaledTartarTestFunction y) s) MeasureTheory.volume

theorem NumberField.Odlyzko.integral_scaledTartarTestFunction {y : ℝ} (hy : 0 < y) : ∫ (x : ℝ), scaledTartarTestFunction y x = 6 * Real.pi / (5 * y)

theorem NumberField.Odlyzko.poitouTransform_scaledTartar_one {y : ℝ} (hy : 0 < y) : poitouTransform (scaledTartarTestFunction y) 1 = ↑(6 * Real.pi / (5 * y))

noncomputable def NumberField.Odlyzko.poitouTransformDerivativeIntegrand (f : ℝ → ℝ) (s : ℂ) (x : ℝ) : ℂ

A poitou transform derivative integrand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.poitouTransformDerivativeIntegrand f s x = ↑x * NumberField.Odlyzko.poitouTransformIntegrand f s x

theorem NumberField.Odlyzko.hasDerivAt_poitouTransformIntegrand (f : ℝ → ℝ) (s : ℂ) (x : ℝ) : HasDerivAt (fun (z : ℂ) => poitouTransformIntegrand f z x) (poitouTransformDerivativeIntegrand f s x) s