liminfs and limsups of functions and filters

Defines the liminf/limsup of a function taking values in a conditionally complete lattice, with respect to an arbitrary filter.

We define limsSup f (limsInf f) where f is a filter taking values in a conditionally complete lattice. limsSup f is the smallest element a such that, eventually, u ≤ a (and vice versa for limsInf f). To work with the Limsup along a function u use limsSup (map u f).

Usually, one defines the Limsup as inf (sup s) where the Inf is taken over all sets in the filter. For instance, in ℕ along a function u, this is inf_n (sup_{k ≥ n} u k) (and the latter quantity decreases with n, so this is in fact a limit.). There is however a difficulty: it is well possible that u is not bounded on the whole space, only eventually (think of limsup (fun x ↦ 1/x) on ℝ. Then there is no guarantee that the quantity above really decreases (the value of the sup beforehand is not really well defined, as one can not use ∞), so that the Inf could be anything. So one can not use this inf sup ... definition in conditionally complete lattices, and one has to use a less tractable definition.

In conditionally complete lattices, the definition is only useful for filters which are eventually bounded above (otherwise, the Limsup would morally be +∞, which does not belong to the space) and which are frequently bounded below (otherwise, the Limsup would morally be -∞, which is not in the space either). We start with definitions of these concepts for arbitrary filters, before turning to the definitions of Limsup and Liminf.

In complete lattices, however, it coincides with the Inf Sup definition.

def Filter.limsSup {α : Type u_1} [ConditionallyCompleteLattice α] (f : Filter α) : α

The limsSup of a filter f is the infimum of the a such that, eventually for f, holds x ≤ a.

Equations

• f.limsSup = sInf {a : α | ∀ᶠ (n : α) in f, n ≤ a}

def Filter.limsInf {α : Type u_1} [ConditionallyCompleteLattice α] (f : Filter α) : α

The limsInf of a filter f is the supremum of the a such that, eventually for f, holds x ≥ a.

Equations

• f.limsInf = sSup {a : α | ∀ᶠ (n : α) in f, a ≤ n}

def Filter.limsup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) : α

The limsup of a function u along a filter f is the infimum of the a such that, eventually for f, holds u x ≤ a.

Equations

• Filter.limsup u f = (Filter.map u f).limsSup

def Filter.liminf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) : α

The liminf of a function u along a filter f is the supremum of the a such that, eventually for f, holds u x ≥ a.

Equations

• Filter.liminf u f = (Filter.map u f).limsInf

def Filter.blimsup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) (p : β → Prop) : α

The blimsup of a function u along a filter f, bounded by a predicate p, is the infimum of the a such that, eventually for f, u x ≤ a whenever p x holds.

Equations

• Filter.blimsup u f p = sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}

def Filter.bliminf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) (p : β → Prop) : α

The bliminf of a function u along a filter f, bounded by a predicate p, is the supremum of the a such that, eventually for f, a ≤ u x whenever p x holds.

Equations

• Filter.bliminf u f p = sSup {a : α | ∀ᶠ (x : β) in f, p x → a ≤ u x}

theorem Filter.limsup_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} : limsup u f = sInf {a : α | ∀ᶠ (n : β) in f, u n ≤ a}

theorem Filter.liminf_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} : liminf u f = sSup {a : α | ∀ᶠ (n : β) in f, a ≤ u n}

theorem Filter.blimsup_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : blimsup u f p = sInf {a : α | ∀ᶠ (x : β) in f, p x → u x ≤ a}

theorem Filter.bliminf_eq {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : bliminf u f p = sSup {a : α | ∀ᶠ (x : β) in f, p x → a ≤ u x}

theorem Filter.liminf_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] (u : β → α) (v : γ → β) (f : Filter γ) : liminf (u ∘ v) f = liminf u (map v f)

theorem Filter.limsup_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] (u : β → α) (v : γ → β) (f : Filter γ) : limsup (u ∘ v) f = limsup u (map v f)

@[simp]

theorem Filter.blimsup_true {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (f : Filter β) (u : β → α) : (blimsup u f fun (x : β) => True) = limsup u f

@[simp]

theorem Filter.bliminf_true {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (f : Filter β) (u : β → α) : (bliminf u f fun (x : β) => True) = liminf u f

theorem Filter.blimsup_eq_limsup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : blimsup u f p = limsup u (f ⊓ principal {x : β | p x})

theorem Filter.bliminf_eq_liminf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : bliminf u f p = liminf u (f ⊓ principal {x : β | p x})

theorem Filter.blimsup_eq_limsup_subtype {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : blimsup u f p = limsup (u ∘ Subtype.val) (comap Subtype.val f)

theorem Filter.bliminf_eq_liminf_subtype {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : bliminf u f p = liminf (u ∘ Subtype.val) (comap Subtype.val f)

theorem Filter.limsSup_le_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} {a : α} (hf : IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (h : ∀ᶠ (n : α) in f, n ≤ a) : f.limsSup ≤ a

theorem Filter.le_limsInf_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} {a : α} (hf : IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (h : ∀ᶠ (n : α) in f, a ≤ n) : a ≤ f.limsInf

theorem Filter.limsup_le_of_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h : ∀ᶠ (n : β) in f, u n ≤ a) : limsup u f ≤ a

theorem Filter.le_liminf_of_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) (h : ∀ᶠ (n : β) in f, a ≤ u n) : a ≤ liminf u f

theorem Filter.le_limsSup_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} {a : α} (hf : IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : α) in f, n ≤ b) → a ≤ b) : a ≤ f.limsSup

