English
Let u: ι → ENNReal be a bounded function along a filter f. If there exists b ∈ ℝ≥0∞ with b ≠ ∞ such that u i ≤ b for i eventually in f, then the limsup of the real-valued sequence (u i).toReal along f equals the real of the limsup of u along f.
Русский
Пусть u: ι → ℝ≥0∞ ограничено по фильтру f. Тогда существует b ∈ ℝ≥0∞, b ≠ ∞, такое что u i ≤ b почти наверняка по i в f, и тогда limsup (u i).toReal по f равен toReal(limsup u по f).
LaTeX
$$$$\\exists b \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\ b \\neq \\infty \\ \\\\land\\ {i \\in ι} : u(i) \\le b \\text{ eventually in } f \\quad \\Rightarrow\\quad \\limsup_{i \\to f} (u(i))^{\\toReal} = \\left(\\limsup_{i \\to f} u(i)\\right)^{\\toReal}.$$$$
Lean4
/-- If `u : ι → ℝ≥0∞` is bounded, then we have `liminf (toReal ∘ u) = toReal (liminf u)`. -/
theorem limsup_toReal_eq [NeBot f] {b : ℝ≥0∞} (b_ne_top : b ≠ ∞) (le_b : ∀ᶠ i in f, u i ≤ b) :
f.limsup (fun i ↦ (u i).toReal) = (f.limsup u).toReal :=
by
have aux : ∀ᶠ i in f, (u i).toReal = ENNReal.truncateToReal b (u i) :=
by
filter_upwards [le_b] with i i_le_b
simp only [truncateToReal_eq_toReal b_ne_top i_le_b]
have aux' : (f.limsup u).toReal = ENNReal.truncateToReal b (f.limsup u) := by
rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]
simp_rw [limsup_congr aux, aux']
have key :=
Monotone.map_limsup_of_continuousAt (F := f) (monotone_truncateToReal b_ne_top) u
(continuous_truncateToReal b_ne_top).continuousAt ⟨b, by simpa only [eventually_map] using le_b⟩
(IsBoundedUnder.isCoboundedUnder_le ⟨0, Eventually.of_forall (by simp)⟩)
rw [key]
rfl
