## Stream: new members

### Topic: Cube root of cubic is id?

#### Sandy Maguire (Jan 16 2021 at 18:21):

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 (Jan 16 2021 at 18:29):

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

#### Bryan Gin-ge Chen (Jan 16 2021 at 18:29):

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 (Jan 16 2021 at 18:30):

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

#### Sandy Maguire (Jan 16 2021 at 18:31):

@Patrick Massot mind being more specific about that?

#### Patrick Massot (Jan 16 2021 at 18:32):

It's pretty specific.

#### Sandy Maguire (Jan 16 2021 at 18:32):

@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 (Jan 16 2021 at 18:38):

well wolfram alpha disagrees with me :)

#### Sandy Maguire (Jan 16 2021 at 18:44):

@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 (Jan 16 2021 at 18:44):

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

#### Patrick Massot (Jan 16 2021 at 18:45):

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

#### Bryan Gin-ge Chen (Jan 16 2021 at 18:45):

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 (Jan 16 2021 at 18:45):

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

#### Patrick Massot (Jan 16 2021 at 18:45):

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

noted. thanks

#### Patrick Massot (Jan 16 2021 at 18:46):

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 (Jan 16 2021 at 18:47):

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 (Jan 16 2021 at 18:47):

no disrespect meant

#### Patrick Massot (Jan 16 2021 at 18:47):

Ok, let me mute this thread then.

#### Kevin Buzzard (Jan 16 2021 at 18:47):

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 (Jan 16 2021 at 18:48):

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 (Jan 16 2021 at 18:48):

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

#### Kevin Buzzard (Jan 16 2021 at 18:49):

I'm not sure it's true in Lean

:surprise:

#### Kevin Buzzard (Jan 16 2021 at 18:50):

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

#### Kevin Buzzard (Jan 16 2021 at 18:50):

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

#### Kevin Buzzard (Jan 16 2021 at 18:50):

x^pi is meaningless if x is negative

#### Kevin Buzzard (Jan 16 2021 at 18:51):

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 (Jan 16 2021 at 18:52):

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 (Jan 16 2021 at 18:52):

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 (Jan 16 2021 at 18:52):

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

#### Kevin Buzzard (Jan 16 2021 at 18:53):

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

#### Sandy Maguire (Jan 16 2021 at 18:53):

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

#### Kevin Buzzard (Jan 16 2021 at 18:53):

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 (Jan 16 2021 at 18:54):

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

#### Kevin Buzzard (Jan 16 2021 at 18:54):

^ has type real -> real -> real

#### Kevin Buzzard (Jan 16 2021 at 18:54):

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

#### Sandy Maguire (Jan 16 2021 at 18:54):

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 (Jan 16 2021 at 18:54):

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 (Jan 16 2021 at 18:56):

you might be lucky then

#### Sandy Maguire (Jan 16 2021 at 18:56):

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 (Jan 16 2021 at 18:59):

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

#### Kevin Buzzard (Jan 16 2021 at 19:00):

it might not be true! It might be though

#### Sandy Maguire (Jan 16 2021 at 19:01):

sorry, what might not be true? the axiom?

right

#### Kevin Buzzard (Jan 16 2021 at 19:01):

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 (Jan 16 2021 at 19:01):

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

#### Sandy Maguire (Jan 16 2021 at 19:02):

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

#### Sandy Maguire (Jan 16 2021 at 19:03):

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 (Jan 16 2021 at 19:07):

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

#### Kevin Buzzard (Jan 16 2021 at 19:08):

@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 (Jan 16 2021 at 19:10):

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 (Jan 16 2021 at 19:11):

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

2not1.png

#### Johan Commelin (Jan 16 2021 at 19:12):

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

#### Rémy Degenne (Jan 16 2021 at 19:12):

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

slide_before.png

#### Kevin Buzzard (Jan 16 2021 at 19:13):

Me trying to formalise undergraduate mathematics in 2017

#### Johan Commelin (Jan 16 2021 at 19:13):

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 (Jan 16 2021 at 19:14):

