real powers

Stream: maths

[Chris Hughes]

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

[Kevin Buzzard]

nonono

[Kevin Buzzard]

real^real is surely not a good idea

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

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

[Kevin Buzzard]

you can make sense of $a^b$ for $a$ any non-zero complex number and $b$ any integer

[Kevin Buzzard]

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

[Johannes Hölzl]

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

[Chris Hughes]

Don't we want $0^0 = 1$?

[Kevin Buzzard]

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

[Johannes Hölzl]

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.

[Kevin Buzzard]

and undefined := 0 in Lean

[Johannes Hölzl]

Undefined means we are free to choose a value

[Johannes Hölzl]

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

[Kevin Buzzard]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Johannes Hölzl]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Kevin Buzzard]

that ain't no real

[Mario Carneiro]

like I said, complex

[Mario Carneiro]

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

[Johannes Hölzl]

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

[Kevin Buzzard]

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

[Johannes Hölzl]

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

[Mario Carneiro]

that could work...

[Johannes Hölzl]

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

[Mario Carneiro]

except of course where it isn't

[Mario Carneiro]

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

[Johannes Hölzl]

argh, yes

[Kevin Buzzard]

not if you restrict the power to be in nat

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

but that 0 is 0:nat

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

oh

[Mario Carneiro]

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

[Johannes Hölzl]

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

[Kevin Buzzard]

but one issue is whether it should extend the nat version

[Mario Carneiro]

of course, that should be easy

[Johannes Hölzl]

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

[Mario Carneiro]

extending int should also be possible

[Kevin Buzzard]

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...

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

lolno

[Kevin Buzzard]

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

[Chris Hughes]

Noooo

[Kevin Buzzard]

:-)

[Johannes Hölzl]

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

[Chris Hughes]

But then cast_pow requires proving things are non zero.

[Mario Carneiro]

I was not sure about log of negatives either

[Mario Carneiro]

log of 0 is even worse

[Kevin Buzzard]

junk!

[Kevin Buzzard]

37

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johannes Hölzl]

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

[Mario Carneiro]

whoa

[Mario Carneiro]

what is that for?

[Mario Carneiro]

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

[Johannes Hölzl]

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 :-)

[Johannes Hölzl]

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

[Kevin Buzzard]

that's a junk theorem!

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Johannes Hölzl]

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

[Kevin Buzzard]

boggle

[Mario Carneiro]

I mean it is literally a weaker hypothesis

[Kevin Buzzard]

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

[Chris Hughes]

Proving things are $>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.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

x>>0

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

it's NaN

[Mario Carneiro]

unfortunately (or fortunately), real has no NaN

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I think we need a with_NaN structure

[Mario Carneiro]

with_bot?

[Kevin Buzzard]

but it might not be a bottom

[Mario Carneiro]

or equal to itself..

[Kevin Buzzard]

well obviously we'd have to modify eq

[Mario Carneiro]

obviously

[Kevin Buzzard]

we need not_a_Type

[Kevin Buzzard]

or not_a_term or something

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

we realised we needed semimodules

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

nuprl uses it

[Kevin Buzzard]

is that where you drop reflexivity?

[Mario Carneiro]

yeah

[Kevin Buzzard]

so you get equivalence classes and then some wasteland

[Kevin Buzzard]

of terms which are related to nothing

[Mario Carneiro]

it's just an equivalence relation on a subtype

[Kevin Buzzard]

right

[Mario Carneiro]

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

[Mario Carneiro]

so you get some nice categorical structure