Lean/Mathlib: explicit lower bound for |L(1,χ)| from Mathlib's 3-4-1 lemma

Mathlib proves L(1,χ) ≠ 0 but gives no lower bound. DirichletCharacter.norm_LSeries_product_ge_one χ hx 0 gives ‖L(1+x,1_N)^3 L(1+x,χ)^4 L(1+x,χ²)‖ ≥ 1 directly, after simp [ofReal_zero, mul_zero, add_zero]. You then need three bounds. (a) ‖L(σ,1_N)‖ ≤ σ/(σ-1): use tsum_of_norm_bounded with g n = 1/n^σ, then Real.tsum_le_of_sum_range_le, and on the n ≥ 2 part AntitoneOn.sum_le_integral + integral_rpow (Or.inr ⟨_, 0 ∉ uIcc⟩). (b) An L' bound: get HasDerivAt from (LSeries_hasDerivAt h).congr_of_eventuallyEq heq with heq : LFunction χ =ᶠ[𝓝 t] LSeries; take the filter from (isOpen_lt continuous_const continuous_re).mem_nhds. Then .comp_ofReal gives a real-variable derivative. The abscissa bound is abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable with ZMod.LSeriesSummable_of_one_lt_re. (c) For the mean value inequality up to the point 1, where you have no derivative bound, apply Convex.norm_image_sub_le_of_norm_hasDerivWithin_le on convex_Ioi 1. Then pass x → 1⁺ with le_of_tendsto_of_tendsto on 𝓝[>] 1, using continuity of LFunction. Choosing x = δ/ℓ² yields ‖L(1,χ)‖ ≥ 1/(128 ℓ⁷), ℓ = log(N+3)+3. Gotcha: an info message 'ring failed, use ring_nf' without a position can appear even when the file compiles (exit 0). It came from ring after convert ... using 4, where the cast goal needed ring_nf.