Is there a theorem in Mathlib4 for deriv_const_rpow

Stream: mathlib4

[Samarendra Dash]

Hello,

I’m looking for a lemma in Mathlib4 that states deriv c^x = c^x * Real.log c ?

We have theorems such as Real.hasStrictDerivAt_const_rpow , HasFDerivAt.const_rpow .

but I haven’t found a theorem that directly packages the rule

$$\frac{d}{dx}\,c^x = c^x \cdot \log c.$$

Does such a lemma already exist in Mathlib4, or would it be worthwhile to add one?

Thanks in advance for any pointers!

[Patrick Massot]

@loogle HasDerivAt, Real.log, HPow.hPow

[loogle]

:search: HasDerivAt.rpow, mellin_hasDerivAt_of_isBigO_rpow, and 1 more

[Patrick Massot]

@Samarendra Dash notice how I asked your question to the loogle bot and it replied with useful starting point to explore around.

[Patrick Massot]

Exploring the file containing the first result returned by loogle should be useful.

[Patrick Massot]

That being said, your lemma doesn’t seem to be explicitly stated. You can prove it using

example (c : ℝ) (h : 0 < c) : deriv (fun x : ℝ ↦ c ^ x) = fun x ↦ c^x*(Real.log c) := by
  ext x
  simpa using (hasDerivAt_const x c).rpow (hasDerivAt_id' x) h |>.deriv

but I think it’s fair for users to expect this to be explicitly stated. So I would say you could contribute it to Mathlib.

[Samarendra Dash]

Thank you @Patrick Massot . I had used loogle to find the expressions and I had searched the file. I just didn't understand how use that to solve this problem. Because usually we have explicit deriv_* expressions to help us. Thank you for the help.

[Patrick Massot]

I think a big part of the issue is the following counter-intuitive thing: the most useful theorem are the ones in term of HasDerivAt, not the ones in terms of deriv. In informal math, a course on derivative will typically start with a nice definition of “$f$ is differentiable at $x₀$ if there is some number $a$ such that…”, but then very quickly it will say “in this case the number $a$ is unique and denoted by $f'(x₀)$”. And you will never see statement like: for any positive number $c$, the function $x ↦ c^x$ is differentiable at every $x₀$ with derivative $c^{x₀}\log(c)$. You will rather see a formula as in your first message. But that formula is really a concise (slightly cheating?) way to write the above sentence. In Mathlib it’s not so easy to cheat.

[Patrick Massot]

A more elementary variation of this issue already appears with limits. Whenever you write $\lim_{n → ∞} u_n = l$ you are abusing notations a bit, because it looks like an equality between $\lim_{n → ∞} u_n$ and the number $l$. But this interpretation relies on the incorrect claim that every sequence admits a limit. So it is much closer the mathematical reality to use some notation like $u_n \longrightarrow l$ that doesn’t look like an equality.