[Merged by Bors] - feat(analysis/special_functions/{log, pow}): add log_base

[BoltonBailey]

Adds real.logb, the log base b of x, defined as log x / log b. Proves that this is related to real.rpow.

---

[BoltonBailey]

I'm willing to hear comments on how to handle the proliferation of one_lt_b everywhere in the file. Should I prove these lemmas for 0 < b < 1 as well? If so, how should I name all these lemmas? Should I write simp lemmas of the form log b x < log b y \iff <some expression on inequalities>? My thinking is the-1 < b < 0 and b < -1 ranges are probably not worth the time to write them all.

[BoltonBailey]

I've opened a discussion on the naming of this new function on Zulip

[dupuisf]

Regarding the one_lt_b issue, I think a good way to deal with it would be via the typeclass system, as is done in docs#pi_Lp (see how fact_one_le_p is used in that file).

[BoltonBailey]

@dupuisf Do you like this better than the suggestion from Zulip of using include without involving the typeclass system? I prefer not using it, since fact confuses me, and my understanding is that it should only be used when you actually need to infer another typeclass from it (such as inferring field from fact p.prime). Also, it seems like when I make this change all the lemma proofs get longer.

For example
by rw [←rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one hb) hx]
becomes
by {rw [←rpow_le_rpow_left_iff hb.out, rpow_logb (b_pos) (b_ne_one) hx], assumption, assumption, }

Also, presumably this way if someone calls library_search for one of these lemmas with the vanilla argument, it won't be found.

[dupuisf]

I don't have a particular preference for that solution, I thought it was an idea that could be tried out. So if you've tried it out and it's not great, let's just stick with the current version.

bors d+

[bors]

✌️ BoltonBailey can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[BoltonBailey]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests