# Zulip Chat Archive

## 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_mul`

s 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):

Did you follow the link?

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

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

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

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

: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?

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

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.

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

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

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

#### 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:15):

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

#### 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?

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

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

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

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

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

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

...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, isnotthis 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 thoughcoincidentallythere 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):

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

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

*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