zetaMul_nonneg — Mathlib

English

If χ is a quadratic Dirichlet character, then zetaMul χ n is nonnegative for all n.

Русский

Если χ — квадратичный символь Дирихле, то zetaMul χ n неотрицательно для всех n.

LaTeX

$$$\forall χ:\mathrm{DirichletCharacter}\;\mathbb{C}\;N,\ χ^2=1\Rightarrow \ 0 \le zetaMul χ n$$$

Lean4

/-- `zetaMul χ` takes nonnegative real values when `χ` is a quadratic character. -/
theorem zetaMul_nonneg {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) (n : ℕ) : 0 ≤ zetaMul χ n :=
  by
  rcases eq_or_ne n 0 with rfl | hn
  · simp only [ArithmeticFunction.map_zero, le_refl]
  ·
    simpa only [χ.isMultiplicative_zetaMul.multiplicative_factorization _ hn] using
      Finset.prod_nonneg fun p hp ↦
        zetaMul_prime_pow_nonneg hχ (Nat.prime_of_mem_primeFactors hp)
          _
            /-
            ### "Bad" Dirichlet characters

            Our goal is to show that `L(χ, 1) ≠ 0` when `χ` is a (nontrivial) quadratic Dirichlet character.
            To do that, we package the contradictory properties in a (private) structure
            `DirichletCharacter.BadChar` and derive further statements eventually leading to a contradiction.

            This entire section is private.
            -/

Похожие утверждения