mul_mu_eq_one — Mathlib

English

For χ and s with Re(s) > 1, L(χ)(s) L(χ · μ)(s) = 1.

Русский

Для χ и s с Re(s) > 1 имеем L(χ)(s) L(χ · μ)(s) = 1.

LaTeX

$$$L(\uparrow χ)(s) \cdot L(\uparrow χ * \uparrow μ)(s) = 1 \quad (1 < \Re(s)).$$$

Lean4

/-- The L-series of a Dirichlet character `χ` and of the twist of `μ` by `χ` are multiplicative
inverses. -/
theorem mul_mu_eq_one {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : L (↗χ) s * L (↗χ * ↗μ) s = 1 := by
  rw [←
    LSeries_convolution' (LSeriesSummable_of_one_lt_re χ hs) <|
      LSeriesSummable_mul χ <| ArithmeticFunction.LSeriesSummable_moebius_iff.mpr hs,
    convolution_mul_moebius, LSeries_delta, Pi.one_apply]

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