# Multidimensional Binary Search Trees

 Title: Multidimensional Binary Search Trees Author: Martin Rau (martin /dot/ rau /at/ tum /dot/ de) Submission date: 2019-05-30 Abstract: This entry provides a formalization of multidimensional binary trees, also known as k-d trees. It includes a balanced build algorithm as well as the nearest neighbor algorithm and the range search algorithm. It is based on the papers Multidimensional binary search trees used for associative searching and An Algorithm for Finding Best Matches in Logarithmic Expected Time. Change history: [2020-15-04]: Change representation of k-dimensional points from 'list' to HOL-Analysis.Finite_Cartesian_Product 'vec'. Update proofs to incorporate HOL-Analysis 'dist' and 'cbox' primitives. BibTeX: @article{KD_Tree-AFP, author = {Martin Rau}, title = {Multidimensional Binary Search Trees}, journal = {Archive of Formal Proofs}, month = may, year = 2019, note = {\url{https://isa-afp.org/entries/KD_Tree.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Median_Of_Medians_Selection