mathlib3 documentation

mathlib-archive / wiedijk_100_theorems.area_of_a_circle

Freek № 9: The Area of a Circle #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_region_between_eq_integral, which allows us to represent the area of the disc as an integral, and interval_integral.integral_eq_sub_of_has_deriv_at'_of_le, the second fundamental theorem of calculus.

We begin by defining disc in ℝ × ℝ, then show that disc can be represented as the region_between 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_region_between_eq_integral followed by interval_integral.integral_of_le to reduce our goal to a single interval_integral: ∫ (x : ℝ) in -r..r, 2 * sqrt (r ^ 2 - x ^ 2) = π * r ^ 2. After disposing of the trivial case r = 0, we show that λ x, 2 * sqrt (r ^ 2 - x ^ 2) is equal to the derivative of λ 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 euclidean_space ℝ (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 measure_theory.measure.prod_apply) which do not yet exist for Euclidean space, thus forcing us to use this less-preferable definition. As measure_theory.pi continues to develop, it should eventually become possible to redefine disc and extend our proof to the n-ball.

def theorems_100.disc (r : ) :

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.

theorem theorems_100.disc_eq_region_between (r : nnreal) :
theorems_100.disc r = region_between (λ (x : ), - (r ^ 2 - x ^ 2)) (λ (x : ), (r ^ 2 - x ^ 2)) (set.Ioc (-r) r)

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

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