Basic help with logarithms

Stream: general

[J Li]

Hi, I'm new here and have a simple question. I just installed Lean with mathlib following https://leanprover-community.github.io/install/project.html in Lean 4. I imported "import Mathlib.Data.Nat.Log" and am trying to use expressions like "log 2 8" but getting the error "function expected at log, term has type ?m.15". I'm not sure what this means. Could someone please advise?

[J Li]

Another question: say I am looking for a logarithm function in mathlib, what's the easiest way to search for it?

[Moritz Doll]

You need to either open Nat or write Nat.log 2 8

[J Li]

Thanks, is there any way to do it for real numbers?

[Moritz Doll]

yes, docs#Real.log

[J Li]

so to use this I would need to do import Mathlib.Analysis.SpecialFunctions.Log.Basic, and then how do I call the log function?

[J Li]

any reason Basic.Real.log doesn't work?

[J Li]

i'm getting this error failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Real.instDivisionRingReal', and it does not have executable code

[Moritz Doll]

yes, you need to import the corresponding file and the real logarithm is called Real.log not Basic.Real.log. Note also that you cannot evaluate the logarithm, but you can prove things about it.

[J Li]

sorry, why can't I evaluate the logarithm?

[Ruben Van de Velde]

The real numbers are implemented in mathlib in a way that doesn't support direct evaluation, but you could use #norm_num Real.log 1 if I'm getting the syntax right

[Mario Carneiro]

norm_num does not know logarithms, although that particular example can be solved by simp

[Ruben Van de Velde]

Well, if anything is going to work here in some generality, it's norm_num. That doesn't mean it already works, though

[Mario Carneiro]

well, there is the fundamental issue that it's not clear what you would want Real.log 2 to "evaluate" to

[Mario Carneiro]

keeping in mind that norm_num is not an approximation tactic, it proves equalities