limsup_sub_const — Mathlib

English

For ENNReal sequences, limsup(c − f_i) = c − limsup f_i, provided c ≠ ∞.

Русский

Для последовательностей ENNReal верно limsup(c − f_i) = c − limsup f_i, при условии c ≠ ∞.

LaTeX

$$$\operatorname{limsup}(c - f_i) = c - \operatorname{limsup} f_i$ (при $c \neq \infty$)$$

Lean4

theorem limsup_sub_const (F : Filter ι) (f : ι → ℝ≥0∞) (c : ℝ≥0∞) :
    Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c :=
  by
  rcases F.eq_or_neBot with rfl | _
  · simp only [limsup_bot, bot_eq_zero', zero_le, tsub_eq_zero_of_le]
  ·
    exact
      (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ x - c)
          (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm

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