feat: lemma limsup_const_add + 7 variants (#6455)

Add 8 lemmas: `limsup_const_add`, ..., `liminf_sub_const`.

The 4 lemmas about `add` are proven with typeclass assumptions which apply to `ℝ`, `ℝ≥0`, and `ℝ≥0∞` (at least). The 4 lemmas about `sub` are proven with typeclass assumptions which apply to `ℝ` and `ℝ≥0` (at least). For `ℝ≥0∞`, we add separate implementations of these latter 4 lemmas `ENNReal.liminf_sub_const`, ...



Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Algebra.IndicatorFunction
+import Mathlib.Topology.Algebra.Group.Basic
 import Mathlib.Order.LiminfLimsup
 import Mathlib.Order.Filter.Archimedean
 import Mathlib.Order.Filter.CountableInter
@@ -554,3 +555,79 @@ theorem limsup_eq_tendsto_sum_indicator_atTop (R : Type*) [StrictOrderedSemiring
 #align limsup_eq_tendsto_sum_indicator_at_top limsup_eq_tendsto_sum_indicator_atTop
 
 end Indicator
+
+section LiminfLimsupAddSub
+
+variable {R : Type*} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R]
+
+/-- `liminf (c + xᵢ) = c + liminf xᵢ`. -/
+lemma limsup_const_add (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
+    [CovariantClass R R (fun x y ↦ x + y) fun x y ↦ x ≤ y] (f : ι → R) (c : R)
+    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
+    Filter.limsup (fun i ↦ c + f i) F = c + Filter.limsup f F :=
+  (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c + x)
+    (fun _ _ h ↦ add_le_add_left h c) (continuous_add_left c).continuousAt bdd_above bdd_below).symm
+
+/-- `limsup (xᵢ + c) = (limsup xᵢ) + c`. -/
+lemma limsup_add_const (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
+    [CovariantClass R R (Function.swap fun x y ↦ x + y) fun x y ↦ x ≤ y] (f : ι → R) (c : R)
+    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
+    Filter.limsup (fun i ↦ f i + c) F = Filter.limsup f F + c :=
+  (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x + c)
+    (fun _ _ h ↦ add_le_add_right h c)
+    (continuous_add_right c).continuousAt bdd_above bdd_below).symm
+
+/-- `liminf (c + xᵢ) = c + limsup xᵢ`. -/
+lemma liminf_const_add (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
+    [CovariantClass R R (fun x y ↦ x + y) fun x y ↦ x ≤ y]  (f : ι → R) (c : R)
+    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
+    Filter.liminf (fun i ↦ c + f i) F = c + Filter.liminf f F :=
+  (Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c + x)
+    (fun _ _ h ↦ add_le_add_left h c) (continuous_add_left c).continuousAt bdd_above bdd_below).symm
+
+/-- `liminf (xᵢ + c) = (liminf xᵢ) + c`. -/
+lemma liminf_add_const (F : Filter ι) [NeBot F] [Add R] [ContinuousAdd R]
+    [CovariantClass R R (Function.swap fun x y ↦ x + y) fun x y ↦ x ≤ y] (f : ι → R) (c : R)
+    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
+    Filter.liminf (fun i ↦ f i + c) F = Filter.liminf f F + c :=
+  (Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x + c)
+    (fun _ _ h ↦ add_le_add_right h c)
+    (continuous_add_right c).continuousAt bdd_above bdd_below).symm
+
+/-- `limsup (c - xᵢ) = c - liminf xᵢ`. -/
+lemma limsup_const_sub (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R]
+    [OrderedSub R] [CovariantClass R R (fun x y ↦ x + y) fun x y ↦ x ≤ y] (f : ι → R) (c : R)
+    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
+    Filter.limsup (fun i ↦ c - f i) F = c - Filter.liminf f F :=
+  (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
+    (fun _ _ h ↦ tsub_le_tsub_left h c)
+    (continuous_sub_left c).continuousAt bdd_above bdd_below).symm
+
+/-- `limsup (xᵢ - c) = (limsup xᵢ) - c`. -/
+lemma limsup_sub_const (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R]
+    [OrderedSub R] (f : ι → R) (c : R)
+    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
+    Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c :=
+  (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c)
+    (fun _ _ h ↦ tsub_le_tsub_right h c)
+    (continuous_sub_right c).continuousAt bdd_above bdd_below).symm
+
+/-- `liminf (c - xᵢ) = c - limsup xᵢ`. -/
+lemma liminf_const_sub (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R]
+    [OrderedSub R] [CovariantClass R R (fun x y ↦ x + y) fun x y ↦ x ≤ y] (f : ι → R) (c : R)
+    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
+    Filter.liminf (fun i ↦ c - f i) F = c - Filter.limsup f F :=
+  (Antitone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ c - x)
+    (fun _ _ h ↦ tsub_le_tsub_left h c)
+    (continuous_sub_left c).continuousAt bdd_above bdd_below).symm
+
+/-- `liminf (xᵢ - c) = (liminf xᵢ) - c`. -/
+lemma liminf_sub_const (F : Filter ι) [NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R]
+    [OrderedSub R] (f : ι → R) (c : R)
+    (bdd_above : F.IsBoundedUnder (· ≤ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
+    Filter.liminf (fun i ↦ f i - c) F = Filter.liminf f F - c :=
+  (Monotone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : R) ↦ x - c)
+    (fun _ _ h ↦ tsub_le_tsub_right h c)
+    (continuous_sub_right c).continuousAt bdd_above bdd_below).symm
+
+end LiminfLimsupAddSub -- section

Mathlib/Topology/Instances/ENNReal.lean

@@ -1598,3 +1598,33 @@ theorem edist_le_tsum_of_edist_le_of_tendsto₀ {f : ℕ → α} (d : ℕ → 
 #align edist_le_tsum_of_edist_le_of_tendsto₀ edist_le_tsum_of_edist_le_of_tendsto₀
 
 end
+
+section LimsupLiminf
+
+namespace ENNReal
+
+lemma limsup_sub_const (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞) (c : ℝ≥0∞) :
+    Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c :=
+  (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
+
+lemma liminf_sub_const (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞) (c : ℝ≥0∞) :
+    Filter.liminf (fun i ↦ f i - c) F = Filter.liminf f F - c :=
+  (Monotone.map_limsInf_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
+
+lemma limsup_const_sub (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞)
+    {c : ℝ≥0∞} (c_ne_top : c ≠ ∞):
+    Filter.limsup (fun i ↦ c - f i) F = c - Filter.liminf f F :=
+  (Antitone.map_limsInf_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
+    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm
+
+lemma liminf_const_sub (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞)
+    {c : ℝ≥0∞} (c_ne_top : c ≠ ∞):
+    Filter.liminf (fun i ↦ c - f i) F = c - Filter.limsup f F :=
+  (Antitone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ c - x)
+    (fun _ _ h ↦ tsub_le_tsub_left h c) (continuous_sub_left c_ne_top).continuousAt).symm
+
+end ENNReal -- namespace
+
+end LimsupLiminf