Say I have N which isn't a power of 2. I want to make sure that if I take the closest power of 2 to N from above (like 16 if N is 11), I won't ruin the complexity.

So, I thought about this trivial lemma: for each N that isn't a power of 2, there is some power of 2 between N and 2N.

If I have this proved, I can say that because replacing [N -> 2N] doesn't ruin the complexity, so shouldn't [N -> closest power of 2 to N from above], because it's smaller than 2N.

OK, now to the proof...

How to I express the closest power of 2 to the number ? I define (like in C's math library) for a positive real X: `floor(X)` is the largest integer smaller than X and `ceil(X)` is the smallest integer larger than X.

Now, the closest power of 2 from below to some N is: `2^floor(log(N))` when *log* is base 2. Similarly, the closest power of 2 from above to some N is `2^ceil(log(N))`. By definition:

`2^ceil(log(N)) => N`

I want to prove that

`2^ceil(log(N)) <=? 2N`

Taking the logarithm (base 2) of both sides I get:

`ceil(log(N)) <=? log(2N)`

But in base 2 logarithms:

`log(2N) = log(N) + 1`

So I have to prove that:

`ceil(log(N)) <=? log(N) + 1`

Which is true by definition of ceil() ! So indeed there is a power of 2 between N and 2N, it is `2^ceil(log(N))`

. Q.E.D.

Corollary: Since the closest power of 2 to 2N from below is:

`2^floor(log(2N)) = 2^floor(log(N) + 1) = 2^ceil(log(N))`

It's actually the closest power of 2 to N from above, so: *for each N (that's not a power of 2) there is one and only one power of 2 between N and 2N.*

This is a very trivial mathematical fact which makes a lot of sense, but it's nice to prove it formally :-)