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.
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.
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).
The disc is a measurable_set.
Area of a Circle: The area of a disc with radius r is π * r ^ 2.