Documentation

Archive.Wiedijk100Theorems.BuffonsNeedle

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 #

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

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
    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
    Instances For
      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
      Instances For
        @[reducible, inline]

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

        Equations
        Instances For
          theorem BuffonsNeedle.volume_needleSpace (d : ) (hd : 0 < d) :
          MeasureTheory.volume (BuffonsNeedle.needleSpace d) = ENNReal.ofReal (d * Real.pi)
          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 (θ : ) => min 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, min d (Real.sin θ * l) = 2 * ∫ (θ : ) in 0 ..Real.pi / 2, min 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), min 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, min 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).