le_iff_sq_le

Stream: Is there code for X?

[Eric Rodriguez]

Patrick Massot said:

I think it isn't the first time I don't manage to find the first lemma above. Is it really missing?

I think you're meant to use docs#pow_left_strictMonoOn

[Jireh Loreaux]

Indeed, I think the first lemma is missing.

[Jireh Loreaux]

Eric, that only gives you one direction of the ↔

[Eric Rodriguez]

docs#StrictMonoOn.le_iff_le

[Jireh Loreaux]

Oh I see what you mean. That seems really messy, I vote for just adding the lemma.

[Eric Rodriguez]

cc @Yaël Dillies; this little discussion should be moved to a separate thread probably

[Patrick Massot]

Eric, do you mean

lemma le_iff_sq_le {R : Type*} [LinearOrderedRing R] {x y : R} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x ≤ y ↔ x^2 ≤ y^2 :=
  ((pow_left_strictMonoOn zero_lt_two.ne').le_iff_le hx hy).symm

[Patrick Massot]

If there is nothing simpler then I think it is worth adding the lemma.

[Eric Rodriguez]

it's what I've been using for the past little bit; in some slight solace it holds for linear ordered semirings too! but I agree it's messy

[Yaël Dillies]

Your lemma is not there because you wrote it the wrong way around!

[Patrick Massot]

Do you mean switching sides of the iff?

[Patrick Massot]

It doesn't change anything, right?

[Kevin Buzzard]

I guess it changes whether the lemma obeys the "left hand side should be more complicated than the right hand side" rule

[Patrick Massot]

The proof is still the complicated

lemma le_iff_sq_le {R : Type*} [LinearOrderedSemiring R] {x y : R} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x^2 ≤ y^2 ↔ x ≤ y :=
  (pow_left_strictMonoOn zero_lt_two.ne').le_iff_le hx hy

[Patrick Massot]

right?

[Patrick Massot]

I would be happy to add to Mathlib

lemma pow_le_pow_iff {R : Type*} [LinearOrderedSemiring R] {x y : R} (n : ℕ)
    (hx : 0 ≤ x) (hy : 0 ≤ y) : x^(n+1) ≤ y^(n+1) ↔ x ≤ y :=
  (pow_left_strictMonoOn n.succ_ne_zero).le_iff_le hx hy

lemma sq_le_sq_iff {R : Type*} [LinearOrderedSemiring R] {x y : R} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x^2 ≤ y^2 ↔ x ≤ y :=
  pow_le_pow_iff 1 hx hy

What do you think @Yaël Dillies?

[Patrick Massot]

Golfing/finding the right general statement for

lemma abs_le_of_mem_uIoc_zero {A : Type*} [LinearOrderedAddCommGroup A] {x y : A} (h : x ∈ Ι 0 y) :
    |x| ≤ |y| := by
  rcases Set.mem_uIoc.1 h with (⟨hx, hxy⟩ | ⟨hxy, hx⟩)
  · rwa [abs_of_pos hx, abs_of_pos <| hx.trans_le hxy]
  · rw [abs_of_nonpos hx, abs_of_neg <| hxy.trans_le hx]
    exact neg_le_neg hxy.le

lemma sq_le_of_mem_uIoc_zero {R : Type*} [LinearOrderedRing R] {x y : R} (h : x ∈ Ι 0 y) :
    x^2 ≤ y^2 := by
  simpa using pow_le_pow_left (abs_nonneg x) (abs_le_of_mem_uIoc_zero h) 2

would also be nice.

[Yaël Dillies]

I think docs#pow_le_pow_iff_left is good enough?

[Yaël Dillies]

Note that I added this lemma two weeks ago.

[Yaël Dillies]

Btw please don't touch anything in the algebraic order part of mathlib right now.I have a 5.5k lines PR to get merged, and the lemmas you care about are right in the middle of my diff.

[Yaël Dillies]

#9411 for reference

[Yaël Dillies]

I can't think of a much better way to state your lemmas. You should use uIcc but that's it.

[Patrick Massot]

Yaël Dillies said:

I think docs#pow_le_pow_iff_left is good enough?

Great. That's one more mysterious exact? failure...

[Patrick Massot]

Yaël Dillies said:

I can't think of a much better way to state your lemmas. You should use uIcc but that's it.

The relevant one for interval integral is uIoc.

[Yaël Dillies]

Ah sure but one is easily a subset of the other

[Patrick Massot]

Of course I agree the uIoc version should be deduced from a uIcc one.

[Patrick Massot]

And I won't touch this, don't worry about your PR.

[Patrick Massot]

I was only trying to help Alex K in another thread.