feat(IK): prove LSeries_liouville_eq

[giuseppesorge]

Summary

Proves LSeries_liouville_eq (#1286): for Re s > 1, the Dirichlet series of the Liouville function λ equals ζ(2s)/ζ(s).

Approach

λ is completely multiplicative with λ(p) = -1, so the summand n ↦ λ(n)·n^(-s) is a ℕ →*₀ ℂ. By the Euler product for completely multiplicative functions it factors as ∏ₚ (1 - λ(p)p^(-s))⁻¹ = ∏ₚ (1 + p^(-s))⁻¹. Multiplying with the Euler product of ζ(s) (HasProd.mul) and identifying the result with that of ζ(2s) (HasProd.unique, via (1-p^(-s))⁻¹(1+p^(-s))⁻¹ = (1-p^(-2s))⁻¹) gives ζ(s)·L(λ,s) = ζ(2s); dividing by ζ(s) ≠ 0 yields the result. Same high-level EulerProduct approach as the existing two_pow_omega lemmas.

On the helper lemmas (duplication with Mathlib)

This file defines its own ArithmeticFunction.liouville rather than importing Mathlib's
Mathlib.NumberTheory.ArithmeticFunction.Liouville, so Mathlib's lemmas about liouville are not in scope here. I
therefore re-prove the small facts I need — liouville_apply, liouville_apply_one, liouville_apply_mul,
liouville_norm_le — which mirror Mathlib's. The cleaner long-term fix would be to have this file use Mathlib's
liouville (dropping the local definition and these helpers), but that touches the existing liouville definition, its
blueprint node, and the other liouville_* lemmas, so I kept this PR focused on LSeries_liouville_eq. Happy to make that
refactor instead if you prefer.

AI assistance

This proof was developed with AI assistance (Claude).

Closes #1286

[giuseppesorge]

awaiting-review

[giuseppesorge]

Added a small follow-up commit (1d7e31c) that fixes a typo in the existing informal blueprint proof of this node: the
intermediate Euler product was written as ∏_p (1 - p^{-s})^{-1}(1 - p^{-2s}), which evaluates to ζ(s)/ζ(2s) rather than ζ(2s)/ζ(s). The text now matches the formalised proof.