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.
f.IsBounded (≺): the filter f is eventually bounded w.r.t. the relation ≺, i.e.
eventually, it is bounded by some uniform bound.
r will be usually instantiated with ≤ or ≥.
Equations
- Filter.IsBounded r f = ∃ (b : α), ∀ᶠ (x : α) in f, r x b
Instances For
def
Filter.IsBoundedUnder
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(f : Filter β)
(u : β → α)
:
f.IsBoundedUnder (≺) u: the image of the filter f under u is eventually bounded w.r.t.
the relation ≺, i.e. eventually, it is bounded by some uniform bound.
Equations
- Filter.IsBoundedUnder r f u = Filter.IsBounded r (Filter.map u f)
Instances For
theorem
Filter.isBounded_iff
{α : Type u_1}
{r : α → α → Prop}
{f : Filter α}
:
Filter.IsBounded r f ↔ ∃ s ∈ f.sets, ∃ (b : α), s ⊆ {x : α | r x b}
f is eventually bounded if and only if, there exists an admissible set on which it is
bounded.
theorem
Filter.isBoundedUnder_of
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{f : Filter β}
{u : β → α}
:
(∃ (b : α), ∀ (x : β), r (u x) b) → Filter.IsBoundedUnder r f u
A bounded function u is in particular eventually bounded.
theorem
Filter.isBounded_top
{α : Type u_1}
{r : α → α → Prop}
:
Filter.IsBounded r ⊤ ↔ ∃ (t : α), ∀ (x : α), r x t
theorem
Filter.isBounded_principal
{α : Type u_1}
{r : α → α → Prop}
(s : Set α)
:
Filter.IsBounded r (Filter.principal s) ↔ ∃ (t : α), ∀ x ∈ s, r x t
theorem
Filter.isBounded_sup
{α : Type u_1}
{r : α → α → Prop}
{f : Filter α}
{g : Filter α}
[IsTrans α r]
[IsDirected α r]
:
Filter.IsBounded r f → Filter.IsBounded r g → Filter.IsBounded r (f ⊔ g)
theorem
Filter.IsBounded.mono
{α : Type u_1}
{r : α → α → Prop}
{f : Filter α}
{g : Filter α}
(h : f ≤ g)
:
Filter.IsBounded r g → Filter.IsBounded r f
theorem
Filter.IsBoundedUnder.mono
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{f : Filter β}
{g : Filter β}
{u : β → α}
(h : f ≤ g)
:
Filter.IsBoundedUnder r g u → Filter.IsBoundedUnder r f u
theorem
Filter.IsBoundedUnder.mono_le
{α : Type u_1}
{β : Type u_2}
[Preorder β]
{l : Filter α}
{u : α → β}
{v : α → β}
(hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l u)
(hv : v ≤ᶠ[l] u)
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l v
theorem
Filter.IsBoundedUnder.mono_ge
{α : Type u_1}
{β : Type u_2}
[Preorder β]
{l : Filter α}
{u : α → β}
{v : α → β}
(hu : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l u)
(hv : u ≤ᶠ[l] v)
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l v
theorem
Filter.isBoundedUnder_const
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
[IsRefl α r]
{l : Filter β}
{a : α}
:
Filter.IsBoundedUnder r l fun (x : β) => a
theorem
Filter.IsBounded.isBoundedUnder
{α : Type u_1}
{β : Type u_2}
{r : α → α → Prop}
{f : Filter α}
{q : β → β → Prop}
{u : α → β}
(hu : ∀ (a₀ a₁ : α), r a₀ a₁ → q (u a₀) (u a₁))
:
Filter.IsBounded r f → Filter.IsBoundedUnder q f u
theorem
Filter.IsBoundedUnder.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{r : α → α → Prop}
{l : Filter γ}
{q : β → β → Prop}
{u : γ → α}
{v : α → β}
(hv : ∀ (a₀ a₁ : α), r a₀ a₁ → q (v a₀) (v a₁))
:
Filter.IsBoundedUnder r l u → Filter.IsBoundedUnder q l (v ∘ u)
theorem
BddAbove.isBoundedUnder_of_range
{α : Type u_1}
{β : Type u_2}
[Preorder α]
{f : Filter β}
{u : β → α}
(hu : BddAbove (Set.range u))
:
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
A bounded above function u is in particular eventually bounded above.
theorem
BddBelow.isBoundedUnder_of_range
{α : Type u_1}
{β : Type u_2}
[Preorder α]
{f : Filter β}
{u : β → α}
(hu : BddBelow (Set.range u))
:
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
A bounded below function u is in particular eventually bounded below.
theorem
Monotone.isBoundedUnder_le_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
{l : Filter γ}
{u : γ → α}
{v : α → β}
(hv : Monotone v)
(hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u)
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l (v ∘ u)
theorem
Monotone.isBoundedUnder_ge_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
{l : Filter γ}
{u : γ → α}
{v : α → β}
(hv : Monotone v)
(hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u)
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l (v ∘ u)
theorem
Antitone.isBoundedUnder_le_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
{l : Filter γ}
{u : γ → α}
{v : α → β}
(hv : Antitone v)
(hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u)
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l (v ∘ u)
theorem
Antitone.isBoundedUnder_ge_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
{l : Filter γ}
{u : γ → α}
{v : α → β}
(hv : Antitone v)
(hl : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u)
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l (v ∘ u)
theorem
Filter.not_isBoundedUnder_of_tendsto_atTop
{α : Type u_1}
{β : Type u_2}
[Preorder β]
[NoMaxOrder β]
{f : α → β}
{l : Filter α}
[l.NeBot]
(hf : Filter.Tendsto f l Filter.atTop)
:
¬Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f
theorem
Filter.not_isBoundedUnder_of_tendsto_atBot
{α : Type u_1}
{β : Type u_2}
[Preorder β]
[NoMinOrder β]
{f : α → β}
{l : Filter α}
[l.NeBot]
(hf : Filter.Tendsto f l Filter.atBot)
:
¬Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f
theorem
Filter.IsBoundedUnder.bddAbove_range_of_cofinite
{α : Type u_1}
{β : Type u_2}
[Preorder β]
[IsDirected β fun (x1 x2 : β) => x1 ≤ x2]
{f : α → β}
(hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) Filter.cofinite f)
:
theorem
Filter.IsBoundedUnder.bddBelow_range_of_cofinite
{α : Type u_1}
{β : Type u_2}
[Preorder β]
[IsDirected β fun (x1 x2 : β) => x1 ≥ x2]
{f : α → β}
(hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) Filter.cofinite f)
:
theorem
Filter.IsBoundedUnder.bddAbove_range
{β : Type u_2}
[Preorder β]
[IsDirected β fun (x1 x2 : β) => x1 ≤ x2]
{f : ℕ → β}
(hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) Filter.atTop f)
:
theorem
Filter.IsBoundedUnder.bddBelow_range
{β : Type u_2}
[Preorder β]
[IsDirected β fun (x1 x2 : β) => x1 ≥ x2]
{f : ℕ → β}
(hf : Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) Filter.atTop f)
:
IsCobounded (≺) f states that the filter f does not tend to infinity w.r.t. ≺. This is
also called frequently bounded. Will be usually instantiated with ≤ or ≥.
There is a subtlety in this definition: we want f.IsCobounded to hold for any f in the case of
complete lattices. This will be relevant to deduce theorems on complete lattices from their
versions on conditionally complete lattices with additional assumptions. We have to be careful in
the edge case of the trivial filter containing the empty set: the other natural definition
¬ ∀ a, ∀ᶠ n in f, a ≤ n
would not work as well in this case.
Equations
- Filter.IsCobounded r f = ∃ (b : α), ∀ (a : α), (∀ᶠ (x : α) in f, r x a) → r b a
Instances For
def
Filter.IsCoboundedUnder
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(f : Filter β)
(u : β → α)
:
IsCoboundedUnder (≺) f u states that the image of the filter f under the map u does not
tend to infinity w.r.t. ≺. This is also called frequently bounded. Will be usually instantiated
with ≤ or ≥.
Equations
- Filter.IsCoboundedUnder r f u = Filter.IsCobounded r (Filter.map u f)
Instances For
theorem
Filter.IsCobounded.mk
{α : Type u_1}
{r : α → α → Prop}
{f : Filter α}
[IsTrans α r]
(a : α)
(h : ∀ s ∈ f, ∃ x ∈ s, r a x)
:
To check that a filter is frequently bounded, it suffices to have a witness
which bounds f at some point for every admissible set.
This is only an implication, as the other direction is wrong for the trivial filter.
theorem
Filter.IsBounded.isCobounded_flip
{α : Type u_1}
{r : α → α → Prop}
{f : Filter α}
[IsTrans α r]
[f.NeBot]
:
Filter.IsBounded r f → Filter.IsCobounded (flip r) f
A filter which is eventually bounded is in particular frequently bounded (in the opposite direction). At least if the filter is not trivial.
theorem
Filter.IsBounded.isCobounded_ge
{α : Type u_1}
{f : Filter α}
[Preorder α]
[f.NeBot]
(h : Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f)
:
Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f
theorem
Filter.IsBounded.isCobounded_le
{α : Type u_1}
{f : Filter α}
[Preorder α]
[f.NeBot]
(h : Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f)
:
Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f
theorem
Filter.IsBoundedUnder.isCoboundedUnder_flip
{α : Type u_1}
{γ : Type u_3}
{r : α → α → Prop}
{u : γ → α}
{l : Filter γ}
[IsTrans α r]
[l.NeBot]
(h : Filter.IsBoundedUnder r l u)
:
Filter.IsCoboundedUnder (flip r) l u
theorem
Filter.IsBoundedUnder.isCoboundedUnder_le
{α : Type u_1}
{γ : Type u_3}
{u : γ → α}
{l : Filter γ}
[Preorder α]
[l.NeBot]
(h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u)
:
Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u
theorem
Filter.IsBoundedUnder.isCoboundedUnder_ge
{α : Type u_1}
{γ : Type u_3}
{u : γ → α}
{l : Filter γ}
[Preorder α]
[l.NeBot]
(h : Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u)
:
Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u
theorem
Filter.isCoboundedUnder_le_of_eventually_le
{α : Type u_1}
{ι : Type u_4}
[Preorder α]
(l : Filter ι)
[l.NeBot]
{f : ι → α}
{x : α}
(hf : ∀ᶠ (i : ι) in l, x ≤ f i)
:
Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l f
theorem
Filter.isCoboundedUnder_ge_of_eventually_le
{α : Type u_1}
{ι : Type u_4}
[Preorder α]
(l : Filter ι)
[l.NeBot]
{f : ι → α}
{x : α}
(hf : ∀ᶠ (i : ι) in l, f i ≤ x)
:
Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l f
theorem
Filter.isCoboundedUnder_le_of_le
{α : Type u_1}
{ι : Type u_4}
[Preorder α]
(l : Filter ι)
[l.NeBot]
{f : ι → α}
{x : α}
(hf : ∀ (i : ι), x ≤ f i)
:
Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l f
theorem
Filter.isCoboundedUnder_ge_of_le
{α : Type u_1}
{ι : Type u_4}
[Preorder α]
(l : Filter ι)
[l.NeBot]
{f : ι → α}
{x : α}
(hf : ∀ (i : ι), f i ≤ x)
:
Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l f
theorem
Filter.isCobounded_bot
{α : Type u_1}
{r : α → α → Prop}
:
Filter.IsCobounded r ⊥ ↔ ∃ (b : α), ∀ (x : α), r b x
theorem
Filter.isCobounded_top
{α : Type u_1}
{r : α → α → Prop}
:
Filter.IsCobounded r ⊤ ↔ Nonempty α
theorem
Filter.isCobounded_principal
{α : Type u_1}
{r : α → α → Prop}
(s : Set α)
:
Filter.IsCobounded r (Filter.principal s) ↔ ∃ (b : α), ∀ (a : α), (∀ x ∈ s, r x a) → r b a
theorem
Filter.IsCobounded.mono
{α : Type u_1}
{r : α → α → Prop}
{f : Filter α}
{g : Filter α}
(h : f ≤ g)
:
Filter.IsCobounded r f → Filter.IsCobounded r g
theorem
Filter.isBoundedUnder_sum
{α : Type u_6}
{f : Filter α}
{R : Type u_7}
{κ : Type u_8}
[AddCommMonoid R]
{r : R → R → Prop}
(hr : ∀ (v₁ v₂ : α → R), Filter.IsBoundedUnder r f v₁ → Filter.IsBoundedUnder r f v₂ → Filter.IsBoundedUnder r f (v₁ + v₂))
(hr₀ : r 0 0)
{u : κ → α → R}
(s : Finset κ)
(h : ∀ k ∈ s, Filter.IsBoundedUnder r f (u k))
:
Filter.IsBoundedUnder r f (∑ k ∈ s, u k)
theorem
Filter.isBoundedUnder_ge_add
{α : Type u_6}
{f : Filter α}
{R : Type u_7}
[Preorder R]
[Add R]
[AddLeftMono R]
[AddRightMono R]
{u : α → R}
{v : α → R}
(u_bdd_ge : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f u)
(v_bdd_ge : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f v)
:
Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (u + v)
theorem
Filter.isBoundedUnder_le_add
{α : Type u_6}
{f : Filter α}
{R : Type u_7}
[Preorder R]
[Add R]
[AddLeftMono R]
[AddRightMono R]
{u : α → R}
{v : α → R}
(u_bdd_le : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f u)
(v_bdd_le : Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f v)
:
Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (u + v)
theorem
Filter.isBoundedUnder_le_sum
{α : Type u_6}
{f : Filter α}
{R : Type u_7}
[Preorder R]
{κ : Type u_8}
[AddCommMonoid R]
[AddLeftMono R]
[AddRightMono R]
{u : κ → α → R}
(s : Finset κ)
:
(∀ k ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (u k)) →
Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≤ x2) f (∑ k ∈ s, u k)
theorem
Filter.isBoundedUnder_ge_sum
{α : Type u_6}
{f : Filter α}
{R : Type u_7}
[Preorder R]
{κ : Type u_8}
[AddCommMonoid R]
[AddLeftMono R]
[AddRightMono R]
{u : κ → α → R}
(s : Finset κ)
:
(∀ k ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (u k)) →
Filter.IsBoundedUnder (fun (x1 x2 : R) => x1 ≥ x2) f (∑ k ∈ s, u k)
theorem
Filter.isBounded_le_atBot
{α : Type u_1}
[Preorder α]
[Nonempty α]
:
Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) Filter.atBot
theorem
Filter.isBounded_ge_atTop
{α : Type u_1}
[Preorder α]
[Nonempty α]
:
Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) Filter.atTop
theorem
Filter.Tendsto.isBoundedUnder_le_atBot
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Nonempty α]
{f : Filter β}
{u : β → α}
(h : Filter.Tendsto u f Filter.atBot)
:
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u
theorem
Filter.Tendsto.isBoundedUnder_ge_atTop
{α : Type u_1}
{β : Type u_2}
[Preorder α]
[Nonempty α]
{f : Filter β}
{u : β → α}
(h : Filter.Tendsto u f Filter.atTop)
:
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
theorem
Filter.bddAbove_range_of_tendsto_atTop_atBot
{α : Type u_1}
[Preorder α]
[Nonempty α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{u : ℕ → α}
(hx : Filter.Tendsto u Filter.atTop Filter.atBot)
:
theorem
Filter.bddBelow_range_of_tendsto_atTop_atTop
{α : Type u_1}
[Preorder α]
[Nonempty α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{u : ℕ → α}
(hx : Filter.Tendsto u Filter.atTop Filter.atTop)
:
theorem
Filter.isCobounded_le_of_bot
{α : Type u_1}
[Preorder α]
[OrderBot α]
{f : Filter α}
:
Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f
theorem
Filter.isCobounded_ge_of_top
{α : Type u_1}
[Preorder α]
[OrderTop α]
{f : Filter α}
:
Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f
theorem
Filter.isBounded_le_of_top
{α : Type u_1}
[Preorder α]
[OrderTop α]
{f : Filter α}
:
Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f
theorem
Filter.isBounded_ge_of_bot
{α : Type u_1}
[Preorder α]
[OrderBot α]
{f : Filter α}
:
Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f
@[simp]
theorem
OrderIso.isBoundedUnder_le_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
(e : α ≃o β)
{l : Filter γ}
{u : γ → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l fun (x : γ) => e (u x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u
@[simp]
theorem
OrderIso.isBoundedUnder_ge_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Preorder α]
[Preorder β]
(e : α ≃o β)
{l : Filter γ}
{u : γ → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l fun (x : γ) => e (u x)) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u
@[simp]
theorem
Filter.isBoundedUnder_le_neg
{α : Type u_1}
{β : Type u_2}
[OrderedAddCommGroup α]
{l : Filter β}
{u : β → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l fun (x : β) => -u x) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u
@[simp]
theorem
Filter.isBoundedUnder_le_inv
{α : Type u_1}
{β : Type u_2}
[OrderedCommGroup α]
{l : Filter β}
{u : β → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l fun (x : β) => (u x)⁻¹) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l u
@[simp]
theorem
Filter.isBoundedUnder_ge_neg
{α : Type u_1}
{β : Type u_2}
[OrderedAddCommGroup α]
{l : Filter β}
{u : β → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l fun (x : β) => -u x) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u
@[simp]
theorem
Filter.isBoundedUnder_ge_inv
{α : Type u_1}
{β : Type u_2}
[OrderedCommGroup α]
{l : Filter β}
{u : β → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) l fun (x : β) => (u x)⁻¹) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) l u
theorem
Filter.IsBoundedUnder.sup
{α : Type u_1}
{β : Type u_2}
[SemilatticeSup α]
{f : Filter β}
{u : β → α}
{v : β → α}
:
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u →
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v →
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => u a ⊔ v a
@[simp]
theorem
Filter.isBoundedUnder_le_sup
{α : Type u_1}
{β : Type u_2}
[SemilatticeSup α]
{f : Filter β}
{u : β → α}
{v : β → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => u a ⊔ v a) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u ∧ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f v
theorem
Filter.IsBoundedUnder.inf
{α : Type u_1}
{β : Type u_2}
[SemilatticeInf α]
{f : Filter β}
{u : β → α}
{v : β → α}
:
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u →
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v →
Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f fun (a : β) => u a ⊓ v a
@[simp]
theorem
Filter.isBoundedUnder_ge_inf
{α : Type u_1}
{β : Type u_2}
[SemilatticeInf α]
{f : Filter β}
{u : β → α}
{v : β → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f fun (a : β) => u a ⊓ v a) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u ∧ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f v
theorem
Filter.isBoundedUnder_le_abs
{α : Type u_1}
{β : Type u_2}
[LinearOrderedAddCommGroup α]
{f : Filter β}
{u : β → α}
:
(Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f fun (a : β) => |u a|) ↔ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u ∧ Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u
Filters are automatically bounded or cobounded in complete lattices. To use the same statements
in complete and conditionally complete lattices but let automation fill automatically the
boundedness proofs in complete lattices, we use the tactic isBoundedDefault in the statements,
in the form (hf : f.IsBounded (≥) := by isBoundedDefault).
Equations
- Filter.tacticIsBoundedDefault = Lean.ParserDescr.node `Filter.tacticIsBoundedDefault 1024 (Lean.ParserDescr.nonReservedSymbol "isBoundedDefault" false)
Instances For
The limsSup of a filter f is the infimum of the a such that, eventually for f,
holds x ≤ a.
Instances For
The limsInf of a filter f is the supremum of the a such that, eventually for f,
holds x ≥ a.
Instances For
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
Instances For
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
Instances For
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}
Instances For
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}
Instances For
theorem
Filter.limsup_eq
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : Filter β}
{u : β → α}
:
Filter.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 : β → α}
:
Filter.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}
:
Filter.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}
:
Filter.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 γ)
:
Filter.liminf (u ∘ v) f = Filter.liminf u (Filter.map v f)
theorem
Filter.limsup_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[ConditionallyCompleteLattice α]
(u : β → α)
(v : γ → β)
(f : Filter γ)
:
Filter.limsup (u ∘ v) f = Filter.limsup u (Filter.map v f)
@[simp]
theorem
Filter.blimsup_true
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
(f : Filter β)
(u : β → α)
:
(Filter.blimsup u f fun (x : β) => True) = Filter.limsup u f
@[simp]
theorem
Filter.bliminf_true
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
(f : Filter β)
(u : β → α)
:
(Filter.bliminf u f fun (x : β) => True) = Filter.liminf u f
theorem
Filter.blimsup_eq_limsup
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : Filter β}
{u : β → α}
{p : β → Prop}
:
Filter.blimsup u f p = Filter.limsup u (f ⊓ Filter.principal {x : β | p x})
theorem
Filter.bliminf_eq_liminf
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : Filter β}
{u : β → α}
{p : β → Prop}
:
Filter.bliminf u f p = Filter.liminf u (f ⊓ Filter.principal {x : β | p x})
theorem
Filter.blimsup_eq_limsup_subtype
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : Filter β}
{u : β → α}
{p : β → Prop}
:
Filter.blimsup u f p = Filter.limsup (u ∘ Subtype.val) (Filter.comap Subtype.val f)
theorem
Filter.bliminf_eq_liminf_subtype
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : Filter β}
{u : β → α}
{p : β → Prop}
:
Filter.bliminf u f p = Filter.liminf (u ∘ Subtype.val) (Filter.comap Subtype.val f)
theorem
Filter.limsSup_le_of_le
{α : Type u_1}
[ConditionallyCompleteLattice α]
{f : Filter α}
{a : α}
(hf : autoParam (Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f) _auto✝)
(h : ∀ᶠ (n : α) in f, n ≤ a)
:
f.limsSup ≤ a
theorem
Filter.le_limsInf_of_le
{α : Type u_1}
[ConditionallyCompleteLattice α]
{f : Filter α}
{a : α}
(hf : autoParam (Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f) _auto✝)
(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 : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) _auto✝)
(h : ∀ᶠ (n : β) in f, u n ≤ a)
:
Filter.limsup u f ≤ a
theorem
Filter.le_liminf_of_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : Filter β}
{u : β → α}
{a : α}
(hf : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u) _auto✝)
(h : ∀ᶠ (n : β) in f, a ≤ u n)
:
a ≤ Filter.liminf u f
theorem
Filter.le_limsSup_of_le
{α : Type u_1}
[ConditionallyCompleteLattice α]
{f : Filter α}
{a : α}
(hf : autoParam (Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f) _auto✝)
(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 : autoParam (Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f) _auto✝)
(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 : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) _auto✝)
(h : ∀ (b : α), (∀ᶠ (n : β) in f, u n ≤ b) → a ≤ b)
:
a ≤ Filter.limsup u f
theorem
Filter.liminf_le_of_le
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : Filter β}
{u : β → α}
{a : α}
(hf : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u) _auto✝)
(h : ∀ (b : α), (∀ᶠ (n : β) in f, b ≤ u n) → b ≤ a)
:
Filter.liminf u f ≤ a
theorem
Filter.limsInf_le_limsSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
{f : Filter α}
[f.NeBot]
(h₁ : autoParam (Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) f) _auto✝)
(h₂ : autoParam (Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f) _auto✝)
:
f.limsInf ≤ f.limsSup
theorem
Filter.liminf_le_limsup
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLattice α]
{f : Filter β}
[f.NeBot]
{u : β → α}
(h : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≤ x2) f u) _auto✝)
(h' : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : α) => x1 ≥ x2) f u) _auto✝)
:
Filter.liminf u f ≤ Filter.limsup u f
theorem
Filter.limsSup_le_limsSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
{f : Filter α}
{g : Filter α}
(hf : autoParam (Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f) _auto✝)
(hg : autoParam (Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) g) _auto✝)
(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 : Filter α}
{g : Filter α}
(hf : autoParam (Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f) _auto✝)
(hg : autoParam (Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) g) _auto✝)
(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 : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(hv : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v) _auto✝)
:
Filter.limsup u f ≤ Filter.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 : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(hv : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f v) _auto✝)
:
Filter.liminf u f ≤ Filter.liminf v f
theorem
Filter.limsSup_le_limsSup_of_le
{α : Type u_1}
[ConditionallyCompleteLattice α]
{f : Filter α}
{g : Filter α}
(h : f ≤ g)
(hf : autoParam (Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f) _auto✝)
(hg : autoParam (Filter.IsBounded (fun (x1 x2 : α) => x1 ≤ x2) g) _auto✝)
:
f.limsSup ≤ g.limsSup
theorem
Filter.limsInf_le_limsInf_of_le
{α : Type u_1}
[ConditionallyCompleteLattice α]
{f : Filter α}
{g : Filter α}
(h : g ≤ f)
(hf : autoParam (Filter.IsBounded (fun (x1 x2 : α) => x1 ≥ x2) f) _auto✝)
(hg : autoParam (Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) g) _auto✝)
:
f.limsInf ≤ g.limsInf
theorem
Filter.limsup_le_limsup_of_le
{α : Type u_6}
{β : Type u_7}
[ConditionallyCompleteLattice β]
{f : Filter α}
{g : Filter α}
(h : f ≤ g)
{u : α → β}
(hf : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(hg : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) g u) _auto✝)
:
Filter.limsup u f ≤ Filter.limsup u g
theorem
Filter.liminf_le_liminf_of_le
{α : Type u_6}
{β : Type u_7}
[ConditionallyCompleteLattice β]
{f : Filter α}
{g : Filter α}
(h : g ≤ f)
{u : α → β}
(hf : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(hg : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) g u) _auto✝)
:
Filter.liminf u f ≤ Filter.liminf u g
theorem
Filter.limsSup_principal_eq_csSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
{s : Set α}
(h : BddAbove s)
(hs : s.Nonempty)
:
(Filter.principal s).limsSup = sSup s
theorem
Filter.limsInf_principal_eq_csSup
{α : Type u_1}
[ConditionallyCompleteLattice α]
{s : Set α}
(h : BddBelow s)
(hs : s.Nonempty)
:
(Filter.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))
:
Filter.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))
:
Filter.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)
:
Filter.limsup u f = Filter.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)
:
Filter.blimsup u f p = Filter.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)
:
Filter.bliminf u f p = Filter.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)
:
Filter.liminf u f = Filter.liminf v f
@[simp]
theorem
Filter.limsup_const
{β : Type u_2}
{α : Type u_6}
[ConditionallyCompleteLattice β]
{f : Filter α}
[f.NeBot]
(b : β)
:
Filter.limsup (fun (x : α) => b) f = b
@[simp]
theorem
Filter.liminf_const
{β : Type u_2}
{α : Type u_6}
[ConditionallyCompleteLattice β]
{f : Filter α}
[f.NeBot]
(b : β)
:
Filter.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)
:
Filter.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 = ∅)
:
Filter.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)
:
Filter.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 = ∅)
:
Filter.limsup f v = sInf Set.univ
@[simp]
theorem
Filter.liminf_nat_add
{α : Type u_1}
[ConditionallyCompleteLattice α]
(f : ℕ → α)
(k : ℕ)
:
Filter.liminf (fun (i : ℕ) => f (i + k)) Filter.atTop = Filter.liminf f Filter.atTop
@[simp]
theorem
Filter.limsup_nat_add
{α : Type u_1}
[ConditionallyCompleteLattice α]
(f : ℕ → α)
(k : ℕ)
:
Filter.limsup (fun (i : ℕ) => f (i + k)) Filter.atTop = Filter.limsup f Filter.atTop
@[simp]
theorem
Filter.limsup_bot
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
(f : β → α)
:
Filter.limsup f ⊥ = ⊥
@[simp]
theorem
Filter.liminf_bot
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
(f : β → α)
:
Filter.liminf f ⊥ = ⊤
@[simp]
theorem
Filter.blimsup_false
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{u : β → α}
:
(Filter.blimsup u f fun (x : β) => False) = ⊥
@[simp]
theorem
Filter.bliminf_false
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{u : β → α}
:
(Filter.bliminf u f fun (x : β) => False) = ⊤
@[simp]
theorem
Filter.limsup_const_bot
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
:
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 β}
:
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)
:
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)
:
theorem
Filter.limsup_le_iSup
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{u : β → α}
:
Filter.limsup u f ≤ ⨆ (n : β), u n
theorem
Filter.iInf_le_liminf
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{u : β → α}
:
⨅ (n : β), u n ≤ Filter.liminf u f
theorem
Filter.limsup_eq_iInf_iSup
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{u : β → α}
:
Filter.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 : ℕ → α}
:
Filter.limsup u Filter.atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i
theorem
Filter.limsup_eq_iInf_iSup_of_nat'
{α : Type u_1}
[CompleteLattice α]
{u : ℕ → α}
:
Filter.limsup u Filter.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)
:
Filter.limsup u f = ⨅ (i : ι), ⨅ (_ : p i), ⨆ a ∈ s i, u a
theorem
Filter.limsSup_principal_eq_sSup
{α : Type u_1}
[CompleteLattice α]
(s : Set α)
:
(Filter.principal s).limsSup = sSup s
theorem
Filter.limsInf_principal_eq_sInf
{α : Type u_1}
[CompleteLattice α]
(s : Set α)
:
(Filter.principal s).limsInf = sInf s
@[simp]
theorem
Filter.limsup_top_eq_iSup
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
(u : β → α)
:
Filter.limsup u ⊤ = ⨆ (i : β), u i
@[simp]
theorem
Filter.liminf_top_eq_iInf
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
(u : β → α)
:
Filter.liminf u ⊤ = ⨅ (i : β), u i
@[deprecated Filter.limsSup_principal_eq_sSup]
theorem
Filter.limsSup_principal
{α : Type u_1}
[CompleteLattice α]
(s : Set α)
:
(Filter.principal s).limsSup = sSup s
Alias of Filter.limsSup_principal_eq_sSup.
@[deprecated Filter.limsInf_principal_eq_sInf]
theorem
Filter.limsInf_principal
{α : Type u_1}
[CompleteLattice α]
(s : Set α)
:
(Filter.principal s).limsInf = sInf s
Alias of Filter.limsInf_principal_eq_sInf.
@[deprecated Filter.limsup_top_eq_iSup]
theorem
Filter.limsup_top
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
(u : β → α)
:
Filter.limsup u ⊤ = ⨆ (i : β), u i
Alias of Filter.limsup_top_eq_iSup.
@[deprecated Filter.liminf_top_eq_iInf]
theorem
Filter.liminf_top
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
(u : β → α)
:
Filter.liminf u ⊤ = ⨅ (i : β), u i
Alias of Filter.liminf_top_eq_iInf.
theorem
Filter.blimsup_congr'
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
(h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x))
:
Filter.blimsup u f p = Filter.blimsup u f q
theorem
Filter.bliminf_congr'
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
(h : ∀ᶠ (x : β) in f, u x ≠ ⊤ → (p x ↔ q x))
:
Filter.bliminf u f p = Filter.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}
:
Filter.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 : β → α}
:
Filter.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 : ℕ → α}
:
theorem
Filter.liminf_eq_iSup_iInf
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{u : β → α}
:
Filter.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 : ℕ → α}
:
Filter.liminf u Filter.atTop = ⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), u i
theorem
Filter.liminf_eq_iSup_iInf_of_nat'
{α : Type u_1}
[CompleteLattice α]
{u : ℕ → α}
:
Filter.liminf u Filter.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)
:
Filter.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 : β → α}
:
Filter.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 : ℕ → α}
:
theorem
Filter.limsup_eq_sInf_sSup
{ι : Type u_6}
{R : Type u_7}
(F : Filter ι)
[CompleteLattice R]
(a : ι → R)
:
theorem
Filter.liminf_eq_sSup_sInf
{ι : Type u_6}
{R : Type u_7}
(F : Filter ι)
[CompleteLattice R]
(a : ι → R)
:
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)
:
Filter.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 ≤ Filter.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.
@[deprecated CompleteLatticeHom.apply_limsup_iterate]
theorem
Filter.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
Alias of CompleteLatticeHom.apply_limsup_iterate.
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.
@[deprecated CompleteLatticeHom.apply_liminf_iterate]
theorem
Filter.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
Alias of CompleteLatticeHom.apply_liminf_iterate.
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 : β → Prop}
{q : β → Prop}
{u : β → α}
(h : ∀ (x : β), p x → q x)
:
Filter.blimsup u f p ≤ Filter.blimsup u f q
theorem
Filter.bliminf_antitone
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
(h : ∀ (x : β), p x → q x)
:
Filter.bliminf u f q ≤ Filter.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)
:
Filter.blimsup u f p ≤ Filter.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)
:
Filter.blimsup u f p ≤ Filter.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)
:
Filter.bliminf u f p ≤ Filter.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)
:
Filter.bliminf u f p ≤ Filter.bliminf v f p
theorem
Filter.bliminf_antitone_filter
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{g : Filter β}
{p : β → Prop}
{u : β → α}
(h : f ≤ g)
:
Filter.bliminf u g p ≤ Filter.bliminf u f p
theorem
Filter.blimsup_monotone_filter
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{g : Filter β}
{p : β → Prop}
{u : β → α}
(h : f ≤ g)
:
Filter.blimsup u f p ≤ Filter.blimsup u g p
theorem
Filter.blimsup_and_le_inf
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
:
(Filter.blimsup u f fun (x : β) => p x ∧ q x) ≤ Filter.blimsup u f p ⊓ Filter.blimsup u f q
@[simp]
theorem
Filter.bliminf_sup_le_inf_aux_left
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
:
(Filter.blimsup u f fun (x : β) => p x ∧ q x) ≤ Filter.blimsup u f p
@[simp]
theorem
Filter.bliminf_sup_le_inf_aux_right
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
:
(Filter.blimsup u f fun (x : β) => p x ∧ q x) ≤ Filter.blimsup u f q
theorem
Filter.bliminf_sup_le_and
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
:
Filter.bliminf u f p ⊔ Filter.bliminf u f q ≤ Filter.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 : β → Prop}
{q : β → Prop}
{u : β → α}
:
Filter.bliminf u f p ≤ Filter.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 : β → Prop}
{q : β → Prop}
{u : β → α}
:
Filter.bliminf u f q ≤ Filter.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 : β → Prop}
{q : β → Prop}
{u : β → α}
:
Filter.blimsup u f p ⊔ Filter.blimsup u f q ≤ Filter.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 : β → Prop}
{q : β → Prop}
{u : β → α}
:
Filter.blimsup u f p ≤ Filter.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 : β → Prop}
{q : β → Prop}
{u : β → α}
:
Filter.blimsup u f q ≤ Filter.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 : β → Prop}
{q : β → Prop}
{u : β → α}
:
(Filter.bliminf u f fun (x : β) => p x ∨ q x) ≤ Filter.bliminf u f p ⊓ Filter.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 : β → Prop}
{q : β → Prop}
{u : β → α}
:
(Filter.bliminf u f fun (x : β) => p x ∨ q x) ≤ Filter.bliminf u f p
@[simp]
theorem
Filter.bliminf_or_le_inf_aux_right
{α : Type u_1}
{β : Type u_2}
[CompleteLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
:
(Filter.bliminf u f fun (x : β) => p x ∨ q x) ≤ Filter.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
@[deprecated OrderIso.apply_blimsup]
theorem
Filter.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
Alias of OrderIso.apply_blimsup.
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
@[deprecated OrderIso.apply_bliminf]
theorem
Filter.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
Alias of OrderIso.apply_bliminf.
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
@[deprecated sSupHom.apply_blimsup_le]
theorem
Filter.SupHom.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
Alias of sSupHom.apply_blimsup_le.
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)
@[deprecated sInfHom.le_apply_bliminf]
theorem
Filter.InfHom.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)
Alias of sInfHom.le_apply_bliminf.
theorem
Filter.limsup_sup_filter
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{u : β → α}
{g : Filter β}
:
Filter.limsup u (f ⊔ g) = Filter.limsup u f ⊔ Filter.limsup u g
theorem
Filter.liminf_sup_filter
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{u : β → α}
{g : Filter β}
:
Filter.liminf u (f ⊔ g) = Filter.liminf u f ⊓ Filter.liminf u g
@[simp]
theorem
Filter.blimsup_or_eq_sup
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
:
(Filter.blimsup u f fun (x : β) => p x ∨ q x) = Filter.blimsup u f p ⊔ Filter.blimsup u f q
@[simp]
theorem
Filter.bliminf_or_eq_inf
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{p : β → Prop}
{q : β → Prop}
{u : β → α}
:
(Filter.bliminf u f fun (x : β) => p x ∨ q x) = Filter.bliminf u f p ⊓ Filter.bliminf u f q
@[simp]
theorem
Filter.blimsup_sup_not
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{p : β → Prop}
{u : β → α}
:
(Filter.blimsup u f p ⊔ Filter.blimsup u f fun (x : β) => ¬p x) = Filter.limsup u f
@[simp]
theorem
Filter.bliminf_inf_not
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{p : β → Prop}
{u : β → α}
:
(Filter.bliminf u f p ⊓ Filter.bliminf u f fun (x : β) => ¬p x) = Filter.liminf u f
@[simp]
theorem
Filter.blimsup_not_sup
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{p : β → Prop}
{u : β → α}
:
(Filter.blimsup u f fun (x : β) => ¬p x) ⊔ Filter.blimsup u f p = Filter.limsup u f
@[simp]
theorem
Filter.bliminf_not_inf
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{p : β → Prop}
{u : β → α}
:
(Filter.bliminf u f fun (x : β) => ¬p x) ⊓ Filter.bliminf u f p = Filter.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 : β → α}
:
Filter.limsup (s.piecewise u v) f = (Filter.blimsup u f fun (x : β) => x ∈ s) ⊔ Filter.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 : β → α}
:
Filter.liminf (s.piecewise u v) f = (Filter.bliminf u f fun (x : β) => x ∈ s) ⊓ Filter.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 ⊔ Filter.limsup u f = Filter.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 ⊓ Filter.liminf u f = Filter.liminf (fun (x : β) => a ⊓ u x) f
theorem
Filter.sup_liminf
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{u : β → α}
(a : α)
:
a ⊔ Filter.liminf u f = Filter.liminf (fun (x : β) => a ⊔ u x) f
theorem
Filter.inf_limsup
{α : Type u_1}
{β : Type u_2}
[CompleteDistribLattice α]
{f : Filter β}
{u : β → α}
(a : α)
:
a ⊓ Filter.limsup u f = Filter.limsup (fun (x : β) => a ⊓ u x) f
theorem
Filter.limsup_compl
{α : Type u_1}
{β : Type u_2}
[CompleteBooleanAlgebra α]
(f : Filter β)
(u : β → α)
:
(Filter.limsup u f)ᶜ = Filter.liminf (compl ∘ u) f
theorem
Filter.liminf_compl
{α : Type u_1}
{β : Type u_2}
[CompleteBooleanAlgebra α]
(f : Filter β)
(u : β → α)
:
(Filter.liminf u f)ᶜ = Filter.limsup (compl ∘ u) f
theorem
Filter.limsup_sdiff
{α : Type u_1}
{β : Type u_2}
[CompleteBooleanAlgebra α]
(f : Filter β)
(u : β → α)
(a : α)
:
Filter.limsup u f \ a = Filter.limsup (fun (b : β) => u b \ a) f
theorem
Filter.liminf_sdiff
{α : Type u_1}
{β : Type u_2}
[CompleteBooleanAlgebra α]
(f : Filter β)
(u : β → α)
[f.NeBot]
(a : α)
:
Filter.liminf u f \ a = Filter.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 \ Filter.limsup u f = Filter.liminf (fun (b : β) => a \ u b) f
theorem
Filter.sdiff_liminf
{α : Type u_1}
{β : Type u_2}
[CompleteBooleanAlgebra α]
(f : Filter β)
(u : β → α)
(a : α)
:
a \ Filter.liminf u f = Filter.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 ∈ Filter.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 ∈ Filter.limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i
theorem
Filter.cofinite.blimsup_set_eq
{α : Type u_1}
{ι : Type u_4}
{p : ι → Prop}
{s : ι → Set α}
:
Filter.blimsup s Filter.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 α}
:
Filter.bliminf s Filter.cofinite p = {x : α | {n : ι | p n ∧ x ∉ s n}.Finite}
theorem
Filter.cofinite.limsup_set_eq
{α : Type u_1}
{ι : Type u_4}
{s : ι → Set α}
:
Filter.limsup s Filter.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 α}
:
Filter.liminf s Filter.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.frequently_lt_of_lt_limsSup
{α : Type u_1}
{f : Filter α}
[ConditionallyCompleteLinearOrder α]
{a : α}
(hf : autoParam (Filter.IsCobounded (fun (x1 x2 : α) => x1 ≤ x2) f) _auto✝)
(h : a < f.limsSup)
:
∃ᶠ (n : α) in f, a < n
theorem
Filter.frequently_lt_of_limsInf_lt
{α : Type u_1}
{f : Filter α}
[ConditionallyCompleteLinearOrder α]
{a : α}
(hf : autoParam (Filter.IsCobounded (fun (x1 x2 : α) => x1 ≥ x2) f) _auto✝)
(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 < Filter.liminf u f)
(hu : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
:
∀ᶠ (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 : Filter.limsup u f < b)
(hu : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
:
∀ᶠ (a : α) in f, u a < b
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 : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
:
b ≤ Filter.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 : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
:
Filter.liminf u f ≤ b
theorem
Filter.frequently_lt_of_lt_limsup
{α : Type u_6}
{β : Type u_7}
[ConditionallyCompleteLinearOrder β]
{f : Filter α}
{u : α → β}
{b : β}
(hu : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(h : b < Filter.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 : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(h : Filter.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₁ : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(h₂ : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
:
Filter.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₁ : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(h₂ : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
:
x ≤ Filter.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₁ : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(h₂ : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
:
x ≤ Filter.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₁ : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(h₂ : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
:
Filter.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 : Filter.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 : α}
:
Filter.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
Instances For
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))
:
Filter.liminf f v = ⨆ (j : Subtype p), ⨅ (i : ↑(s ↑(Filter.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 : ι → α)
:
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
Instances For
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))
:
Filter.limsup f v = ⨅ (j : Subtype p), ⨆ (i : ↑(s ↑(Filter.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 : ι → α)
:
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
Monotone.isBoundedUnder_le_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Nonempty β]
[LinearOrder β]
[Preorder γ]
[NoMaxOrder γ]
{g : β → γ}
{f : α → β}
{l : Filter α}
(hg : Monotone g)
(hg' : Filter.Tendsto g Filter.atTop Filter.atTop)
:
Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f
theorem
Monotone.isBoundedUnder_ge_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Nonempty β]
[LinearOrder β]
[Preorder γ]
[NoMinOrder γ]
{g : β → γ}
{f : α → β}
{l : Filter α}
(hg : Monotone g)
(hg' : Filter.Tendsto g Filter.atBot Filter.atBot)
:
Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f
theorem
Antitone.isBoundedUnder_le_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Nonempty β]
[LinearOrder β]
[Preorder γ]
[NoMaxOrder γ]
{g : β → γ}
{f : α → β}
{l : Filter α}
(hg : Antitone g)
(hg' : Filter.Tendsto g Filter.atBot Filter.atTop)
:
Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) l f
theorem
Antitone.isBoundedUnder_ge_comp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Nonempty β]
[LinearOrder β]
[Preorder γ]
[NoMinOrder γ]
{g : β → γ}
{f : α → β}
{l : Filter α}
(hg : Antitone g)
(hg' : Filter.Tendsto g Filter.atTop Filter.atBot)
:
Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) l (g ∘ f) ↔ Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) l f
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 : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => l (v x)) _auto✝)
(hv_co : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v) _auto✝)
:
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 : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(hu_co : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(hgu : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => g (u x)) _auto✝)
(hgu_co : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : γ) => x1 ≤ x2) f fun (x : α) => g (u x)) _auto✝)
:
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 : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(hu_co : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(hgu : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) f fun (x : α) => g (u x)) _auto✝)
(hgu_co : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : γ) => x1 ≥ x2) f fun (x : α) => g (u x)) _auto✝)
:
g (Filter.liminf u f) = Filter.liminf (fun (x : α) => g (u x)) f
theorem
isCoboundedUnder_le_max
{α : Type u_1}
{β : Type u_2}
[LinearOrder β]
{f : Filter α}
{u : α → β}
{v : α → β}
(h : Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u ∨ Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v)
:
Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => max (u a) (v a)
theorem
limsup_max
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder β]
{f : Filter α}
{u : α → β}
{v : α → β}
(h₁ : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(h₂ : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v) _auto✝)
(h₃ : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f u) _auto✝)
(h₄ : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f v) _auto✝)
:
Filter.limsup (fun (a : α) => max (u a) (v a)) f = max (Filter.limsup u f) (Filter.limsup v f)
theorem
liminf_min
{α : Type u_1}
{β : Type u_2}
[ConditionallyCompleteLinearOrder β]
{f : Filter α}
{u : α → β}
{v : α → β}
(h₁ : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(h₂ : autoParam (Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f v) _auto✝)
(h₃ : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f u) _auto✝)
(h₄ : autoParam (Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f v) _auto✝)
:
Filter.liminf (fun (a : α) => min (u a) (v a)) f = min (Filter.liminf u f) (Filter.liminf v f)
theorem
isBoundedUnder_le_finset_sup'
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[LinearOrder β]
[Nonempty β]
{f : Filter α}
{F : ι → α → β}
{s : Finset ι}
(hs : s.Nonempty)
(h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i))
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => s.sup' hs fun (i : ι) => F i a
theorem
isCoboundedUnder_le_finset_sup'
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[LinearOrder β]
{f : Filter α}
{F : ι → α → β}
{s : Finset ι}
(hs : s.Nonempty)
(h : ∃ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i))
:
Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => s.sup' hs fun (i : ι) => F i a
theorem
isBoundedUnder_le_finset_sup
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[LinearOrder β]
[OrderBot β]
{f : Filter α}
{F : ι → α → β}
{s : Finset ι}
(h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i))
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f fun (a : α) => s.sup fun (i : ι) => F i a
theorem
isBoundedUnder_ge_finset_inf'
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[LinearOrder β]
[Nonempty β]
{f : Filter α}
{F : ι → α → β}
{s : Finset ι}
(hs : s.Nonempty)
(h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i))
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f fun (a : α) => s.inf' hs fun (i : ι) => F i a
theorem
isCoboundedUnder_ge_finset_inf'
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[LinearOrder β]
{f : Filter α}
{F : ι → α → β}
{s : Finset ι}
(hs : s.Nonempty)
(h : ∃ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i))
:
Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f fun (a : α) => s.inf' hs fun (i : ι) => F i a
theorem
isBoundedUnder_ge_finset_inf
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[LinearOrder β]
[OrderTop β]
{f : Filter α}
{F : ι → α → β}
{s : Finset ι}
(h : ∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i))
:
Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f fun (a : α) => s.inf fun (i : ι) => F i a
theorem
limsup_finset_sup'
{α : Type u_1}
{β : Type u_2}
{ι : Type u_4}
[ConditionallyCompleteLinearOrder β]
{f : Filter α}
{F : ι → α → β}
{s : Finset ι}
(hs : s.Nonempty)
(h₁ : autoParam (∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) _auto✝)
(h₂ : autoParam (∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) _auto✝)
:
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₁ : autoParam (∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) _auto✝)
(h₂ : autoParam (∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≤ x2) f (F i)) _auto✝)
:
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₁ : autoParam (∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) _auto✝)
(h₂ : autoParam (∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) _auto✝)
:
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₁ : autoParam (∀ i ∈ s, Filter.IsCoboundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) _auto✝)
(h₂ : autoParam (∀ i ∈ s, Filter.IsBoundedUnder (fun (x1 x2 : β) => x1 ≥ x2) f (F i)) _auto✝)
:
Filter.liminf (fun (a : α) => s.inf fun (i : ι) => F i a) f = s.inf fun (i : ι) => Filter.liminf (F i) f
theorem
Filter.IsCobounded.frequently_ge
{R : Type u_6}
{F : Filter R}
[LinearOrder R]
[F.NeBot]
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F)
:
∃ (l : R), ∃ᶠ (x : R) in F, l ≤ x
For nontrivial filters in linear orders, coboundedness for ≤ implies frequent boundedness
from below.
theorem
Filter.IsCobounded.frequently_le
{R : Type u_6}
{F : Filter R}
[LinearOrder R]
[F.NeBot]
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F)
:
∃ (u : R), ∃ᶠ (x : R) in F, x ≤ u
For nontrivial filters in linear orders, coboundedness for ≥ implies frequent boundedness
from above.
theorem
Filter.IsCobounded.of_frequently_ge
{R : Type u_6}
{F : Filter R}
[LinearOrder R]
{l : R}
(freq_ge : ∃ᶠ (x : R) in F, l ≤ x)
:
Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F
In linear orders, frequent boundedness from below implies coboundedness for ≤.
theorem
Filter.IsCobounded.of_frequently_le
{R : Type u_6}
{F : Filter R}
[LinearOrder R]
{u : R}
(freq_le : ∃ᶠ (r : R) in F, r ≤ u)
:
Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F
In linear orders, frequent boundedness from above implies coboundedness for ≥.
theorem
Monotone.frequently_ge_map_of_frequently_ge
{R : Type u_6}
{S : Type u_7}
{F : Filter R}
[LinearOrder R]
[LinearOrder S]
{f : R → S}
(f_incr : Monotone f)
{l : R}
(freq_ge : ∃ᶠ (x : R) in F, l ≤ x)
:
∃ᶠ (x' : S) in Filter.map f F, f l ≤ x'
theorem
Monotone.frequently_le_map_of_frequently_le
{R : Type u_6}
{S : Type u_7}
{F : Filter R}
[LinearOrder R]
[LinearOrder S]
{f : R → S}
(f_incr : Monotone f)
{u : R}
(freq_le : ∃ᶠ (x : R) in F, x ≤ u)
:
∃ᶠ (y : S) in Filter.map f F, y ≤ f u
theorem
Antitone.frequently_le_map_of_frequently_ge
{R : Type u_6}
{S : Type u_7}
{F : Filter R}
[LinearOrder R]
[LinearOrder S]
{f : R → S}
(f_decr : Antitone f)
{l : R}
(frbdd : ∃ᶠ (x : R) in F, l ≤ x)
:
∃ᶠ (y : S) in Filter.map f F, y ≤ f l
theorem
Antitone.frequently_ge_map_of_frequently_le
{R : Type u_6}
{S : Type u_7}
{F : Filter R}
[LinearOrder R]
[LinearOrder S]
{f : R → S}
(f_decr : Antitone f)
{u : R}
(frbdd : ∃ᶠ (x : R) in F, x ≤ u)
:
∃ᶠ (y : S) in Filter.map f F, f u ≤ y
theorem
Monotone.isCoboundedUnder_le_of_isCobounded
{R : Type u_6}
{S : Type u_7}
{F : Filter R}
[LinearOrder R]
[LinearOrder S]
{f : R → S}
(f_incr : Monotone f)
[F.NeBot]
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F)
:
Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≤ x2) F f
theorem
Monotone.isCoboundedUnder_ge_of_isCobounded
{R : Type u_6}
{S : Type u_7}
{F : Filter R}
[LinearOrder R]
[LinearOrder S]
{f : R → S}
(f_incr : Monotone f)
[F.NeBot]
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F)
:
Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≥ x2) F f
theorem
Antitone.isCoboundedUnder_le_of_isCobounded
{R : Type u_6}
{S : Type u_7}
{F : Filter R}
[LinearOrder R]
[LinearOrder S]
{f : R → S}
(f_decr : Antitone f)
[F.NeBot]
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≥ x2) F)
:
Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≤ x2) F f
theorem
Antitone.isCoboundedUnder_ge_of_isCobounded
{R : Type u_6}
{S : Type u_7}
{F : Filter R}
[LinearOrder R]
[LinearOrder S]
{f : R → S}
(f_decr : Antitone f)
[F.NeBot]
(cobdd : Filter.IsCobounded (fun (x1 x2 : R) => x1 ≤ x2) F)
:
Filter.IsCoboundedUnder (fun (x1 x2 : S) => x1 ≥ x2) F f