nat.log

Stream: general

[Yaël Dillies]

nat.logis only ever used for lemmas about multiplicity and it has the wrong definition for its purpose. nat.log b n is morally floor (real.log n/real.log b) while I claim it should be ceil (real.log n/real.log b). Take for example

theorem nat.prime.multiplicity_factorial {p : ℕ} (hp : nat.prime p) {n b : ℕ} :
nat.log p n < b → multiplicity p n! = ↑∑ (i : ℕ) in finset.Ico 1 b, n / p ^ i

It currently doesn't allow to sum only up to p^i/p^i (when n = p^i). It forces you to sum up to p^i/p^(i + 1). It's morally asking for x ≤ n by requiring floor x + 1 ≤ n, not the correct ceil x ≤ n.

[Yaël Dillies]

Does anybody agree with this rambling? If so, I'll refactor it.

[Kevin Buzzard]

Here's a perhaps related observation. I always thought those computer scientists were funny defining nat.sqrt as floor of the correct sqrt, obviously this is just some random pathological function which is only ever going to be used in algorithms and not proper maths. But browsing through the API I noticed that in fact it formed a Galois connection with the squaring function so this does in some sense justify it, it's a right adjoint to the squaring function on nat. This I found pleasing but also a bit weird because like Yael observes when something isn't integral then who's to say that you shouldn't be taking the ceiling rather than the floor. However then I realized that ceiling of sqrt was the left adjoint to squaring :-) I guess the same thing is happening here. The algorithm people might have a preference though.

[Yaël Dillies]

Yeah! Floor gives you a left adjoint, ceil a right adjoint. How cool is that! I see why the current nat.log could be useful, so maybe I'll just rename it to nat.log_floor and define a new nat.log_ceil.

[Johan Commelin]

How about nat.flog and nat.clog?

[Yaël Dillies]

:rofl: Those are very funky names. But sure, yeah!

[Sebastien Gouezel]

Maybe just nat.log and nat.log_ceil? The floor version looks like the most natural one.

[Mario Carneiro]

Another question that gets you the floor log is "how many digits are in the decimal representation of n"? The answer is nat.log 10 n + 1, except for 0 because humans are afraid of the void (actually nat weirdness happens to coincide with human weirdness in this particular case, so the formula is correct everywhere)