Documentation

LeanPool.Odlyzko.CompletedZeta.VerticalLowerBound

Vertical Lower Bound #

Supporting definitions and lemmas for the Odlyzko-bound formalization.

source
noncomputable def NumberField.Odlyzko.dedekindZetaInverseVerticalMajorant (K : Type u_1) [Field K] [NumberField K] :
ℝ

A dedekind zeta inverse vertical majorant used in the Odlyzko-bound argument.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem NumberField.Odlyzko.one_le_dedekindZetaInverseVerticalMajorant (K : Type u_1) [Field K] [NumberField K] :
    1 ≤ dedekindZetaInverseVerticalMajorant K
    source
    theorem NumberField.Odlyzko.norm_inv_dedekindZeta_two_add_mul_I_le (K : Type u_1) [Field K] [NumberField K] (t : ℝ) :
    ‖(dedekindZeta K (2 + ↑t * Complex.I))⁻¹‖ ≤ dedekindZetaInverseVerticalMajorant K
    source
    theorem NumberField.Odlyzko.one_le_dedekindZetaInverseVerticalMajorant_mul_norm (K : Type u_1) [Field K] [NumberField K] (t : ℝ) :
    1 ≤ dedekindZetaInverseVerticalMajorant K * ‖dedekindZeta K (2 + ↑t * Complex.I)‖
    source
    theorem NumberField.Odlyzko.Gamma_one_add_mul_I_mul_Gamma_one_sub_mul_I {t : ℝ} (ht : t ≠ 0) :
    Complex.Gamma (1 + ↑t * Complex.I) * Complex.Gamma (1 - ↑t * Complex.I) = ↑(Real.pi * t / Real.sinh (Real.pi * t))
    source
    theorem NumberField.Odlyzko.sq_norm_Gamma_one_add_mul_I {t : ℝ} (ht : t ≠ 0) :
    ‖Complex.Gamma (1 + ↑t * Complex.I)‖ ^ 2 = Real.pi * |t| / Real.sinh (Real.pi * |t|)
    source
    theorem NumberField.Odlyzko.sq_norm_Gamma_two_add_mul_I {t : ℝ} (ht : t ≠ 0) :
    ‖Complex.Gamma (2 + ↑t * Complex.I)‖ ^ 2 = (1 + t ^ 2) * (Real.pi * |t| / Real.sinh (Real.pi * |t|))
    source
    theorem NumberField.Odlyzko.two_mul_pi_mul_abs_mul_exp_neg_le_sq_norm_Gamma_one_add_mul_I {t : ℝ} (ht : t ≠ 0) :
    2 * Real.pi * |t| * Real.exp (-(Real.pi * |t|)) ≤ ‖Complex.Gamma (1 + ↑t * Complex.I)‖ ^ 2
    source
    theorem NumberField.Odlyzko.sq_norm_complexPlaceGammaFactor_two_add_mul_I {t : ℝ} (ht : t ≠ 0) :
    ‖CompletedZeta.complexPlaceGammaFactor (2 + ↑t * Complex.I)‖ ^ 2 = (2 * Real.pi) ^ (-4) * (1 + t ^ 2) * (Real.pi * |t| / Real.sinh (Real.pi * |t|))
    source
    theorem NumberField.Odlyzko.complexPlaceGammaFactor_two_vertical_sq_lowerBound {t : ℝ} (ht : t ≠ 0) :
    (2 * Real.pi) ^ (-4) * (1 + t ^ 2) * (2 * Real.pi * |t| * Real.exp (-(Real.pi * |t|))) ≤ ‖CompletedZeta.complexPlaceGammaFactor (2 + ↑t * Complex.I)‖ ^ 2
    source
    noncomputable def NumberField.Odlyzko.complexPlaceGammaVerticalLowerConstant :
    ℝ

    A complex place gamma vertical lower constant used in the Odlyzko-bound argument.

    Equations
    Instances For
      source
      theorem NumberField.Odlyzko.complexPlaceGammaVerticalLowerConstant_pos :
      0 < complexPlaceGammaVerticalLowerConstant
      source
      theorem NumberField.Odlyzko.complexPlaceGammaVerticalLowerConstant_mul_exp_le_sq_norm {t : ℝ} (ht : 1 ≤ |t|) :
      complexPlaceGammaVerticalLowerConstant * Real.exp (-(Real.pi * |t|)) ≤ ‖CompletedZeta.complexPlaceGammaFactor (2 + ↑t * Complex.I)‖ ^ 2
      source
      theorem NumberField.Odlyzko.norm_poleClearedCompletedDedekindZetaContinuation_two_add_mul_I (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (t : ℝ) :
      ‖poleClearedCompletedDedekindZetaContinuation K (2 + ↑t * Complex.I)‖ = ↑(Module.finrank ℚ K) * ‖2 + ↑t * Complex.I‖ * ‖1 - (2 + ↑t * Complex.I)‖ * |↑(discr K)| * ‖CompletedZeta.complexPlaceGammaFactor (2 + ↑t * Complex.I)‖ ^ InfinitePlace.nrComplexPlaces K * ‖dedekindZeta K (2 + ↑t * Complex.I)‖
      source
      theorem NumberField.Odlyzko.completedZeta_two_vertical_factor_le_majorant_mul_norm (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] (t : ℝ) :
      ↑(Module.finrank ℚ K) * ‖2 + ↑t * Complex.I‖ * ‖1 - (2 + ↑t * Complex.I)‖ * |↑(discr K)| * ‖CompletedZeta.complexPlaceGammaFactor (2 + ↑t * Complex.I)‖ ^ InfinitePlace.nrComplexPlaces K ≤ dedekindZetaInverseVerticalMajorant K * ‖poleClearedCompletedDedekindZetaContinuation K (2 + ↑t * Complex.I)‖
      source
      theorem NumberField.Odlyzko.complexGammaExponential_pow_le_majorant_sq_mul_completedZeta_sq (K : Type u_1) [Field K] [NumberField K] [IsTotallyComplex K] {t : ℝ} (ht : 1 ≤ |t|) :
      (complexPlaceGammaVerticalLowerConstant * Real.exp (-(Real.pi * |t|))) ^ InfinitePlace.nrComplexPlaces K ≤ dedekindZetaInverseVerticalMajorant K ^ 2 * ‖poleClearedCompletedDedekindZetaContinuation K (2 + ↑t * Complex.I)‖ ^ 2