# Zulip Chat Archive

## 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`

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

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