Geometric-series expansion of the B.3 double integral
ProvedErlerGross.B3_double_integral_eq_tsumanalysisseries
Expanding the nonnegative integrand by the geometric series and integrating each monomial gives this representation of the double integral as a convergent rational series.
Preamble
import Mathlib open Real Filter Topology MeasureTheory
Formal statement
namespace ErlerGross
theorem B3_double_integral_eq_tsum :
intervalIntegral (fun x : Real =>
intervalIntegral (fun y : Real => (1 - y) / (1 - x ^ 2 * y ^ 3)) 0 1 volume) 0 1 volume =
tsum (fun n : Nat => (1 : Real) / ((2 * n + 1) * (3 * n + 1) * (3 * n + 2))) := by
sorry
end ErlerGrossSource
Direct geometric-series and monotone-convergence argument for the unit-square integral in Erler-Gross, Appendix B, equation (B.3).