Zulip Chat Archive

Stream: maths

Topic: real powers


view this post on Zulip Chris Hughes (Nov 04 2018 at 15:27):

If we did has_pow real real, what would (-1)^(1/3) be?

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 15:28):

nonono

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 15:28):

real^real is surely not a good idea

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 15:28):

what would (-1)^(1/4) be?

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 15:29):

If you want real^real then I would suggest setting ab=0a^b=0 if a0a\leq 0

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 15:29):

You can make sense of aba^b for aa a positive real and bb any complex number, it should be exp(blog(a))\exp(b\log(a))

view this post on Zulip Johan Commelin (Nov 04 2018 at 15:30):

If you want real^real then I would suggest setting ab=0a^b=0 if a0a\leq 0

I am quite sure you made a typo. That should have been ab=37a^b = 37.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 15:30):

you can make sense of aba^b for aa any non-zero complex number and bb any integer

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 15:30):

I would have put 37 but maybe 0370^{37} should be 0...

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:19):

@Chris Hughes the usual thing: we totalize it. I think for log we can force it to by symmetric. either a long the yy-axis, or through the origin. For power on R\mathbb{R} you might want to have ab=aba^b = |a|^b or similar, and of course 0a=00^a = 0.

view this post on Zulip Chris Hughes (Nov 04 2018 at 16:21):

Don't we want 00=10^0 = 1?

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:22):

I think you want 0^0 = undefined if both those 0's are real numbers

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:22):

I don't think there is a natural choice to totalize it. Theorems about log and pow will always assume that the argument is non-negative.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:22):

and undefined := 0 in Lean

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:22):

Undefined means we are free to choose a value

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:22):

and maybe for pow, 00=10^0 = 1 makes more sense. I don't know.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:22):

There's certainly a case for (0 : real) ^ (0 : nat) = 1

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:23):

Yes: an:R=ana^{n : \mathbb{R}}= a^n should hold

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:24):

so 'real'-power should extend 'int'-power should extend 'nat'-power

view this post on Zulip Chris Hughes (Nov 04 2018 at 16:24):

But that doesn't work if an=ana^n = \mid a\mid^n

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:28):

0^a = 0 unless a = 0, otherwise 1

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:28):

right it doesn't extend int-power. And I don't see a sensible default where it would. we could check if floor or ceil of the argument is odd/even, but this feels too forced

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:28):

I have this in the metamath definition, with the if and everything

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:29):

for negative powers I used complexes, because there was only one definition complex ^ complex, of course that's not an option here

view this post on Zulip Chris Hughes (Nov 04 2018 at 16:29):

In metamath is (1)1/3=1(-1)^{1/3} = -1

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:29):

no, it's e^2pi i/3

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:30):

that ain't no real

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:30):

like I said, complex

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:30):

I don't think we should try for the rational extension, it's crazy and not at all complete

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:30):

okay, what about using a^b = Re (a ^ b)?

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:30):

You want to define the Riemann Zeta function for complex s with Re(s)>1 as the infinite sum of n^{-s}

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:31):

where the left one is on reals and right of the equality is the complex power?

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:31):

that could work...

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:31):

AFAIU it is an extension of int-power and it is continuous

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:32):

except of course where it isn't

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:32):

I think the power function is discontinuous at 0,0 no matter what you do

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:32):

argh, yes

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:32):

not if you restrict the power to be in nat

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:33):

and there is probably a branch cut somewhere that will survive in the real version

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:33):

for example, when evaluating a polynomial, it's essential that x^0 gets sent to 1

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:33):

but that 0 is 0:nat

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:33):

right, I am 100% of the view that 0^0 = 1

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:33):

but my point is that this makes things continuous in this domain of real x nat -> real

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:34):

oh

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:34):

a lot of crazy mathematicians use "everything is continuous" ism to justify claiming that it is undefined there

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:34):

in this case one wants to use pow : nat -> real -> real anyway. I think the case we are discussing now is how to define pow : real -> real -> real

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:34):

but one issue is whether it should extend the nat version

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:34):

of course, that should be easy

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:35):

I agree, it should extend the nat-version. and it would be nice if we could extend the int version in a sensible way

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:35):

extending int should also be possible

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:35):

I know a lot of crazy computer scientists use "everything must extend what we already have in every case even if answers are junk"ism...

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:35):

extending to rat is possible but a bad idea in my view

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:35):

