Cube Root

Stream: new members

[Callum Cassidy-Nolan]

Hi there, I was wondering what's the best way of working with x^(1/3) as a function R -> R.

I had been using it freely until I remembered that if x < 0 then I don't think real.pow cuts it (since the output could be a complex in that case).

So would the best way to deal with this to be to use complex.cpow, and force it to be R with coercions?

[Mario Carneiro]

What function do you want? If you only need the nonnegative values then x^(1/3) is fine

[Eric Rodriguez]

this is not the cube root you'll want; (-1 : ℝ) ^ ((1 : ℝ) / 3) = real.cos (real.pi * 3⁻¹)

[Mario Carneiro]

I forget how rpow is defined on negative numbers but I guess it's probably projecting from complex like you describe, so you won't get the nice answer for negative numbers and instead get what Eric said

[Bryan Gin-ge Chen]

(This doesn't answer the main question here, but there was a fun thread about the cube root function last year that I feel compelled to link: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Cube.20root.20of.20cubic.20is.20id.3F/near/222997128 )

[Callum Cassidy-Nolan]

Mario Carneiro said:

What function do you want? If you only need the nonnegative values then x^(1/3) is fine

I'm looking for the function which comes from this graph as a function R -> R: image.png

[Callum Cassidy-Nolan]

Eric Rodriguez said:

this is not the cube root you'll want; (-1 : ℝ) ^ ((1 : ℝ) / 3) = real.cos (real.pi * 3⁻¹)

Where can I learn more about that formula?

[Eric Rodriguez]

docs#complex.cpow

[Eric Rodriguez]

(note that the real power is defined as the real part of that)

[Callum Cassidy-Nolan]

The complex power function x^y, given by x^y = exp(y log x) (where log is the principal determination of the logarithm), unless x = 0 where one sets 0^0 = 1 and 0^y = 0 for y ≠ 0.

Where did your cos come from?

[Mario Carneiro]

Here's what it looks like: cube-root.png

[Mario Carneiro]

the function is $\Re[\exp(y\log x)]$

[Eric Rodriguez]

Callum Cassidy-Nolan said:

The complex power function x^y, given by x^y = exp(y log x) (where log is the principal determination of the logarithm), unless x = 0 where one sets 0^0 = 1 and 0^y = 0 for y ≠ 0.

Where did your cos come from?

maybe this code wil explain some:

import analysis.special_functions.pow

example : (-1 : ℂ) ^ ((1 : ℂ) / 3) = complex.cos (↑real.pi * 3⁻¹) + complex.sin (↑real.pi * 3⁻¹) * complex.I :=
begin
  rw complex.cpow_def,
  simp,
  rw [complex.log_neg_one, mul_comm (real.pi : ℂ), mul_assoc, mul_comm, complex.exp_mul_I],
end

[Mario Carneiro]

There are three solutions to x^3 = a in the complex plane, which form a triangle with one point on the real line and the other two above and below the line. For positive x we pick the solution that lies on the real line, and for negative x we pick the one at 60 degrees up

[Mario Carneiro]

and then project down to the real line again to get the real function. That's why the negative function is the reflection of the positive one but scaled down by 1/2

[Callum Cassidy-Nolan]

What is ite ? image.png

[Mario Carneiro]

if-then-else

[Mario Carneiro]

it has the syntax if c then t else e

[Callum Cassidy-Nolan]

Callum Cassidy-Nolan said:

Eric Rodriguez said:

this is not the cube root you'll want; (-1 : ℝ) ^ ((1 : ℝ) / 3) = real.cos (real.pi * 3⁻¹)

Where can I learn more about that formula?

What would the general version x^(1/3) look like as R -> R rather than just (-1)^1/3) ?

[Mario Carneiro]

I plotted it above

[Mario Carneiro]

for negative x it is (-x)^(1/3) / 2