Redefine `rpow`?

Stream: maths

[Yury G. Kudryashov]

What do you think about using exp (b * log a) as the definition of a ^ b for real a and b (with usual exceptions for a = 0)? Some pros and cons I see:

• pro: we can define a ^ b (and Lp spaces) before we have π and inverse trig functions;
• pro: probably easier simp lemmas for a ^ b, a < 0;
• con: we loose equalities about real.rpow and complex.cpow.

Another possibility is to make a new definition propositionally equal to the current one, just write it explicitly.

[Kevin Buzzard]

I would be very happy if this was even the definition for a real and b complex

[Kevin Buzzard]

this is the definition which is easiest to work with when doing Dirichlet series (like the Riemann zeta function defined as an infinite sum)

[Kevin Buzzard]

but this is a definition question so I guess I'm not really the right person to answer

[Sebastien Gouezel]

There is the problem that with your definition you don't have a ^ (3 : N) = a ^ (3 : R) for negative a, right? I think this is a non-negotiable property I want to have of my power function.

[Yury G. Kudryashov]

You're right.

[Yury G. Kudryashov]

I'll think about it.

[Yaël Dillies]

Btw this property is unknown to norm_cast. Is it intended?

[Sebastien Gouezel]

Giving an explicit formula directly, without going through all the complex stuff, looks like a good idea to me, though.

[Sebastien Gouezel]

Except that the explicit formula uses cos and pi...

[Yury G. Kudryashov]

Exactly.

[Yury G. Kudryashov]

So, we need large parts of inverse trig functions anyway.

[Yury G. Kudryashov]

Then I'm not sure that removing complex.log/complex.cpow as dependencies is worth it.

[Sebastien Gouezel]

Yes, I agree.