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

def BuffonsNeedle.needleProjX (l x θ : ℝ) : Set ℝ

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

• BuffonsNeedle.needleProjX l x θ = Set.Icc (x - Real.sin θ * l / 2) (x + Real.sin θ * l / 2)

noncomputable def BuffonsNeedle.needleCrossesIndicator (l : ℝ) (p : ℝ × ℝ) : ℝ

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

noncomputable def BuffonsNeedle.N {Ω : Type u_1} (l : ℝ) (B : Ω → ℝ × ℝ) : Ω → ℝ

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

• BuffonsNeedle.N l B = BuffonsNeedle.needleCrossesIndicator l ∘ B

@[reducible, inline]

abbrev BuffonsNeedle.needleSpace (d : ℝ) : Set (ℝ × ℝ)

The possible x-positions and angle relative to the y-axis of a needle.

Equations

• BuffonsNeedle.needleSpace d = Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 Real.pi

theorem BuffonsNeedle.volume_needleSpace (d : ℝ) (hd : 0 < d) : MeasureTheory.volume (BuffonsNeedle.needleSpace d) = ENNReal.ofReal (d * Real.pi)

theorem BuffonsNeedle.measurable_needleCrossesIndicator (l : ℝ) : Measurable (BuffonsNeedle.needleCrossesIndicator l)

theorem BuffonsNeedle.stronglyMeasurable_needleCrossesIndicator (l : ℝ) : MeasureTheory.StronglyMeasurable (BuffonsNeedle.needleCrossesIndicator l)

theorem BuffonsNeedle.integrable_needleCrossesIndicator (d l : ℝ) (hd : 0 < d) : MeasureTheory.Integrable (BuffonsNeedle.needleCrossesIndicator l) ((MeasureTheory.volume.restrict (Set.Icc (-d / 2) (d / 2))).prod (MeasureTheory.volume.restrict (Set.Icc 0 Real.pi)))

theorem BuffonsNeedle.buffon_integral {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (d l : ℝ) (hd : 0 < d) (B : Ω → ℝ × ℝ) (hBₘ : Measurable B) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 Real.pi) MeasureTheory.volume MeasureTheory.volume) : ∫ (a : Ω), BuffonsNeedle.N l B a = (d * Real.pi)⁻¹ * ∫ (θ : ℝ) in Set.Icc 0 Real.pi, ∫ (x : ℝ) in Set.Icc (-d / 2) (d / 2) ∩ Set.Icc (-Real.sin θ * l / 2) (Real.sin θ * l / 2), 1

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.

theorem BuffonsNeedle.short_needle_inter_eq (d l : ℝ) (hl : 0 < l) (h : l ≤ d) (θ : ℝ) : Set.Icc (-d / 2) (d / 2) ∩ Set.Icc (-Real.sin θ * l / 2) (Real.sin θ * l / 2) = Set.Icc (-Real.sin θ * l / 2) (Real.sin θ * l / 2)

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).

theorem BuffonsNeedle.buffon_short {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (d l : ℝ) (hd : 0 < d) (hl : 0 < l) (B : Ω → ℝ × ℝ) (hBₘ : Measurable B) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 Real.pi) MeasureTheory.volume MeasureTheory.volume) (h : l ≤ d) : ∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l * (d * Real.pi)⁻¹

Buffon's Needle, the short case (l ≤ d). The probability of the needle crossing a line equals (2 * l) / (d * π).

theorem BuffonsNeedle.intervalIntegrable_min_const_sin_mul (d l a b : ℝ) : IntervalIntegrable (fun (θ : ℝ) => d ⊓ Real.sin θ * l) MeasureTheory.volume a b

The integrand in the long case is min d (θ.sin * l) and its integrability is necessary for the integral lemmas below.

theorem BuffonsNeedle.integral_min_eq_two_mul (d l : ℝ) : ∫ (θ : ℝ) in 0 ..Real.pi, d ⊓ Real.sin θ * l = 2 * ∫ (θ : ℝ) in 0 ..Real.pi / 2, d ⊓ Real.sin θ * l

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.

theorem BuffonsNeedle.integral_zero_to_arcsin_min (d l : ℝ) (hd : 0 < d) (hl : 0 < l) : ∫ (θ : ℝ) in 0 ..Real.arcsin (d / l), d ⊓ Real.sin θ * l = (1 - √(1 - (d / l) ^ 2)) * l

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.

theorem BuffonsNeedle.integral_arcsin_to_pi_div_two_min (d l : ℝ) (hl : 0 < l) (h : d ≤ l) : ∫ (θ : ℝ) in Real.arcsin (d / l)..Real.pi / 2, d ⊓ Real.sin θ * l = (Real.pi / 2 - Real.arcsin (d / l)) * d

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.

theorem BuffonsNeedle.buffon_long {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] (d l : ℝ) (hd : 0 < d) (hl : 0 < l) (B : Ω → ℝ × ℝ) (hBₘ : Measurable B) (hB : MeasureTheory.pdf.IsUniform B (Set.Icc (-d / 2) (d / 2) ×ˢ Set.Icc 0 Real.pi) MeasureTheory.volume MeasureTheory.volume) (h : d ≤ l) : ∫ (x : Ω), BuffonsNeedle.N l B x = 2 * l / (d * Real.pi) - 2 / (d * Real.pi) * (√(l ^ 2 - d ^ 2) + d * Real.arcsin (d / l)) + 1

Buffon's Needle, the long case (d ≤ l).