How to prove (x^ (1/3 : ℝ))^(3:ℝ) = x

Stream: new members

[RedPig]

Is this true of false, I think it is well defined for negative numbers

import Mathlib
example (x:ℝ) : (x^ (1/3 : ℝ))^(3:ℝ) = x := by sorry
-- Real.rpow_mul requires positivity on x

The Real.rpow_mul requires positivity on x.

[Kevin Buzzard]

That is false for negative x

[Kevin Buzzard]

Somewhere I recently posted a proof that (-1)^(1/3)=1/2

[Etienne Marion]

Although in principle you could define $x^{1/3}$ for $x < 0$ in practice it is not useful because the usual rules for power won't apply properly. For instance you would like to say that $(-1)^{1/3} = -1$ but if power rules applied you could also write $(-1)^{1/3} = (-1)^{2/6} = (-1)^{2 \times 1/6} = ((-1)^2)^{1/6} = 1^{1/6} = 1$, and you'd get a contradiction.

[Kevin Buzzard]

#lean4 > ✔ Weird `ring`performance and how to simplify `(x^3)^(1/3)` @ 💬

My proof exhibits a non-confluence issue in simp BTW.

[RedPig]

Thank you, this is interesting! What is the best way to manually define the $x^{1/3}$ in the usual math context, maybe by defining an odd function where the positive part is given by $x^{1/3}$ ? or the inverse of $x^3$?

[RedPig]

Kevin Buzzard said:

That is false for negative x

Interesting! I guess that is because of the exp (y log x) cos (π y) part?

[Kevin Buzzard]

RedPig said:

Thank you, this is interesting! What is the best way to manually define the $x^{1/3}$ in the usual math context, maybe by defining an odd function where the positive part is given by $x^{1/3}$ ? or the inverse of $x^3$?

If x>=0 then x^{1/3} else -((-x)^{1/3}).

[Weiyi Wang]

I remember one of the things I checked immediately when I learned mathlib was to check how Real.pow is defined, because I know it is totally a mess for negative numbers. I am somewhat surprised it is not all 0 for negative inputs

[Sébastien Gouëzel]

You want (-1) ^ x to coincide with the integer power when x is an integer, for instance (-1) ^ (1 : ℝ) should be -1. So taking (-1) ^ x = 0 uniformly is not a good choice. You could take (-1) ^ x = 0 if x is not an integer, and 0 otherwise, but this is not continuous so not very nice. The choice we have is analytic and works fine for integer powers, so it is pretty good!

[Bohan Lyu]

(x:ℝ) : (x^ (1/3 : ℝ))^(3:ℝ) = x is incorrect
(x : ℂ) : (x ^ ((3 : ℕ)⁻¹ : ℂ)) ^ (3 : ℕ) = x is correct
I will provide the respective disproof and proof

[Bohan Lyu]

disproof of the first statement

import Mathlib

-- Disproof of the statement ∀ x : ℝ, (x ^ (1/3 : ℝ)) ^ (3 : ℝ) = x
theorem cube_root_cubed_is_false : ¬ (∀ x : ℝ, (x ^ (1/3 : ℝ)) ^ (3 : ℝ) = x) := by
  push_neg
  use -1
  -- Goal: ((-1 : ℝ) ^ (1 / 3 : ℝ)) ^ (3 : ℝ) ≠ -1

  -- Calculate (-1)^(1/3)
  have hcbrt : (-1 : ℝ) ^ (1 / 3 : ℝ) = 1 / 2 := by
    have h_neg_one_lt_zero : (-1 : ℝ) < 0 := by norm_num
    rw [Real.rpow_def_of_neg h_neg_one_lt_zero]
    -- Goal: Real.exp (Real.log (-1) * (1 / 3)) * Real.cos ((1 / 3) * Real.pi) = 1 / 2

    rw [Real.log_neg_eq_log 1] -- Rewrites log (-1) to log 1
    -- Goal: Real.exp (Real.log 1 * (1 / 3)) * Real.cos ((1 / 3) * Real.pi) = 1 / 2

    rw [Real.log_one, zero_mul, Real.exp_zero, one_mul]
    -- Goal now: Real.cos ((1 / 3) * Real.pi) = 1 / 2

    -- Normalize the argument to cos to match Real.cos_pi_div_three
    rw [mul_comm] -- Changes goal to Real.cos (Real.pi * (1 / 3)) = 1 / 2
    -- We need the argument to be Real.pi / 3.
    -- Division is defined as multiplication by the inverse.
    -- We can assert that Real.pi * (1/3) = Real.pi / 3
    have arg_eq : Real.pi * (1 / 3) = Real.pi / 3 := by
      field_simp -- Use field_simp to handle division/multiplication identities
      -- Or: rw [div_eq_mul_inv]
    rw [arg_eq] -- Now the goal is Real.cos (Real.pi / 3) = 1 / 2
    rw [Real.cos_pi_div_three] -- Apply known value

  -- Substitute the calculated value
  rw [hcbrt]
  -- Goal: (1 / 2 : ℝ) ^ (3 : ℝ) ≠ -1

  -- Let norm_num handle the final computation and comparison
  norm_num

[Bohan Lyu]

Proof of the second proof

import Mathlib

theorem complex_cube_root_cubed_eq_self (x : ℂ) : (x ^ ((3 : ℕ)⁻¹ : ℂ)) ^ (3 : ℕ) = x := by
  have h3 : (3 : ℕ) ≠ 0 := by decide
  exact Complex.cpow_nat_inv_pow x h3

[Jireh Loreaux]

If you want the function that you originally conceived, you should use x ↦ x.sign * |x| ^ (1 / 3 : ℝ)

[Kevin Buzzard]

This is better than my suggestion (if then else) because you don't have to constantly split the ifs, you'll be able to use lemmas in the library like x.sign * |x| = x etc.