## Stream: Is there code for X?

### Topic: real powers of positive reals?

#### Jalex Stark (Apr 29 2020 at 23:00):

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 (Apr 29 2020 at 23:01):

Maybe the thing I said is already the right definition

#### Jalex Stark (Apr 29 2020 at 23:02):

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

#### Jalex Stark (Apr 29 2020 at 23:03):

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

#### Kevin Buzzard (Apr 29 2020 at 23:15):

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 (Apr 29 2020 at 23:16):

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 (Apr 29 2020 at 23:18):

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 (Apr 29 2020 at 23:19):

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 (Apr 29 2020 at 23:22):

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

#### Chris Hughes (Apr 29 2020 at 23:22):

There already is a real to the power real instance.

#### Chris Hughes (Apr 29 2020 at 23:23):

I don't remember it's junk behaviour.

#### Chris Hughes (Apr 29 2020 at 23:24):

It might have actually just changed now that log changed.

#### Kevin Buzzard (Apr 29 2020 at 23:27):

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

#### Jalex Stark (Apr 30 2020 at 00:15):

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 (Apr 30 2020 at 00:26):

Should be in analysis.complex.exponential

Thanks!

#### Jalex Stark (Apr 30 2020 at 15:01):

I think now it is in  analysis.special_functions.pow

Last updated: May 17 2021 at 14:12 UTC