Cube root of cubic is id?

Stream: new members

[Sandy Maguire]

I'm trying to prove

z: ℝ
⊢ (z ^ 3) ^ 3⁻¹ = z

and having one heck of a hard time. I'd assume there's a lemma somewhere for this, but i can't find it and norm_num is no help. Any tips?

[Sandy Maguire]

There are lots of pow_muls for nats, but none for reals afaict

[Bryan Gin-ge Chen]

The real power function is in analysis.special_functions.pow:

import analysis.special_functions.pow

example (z : ℝ) (h : 0 ≤ z) : (z ^ (3 : ℝ)) ^ (3 : ℝ)⁻¹ = z :=
begin
  rw ← real.rpow_mul h,
  norm_num,
end

[Patrick Massot]

Sandy, you need to learn about #mwe in order to help people helping you.

[Sandy Maguire]

@Patrick Massot mind being more specific about that?

[Patrick Massot]

Did you follow the link?

[Patrick Massot]

It's pretty specific.

[Sandy Maguire]

@Bryan Gin-ge Chen thanks, that's helpful. tho i think this is true even for negative x in the case of y = 3, z = 3^-1

[Sandy Maguire]

well wolfram alpha disagrees with me :)

[Sandy Maguire]

@Patrick Massot my confusion here is that i don't see how the problem statement doesn't pose enough information. hypothetically, what could be going wrong that me giving you the imports would help clarify?

[Sandy Maguire]

are there lots of ^s i need to worry about?

[Patrick Massot]

The type of 3 is one crucial thing here, and it comes with ^.

[Bryan Gin-ge Chen]

Also it's just much more convenient to copy and paste working code than having to figure out which imports and namespaces are needed...

[Sandy Maguire]

yeah, fair. they're all Reals (which i learned the hard way)

[Patrick Massot]

And providing a #mwe that others can simply copy-paste to their editor is simply showing respect.

[Sandy Maguire]

noted. thanks

[Patrick Massot]

The trick is to at least pretend you can imagine that the time of people that are ready to help is as worthy as yours.

[Sandy Maguire]

i think it's a difference of community culture is all. i come from hs land where people do all the reasoning in their head

[Sandy Maguire]

no disrespect meant

[Patrick Massot]

Ok, let me mute this thread then.

[Kevin Buzzard]

There are times when people post questions in the style you posted, when I've not been able to get a working Lean session with the question in, because I can't figure out the imports. This is why I think MWEs are cool :-)

[Sandy Maguire]

import data.real.basic
import tactic
import analysis.special_functions.pow

namespace lecture11

def injective {α β : Type} (f : α → β) := ∀ x y, f x = f y → x = y

example : injective (λ (x : ℝ), 2 * x^(3 : ℝ) + 1) := begin
  unfold injective,
  intros x y,
  norm_num,
  intro h,
  have idiot : (x ^ (3 : ℝ)) ^ (3 : ℝ)⁻¹ = (y ^ (3 : ℝ)) ^ (3 : ℝ)⁻¹ :=
  begin
    finish,
  end,
  sorry,
end


end lecture11

[Sandy Maguire]

so here's a MWE. is there a way i can prove this for all x, not just those >= 0?

[Kevin Buzzard]

I'm not sure it's true in Lean

[Sandy Maguire]

:surprise:

[Kevin Buzzard]

x^(1/2) won't be correctly defined for every real number, because the result must be real

[Kevin Buzzard]

so probably if x<0 then x^(1/2)=0 because it will have to be something

[Kevin Buzzard]

x^pi is meaningless if x is negative

[Kevin Buzzard]

so I would be very surprised if x^(1/3) happens to be the thing you want it to be if x<0

[Kevin Buzzard]

I haven't looked at the definition but it would not surprise me if a^b is a random junk value e.g. 0 or 1 if a<0

[Sandy Maguire]

is the issue that ^(1/3) just incidentally happens to compute the cube root, but isn't defined as cuberoot (x^3) = x?

[Kevin Buzzard]

If I had to define x^y in Lean I'd probably go for exp(y*log(x))

[Kevin Buzzard]

you can't just define x^(1/3), you have to define x^(any real number at all)

[Sandy Maguire]

2021-01-16-105246_486x369_scrot.png here's the exercise i'm working through

[Kevin Buzzard]

so it's highly unlikely to say "if y is a rational number which happens to have an odd denominator then there's a way of making this make sense"

[Sandy Maguire]

i think i might not be a sophisticated-enough mathematician to appreciate the point you're trying to express

[Kevin Buzzard]

^ has type real -> real -> real

[Kevin Buzzard]

So what do you think (-2)^(1/2) is?

[Sandy Maguire]

i understand that this isn't true for y=2 and z=1/2, and i think you're saying "since it's not true for some cases, we need to define it in a way that works for all of them, and there are no special cases for the odd naturals"?

[Rémy Degenne]

about what pow is for negative x: the doc of real.rpow states "For x < 0, the definition is somewhat arbitary as it depends on the choice of a complex determination of the logarithm. With our conventions, it is equal to exp (y log x) cos (πy)."

[Kevin Buzzard]

