Documentation

Mathlib.Topology.Algebra.Order.LiminfLimsup

Lemmas about liminf and limsup in an order topology. #

Main declarations #

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 α] [CovariantClass α α (fun (a b : α) => a + b) fun (x1 x2 : α) => x1 x2] {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) :
theorem limsup_add_le {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [CovariantClass α α (fun (a b : α) => a + b) fun (x1 x2 : α) => x1 x2] {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) :
theorem le_liminf_add {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [CovariantClass α α (fun (a b : α) => a + b) fun (x1 x2 : α) => x1 x2] {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) :
theorem liminf_add_le {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [CovariantClass α α (fun (a b : α) => a + b) fun (x1 x2 : α) => x1 x2] {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) :
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) :
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) :
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) :
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) :
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.