Ball tree

23 fully proved

Ball Tree

InductiveBall tree#✓fully proved

For a dimension \(d\), a ball tree over the integer points \(\mathbb{Z}^d\) (functions \(\{0, \dots, d-1\} \to \mathbb{Z}\)) is either empty, a leaf holding one point, or a node holding a center point \(c \in \mathbb{Z}^d\), a natural number \(b\) (the squared-radius bound of the node's sphere) and two child ball trees.

That the sphere around \(c\) actually contains the points below the node is a separate validity invariant, not part of this definition.

inductive BallTree (d : Nat) where
  | empty : BallTree d
  | leaf : (Fin d → Int) → BallTree d
  | node : (Fin d → Int) → Nat → BallTree d → BallTree d → BallTree d

Used by 12

Used byBuilding a ball tree by halving · Number of points of a ball tree · Search of a valid ball tree · Ball-tree similarity search · Accumulating ball-tree search · Ball-tree search is exact · Size of a ball tree · Point list of a ball tree · Accumulating traversal of a ball tree · A built ball tree stores a permutation of its input · Bounding-sphere invariant of a ball tree · Ball trees built by halving are valid

DefinitionAccumulating traversal of a ball tree#✓fully proved

For a ball tree \(T\) and a list \(A\) of points, the accumulating traversal returns \(A\) when \(T\) is empty, the point \(p\) followed by \(A\) when \(T\) is a leaf holding \(p\), and, when \(T\) is a node with children \(L\) and \(R\), the accumulating traversal of \(L\) whose accumulator is the accumulating traversal of \(R\) with accumulator \(A\).

The result is the leaf points of \(T\), from left to right, followed by \(A\).

def toListAux : BallTree d → List (Fin d → Int) → List (Fin d → Int)
  | .empty, acc => acc
  | .leaf p, acc => p :: acc
  | .node _ _ left right, acc => left.toListAux (right.toListAux acc)

Uses 1 · Used by 5

Statement usesBall tree

Used byNumber of points of a ball tree · Ball-tree search is exact · Point list of a ball tree · A built ball tree stores a permutation of its input · Ball trees built by halving are valid

DefinitionPoint list of a ball tree#✓fully proved

The point list of a ball tree is the list of the points held at its leaves, from left to right: the empty tree gives the empty list, a leaf holding \(p\) gives the list \([p]\), and a node gives the point list of its left subtree followed by the point list of its right subtree. The centers stored at nodes are not included.

def toList (t : BallTree d) : List (Fin d → Int) :=
  t.toListAux []

Uses 2 · Used by 11

Statement usesBall tree · Accumulating traversal of a ball tree

Used byNumber of points of a ball tree · Search of a built ball tree · Search of a valid ball tree · Points of a built ball tree · Ball-tree search of a built tree · Ball-tree search of a built tree, up to order · Ball-tree search is exact · Size of a built ball tree · A built ball tree stores a permutation of its input · Bounding-sphere invariant of a ball tree · Ball trees built by halving are valid

DefinitionSize of a ball tree#✓fully proved

The size of a ball tree is the number of points held in its leaves: it is \(0\) for the empty tree, \(1\) for a leaf, and the sum of the sizes of the two children for a node; the center of a node is not counted.

def size : BallTree d → Nat
  | .empty => 0
  | .leaf _ => 1
  | .node _ _ left right => left.size + right.size

Uses 1 · Used by 2

Statement usesBall tree

Used byNumber of points of a ball tree · Size of a built ball tree

TheoremNumber of points of a ball tree#✓fully proved

For every ball tree \(t\), the list of points stored in \(t\), read from left to right, has length equal to the size of \(t\).

@[simp]
theorem length_toList (t : BallTree d) : t.toList.length = t.size

Uses 4 · Used by 1

Statement usesBall tree · Size of a ball tree · Point list of a ball tree

Proof usesAccumulating traversal of a ball tree

Used bySize of a built ball tree

DefinitionSquared Euclidean distance#✓fully proved

For points \(p, q \in \mathbb{Z}^d\), the squared distance from \(p\) to \(q\) is the natural number \(\sum_{i=0}^{d-1} (p_i - q_i)^2\), computed in \(\mathbb{Z}\) and then converted to \(\mathbb{N}\).

def distSq (p q : Fin d → Int) : Nat :=
  (∑ i, (p i - q i) ^ 2).toNat

Used by 13

Used bySymmetry of squared distance · Points lie within the squared radius · Relaxed triangle inequality for squared distance · Search of a built ball tree · Search of a valid ball tree · Squared covering radius · Accumulating ball-tree search · Ball-tree search of a built tree · Ball-tree search of a built tree, up to order · Ball-tree search is exact · A built ball tree stores a permutation of its input · Bounding-sphere invariant of a ball tree · Ball trees built by halving are valid

TheoremSymmetry of squared distance#✓fully proved

For all points \(p, q \in \mathbb{Z}^d\), the squared distance from \(p\) to \(q\) equals the squared distance from \(q\) to \(p\).

theorem distSq_comm (p q : Fin d → Int) : distSq p q = distSq q p

Uses 1 · Used by 1

Statement usesSquared Euclidean distance

Used byBall-tree search is exact

TheoremRelaxed triangle inequality for squared distance#✓fully proved

For all points \(a, b, c \in \mathbb{Z}^d\), writing \(\delta(x, y)\) for the squared distance from \(x\) to \(y\), we have \(\delta(a, c) \le 2\,(\delta(a, b) + \delta(b, c))\).

The factor \(2\) comes from \((x + y)^2 \le 2(x^2 + y^2)\) applied coordinatewise. This is the estimate that makes bounding-sphere pruning sound without square roots.

theorem distSq_le_two_mul (a b c : Fin d → Int) :
    distSq a c ≤ 2 * (distSq a b + distSq b c)

Uses 1 · Used by 1

Statement usesSquared Euclidean distance

Used byBall-tree search is exact

DefinitionSquared covering radius#✓fully proved

For a center \(c \in \mathbb{Z}^d\) and a list \(P\) of points of \(\mathbb{Z}^d\), the squared covering radius of \(P\) about \(c\) is the largest squared distance from \(c\) to a point of \(P\), or \(0\) if \(P\) is empty.

def radiusSq (c : Fin d → Int) (pts : List (Fin d → Int)) : Nat :=
  pts.foldl (fun acc p => max acc (distSq c p)) 0

Uses 1 · Used by 4

Statement usesSquared Euclidean distance

Used byBuilding a ball tree by halving · Points lie within the squared radius · A built ball tree stores a permutation of its input · Ball trees built by halving are valid

TheoremPoints lie within the squared radius#✓fully proved

Let \(c \in \mathbb{Z}^d\) and let \(L\) be a list of points of \(\mathbb{Z}^d\). For every point \(p\) of \(L\), the squared distance from \(c\) to \(p\) is at most the squared radius of \(L\) around \(c\), the largest squared distance from \(c\) to a point of \(L\).

theorem distSq_le_radiusSq {c p : Fin d → Int} {pts : List (Fin d → Int)}
    (hp : p ∈ pts) : distSq c p ≤ radiusSq c pts

Uses 2 · Used by 2

Statement usesSquared Euclidean distance · Squared covering radius

Used byA built ball tree stores a permutation of its input · Ball trees built by halving are valid

DefinitionAccumulating ball-tree search#✓fully proved

Let \(d\) be a dimension and write \(\delta(x, y)\) for the squared distance from \(x\) to \(y\) in \(\mathbb{Z}^d\). For a ball tree \(T\) over \(\mathbb{Z}^d\), a query point \(q \in \mathbb{Z}^d\), a squared radius \(r \in \mathbb{N}\) and a list \(A\) of points, the accumulating search of \(T\) for \(q\) and \(r\) with accumulator \(A\) is \(A\) when \(T\) is empty; when \(T\) is a leaf holding \(p\), it is \(p\) followed by \(A\) if \(\delta(q, p) \le r\) and \(A\) otherwise; when \(T\) is a node with center \(c\), squared-radius bound \(b\) and children \(L\) and \(R\), it is \(A\) if \(2(b + r) < \delta(c, q)\), and otherwise the accumulating search of \(L\) for \(q\) and \(r\) whose accumulator is the accumulating search of \(R\) for \(q\) and \(r\) with accumulator \(A\).

When \(T\) satisfies the bounding-sphere invariant, this pruning is sound by the relaxed triangle inequality \(\delta(x, z) \le 2(\delta(x, y) + \delta(y, z))\) for all \(x, y, z \in \mathbb{Z}^d\), and the result is the points of \(T\) within squared distance \(r\) of \(q\), from left to right, followed by \(A\).

def searchAux : BallTree d → (Fin d → Int) → Nat →
    List (Fin d → Int) → List (Fin d → Int)
  | .empty, _, _, acc => acc
  | .leaf p, query, radius, acc =>
      if distSq query p ≤ radius then p :: acc else acc
  | .node center bound left right, query, radius, acc =>
      if 2 * (bound + radius) < distSq center query then acc
      else left.searchAux query radius (right.searchAux query radius acc)

Uses 2 · Used by 2

Statement usesBall tree · Squared Euclidean distance

Used byBall-tree similarity search · Ball-tree search is exact

DefinitionBall-tree similarity search#✓fully proved

The search of a ball tree \(T\) for a query point \(q \in \mathbb{Z}^d\) and a squared radius \(r \in \mathbb{N}\) is the accumulating search of \(T\) for \(q\) and \(r\) started with the empty accumulator.

When \(T\) satisfies the bounding-sphere invariant, the search lists exactly the points of \(T\) within squared distance \(r\) of \(q\), from left to right.

def search (t : BallTree d) (query : Fin d → Int) (radius : Nat) :
    List (Fin d → Int) :=
  t.searchAux query radius []

Uses 2 · Used by 5

Statement usesBall tree · Accumulating ball-tree search

Used bySearch of a built ball tree · Search of a valid ball tree · Ball-tree search of a built tree · Ball-tree search of a built tree, up to order · Ball-tree search is exact

InductiveBounding-sphere invariant of a ball tree#✓fully proved

Validity of a ball tree is defined inductively: the empty tree and every leaf are valid, and a node with center \(c\) and squared-radius bound \(b\) is valid when both of its subtrees are valid and every point in the point list of either subtree lies within squared Euclidean distance \(b\) of \(c\).

inductive Valid : BallTree d → Prop where
  | empty : Valid .empty
  | leaf (p : Fin d → Int) : Valid (.leaf p)
  | node {center : Fin d → Int} {bound : Nat} {left right : BallTree d}
      (hLeft : Valid left) (hRight : Valid right)
      (hSphereLeft : ∀ p ∈ left.toList, distSq center p ≤ bound)
      (hSphereRight : ∀ p ∈ right.toList, distSq center p ≤ bound) :
      Valid (.node center bound left right)

Uses 3 · Used by 4

Statement usesBall tree · Squared Euclidean distance · Point list of a ball tree

Used bySearch of a valid ball tree · Ball-tree search is exact · A built ball tree stores a permutation of its input · Ball trees built by halving are valid

TheoremBall-tree search is exact#✓fully proved

For every ball tree \(T\) over \(\mathbb{Z}^d\) satisfying the bounding-sphere invariant, every query point \(q \in \mathbb{Z}^d\) and every \(r \in \mathbb{N}\), the search of \(T\) for \(q\) and \(r\) equals the list of points of \(T\), from left to right, filtered to the points \(p\) whose squared distance from \(q\) is at most \(r\), in their order. Pruning against the bounding spheres loses no point.

theorem search_eq_filter {t : BallTree d} (h : t.Valid)
    (query : Fin d → Int) (radius : Nat) :
    t.search query radius =
      t.toList.filter (fun p => distSq query p ≤ radius)

Uses 9 · Used by 2

Statement usesBall tree · Bounding-sphere invariant of a ball tree · Squared Euclidean distance · Ball-tree similarity search · Point list of a ball tree

Proof usesSymmetry of squared distance · Relaxed triangle inequality for squared distance · Accumulating ball-tree search · Accumulating traversal of a ball tree

Used bySearch of a valid ball tree · Ball-tree search of a built tree

TheoremSearch of a valid ball tree#✓fully proved

Let \(t\) be a ball tree satisfying the bounding-sphere invariant. For all \(q, p \in \mathbb{Z}^d\) and every natural number \(r\), \(p\) is returned by the similarity search of \(t\) with query \(q\) and squared radius \(r\) if and only if \(p\) is one of the points stored in \(t\) and the squared distance from \(q\) to \(p\) is at most \(r\).

theorem mem_search_iff {t : BallTree d} (h : t.Valid)
    {query p : Fin d → Int} {radius : Nat} :
    p ∈ t.search query radius ↔ p ∈ t.toList ∧ distSq query p ≤ radius

Uses 6 · Used by 1

Statement usesBall tree · Bounding-sphere invariant of a ball tree · Squared Euclidean distance · Ball-tree similarity search · Point list of a ball tree

Proof usesBall-tree search is exact

Used bySearch of a built ball tree

DefinitionBuilding a ball tree by halving#✓fully proved

The ball tree built from a list of points of \(\mathbb{Z}^d\) is defined by recursion on the list. The empty list gives the empty tree and a one-point list \([p]\) gives the leaf \(p\). A list \(L = [x_1, \dots, x_n]\) with \(n \ge 2\) gives a node whose center is \(x_1\), whose bound is the squared radius of \(L\) around \(x_1\) (the largest squared distance from \(x_1\) to a point of \(L\)), whose left child is the tree built from the first \(\lfloor n/2 \rfloor\) points of \(L\), and whose right child is the tree built from the remaining points of \(L\).

def build : List (Fin d → Int) → BallTree d
  | [] => .empty
  | [p] => .leaf p
  | pts@(x :: _ :: _) =>
      .node x (radiusSq x pts)
        (build (pts.take (pts.length / 2)))
        (build (pts.drop (pts.length / 2)))
termination_by pts => pts.length
decreasing_by
  all_goals
    simp_all only [List.length_take, List.length_drop, List.length_cons]
    omega

Uses 2 · Used by 7

Statement usesBall tree · Squared covering radius

Used bySearch of a built ball tree · Points of a built ball tree · Ball-tree search of a built tree · Ball-tree search of a built tree, up to order · Size of a built ball tree · A built ball tree stores a permutation of its input · Ball trees built by halving are valid

TheoremBall trees built by halving are valid#✓fully proved

For every list of points in \(\mathbb{Z}^d\), the ball tree built from it by recursive halving satisfies the bounding-sphere invariant.

theorem valid_build (pts : List (Fin d → Int)) : (build pts).Valid

Uses 8 · Used by 2

Statement usesBounding-sphere invariant of a ball tree · Building a ball tree by halving

Proof usesBall tree · Squared Euclidean distance · Points lie within the squared radius · Squared covering radius · Point list of a ball tree · Accumulating traversal of a ball tree

Used bySearch of a built ball tree · Ball-tree search of a built tree

TheoremA built ball tree stores a permutation of its input#✓fully proved

For every list \(P\) of points of \(\mathbb{Z}^d\), the list of points of the ball tree built from \(P\), from left to right, is a permutation of \(P\).

theorem toList_build_perm (pts : List (Fin d → Int)) :
    (build pts).toList.Perm pts

Uses 8 · Used by 3

Statement usesBuilding a ball tree by halving · Point list of a ball tree

Proof usesBall tree · Bounding-sphere invariant of a ball tree · Squared Euclidean distance · Points lie within the squared radius · Squared covering radius · Accumulating traversal of a ball tree

Used byPoints of a built ball tree · Ball-tree search of a built tree, up to order · Size of a built ball tree

TheoremPoints of a built ball tree#✓fully proved

For every list \(L\) of points of \(\mathbb{Z}^d\) and every point \(p \in \mathbb{Z}^d\), \(p\) is one of the points stored in the ball tree built from \(L\) if and only if \(p\) occurs in \(L\).

theorem mem_toList_build_iff (pts : List (Fin d → Int)) (p : Fin d → Int) :
    p ∈ (build pts).toList ↔ p ∈ pts

Uses 3 · Used by 1

Statement usesBuilding a ball tree by halving · Point list of a ball tree

Proof usesA built ball tree stores a permutation of its input

Used bySearch of a built ball tree

TheoremSize of a built ball tree#✓fully proved

For every list \(P\) of points of \(\mathbb{Z}^d\), the size of the ball tree built from \(P\) equals the length of \(P\), that is, the number of entries of \(P\) counted with repetition.

@[simp]
theorem size_build (pts : List (Fin d → Int)) :
    (build pts).size = pts.length

Uses 5

Statement usesBuilding a ball tree by halving · Size of a ball tree

Proof usesNumber of points of a ball tree · Point list of a ball tree · A built ball tree stores a permutation of its input

TheoremBall-tree search of a built tree#✓fully proved

For every list \(P\) of points of \(\mathbb{Z}^d\), every query point \(q \in \mathbb{Z}^d\) and every \(r \in \mathbb{N}\), let \(T\) be the ball tree built from \(P\). The search of \(T\) for \(q\) and \(r\) equals the list of points of \(T\), from left to right, filtered to the points \(p\) whose squared distance from \(q\) is at most \(r\), in their order.

theorem search_build (pts : List (Fin d → Int)) (query : Fin d → Int)
    (radius : Nat) :
    (build pts).search query radius =
      (build pts).toList.filter (fun p => distSq query p ≤ radius)

Uses 6 · Used by 1

Statement usesBuilding a ball tree by halving · Squared Euclidean distance · Ball-tree similarity search · Point list of a ball tree

Proof usesBall-tree search is exact · Ball trees built by halving are valid

Used byBall-tree search of a built tree, up to order

TheoremBall-tree search of a built tree, up to order#✓fully proved

For every list \(P\) of points of \(\mathbb{Z}^d\), every query point \(q \in \mathbb{Z}^d\) and every \(r \in \mathbb{N}\), the search of the ball tree built from \(P\) for \(q\) and \(r\) is a permutation of the sublist of \(P\) consisting of the points \(p\) whose squared distance from \(q\) is at most \(r\), kept with their multiplicities.

theorem search_build_perm (pts : List (Fin d → Int)) (query : Fin d → Int)
    (radius : Nat) :
    ((build pts).search query radius).Perm
      (pts.filter (fun p => distSq query p ≤ radius))

Uses 6

Statement usesBuilding a ball tree by halving · Squared Euclidean distance · Ball-tree similarity search

Proof usesBall-tree search of a built tree · Point list of a ball tree · A built ball tree stores a permutation of its input

TheoremSearch of a built ball tree#✓fully proved

Let \(L\) be a list of points of \(\mathbb{Z}^d\), let \(q, p \in \mathbb{Z}^d\) and let \(r\) be a natural number. Then \(p\) is returned by the similarity search with query \(q\) and squared radius \(r\) on the ball tree built from \(L\) if and only if \(p\) occurs in \(L\) and the squared distance from \(q\) to \(p\) is at most \(r\).

theorem mem_search_build_iff (pts : List (Fin d → Int))
    {query p : Fin d → Int} {radius : Nat} :
    p ∈ (build pts).search query radius ↔
      p ∈ pts ∧ distSq query p ≤ radius

Uses 7

Statement usesBuilding a ball tree by halving · Squared Euclidean distance · Ball-tree similarity search

Proof usesSearch of a valid ball tree · Points of a built ball tree · Point list of a ball tree · Ball trees built by halving are valid

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.