Evaluation of the rational series from the B.3 integral
ProvedErlerGross.B3_rational_tsum_evalanalysisseries
The convergent rational series with nth term 1/((2n+1)(3n+1)(3n+2)) sums to log(27/16). A partial-fraction decomposition reduces this to logarithmic limits of harmonic sums in residue classes.
Preamble
import Mathlib open Real Filter Topology MeasureTheory
Formal statement
namespace ErlerGross
theorem B3_rational_tsum_eval :
tsum (fun n : Nat => (1 : Real) / ((2 * n + 1) * (3 * n + 1) * (3 * n + 2))) =
Real.log (27 / 16) := by
sorry
end ErlerGrossSource
Independent partial-fractions evaluation of the series arising from the geometric expansion of the integral in Erler-Gross, Appendix B, equation (B.3).