Zulip Chat Archive

Stream: Is there code for X?

Topic: real powers of positive reals?


view this post on Zulip 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

view this post on Zulip Jalex Stark (Apr 29 2020 at 23:01):

Maybe the thing I said is already the right definition

view this post on Zulip 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 ?

view this post on Zulip Jalex Stark (Apr 29 2020 at 23:03):

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

view this post on Zulip 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 ζ(s)\zeta(s) is defined, for ss a complex number with real part greater than one, to be the infinite sum 1s+2s+3s+1^s+2^s+3^s+\cdots and here the convention is that if rr is a positive real and ss is a complex number then rsr^s is defined as exp(s log r) and this function has good properties. For r0r\leq0 it's a nightmare and you probably want to let it be zero -- but here's the catch! If rr is a negative real and ss is an integer then rsr^s makes perfect sense and isn't zero, so one would have to be careful with coercions.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Apr 29 2020 at 23:22):

There already is a real to the power real instance.

view this post on Zulip Chris Hughes (Apr 29 2020 at 23:23):

I don't remember it's junk behaviour.

view this post on Zulip Chris Hughes (Apr 29 2020 at 23:24):

It might have actually just changed now that log changed.

view this post on Zulip Kevin Buzzard (Apr 29 2020 at 23:27):

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

view this post on Zulip 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 : )

view this post on Zulip Chris Hughes (Apr 30 2020 at 00:26):

Should be in analysis.complex.exponential

view this post on Zulip Jalex Stark (Apr 30 2020 at 00:44):

Thanks!

view this post on Zulip 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