there is docs#pow_left_inj for positive inputs

#### Sandy Maguire (Jan 16 2021 at 19:15):

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 (Jan 16 2021 at 19:15):

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

#### Johan Commelin (Jan 16 2021 at 19:16):

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

#### Sandy Maguire (Jan 16 2021 at 19:16):

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 (Jan 16 2021 at 19:17):

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 (Jan 16 2021 at 19:17):

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

#### Bryan Gin-ge Chen (Jan 16 2021 at 19:19):

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 (Jan 16 2021 at 19:24):

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 (Jan 16 2021 at 19:24):

so -z/2 ?

#### Sandy Maguire (Jan 16 2021 at 19:24):

thanks for all of your input everyone

#### Johan Commelin (Jan 16 2021 at 19:29):

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 (Jan 16 2021 at 19:29):

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 (Jan 16 2021 at 19:32):

wait, that should already be the case

#### Kevin Buzzard (Jan 16 2021 at 19:33):

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

#### Mario Carneiro (Jan 16 2021 at 19:33):

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 (Jan 16 2021 at 19:35):

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 (Jan 16 2021 at 19:36):

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 (Jan 16 2021 at 19:37):

(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 (Jan 16 2021 at 19:38):

@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 (Jan 16 2021 at 19:38):

No, it's inconsistent

#### Mario Carneiro (Jan 16 2021 at 19:39):

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

#### Mario Carneiro (Jan 16 2021 at 19:39):

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

#### Sandy Maguire (Jan 16 2021 at 19:40):

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

That is true

#### Sandy Maguire (Jan 16 2021 at 19:41):

my proof sucks, admittedly

#### Mario Carneiro (Jan 16 2021 at 19:41):

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

#### Sandy Maguire (Jan 16 2021 at 19:41):

i think i see your point

#### Sandy Maguire (Jan 16 2021 at 19:41):

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

#### Sandy Maguire (Jan 16 2021 at 19:41):

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

#### Bryan Gin-ge Chen (Jan 16 2021 at 19:41):

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 (Jan 16 2021 at 19:42):

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

#### Bryan Gin-ge Chen (Jan 16 2021 at 19:43):

Oh right. Whoops.

#### Mario Carneiro (Jan 16 2021 at 19:43):

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

#### Sandy Maguire (Jan 16 2021 at 19:43):

@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 (Jan 16 2021 at 19:44):

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

#### Mario Carneiro (Jan 16 2021 at 19:44):

noncomputable is a keyword, not an attribute

#### Sandy Maguire (Jan 16 2021 at 19:44):

that does it. thanks

#### Mario Carneiro (Jan 16 2021 at 19:45):

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

#### Mario Carneiro (Jan 16 2021 at 19:46):

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

yeah :)

#### Sandy Maguire (Jan 16 2021 at 19:46):

i learned that the hard way the other day

#### Sandy Maguire (Jan 16 2021 at 20:20):

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 (Jan 16 2021 at 20:21):

also golfing tips GREATLY appreciated

#### Sandy Maguire (Jan 16 2021 at 20:22):

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 (Jan 16 2021 at 20:35):

:shock: :shock: does mathlib not know

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


this is painful

#### Johan Commelin (Jan 16 2021 at 20:35):

norm_num and norm_cast don't help

#### Johan Commelin (Jan 16 2021 at 20:36):

if I replace 3 by n : nat it does work

#### Ruben Van de Velde (Jan 16 2021 at 20:36):

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

#### Johan Commelin (Jan 16 2021 at 20:39):

but norm_cast should be able to do that for me

#### Sandy Maguire (Jan 16 2021 at 20:40):

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
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 (Jan 16 2021 at 20:44):

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

#### Ruben Van de Velde (Jan 16 2021 at 20:50):

rwa real.rpow_nat_cast works, fwiw

#### Bryan Gin-ge Chen (Jan 16 2021 at 20:50):

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.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 (Jan 16 2021 at 20:54):

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 (Jan 16 2021 at 20:55):

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

