Freek № 99: Buffon's Needle #
This file proves Theorem 99 from the 100 Theorems List, also
known as Buffon's Needle, which gives the probability of a needle of length l > 0
crossing any
one of infinite vertical lines spaced out d > 0
apart.
The two cases are proven in buffon_short
and buffon_long
.
Overview of the Proof #
We define a random variable B : Ω → ℝ × ℝ
with a uniform distribution on [-d/2, d/2] × [0, π]
.
This represents the needle's x-position and angle with respect to a vertical line. By symmetry, we
need to consider only a single vertical line positioned at x = 0
. A needle therefore crosses the
vertical line if its projection onto the x-axis contains 0
.
We define a random variable N : Ω → ℝ
that is 1
if the needle crosses a vertical line, and 0
otherwise. This is defined as fun ω => Set.indicator (needleProjX l (B ω).1 (B ω).2) 1 0
.
f
As in many references, the problem is split into two cases, l ≤ d
(buffon_short
), and d ≤ l
(buffon_long
). For both cases, we show that
ℙ[N] = (d * π) ⁻¹ *
∫ θ in 0..π,
∫ x in Set.Icc (-d / 2) (d / 2) ∩ Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2), 1
In the short case l ≤ d
, we show that [-l * θ.sin/2, l * θ.sin/2] ⊆ [-d/2, d/2]
(short_needle_inter_eq
), and therefore the inner integral simplifies to
∫ x in (-θ.sin * l / 2)..(θ.sin * l / 2), 1 = θ.sin * l
Which then concludes in the short case being ℙ[N] = (2 * l) / (d * π)
.
In the long case, l ≤ d
(buffon_long
), we show the outer integral simplifies to
∫ θ in 0..π, min d (θ.sin * l)
which can be expanded to
2 * (
∫ θ in 0..(d / l).arcsin, min d (θ.sin * l) +
∫ θ in (d / l).arcsin..(π / 2), min d (θ.sin * l)
)
We then show the two integrals equal their respective values l - √(l^2 - d^2)
and
(π / 2 - (d / l).arcsin) * d
. Then with some algebra we conclude
ℙ[N] = (2 * l) / (d * π) - 2 / (d * π) * (√(l^2 - d^2) + d * (d / l).arcsin) + 1
References #
- https://en.wikipedia.org/wiki/Buffon%27s_needle_problem
- https://www.math.leidenuniv.nl/~hfinkeln/seminarium/stelling_van_Buffon.pdf
- https://www.isa-afp.org/entries/Buffons_Needle.html
Projection of a needle onto the x-axis. The needle's center is at x-coordinate x
, of length
l
and angle θ
. Note, θ
is measured relative to the y-axis, that is, a vertical needle has
θ = 0
.
Equations
Instances For
The indicator function of whether a needle at position ⟨x, θ⟩ : ℝ × ℝ
crosses the line x = 0
.
In order to faithfully model the problem, we compose needleCrossesIndicator
with a random
variable B : Ω → ℝ × ℝ
with uniform distribution on [-d/2, d/2] × [0, π]
. Then, by symmetry,
the probability that the needle crosses x = 0
, is the same as the probability of a needle
crossing any of the infinitely spaced vertical lines distance d
apart.
Equations
- BuffonsNeedle.needleCrossesIndicator l p = (BuffonsNeedle.needleProjX l p.1 p.2).indicator 1 0
Instances For
A random variable representing whether the needle crosses a line.
The line is at x = 0
, and therefore a needle crosses the line if its projection onto the x-axis
contains 0
. This random variable is 1
if the needle crosses the line, and 0
otherwise.
Equations
Instances For
This is a common step in both the short and the long case to simplify the expectation of the needle crossing a line to a double integral.
∫ (θ : ℝ) in Set.Icc 0 π,
∫ (x : ℝ) in Set.Icc (-d / 2) (d / 2) ∩ Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2), 1
The domain of the inner integral is simpler in the short case, where the intersection is
equal to Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2)
by short_needle_inter_eq
.
From buffon_integral
, in both the short and the long case, we have
𝔼[N l B] = (d * π)⁻¹ *
∫ (θ : ℝ) in Set.Icc 0 π,
∫ (x : ℝ) in Set.Icc (-d / 2) (d / 2) ∩ Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2), 1
With this lemma, in the short case, the inner integral's domain simplifies to
Set.Icc (-θ.sin * l / 2) (θ.sin * l / 2)
.
Buffon's Needle, the short case (l ≤ d
). The probability of the needle crossing a line
equals (2 * l) / (d * π)
.
This equality is useful since θ.sin
is increasing in 0..π / 2
(but not in 0..π
).
Then, ∫ θ in (0)..π / 2, min d (θ.sin * l)
can be split into two adjacent integrals, at the
point where d = θ.sin * l
, which is θ = (d / l).arcsin
.
The first of two adjacent integrals in the long case. In the range (0)..(d / l).arcsin
, we
have that θ.sin * l ≤ d
, and thus the integral is ∫ θ in (0)..(d / l).arcsin, θ.sin * l
.
The second of two adjacent integrals in the long case. In the range (d / l).arcsin..(π / 2)
, we
have that d ≤ θ.sin * l
, and thus the integral is ∫ θ in (d / l).arcsin..(π / 2), d
.
Buffon's Needle, the long case (d ≤ l
).