Beardwood–Halton–Hammersley theorem

AbbreviationPoints of the Euclidean plane#✓fully proved

A planar point is a point of the Euclidean plane \(\mathbb{R}^2\): a pair \((x, y)\) of real numbers, with the Euclidean norm \(\lVert (x, y) \rVert = \sqrt{x^2 + y^2}\).

abbrev PlanarPoint := EuclideanSpace ℝ (Fin 2)

Used by 14

Used byBHH constant of a sampling law · The BHH constant equals the unique BHH limit · BHH limit values of a sampling law · Almost-sure BHH limit · Unique BHH constant of a law · I.i.d. realization · BHH constant of a law · I.i.d. points with a given law · Membership in the set of BHH limit values · Normalized tour length · Shortest tour length · Length of a closed tour · Unit square · Uniform law on the unit square

DefinitionCyclic successor#✓fully proved

For a natural number \(n\) and an index \(i\) with \(0 \le i < n\), the cyclic successor of \(i\) is \((i + 1) \bmod n\); in particular the successor of \(n - 1\) is \(0\). For \(n = 0\) there are no indices.

def cyclicNext {n : ℕ} (i : Fin n) : Fin n :=
  ⟨(i.val + 1) % n, Nat.mod_lt _ (Nat.zero_lt_of_lt i.isLt)⟩

Used by 1

Used byLength of a closed tour

DefinitionLength of a closed tour#✓fully proved

For points \(x_0, \dots, x_{n-1}\) in the Euclidean plane and a permutation \(\sigma\) of \(\{0, \dots, n-1\}\), the tour length is \(\sum_{i=0}^{n-1} \lVert x_{\sigma(i)} - x_{\sigma(i+1 \bmod n)} \rVert\), the length of the closed tour that visits \(x_{\sigma(0)}, \dots, x_{\sigma(n-1)}\) in this order and returns to its start.

noncomputable def tourLength
    {n : ℕ} (points : Fin n → PlanarPoint) (order : Equiv.Perm (Fin n)) : ℝ :=
  ∑ i : Fin n, dist (points (order i)) (points (order (cyclicNext i)))

Uses 2 · Used by 1

Statement usesPoints of the Euclidean plane · Cyclic successor

Used byShortest tour length

DefinitionShortest tour length#✓fully proved

For points \(x_0, \dots, x_{n-1}\) in the Euclidean plane, \(L_n\) is the minimum, over all permutations \(\sigma\) of \(\{0, \dots, n-1\}\), of the length of the closed tour that visits \(x_{\sigma(0)}, \dots, x_{\sigma(n-1)}\) in this order and returns to its start.

noncomputable def shortestTourLength {n : ℕ} (points : Fin n → PlanarPoint) : ℝ :=
  (Finset.univ : Finset (Equiv.Perm (Fin n))).inf'
    ⟨Equiv.refl (Fin n), Finset.mem_univ _⟩ (tourLength points)

Uses 2 · Used by 1

Statement usesPoints of the Euclidean plane · Length of a closed tour

Used byNormalized tour length

DefinitionNormalized tour length#✓fully proved

Let \(\Omega\) be a set and let \(X_0, X_1, X_2, \dots \colon \Omega \to \mathbb{R}^2\) be functions. For an outcome \(\omega \in \Omega\) and \(n \ge 1\), the normalized tour length is \(L_n(\omega)/\sqrt{n}\), where \(L_n(\omega)\) is the length of a shortest closed tour through \(X_0(\omega), \dots, X_{n-1}(\omega)\). For \(n = 0\) it is defined to be \(0\).

The value at \(n = 0\) does not affect limits as \(n \to \infty\).

noncomputable def normalizedTourLength
    {Ω : Type*} (points : ℕ → Ω → PlanarPoint) (ω : Ω) (n : ℕ) : ℝ :=
  if 0 < n then
    shortestTourLength (fun i : Fin n => points i.val ω) / Real.sqrt n
  else
    0

