The Pappus–Guldin theorem for volumes of revolution

Revolving a measurable plane region R (coordinates (r, z)) about the z-axis gives a solid of volume 2π ∫_R r, i.e. the area of R times the length 2π r̄ of the path of its centroid; points with r ≤ 0 contribute nothing to either side, so no sign condition is needed. Built on Mathlib's polar coordinates: each horizontal slice is a planar set {√(u² + v²) ∈ A}, whose area is 2π ∫_A r by lintegral_comp_polarCoord_symm, and Tonelli reassembles the slices.

Main results

• PappusGuldin.volume_revolution: volume of the solid of revolution of R = 2 pi * integral over R of r

References

• P. Guldin, Centrobaryca, Vienna, 1635–1641; Pappus of Alexandria, Collection, Book VII.

theorem PappusGuldin.volume_revolution (R : Set (ℝ × ℝ)) (hR : MeasurableSet R) : MeasureTheory.volume {q : (ℝ × ℝ) × ℝ | (√(q.1.1 ^ 2 + q.1.2 ^ 2), q.2) ∈ R} = ENNReal.ofReal (2 * Real.pi) * ∫⁻ (p : ℝ × ℝ) in R, ENNReal.ofReal p.1

Pappus–Guldin (volume). Revolving a measurable plane region R (coordinates (r, z)) about the z-axis gives a solid of volume 2π ∫_R r.