Evaluation of the B.3 double integral

Proved

ErlerGross.B3_double_integral_eval

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

The double integral over the unit square of $(1-y)/(1-x^2y^3)$ evaluates to $\ln(27/16)$ . The integrand can be assigned any value at the corner where its displayed denominator vanishes.

Preamble

import Mathlib
open Real Filter Topology MeasureTheory

Formal statement

namespace ErlerGross

theorem B3_double_integral_eval :
    (∫ x in (0 : ℝ)..1, ∫ y in (0 : ℝ)..1,
      (1 - y) / (1 - x ^ 2 * y ^ 3)) = Real.log (27 / 16) := by
  sorry

end ErlerGross

Source

Independent integral evaluation associated with Erler and Gross, Appendix B, equation (B.3).

View graph