English
For a quadratic Dirichlet character χ (χ^2 = 1) and any prime p and exponent k, zetaMul χ (p^k) is nonnegative.
Русский
Для квадратичного χ (χ^2 = 1) и любого простого p, степени k, zetaMul χ (p^k) неотрицательно.
LaTeX
$$$0 \le zetaMul χ (p^k) \quad\text{for prime } p$$$
Lean4
theorem zetaMul_prime_pow_nonneg {χ : DirichletCharacter ℂ N} (hχ : χ ^ 2 = 1) {p : ℕ} (hp : p.Prime) (k : ℕ) :
0 ≤ zetaMul χ (p ^ k) :=
by
simp only [zetaMul, toArithmeticFunction, coe_zeta_mul_apply, coe_mk, Nat.sum_divisors_prime_pow hp, pow_eq_zero_iff',
hp.ne_zero, ne_eq, false_and, ↓reduceIte, Nat.cast_pow, map_pow]
rcases MulChar.isQuadratic_iff_sq_eq_one.mpr hχ p with h | h | h
· refine Finset.sum_nonneg fun i _ ↦ ?_
simp only [h, le_refl, pow_nonneg]
· refine Finset.sum_nonneg fun i _ ↦ ?_
simp only [h, one_pow, zero_le_one]
· simp only [h, neg_one_geom_sum]
split_ifs
exacts [le_rfl, zero_le_one]
