Theorems · Theorem · number theory

DirichletCharacter.norm_LSeries_product_ge_one

∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {x : ℝ},
  0 < x →
    ∀ (y : ℝ),
      ‖LSeries (fun n => 1 ↑n) (1 + ↑x) ^ 3 * LSeries (fun n => χ ↑n) (1 + ↑x + Complex.I * ↑y) ^ 4 *
            LSeries (fun n => (χ ^ 2) ↑n) (1 + ↑x + 2 * Complex.I * ↑y)‖ ≥
        1

For positive x and nonzero y and a Dirichlet character χ we have |L(χ^0, 1 + x)^3 * L(χ, 1 + x + I * y)^4 * L(χ^2, 1 + x + 2 * I * y)| ≥ 1.

Defined in

Mathlib.NumberTheory.LSeries.Nonvanishing

Cited by

1 results in Mathlib

Foundations

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