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 α]
[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_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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
liminf (xᵢ - c) = (liminf xᵢ) - c
.