limsup_add_of_right_tendsto_zero — Mathlib

English

If a function g tends to 0 along a filter u, then limsup_u (f + g) = limsup_u f for any f: ι → ENNReal.

Русский

Если функция g стремится к нулю по фильтру u, то limsup_u (f + g) = limsup_u f для любой f.

LaTeX

$$$$\\text{If } u \\xrightarrow{T} 0\\text{, then } \\limsup_{u} (f + g) = \\limsup_{u} f.$$$$

Lean4

theorem limsup_add_of_right_tendsto_zero {u : Filter ι} {g : ι → ℝ≥0∞} (hg : u.Tendsto g (𝓝 0)) (f : ι → ℝ≥0∞) :
    u.limsup (f + g) = u.limsup f :=
  by
  refine le_antisymm ?_ <| limsup_le_limsup <| .of_forall <| by simp
  refine le_limsup_of_le (by isBoundedDefault) fun b hb ↦ ?_
  rw [Filter.limsup_le_iff']
  rintro a hba
  filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| tsub_pos_of_lt hba] with i hf hg
  calc
    f i + g i
    _ ≤ b + g i := by gcongr
    _ ≤ a := add_le_of_le_tsub_left_of_le hba.le hg

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