#### Johan Commelin (Jan 16 2021 at 21:10):

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 (Jan 16 2021 at 21:11):

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

#### Johan Commelin (Jan 16 2021 at 21:13):

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 (Jan 16 2021 at 21:21):

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 (Jan 16 2021 at 21:35):

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

#### Bryan Gin-ge Chen (Jan 17 2021 at 01:24):

(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 (Jan 17 2021 at 11:11):

@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 (Jan 17 2021 at 11:30):

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 (Jan 17 2021 at 11:53):

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 (Jan 17 2021 at 11:58):

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 (Jan 17 2021 at 12:08):

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 (Jan 17 2021 at 12:09):

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 (Jan 17 2021 at 12:10):

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 (Jan 17 2021 at 12:10):

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

#### Kevin Buzzard (Jan 17 2021 at 12:12):

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 (Jan 17 2021 at 12:30):

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

#### Mario Carneiro (Jan 17 2021 at 12:31):

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

#### Kevin Buzzard (Jan 17 2021 at 12:40):

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 (Jan 17 2021 at 13:15):

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 (Jan 17 2021 at 14:23):

So does docs#qpow exist already then?

#### Sebastien Gouezel (Jan 17 2021 at 14:27):

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 (Jan 17 2021 at 14:29):

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

#### Mario Carneiro (Jan 17 2021 at 14:30):

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

#### Eric Wieser (Jan 17 2021 at 14:35):

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

#### Mario Carneiro (Jan 17 2021 at 14:35):

I know, but garbage is garbage

#### Mario Carneiro (Jan 17 2021 at 14:36):

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

#### Mario Carneiro (Jan 17 2021 at 14:36):

AFAICT this gives the right answer whenever one exists

#### Mario Carneiro (Jan 17 2021 at 14:37):

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

#### Mario Carneiro (Jan 17 2021 at 14:38):

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

#### Eric Wieser (Jan 17 2021 at 14:38):

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 (Jan 17 2021 at 14:38):

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

#### Eric Wieser (Jan 17 2021 at 14:39):

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

#### Eric Wieser (Jan 17 2021 at 14:39):

Which iirc correctly is what docs#real.sqrt gives

#### Mario Carneiro (Jan 17 2021 at 14:40):

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

#### Eric Wieser (Jan 17 2021 at 14:41):

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

#### Mario Carneiro (Jan 17 2021 at 14:42):

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

#### Eric Wieser (Jan 17 2021 at 14:43):

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

#### Mario Carneiro (Jan 17 2021 at 14:43):

Does anyone use the current behavior?

#### Mario Carneiro (Jan 17 2021 at 14:44):

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

#### Damiano Testa (Jan 17 2021 at 15:28):

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

#### Mario Carneiro (Jan 17 2021 at 15:40):

it's not an abs though

#### Mario Carneiro (Jan 17 2021 at 15:40):

it's negative for negative input

#### Damiano Testa (Jan 17 2021 at 16:19):

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

#### Sebastien Gouezel (Jan 17 2021 at 16:52):

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...

...right

#### Mario Carneiro (Jan 17 2021 at 16:58):

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 (Jan 17 2021 at 17:00):

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 (Jan 17 2021 at 17:01):

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 (Jan 17 2021 at 17:03):

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 (Jan 17 2021 at 20:38):

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 (Jan 17 2021 at 20:39):

@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 (Jan 17 2021 at 20:40):

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 (Jan 18 2021 at 02:34):

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 (Apr 06 2021 at 19:50):

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 (Apr 06 2021 at 19:53):

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

#### Bryan Gin-ge Chen (Apr 06 2021 at 19:54):

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 (Apr 06 2021 at 19:55):

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

#### Manuel Candales (Apr 06 2021 at 19:59):

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.

*cubic roots

#### Bryan Gin-ge Chen (Apr 06 2021 at 20:00):

Oh right, I missed the cpow!

#### Mario Carneiro (Apr 07 2021 at 00:03):

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

Last updated: May 13 2021 at 21:12 UTC