Prove2Me

Proof of Lemma 5, p. 912 — the L_m diameter of a rectangle is at most d times (indeed d^{1/m} times) its longest side

Proved
AryaANN.Search.rect_diam_le

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

boxesminkowski-metricp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Fix an LmL_m distance on Rd\mathbb R^d with 1≤m≤∞1\le m\le\infty and a rectangle RR whose longest side has length size⁡(R)\operatorname{size}(R). For all x,y∈Rx,y\in R,

dist⁡m(x,y)≤d⋅size⁡(R),\operatorname{dist}_m(x,y)\le d\cdot\operatorname{size}(R),

and, when mm is finite, dist⁡m(x,y)≤d1/msize⁡(R)\operatorname{dist}_m(x,y)\le d^{1/m}\operatorname{size}(R).

In the proof of Lemma 5 this bounds the distance between a point of a visited cell and the data point associated with it, both of which lie in the cell's outer box.

Formalization Note The paper speaks of "this cell"; the bound is stated for rectangles, which covers the outer box of a cell and hence the cell and its associated data point.

Preamble
import Mathlib
import Definitions.Def_AryaANN_Search_Setting
Formal statement
namespace AryaANN.Search

theorem rect_diam_le {d : ℕ} (m : ℕ∞) (hm : 1 ≤ m) (R : Rect d) :
    ∀ x ∈ R.toSet, ∀ y ∈ R.toSet,
      lmDist m x y ≤ (d : ℝ) * R.size ∧
      (m ≠ ⊤ → lmDist m x y ≤ (d : ℝ) ^ ((1 : ℝ) / m.toNat) * R.size) := by sorry

end AryaANN.Search
Source
Arya et al., An optimal algorithm for approximate nearest neighbor searching in fixed dimensions, J. ACM 45 (1998), p. 912, proof of Lemma 5, first paragraph
Human review

  • Endorsed by Shuze Chen · Oct 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph