Poitou Transform

Supporting definitions and lemmas for the Odlyzko-bound formalization.

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

A poitou kernel used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.poitouKernel f x = f x / Real.cosh (x / 2)

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

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

Equations

• NumberField.Odlyzko.poitouTransformIntegrand f s x = ↑(NumberField.Odlyzko.poitouKernel f x) * Complex.exp ((s - 1 / 2) * ↑x)

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

A poitou transform used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.poitouTransform f s = ∫ (x : ℝ), NumberField.Odlyzko.poitouTransformIntegrand f s x

theorem NumberField.Odlyzko.poitouKernel_neg {f : ℝ → ℝ} (hf : ∀ (x : ℝ), f (-x) = f x) (x : ℝ) : poitouKernel f (-x) = poitouKernel f x

theorem NumberField.Odlyzko.poitouTransform_one_sub {f : ℝ → ℝ} (hf : ∀ (x : ℝ), f (-x) = f x) (s : ℂ) : poitouTransform f (1 - s) = poitouTransform f s

theorem NumberField.Odlyzko.poitouTransform_reflection {f : ℝ → ℝ} (hf : ∀ (x : ℝ), f (-x) = f x) (s : ℂ) : poitouTransform f s = poitouTransform f (1 - s)

theorem NumberField.Odlyzko.re_poitouTransform_mul_I_eq_cosineTransform {f : ℝ → ℝ} (hf : ∀ (x : ℝ), f (-x) = f x) (t : ℝ) (hint : MeasureTheory.Integrable (poitouTransformIntegrand f (↑t * Complex.I)) MeasureTheory.volume) : (poitouTransform f (↑t * Complex.I)).re = Poitou.cosineTransform f t

theorem NumberField.Odlyzko.re_poitouTransform_mul_I_nonneg {f : ℝ → ℝ} (hf : Poitou.Admissible f) (t : ℝ) (hint : MeasureTheory.Integrable (poitouTransformIntegrand f (↑t * Complex.I)) MeasureTheory.volume) : 0 ≤ (poitouTransform f (↑t * Complex.I)).re

theorem NumberField.Odlyzko.re_poitouTransform_one_add_mul_I_nonneg {f : ℝ → ℝ} (hf : Poitou.Admissible f) (t : ℝ) (hint : MeasureTheory.Integrable (poitouTransformIntegrand f (↑(-t) * Complex.I)) MeasureTheory.volume) : 0 ≤ (poitouTransform f (1 + ↑t * Complex.I)).re

theorem NumberField.Odlyzko.poitouTransform_one_eq_integral {f : ℝ → ℝ} (hf : ∀ (x : ℝ), f (-x) = f x) (hint : MeasureTheory.Integrable (poitouTransformIntegrand f 0) MeasureTheory.volume) : poitouTransform f 1 = ↑(∫ (x : ℝ), f x)