I think (0 : real) ^ (0 : real) is junk so should be 0

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:35):

lolno

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:36):

but (0 : real) ^ (0 : nat) is not junk so should be 1

view this post on Zulip Chris Hughes (Nov 04 2018 at 16:36):

Noooo

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:36):

:-)

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:36):

we don't extend everything. In Isabelle the logarithm of a negative argument is undefined in the sense of a fixed but unknown value

view this post on Zulip Chris Hughes (Nov 04 2018 at 16:36):

But then cast_pow requires proving things are non zero.

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:36):

I was not sure about log of negatives either

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:37):

log of 0 is even worse

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:37):

junk!

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:37):

37

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:37):

log x = log |x| makes some calculus stuff very slightly slicker

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:38):

but I don't think it will come up much anyway

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:38):

What about sgn x * log |x|? I think both have their advantages/disadvantages.

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:38):

whoa

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:38):

what is that for?

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:39):

it looks cool on the graph paper in my head...

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:40):

I think there were some cases where it could have been helpful. But I don't remember the exact statements where it would save some non-negativity assumption. But yes the graph looks nice :-)

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:43):

But x /= 0 -> y /= 0 -> log (x * y) = log x + log y only works for the log x = log |x| case

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:43):

that's a junk theorem!

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:44):

This islike you trying to figure out what the square root of anegative number should be so that sqrt(ab)=sqrt(a)sqrt(b) always works. Nobody who wants to apply that theorem will have a,b<0

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:45):

sometimes a,b>0 but it's a hassle to prove

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:45):

you can't say "x != 0" is any better than "x > 0". It's still a precondition, so tehe user has to supply something

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 16:45):

but sometimes x !=0 is easier to proof than x > 0.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:45):

boggle

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:46):

I mean it is literally a weaker hypothesis

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:46):

if you're in a situation where you're taking logs and you don't have x>0 as a hypothesis then something is seriously wrong with your local context anyway

view this post on Zulip Chris Hughes (Nov 04 2018 at 16:46):

Proving things are >0>0 is cheap on paper but expensive in lean. Keeping track of which theorems are randomly true for some non-intuitive definition is cheap in Lean but expensive on paper.

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:46):

you had it in your context once, then you did 5 rewrites and it's not obviously true any more

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:47):

I did see that in a 1st year's code recently -- "let H2 := H,..." and I thought "wooah what is this fool doing?" and then I understood that they wanted to rewrite H but keep track of it anyway

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:49):

those could be some combination of rewrites to the log(s) and rewrites to the hypothesis too

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:49):

What are the preconditions to log (log (log x + 1)) < 3?

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:50):

x>>0

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:50):

but not too >> or else it won't be < 3 :)

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:50):

If it's too >> then it's false. If it's not >> enough then it makes no sense

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:51):

it's NaN

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:51):

unfortunately (or fortunately), real has no NaN

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:51):

just ask anyone who has dealt with IEEE floats, NaN is a mess

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:51):

If you say to a mathematician "this is true for x=20" they will assume you mean that the LHS evaluates to something meaningful in maths

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:52):

right, and that's one of the more expensive in lean things to do

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:53):

you might think "we could just have preconditions on log and then it would all make sense" but that would just make the problem worse

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:53):

I think we need a with_NaN structure

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:54):

with_bot?

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:54):

but it might not be a bottom

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:54):

or equal to itself..

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:54):

well obviously we'd have to modify eq

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:54):

obviously

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:55):

we need not_a_Type

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:55):

or not_a_term or something

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:56):

it was silly of us to assume that all types have a reflexive relation... we should generalize to semitypes

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:56):

rofl that's clearly what these guys have been missing for the last 100 years

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:56):

we realised we needed semimodules

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:56):

it was only a matter of time before we had the real breakthrough

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:57):

I joke, but PERs (partial equivalence relations) as types are a thing

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:57):

nuprl uses it

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:57):

is that where you drop reflexivity?

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:57):

yeah

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:58):

so you get equivalence classes and then some wasteland

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:58):

of terms which are related to nothing

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:58):

it's just an equivalence relation on a subtype

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 16:58):

right

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:58):

In type theory it has the purpose of rolling subtyping and quotients into one construct

view this post on Zulip Mario Carneiro (Nov 04 2018 at 16:59):

so you get some nice categorical structure


Last updated: May 10 2021 at 08:14 UTC