Integral representation of the B.3 series

Proved

ErlerGross.B3_series_double_integral

by Eyal1990 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

For the sequence of terms in Erler and Gross equation (B.3), its sum is negative one half of a double integral over the unit square with integrand $(1-y)/(1-x^2y^3)$ . The geometric series in the denominator gives this integral representation.

Preamble

import Mathlib
import Definitions.Def_ErlerGross_defs
open Real Filter Topology MeasureTheory

Formal statement

namespace ErlerGross

theorem B3_series_double_integral :
    HasSum (fun n : ℕ => b3Term (n + 1))
      ((-1 / 2) * (∫ x in (0 : ℝ)..1, ∫ y in (0 : ℝ)..1,
        (1 - y) / (1 - x ^ 2 * y ^ 3))) := by
  sorry

end ErlerGross

Source

Independent integral method for Erler and Gross, Appendix B, equation (B.3).

View graph