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.

class BoundedLENhdsClass (α : Type u_7) [Preorder α] [TopologicalSpace α] : Prop

Ad hoc typeclass stating that neighborhoods are eventually bounded above.

• isBounded_le_nhds : ∀ (a : α), Filter.IsBounded (fun (x x_1 : α) => x ≤ x_1) (nhds a)

class BoundedGENhdsClass (α : Type u_7) [Preorder α] [TopologicalSpace α] : Prop

Ad hoc typeclass stating that neighborhoods are eventually bounded below.

• isBounded_ge_nhds : ∀ (a : α), Filter.IsBounded (fun (x x_1 : α) => x ≥ x_1) (nhds a)

theorem isBounded_le_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] (a : α) : Filter.IsBounded (fun (x x_1 : α) => x ≤ x_1) (nhds a)

theorem Filter.Tendsto.isBoundedUnder_le {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {f : Filter ι} {u : ι → α} {a : α} (h : Filter.Tendsto u f (nhds a)) : Filter.IsBoundedUnder (fun (x x_1 : α) => x ≤ x_1) f u

theorem Filter.Tendsto.bddAbove_range_of_cofinite {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {u : ι → α} {a : α} [IsDirected α fun (x x_1 : α) => x ≤ x_1] (h : Filter.Tendsto u Filter.cofinite (nhds a)) : BddAbove (Set.range u)

theorem Filter.Tendsto.bddAbove_range {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {a : α} [IsDirected α fun (x x_1 : α) => x ≤ x_1] {u : ℕ → α} (h : Filter.Tendsto u Filter.atTop (nhds a)) : BddAbove (Set.range u)

theorem isCobounded_ge_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] (a : α) : Filter.IsCobounded (fun (x x_1 : α) => x ≥ x_1) (nhds a)

theorem Filter.Tendsto.isCoboundedUnder_ge {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] {f : Filter ι} {u : ι → α} {a : α} [Filter.NeBot f] (h : Filter.Tendsto u f (nhds a)) : Filter.IsCoboundedUnder (fun (x x_1 : α) => x ≥ x_1) f u

instance instBoundedGENhdsClassOrderDualInstPreorderInstTopologicalSpaceOrderDual {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedLENhdsClass α] : BoundedGENhdsClass αᵒᵈ

Equations

• (_ : BoundedGENhdsClass αᵒᵈ) = (_ : BoundedGENhdsClass αᵒᵈ)

instance Prod.instBoundedLENhdsClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [BoundedLENhdsClass α] [BoundedLENhdsClass β] : BoundedLENhdsClass (α × β)

Equations

• (_ : BoundedLENhdsClass (α × β)) = (_ : BoundedLENhdsClass (α × β))

instance Pi.instBoundedLENhdsClass {ι : Type u_1} {π : ι → Type u_6} [Finite ι] [(i : ι) → Preorder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), BoundedLENhdsClass (π i)] : BoundedLENhdsClass ((i : ι) → π i)

Equations

• (_ : BoundedLENhdsClass ((i : ι) → π i)) = (_ : BoundedLENhdsClass ((i : ι) → π i))

theorem isBounded_ge_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] (a : α) : Filter.IsBounded (fun (x x_1 : α) => x ≥ x_1) (nhds a)

