Freek № 9: The Area of a Circle

In this file we show that the area of a disc with nonnegative radius r is π * r^2. The main tools our proof uses are volume_regionBetween_eq_integral, which allows us to represent the area of the disc as an integral, and intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, the second fundamental theorem of calculus.

We begin by defining disc in ℝ × ℝ, then show that disc can be represented as the regionBetween two functions.

Though not necessary for the main proof, we nonetheless choose to include a proof of the measurability of the disc in order to convince the reader that the set whose volume we will be calculating is indeed measurable and our result is therefore meaningful.

In the main proof, area_disc, we use volume_regionBetween_eq_integral followed by intervalIntegral.integral_of_le to reduce our goal to a single intervalIntegral: ∫ (x : ℝ) in -r..r, 2 * sqrt (r ^ 2 - x ^ 2) = π * r ^ 2. After disposing of the trivial case r = 0, we show that fun x => 2 * sqrt (r ^ 2 - x ^ 2) is equal to the derivative of fun x => r ^ 2 * arcsin (x / r) + x * sqrt (r ^ 2 - x ^ 2) everywhere on Ioo (-r) r and that those two functions are continuous, then apply the second fundamental theorem of calculus with those facts. Some simple algebra then completes the proof.

Note that we choose to define disc as a set of points in ℝ × ℝ. This is admittedly not ideal; it would be more natural to define disc as a Metric.ball in EuclideanSpace ℝ (Fin 2) (as well as to provide a more general proof in higher dimensions). However, our proof indirectly relies on a number of theorems (particularly MeasureTheory.Measure.prod_apply) which do not yet exist for Euclidean space, thus forcing us to use this less-preferable definition. As MeasureTheory.pi continues to develop, it should eventually become possible to redefine disc and extend our proof to the n-ball.

def Theorems100.disc (r : ℝ) : Set (ℝ × ℝ)

A disc of radius r is defined as the collection of points (p.1, p.2) in ℝ × ℝ such that p.1 ^ 2 + p.2 ^ 2 < r ^ 2. Note that this definition is not equivalent to Metric.ball (0 : ℝ × ℝ) r. This was done intentionally because dist in ℝ × ℝ is defined as the uniform norm, making the Metric.ball in ℝ × ℝ a square, not a disc. See the module docstring for an explanation of why we don't define the disc in Euclidean space.

Equations

• Theorems100.disc r = {p : ℝ × ℝ | p.1 ^ 2 + p.2 ^ 2 < r ^ 2}

theorem Theorems100.disc_eq_regionBetween (r : NNReal) : Theorems100.disc ↑r = regionBetween (fun (x : ℝ) => -√(↑r ^ 2 - x ^ 2)) (fun (x : ℝ) => √(↑r ^ 2 - x ^ 2)) (Set.Ioc (-↑r) ↑r)

A disc of radius r can be represented as the region between the two curves fun x => - sqrt (r ^ 2 - x ^ 2) and fun x => sqrt (r ^ 2 - x ^ 2).

theorem Theorems100.measurableSet_disc (r : NNReal) : MeasurableSet (Theorems100.disc ↑r)

The disc is a MeasurableSet.

theorem Theorems100.area_disc (r : NNReal) : MeasureTheory.volume (Theorems100.disc ↑r) = ↑NNReal.pi * ↑r ^ 2

Area of a Circle: The area of a disc with radius r is π * r ^ 2.