Uses 2 · Used by 1

Statement usesPoints of the Euclidean plane · Shortest tour length

Used byAlmost-sure BHH limit

DefinitionI.i.d. points with a given law#✓fully proved

Let \(\Omega\) be a measurable space with a measure \(\mathbb{P}\), let \(X_0, X_1, X_2, \dots \colon \Omega \to \mathbb{R}^2\) be functions and let \(\nu\) be a measure on the Borel sets of the plane. The \(X_i\) are i.i.d. with law \(\nu\) when \(\mathbb{P}\) and \(\nu\) are probability measures, every \(X_i\) is measurable, the \(X_i\) are mutually independent under \(\mathbb{P}\), and the distribution of each \(X_i\) under \(\mathbb{P}\) is \(\nu\).

def IsIIDWithLaw
    {Ω : Type*}
    (mΩ : MeasurableSpace Ω)
    (probability : Measure Ω)
    (points : ℕ → Ω → PlanarPoint)
    (law : Measure PlanarPoint) : Prop :=
  letI := mΩ
  IsProbabilityMeasure probability ∧
    IsProbabilityMeasure law ∧
    (∀ i, Measurable (points i)) ∧
    ProbabilityTheory.iIndepFun points probability ∧
    ∀ i, Measure.map (points i) probability = law

Uses 1 · Used by 1

Statement usesPoints of the Euclidean plane

Used byI.i.d. realization

StructureI.i.d. realization#✓fully proved

For a measure \(\nu\) on the plane, an i.i.d. realization with law \(\nu\) consists of a measurable space \(\Omega\) with a measure \(\mathbb{P}\), together with a sequence \(X_0, X_1, X_2, \dots \colon \Omega \to \mathbb{R}^2\) of points that is i.i.d. with common law \(\nu\) under \(\mathbb{P}\).

structure IIDRealization (law : Measure PlanarPoint) where
  Ω : Type
  measurableSpace : MeasurableSpace Ω
  probability : Measure Ω
  points : ℕ → Ω → PlanarPoint
  isIID : IsIIDWithLaw measurableSpace probability points law

Uses 2 · Used by 1

Statement usesI.i.d. points with a given law · Points of the Euclidean plane

Used byBHH constant of a law

DefinitionAlmost-sure BHH limit#✓fully proved

Let \(\Omega\) be a measurable space with a measure \(\mu\), let \(X_0, X_1, X_2, \dots \colon \Omega \to \mathbb{R}^2\) be functions into the plane, and let \(\beta\) be a real number. The sequence has BHH limit \(\beta\) when, for \(\mu\)-almost every \(\omega \in \Omega\), the normalized tour length \(L_n(\omega)/\sqrt{n}\) tends to \(\beta\) as \(n \to \infty\), where \(L_n(\omega)\) is the length of a shortest closed tour through \(X_0(\omega), \dots, X_{n-1}(\omega)\).

def HasBHHLimit
    {Ω : Type*}
    (mΩ : MeasurableSpace Ω)
    (probability : Measure Ω)
    (points : ℕ → Ω → PlanarPoint)
    (β : ℝ) : Prop :=
  letI := mΩ
  ∀ᵐ ω ∂probability,
    Tendsto (normalizedTourLength points ω) atTop (nhds β)

Uses 2 · Used by 1

Statement usesPoints of the Euclidean plane · Normalized tour length

Used byBHH constant of a law

DefinitionBHH constant of a law#✓fully proved

For a measure \(\nu\) on the plane and a real number \(\beta\), \(\beta\) is a BHH constant for \(\nu\) when an i.i.d. realization with law \(\nu\) exists and every i.i.d. realization with law \(\nu\) has almost-sure BHH limit \(\beta\): almost surely, \(L_n/\sqrt{n} \to \beta\), where \(L_n\) is the length of a shortest closed tour through the first \(n\) points.