theorem Filter.Tendsto.isBoundedUnder_ge {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {f : Filter ι} {u : ι → α} {a : α} (h : Filter.Tendsto u f (nhds a)) : Filter.IsBoundedUnder (fun (x x_1 : α) => x ≥ x_1) f u

theorem Filter.Tendsto.bddBelow_range_of_cofinite {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {u : ι → α} {a : α} [IsDirected α fun (x x_1 : α) => x ≥ x_1] (h : Filter.Tendsto u Filter.cofinite (nhds a)) : BddBelow (Set.range u)

theorem Filter.Tendsto.bddBelow_range {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {a : α} [IsDirected α fun (x x_1 : α) => x ≥ x_1] {u : ℕ → α} (h : Filter.Tendsto u Filter.atTop (nhds a)) : BddBelow (Set.range u)

theorem isCobounded_le_nhds {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] (a : α) : Filter.IsCobounded (fun (x x_1 : α) => x ≤ x_1) (nhds a)

theorem Filter.Tendsto.isCoboundedUnder_le {ι : Type u_1} {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] {f : Filter ι} {u : ι → α} {a : α} [Filter.NeBot f] (h : Filter.Tendsto u f (nhds a)) : Filter.IsCoboundedUnder (fun (x x_1 : α) => x ≤ x_1) f u

instance instBoundedLENhdsClassOrderDualInstPreorderInstTopologicalSpaceOrderDual {α : Type u_2} [Preorder α] [TopologicalSpace α] [BoundedGENhdsClass α] : BoundedLENhdsClass αᵒᵈ

Equations

• (_ : BoundedLENhdsClass αᵒᵈ) = (_ : BoundedLENhdsClass αᵒᵈ)

instance Prod.instBoundedGENhdsClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [BoundedGENhdsClass α] [BoundedGENhdsClass β] : BoundedGENhdsClass (α × β)

Equations

• (_ : BoundedGENhdsClass (α × β)) = (_ : BoundedGENhdsClass (α × β))

instance Pi.instBoundedGENhdsClass {ι : Type u_1} {π : ι → Type u_6} [Finite ι] [(i : ι) → Preorder (π i)] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), BoundedGENhdsClass (π i)] : BoundedGENhdsClass ((i : ι) → π i)

Equations

• (_ : BoundedGENhdsClass ((i : ι) → π i)) = (_ : BoundedGENhdsClass ((i : ι) → π i))

instance OrderTop.to_BoundedLENhdsClass {α : Type u_2} [Preorder α] [TopologicalSpace α] [OrderTop α] : BoundedLENhdsClass α

Equations

• (_ : BoundedLENhdsClass α) = (_ : BoundedLENhdsClass α)

instance OrderBot.to_BoundedGENhdsClass {α : Type u_2} [Preorder α] [TopologicalSpace α] [OrderBot α] : BoundedGENhdsClass α

Equations

• (_ : BoundedGENhdsClass α) = (_ : BoundedGENhdsClass α)

instance OrderTopology.to_BoundedLENhdsClass {α : Type u_2} [Preorder α] [TopologicalSpace α] [IsDirected α fun (x x_1 : α) => x ≤ x_1] [OrderTopology α] : BoundedLENhdsClass α

Equations

• (_ : BoundedLENhdsClass α) = (_ : BoundedLENhdsClass α)

instance OrderTopology.to_BoundedGENhdsClass {α : Type u_2} [Preorder α] [TopologicalSpace α] [IsDirected α fun (x x_1 : α) => x ≥ x_1] [OrderTopology α] : BoundedGENhdsClass α

Equations

• (_ : BoundedGENhdsClass α) = (_ : BoundedGENhdsClass α)

theorem le_nhds_of_limsSup_eq_limsInf {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter α} {a : α} (hl : Filter.IsBounded (fun (x x_1 : α) => x ≤ x_1) f) (hg : Filter.IsBounded (fun (x x_1 : α) => x ≥ x_1) f) (hs : Filter.limsSup f = a) (hi : Filter.limsInf f = a) : f ≤ nhds a

If the liminf and the limsup of a filter coincide, then this filter converges to their common value, at least if the filter is eventually bounded above and below.

theorem limsSup_nhds {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] (a : α) : Filter.limsSup (nhds a) = a

theorem limsInf_nhds {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] (a : α) : Filter.limsInf (nhds a) = a

theorem limsInf_eq_of_le_nhds {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter α} {a : α} [Filter.NeBot f] (h : f ≤ nhds a) : Filter.limsInf f = a

If a filter is converging, its limsup coincides with its limit.

theorem limsSup_eq_of_le_nhds {α : Type u_2} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter α} {a : α} [Filter.NeBot f] : f ≤ nhds a → Filter.limsSup f = a

If a filter is converging, its liminf coincides with its limit.

theorem Filter.Tendsto.limsup_eq {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : β → α} {a : α} [Filter.NeBot f] (h : Filter.Tendsto u f (nhds a)) : Filter.limsup u f = a

If a function has a limit, then its limsup coincides with its limit.

theorem Filter.Tendsto.liminf_eq {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : β → α} {a : α} [Filter.NeBot f] (h : Filter.Tendsto u f (nhds a)) : Filter.liminf u f = a

If a function has a limit, then its liminf coincides with its limit.

theorem tendsto_of_liminf_eq_limsup {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : β → α} {a : α} (hinf : Filter.liminf u f = a) (hsup : Filter.limsup u f = a) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x ≤ x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x ≥ x_1) f u) _auto✝) : Filter.Tendsto u f (nhds a)