you might be lucky then

[Sandy Maguire]

i'm confused about whether or not this is a problem in my understanding, in the given proof, or in how lean is implemented

[Sandy Maguire]

and whether anything will go wrong if i just introduce an axiom for \forall z, z^3^(1/3) = z

[Kevin Buzzard]

it might not be true! It might be though

[Sandy Maguire]

sorry, what might not be true? the axiom?

[Kevin Buzzard]

right

[Kevin Buzzard]

I do not know if it's true or not, I will have to read the docstring but I'm in a lecture right now

[Sandy Maguire]

this isn't a burning question that i'm going to stay up all night wondering about

[Sandy Maguire]

if you're curious i'd be happy to know the answer, but please don't put yourself out

[Sandy Maguire]

but this exercise has definitely decreased some of my trust in lean if i can't just show the first-year first-week example as it's given

[Johan Commelin]

there will be a lemma in mathlib saying that x |-> x ^ 3 is injective. That should be good enough

[Kevin Buzzard]

@Sandy Maguire you should see one of the slides in the talk I just gave :-) I'll post it when I'm done here

[Bryan Gin-ge Chen]

I don't think that this should decrease your trust in Lean, but there are definitely things we could do to make mathlib more accessible / easier to use.

[Rémy Degenne]

see docs#injective_pow_p for the statement that x^p is injective for p in N.

[Kevin Buzzard]

2not1.png

[Johan Commelin]

@Rémy Degenne that's not the one you want... it's for perfect rings of characteristic p...

[Rémy Degenne]

oh yes indeed. i was suprised about the p in the name. Sorry

[Kevin Buzzard]

slide_before.png

[Kevin Buzzard]

Me trying to formalise undergraduate mathematics in 2017

[Johan Commelin]

Sandy Maguire said:

but this exercise has definitely decreased some of my trust in lean if i can't just show the first-year first-week example as it's given

[joking] does this mean it also decreases your trust in haskell, because I don't think you can do this exercise in haskell either... [/joking]

[Rémy Degenne]

there is docs#pow_left_inj for positive inputs

[Sandy Maguire]

Johan Commelin said:

Sandy Maguire said:

but this exercise has definitely decreased some of my trust in lean if i can't just show the first-year first-week example as it's given

[joking] does this mean it also decreases your trust in haskell, because I don't think you can do this exercise in haskell either... [/joking]

fair --- but i don't even pretend to be productive haskell :)

[Rémy Degenne]

don't we have a lemma stating that x^n is injective for n odd? I can't find one.

[Johan Commelin]

https://leanprover-community.github.io/mathlib_docs/algebra/group_power/basic.html#pow_left_inj is the closest I got

[Johan Commelin]

maybe nobody ever cared about odd powers until today :rofl:

[Sandy Maguire]

Bryan Gin-ge Chen said:

I don't think that this should decrease your trust in Lean, but there are definitely things we could do to make mathlib more accessible / easier to use.

that's fair. i'm such a noob that lean and mathlib are the same to me

[Sandy Maguire]

Johan Commelin said:

maybe nobody ever cared about odd powers until today :rofl:

that's the other thing i never know. am i an idiot or a trailblazer? ... or both? :)

[Kevin Buzzard]

we only got odd numbers in 2020 I think ;-)

[Bryan Gin-ge Chen]

It seems that the negative case evaluates to something weird:

import analysis.special_functions.pow

example (z : ℝ) (h : z < 0) : (z ^ (3 : ℝ)) ^ (3 : ℝ)⁻¹ = -z/2 :=
begin
  rw real.rpow_def_of_neg h,
  have : 3 * real.pi = (1 : ℤ) * (2 * real.pi) + real.pi := by norm_cast; ring,
  rw this,
  conv_lhs { congr, congr, skip, rw real.cos_int_mul_two_pi_add_pi 1, },
  rw [real.exp_mul, real.exp_log_of_neg h, mul_neg_one],
  have hnz : 0 < -z := neg_pos_of_neg h,
  have hnz3 : -(-z)^(3 : ℝ) < 0 := neg_neg_of_pos (real.rpow_pos_of_pos hnz _),
  have hnz3' : 0 < (-z)^(3 : ℝ) := pos_of_neg_neg hnz3,
  rw [real.rpow_def_of_neg hnz3, real.log_neg_eq_log, real.exp_mul,
    real.exp_log hnz3', ← real.rpow_mul hnz.le, inv_eq_one_div, mul_comm _ real.pi,
    mul_one_div real.pi _, real.cos_pi_div_three, mul_one_div, mul_one_div, div_self];
  norm_num,
end

golfing, etc. welcome!

[Sandy Maguire]

i think i'm going to proceed by introducing an axiom to eliminate ^3^(1/3) and go on my merry way

[Rémy Degenne]

so -z/2 ?

[Sandy Maguire]

thanks for all of your input everyone

[Johan Commelin]

Rémy Degenne said:

so -z/2 ?

it's the real part of two of the complex cube roots... clearly they outvoted the other complex cube root :rofl:

[Rémy Degenne]

could we change the definition of real.rpow to have x^(n:R) = x^(n:N) for all x in R? without breaking everything that is

