English
Subtraction of a constant from every term shifts the limsup to the left by that constant: limsup (f_i - c) = limsup f_i - c.
Русский
Вычитание константы из каждого члена сдвигает limsup влево на эту константу: limsup (f_i - c) = limsup f_i - c.
LaTeX
$$$\mathrm{limsup}\ (f_i - c) = \mathrm{limsup}\ f_i - c.$$$
Lean4
/-- `limsup (xᵢ - c) = (limsup xᵢ) - c`. -/
theorem limsup_sub_const (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ι → R)
(c : R) (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (cobdd : F.IsCoboundedUnder (· ≤ ·) f) :
Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c :=
by
rcases F.eq_or_neBot with rfl | _
· have {a : R} : sInf Set.univ ≤ a := by
apply csInf_le _ (Set.mem_univ a)
simp only [IsCoboundedUnder, IsCobounded, map_bot, eventually_bot, true_implies] at cobdd
rcases cobdd with ⟨x, hx⟩
refine ⟨x, mem_lowerBounds.2 fun y ↦ ?_⟩
simp only [Set.mem_univ, hx y, implies_true]
simp only [limsup, limsSup, map_bot, eventually_bot, Set.setOf_true]
exact this.antisymm (tsub_le_iff_right.2 this)
· apply (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c) _ _).symm
· exact fun _ _ h ↦ tsub_le_tsub_right h c
· exact (continuous_sub_right c).continuousAt
