Prove that `(-3 : ℂ)^(1/2 : ℂ) = √3 * I`

Stream: new members

[张守信(Shouxin Zhang)]

It's trivial in math. Just using the cpow def. I'm wondering if there's an simple way done it using one line simp [xxx] in Lean?

import Mathlib

open Complex

example :
  (-3 : ℂ)^(1/2 : ℂ) = √3 * I := by
  rw [cpow_def]
  simp
  rw [show log (-3) = log 3 + Real.pi * I by
    unfold log
    simp
    refine arg_eq_pi_iff_lt_zero.mpr ?_
    rw [@neg_iff]
    simp]
  field_simp
  rw [add_div, exp_add]
  rw [show log 3 / 2 = log ((√3 : ℂ)) by
    rw [← Complex.ofReal_log (by simp), ← ofReal_ofNat]
    rw [← Complex.ofReal_log (by simp)]
    norm_cast
    field_simp
    rw [mul_comm]
    rw [← Real.log_rpow (by simp)]
    simp]
  rw [show cexp (log (√3 : ℂ)) = (√3 : ℂ) by
    refine exp_log ?_
    simp]
  congr 1
  show cexp (↑Real.pi * I / 2) = I
  rw [show ↑Real.pi * I / 2 = (↑Real.pi / 2) * I by ring_nf]
  rw [Complex.exp_mul_I]
  simp

[张守信(Shouxin Zhang)]

I know Complex.sq_cpow_two_inv is useful for some cases, but seems unuseful in this case. Since it needs the real part nonneg.

[张守信(Shouxin Zhang)]

I think maybe we should had a rw lemma like If a is a pos real number, then (-a : ℂ)^(1/2 : ℂ) = √a * I.

[Kevin Buzzard]

Do we have much API at all for raising complex numbers to complex powers? This is not a well-behaved notion, is it? Why have you ended up wanting to do this? Surely it would be better to raise a complex number to a real power? This is a much better-behaved function.

[Kevin Buzzard]

Oh wait -- we don't even have complex number to real or rational power??

[张守信(Shouxin Zhang)]

Kevin Buzzard said:

Do we have much API at all for raising complex numbers to complex powers? This is not a well-behaved notion, is it? Why have you ended up wanting to do this? Surely it would be better to raise a complex number to a real power? This is a much better-behaved function.

I want to prove the following example( $\sqrt{1+\sqrt{-3}}+\sqrt{1-\sqrt{-3}} = \sqrt{6}$), so the first step is the beginning thing.

example :
  (1 + (-3 : ℂ)^(1/2 : ℂ))^(1/2 : ℂ) + (1 - (-3 : ℂ)^(1/2 : ℂ))^(1/2 : ℂ) = √6  := by
  sorry

[张守信(Shouxin Zhang)]

Kevin Buzzard said:

Oh wait -- we don't even have complex number to real or rational power??

Yeah. That's really unfortunate; we definitely should have nice things like this!

[Kevin Buzzard]

I have a family lunch to go to so I need to stop thinking about this, but two last thoughts: firstly I nearly finished my version of the proof

import Mathlib

open Complex

example : (-3 : ℂ) ^ (1 / 2 : ℂ) = √3 * I := by
  rw [cpow_def_of_ne_zero (by norm_num)]
  rw [show (-3 : ℂ) = (-1 : ℂ) * (3 : ℝ) by norm_num,
    Complex.log_mul (by norm_num) (by norm_num) (by simp [Real.pi_pos]),
    show (1 / 2 : ℂ) = (1 / 2 : ℝ) by norm_num,
    log_neg_one, add_mul, exp_add, mul_comm _ (exp _), ← Complex.ofReal_log (by norm_num)]
  congr 1
  · norm_cast
    rw [Real.exp_mul, Real.exp_log (by norm_num), Real.sqrt_eq_rpow 3]
  · sorry

(the sorry should basically be in the library, it's $e^{i\pi/2}=i$) and secondly, I think that to prove things about $\sqrt{-1+\sqrt{-3}}$ you should first prove $1+\sqrt{-3}=2e^{i\pi/3}$ and then things will be much easier to manipulate.

[Kevin Buzzard]

张守信(Shouxin Zhang) said:

Kevin Buzzard said:

Oh wait -- we don't even have complex number to real or rational power??

Yeah. That's really unfortunate; we definitely should have nice things like this!

Thinking about it, I guess the problem is the complex base not the complex power, as that's where the branch cut is, so maybe the logic is that with a complex base you're always going to have issues with checking args so you may as well have complex powers