Rich line bound (source code)

= Rich line bound
{title2=$L_{\geq k}=O(n^2/k^3+n/k)$}

For $n$ distinct points in the real plane, $L_{\geq k}$ counts <lines> containing at least $k\geq2$ points. The <Szemerédi–Trotter theorem> applied to these <lines> gives the bound by absorbing its additive line-count term; bounded $k$ follows by counting point pairs. Consequently, summing occupancies of <lines> with at least $k$ points by dyadic ranges gives $O(n^2/k^2+n\log n)$.