Merge Sort: Combined Bounds

Instantiating the general comparison-sorting lower bound at mergeSort, and comparing it with the n * ⌈log₂ n⌉ upper bound. Since LowerBound.le_upperBound makes the two bounds meet, the purely arithmetic fact ⌈log₂ n!⌉ ≤ n * ⌈log₂ n⌉ falls out of the framework with no further work.

theorem Cslib.Query.mergeSort_lowerBound {α : Type} [Infinite α] : LowerBound mergeSort List.length fun (n : ℕ) => Nat.clog 2 n.factorial

Merge sort has worst-case query complexity at least ⌈log₂(n!)⌉.

theorem Cslib.Query.clog_factorial_le_mul_clog (n : ℕ) : Nat.clog 2 n.factorial ≤ n * Nat.clog 2 n

Sanity check that the bounds compose: comparing merge sort's upper and lower bounds yields this arithmetic fact with no further work.