theorem Filter.limsInf_le_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} {a : α} (hf : IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : α) in f, b ≤ n) → b ≤ a) : f.limsInf ≤ a

theorem Filter.le_limsup_of_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : β) in f, u n ≤ b) → a ≤ b) : a ≤ limsup u f

theorem Filter.liminf_le_of_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : β) in f, b ≤ u n) → b ≤ a) : liminf u f ≤ a

theorem Filter.limsInf_le_limsSup {α : Type u_1} [ConditionallyCompleteLattice α] {f : Filter α} [f.NeBot] (h₁ : IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (h₂ : IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) : f.limsInf ≤ f.limsSup

theorem Filter.liminf_le_limsup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} [f.NeBot] {u : β → α} (h : IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u := by isBoundedDefault) (h' : IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u := by isBoundedDefault) : liminf u f ≤ limsup u f

theorem Filter.limsSup_le_limsSup {α : Type u_1} [ConditionallyCompleteLattice α] {f g : Filter α} (hf : IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (hg : IsBounded (fun (x1 x2 : α) => x1 ≤ x2) g := by isBoundedDefault) (h : ∀ (a : α), (∀ᶠ (n : α) in g, n ≤ a) → ∀ᶠ (n : α) in f, n ≤ a) : f.limsSup ≤ g.limsSup

theorem Filter.limsInf_le_limsInf {α : Type u_1} [ConditionallyCompleteLattice α] {f g : Filter α} (hf : IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (hg : IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) g := by isBoundedDefault) (h : ∀ (a : α), (∀ᶠ (n : α) in f, a ≤ n) → ∀ᶠ (n : α) in g, a ≤ n) : f.limsInf ≤ g.limsInf

theorem Filter.limsup_le_limsup {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : u ≤ᶠ[f] v) (hu : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (hv : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v := by isBoundedDefault) : limsup u f ≤ limsup v f

theorem Filter.liminf_le_liminf {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a ≤ v a) (hu : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (hv : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f v := by isBoundedDefault) : liminf u f ≤ liminf v f

theorem Filter.limsSup_le_limsSup_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f g : Filter α} (h : f ≤ g) (hf : IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (hg : IsBounded (fun (x1 x2 : α) => x1 ≤ x2) g := by isBoundedDefault) : f.limsSup ≤ g.limsSup

theorem Filter.limsInf_le_limsInf_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {f g : Filter α} (h : g ≤ f) (hf : IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (hg : IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) g := by isBoundedDefault) : f.limsInf ≤ g.limsInf

theorem Filter.limsup_le_limsup_of_le {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLattice β] {f g : Filter α} (h : f ≤ g) {u : α → β} (hf : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (hg : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) g u := by isBoundedDefault) : limsup u f ≤ limsup u g

theorem Filter.liminf_le_liminf_of_le {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLattice β] {f g : Filter α} (h : g ≤ f) {u : α → β} (hf : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (hg : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) g u := by isBoundedDefault) : liminf u f ≤ liminf u g

theorem Filter.limsSup_principal_eq_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddAbove s) (hs : s.Nonempty) : (principal s).limsSup = sSup s

theorem Filter.limsInf_principal_eq_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddBelow s) (hs : s.Nonempty) : (principal s).limsInf = sInf s

theorem Filter.limsup_top_eq_ciSup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {u : β → α} [Nonempty β] (hu : BddAbove (Set.range u)) : limsup u ⊤ = ⨆ (i : β), u i

theorem Filter.liminf_top_eq_ciInf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {u : β → α} [Nonempty β] (hu : BddBelow (Set.range u)) : liminf u ⊤ = ⨅ (i : β), u i

theorem Filter.limsup_congr {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a = v a) : limsup u f = limsup v f

theorem Filter.blimsup_congr {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ (a : β) in f, p a → u a = v a) : blimsup u f p = blimsup v f p

theorem Filter.bliminf_congr {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ (a : β) in f, p a → u a = v a) : bliminf u f p = bliminf v f p

theorem Filter.liminf_congr {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a = v a) : liminf u f = liminf v f

@[simp]

theorem Filter.limsup_const {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β) : limsup (fun (x : α) => b) f = b

@[simp]

theorem Filter.liminf_const {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β) : liminf (fun (x : α) => b) f = b

theorem Filter.HasBasis.liminf_eq_sSup_iUnion_iInter {α : Type u_1} [ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) : liminf f v = sSup (⋃ (j : Subtype p), ⋂ (i : ↑(s ↑j)), Set.Iic (f ↑i))

theorem Filter.HasBasis.liminf_eq_sSup_univ_of_empty {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLattice α] {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) : liminf f v = sSup Set.univ

theorem Filter.HasBasis.limsup_eq_sInf_iUnion_iInter {α : Type u_1} [ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) : limsup f v = sInf (⋃ (j : Subtype p), ⋂ (i : ↑(s ↑j)), Set.Ici (f ↑i))

theorem Filter.HasBasis.limsup_eq_sInf_univ_of_empty {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLattice α] {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) : limsup f v = sInf Set.univ

@[simp]

theorem Filter.liminf_nat_add {α : Type u_1} [ConditionallyCompleteLattice α] (f : ℕ → α) (k : ℕ) : liminf (fun (i : ℕ) => f (i + k)) atTop = liminf f atTop

@[simp]

theorem Filter.limsup_nat_add {α : Type u_1} [ConditionallyCompleteLattice α] (f : ℕ → α) (k : ℕ) : limsup (fun (i : ℕ) => f (i + k)) atTop = limsup f atTop

@[simp]

theorem Filter.limsSup_bot {α : Type u_1} [CompleteLattice α] : ⊥.limsSup = ⊥

@[simp]

theorem Filter.limsup_bot {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) : limsup f ⊥ = ⊥

@[simp]

theorem Filter.limsInf_bot {α : Type u_1} [CompleteLattice α] : ⊥.limsInf = ⊤

@[simp]

theorem Filter.liminf_bot {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) : liminf f ⊥ = ⊤

@[simp]

theorem Filter.limsSup_top {α : Type u_1} [CompleteLattice α] : ⊤.limsSup = ⊤

@[simp]

theorem Filter.limsInf_top {α : Type u_1} [CompleteLattice α] : ⊤.limsInf = ⊥

@[simp]

theorem Filter.blimsup_false {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : (blimsup u f fun (x : β) => False) = ⊥

@[simp]

theorem Filter.bliminf_false {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : (bliminf u f fun (x : β) => False) = ⊤

@[simp]

theorem Filter.limsup_const_bot {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} : limsup (fun (x : β) => ⊥) f = ⊥

Same as limsup_const applied to ⊥ but without the NeBot f assumption

@[simp]

theorem Filter.liminf_const_top {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} : liminf (fun (x : β) => ⊤) f = ⊤

Same as limsup_const applied to ⊤ but without the NeBot f assumption

theorem Filter.HasBasis.limsSup_eq_iInf_sSup {α : Type u_1} [CompleteLattice α] {ι : Sort u_6} {p : ι → Prop} {s : ι → Set α} {f : Filter α} (h : f.HasBasis p s) : f.limsSup = ⨅ (i : ι), ⨅ (_ : p i), sSup (s i)

theorem Filter.HasBasis.limsInf_eq_iSup_sInf {α : Type u_1} {ι : Type u_4} [CompleteLattice α] {p : ι → Prop} {s : ι → Set α} {f : Filter α} (h : f.HasBasis p s) : f.limsInf = ⨆ (i : ι), ⨆ (_ : p i), sInf (s i)

theorem Filter.limsSup_eq_iInf_sSup {α : Type u_1} [CompleteLattice α] {f : Filter α} : f.limsSup = ⨅ s ∈ f, sSup s

theorem Filter.limsInf_eq_iSup_sInf {α : Type u_1} [CompleteLattice α] {f : Filter α} : f.limsInf = ⨆ s ∈ f, sInf s

theorem Filter.limsup_le_iSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : limsup u f ≤ ⨆ (n : β), u n

theorem Filter.iInf_le_liminf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : ⨅ (n : β), u n ≤ liminf u f

theorem Filter.limsup_eq_iInf_iSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a

In a complete lattice, the limsup of a function is the infimum over sets s in the filter of the supremum of the function over s

theorem Filter.limsup_eq_iInf_iSup_of_nat {α : Type u_1} [CompleteLattice α] {u : ℕ → α} : limsup u atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i

theorem Filter.limsup_eq_iInf_iSup_of_nat' {α : Type u_1} [CompleteLattice α] {u : ℕ → α} : limsup u atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), u (i + n)

theorem Filter.HasBasis.limsup_eq_iInf_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (h : f.HasBasis p s) : limsup u f = ⨅ (i : ι), ⨅ (_ : p i), ⨆ a ∈ s i, u a

theorem Filter.limsSup_principal_eq_sSup {α : Type u_1} [CompleteLattice α] (s : Set α) : (principal s).limsSup = sSup s

theorem Filter.limsInf_principal_eq_sInf {α : Type u_1} [CompleteLattice α] (s : Set α) : (principal s).limsInf = sInf s

@[simp]

theorem Filter.limsup_top_eq_iSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] (u : β → α) : limsup u ⊤ = ⨆ (i : β), u i

@[simp]

theorem Filter.liminf_top_eq_iInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] (u : β → α) : liminf u ⊤ = ⨅ (i : β), u i

theorem Filter.blimsup_congr' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)) : blimsup u f p = blimsup u f q

theorem Filter.bliminf_congr' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ᶠ (x : β) in f, u x ≠ ⊤ → (p x ↔ q x)) : bliminf u f p = bliminf u f q

theorem Filter.HasBasis.blimsup_eq_iInf_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (hf : f.HasBasis p s) {q : β → Prop} : blimsup u f q = ⨅ (i : ι), ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

theorem Filter.blimsup_eq_iInf_biSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : blimsup u f p = ⨅ s ∈ f, ⨆ (b : β), ⨆ (_ : p b ∧ b ∈ s), u b

theorem Filter.blimsup_eq_iInf_biSup_of_nat {α : Type u_1} [CompleteLattice α] {p : ℕ → Prop} {u : ℕ → α} : blimsup u atTop p = ⨅ (i : ℕ), ⨆ (j : ℕ), ⨆ (_ : p j ∧ i ≤ j), u j

theorem Filter.liminf_eq_iSup_iInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a

In a complete lattice, the liminf of a function is the infimum over sets s in the filter of the supremum of the function over s

theorem Filter.liminf_eq_iSup_iInf_of_nat {α : Type u_1} [CompleteLattice α] {u : ℕ → α} : liminf u atTop = ⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), u i

theorem Filter.liminf_eq_iSup_iInf_of_nat' {α : Type u_1} [CompleteLattice α] {u : ℕ → α} : liminf u atTop = ⨆ (n : ℕ), ⨅ (i : ℕ), u (i + n)

theorem Filter.HasBasis.liminf_eq_iSup_iInf {α : Type u_1} {β : Type u_2} {ι : Type u_4} [CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (h : f.HasBasis p s) : liminf u f = ⨆ (i : ι), ⨆ (_ : p i), ⨅ a ∈ s i, u a

theorem Filter.bliminf_eq_iSup_biInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : bliminf u f p = ⨆ s ∈ f, ⨅ (b : β), ⨅ (_ : p b ∧ b ∈ s), u b

theorem Filter.bliminf_eq_iSup_biInf_of_nat {α : Type u_1} [CompleteLattice α] {p : ℕ → Prop} {u : ℕ → α} : bliminf u atTop p = ⨆ (i : ℕ), ⨅ (j : ℕ), ⨅ (_ : p j ∧ i ≤ j), u j

theorem Filter.limsup_eq_sInf_sSup {ι : Type u_6} {R : Type u_7} (F : Filter ι) [CompleteLattice R] (a : ι → R) : limsup a F = sInf ((fun (I : Set ι) => sSup (a '' I)) '' F.sets)

theorem Filter.liminf_eq_sSup_sInf {ι : Type u_6} {R : Type u_7} (F : Filter ι) [CompleteLattice R] (a : ι → R) : liminf a F = sSup ((fun (I : Set ι) => sInf (a '' I)) '' F.sets)

theorem Filter.liminf_le_of_frequently_le' {α : Type u_6} {β : Type u_7} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β} (h : ∃ᶠ (a : α) in f, u a ≤ x) : liminf u f ≤ x

theorem Filter.le_limsup_of_frequently_le' {α : Type u_6} {β : Type u_7} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β} (h : ∃ᶠ (a : α) in f, x ≤ u a) : x ≤ limsup u f

@[simp]

theorem CompleteLatticeHom.apply_limsup_iterate {α : Type u_1} [CompleteLattice α] (f : CompleteLatticeHom α α) (a : α) : f (Filter.limsup (fun (n : ℕ) => (⇑f)^[n] a) Filter.atTop) = Filter.limsup (fun (n : ℕ) => (⇑f)^[n] a) Filter.atTop

If f : α → α is a morphism of complete lattices, then the limsup of its iterates of any a : α is a fixed point.

theorem CompleteLatticeHom.apply_liminf_iterate {α : Type u_1} [CompleteLattice α] (f : CompleteLatticeHom α α) (a : α) : f (Filter.liminf (fun (n : ℕ) => (⇑f)^[n] a) Filter.atTop) = Filter.liminf (fun (n : ℕ) => (⇑f)^[n] a) Filter.atTop

If f : α → α is a morphism of complete lattices, then the liminf of its iterates of any a : α is a fixed point.

theorem Filter.blimsup_mono {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ (x : β), p x → q x) : blimsup u f p ≤ blimsup u f q

theorem Filter.bliminf_antitone {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} (h : ∀ (x : β), p x → q x) : bliminf u f q ≤ bliminf u f p

theorem Filter.mono_blimsup' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α} (h : ∀ᶠ (x : β) in f, p x → u x ≤ v x) : blimsup u f p ≤ blimsup v f p

theorem Filter.mono_blimsup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α} (h : ∀ (x : β), p x → u x ≤ v x) : blimsup u f p ≤ blimsup v f p

theorem Filter.mono_bliminf' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α} (h : ∀ᶠ (x : β) in f, p x → u x ≤ v x) : bliminf u f p ≤ bliminf v f p

theorem Filter.mono_bliminf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α} (h : ∀ (x : β), p x → u x ≤ v x) : bliminf u f p ≤ bliminf v f p