Requiring a realization to exist keeps the condition from holding vacuously.

def IsBHHConstantFor (law : Measure PlanarPoint) (β : ℝ) : Prop :=
  Nonempty (IIDRealization law) ∧
    ∀ realization : IIDRealization law,
      HasBHHLimit realization.measurableSpace realization.probability realization.points β

Uses 3 · Used by 5

Statement usesAlmost-sure BHH limit · I.i.d. realization · Points of the Euclidean plane

Used byThe BHH constant equals the unique BHH limit · BHH limit values of a sampling law · Unique BHH constant of a law · Membership in the set of BHH limit values · Statement of the Beardwood–Halton–Hammersley theorem

DefinitionBHH limit values of a sampling law#✓fully proved

For a measure \(\mu\) on the plane, the BHH limit values of \(\mu\) form the set of real numbers \(\beta\) that are BHH limits for \(\mu\).

def bhhLimitValues (law : Measure PlanarPoint) : Set ℝ :=
  {β | IsBHHConstantFor law β}

Uses 2 · Used by 3

Statement usesBHH constant of a law · Points of the Euclidean plane

Used byBHH constant of a sampling law · The BHH constant equals the unique BHH limit · Membership in the set of BHH limit values

TheoremMembership in the set of BHH limit values#✓fully proved

For a measure \(\nu\) on the plane and a real number \(\beta\), \(\beta\) belongs to the set of BHH limit values of \(\nu\) if and only if \(\beta\) is a BHH constant for \(\nu\).

theorem mem_bhhLimitValues_iff (law : Measure PlanarPoint) (β : ℝ) :
    β ∈ bhhLimitValues law ↔ IsBHHConstantFor law β

Uses 3

Statement usesBHH constant of a law · Points of the Euclidean plane · BHH limit values of a sampling law

DefinitionUnique BHH constant of a law#✓fully proved

A measure \(\nu\) on the plane has a unique BHH constant when there is exactly one real number \(\beta\) that is a BHH constant for \(\nu\).

def HasUniqueBHHConstantFor (law : Measure PlanarPoint) : Prop :=
  ∃! β : ℝ, IsBHHConstantFor law β

Uses 2

Statement usesBHH constant of a law · Points of the Euclidean plane

DefinitionBHH constant of a sampling law#✓fully proved

For a measure \(\mu\) on the plane, the BHH constant of \(\mu\) is the infimum of the set of real numbers \(\beta\) that are BHH limits for \(\mu\). The infimum of a set of reals that is empty or not bounded below is taken to be \(0\).

No existence theorem is assumed: the definition does not presuppose that a BHH limit exists.

noncomputable def bhhConstantFor (law : Measure PlanarPoint) : ℝ :=
  sInf (bhhLimitValues law)

Uses 2 · Used by 2

Statement usesPoints of the Euclidean plane · BHH limit values of a sampling law

Used byBeardwood–Halton–Hammersley constant · The BHH constant equals the unique BHH limit

TheoremThe BHH constant equals the unique BHH limit#✓fully proved

Let \(\mu\) be a measure on the plane and \(\beta\) a real number. If, for every real \(\gamma\), \(\gamma\) is a BHH limit for \(\mu\) if and only if \(\gamma = \beta\), then the BHH constant of \(\mu\) (the infimum of its BHH limits) equals \(\beta\).

The hypothesis excludes the case with no BHH limit, where the infimum is \(0\) by convention.

theorem bhhConstantFor_eq_of_unique_characterization
    (law : Measure PlanarPoint) (β : ℝ)
    (h : ∀ γ : ℝ, IsBHHConstantFor law γ ↔ γ = β) :
    bhhConstantFor law = β

Uses 4

Statement usesBHH constant of a law · Points of the Euclidean plane · BHH constant of a sampling law

Proof usesBHH limit values of a sampling law

DefinitionUnit square#✓fully proved

