Documentation

MathlibNt.AnalyticNumberTheory.DirichletL.DirichletLGlobalConductorLogValueBound

A logarithmic conductor-height bound for nonprincipal Dirichlet L-values #

The natural-order conditional series is cut at q * (⌊|t|⌋₊ + 1). The finite part is bounded by a harmonic sum, while the factor q / m in the Abel tail pays for the height of s.

source
noncomputable def DirichletLGlobalConductorLogValueBound.dirichletLHeightBlock (t : ℝ) :
ℕ

The integral block which strictly dominates the analytic height.

Equations
Instances For
    Inspect dependencies

    DirichletLGlobalConductorLogValueBound.dirichletLHeightBlock · compiled type and proof/definition references.

    source
    noncomputable def DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff (q : ℕ) (t : ℝ) :
    ℕ

    The natural conductor-height truncation point.

    Equations
    Instances For
      Inspect dependencies

      DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff · compiled type and proof/definition references.

      source
      theorem DirichletLGlobalConductorLogValueBound.two_le_modulus_of_ne_one {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) :
      2 ≤ q

      A nonprincipal character cannot have modulus zero or one.

      Inspect dependencies

      DirichletLGlobalConductorLogValueBound.two_le_modulus_of_ne_one · compiled type and proof/definition references.

      source
      theorem DirichletLGlobalConductorLogValueBound.abs_lt_heightBlock (t : ℝ) :
      |t| < ↑(dirichletLHeightBlock t)
      Inspect dependencies

      DirichletLGlobalConductorLogValueBound.abs_lt_heightBlock · compiled type and proof/definition references.

      source
      theorem DirichletLGlobalConductorLogValueBound.one_le_heightBlock (t : ℝ) :
      1 ≤ dirichletLHeightBlock t
      Inspect dependencies

      DirichletLGlobalConductorLogValueBound.one_le_heightBlock · compiled type and proof/definition references.

      source
      theorem DirichletLGlobalConductorLogValueBound.two_le_conductorHeightCutoff {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (t : ℝ) :
      2 ≤ dirichletLConductorHeightCutoff q t
      Inspect dependencies

      DirichletLGlobalConductorLogValueBound.two_le_conductorHeightCutoff · compiled type and proof/definition references.

      source
      theorem DirichletLGlobalConductorLogValueBound.log_conductorHeightCutoff_pos {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (t : ℝ) :
      0 < Real.log ↑(dirichletLConductorHeightCutoff q t)
      Inspect dependencies

      DirichletLGlobalConductorLogValueBound.log_conductorHeightCutoff_pos · compiled type and proof/definition references.

      source
      theorem DirichletLGlobalConductorLogValueBound.rpow_one_sub_le_exp_one {m k : ℕ} {σ : ℝ} (hm : 2 ≤ m) (hk1 : 1 ≤ k) (hkm : k ≤ m) (hnear : 1 - 1 / Real.log ↑m ≤ σ) :
      ↑k ^ (1 - σ) ≤ Real.exp 1

      Natural powers near the line σ = 1 are bounded by exp 1 up to the cutoff.

      Inspect dependencies

      DirichletLGlobalConductorLogValueBound.rpow_one_sub_le_exp_one · compiled type and proof/definition references.

      source
      theorem DirichletLGlobalConductorLogValueBound.norm_LFunction_le_thirtytwo_mul_one_add_log_conductorHeightCutoff {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {σ t : ℝ} (hσlower : 1 / 2 ≤ σ) (hσupper : σ ≤ 2) (hnear : 1 - 1 / Real.log ↑(dirichletLConductorHeightCutoff q t) ≤ σ) :
      ‖DirichletCharacter.LFunction χ (↑σ + Complex.I * ↑t)‖ ≤ 32 * (1 + Real.log ↑(dirichletLConductorHeightCutoff q t))

      Sharp logarithmic growth in the conductor-height cutoff throughout the near-one strip.

      Inspect dependencies

      DirichletLGlobalConductorLogValueBound.norm_LFunction_le_thirtytwo_mul_one_add_log_conductorHeightCutoff · compiled type and proof/definition references.