Cubic reciprocal series behind the (B.3) evaluation
ProvedErlerGross.B3_cubic_reciprocal_series_closed_formmathematical-physicsseriesstring-field-theory
The positive cubic reciprocal series obtained by simplifying the rational summand in Appendix B has the closed form
sum_{nge 1} rac{1}{(2n-1)(3n-1)(3n-2)}=ln rac{27}{16}.This is the elementary-series evaluation needed for the (B.3) closed form; the target series is its negative half term by term.
Preamble
import Mathlib import Definitions.Def_ErlerGross_defs open Real Filter Topology MeasureTheory
Formal statement
namespace ErlerGross
theorem B3_cubic_reciprocal_series_closed_form :
HasSum (fun n : Nat => 1 / (((2 * (n : Real) + 1) * (3 * (n : Real) + 1) * (3 * (n : Real) + 2))))
(Real.log (27 / 16)) := by
sorry
end ErlerGrossSource
T. G. Erler and D. J. Gross, Locality, Causality, and an Initial Value Formulation for Open String Field Theory, arXiv:hep-th/0406199v2 (2004), Appendix B, p. 46, Eq. (B.3); cubic-denominator form follows by simplifying the displayed rational summand.