Zulip Chat Archive

Stream: new members

Topic: Cube root of cubic is id?


view this post on Zulip 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?

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:29):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 16 2021 at 18:30):

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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:31):

@Patrick Massot mind being more specific about that?

view this post on Zulip Patrick Massot (Jan 16 2021 at 18:32):

Did you follow the link?

view this post on Zulip Patrick Massot (Jan 16 2021 at 18:32):

It's pretty specific.

view this post on Zulip 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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:38):

well wolfram alpha disagrees with me :)

view this post on Zulip 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?

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:44):

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

view this post on Zulip Patrick Massot (Jan 16 2021 at 18:45):

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

view this post on Zulip 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...

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:45):

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

view this post on Zulip 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.

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:46):

noted. thanks

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:47):

no disrespect meant

view this post on Zulip Patrick Massot (Jan 16 2021 at 18:47):

Ok, let me mute this thread then.

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 18:49):

I'm not sure it's true in Lean

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:49):

:surprise:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 18:50):

x^pi is meaningless if x is negative

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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))

view this post on Zulip 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)

view this post on Zulip Sandy Maguire (Jan 16 2021 at 18:53):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 18:54):

^ has type real -> real -> real

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 18:54):

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

view this post on Zulip 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"?

view this post on Zulip 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)."

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 18:56):

you might be lucky then

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 19:00):

it might not be true! It might be though

view this post on Zulip Sandy Maguire (Jan 16 2021 at 19:01):

sorry, what might not be true? the axiom?

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 19:01):

right

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 19:11):

2not1.png

view this post on Zulip 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...

view this post on Zulip Rémy Degenne (Jan 16 2021 at 19:12):

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

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 19:12):

slide_before.png

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 19:13):

Me trying to formalise undergraduate mathematics in 2017

view this post on Zulip 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]

view this post on Zulip Rémy Degenne (Jan 16 2021 at 19:14):

there is docs#pow_left_inj for positive inputs

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 16 2021 at 19:16):

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

view this post on Zulip 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

view this post on Zulip 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? :)

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 19:17):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Rémy Degenne (Jan 16 2021 at 19:24):

so -z/2 ?

view this post on Zulip Sandy Maguire (Jan 16 2021 at 19:24):

thanks for all of your input everyone

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:32):

wait, that should already be the case

view this post on Zulip Kevin Buzzard (Jan 16 2021 at 19:33):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:38):

No, it's inconsistent

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:39):

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

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:39):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:40):

That is true

view this post on Zulip Sandy Maguire (Jan 16 2021 at 19:41):

my proof sucks, admittedly

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:41):

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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 19:41):

i think i see your point

view this post on Zulip 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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 19:41):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:42):

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

view this post on Zulip Bryan Gin-ge Chen (Jan 16 2021 at 19:43):

Oh right. Whoops.

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:43):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:44):

noncomputable is a keyword, not an attribute

view this post on Zulip Sandy Maguire (Jan 16 2021 at 19:44):

that does it. thanks

view this post on Zulip Mario Carneiro (Jan 16 2021 at 19:45):

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

view this post on Zulip 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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 19:46):

yeah :)

view this post on Zulip Sandy Maguire (Jan 16 2021 at 19:46):

i learned that the hard way the other day

view this post on Zulip 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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 20:21):

also golfing tips GREATLY appreciated

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 16 2021 at 20:35):

:shock: :shock: does mathlib not know

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

this is painful

view this post on Zulip Johan Commelin (Jan 16 2021 at 20:35):

norm_num and norm_cast don't help

view this post on Zulip Johan Commelin (Jan 16 2021 at 20:36):

if I replace 3 by n : nat it does work

view this post on Zulip Ruben Van de Velde (Jan 16 2021 at 20:36):

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

view this post on Zulip Johan Commelin (Jan 16 2021 at 20:39):

but norm_cast should be able to do that for me

view this post on Zulip 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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 20:44):

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

view this post on Zulip Ruben Van de Velde (Jan 16 2021 at 20:50):

rwa real.rpow_nat_cast works, fwiw

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jan 16 2021 at 21:11):

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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Sandy Maguire (Jan 16 2021 at 21:35):

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

view this post on Zulip 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... )

view this post on Zulip 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

view this post on Zulip 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 xx3x\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 x1/3x^{1/3} for negative real xx, there really is no good choice of xrx^r for an arbitrary real number when xx 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 e2πi/3e^{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.

view this post on Zulip 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 :-)

view this post on Zulip 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 xab=(xa)bx^{ab}=(x^a)^b even sometimes when xx is negative.

view this post on Zulip Sebastien Gouezel (Jan 17 2021 at 12:10):

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

view this post on Zulip 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 x1/3x^{1/3} happening to make sense for negative xx 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.

view this post on Zulip Mario Carneiro (Jan 17 2021 at 12:30):

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

view this post on Zulip Mario Carneiro (Jan 17 2021 at 12:31):

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

view this post on Zulip Kevin Buzzard (Jan 17 2021 at 12:40):

Even before Lean I was well aware that you need nsn^{-s} to make sense for nR>0n\in\mathbb{R}_{>0} and sCs\in\mathbb{C} so you can talk about the zeta function, but you also needed it to make sense for nC×n\in\mathbb{C}^\times and sZs\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.

view this post on Zulip Sebastien Gouezel (Jan 17 2021 at 13:15):

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

view this post on Zulip Eric Wieser (Jan 17 2021 at 14:23):

So does docs#qpow exist already then?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 17 2021 at 14:30):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 17 2021 at 14:35):

I know, but garbage is garbage

view this post on Zulip Mario Carneiro (Jan 17 2021 at 14:36):

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

view this post on Zulip Mario Carneiro (Jan 17 2021 at 14:36):

AFAICT this gives the right answer whenever one exists

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 17 2021 at 14:38):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 17 2021 at 14:38):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 17 2021 at 14:39):

Which iirc correctly is what docs#real.sqrt gives

view this post on Zulip 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

view this post on Zulip 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'

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 17 2021 at 14:43):

Does anyone use the current behavior?

view this post on Zulip 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

view this post on Zulip Damiano Testa (Jan 17 2021 at 15:28):

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

view this post on Zulip Mario Carneiro (Jan 17 2021 at 15:40):

it's not an abs though

view this post on Zulip Mario Carneiro (Jan 17 2021 at 15:40):

it's negative for negative input

view this post on Zulip Damiano Testa (Jan 17 2021 at 16:19):

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

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Jan 17 2021 at 16:55):

...right

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 xx3x\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 x1/3x^{1/3} for negative real xx, there really is no good choice of xrx^r for an arbitrary real number when xx 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!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2021 at 19:55):

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

view this post on Zulip 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.

view this post on Zulip Manuel Candales (Apr 06 2021 at 19:59):

*cubic roots

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2021 at 20:00):

Oh right, I missed the cpow!

view this post on Zulip 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