Theorems · Theorem · number theory

DirichletCharacter.norm_LFunction_product_ge_one

∀ {N : ℕ} (χ : DirichletCharacter ℂ N) [inst : NeZero N] {x : ℝ},
  0 < x →
    ∀ (y : ℝ),
      ‖DirichletCharacter.LFunctionTrivChar N (1 + ↑x) ^ 3 *
              DirichletCharacter.LFunction χ (1 + ↑x + Complex.I * ↑y) ^ 4 *
            DirichletCharacter.LFunction (χ ^ 2) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥
        1

A variant of DirichletCharacter.norm_LSeries_product_ge_one in terms of the L-functions.

Defined in

Mathlib.NumberTheory.LSeries.Nonvanishing

Cited by

0 results in Mathlib

Foundations

Depth 310 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZero