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^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
second fundamental theorem of calculus.
We begin by defining
ℝ × ℝ, 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
∫ (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
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
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
ℝ × ℝ is defined as the uniform norm, making the
ℝ × ℝ 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).