[Mario Carneiro]

wait, that should already be the case

[Kevin Buzzard]

I think cos(Pi/3)=0.5 so the theorem really is false.

[Mario Carneiro]

Regarding the crazy discontinuous definition of x^y for negative x, I suppose we can do that but I think it would be better to use a dedicated function

[Mario Carneiro]

and @Sandy Maguire if a theorem doesn't work out, don't force it with an axiom! Make a better definition that satisfies the properties you want instead

[Mario Carneiro]

In this case, I would suggest something like def cube_root (x : R) := if x >= 0 then x ^ (1/3) else -((-x) ^ (1/3))

[Bryan Gin-ge Chen]

(I've edited my snippet to show that it's indeed -z/2. This was probably much more painful than it had to be.)

[Sandy Maguire]

@Mario Carneiro that's a good idea. does anything go wrong with this axiom if i only use it locally in this proof? is it just a matter of bad style?

[Mario Carneiro]

No, it's inconsistent

[Mario Carneiro]

You are asserting a thing lean knows to be false, anything will follow and math crumbles

[Mario Carneiro]

please don't assert axioms that you know to be disprovable

[Sandy Maguire]

well what i'm really proving is example : injective (λ (x : ℝ), 2 * x^(3 : ℝ) + 1) --- whcih i think IS true?

[Mario Carneiro]

That is true

[Sandy Maguire]

my proof sucks, admittedly

[Mario Carneiro]

You can use cube_root if you want an explicit inverse in order to prove injectivity

[Sandy Maguire]

i think i see your point

[Sandy Maguire]

i am torn between "i hate this example and want to move onto something else" vs just doing it right

[Sandy Maguire]

and i think i'll do the latter. thanks for the push

[Bryan Gin-ge Chen]

There are a lot of .injective lemmas which should let you chain together a neat-looking proof of your statement with dot notation.

[Mario Carneiro]

do we have a .injective for rpow though? That seems to be the crux of it

[Bryan Gin-ge Chen]

Oh right. Whoops.

[Mario Carneiro]

Or even monoid.pow, we know that's equal

[Sandy Maguire]

@Mario Carneiro your cube_root is noncomputable and lean yells at me.

import data.real.basic
import tactic
import analysis.special_functions.pow

def injective {α β : Type} (f : α → β) := ∀ x y, f x = f y → x = y

-- axiom cube_root (x : ℝ) : (x ^ (3 : ℝ)) ^ (3 : ℝ)⁻¹ = x

@[noncomputable] def cube_root (x : ℝ) := if x >= 0 then x ^ (1/3) else -((-x) ^ (1/3))

example : injective (λ (x : ℝ), 2 * x^(3 : ℝ) + 1) := begin
  unfold injective,
  intros x y,
  norm_num,
  intro h,
  suffices idiot : (x ^ (3 : ℝ)) ^ (3 : ℝ)⁻¹ = (y ^ (3 : ℝ)) ^ (3 : ℝ)⁻¹,
  rw ←cube_root x,
  rw ←cube_root y,
  assumption,
  finish,
end

[Mario Carneiro]

The whole alternating odd/even thing seems like it would be better suited as a theorem about monoid.pow

[Mario Carneiro]

noncomputable is a keyword, not an attribute

[Sandy Maguire]

that does it. thanks

[Mario Carneiro]

also you probably need to put a type ascription on the 1/3's

[Mario Carneiro]

lean usually can't figure out the type in an exponent because it's not determined from context, so it will default to nat and that's definitely not what you want here because then 1/3=0

[Sandy Maguire]

yeah :)

[Sandy Maguire]

i learned that the hard way the other day

[Sandy Maguire]

okay, working on proving this with the cube_root... now getting stuck saying i can't apply a rewrite that pretty obviously seems like it should apply

import data.real.basic
import tactic
import analysis.special_functions.pow

def injective {α β : Type} (f : α → β) := ∀ x y, f x = f y → x = y

lemma x_iff_x_cubed_ge_zero {x : ℝ} (h : x ^ (3:ℝ) ≥ 0) : x ≥ 0 := by sorry

noncomputable def cube_root (x : ℝ) :=
  if x >= 0 then x ^ (3⁻¹ : ℝ) else -((-x) ^ (3⁻¹ : ℝ))

example : injective (λ (x : ℝ), 2 * x^(3 : ℝ) + 1) := begin
  unfold injective,
  intros x y,
  norm_num,
  intro hxycube,
  have idiot : cube_root (x ^ (3 : ℝ)) = cube_root (y ^ (3 : ℝ)) := by finish,
  unfold cube_root at idiot,
  by_cases x^(3:ℝ) ≥ 0,
  {
    have hy : y ^ (3:ℝ) ≥ 0 := begin
      rw ←hxycube,
      assumption,
    end,
    simp [h, hy] at idiot,
    rw ←real.rpow_mul at idiot,
    rw ←real.rpow_mul at idiot,
    rw mul_inv_cancel at idiot,
    rw real.rpow_one at idiot,
    rw real.rpow_one at idiot,
    assumption,
    exact nonzero_of_invertible 3,
    refine x_iff_x_cubed_ge_zero _,
    assumption,
    refine x_iff_x_cubed_ge_zero _,
    assumption,
  },
  {
    have hy : ¬ (y ^ (3:ℝ) ≥ 0) := begin
      rw ←hxycube,
      assumption,
    end,
    simp [h, hy] at idiot,
    rw ←real.rpow_mul at idiot,


  },
