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.

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

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

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

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

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

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

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

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

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ᵢ.

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.

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ᵢ.

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.

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ᵢ.

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.

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ᵢ.

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.