Documentation

MathlibNt.AnalyticNumberTheory.DirichletL.DirichletLActualCompletedArchimedeanBridge

The actual symmetrically completed Dirichlet L-function #

This module removes the abstract hgammaBridge input from the Tatuzawa zero contribution layer. Mathlib's DirichletCharacter.completedLFunction contains the Deligne gamma factor but not the symmetric conductor factor. We therefore adjoin q ^ (s / 2) and prove its exact logarithmic-derivative identity.

source
noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.symmetricCompletedLFunction {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (s : ℂ) :
ℂ

The standard symmetric completion q^(s/2) Γℝ(s+a) L(s,χ), using Mathlib's completed L-function.

Equations
Instances For
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.symmetricCompletedLFunction · compiled type and proof/definition references.

    source
    noncomputable def AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.conductorGammaTerm {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (s : ℂ) :
    ℂ

    Its explicit conductor/gamma logarithmic derivative.

    Equations
    Instances For
      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.conductorGammaTerm · compiled type and proof/definition references.

      source
      theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.differentiable_symmetricCompletedLFunction {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ ≠ 1) :
      Differentiable ℂ (symmetricCompletedLFunction χ)
      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.differentiable_symmetricCompletedLFunction · compiled type and proof/definition references.

      source
      theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.gammaFactor_ne_zero_of_pos {q : ℕ} (χ : DirichletCharacter ℂ q) {σ : ℝ} (hσ : 0 < σ) :
      χ.gammaFactor ↑σ ≠ 0
      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.gammaFactor_ne_zero_of_pos · compiled type and proof/definition references.

      source
      theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.differentiableAt_gammaFactor_of_pos {q : ℕ} (χ : DirichletCharacter ℂ q) {σ : ℝ} (hσ : 0 < σ) :
      DifferentiableAt ℂ χ.gammaFactor ↑σ
      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.differentiableAt_gammaFactor_of_pos · compiled type and proof/definition references.

      source
      theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.logDeriv_conductorFactor {q : ℕ} [NeZero q] (σ : ℂ) :
      logDeriv (fun (s : ℂ) => ↑q ^ (s / 2)) σ = Complex.log ↑q / 2
      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.logDeriv_conductorFactor · compiled type and proof/definition references.

      source
      theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.negLogDerivative_eq_conductorGamma_sub_completed {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {σ : ℝ} (hσ : 0 < σ) (hL : DirichletCharacter.LFunction χ ↑σ ≠ 0) :
      -logDeriv (DirichletCharacter.LFunction χ) ↑σ = conductorGammaTerm χ ↑σ - logDeriv (symmetricCompletedLFunction χ) ↑σ

      Exact character-specific archimedean bridge. Unlike the former abstract hgammaBridge, every function here is the actual Dirichlet L-function, its actual symmetric completion, or the explicit conductor/gamma term.

      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.negLogDerivative_eq_conductorGamma_sub_completed · compiled type and proof/definition references.

      source
      theorem AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.negLogDerivative_re_eq_conductorGamma_sub_completed {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {σ : ℝ} (hσ : 0 < σ) (hL : DirichletCharacter.LFunction χ ↑σ ≠ 0) :
      (-deriv (DirichletCharacter.LFunction χ) ↑σ / DirichletCharacter.LFunction χ ↑σ).re = (conductorGammaTerm χ ↑σ).re - (deriv (symmetricCompletedLFunction χ) ↑σ / symmetricCompletedLFunction χ ↑σ).re

      Real-part form used on the real strip in zero-repulsion arguments.

      Inspect dependencies

      AnalyticNumberTheory.LargeSieve.TatuzawaZeroContribution.negLogDerivative_re_eq_conductorGamma_sub_completed · compiled type and proof/definition references.