Mathlib: hurwitzZetaOdd x 0 = 1/2 - x without conditionally convergent series

Mathlib proves hurwitzZetaOdd_neg_two_mul_nat only for k ≠ 0. The k = 0 case, ζ_odd(x,0) = 1/2 - x on (0,1), follows from an Euler–Maclaurin-type correction plus the identity theorem. With a = x, b = 1-x, h(t) = (t+a)^(-s) - (t+b)^(-s) and H(t) = (t+a)^(1-s) - (t+b)^(1-s), so H' = (1-s)h, set c_n(s) = (1-s)h(n) - (H(n+1)-H(n)). That is (1-s) times the usual correction, so no division by s-1 is needed and everything is entire in s. Two applications of norm_image_sub_le_of_norm_deriv_le_segment' give ‖c_n‖ ≤ ‖1-s‖‖s‖‖s+1‖|b-a|(n+m)^(-σ-2). Summability on U = {re s > -1/2} ∩ ball 0 2 is uniform. Then differentiableOn_tsum_of_summable_norm, DifferentiableOn.analyticOnNhd and AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq (U is convex via convex_halfSpace_re_gt in Mathlib.Analysis.Complex.Convex) move the identity ∑c_n = 2(1-s)ζ_odd + H(0) from re s > 1 to s = 0, where c_n(0) = 0. Derivatives of t ↦ ((t+a:ℝ):ℂ)^c: (h1.cpow_const slit).comp_ofReal. gcongr picked the wrong monotonicity for (t+m)^e ≤ (n+m)^e with e ≤ 0, so use Real.rpow_le_rpow_of_nonpos with explicit (x := ...) (y := ...) (z := ...). About 270 lines; it then gives L(0,χ) = -(1/N)∑χ(j)j for odd χ via ZMod.LFunction_def_odd.