Computable integer bounds for log

Stream: new members

[Adrian Dole]

Trying some Big-O stuff which is complicated by log being noncomputable. What would really help is some computable function f : Nat -> Nat where f x - 1 <= log x <= f x. Does this exist?

[namibj]

Adrian Dole said:

Trying some Big-O stuff which is complicated by log being noncomputable. What would really help is some computable function f : Nat -> Nat where f x - 1 <= log x <= f x. Does this exist?

If you're ok with a non-natural logarithm, you should be able to use the e.g. base-2 integer/rounded logarithm Nat.log2.

[Adrian Dole]

That’ll work, thanks!