English
If a function g tends to 0 along a filter u, then for any f: ι → ENNReal we have liminf_u (f + g) = liminf_u f.
Русский
Если функция g стремится к нулю по фильтру u, то для любой f: ι → ENNReal выполняется liminf_u (f + g) = liminf_u f.
LaTeX
$$$$\\text{If } u \\xrightarrow{T} 0\\text{, then } \\liminf_{u} (f + g) = \\liminf_{u} f.$$$$
Lean4
theorem liminf_add_of_right_tendsto_zero {u : Filter ι} {g : ι → ℝ≥0∞} (hg : u.Tendsto g (𝓝 0)) (f : ι → ℝ≥0∞) :
u.liminf (f + g) = u.liminf f :=
by
refine le_antisymm ?_ <| liminf_le_liminf <| .of_forall <| by simp
refine liminf_le_of_le (by isBoundedDefault) fun b hb ↦ ?_
rw [Filter.le_liminf_iff']
rintro a hab
filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| lt_min (tsub_pos_of_lt hab) one_pos] with i hfg hg
exact
ENNReal.le_of_add_le_add_right (hg.trans_lt <| by simp).ne <|
(add_le_of_le_tsub_left_of_le hab.le <| hg.trans <| min_le_left ..).trans hfg
