# Lemmas about liminf and limsup in an order topology. #

## Main declarations #

- `BoundedLENhdsClass`: Typeclass stating that neighborhoods are eventually bounded above.
- `BoundedGENhdsClass`: Typeclass stating that neighborhoods are eventually bounded below.

## Implementation notes #

The same lemmas are true in `ℝ`, `ℝ × ℝ`, `ι → ℝ`, `EuclideanSpace ι ℝ`. To avoid code duplication, we provide an ad hoc axiomatisation of the properties we need.

source
theorem le_limsup_add {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h₃ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault) :
Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f
source
theorem limsup_add_le {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h₃ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v := by isBoundedDefault) :
Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
source
theorem le_liminf_add {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h₃ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault) (h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault) :
Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (u + v) f
source
theorem liminf_add_le {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h₃ : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault) (h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v := by isBoundedDefault) :
Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f
source
theorem le_limsup_mul {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} (h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f v) :
Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
source
theorem limsup_mul_le {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} (h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f v) :
Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
source
theorem le_liminf_mul {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) f v) :
Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f
source
theorem liminf_mul_le {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) f v) :
Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
source
theorem limsup_const_add {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f) :
Filter.limsup (fun (i : ι) => c + f i) F = c + Filter.limsup f F

`liminf (c + xᵢ) = c + liminf xᵢ`.

source
theorem limsup_add_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f) :
Filter.limsup (fun (i : ι) => f i + c) F = Filter.limsup f F + c

`limsup (xᵢ + c) = (limsup xᵢ) + c`.

source
theorem liminf_const_add {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f) (bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f) :
Filter.liminf (fun (i : ι) => c + f i) F = c + Filter.liminf f F

`liminf (c + xᵢ) = c + liminf xᵢ`.

source
theorem liminf_add_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f) (bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f) :
Filter.liminf (fun (i : ι) => f i + c) F = Filter.liminf f F + c

`liminf (xᵢ + c) = (liminf xᵢ) + c`.

source
theorem limsup_const_sub {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [AddLeftMono R] (f : ι → R) (c : R) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f) (bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f) :
Filter.limsup (fun (i : ι) => c - f i) F = c - Filter.liminf f F

`limsup (c - xᵢ) = c - liminf xᵢ`.

source
theorem limsup_sub_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f) :
Filter.limsup (fun (i : ι) => f i - c) F = Filter.limsup f F - c

`limsup (xᵢ - c) = (limsup xᵢ) - c`.

source
theorem liminf_const_sub {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [AddLeftMono R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≤ x2) F f) :
Filter.liminf (fun (i : ι) => c - f i) F = c - Filter.limsup f F

`liminf (c - xᵢ) = c - limsup xᵢ`.

source
theorem liminf_sub_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ι → R) (c : R) (cobdd : Filter.IsCoboundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f) (bdd_below : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) F f) :
Filter.liminf (fun (i : ι) => f i - c) F = Filter.liminf f F - c

`liminf (xᵢ - c) = (liminf xᵢ) - c`.