Documentation

Project.EasyCase

Lemma 2: non-vanishing for t ≠ 0 or χ² ≠ 1 #

source
theorem continuous_cpow_natCast_neg (n : ℕ) [NeZero n] :
Continuous fun (s : ℂ) => ↑n ^ (-s)
source
@[reducible, inline]
noncomputable abbrev DirichletCharacter.LFunction_one (N : ℕ) [NeZero N] (s : ℂ) :
ℂ
Equations
Instances For
    source
    theorem DirichletCharacter.LSeries_changeLevel {M : ℕ} {N : ℕ} [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : 1 < s.re) :
    LSeries (fun (n : ℕ) => ((DirichletCharacter.changeLevel hMN) χ) ↑n) s = LSeries (fun (n : ℕ) => χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

    If χ is a Dirichlet character and its level M divides N, then we obtain the L-series of χ considered as a Dirichlet character of level N from the L-series of χ by multiplying with ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s)).

    source
    theorem DirichletCharacter.LFunction_changeLevel_aux {M : ℕ} {N : ℕ} [NeZero M] [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : s ≠ 1) :
    ((DirichletCharacter.changeLevel hMN) χ).LFunction s = χ.LFunction s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
    source
    theorem DirichletCharacter.LFunction_changeLevel {M : ℕ} {N : ℕ} [NeZero M] [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (h : χ ≠ 1 ∨ s ≠ 1) :
    ((DirichletCharacter.changeLevel hMN) χ).LFunction s = χ.LFunction s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

    If χ is a Dirichlet character and its level M divides N, then we obtain the L function of χ considered as a Dirichlet character of level N from the L function of χ by multiplying with ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s)).

    source
    theorem DirichletCharacter.LFunction_one_eq_mul_riemannZeta {N : ℕ} [NeZero N] {s : ℂ} (hs : s ≠ 1) :
    DirichletCharacter.LFunction_one N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * riemannZeta s

    The L function of the trivial Dirichlet character mod N is obtained from the Riemann zeta function by multiplying with ∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s)).

    source
    theorem DirichletCharacter.LFunction_one_residue_one {N : ℕ} [NeZero N] :
    Filter.Tendsto (fun (s : ℂ) => (s - 1) * DirichletCharacter.LFunction_one N s) (nhdsWithin 1 {1}ᶜ) (nhds (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

    The L function of the trivial Dirichlet character mod N has a simple pole with residue ∏ p ∈ N.primeFactors, (1 - p⁻¹) at s = 1.

    source
    theorem DirichletCharacter.norm_LFunction_product_ge_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} {x : ℝ} (hx : 0 < x) (y : ℝ) :
    ‖DirichletCharacter.LFunction_one N (1 + ↑x) ^ 3 * χ.LFunction (1 + ↑x + Complex.I * ↑y) ^ 4 * (χ ^ 2).LFunction (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥ 1

    A variant of norm_dirichlet_product_ge_one in terms of the L functions.

    source
    theorem DirichletCharacter.LFunction_one_isBigO_near_one_horizontal {N : ℕ} [NeZero N] :
    (fun (x : ℝ) => DirichletCharacter.LFunction_one N (1 + ↑x)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1 / ↑x
    source
    theorem DirichletCharacter.LFunction_isBigO_of_ne_one_horizontal {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1) :
    (fun (x : ℝ) => χ.LFunction (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => 1
    source
    theorem DirichletCharacter.LFunction_isBigO_near_root_horizontal {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1) (h : χ.LFunction (1 + Complex.I * ↑y) = 0) :
    (fun (x : ℝ) => χ.LFunction (1 + ↑x + Complex.I * ↑y)) =O[nhdsWithin 0 (Set.Ioi 0)] fun (x : ℝ) => ↑x
    source
    theorem mainTheorem_general {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} {t : ℝ} (h : χ ^ 2 ≠ 1 ∨ t ≠ 0) :
    χ.LFunction (1 + Complex.I * ↑t) ≠ 0

    The L function of a Dirichlet character χ does not vanish at 1 + I*t if t ≠ 0 or χ^2 ≠ 1.