English
A variant of liminf_toReal_eq with a different bounding condition, yielding the same conclusion.
Русский
Вариант liminf_toReal_eq с другой ограничивающей условией, приводящий к тому же выводу.
LaTeX
$$$\text{liminf}_{i} (u_i)^{\mathrm{toReal}} = (\text{liminf}_{i} u_i)^{\mathrm{toReal}}$$$
Lean4
/-- If `u : ι → ℝ≥0∞` is bounded, then we have `liminf (toReal ∘ u) = toReal (liminf u)`. -/
theorem liminf_toReal_eq [NeBot f] {b : ℝ≥0∞} (b_ne_top : b ≠ ∞) (le_b : ∀ᶠ i in f, u i ≤ b) :
f.liminf (fun i ↦ (u i).toReal) = (f.liminf u).toReal :=
by
have liminf_le : f.liminf u ≤ b := by
apply liminf_le_of_le ⟨0, by simp⟩
intro y h
obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists
exact hi.1.trans hi.2
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.liminf u).toReal = ENNReal.truncateToReal b (f.liminf u) := by
rw [truncateToReal_eq_toReal b_ne_top liminf_le]
simp_rw [liminf_congr aux, aux']
have key :=
Monotone.map_liminf_of_continuousAt (F := f) (monotone_truncateToReal b_ne_top) u
(continuous_truncateToReal b_ne_top).continuousAt
(IsBoundedUnder.isCoboundedUnder_ge ⟨b, by simpa only [eventually_map] using le_b⟩)
⟨0, Eventually.of_forall (by simp)⟩
rw [key]
rfl
