order_iso for ennreal rpow

Stream: Is there code for X?

[Jireh Loreaux]

Do we already know that rpow on ennreal is an order_iso when the exponent is positive? It seems that all the ingredients are there in analysis.special_functions.pow, but I didn't see that bundle explicitly.

[Heather Macbeth]

I don't think so, feel free to add it! The closest seems to be docs#ennreal.monotone_rpow_of_nonneg

[Yury G. Kudryashov]

I think that docs#ennreal.rpow_left_strict_mono_of_pos is closer

[Yury G. Kudryashov]

But you probably want an explicit inv_fun.

[Yury G. Kudryashov]

strict_mono.order_iso_of_right_inverse from #10701 might be useful here.

[Yury G. Kudryashov]

(or you can rewrite the proofs so that you build an order_iso first, then prove strict_mono from it)

[Yury G. Kudryashov]

E.g., if you can build an order_iso using docs#equiv.to_order_iso and docs#ennreal.monotone_rpow_of_nonneg, then get strict_mono for free.

[Yury G. Kudryashov]

UPD: currently, we use strict_mono in the proof of mono, so you can't simplify using equiv.to_order_iso (unless you do a larger refactor).

[Jireh Loreaux]

Am I crazy, or are these redundant in analysis/special_functions/pow? I also don't understand the left in the names.

lemma rpow_left_monotone_of_nonneg {x : ℝ} (hx : 0 ≤ x) : monotone (λ y : ℝ≥0∞, y^x) :=
λ y z hyz, rpow_le_rpow hyz hx

lemma rpow_left_strict_mono_of_pos {x : ℝ} (hx : 0 < x) : strict_mono (λ y : ℝ≥0∞, y^x) :=
λ y z hyz, rpow_lt_rpow hyz hx

They seem to be copies of

lemma strict_mono_rpow_of_pos {z : ℝ} (h : 0 < z) : strict_mono (λ x : ℝ≥0∞, x ^ z) :=
begin
  intros x y hxy,
  lift x to ℝ≥0 using ne_top_of_lt hxy,
  rcases eq_or_ne y ∞ with rfl|hy,
  { simp only [top_rpow_of_pos h, coe_rpow_of_nonneg _ h.le, coe_lt_top] },
  { lift y to ℝ≥0 using hy,
    simp only [coe_rpow_of_nonneg _ h.le, nnreal.rpow_lt_rpow (coe_lt_coe.1 hxy) h, coe_lt_coe] }
end

lemma monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) : monotone (λ x : ℝ≥0∞, x ^ z) :=
h.eq_or_lt.elim (λ h0, h0 ▸ by simp only [rpow_zero, monotone_const])
  (λ h0, (strict_mono_rpow_of_pos h0).monotone)

and moreover, their proofs use rpow_{le,lt}_rpow, which themselves depend on these latter two.

[Sebastien Gouezel]

The left refers to the fact that, in y ^ x, you are varying the left variable y while keeping x fixed.

[Yaël Dillies]

Best way to find out is to try replacing the proofs of the latter by the former.

[Sebastien Gouezel]

It is perfectly possible that we have two identical lemmas like that, just by oversight. A good test is to check whether you can solve one just by invoking the other.

[Eric Wieser]

Are all four lemmas in the same file?

[Sebastien Gouezel]

If this is the case, a PR to remove the duplicated versions is most welcome!

[Jireh Loreaux]

Indeed, all in the same file and they are duplicates. I'll submit a PR. The duplicates are used in a very small number of places throughout mathlib; I'll switch them.

[Jireh Loreaux]

#10794