toReal_limsup — Mathlib

English

The limit superior commutes with the real coercion: taking limsup of a Real-valued sequence obtained from NNReal values equals the limsup of the NNReal sequence viewed in Real.

Русский

Предел верхний сочетает предел с приведением к действительным: лимсуп последовательности в Real совпадает с лимсуп последовательности NNReal после приведения к Real.

LaTeX

$$$\\\\limsup_f ((u(i))^{\\\\mathbb{R}}) = (\\\\limsup_f u(i))^{\\\\mathbb{R}}$$$

Lean4

@[simp, norm_cast]
theorem toReal_limsup : limsup (fun i ↦ (u i : ℝ)) f = limsup u f :=
  by
  obtain rfl | hf := f.eq_or_neBot
  · simp [limsup, limsSup]
  by_cases hf : f.IsBoundedUnder (· ≤ ·) u; swap
  · simp [*]
  have : f.IsCoboundedUnder (· ≤ ·) u := by isBoundedDefault
  refine eq_of_forall_le_iff fun c ↦ ?_
  rw [← Real.toNNReal_le_iff_le_coe, le_limsup_iff (by simpa) (by simpa), le_limsup_iff ‹_›]
  simp only [← coe_lt_coe, Real.coe_toNNReal', lt_sup_iff, or_imp, isEmpty_Prop, not_lt, zero_le_coe,
    IsEmpty.forall_iff, and_true, NNReal.forall, coe_mk, forall_swap (α := _ ≤ _)]
  refine forall₂_congr fun r hr ↦ ?_
  simpa using (le_or_gt 0 r).imp_right fun hr ↦ .of_forall fun i ↦ hr.trans_le (by simp)

Похожие утверждения