The closed unit square \([0,1]^2\): the set of points of the Euclidean plane both of whose coordinates lie in the interval \([0,1]\).

def unitSquare : Set PlanarPoint :=
  {point | ∀ coordinate, point coordinate ∈ Set.Icc (0 : ℝ) 1}

Uses 1 · Used by 1

Statement usesPoints of the Euclidean plane

Used byUniform law on the unit square

DefinitionUniform law on the unit square#✓fully proved

Lebesgue measure on the Euclidean plane restricted to the closed unit square \([0,1]^2\).

noncomputable def unitSquareUniformLaw : Measure PlanarPoint :=
  volume.restrict unitSquare

Uses 2 · Used by 2

Statement usesPoints of the Euclidean plane · Unit square

Used byBeardwood–Halton–Hammersley constant · Statement of the Beardwood–Halton–Hammersley theorem

DefinitionBeardwood–Halton–Hammersley constant#✓fully proved

The Beardwood–Halton–Hammersley constant is the BHH constant of the uniform law on the closed unit square \([0,1]^2\) (Lebesgue measure restricted to \([0,1]^2\)): the infimum of the set of real numbers \(\beta\) such that i.i.d. samples with this law exist and, for every such sample \(X_1, X_2, \dots\), the length of the shortest closed tour through \(X_1, \dots, X_n\) divided by \(\sqrt{n}\) tends to \(\beta\) almost surely. The infimum of a set of reals that is empty or not bounded below is taken to be \(0\).

noncomputable def beardwoodHaltonHammersleyConstant : ℝ :=
  bhhConstantFor unitSquareUniformLaw

Uses 2 · Used by 1

Statement usesBHH constant of a sampling law · Uniform law on the unit square

Used byThe notation \(\beta_2\)

AbbreviationThe notation \(\beta_2\)#✓fully proved

We write \(\beta_2\) for the real-valued Beardwood–Halton–Hammersley constant of the unit square.

noncomputable abbrev β₂ : ℝ := beardwoodHaltonHammersleyConstant

Uses 1 · Used by 8

Statement usesBeardwood–Halton–Hammersley constant

Used byStatement of the Beardwood–Halton–Hammersley lower bound · Statement of the Beardwood–Halton–Hammersley upper bound · Notation C₁₂ for the BHH constant · Statement of the Gaudio–Jaillet lower bound · Statement of the corrected Steinerberger lower bound · Statement of Steinerberger's upper bound · Statement of the Beardwood–Halton–Hammersley theorem · Statement of the Yu–Carlsson upper bound

AbbreviationNotation C₁₂ for the BHH constant#✓fully proved

The constant \(C_{12}\) is defined to be the Beardwood–Halton–Hammersley constant \(\beta_2\) for uniform points in the unit square; \(C_{12}\) is the name the source uses for it.

noncomputable abbrev C₁₂ : ℝ := β₂

Uses 1

Statement usesThe notation \(\beta_2\)

DefinitionStatement of the Beardwood–Halton–Hammersley theorem#✓fully proved

The proposition that the Beardwood–Halton–Hammersley constant \(\beta_2\) is a BHH constant for the uniform law on the closed unit square \([0,1]^2\), and that every real number \(\beta\) that is a BHH constant for this law equals \(\beta_2\). Here a real number \(\beta\) is a BHH constant for a law \(\mu\) on the plane when a sequence \(X_0, X_1, \dots\) of independent random points with common law \(\mu\) exists on some probability space, and for every such sequence, almost surely \(L_n / \sqrt{n} \to \beta\) as \(n \to \infty\), where \(L_n\) is the length of the shortest closed tour through \(X_0, \dots, X_{n-1}\).

def unitSquareBHHTheorem : Prop :=
  IsBHHConstantFor unitSquareUniformLaw β₂ ∧
    ∀ β : ℝ, IsBHHConstantFor unitSquareUniformLaw β → β = β₂