end

[Sandy Maguire]

also golfing tips GREATLY appreciated

[Sandy Maguire]

tho i really really feel like i'm going against the grain here. it feels like this shouldn't be so hard to prove

[Johan Commelin]

:shock: :shock: does mathlib not know

example (x : ℝ) : x ^ (3 : ℝ) = x ^ 3 := sorry

this is painful

[Johan Commelin]

norm_num and norm_cast don't help

[Johan Commelin]

if I replace 3 by n : nat it does work

[Ruben Van de Velde]

replace (3 : real) with ((3 : nat) : real) first?

[Johan Commelin]

but norm_cast should be able to do that for me

[Sandy Maguire]

maybe i'm running into the same thing.

import data.real.basic
import tactic
import analysis.special_functions.pow

lemma x_iff_x_cubed_ge_zero {x : ℝ} (hx3 : x ^ (3:ℝ) ≥ 0) : x ≥ 0 :=
begin
  by_contradiction,
  simp at h,
  have hx_3 : x^3 < 0 := begin
    repeat {rw pow_succ},
    rw pow_zero,
    rw mul_one,
    rw mul_neg_iff,
    refine or.inr _,
    split,
    assumption,
    refine mul_pos_iff.mpr _,
    refine or.inr _,
    split,
    assumption,
    assumption,
  end,
  have hx_3' : x^((3 : ℕ) : ℝ) < 0 :=
  begin
    assumption_mod_cast,
  end,
end

this assumption_mod_cast fails

[Sandy Maguire]

and then :scream: contradiction doesn't find any contradictions

[Ruben Van de Velde]

rwa real.rpow_nat_cast works, fwiw

[Bryan Gin-ge Chen]

Here's another approach:

import analysis.special_functions.pow

-- we should have this in mathlib!
lemma rpow_odd_strict_mono (n : ℕ) : strict_mono (λ (x : ℝ), x ^ (2 * n + 1)) :=
sorry

example : function.injective (λ (x : ℝ), 2 * x^(3 : ℝ) + 1) :=
begin
  apply strict_mono.injective,
  apply strict_mono.add_const,
  apply strict_mono.const_mul,
  { convert rpow_odd_strict_mono 1,
    ext x, norm_num, exact_mod_cast real.rpow_nat_cast x 3, },
  { norm_num, }
end

I'm working on rpow_odd_strict_mono still...

[Shing Tak Lam]

and yet another approach. not sure about the proof of pow_sub_pow yet, but I think this proves that for all odd n, x^n is injective.

import data.real.basic
import tactic
import analysis.special_functions.pow
import data.nat.parity

open_locale big_operators

lemma pos_of_odd_pow_pos {n : ℕ} (hn : odd n) {x : ℝ} (hx : 0 < x^n) : 0 < x :=
begin
  rcases hn with ⟨k, rfl⟩,
  rw [pow_succ, mul_pos_iff] at hx,
  cases hx,
  { exact hx.1 },
  { cases hx with hx1 hx2,
    rw [mul_comm, pow_mul] at hx2,
    nlinarith }
end

lemma neg_of_odd_pow_neg {n : ℕ} (hn : odd n) {x : ℝ} (hx : x^n < 0) : x < 0 :=
begin
  rcases hn with ⟨k, rfl⟩,
  rw [pow_succ, mul_neg_iff] at hx,
  cases hx,
  { cases hx with hx1 hx2,
    rw [mul_comm, pow_mul] at hx2,
    nlinarith },
  { exact hx.1 }
end

lemma odd_pow_pos_iff_pos {n : ℕ} (hn : odd n) {x : ℝ} : 0 < x^n ↔ 0 < x :=
begin
  split,
  { exact pos_of_odd_pow_pos hn },
  intro hx,
  apply pow_pos,
  exact hx,
end

lemma odd_pow_neg_iff_neg {n : ℕ} (hn : odd n) {x : ℝ} : x^n < 0 ↔ x < 0 :=
begin
  split,
  { exact neg_of_odd_pow_neg hn },
  intro hx,
  rcases hn with ⟨k, rfl⟩,
  rw [pow_succ, mul_comm 2, pow_mul],
  apply mul_neg_of_neg_of_pos,
  { exact hx },
  { apply pow_two_pos_of_ne_zero,
    intro h,
    have := pow_eq_zero h,
    rw this at hx,
    linarith }
end

lemma pow_sub_pow (x y : ℝ) (n : ℕ) : x^(n + 1) - y^(n + 1) = (x - y) * ∑ j in (finset.range n.succ), x^j * y^(n - j) :=
begin
  sorry,
end

