Mathlib: L(1,χ) = Σχ(n)/n and expZeta x 1 = -log(1-e(x)) without conditional series

Mathlib has the analytic continuation of L-functions but nothing tying L(1,χ) to the conditionally convergent series. One route: (1) Abel summation for real s > 1, ‖Σ_{M≤n<K} b_n a_n‖ ≤ 2B b_M for antitone b ≥ 0 and partial sums of a bounded by B. Induct on K (Nat.le_induction) on ‖T_K - b_K G_K‖ ≤ B b_M + B(b_M - b_K); this is easier than Finset.sum_Ico_by_parts. (2) Take le_of_tendsto of the tail, using HasSum.tendsto_sum_nat and sum_Ico_eq_sub, to get ‖F(s) - S_K(s)‖ ≤ 2B(K+1)^{-s}. (3) Let s → 1⁺ with le_of_tendsto_of_tendsto on 𝓝[>] 1; both sides are continuous in real s. The result is ‖L(1,χ) - Σ_{n≤K} χ(n)/n‖ ≤ 2N/(K+1), using ZMod.differentiableAt_LFunction (Or.inr hΦ) and ZMod.LFunction_eq_LSeries. For expZeta x 1, feed the partial sums to Complex.tendsto_tsum_powerSeries_nhdsWithin_lt (Abel's limit theorem) and compare with -log(1 - z w) from hasSum_taylorSeries_neg_log by tendsto_nhds_unique. Then ZMod.LFunction_dft with IsPrimitive.fourierTransform_eq_inv_mul_gaussSum gives L(1,χ) as a sum of logs. Gotchas: continuousAt_finset_sum does not exist (use tendsto_finsetSum); Even.eval_neg takes χ explicitly (Even.eval_neg χ j he); (by tac : T) is not term syntax, use (show T by tac).