Base-2 Logarithm

Interface of a log2 function, then its specification on naturals

Derived properties of logarithm

log2 is always non-negative

A tactic for proving positivity and non-negativity

The spec of log2 indeed determines it

Hence log2 is a morphism.

An alternate specification

log2 is exact on powers of 2

log2 and predecessors of powers of 2

log2 and basic constants

log2 n is strictly positive for 1<n

Said otherwise, log2 is null only below 1

log2 is a monotone function (but not a strict one)

No reverse result for <=, consider for instance log2 3 <= log2 2

When left side is a power of 2, we have an equivalence for <=

When right side is a square, we have an equivalence for <

Comparing log2 and identity

Log2 and multiplication. Due to rounding error, we don't have the usual log2 (a*b) = log2 a + log2 b but we may be off by 1 at most

And we can't find better approximations in general.

• The lower bound is exact for powers of 2.
• Concerning the upper bound, for any c>1, take a=b=2^c-1, then log2 (a*b) = c+c -1 while (log2 a) = (log2 b) = c-1

At least, we get back the usual equation when we multiply by 2 (or 2^k)

Two numbers with same log2 cannot be far away.

Log2 and successor :

• the log2 function climbs by at most 1 at a time
• otherwise it stays at the same value
• the +1 steps occur for powers of two

Log2 and addition

The sum of two log2 is less than twice the log2 of the sum. The large inequality is obvious thanks to monotonicity. The strict one requires some more work. This is almost a convexity inequality for points 2a, 2b and their middle a+b : ideally, we would have 2*log(a+b) >= log(2a)+log(2b) = 2+log a+log b. Here, we cannot do better: consider for instance a=2 b=4, then 1+2<2*2

log2_up : a binary logarithm that rounds up instead of down

For once, we define instead of axiomatizing, thanks to log2

log2_up is always non-negative

The spec of log2_up indeed determines it

log2_up is exact on powers of 2

log2_up and successors of powers of 2

Basic constants

Links between log2 and log2_up

log2_up n is strictly positive for 1<n

Said otherwise, log2_up is null only below 1

log2_up is a monotone function (but not a strict one)

No reverse result for <=, consider for instance log2_up 4 <= log2_up 3

When left side is a power of 2, we have an equivalence for <

When right side is a square, we have an equivalence for <=

Comparing log2_up and identity

log2_up and multiplication. Due to rounding error, we don't have the usual log2_up (a*b) = log2_up a + log2_up b but we may be off by 1 at most

And we can't find better approximations in general.

• The upper bound is exact for powers of 2.
• Concerning the lower bound, for any c>1, take a=b=2^c+1, then log2_up (a*b) = c+c +1 while (log2_up a) = (log2_up b) = c+1

At least, we get back the usual equation when we multiply by 2 (or 2^k)

Two numbers with same log2_up cannot be far away.

log2_up and successor :

• the log2_up function climbs by at most 1 at a time
• otherwise it stays at the same value
• the +1 steps occur after powers of two

log2_up and addition

The sum of two log2_up is less than twice the log2_up of the sum. The large inequality is obvious thanks to monotonicity. The strict one requires some more work. This is almost a convexity inequality for points 2a, 2b and their middle a+b : ideally, we would have 2*log(a+b) >= log(2a)+log(2b) = 2+log a+log b. Here, we cannot do better: consider for instance a=3 b=5, then 2+3<2*3