If the liminf and the limsup of a function coincide, then the limit of the function exists and has the same value.

theorem tendsto_of_le_liminf_of_limsup_le {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : β → α} {a : α} (hinf : a ≤ Filter.liminf u f) (hsup : Filter.limsup u f ≤ a) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x ≤ x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x ≥ x_1) f u) _auto✝) : Filter.Tendsto u f (nhds a)

If a number a is less than or equal to the liminf of a function f at some filter and is greater than or equal to the limsup of f, then f tends to a along this filter.

theorem tendsto_of_no_upcrossings {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {f : Filter β} {u : β → α} {s : Set α} (hs : Dense s) (H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)) (h : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x ≤ x_1) f u) _auto✝) (h' : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x ≥ x_1) f u) _auto✝) : ∃ (c : α), Filter.Tendsto u f (nhds c)

Assume that, for any a < b, a sequence can not be infinitely many times below a and above b. If it is also ultimately bounded above and below, then it has to converge. This even works if a and b are restricted to a dense subset.

theorem eventually_le_limsup {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x ≤ x_1) f u) _auto✝) : ∀ᶠ (b : β) in f, u b ≤ Filter.limsup u f

theorem eventually_liminf_le {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α} (hf : autoParam (Filter.IsBoundedUnder (fun (x x_1 : α) => x ≥ x_1) f u) _auto✝) : ∀ᶠ (b : β) in f, Filter.liminf u f ≤ u b

@[simp]

theorem limsup_eq_bot {α : Type u_2} {β : Type u_3} [CompleteLinearOrder α] [TopologicalSpace α] [FirstCountableTopology α] [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α} : Filter.limsup u f = ⊥ ↔ u =ᶠ[f] ⊥

@[simp]

theorem liminf_eq_top {α : Type u_2} {β : Type u_3} [CompleteLinearOrder α] [TopologicalSpace α] [FirstCountableTopology α] [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α} : Filter.liminf u f = ⊤ ↔ u =ᶠ[f] ⊤

theorem Antitone.map_limsSup_of_continuousAt {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [Filter.NeBot F] {f : R → S} (f_decr : Antitone f) (f_cont : ContinuousAt f (Filter.limsSup F)) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x ≤ x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x ≥ x_1) F) _auto✝) : f (Filter.limsSup F) = Filter.liminf f F

An antitone function between (conditionally) complete linear ordered spaces sends a Filter.limsSup to the Filter.liminf of the image if the function is continuous at the limsSup (and the filter is bounded from above and below).

theorem Antitone.map_limsup_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : R → S} (f_decr : Antitone f) (a : ι → R) (f_cont : ContinuousAt f (Filter.limsup a F)) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) F a) _auto✝) : f (Filter.limsup a F) = Filter.liminf (f ∘ a) F

A continuous antitone function between (conditionally) complete linear ordered spaces sends a Filter.limsup to the Filter.liminf of the images (if the filter is bounded from above and below).

theorem Antitone.map_limsInf_of_continuousAt {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [Filter.NeBot F] {f : R → S} (f_decr : Antitone f) (f_cont : ContinuousAt f (Filter.limsInf F)) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x ≤ x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x ≥ x_1) F) _auto✝) : f (Filter.limsInf F) = Filter.limsup f F

An antitone function between (conditionally) complete linear ordered spaces sends a Filter.limsInf to the Filter.limsup of the image if the function is continuous at the limsInf (and the filter is bounded from above and below).

theorem Antitone.map_liminf_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : R → S} (f_decr : Antitone f) (a : ι → R) (f_cont : ContinuousAt f (Filter.liminf a F)) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) F a) _auto✝) : f (Filter.liminf a F) = Filter.limsup (f ∘ a) F

A continuous antitone function between (conditionally) complete linear ordered spaces sends a Filter.liminf to the Filter.limsup of the images (if the filter is bounded from above and below).

theorem Monotone.map_limsSup_of_continuousAt {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [Filter.NeBot F] {f : R → S} (f_incr : Monotone f) (f_cont : ContinuousAt f (Filter.limsSup F)) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x ≤ x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x ≥ x_1) F) _auto✝) : f (Filter.limsSup F) = Filter.limsup f F

A monotone function between (conditionally) complete linear ordered spaces sends a Filter.limsSup to the Filter.limsup of the image if the function is continuous at the limsSup (and the filter is bounded from above and below).

