Prove2Me

The volume of the half box is −∫0π/4log⁡(1−14cos⁡2θ) dθ-\int_0^{\pi/4} \log\bigl(1 - \tfrac{1}{4\cos^2\theta}\bigr)\,d\theta

Proved
Thurston23.hvol_halfBox_eq_ofReal_integral

by t4v1 · Sep 13, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

hyperbolic-geometrykleinian-groupsthurston-question-23

The hyperbolic volume ∫Bt−3 dx dy dt\int_B t^{-3}\,dx\,dy\,dt of the half box B={∣x∣≤12, 0≤y≤12, x2+y2+t2≥1}B = \{|x| \le \tfrac12,\ 0 \le y \le \tfrac12,\ x^2+y^2+t^2 \ge 1\} equals

−∫0π/4log⁡(1−14cos⁡2θ) dθ,-\int_0^{\pi/4} \log\Bigl(1 - \frac{1}{4\cos^2\theta}\Bigr)\,d\theta,

stated in [0,∞][0, \infty] through ENNReal.ofReal. The height integral ∫a∞t−3 dt=1/(2a2)\int_a^\infty t^{-3}\,dt = 1/(2a^2) reduces the volume to the plane integral ∫Ddx dy/(2(1−x2−y2))\int_D dx\,dy / (2(1 - x^2 - y^2)) over the base D=[−12,12]×[0,12]D = [-\tfrac12, \tfrac12] \times [0, \tfrac12]; in polar coordinates a ray at angle θ∈[0,π)\theta \in [0, \pi) leaves DD at r=1/(2max⁡(∣cos⁡θ∣,sin⁡θ))r = 1/(2\max(|\cos\theta|, \sin\theta)), the radial integral is −14log⁡(1−r2)-\tfrac14 \log(1 - r^2), and the angular integral over [0,π][0, \pi] folds by θ↦π−θ\theta \mapsto \pi - \theta and θ↦π/2−θ\theta \mapsto \pi/2 - \theta onto [0,π/4][0, \pi/4], where the bound is 1/(2cos⁡θ)1/(2\cos\theta). The integral evaluates to −G/3-G/3, GG Catalan's constant (a separate, Mathlib-only statement), which is Humbert's formula for Q(i)\mathbb{Q}(i).

Preamble
import Definitions.Def_Thurston23_picard
Formal statement
namespace Thurston23

open MeasureTheory

theorem hvol_halfBox_eq_ofReal_integral :
    hvol halfBox = ENNReal.ofReal
      (-∫ θ in (0:ℝ)..Real.pi / 4, Real.log (1 - 1 / (4 * Real.cos θ ^ 2))) := by
  sorry

end Thurston23
Source
W. P. Thurston, Three-dimensional manifolds, Kleinian groups and hyperbolic geometry, Bull. Amer. Math. Soc. 6 (1982), 357-381, Question 23 (p. 380). G. Humbert, Sur la mesure des classes d'Hermite de discriminant donné dans un corps quadratique imaginaire, C. R. Acad. Sci. Paris 169 (1919), 448-454. Formalisation: https://github.com/t4v1/thurston23/blob/58bb3fd/Thurston23.lean#L3744-L3751 (section Polar).

View graph