theorem Filter.bliminf_antitone_filter {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f g : Filter β} {p : β → Prop} {u : β → α} (h : f ≤ g) : bliminf u g p ≤ bliminf u f p

theorem Filter.blimsup_monotone_filter {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f g : Filter β} {p : β → Prop} {u : β → α} (h : f ≤ g) : blimsup u f p ≤ blimsup u g p

theorem Filter.blimsup_and_le_inf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : (blimsup u f fun (x : β) => p x ∧ q x) ≤ blimsup u f p ⊓ blimsup u f q

@[simp]

theorem Filter.bliminf_sup_le_inf_aux_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : (blimsup u f fun (x : β) => p x ∧ q x) ≤ blimsup u f p

@[simp]

theorem Filter.bliminf_sup_le_inf_aux_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : (blimsup u f fun (x : β) => p x ∧ q x) ≤ blimsup u f q

theorem Filter.bliminf_sup_le_and {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : bliminf u f p ⊔ bliminf u f q ≤ bliminf u f fun (x : β) => p x ∧ q x

@[simp]

theorem Filter.bliminf_sup_le_and_aux_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : bliminf u f p ≤ bliminf u f fun (x : β) => p x ∧ q x

@[simp]

theorem Filter.bliminf_sup_le_and_aux_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : bliminf u f q ≤ bliminf u f fun (x : β) => p x ∧ q x

theorem Filter.blimsup_sup_le_or {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : blimsup u f p ⊔ blimsup u f q ≤ blimsup u f fun (x : β) => p x ∨ q x

See also Filter.blimsup_or_eq_sup.

@[simp]

theorem Filter.bliminf_sup_le_or_aux_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : blimsup u f p ≤ blimsup u f fun (x : β) => p x ∨ q x

@[simp]

theorem Filter.bliminf_sup_le_or_aux_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : blimsup u f q ≤ blimsup u f fun (x : β) => p x ∨ q x

theorem Filter.bliminf_or_le_inf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : (bliminf u f fun (x : β) => p x ∨ q x) ≤ bliminf u f p ⊓ bliminf u f q

See also Filter.bliminf_or_eq_inf.

@[simp]

theorem Filter.bliminf_or_le_inf_aux_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : (bliminf u f fun (x : β) => p x ∨ q x) ≤ bliminf u f p

@[simp]

theorem Filter.bliminf_or_le_inf_aux_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : (bliminf u f fun (x : β) => p x ∨ q x) ≤ bliminf u f q

theorem OrderIso.apply_blimsup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (e : α ≃o γ) : e (Filter.blimsup u f p) = Filter.blimsup (⇑e ∘ u) f p

theorem OrderIso.apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (e : α ≃o γ) : e (Filter.bliminf u f p) = Filter.bliminf (⇑e ∘ u) f p

theorem sSupHom.apply_blimsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (g : sSupHom α γ) : g (Filter.blimsup u f p) ≤ Filter.blimsup (⇑g ∘ u) f p

theorem sInfHom.le_apply_bliminf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α} [CompleteLattice γ] (g : sInfHom α γ) : Filter.bliminf (⇑g ∘ u) f p ≤ g (Filter.bliminf u f p)

theorem Filter.limsup_sup_filter {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {g : Filter β} : limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

theorem Filter.liminf_sup_filter {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {g : Filter β} : liminf u (f ⊔ g) = liminf u f ⊓ liminf u g

@[simp]

theorem Filter.blimsup_or_eq_sup {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : (blimsup u f fun (x : β) => p x ∨ q x) = blimsup u f p ⊔ blimsup u f q

@[simp]

theorem Filter.bliminf_or_eq_inf {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p q : β → Prop} {u : β → α} : (bliminf u f fun (x : β) => p x ∨ q x) = bliminf u f p ⊓ bliminf u f q

@[simp]

theorem Filter.blimsup_sup_not {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : (blimsup u f p ⊔ blimsup u f fun (x : β) => ¬p x) = limsup u f

@[simp]

theorem Filter.bliminf_inf_not {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : (bliminf u f p ⊓ bliminf u f fun (x : β) => ¬p x) = liminf u f

@[simp]

theorem Filter.blimsup_not_sup {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : (blimsup u f fun (x : β) => ¬p x) ⊔ blimsup u f p = limsup u f

@[simp]

theorem Filter.bliminf_not_inf {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : (bliminf u f fun (x : β) => ¬p x) ⊓ bliminf u f p = liminf u f

theorem Filter.limsup_piecewise {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {s : Set β} [DecidablePred fun (x : β) => x ∈ s] {v : β → α} : limsup (s.piecewise u v) f = (blimsup u f fun (x : β) => x ∈ s) ⊔ blimsup v f fun (x : β) => x ∉ s

theorem Filter.liminf_piecewise {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {s : Set β} [DecidablePred fun (x : β) => x ∈ s] {v : β → α} : liminf (s.piecewise u v) f = (bliminf u f fun (x : β) => x ∈ s) ⊓ bliminf v f fun (x : β) => x ∉ s

theorem Filter.sup_limsup {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α) : a ⊔ limsup u f = limsup (fun (x : β) => a ⊔ u x) f

theorem Filter.inf_liminf {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α) : a ⊓ liminf u f = liminf (fun (x : β) => a ⊓ u x) f

theorem Filter.sup_liminf {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} (a : α) : a ⊔ liminf u f = liminf (fun (x : β) => a ⊔ u x) f

theorem Filter.inf_limsup {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} (a : α) : a ⊓ limsup u f = limsup (fun (x : β) => a ⊓ u x) f

theorem Filter.limsup_compl {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) : (limsup u f)ᶜ = liminf (compl ∘ u) f

theorem Filter.liminf_compl {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) : (liminf u f)ᶜ = limsup (compl ∘ u) f

theorem Filter.limsup_sdiff {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) (a : α) : limsup u f \ a = limsup (fun (b : β) => u b \ a) f

theorem Filter.liminf_sdiff {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α) : liminf u f \ a = liminf (fun (b : β) => u b \ a) f

theorem Filter.sdiff_limsup {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α) : a \ limsup u f = liminf (fun (b : β) => a \ u b) f

theorem Filter.sdiff_liminf {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) (a : α) : a \ liminf u f = limsup (fun (b : β) => a \ u b) f

theorem Filter.mem_liminf_iff_eventually_mem {α : Type u_1} {ι : Type u_4} {s : ι → Set α} {𝓕 : Filter ι} {a : α} : a ∈ liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i

theorem Filter.mem_limsup_iff_frequently_mem {α : Type u_1} {ι : Type u_4} {s : ι → Set α} {𝓕 : Filter ι} {a : α} : a ∈ limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i

theorem Filter.cofinite.blimsup_set_eq {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α} : blimsup s cofinite p = {x : α | {n : ι | p n ∧ x ∈ s n}.Infinite}

theorem Filter.cofinite.bliminf_set_eq {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α} : bliminf s cofinite p = {x : α | {n : ι | p n ∧ x ∉ s n}.Finite}

theorem Filter.cofinite.limsup_set_eq {α : Type u_1} {ι : Type u_4} {s : ι → Set α} : limsup s cofinite = {x : α | {n : ι | x ∈ s n}.Infinite}

In other words, limsup cofinite s is the set of elements lying inside the family s infinitely often.

theorem Filter.cofinite.liminf_set_eq {α : Type u_1} {ι : Type u_4} {s : ι → Set α} : liminf s cofinite = {x : α | {n : ι | x ∉ s n}.Finite}

In other words, liminf cofinite s is the set of elements lying outside the family s finitely often.

theorem Filter.exists_forall_mem_of_hasBasis_mem_blimsup {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : Filter β} {b : ι → Set β} {q : ι → Prop} (hl : l.HasBasis q b) {u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ blimsup u l p) : ∃ (f : ↑{i : ι | q i} → β), ∀ (i : ↑{i : ι | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i

theorem Filter.exists_forall_mem_of_hasBasis_mem_blimsup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : Filter β} {b : ι → Set β} (hl : l.HasBasis (fun (x : ι) => True) b) {u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ blimsup u l p) : ∃ (f : ι → β), ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i

theorem Filter.frequently_lt_of_lt_limsSup {α : Type u_1} {f : Filter α} [ConditionallyCompleteLinearOrder α] {a : α} (hf : IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f := by isBoundedDefault) (h : a < f.limsSup) : ∃ᶠ (n : α) in f, a < n

theorem Filter.frequently_lt_of_limsInf_lt {α : Type u_1} {f : Filter α} [ConditionallyCompleteLinearOrder α] {a : α} (hf : IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f := by isBoundedDefault) (h : f.limsInf < a) : ∃ᶠ (n : α) in f, n < a

theorem Filter.eventually_lt_of_lt_liminf {α : Type u_1} {β : Type u_2} {f : Filter α} [ConditionallyCompleteLinearOrder β] {u : α → β} {b : β} (h : b < liminf u f) (hu : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) : ∀ᶠ (a : α) in f, b < u a

theorem Filter.eventually_lt_of_limsup_lt {α : Type u_1} {β : Type u_2} {f : Filter α} [ConditionallyCompleteLinearOrder β] {u : α → β} {b : β} (h : limsup u f < b) (hu : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) : ∀ᶠ (a : α) in f, u a < b

theorem Filter.eventually_lt_add_pos_of_limsup_le {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [Preorder β] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder LE.le atTop u) (hu : limsup u atTop ≤ x) (hε : 0 < ε) : ∀ᶠ (b : β) in atTop, u b < x + ε

If Filter.limsup u atTop ≤ x, then for all ε > 0, eventually we have u b < x + ε.

theorem Filter.eventually_add_neg_lt_of_le_liminf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [Preorder β] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α} (hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ liminf u atTop) (hε : ε < 0) : ∀ᶠ (b : β) in atTop, x + ε < u b

If x ≤ Filter.liminf u atTop, then for all ε < 0, eventually we have x + ε < u b.

theorem Filter.exists_lt_of_limsup_le {α : Type u_1} [ConditionallyCompleteLinearOrder α] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α} (hu_bdd : IsBoundedUnder LE.le atTop u) (hu : limsup u atTop ≤ x) (hε : 0 < ε) : ∃ (n : ℕ+), u ↑n < x + ε

If Filter.limsup u atTop ≤ x, then for all ε > 0, there exists a positive natural number n such that u n < x + ε.

theorem Filter.exists_lt_of_le_liminf {α : Type u_1} [ConditionallyCompleteLinearOrder α] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α} (hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ liminf u atTop) (hε : ε < 0) : ∃ (n : ℕ+), x + ε < u ↑n

If x ≤ Filter.liminf u atTop, then for all ε < 0, there exists a positive natural number n such that x + ε < u n.

theorem Filter.le_limsup_of_frequently_le {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu_le : ∃ᶠ (x : α) in f, b ≤ u x) (hu : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) : b ≤ limsup u f

theorem Filter.liminf_le_of_frequently_le {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu_le : ∃ᶠ (x : α) in f, u x ≤ b) (hu : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) : liminf u f ≤ b

theorem Filter.frequently_lt_of_lt_limsup {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (h : b < limsup u f) : ∃ᶠ (x : α) in f, b < u x

theorem Filter.frequently_lt_of_liminf_lt {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (h : liminf u f < b) : ∃ᶠ (x : α) in f, u x < b

theorem Filter.limsup_le_iff {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) : limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y

theorem Filter.le_limsup_iff {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) : x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a

theorem Filter.le_liminf_iff {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) : x ≤ liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y < u a

theorem Filter.liminf_le_iff {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) : liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a < y

theorem Filter.lt_mem_sets_of_limsSup_lt {α : Type u_1} [ConditionallyCompleteLinearOrder α] {f : Filter α} {b : α} (h : IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f) (l : f.limsSup < b) : ∀ᶠ (a : α) in f, a < b

theorem Filter.gt_mem_sets_of_limsInf_gt {α : Type u_1} [ConditionallyCompleteLinearOrder α] {f : Filter α} {b : α} : IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f → b < f.limsInf → ∀ᶠ (a : α) in f, b < a

noncomputable def Filter.liminf_reparam {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)] (j : Subtype p) : Subtype p

Given an indexed family of sets s j over j : Subtype p and a function f, then liminf_reparam j is equal to j if f is bounded below on s j, and otherwise to some index k such that f is bounded below on s k (if there exists one). To ensure good measurability behavior, this index k is chosen as the minimal suitable index. This function is used to write down a liminf in a measurable way, in Filter.HasBasis.liminf_eq_ciSup_ciInf and Filter.HasBasis.liminf_eq_ite.

Equations

• Filter.liminf_reparam f s p j = if j ∈ {j : Subtype p | BddBelow (Set.range fun (i : ↑(s ↑j)) => f ↑i)} then j else ⋯.choose (Nat.find ⋯)

theorem Filter.HasBasis.liminf_eq_ciSup_ciInf {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s ↑j).Nonempty) (H : ∃ (j : Subtype p), BddBelow (Set.range fun (i : ↑(s ↑j)) => f ↑i)) : liminf f v = ⨆ (j : Subtype p), ⨅ (i : ↑(s ↑(liminf_reparam f s p j))), f ↑i

Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are not bounded below.

theorem Filter.HasBasis.liminf_eq_ite {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) : liminf f v = if ∃ (j : Subtype p), s ↑j = ∅ then sSup Set.univ else if ∀ (j : Subtype p), ¬BddBelow (Set.range fun (i : ↑(s ↑j)) => f ↑i) then sSup ∅ else ⨆ (j : Subtype p), ⨅ (i : ↑(s ↑(liminf_reparam f s p j))), f ↑i

Writing a liminf as a supremum of infimum, in a (possibly non-complete) conditionally complete linear order. A reparametrization trick is needed to avoid taking the infimum of sets which are not bounded below.

noncomputable def Filter.limsup_reparam {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)] [Nonempty (Subtype p)] (j : Subtype p) : Subtype p

Given an indexed family of sets s j and a function f, then limsup_reparam j is equal to j if f is bounded above on s j, and otherwise to some index k such that f is bounded above on s k (if there exists one). To ensure good measurability behavior, this index k is chosen as the minimal suitable index. This function is used to write down a limsup in a measurable way, in Filter.HasBasis.limsup_eq_ciInf_ciSup and Filter.HasBasis.limsup_eq_ite.

Equations

• Filter.limsup_reparam f s p j = Filter.liminf_reparam f s p j

theorem Filter.HasBasis.limsup_eq_ciInf_ciSup {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s ↑j).Nonempty) (H : ∃ (j : Subtype p), BddAbove (Set.range fun (i : ↑(s ↑j)) => f ↑i)) : limsup f v = ⨅ (j : Subtype p), ⨆ (i : ↑(s ↑(limsup_reparam f s p j))), f ↑i

Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are not bounded above.

theorem Filter.HasBasis.limsup_eq_ite {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) : limsup f v = if ∃ (j : Subtype p), s ↑j = ∅ then sInf Set.univ else if ∀ (j : Subtype p), ¬BddAbove (Set.range fun (i : ↑(s ↑j)) => f ↑i) then sInf ∅ else ⨅ (j : Subtype p), ⨆ (i : ↑(s ↑(limsup_reparam f s p j))), f ↑i

Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are not bounded below.

theorem GaloisConnection.l_limsup_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {f : Filter α} {v : α → β} {l : β → γ} {u : γ → β} (gc : GaloisConnection l u) (hlv : Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => l (v x) := by isBoundedDefault) (hv_co : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v := by isBoundedDefault) : l (Filter.limsup v f) ≤ Filter.limsup (fun (x : α) => l (v x)) f

theorem OrderIso.limsup_apply {α : Type u_1} {β : Type u_2} {γ : Type u_6} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (hu_co : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u := by isBoundedDefault) (hgu : Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => g (u x) := by isBoundedDefault) (hgu_co : Filter.IsCoboundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => g (u x) := by isBoundedDefault) : g (Filter.limsup u f) = Filter.limsup (fun (x : α) => g (u x)) f

theorem OrderIso.liminf_apply {α : Type u_1} {β : Type u_2} {γ : Type u_6} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ) (hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (hu_co : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u := by isBoundedDefault) (hgu : Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) f fun (x : α) => g (u x) := by isBoundedDefault) (hgu_co : Filter.IsCoboundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) f fun (x : α) => g (u x) := by isBoundedDefault) : g (Filter.liminf u f) = Filter.liminf (fun (x : α) => g (u x)) f

theorem limsup_max {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β} (h₁ : Filter.IsCoboundedUnder (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 u := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v := by isBoundedDefault) : Filter.limsup (fun (a : α) => u a ⊔ v a) f = Filter.limsup u f ⊔ Filter.limsup v f

theorem liminf_min {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β} (h₁ : Filter.IsCoboundedUnder (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 u := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f v := by isBoundedDefault) : Filter.liminf (fun (a : α) => u a ⊓ v a) f = Filter.liminf u f ⊓ Filter.liminf v f

theorem limsup_finset_sup' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [ConditionallyCompleteLinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) : Filter.limsup (fun (a : α) => s.sup' hs fun (i : ι) => F i a) f = s.sup' hs fun (i : ι) => Filter.limsup (F i) f

theorem limsup_finset_sup {α : Type u_1} {β : Type u_2} {ι : Type u_4} [ConditionallyCompleteLinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) : Filter.limsup (fun (a : α) => s.sup fun (i : ι) => F i a) f = s.sup fun (i : ι) => Filter.limsup (F i) f

theorem liminf_finset_inf' {α : Type u_1} {β : Type u_2} {ι : Type u_4} [ConditionallyCompleteLinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) : Filter.liminf (fun (a : α) => s.inf' hs fun (i : ι) => F i a) f = s.inf' hs fun (i : ι) => Filter.liminf (F i) f

theorem liminf_finset_inf {α : Type u_1} {β : Type u_2} {ι : Type u_4} [ConditionallyCompleteLinearOrder β] [OrderTop β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) : Filter.liminf (fun (a : α) => s.inf fun (i : ι) => F i a) f = s.inf fun (i : ι) => Filter.liminf (F i) f