theorem Monotone.map_limsup_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : R → S} (f_incr : Monotone f) (a : ι → R) (f_cont : ContinuousAt f (Filter.limsup a F)) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) F a) _auto✝) : f (Filter.limsup a F) = Filter.limsup (f ∘ a) F

A continuous monotone function between (conditionally) complete linear ordered spaces sends a Filter.limsup to the Filter.limsup of the images (if the filter is bounded from above and below).

theorem Monotone.map_limsInf_of_continuousAt {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [Filter.NeBot F] {f : R → S} (f_incr : Monotone f) (f_cont : ContinuousAt f (Filter.limsInf F)) (bdd_above : autoParam (Filter.IsBounded (fun (x x_1 : R) => x ≤ x_1) F) _auto✝) (bdd_below : autoParam (Filter.IsBounded (fun (x x_1 : R) => x ≥ x_1) F) _auto✝) : f (Filter.limsInf F) = Filter.liminf f F

A monotone function between (conditionally) complete linear ordered spaces sends a Filter.limsInf to the Filter.liminf of the image if the function is continuous at the limsInf (and the filter is bounded from above and below).

theorem Monotone.map_liminf_of_continuousAt {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [Filter.NeBot F] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : R → S} (f_incr : Monotone f) (a : ι → R) (f_cont : ContinuousAt f (Filter.liminf a F)) (bdd_above : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F a) _auto✝) (bdd_below : autoParam (Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) F a) _auto✝) : f (Filter.liminf a F) = Filter.liminf (f ∘ a) F

A continuous monotone function between (conditionally) complete linear ordered spaces sends a Filter.liminf to the Filter.liminf of the images (if the filter is bounded from above and below).

theorem iInf_eq_of_forall_le_of_tendsto {ι : Type u_1} {R : Type u_4} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] {x : R} {as : ι → R} (x_le : ∀ (i : ι), x ≤ as i) {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (nhds x)) : ⨅ (i : ι), as i = x

theorem iSup_eq_of_forall_le_of_tendsto {ι : Type u_1} {R : Type u_4} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] {x : R} {as : ι → R} (le_x : ∀ (i : ι), as i ≤ x) {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (nhds x)) : ⨆ (i : ι), as i = x

theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type u_1} {R : Type u_4} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (x : R) {as : ι → R} (x_lt : ∀ (i : ι), x < as i) {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (nhds x)) : ⋃ (i : ι), Set.Ici (as i) = Set.Ioi x

theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {ι : Type u_1} {R : Type u_4} [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (x : R) {as : ι → R} (lt_x : ∀ (i : ι), as i < x) {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (nhds x)) : ⋃ (i : ι), Set.Iic (as i) = Set.Iio x

theorem limsup_eq_tendsto_sum_indicator_nat_atTop {α : Type u_2} (s : ℕ → Set α) : Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range n) fun (k : ℕ) => Set.indicator (s (k + 1)) 1 ω) Filter.atTop Filter.atTop}

theorem limsup_eq_tendsto_sum_indicator_atTop {α : Type u_2} (R : Type u_7) [StrictOrderedSemiring R] [Archimedean R] (s : ℕ → Set α) : Filter.limsup s Filter.atTop = {ω : α | Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range n) fun (k : ℕ) => Set.indicator (s (k + 1)) 1 ω) Filter.atTop Filter.atTop}

theorem limsup_const_add {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [Add R] [ContinuousAdd R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x ≤ y] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) 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 ι) [Filter.NeBot F] [Add R] [ContinuousAdd R] [CovariantClass R R (Function.swap fun (x y : R) => x + y) fun (x y : R) => x ≤ y] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) 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 ι) [Filter.NeBot F] [Add R] [ContinuousAdd R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x ≤ y] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) F f) : Filter.liminf (fun (i : ι) => c + f i) F = c + Filter.liminf f F

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

theorem liminf_add_const {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [Filter.NeBot F] [Add R] [ContinuousAdd R] [CovariantClass R R (Function.swap fun (x y : R) => x + y) fun (x y : R) => x ≤ y] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) 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 ι) [Filter.NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x ≤ y] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) 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 ι) [Filter.NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) 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 ι) [Filter.NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [CovariantClass R R (fun (x y : R) => x + y) fun (x y : R) => x ≤ y] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) 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 ι) [Filter.NeBot F] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≤ x_1) F f) (bdd_below : Filter.IsBoundedUnder (fun (x x_1 : R) => x ≥ x_1) F f) : Filter.liminf (fun (i : ι) => f i - c) F = Filter.liminf f F - c

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