Abstract: 
This entry contains proofs for the textbook results about the
distributions of the height and internal path length of random binary
search trees (BSTs), i. e. BSTs that are formed by taking
an empty BST and inserting elements from a fixed set in random
order. In particular, we prove a logarithmic upper
bound on the expected height and the Θ(n log n)
closedform solution for the expected internal path length in terms of
the harmonic numbers. We also show how the internal path length
relates to the averagecase cost of a lookup in a BST. 
BibTeX: 
@article{Random_BSTsAFP,
author = {Manuel Eberl},
title = {Expected Shape of Random Binary Search Trees},
journal = {Archive of Formal Proofs},
month = apr,
year = 2017,
note = {\url{http://isaafp.org/entries/Random_BSTs.shtml},
Formal proof development},
ISSN = {2150914x},
}