Uses 3 · Used by 1

Statement usesBHH constant of a law · Uniform law on the unit square · The notation \(\beta_2\)

Used byBeardwood–Halton–Hammersley theorem

DefinitionStatement of the Beardwood–Halton–Hammersley upper bound#✓fully proved

This is the proposition that the Beardwood–Halton–Hammersley constant \(\beta_2\) for uniform points in the unit square satisfies \(\beta_2 \le 0.92117\), the upper bound reported by Beardwood, Halton and Hammersley (1959).

def bhh1959UpperBound : Prop :=
  β₂ ≤ (92117 : ℝ) / 100000

Uses 1 · Used by 1

Statement usesThe notation \(\beta_2\)

Used byBeardwood–Halton–Hammersley upper bound

DefinitionStatement of Steinerberger's upper bound#✓fully proved

The proposition that the Beardwood–Halton–Hammersley constant \(\beta_2\) satisfies \(\beta_2 \le 0.92117 - \frac{9}{16} \cdot 10^{-6}\).

def steinerberger2015ImprovedUpperBound : Prop :=
  β₂ ≤ (92117 : ℝ) / 100000 - (9 : ℝ) / 16 * (1 / 1000000)

Uses 1 · Used by 1

Statement usesThe notation \(\beta_2\)

Used bySteinerberger's upper bound for the BHH constant

DefinitionStatement of the Yu–Carlsson upper bound#✓fully proved

This is the proposition that the real-valued Beardwood–Halton–Hammersley constant \(\beta_2\) of the unit square satisfies \(\beta_2 < 0.90304\).

def yuCarlsson2023StrictUpperBound : Prop :=
  β₂ < (90304 : ℝ) / 100000

Sources

• [YC2023], strict computer-aided upper bound.

Uses 1 · Used by 1

Statement usesThe notation \(\beta_2\)

Used byYu–Carlsson upper bound on the BHH constant

DefinitionStatement of the Beardwood–Halton–Hammersley lower bound#✓fully proved

This is the proposition that the Beardwood–Halton–Hammersley constant \(\beta_2\) for uniform points in the unit square satisfies \(\beta_2 \ge 5/8 = 0.625\), the lower bound reported by Beardwood, Halton and Hammersley (1959).

def bhh1959LowerBound : Prop :=
  (5 : ℝ) / 8 ≤ β₂

Uses 1 · Used by 1

Statement usesThe notation \(\beta_2\)

Used byBeardwood–Halton–Hammersley lower bound

DefinitionStatement of the corrected Steinerberger lower bound#✓fully proved

The proposition that the Beardwood–Halton–Hammersley constant \(\beta_2\) satisfies \(\frac{5}{8} + \frac{19}{10368} \le \beta_2\).

The bound is the exact rational \(\frac{5}{8} + \frac{19}{10368}\), not a decimal approximation of it.

def steinerberger2015CorrectedSymbolicLowerBound : Prop :=
  (5 : ℝ) / 8 + 19 / 10368 ≤ β₂

Uses 1 · Used by 1

Statement usesThe notation \(\beta_2\)

Used byGaudio–Jaillet corrected lower bound for the BHH constant

DefinitionStatement of the Gaudio–Jaillet lower bound#✓fully proved

The proposition that the Beardwood–Halton–Hammersley constant \(\beta_2\) of the unit square is at least \(0.6277\), that is, \(0.6277 \le \beta_2\).

def gaudioJaillet2020LowerBound : Prop :=
  (6277 : ℝ) / 10000 ≤ β₂

Uses 1 · Used by 1

Statement usesThe notation \(\beta_2\)

Used byGaudio–Jaillet lower bound for the BHH constant

TheoremBeardwood–Halton–Hammersley theorem#●ready to prove

