1.3. Complexity expressions
The complexity expression on the right of => has type Nat → Nat.
Pick whichever expression best models the algorithm:
Asymptotic | Lean expression |
|---|---|
O(1) |
|
O(n) |
|
O(n log n) |
|
O(n²) |
|
O(n³) |
|
O(2ⁿ) |
|
Nat.log2 is in core Lean. The + 1 in the n log n row guards
against log2 0 = 0 producing a zero denominator in the ratio.