real powers of positive reals?

Stream: Is there code for X?

[Jalex Stark]

I feel like we should have a function
pow (a x : \R) \to \R which is equal to 0 (or 37 :) ) if a is negative and agrees with exp(x log a) otherwise

[Jalex Stark]

Maybe the thing I said is already the right definition

[Jalex Stark]

If we had this function, would it make sense to use it an as instance of has_pow \R \R ?

[Jalex Stark]

I guess I'm still asking a silly question, I can just try to do this

[Kevin Buzzard]

There has been some discussion of powers in the past, including some debunking of attempts to attach a meaning to various notions of powers, but the Riemann zeta function $\zeta(s)$ is defined, for $s$ a complex number with real part greater than one, to be the infinite sum $1^s+2^s+3^s+\cdots$ and here the convention is that if $r$ is a positive real and $s$ is a complex number then $r^s$ is defined as exp(s log r) and this function has good properties. For $r\leq0$ it's a nightmare and you probably want to let it be zero -- but here's the catch! If $r$ is a negative real and $s$ is an integer then $r^s$ makes perfect sense and isn't zero, so one would have to be careful with coercions.

[Kevin Buzzard]

I guess the coercion claim can be made subject to hypotheses, analogous to claims about subtraction on naturals and integers only being equal under an inequality assumption

[Kevin Buzzard]

So in summary I would be happy to see it as an instance for has_pow \R \C and has_pow \R \R with the convention that it's zero if r<0

[Kevin Buzzard]

It's hard to imagine someone taking a negative number to a negative integer power and then wanting to coerce the integer to a real and expecting good things to happen

[Kevin Buzzard]

Actually after the change in log today one could let the log definition work for all nonzero r

[Chris Hughes]

There already is a real to the power real instance.

[Chris Hughes]

I don't remember it's junk behaviour.

[Chris Hughes]

It might have actually just changed now that log changed.

[Kevin Buzzard]

Oh you can't have R to C to C for a power!

[Jalex Stark]

Chris Hughes said:

There already is a real to the power real instance.

Where is it defined? I don't have it with this import list:

import data.real.basic
import data.complex.exponential
import analysis.asymptotics

#check (1 : ℝ)^(1 : ℝ)

[Chris Hughes]

Should be in analysis.complex.exponential

[Jalex Stark]

Thanks!

[Jalex Stark]

I think now it is in analysis.special_functions.pow