real map_supr

Stream: general

[Jireh Loreaux]

All our map_supr and map_csupr lemmas require an order_iso. This is annoying, when, for example, you have a norm (so the term has type ℝ) which is a supr of nonnegative terms and you need to square it (as happens frequently for the C∗-property).

Of course, in normal mathematics, you just pull the square in and out of the supremum freely because everything is nonnegative and squaring is an order isomorphism on the nonnegative reals. But this is a royal pain to do in mathlib, so I wrote the following.

The first lemma is the main one, and it gives you a general technique to do what I described above. The rest is just deriving the basic facts to show that you can apply this specifically to squaring.

import analysis.special_functions.pow

open_locale nnreal

lemma order_iso.map_Sup_real_of_nonneg {s : set ℝ} (hs : s ⊆ {x : ℝ | 0 ≤ x})
  (e' : ℝ≥0 ≃o ℝ≥0) (e : ℝ → ℝ) (he' : (∀ x : ℝ≥0, e x = e' x)) :
  e (Sup s) = Sup (e '' s) :=
begin
  refine or.elim s.eq_empty_or_nonempty (λ h, _) (λ h, _),
  { rw [h],
    simpa only [set.image_empty, real.Sup_empty, ←nnreal.coe_zero, he']
      using congr_arg coe e'.map_bot },
  lift s to set ℝ≥0 using hs,
  simp_rw [←nnreal.coe_Sup, he', set.image_image, he'],
  rw [←set.image_image, ←nnreal.coe_Sup],
  have h' : s.nonempty := set.nonempty_image_iff.mp h,
  refine congr_arg _ (or.elim (em $ bdd_above s) (λ bdd, e'.map_cSup' h' bdd) (λ ubdd, _)),
  have : ∀ t : set ℝ≥0, t.nonempty → ¬ bdd_above t → Sup t = 0,
  { intros t ht' ht,
    rw [←nnreal.coe_eq, nnreal.coe_Sup, nnreal.coe_zero],
    convert real.Sup_of_not_bdd_above (λ hbdd, ht _),
    obtain ⟨c, hc⟩ := hbdd,
    use ⟨c, nnreal.zero_le_coe.trans (hc ⟨ht'.some, ⟨ht'.some_spec, rfl⟩⟩)⟩,
    exact λ x hx, hc ⟨x, ⟨hx, rfl⟩⟩ },
  rw [this s h' ubdd,
    this (e' '' s) (set.nonempty_image_iff.mpr h') (mt e'.bdd_above_image.mp ubdd)],
  exact e'.map_bot,
end

lemma order_iso.map_supr_real_of_nonneg {ι : Type*} {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i)
  (e' : ℝ≥0 ≃o ℝ≥0) (e : ℝ → ℝ) (he' : (∀ x : ℝ≥0, e x = e' x)) :
  e (⨆ i, f i) = ⨆ i, e (f i) :=
begin
  simp only [supr, ←set.image_univ],
  rw set.image_comp e,
  exact order_iso.map_Sup_real_of_nonneg (by { rintros _ ⟨i, ⟨_, rfl⟩⟩, exact hf i }) e' e he',
end

lemma nnreal.strict_mono_rpow_of_pos {z : ℝ} (h : 0 < z) : strict_mono (λ x : ℝ≥0, x ^ z) :=
λ x y hxy, nnreal.rpow_lt_rpow hxy h

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

/-- Bundles `λ x : ℝ≥0, x ^ y` into an order isomorphism when `y : ℝ` is positive,
where the inverse is `λ x : ℝ≥0, x ^ (1 / y)`. -/
@[simps apply]
noncomputable def order_iso.nnreal_rpow (y : ℝ) (hy : 0 < y) : ℝ≥0 ≃o ℝ≥0 :=
(nnreal.strict_mono_rpow_of_pos hy).order_iso_of_right_inverse (λ x, x ^ y) (λ x, x ^ (1 / y))
  (λ x, by { dsimp, rw [←nnreal.rpow_mul, one_div_mul_cancel hy.ne.symm, nnreal.rpow_one] })

@[simp] lemma order_iso.nnreal_rpow_symm_apply (y : ℝ) (hy : 0 < y) :
  (order_iso.nnreal_rpow y hy).symm = order_iso.nnreal_rpow (1 / y) (one_div_pos.2 hy) :=
by { simp only [order_iso.nnreal_rpow, one_div_one_div y], refl, }

lemma real.map_supr_pow_of_nonneg {ι : Type*} (f : ι → ℝ) (h : ∀ i, 0 ≤ f i) {n : ℕ} (hn : 0 < n) :
  (⨆ i, f i) ^ n = ⨆ i, (f i) ^ n :=
(order_iso.nnreal_rpow n $ nat.cast_pos.2 hn).map_supr_real_of_nonneg h (λ x, x ^ n)
  (λ x, by simp only [order_iso.nnreal_rpow_apply, nnreal.rpow_nat_cast, nnreal.coe_pow])

lemma real.map_supr_rpow_of_nonneg {ι : Type*} (f : ι → ℝ) (h : ∀ i, 0 ≤ f i) {y : ℝ}
  (hy : 0 < y) : (⨆ i, f i) ^ y = ⨆ i, (f i) ^ y :=
(order_iso.nnreal_rpow y hy).map_supr_real_of_nonneg h (λ x, x ^ y)
  (λ x, by simp only [order_iso.nnreal_rpow_apply, nnreal.coe_rpow])

[Jireh Loreaux]

The question is, should I do it differently, or perhaps more generally? For example, I suspect that if you have a conditionally complete linear order with the order topology which is densely orderd, then you should be able to pull a function f in and out of a supremum over a (nonempty?) set s contained in a closed interval Icc a b so long as strict_mono_on f s and continuous_on f s. Of course, the stuff I already have is a bit nice because I can remove the nonempty and bdd_above restrictions.

[Yaël Dillies]

What you really want is a local order_iso, which is to order_iso what monotone_on is to order_hom.