Sorting has `Θ(n log n)` query complexity

Stream: Program verification

[Geoffrey Irving]

I formalized the fact that sorting has Θ(n log n) query complexity, including for randomized algorithms: https://github.com/girving/debate/blob/f5a4cf1692c9d501c7a922081dc3cf3965e57802/Comp/Sort.lean

The lower bound is via information theory (you can only learn one bit about the oracle per query), and the upper bound is via merge sort.

[Geoffrey Irving]

@Eric Wieser In particular I did this by adding information theory to the debate repo and generalizing it various ways (oracles can take any input type, expectations can be over vector spaces, etc.). If you're fine with this I can start upstreaming the various pieces to the main debate repo.

https://github.com/girving/debate/commit/f5a4cf1692c9d501c7a922081dc3cf3965e57802

[Geoffrey Irving]

After DM discussion: we'll keep it separate for now, and I'll eventually make a comp or complexity repo with finite probability theory and stochastic oracle computations which that debate repo will depend on.

[Shreyas Srinivas]

When you say query complexity, what precisely is getting counted?

[Shreyas Srinivas]

Number of calls to a comparison oracle?

[Geoffrey Irving]

Yes. See Comp/Defs.lean for the definition of oracle computation.