lemma pow_odd_inj_of_pos {n : ℕ} (hn : odd n) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hxy : x^n = y^n) : x = y :=
begin
  rcases hn with ⟨k, rfl⟩,
  rw [←sub_eq_zero, pow_sub_pow x y] at hxy,
  have : 0 < ∑ (j : ℕ) in finset.range (2 * k).succ, x ^ j * y ^ (2 * k - j),
  { rw ←finset.sum_const_zero,
    apply finset.sum_lt_sum,
    { intros i hi,
      apply le_of_lt,
      apply mul_pos,
      { apply pow_pos,
        exact hx },
      { apply pow_pos,
        exact hy } },
    { use [0],
      split,
      { simp },
      { rw [pow_zero, one_mul, nat.sub_zero, mul_comm, pow_mul],
        apply pow_two_pos_of_ne_zero,
        intro h,
        have := pow_eq_zero h,
        rw this at hy,
        linarith } } },
    { rw mul_eq_zero at hxy,
      cases hxy,
      { rwa [←sub_eq_zero_iff_eq] },
      { rw hxy at this,
        linarith } }
end

lemma pow_odd_inj_of_neg {n : ℕ} (hn : odd n) {x y : ℝ} (hx : x < 0) (hy : y < 0) (hxy : x^n = y^n) : x = y :=
begin
  suffices : -x = -y, linarith,
  apply pow_odd_inj_of_pos hn,
  { linarith },
  { linarith },
  rw [neg_pow x, neg_pow y, nat.neg_one_pow_of_odd hn],
  linarith,
end

lemma pow_odd_inj {n : ℕ} (hn : odd n) {x y : ℝ} (hxy : x^n = y^n) : x = y :=
begin
  rcases lt_trichotomy 0 x with (hx|rfl|hx),
  { have hy : 0 < y,
    { have : 0 < y^n,
      { rwa [←hxy, odd_pow_pos_iff_pos hn] },
    rwa odd_pow_pos_iff_pos hn at this },
    apply pow_odd_inj_of_pos hn hx hy hxy },
  { rw [zero_pow] at hxy,
    exact (pow_eq_zero hxy.symm).symm,
    exact nat.odd_gt_zero hn },
  { have hy : y < 0,
    { have : y^n < 0,
      { rwa [←hxy, odd_pow_neg_iff_neg hn] },
    rwa odd_pow_neg_iff_neg hn at this },
    apply pow_odd_inj_of_neg hn hx hy hxy }
end

[Sandy Maguire]

seeing all of these big scary suggestions makes me feel better about not being able to get it on my own

[Johan Commelin]

import data.real.basic
import tactic
import analysis.special_functions.pow

open function

variables {R : Type*} [linear_ordered_ring R] {x y : R} {n : ℕ}

