Torricelli's trumpet

Revolving y = 1/x, x ≥ 1, about the x-axis gives a solid of volume π; adding the cylinder of radius 1 and height 1 gives the volume 2π of the cylinder of radius √2 and height 1 (Theorem of the Day's form). The plane region under the hyperbola has infinite area and the surface integrand (1/x)√(1 + x⁻⁴) ≥ 1/x is not integrable: a finite volume with an infinite cross-section and skin. The volumes come from our Pappus–Guldin volume_revolution.

Main results

• Torricelli.volume_trumpet: the trumpet has volume π
• Torricelli.volume_trumpet_union_cylinder: trumpet + unit cylinder = cylinder of radius √2 and height 1 (volume 2π)
• Torricelli.volume_section_eq_top: the plane section has infinite area
• Torricelli.not_integrableOn_surface: the surface-area integrand is not integrable on [1, ∞)

References

• R. Whitty, Theorem of the Day, «Torricelli's Trumpet» (Analysis/Torricelli).
• E. Torricelli, Opera geometrica (1644); P. Mancosu, Philosophy of Mathematics and Mathematical Practice in the Seventeenth Century, OUP 1999, ch. 5.

theorem Torricelli.volume_trumpet : MeasureTheory.volume {q : (ℝ × ℝ) × ℝ | 1 ≤ q.2 ∧ √(q.1.1 ^ 2 + q.1.2 ^ 2) ≤ 1 / q.2} = ENNReal.ofReal Real.pi

The trumpet has volume π.

theorem Torricelli.volume_trumpet_union_cylinder : MeasureTheory.volume ({q : (ℝ × ℝ) × ℝ | 1 ≤ q.2 ∧ √(q.1.1 ^ 2 + q.1.2 ^ 2) ≤ 1 / q.2} ∪ {q : (ℝ × ℝ) × ℝ | 0 ≤ q.2 ∧ q.2 ≤ 1 ∧ √(q.1.1 ^ 2 + q.1.2 ^ 2) ≤ 1}) = MeasureTheory.volume {q : (ℝ × ℝ) × ℝ | 0 ≤ q.2 ∧ q.2 ≤ 1 ∧ √(q.1.1 ^ 2 + q.1.2 ^ 2) ≤ √2} ∧ MeasureTheory.volume {q : (ℝ × ℝ) × ℝ | 0 ≤ q.2 ∧ q.2 ≤ 1 ∧ √(q.1.1 ^ 2 + q.1.2 ^ 2) ≤ √2} = ENNReal.ofReal (2 * Real.pi)

Trumpet plus unit cylinder has the volume 2π of the cylinder of radius √2, height 1.

theorem Torricelli.volume_section_eq_top : MeasureTheory.volume {p : ℝ × ℝ | 1 ≤ p.1 ∧ |p.2| ≤ 1 / p.1} = ⊤

The plane section of the trumpet has infinite area.

theorem Torricelli.not_integrableOn_surface : ¬MeasureTheory.IntegrableOn (fun (x : ℝ) => 1 / x * √(1 + x⁻¹ ^ 4)) (Set.Ici 1) MeasureTheory.volume

The surface-area integrand is not integrable on [1, ∞).

theorem Torricelli.trumpet : have ρ := fun (q : (ℝ × ℝ) × ℝ) => √(q.1.1 ^ 2 + q.1.2 ^ 2); have T := {q : (ℝ × ℝ) × ℝ | 1 ≤ q.2 ∧ ρ q ≤ 1 / q.2}; have Cyl := {q : (ℝ × ℝ) × ℝ | 0 ≤ q.2 ∧ q.2 ≤ 1 ∧ ρ q ≤ 1}; have Cyl2 := {q : (ℝ × ℝ) × ℝ | 0 ≤ q.2 ∧ q.2 ≤ 1 ∧ ρ q ≤ √2}; MeasureTheory.volume (T ∪ Cyl) = MeasureTheory.volume Cyl2 ∧ MeasureTheory.volume Cyl2 = ENNReal.ofReal (2 * Real.pi) ∧ MeasureTheory.volume T = ENNReal.ofReal Real.pi ∧ MeasureTheory.volume {p : ℝ × ℝ | 1 ≤ p.1 ∧ |p.2| ≤ 1 / p.1} = ⊤ ∧ ¬MeasureTheory.IntegrableOn (fun (x : ℝ) => 1 / x * √(1 + x⁻¹ ^ 4)) (Set.Ici 1) MeasureTheory.volume

Torricelli's trumpet.