complex powers of positive reals

Stream: Is there code for X?

[Alex Kontorovich]

Do we have tactics that handle something like this?

import Mathlib

lemma Complex.cpow_neg_eq_inv_pow_ofReal_pos {a : ℝ} (ha : 0 < a) (r : ℂ) :
    (a : ℂ) ^ (-r) = (a⁻¹ : ℂ) ^ r := by
  -- exact? fails
  -- apply? junk
  -- rw? suggests `rw [cpow_neg]`
  -- simp? no progress
  sorry

Or must it be done "by hand"?... If I take the suggestion of rw?, then I still need:

import Mathlib

lemma Complex.cpow_inv_ofReal_pos {a : ℝ} (ha : 0 < a) (r : ℂ) :
    ((a : ℂ) ^ r)⁻¹ = (a : ℂ)⁻¹ ^ r := by
  -- exact? fails
  -- apply? junk
  -- rw? junk
  -- simp? no progress
  sorry

Should things like this be added to Mathlib?... Thanks!

[Vincent Beffara]

"by hand" kind of works

lemma Complex.cpow_neg_eq_inv_pow_ofReal_pos {a : ℝ} (ha : 0 < a) (r : ℂ) :
    (a : ℂ) ^ (-r) = (a⁻¹ : ℂ) ^ r := by
  have : arg ↑a ≠ Real.pi := by simp [Complex.arg_ofReal_of_nonneg ha.le, Real.pi_ne_zero.symm]
  simp only [← Complex.cpow_eq_pow, cpow, ofReal_eq_zero, ha.ne.symm, ↓reduceIte, mul_neg, inv_eq_zero]
  congr
  simp [Complex.log_inv _ this]

[Alex Kontorovich]

Indeed, but is quite painful, no? Could tactics be developed to make it more reasonable? (Alternatively, add a bunch of things like this to the API...?)

[Ruben Van de Velde]

What would the scope be of a tactic that can solve this?

[Yaël Dillies]

This just sounds like API lemmas to me

[Vincent Beffara]

lemma toto (x : ℝ) (hx : 0 < x) (y : ℂ) : (x : ℂ) ^ y = Complex.exp (Real.log x * y) := by
  simp [← Complex.cpow_eq_pow, Complex.cpow, hx.ne.symm, ← Complex.ofReal_log hx.le]

lemma Complex.cpow_neg_eq_inv_pow_ofReal_pos {a : ℝ} (ha : 0 < a) (r : ℂ) :
    (a : ℂ) ^ (-r) = (a⁻¹ : ℂ) ^ r := by
  norm_cast
  rw [toto _ ha, toto _ (inv_pos.mpr ha)]
  simp

[Vincent Beffara]

One might like to turn toto into a @[simp] lemma ? It does not turn the second proof into by simp [ha] because simp wants to revert the norm_cast.

[Vincent Beffara]

But this works and looks better:

lemma toto {x : ℝ} (hx : 0 < x) {y : ℂ} : (x : ℂ) ^ y = Complex.exp (Real.log x * y) := by
  simp [← Complex.cpow_eq_pow, Complex.cpow, hx.ne.symm, ← Complex.ofReal_log hx.le]

lemma Complex.cpow_neg_eq_inv_pow_ofReal_pos {a : ℝ} (ha : 0 < a) (r : ℂ) :
    (a : ℂ) ^ (-r) = (a⁻¹ : ℂ) ^ r := by
  norm_cast
  simp only [toto, ha, inv_pos.mpr ha, mul_neg, Real.log_inv, ofReal_neg, neg_mul]

[llllvvuu]

rw_search kind of works:

lemma Complex.cpow_neg_eq_inv_pow_ofReal_pos {a : ℝ} (ha : 0 < a) (r : ℂ) :
    (a : ℂ) ^ (-r) = (a⁻¹ : ℂ) ^ r := by
  rw [cpow_neg, Complex.inv_cpow]
  exact slitPlane_arg_ne_pi (.inl ha)

(it finds the first rw term, the second one I moogled, and the exact I exact?ed)

I wonder why it didn't find the second rw term. Does it consider rw lemmas that generate side conditions?

[Vincent Beffara]

Ah, that's cool. apply? finds the second step:

lemma Complex.cpow_neg_eq_inv_pow_ofReal_pos' {a : ℝ} (ha : 0 < a) (r : ℂ) :
    (a : ℂ) ^ (-r) = (a⁻¹ : ℂ) ^ r := by
  rw [cpow_neg] -- from rw_search
  refine (inv_cpow (↑a) r ?hx).symm -- from apply?
  exact slitPlane_arg_ne_pi (Or.inl ha) -- from exact?

[llllvvuu]

Now having intrusive thoughts about how well a deep q learning based rw_search would perform vs the current Levenshtein edit distance based one :thinking: