ennreal.supr_coe

Stream: Is there code for X?

[Jireh Loreaux]

We don't have these relating the supremum on ℝ≥0∞ to the supremum on ℝ≥0, right? If not, I assume we want it?

import data.real.ennreal

open_locale ennreal nnreal

lemma ennreal.supr_coe_eq_top {α : Type*} {f : α → ℝ≥0} :
  (⨆ x, (f x : ℝ≥0∞)) = ∞ ↔ ¬ bdd_above (set.range f) :=
begin
  refine ⟨_, λ hf, _⟩,
  { rw [supr_eq_top, not_bdd_above_iff],
    intros hf r,
    rcases hf r ennreal.coe_lt_top with ⟨i, hi⟩,
    exact ⟨f i, ⟨i, rfl⟩, ennreal.coe_lt_coe.mp hi⟩ },
  { refine (supr_eq_top _).mpr (λ b hb, _),
    rcases not_bdd_above_iff.mp hf b.to_nnreal with ⟨-, ⟨i, rfl⟩, hi⟩,
    exact ⟨i, by simpa only [ennreal.coe_to_nnreal hb.ne] using ennreal.coe_lt_coe.mpr hi⟩ },
end

lemma ennreal.supr_coe_lt_top {α : Type*} {f : α → ℝ≥0} :
  (⨆ x, (f x : ℝ≥0∞)) < ∞ ↔ bdd_above (set.range f) :=
by simpa only [not_not, lt_top_iff_ne_top] using not_iff_not.mpr ennreal.supr_coe_eq_top

lemma ennreal.supr_coe_to_nnreal {α : Type*} {f : α → ℝ≥0} :
  (⨆ x, (f x : ℝ≥0∞)).to_nnreal = supr f :=
begin
  casesI is_empty_or_nonempty α,
  { simp only [csupr_of_empty, ennreal.zero_to_nnreal, bot_eq_zero']},
  { by_cases hf : bdd_above (set.range f),
    { refine le_antisymm ((le_csupr_iff' hf).mpr (λ b hb, _)) _,
      exact ennreal.coe_le_coe.mp (ennreal.coe_to_nnreal_le_self.trans (supr_le (by exact_mod_cast hb))),
      refine csupr_le (λ i, ennreal.coe_le_coe.mp _),
      simpa only [ennreal.coe_to_nnreal (ennreal.supr_coe_lt_top.mpr hf).ne]
        using le_supr (λ x, (f x : ℝ≥0∞)) i },
    { simp only [nnreal.supr_of_not_bdd_above hf, ennreal.supr_coe_eq_top.mpr hf,
        ennreal.top_to_nnreal], } }
end

[Kevin Buzzard]

I would definitely say we want them if we don't have them! When I was doing a bunch of sums (not suprs) in LTE it was really nice to be able to switch seamlessly between sums in nnreal and ennreal depending on what I was doing

[Eric Wieser]

You seem to be missing the titular lemma,

lemma ennreal.supr_coe {α : Type*} {f : α → ℝ≥0} (h : bdd_above (set.range f)) :
  (⨆ x, (f x : ℝ≥0∞)) = ↑(supr f) :=

[Yaël Dillies]

That sounds more useful reversed (and tagged norm_cast). Does docs#ennreal.coe_supr exist? edit: no :(

[Eric Wieser]

I'm about to write with_top.coe_supr to match docs#with_top.coe_Sup

[Eric Wieser]

#15975

[Eric Wieser]

(with the direction reversed as suggested, and norm_cast)

[Jireh Loreaux]

generalized slightly with essentially the same proof:

lemma with_top.supr_coe_eq_top {α β : Type*} [conditionally_complete_linear_order_bot β]
  {f : α → β} : (⨆ x, (f x : with_top β)) = ⊤ ↔ ¬ bdd_above (set.range f) :=
begin
  refine ⟨_, λ hf, _⟩,
  { rw [supr_eq_top, not_bdd_above_iff],
    intros hf r,
    rcases hf r (with_top.coe_lt_top r) with ⟨i, hi⟩,
    exact ⟨f i, ⟨i, rfl⟩, with_top.coe_lt_coe.mp hi⟩ },
  { refine (supr_eq_top _).mpr (λ b hb, _),
    rcases not_bdd_above_iff.mp hf (b.untop hb.ne) with ⟨-, ⟨i, rfl⟩, hi⟩,
    exact ⟨i, by simpa only [with_top.coe_untop _ hb.ne] using with_top.coe_lt_coe.mpr hi⟩ },
end

lemma with_top.supr_coe_lt_top {α β : Type*} [conditionally_complete_linear_order_bot β]
  {f : α → β} : (⨆ x, (f x : with_top β)) < ⊤ ↔ bdd_above (set.range f) :=
by simpa only [not_not, lt_top_iff_ne_top] using not_iff_not.mpr with_top.supr_coe_eq_top

[Jireh Loreaux]

Interestingly, we can't even state the infi versions because we don't have any such thing as conditionally_complete_linear_order_top (not that I think it's necessary).

[Eric Wieser]

Note that the versions in my PR didn't need anything stronger than partial_order β and has_Inf β; so maybe the infi version can be stated after all

[Jireh Loreaux]

hmmm... does docs#supr_eq_top have requirements that are too stringent?

[Jireh Loreaux]

In any case, I just made #15979