Real.logb in lean4

Stream: new members

[Rahul Saha]

Hello, I am trying to convert the following lean 3 code to lean 4.

theorem aime_1984_p5
  (a b : ℝ)
  (h₀ : real.logb 8 a + real.logb 4 (b^2) = 5)
  (h₁ : real.logb 8 b + real.logb 4 (a^2) = 7) :
  a * b = 512 :=
  sorry

Using mathlib port produced

theorem aime_1984_p5 (a b : ℝ) (h₀ : Real.logb 8 a + Real.logb 4 (b ^ 2) = 5)
    (h₁ : Real.logb 8 b + Real.logb 4 (a ^ 2) = 7) : a * b = 512 := by sorry

But upon checking the github for mathlib4, there does not appear to be a logb in Real. Instead, there is one inside Analysis.SpecialFucntions.Functions.Log. I am wondering if this is the intended place to import logb from. Thank you!

[Ruben Van de Velde]

docs3#real.logb shows that it was also in that file in mathlib 3

[Rahul Saha]

@Ruben Van de Velde yep, it's why i am slightly confused by this reorganization.

[Rahul Saha]

also its not a reorganization - the log in analysis is also present in mathlib 3

[Rahul Saha]

it appears to be in the docs for mathlib4 - https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Log/Base.html#Real.logb

[Rahul Saha]

but it links to the a file that is not Real.logb

[Kevin Buzzard]

So you need to import Mathlib.Analysis.SpecialFunctions.Log.Base

[Ruben Van de Velde]

logb is a definition, not a file, and it's defined in the same place in mathlib 3 and 4

[Rahul Saha]

Ah I see, okay, I was being dum. Thank you.