Let \(\beta_2\) be the Beardwood–Halton–Hammersley constant and, for points \(X_0, X_1, \dots\) of the plane, let \(L_n\) be the length of the shortest closed tour through \(X_0, \dots, X_{n-1}\). Then a sequence of independent random points \(X_0, X_1, \dots\), each uniformly distributed on the closed unit square \([0,1]^2\), exists on some probability space; for every such sequence, almost surely \(L_n / \sqrt{n} \to \beta_2\) as \(n \to \infty\); and \(\beta_2\) is the only real number \(\beta\) such that every such sequence almost surely satisfies \(L_n / \sqrt{n} \to \beta\).

theorem_wanted unitSquareBHHTheorem_holds : unitSquareBHHTheorem

Sources

• Beardwood, Halton and Hammersley (1959), quoted in Steinerberger (2015).

Uses 1

Statement usesStatement of the Beardwood–Halton–Hammersley theorem

TheoremBeardwood–Halton–Hammersley upper bound#●ready to prove

The Beardwood–Halton–Hammersley constant \(\beta_2\) for uniform points in the unit square satisfies \(\beta_2 \le 0.92117\).

theorem_wanted bhh1959UpperBound_holds : bhh1959UpperBound

Sources

• Beardwood, Halton and Hammersley (1959), catalogue upper-bound row.

Uses 1

Statement usesStatement of the Beardwood–Halton–Hammersley upper bound

TheoremSteinerberger's upper bound for the BHH constant#●ready to prove

The Beardwood–Halton–Hammersley constant \(\beta_2\) satisfies \(\beta_2 \le 0.92117 - \frac{9}{16} \cdot 10^{-6}\).

theorem_wanted steinerberger2015ImprovedUpperBound_holds :
    steinerberger2015ImprovedUpperBound

Sources

• Steinerberger, New Bounds for the Traveling Salesman Constant (2015).

Uses 1

Statement usesStatement of Steinerberger's upper bound

TheoremYu–Carlsson upper bound on the BHH constant#●ready to prove

The real-valued Beardwood–Halton–Hammersley constant \(\beta_2\) of the unit square satisfies \(\beta_2 < 0.90304\).

theorem_wanted yuCarlsson2023StrictUpperBound_holds : yuCarlsson2023StrictUpperBound

Sources

• Yu and Carlsson (2023), strict upper-bound row in the catalogue.

Uses 1

Statement usesStatement of the Yu–Carlsson upper bound

TheoremBeardwood–Halton–Hammersley lower bound#●ready to prove

The Beardwood–Halton–Hammersley constant \(\beta_2\) for uniform points in the unit square satisfies \(\beta_2 \ge 5/8 = 0.625\).

theorem_wanted bhh1959LowerBound_holds : bhh1959LowerBound

Sources

• Beardwood, Halton and Hammersley (1959), catalogue lower-bound row.

Uses 1

Statement usesStatement of the Beardwood–Halton–Hammersley lower bound

TheoremGaudio–Jaillet corrected lower bound for the BHH constant#●ready to prove

The Beardwood–Halton–Hammersley constant \(\beta_2\) satisfies \(\frac{5}{8} + \frac{19}{10368} \le \beta_2\).

theorem_wanted steinerberger2015CorrectedSymbolicLowerBound_holds :
    steinerberger2015CorrectedSymbolicLowerBound

Sources

• Gaudio and Jaillet (2020), correction of Steinerberger's lower coefficient.

Uses 1

Statement usesStatement of the corrected Steinerberger lower bound

TheoremGaudio–Jaillet lower bound for the BHH constant#●ready to prove

The Beardwood–Halton–Hammersley constant \(\beta_2\) of the unit square satisfies \(0.6277 \le \beta_2\).

theorem_wanted gaudioJaillet2020LowerBound_holds : gaudioJaillet2020LowerBound

Sources

• Gaudio and Jaillet, An improved lower bound for the Traveling Salesman constant.

Uses 1

Statement usesStatement of the Gaudio–Jaillet lower bound

26 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.