lemma nonneg_of_pow_nonneg (hn : odd n) (hx : 0 ≤ x ^ n) : 0 ≤ x :=
begin
  rcases hn with ⟨n, rfl⟩,
  rw pow_succ at hx,
  rw [pow_mul', mul_nonneg_iff] at hx,
  simp only [pow_two_nonneg, and_true] at hx,
  cases hx, { exact hx },
  cases hx with hx0 hx,
  have hx' : (x ^ n) ^ 2 = 0 := le_antisymm hx (pow_two_nonneg _),
  exact (pow_eq_zero (pow_eq_zero hx')).ge
end

lemma pow_nonneg_iff (hn : odd n) : 0 ≤ x ^ n ↔ 0 ≤ x :=
⟨nonneg_of_pow_nonneg hn, λ h, pow_nonneg h n⟩

lemma pow_neg_iff (hn : odd n) : x ^ n < 0 ↔ x < 0 :=
by { rw [← not_iff_not], push_neg, exact pow_nonneg_iff hn }

lemma pow_neg_eq_neg_pow_of_odd (hn : odd n) : (- x) ^ n = - (x ^ n) :=
begin
  rcases hn with ⟨n, rfl⟩,
  have := neg_pow_bit1 x n,
  rwa [bit1, bit0_eq_two_mul] at this
end

lemma nat.pos_of_odd (hn : odd n) : 0 < n :=
by { rcases hn with ⟨n, rfl⟩, dec_trivial }

theorem pow_left_inj_of_odd (hn : odd n) (h : x ^ n = y ^ n) : x = y :=
begin
  cases le_or_lt 0 x with hx hx,
  { have hy : 0 ≤ y, by rwa [← pow_nonneg_iff hn, h, pow_nonneg_iff hn] at hx,
    exact pow_left_inj hx hy (nat.pos_of_odd hn) h },
  { have hy : y < 0, by rwa [← pow_neg_iff hn, h, pow_neg_iff hn] at hx,
    have hx' : 0 ≤ -x, simpa only [neg_nonneg] using hx.le,
    have hy' : 0 ≤ -y, simpa only [neg_nonneg] using hy.le,
    have := pow_left_inj hx' hy' (nat.pos_of_odd hn) _,
    { simpa },
    simpa only [pow_neg_eq_neg_pow_of_odd hn, neg_inj] }
end

example : injective (λ (x : ℝ), 2 * x^3 + 1) :=
begin
  intros x y h,
  norm_num at h,
  exact pow_left_inj_of_odd ⟨1, rfl⟩ h
end

[Johan Commelin]

it's not exactly the strict_mono from Bryan's approach... but well

[Johan Commelin]

I don't have time to turn this into a PR... but if someone else wants to do that, please go ahead :thumbs_up:

[Ruben Van de Velde]

Poking at Sandy's approach a little more:

lemma x_iff_x_cubed_ge_zero {x : ℝ} (hx3 : x ^ (3:ℝ) ≥ 0) : x ≥ 0 :=
begin
  contrapose! hx3,
  have : (3 : ℝ) = ((3 : ℕ) : ℝ) := by norm_cast,
  rw [this, real.rpow_nat_cast, pow_succ, mul_neg_iff],
  right,
  refine ⟨hx3, _⟩,
  refine lt_of_le_of_ne (pow_two_nonneg _) (ne.symm _),
  contrapose! hx3,
  exact (pow_eq_zero hx3).ge,
end

[Sandy Maguire]

@Ruben Van de Velde amazing! ooc how did decide to use lt_of_le_of_ne?

[Bryan Gin-ge Chen]

(I finished my proof of rpow_odd_strict_mono finally and edited it into my message above. There's surely a better way, but I ended up just following my nose instead of thinking about the math... )

[Ruben Van de Velde]

@Sandy Maguire I needed to prove 0 < x², so it seemed helpful to point out the fact that 0 <= x², so I'd only need to rule out x² = 0

[Kevin Buzzard]

Sandy -- sorry for not really finishing my sentences yesterday -- I was busy doing something else and just occasionally looking at the chat. What is going on in the proof that you posted is that there's a "cube root" function involved, which is the inverse map to the bijection $x\mapsto x^3$ on the reals. The point is that Lean does not have that function right now (at least not until this thread) and in particular the function lam x, x^(1/3:real), which looks superficially similar, is not this function. The point is that that rpow, which is what ^ expands to, is defined for all real inputs and is what you think it is for positive reals, but returns junk values for negative reals. The reason for this is that even though coincidentally there is a good choice of $x^{1/3}$ for negative real $x$, there really is no good choice of $x^r$ for an arbitrary real number when $x$ is negative, and rpow makes no attempt to distinguish between the real numbers for which there is a good choice (which happen to be the rational numbers with odd denominator) and the real numbers for which there is no good choice -- it just returns junk if x is negative, in all cases. There is no problem formalising this proof in Lean, but you will need the cube root function which is defined on all the reals, so this function needs to be made first.

[Ruben Van de Velde]

So if we're free to choose a junk value for rpow with negative x, could we choose one that matches the good definition when it exists? Or would that cause too much trouble elsewhere?

[Sebastien Gouezel]

The value of rpow for negative x is not really junk. It is the real part of the complex-valued function given by x ^ y = exp (x log y), where log is the principal branch of the complex logarithm.

[Kevin Buzzard]

The fact that it returns -1/2 on an input of (-1)^(1/3) certainly makes it look like junk -- it's just the real part of $e^{2\pi i/3}$ but this answer is wrong on many levels :-) Given that the only possible values for the exponent where there happens to be a non-junk answer are rational, it makes me think that one could define a power function real -> rat -> real which returned the right answer when the real was negative and the rational had odd denominator, and that this would perhaps be the more sensible approach.

[Sebastien Gouezel]

You want the power function to be continuous, and even analytic where it can be. Well, I don't know if you want it, but I want it :-)

[Kevin Buzzard]

Of course every definition comes with a cost, and the cost here would be the theorems saying that it agrees with rpow when the base is positive, and that it satisfies stuff like $x^{ab}=(x^a)^b$ even sometimes when $x$ is negative.

[Sebastien Gouezel]

And you want it to be compatible with casts, also.

[Kevin Buzzard]

Sebastien Gouezel said:

You want the power function to be continuous, and even analytic where it can be. Well, I don't know if you want it, but I want it :-)

You are talking about behaviour in the second variable here I guess. This phenomenon about $x^{1/3}$ happening to make sense for negative $x$ is something which is happening on a discrete set, which is why I am suggesting rational powers, where things like continuity are not really so meaningful.

[Mario Carneiro]

well it's not called qpow is it? :)

[Mario Carneiro]

I think that the power function is rather unfortunately overloaded in mathematics

[Kevin Buzzard]

Even before Lean I was well aware that you need $n^{-s}$ to make sense for $n\in\mathbb{R}_{>0}$ and $s\in\mathbb{C}$ so you can talk about the zeta function, but you also needed it to make sense for $n\in\mathbb{C}^\times$ and $s\in\mathbb{Z}$ to talk about integrating around poles etc. Each of those functions is well-behaved, the union of the two sets is random, and attempts to extend the definition to a larger set in a "natural" way are fraught with difficulty.

[Sebastien Gouezel]

Note that our definition has the right behavior both for $n \in \mathbb{R}_{>0}$ and $s\in \mathbb{C}$ on the one hand, and for $n \in \mathbb{C}$ and $s\in \mathbb{Z}$ on the other hand.

[Eric Wieser]

So does docs#qpow exist already then?

[Sebastien Gouezel]

No, we just have docs#rpow, but x ^ y behaves well when x is positive, and also when y is (the cast of) an integer. It does not behave well for y = 1/3, though.

[Mario Carneiro]

here's a crazy idea for qpow: x ^ y := if y < 0 then -((-x) ^ y) else x ^ y

[Mario Carneiro]

i.e. don't bother with the odd power thing, just always extend oddly

[Eric Wieser]

That makes (-4) ^ (1/2) = 2 which seems like a dangerous kind of garbage that is easy to not notice

[Mario Carneiro]

I know, but garbage is garbage

[Mario Carneiro]

this version has the advantage that it's still somewhat continuous

[Mario Carneiro]

AFAICT this gives the right answer whenever one exists

[Mario Carneiro]

and if you are trying to solve (-1)^(1/2) over the reals, read an intro to complex analysis book

[Mario Carneiro]

it also agrees in magnitude with the correct complex answer for all inputs

[Eric Wieser]

I'm more concerned about someone stating a theorem that is nonsense but happens to be true for that unusual definition of power

[Mario Carneiro]

that's the point of "least bad" garbage definitions

[Eric Wieser]

Right; my question is whether 0 is a less bad result for negative x and even denominator

[Eric Wieser]

Which iirc correctly is what docs#real.sqrt gives

[Mario Carneiro]

well for example, you get a theorem of the form x ^ y = 0 <-> x = 0 in some generality

[Eric Wieser]

Right, although that problem is already solved one way by docs#real.sqrt_eq_zero and docs#real.sqrt_eq_zero'

[Mario Carneiro]

yes, that's a fine solution for a function which just does square root, but that doesn't generalize very well

[Eric Wieser]

I suppose the other question to ask is whether real.sqrt should be redefined to match your qpow suggestion

[Mario Carneiro]

Does anyone use the current behavior?

[Mario Carneiro]

I don't think it really matters except in the theorem that rewrites odd_rpow to sqrt

[Damiano Testa]

Mario, if you throw in an abs in the name, it is neither garage, nor misleading...

[Mario Carneiro]

it's not an abs though

[Mario Carneiro]

it's negative for negative input

[Damiano Testa]

Ah, I had missed the sign in front! `signed_pow``. Not sure...

[Sebastien Gouezel]

Mario Carneiro said:

here's a crazy idea for qpow: x ^ y := if x < 0 then -((-x) ^ y) else x ^ y

For y = 2, it doesn't give the square...

[Mario Carneiro]

...right

[Mario Carneiro]

ok, plan B: root x n := if x < 0 then -((-x) ^ (1/n)) else x ^ (1/n). No claim that this is a general power function anymore, n is a natural number that you probably want to be odd

[Mario Carneiro]

actually in that case we can just as well do the alternations,
root x n := if x < 0 then (-1)^n * ((-x) ^ (1/n)) else x ^ (1/n).

[Mario Carneiro]

the idea being that there will be theorems of the form root x n = x ^ (1/n), root x n ^ m = x ^ (m/n) and so on under limited conditions

[Mario Carneiro]

I don't know any practical utility to extending this root function to rationals with odd denominator; you can use root (x^m) n to express that

[Sandy Maguire]

Mario Carneiro said:

here's a crazy idea for qpow: x ^ y := if x < 0 then -((-x) ^ y) else x ^ y

i tried this yesterday for an hour or two (via your cube_root def) and still wasn't able to make the proof work. the issue is eliminating that negative that is now introduced --- i'd like to factor it into (-1)^y * x^y but then we run back into the 0<= constraint on rpow.

[Sandy Maguire]

@Mario Carneiro here's as far as i could take it:

import data.real.basic
import tactic
import analysis.special_functions.pow


lemma x_iff_x_cubed_ge_zero {x : ℝ} (hx3 : x ^ (3:ℝ) ≥ 0) : x ≥ 0 :=
begin
  contrapose! hx3,
  have : (3 : ℝ) = ((3 : ℕ) : ℝ) := by norm_cast,
  rw [this, real.rpow_nat_cast, pow_succ, mul_neg_iff],
  right,
  refine ⟨hx3, _⟩,
  refine lt_of_le_of_ne (pow_two_nonneg _) (ne.symm _),
  norm_num,
  contrapose! hx3,
  exact eq.ge hx3,
end


def injective {α β : Type} (f : α → β) := ∀ x y, f x = f y → x = y

noncomputable def cube_root (x : ℝ) :=
  if x >= 0 then x ^ (3⁻¹ : ℝ) else -((-x) ^ (3⁻¹ : ℝ))

example : injective (λ (x : ℝ), 2 * x^(3 : ℝ) + 1) := begin
  unfold injective,
  intros x y,
  norm_num,
  intro hxycube,

  have idiot : cube_root (x ^ (3 : ℝ)) = cube_root (y ^ (3 : ℝ)) := by finish,
  unfold cube_root at idiot,
  by_cases x^(3:ℝ) ≥ 0,
  {
    have hy : y ^ (3:ℝ) ≥ 0 := begin
      rw ←hxycube,
      assumption,
    end,
    simp [h, hy] at idiot,
    rw ←real.rpow_mul at idiot,
    rw ←real.rpow_mul at idiot,
    rw mul_inv_cancel at idiot,
    rw real.rpow_one at idiot,
    rw real.rpow_one at idiot,
    assumption,
    exact nonzero_of_invertible 3,
    refine x_iff_x_cubed_ge_zero _,
    assumption,
    refine x_iff_x_cubed_ge_zero _,
    assumption,
  },
  {
    have hy : ¬ (y ^ (3:ℝ) ≥ 0) := begin
      rw ←hxycube,
      assumption,
    end,
    simp [h, hy] at idiot,
    -- simp at h,
    -- simp at hy,
    rw ←neg_one_mul at idiot,
    rw real.mul_rpow at idiot,
    {
      have : (-1 : ℝ) ^ (3⁻¹ : ℝ) = -1 := by sorry,
      rw this at idiot,
      rw ←neg_one_mul (y^(3:ℝ)) at idiot,
      rw real.mul_rpow at idiot,
      {
        rw this at idiot,
        simp at idiot,
        rw ←real.rpow_mul at idiot,
        rw ←real.rpow_mul at idiot,
        rw mul_inv_cancel at idiot,
        rw real.rpow_one at idiot,
        rw real.rpow_one at idiot,
        assumption,
        exact nonzero_of_invertible 3,
        refine x_iff_x_cubed_ge_zero _,
        sorry,
        refine x_iff_x_cubed_ge_zero _,
        sorry,
      },
      sorry,
      sorry,
    },
    sorry,
    sorry,


  },
end

[Sandy Maguire]

Kevin Buzzard said:

Sandy -- sorry for not really finishing my sentences yesterday -- I was busy doing something else and just occasionally looking at the chat. What is going on in the proof that you posted is that there's a "cube root" function involved, which is the inverse map to the bijection $x\mapsto x^3$ on the reals. The point is that Lean does not have that function right now (at least not until this thread) and in particular the function lam x, x^(1/3:real), which looks superficially similar, is not this function. The point is that that rpow, which is what ^ expands to, is defined for all real inputs and is what you think it is for positive reals, but returns junk values for negative reals. The reason for this is that even though coincidentally there is a good choice of $x^{1/3}$ for negative real $x$, there really is no good choice of $x^r$ for an arbitrary real number when $x$ is negative, and rpow makes no attempt to distinguish between the real numbers for which there is a good choice (which happen to be the rational numbers with odd denominator) and the real numbers for which there is no good choice -- it just returns junk if x is negative, in all cases. There is no problem formalising this proof in Lean, but you will need the cube root function which is defined on all the reals, so this function needs to be made first.

that's an extremely helpful elaboration, thank you kevin!

[Mario Carneiro]

Sandy Maguire said:

Mario Carneiro said:

here's a crazy idea for qpow: x ^ y := if x < 0 then -((-x) ^ y) else x ^ y

i tried this yesterday for an hour or two (via your cube_root def) and still wasn't able to make the proof work. the issue is eliminating that negative that is now introduced --- i'd like to factor it into (-1)^y * x^y but then we run back into the 0<= constraint on rpow.

Why are you factoring it? The idea here, explicit in the if, is to break into cases based on x < 0 or 0 <= x. In the second case it's just rpow and you're covered. In the first case, x < 0 means 0 <= -x so the properties of rpow imply (-((-x) ^ (1/3))) ^ 3 = -(((-x) ^ (1/3)) ^ 3) = --x = x. I think you are saying that the first equality is the one giving you trouble, because rpow isn't nice on negatives, but this one isn't rpow, it's x ^ 3 which can be rewritten as an instance of monoid.pow, because the exponent is an integer, which does have the (-x)^n = (-1)^n * x ^n theorem you want.

[Manuel Candales]

Reopening this thread. The following gives me a "goals accomplished" message.

import data.complex.basic

example : (-1 : ℂ) ^ (1/3) = 1 :=
begin
  norm_num,
end

[Bryan Gin-ge Chen]

@Manuel Candales That's because (1/3) is being interpreted as natural number division, which results in 0.

[Bryan Gin-ge Chen]

Try this instead:

import data.complex.basic
import analysis.special_functions.pow
example : (-1 : ℂ) ^ ((1 : ℂ)/3) = 1 :=
begin
  norm_num, -- doesn't work
end

[Bryan Gin-ge Chen]

I think (-1 : ℂ) ^ ((1 : ℂ)/3) evaluates to -1/2, see this post.

[Manuel Candales]

I am confused about the 1/3 evaluating to 0, because I used 1/2 in a recent proof without casting it. Anyway, I'll try to figure that out on my own. But in any case, -1/2 so the real part of one of the complex square roots. That makes sense for rpow. But not for cpow. cpow is defined from C to C.

[Manuel Candales]

*cubic roots

[Bryan Gin-ge Chen]

Oh right, I missed the cpow!

[Mario Carneiro]

norm_num doesn't know anything about real or complex powers. It can evaluate the exponent into a fraction but anything transcendental can't be evaluated