Mathlib.Order.Filter.IsBounded

Filter.isBounded_iff theorem

: f.IsBounded r ↔ ∃ s ∈ f.sets, ∃ b, s ⊆ {x | r x b}

Full source

/-- `f` is eventually bounded if and only if, there exists an admissible set on which it is
bounded. -/
theorem isBounded_iff : f.IsBounded r ↔ ∃ s ∈ f.sets, ∃ b, s ⊆ { x | r x b } :=
  Iff.intro (fun ⟨b, hb⟩ => ⟨{ a | r a b }, hb, b, Subset.refl _⟩) fun ⟨_, hs, b, hb⟩ =>
    ⟨b, mem_of_superset hs hb⟩

Characterization of Bounded Filters via Uniform Bounding

Informal description

A filter $f$ on a type $\alpha$ is bounded with respect to a relation $r : \alpha \to \alpha \to \text{Prop}$ if and only if there exists a set $s \in f$ and an element $b \in \alpha$ such that for all $x \in s$, the relation $r(x, b)$ holds. In other words, $f$ is bounded if there is some admissible set in $f$ on which the relation $r$ is uniformly bounded by some element $b$.

Filter.isBoundedUnder_of theorem

{f : Filter β} {u : β → α} : (∃ b, ∀ x, r (u x) b) → f.IsBoundedUnder r u

Full source

/-- A bounded function `u` is in particular eventually bounded. -/
theorem isBoundedUnder_of {f : Filter β} {u : β → α} : (∃ b, ∀ x, r (u x) b) → f.IsBoundedUnder r u
  | ⟨b, hb⟩ => ⟨b, show ∀ᶠ x in f, r (u x) b from Eventually.of_forall hb⟩

Global Boundedness Implies Filter Boundedness Under a Relation

Informal description

Given a relation $r$ on a type $\alpha$, a filter $f$ on a type $\beta$, and a function $u : \beta \to \alpha$, if there exists an element $b \in \alpha$ such that $r(u(x), b)$ holds for all $x \in \beta$, then the filter $f$ is bounded under $r$ with respect to $u$.

Filter.isBounded_bot theorem

: IsBounded r ⊥ ↔ Nonempty α

Full source

theorem isBounded_bot : IsBoundedIsBounded r ⊥ ↔ Nonempty α := by simp [IsBounded, exists_true_iff_nonempty]

Boundedness of Bottom Filter ↔ Nonempty Type

Informal description

The bottom filter $\bot$ on a type $\alpha$ is bounded with respect to a relation $r$ if and only if $\alpha$ is nonempty.

Filter.isBounded_top theorem

: IsBounded r ⊤ ↔ ∃ t, ∀ x, r x t

Full source

theorem isBounded_top : IsBoundedIsBounded r ⊤ ↔ ∃ t, ∀ x, r x t := by simp [IsBounded, eq_univ_iff_forall]

Boundedness of the Top Filter with Respect to a Relation

Informal description

A filter $\top$ (the collection of all subsets of $\alpha$) is bounded with respect to a relation $r$ if and only if there exists an element $t \in \alpha$ such that $r(x, t)$ holds for all $x \in \alpha$.

Filter.isBounded_principal theorem

(s : Set α) : IsBounded r (𝓟 s) ↔ ∃ t, ∀ x ∈ s, r x t

Full source

theorem isBounded_principal (s : Set α) : IsBoundedIsBounded r (𝓟 s) ↔ ∃ t, ∀ x ∈ s, r x t := by
  simp [IsBounded, subset_def]

Boundedness of Principal Filter with Respect to a Relation

Informal description

For any set $s$ in a type $\alpha$ and a relation $r$ on $\alpha$, the principal filter $\mathfrak{P}(s)$ is bounded with respect to $r$ if and only if there exists an element $t \in \alpha$ such that for every $x \in s$, the relation $r(x, t)$ holds.

Filter.isBounded_sup theorem

[IsTrans α r] [IsDirected α r] : IsBounded r f → IsBounded r g → IsBounded r (f ⊔ g)

Full source

theorem isBounded_sup [IsTrans α r] [IsDirected α r] :
    IsBounded r f → IsBounded r g → IsBounded r (f ⊔ g)
  | ⟨b₁, h₁⟩, ⟨b₂, h₂⟩ =>
    let ⟨b, rb₁b, rb₂b⟩ := directed_of r b₁ b₂
    ⟨b, eventually_sup.mpr
      ⟨h₁.mono fun _ h => _root_.trans h rb₁b, h₂.mono fun _ h => _root_.trans h rb₂b⟩⟩

Boundedness of Filter Supremum under Transitive Directed Relations

Informal description

Let $\alpha$ be a type with a transitive and directed relation $r$. For any filters $f$ and $g$ on $\alpha$, if $f$ is bounded with respect to $r$ and $g$ is bounded with respect to $r$, then the supremum filter $f \sqcup g$ is also bounded with respect to $r$.

Filter.IsBounded.mono theorem

(h : f ≤ g) : IsBounded r g → IsBounded r f

Full source

theorem IsBounded.mono (h : f ≤ g) : IsBounded r g → IsBounded r f
  | ⟨b, hb⟩ => ⟨b, h hb⟩

Boundedness is preserved under filter refinement

Informal description

If a filter $g$ is bounded with respect to a relation $r$ and $f$ is a finer filter than $g$ (i.e., $f \leq g$), then $f$ is also bounded with respect to $r$.

Filter.IsBoundedUnder.mono theorem

{f g : Filter β} {u : β → α} (h : f ≤ g) : g.IsBoundedUnder r u → f.IsBoundedUnder r u

Full source

theorem IsBoundedUnder.mono {f g : Filter β} {u : β → α} (h : f ≤ g) :
    g.IsBoundedUnder r u → f.IsBoundedUnder r u := fun hg => IsBounded.mono (map_mono h) hg

Boundedness Under Relation is Preserved by Finer Filters

Informal description

Let $f$ and $g$ be filters on a type $\beta$, and let $u : \beta \to \alpha$ be a function. If $f$ is finer than $g$ (i.e., $f \leq g$) and $g$ is bounded under a relation $r$ with respect to $u$, then $f$ is also bounded under $r$ with respect to $u$.

Filter.IsBoundedUnder.mono_le theorem

 [Preorder β] {l : Filter α} {u v : α → β} (hu : IsBoundedUnder (· ≤ ·) l u) (hv : v ≤ᶠ[l] u) :
  IsBoundedUnder (· ≤ ·) l v

Full source

theorem IsBoundedUnder.mono_le [Preorder β] {l : Filter α} {u v : α → β}
    (hu : IsBoundedUnder (· ≤ ·) l u) (hv : v ≤ᶠ[l] u) : IsBoundedUnder (· ≤ ·) l v := by
  apply hu.imp
  exact fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans

Boundedness under $\leq$ is preserved by eventual domination

Informal description

Let $\beta$ be a preorder, $l$ a filter on a type $\alpha$, and $u, v : \alpha \to \beta$ functions. If $u$ is bounded under the relation $\leq$ with respect to $l$, and $v(x) \leq u(x)$ holds eventually for all $x$ in $l$, then $v$ is also bounded under $\leq$ with respect to $l$.

Filter.IsBoundedUnder.mono_ge theorem

 [Preorder β] {l : Filter α} {u v : α → β} (hu : IsBoundedUnder (· ≥ ·) l u) (hv : u ≤ᶠ[l] v) :
  IsBoundedUnder (· ≥ ·) l v

Full source

theorem IsBoundedUnder.mono_ge [Preorder β] {l : Filter α} {u v : α → β}
    (hu : IsBoundedUnder (· ≥ ·) l u) (hv : u ≤ᶠ[l] v) : IsBoundedUnder (· ≥ ·) l v :=
  IsBoundedUnder.mono_le (β := βᵒᵈ) hu hv

Boundedness under $\geq$ is preserved by eventual domination

Informal description

Let $\beta$ be a preorder, $l$ a filter on a type $\alpha$, and $u, v : \alpha \to \beta$ functions. If $u$ is bounded under the relation $\geq$ with respect to $l$, and $u(x) \leq v(x)$ holds eventually for all $x$ in $l$, then $v$ is also bounded under $\geq$ with respect to $l$.

Filter.isBoundedUnder_const theorem

[IsRefl α r] {l : Filter β} {a : α} : IsBoundedUnder r l fun _ => a

Full source

theorem isBoundedUnder_const [IsRefl α r] {l : Filter β} {a : α} : IsBoundedUnder r l fun _ => a :=
  ⟨a, eventually_map.2 <| Eventually.of_forall fun _ => refl _⟩

Boundedness of Constant Function under Reflexive Relation

Informal description

Let $\alpha$ be a type with a reflexive relation $r$, and let $\beta$ be another type. For any filter $l$ on $\beta$ and any element $a \in \alpha$, the constant function $(\_ : \beta) \mapsto a$ is bounded under $r$ with respect to $l$. In other words, there exists an element $b \in \alpha$ such that for all $y$ in some set belonging to $l$, the relation $r(a, b)$ holds.

Filter.IsBounded.isBoundedUnder theorem

 {q : β → β → Prop} {u : α → β} (hu : ∀ a₀ a₁, r a₀ a₁ → q (u a₀) (u a₁)) : f.IsBounded r → f.IsBoundedUnder q u

Full source

theorem IsBounded.isBoundedUnder {q : β → β → Prop} {u : α → β}
    (hu : ∀ a₀ a₁, r a₀ a₁ → q (u a₀) (u a₁)) : f.IsBounded r → f.IsBoundedUnder q u
  | ⟨b, h⟩ => ⟨u b, show ∀ᶠ x in f, q (u x) (u b) from h.mono fun x => hu x b⟩

Boundedness under a relation via a relation-preserving function

Informal description

Let $r$ be a relation on $\alpha$, $q$ a relation on $\beta$, and $u : \alpha \to \beta$ a function. If $u$ preserves the relations in the sense that for all $a₀, a₁ \in \alpha$, $r(a₀, a₁)$ implies $q(u(a₀), u(a₁))$, then whenever a filter $f$ on $\alpha$ is bounded with respect to $r$, the filter $f$ is bounded under $q$ with respect to $u$.

Filter.IsBoundedUnder.comp theorem

 {l : Filter γ} {q : β → β → Prop} {u : γ → α} {v : α → β} (hv : ∀ a₀ a₁, r a₀ a₁ → q (v a₀) (v a₁)) :
  l.IsBoundedUnder r u → l.IsBoundedUnder q (v ∘ u)

Full source

theorem IsBoundedUnder.comp {l : Filter γ} {q : β → β → Prop} {u : γ → α} {v : α → β}
    (hv : ∀ a₀ a₁, r a₀ a₁ → q (v a₀) (v a₁)) : l.IsBoundedUnder r u → l.IsBoundedUnder q (v ∘ u)
  | ⟨a, h⟩ => ⟨v a, show ∀ᶠ x in map u l, q (v x) (v a) from h.mono fun x => hv x a⟩

Composition Preserves Boundedness Under Relation

Informal description

Let $r$ be a relation on $\alpha$, $q$ a relation on $\beta$, $u : \gamma \to \alpha$ a function, and $v : \alpha \to \beta$ a function. If $v$ preserves the relations (i.e., for all $a₀, a₁ \in \alpha$, $r(a₀, a₁)$ implies $q(v(a₀), v(a₁))$), then whenever the filter $l$ on $\gamma$ is bounded under $r$ with respect to $u$, it is also bounded under $q$ with respect to the composition $v \circ u$.

Filter.isBoundedUnder_map_iff theorem

 {ι κ X : Type*} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter κ} :
  (map φ 𝓕).IsBoundedUnder r f ↔ 𝓕.IsBoundedUnder r (f ∘ φ)

Full source

lemma isBoundedUnder_map_iff {ι κ X : Type*} {r : X → X → Prop} {f : ι → X} {φ : κ → ι}
    {𝓕 : Filter κ} :
    (map φ 𝓕).IsBoundedUnder r f ↔ 𝓕.IsBoundedUnder r (f ∘ φ) :=
  Iff.rfl

Boundedness Under Relation Preserved by Precomposition

Informal description

Let $X$, $\iota$, and $\kappa$ be types, $r$ a relation on $X$, $f : \iota \to X$ a function, $\varphi : \kappa \to \iota$ a function, and $\mathcal{F}$ a filter on $\kappa$. Then the image filter $\text{map } \varphi \mathcal{F}$ is bounded under $r$ with respect to $f$ if and only if $\mathcal{F}$ is bounded under $r$ with respect to the composition $f \circ \varphi$.

Filter.Tendsto.isBoundedUnder_comp theorem

 {ι κ X : Type*} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter ι} {𝓖 : Filter κ} (φ_tendsto : Tendsto φ 𝓖 𝓕)
  (𝓕_bounded : 𝓕.IsBoundedUnder r f) : 𝓖.IsBoundedUnder r (f ∘ φ)

Full source

lemma Tendsto.isBoundedUnder_comp {ι κ X : Type*} {r : X → X → Prop} {f : ι → X} {φ : κ → ι}
    {𝓕 : Filter ι} {𝓖 : Filter κ} (φ_tendsto : Tendsto φ 𝓖 𝓕) (𝓕_bounded : 𝓕.IsBoundedUnder r f) :
    𝓖.IsBoundedUnder r (f ∘ φ) :=
  isBoundedUnder_map_iff.mp (𝓕_bounded.mono φ_tendsto)

Boundedness Under Relation is Preserved by Composition with a Tendsto Function

Informal description

Let $X$, $\iota$, and $\kappa$ be types, $r$ a relation on $X$, $f : \iota \to X$ a function, $\varphi : \kappa \to \iota$ a function, $\mathcal{F}$ a filter on $\iota$, and $\mathcal{G}$ a filter on $\kappa$. If $\varphi$ tends to $\mathcal{F}$ along $\mathcal{G}$ (i.e., $\text{Tendsto}\, \varphi\, \mathcal{G}\, \mathcal{F}$) and $\mathcal{F}$ is bounded under $r$ with respect to $f$, then $\mathcal{G}$ is bounded under $r$ with respect to the composition $f \circ \varphi$.

Filter.IsBoundedUnder.eventually_le theorem

(h : IsBoundedUnder (· ≤ ·) f u) : ∃ a, ∀ᶠ x in f, u x ≤ a

Full source

lemma IsBoundedUnder.eventually_le (h : IsBoundedUnder (· ≤ ·) f u) :
    ∃ a, ∀ᶠ x in f, u x ≤ a := by
  obtain ⟨a, ha⟩ := h
  use a
  exact eventually_map.1 ha

Existence of Upper Bound for Eventually Bounded Function under a Filter

Informal description

Given a filter $f$ on a type $\alpha$ and a function $u : \alpha \to \beta$ where $\beta$ is equipped with a preorder, if the values of $u$ are bounded above under $f$ (i.e., $\text{IsBoundedUnder}\, (\leq)\, f\, u$), then there exists an element $a \in \beta$ such that $u(x) \leq a$ holds for all $x$ in some set belonging to $f$. In other words, if the function $u$ is eventually bounded above with respect to the filter $f$, then there exists a bound $a$ such that $u(x) \leq a$ holds "eventually" under $f$.

Filter.IsBoundedUnder.eventually_ge theorem

(h : IsBoundedUnder (· ≥ ·) f u) : ∃ a, ∀ᶠ x in f, a ≤ u x

Full source

lemma IsBoundedUnder.eventually_ge (h : IsBoundedUnder (· ≥ ·) f u) :
    ∃ a, ∀ᶠ x in f, a ≤ u x :=
  IsBoundedUnder.eventually_le (α := αᵒᵈ) h

Existence of Lower Bound for Eventually Bounded Function under a Filter

Informal description

Given a filter $f$ on a type $\beta$ and a function $u : \beta \to \alpha$ where $\alpha$ is equipped with a preorder, if the values of $u$ are bounded below under $f$ (i.e., $\text{IsBoundedUnder}\, (\geq)\, f\, u$), then there exists an element $a \in \alpha$ such that $a \leq u(x)$ holds for all $x$ in some set belonging to $f$. In other words, if the function $u$ is eventually bounded below with respect to the filter $f$, then there exists a bound $a$ such that $a \leq u(x)$ holds "eventually" under $f$.

Filter.isBoundedUnder_of_eventually_le theorem

{a : α} (h : ∀ᶠ x in f, u x ≤ a) : IsBoundedUnder (· ≤ ·) f u

Full source

lemma isBoundedUnder_of_eventually_le {a : α} (h : ∀ᶠ x in f, u x ≤ a) :
    IsBoundedUnder (· ≤ ·) f u := ⟨a, h⟩

Boundedness from above under eventual inequality

Informal description

Let $\alpha$ be a type with a preorder, $\beta$ be another type, $f$ be a filter on $\beta$, and $u : \beta \to \alpha$ be a function. If there exists an element $a \in \alpha$ such that eventually for all $x$ in $f$, $u(x) \leq a$, then the filter $f$ is bounded above under the relation $\leq$ with respect to $u$.

Filter.isBoundedUnder_of_eventually_ge theorem

{a : α} (h : ∀ᶠ x in f, a ≤ u x) : IsBoundedUnder (· ≥ ·) f u

Full source

lemma isBoundedUnder_of_eventually_ge {a : α} (h : ∀ᶠ x in f, a ≤ u x) :
    IsBoundedUnder (· ≥ ·) f u := ⟨a, h⟩

Boundedness from below under eventual inequality

Informal description

Let $\alpha$ be a type with a preorder, $\beta$ be another type, $f$ be a filter on $\beta$, and $u : \beta \to \alpha$ be a function. If there exists an element $a \in \alpha$ such that eventually for all $x$ in $f$, $a \leq u(x)$, then the filter $f$ is bounded below under the relation $\geq$ with respect to $u$.

Filter.isBoundedUnder_iff_eventually_bddAbove theorem

: f.IsBoundedUnder (· ≤ ·) u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ x in f, x ∈ s

Full source

lemma isBoundedUnder_iff_eventually_bddAbove :
    f.IsBoundedUnder (· ≤ ·) u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ x in f, x ∈ s := by
  constructor
  · rintro ⟨b, hb⟩
    exact ⟨{a | u a ≤ b}, ⟨b, by rintro _ ⟨a, ha, rfl⟩; exact ha⟩, hb⟩
  · rintro ⟨s, ⟨b, hb⟩, hs⟩
    exact ⟨b, hs.mono <| by simpa [upperBounds] using hb⟩

Characterization of Boundedness Above Under a Filter: $f$ is bounded under $\leq$ with respect to $u$ iff $u$ is eventually bounded above on some set in $f$

Informal description

Let $\alpha$ be a type with a preorder, $\beta$ be another type, $f$ be a filter on $\beta$, and $u : \beta \to \alpha$ be a function. The filter $f$ is bounded above under the relation $\leq$ with respect to $u$ if and only if there exists a set $s \subseteq \beta$ such that the image $u(s)$ is bounded above in $\alpha$ and $s$ contains all elements of $f$ eventually (i.e., $\forallᶠ x \text{ in } f, x \in s$).

Filter.isBoundedUnder_iff_eventually_bddBelow theorem

: f.IsBoundedUnder (· ≥ ·) u ↔ ∃ s, BddBelow (u '' s) ∧ ∀ᶠ x in f, x ∈ s

Full source

lemma isBoundedUnder_iff_eventually_bddBelow :
    f.IsBoundedUnder (· ≥ ·) u ↔ ∃ s, BddBelow (u '' s) ∧ ∀ᶠ x in f, x ∈ s :=
  isBoundedUnder_iff_eventually_bddAbove (α := αᵒᵈ)

Characterization of Boundedness Below Under a Filter: $f$ is bounded under $\geq$ with respect to $u$ iff $u$ is eventually bounded below on some set in $f$

Informal description

Let $\alpha$ be a type with a preorder, $\beta$ be another type, $f$ be a filter on $\beta$, and $u : \beta \to \alpha$ be a function. The filter $f$ is bounded below under the relation $\geq$ with respect to $u$ if and only if there exists a set $s \subseteq \beta$ such that the image $u(s)$ is bounded below in $\alpha$ and $s$ contains all elements of $f$ eventually (i.e., $\forallᶠ x \text{ in } f, x \in s$).

BddAbove.isBoundedUnder theorem

(hs : s ∈ f) (hu : BddAbove (u '' s)) : f.IsBoundedUnder (· ≤ ·) u

Full source

lemma _root_.BddAbove.isBoundedUnder (hs : s ∈ f) (hu : BddAbove (u '' s)) :
    f.IsBoundedUnder (· ≤ ·) u := isBoundedUnder_iff_eventually_bddAbove.2 ⟨_, hu, hs⟩

Bounded Above Image Implies Filter Boundedness Under $\leq$

Informal description

Let $\alpha$ be a type with a preorder, $\beta$ be another type, $f$ be a filter on $\beta$, and $u : \beta \to \alpha$ be a function. If a set $s$ belongs to the filter $f$ and the image $u(s)$ is bounded above in $\alpha$, then the filter $f$ is bounded above under the relation $\leq$ with respect to $u$.

BddAbove.isBoundedUnder_of_range theorem

(hu : BddAbove (Set.range u)) : f.IsBoundedUnder (· ≤ ·) u

Full source

/-- A bounded above function `u` is in particular eventually bounded above. -/
lemma _root_.BddAbove.isBoundedUnder_of_range (hu : BddAbove (Set.range u)) :
    f.IsBoundedUnder (· ≤ ·) u := BddAbove.isBoundedUnder (s := univ) f.univ_mem (by simpa)

Bounded range implies filter boundedness under $\leq$

Informal description

Let $\alpha$ be a type with a preorder, $\beta$ be another type, $f$ be a filter on $\beta$, and $u : \beta \to \alpha$ be a function. If the range of $u$ is bounded above in $\alpha$, then the filter $f$ is bounded above under the relation $\leq$ with respect to $u$.

BddBelow.isBoundedUnder theorem

(hs : s ∈ f) (hu : BddBelow (u '' s)) : f.IsBoundedUnder (· ≥ ·) u

Full source

lemma _root_.BddBelow.isBoundedUnder (hs : s ∈ f) (hu : BddBelow (u '' s)) :
    f.IsBoundedUnder (· ≥ ·) u := isBoundedUnder_iff_eventually_bddBelow.2 ⟨_, hu, hs⟩

Bounded Below Image Implies Filter Boundedness Under $\geq$

Informal description

Let $\alpha$ be a type with a preorder, $\beta$ be another type, $f$ be a filter on $\beta$, and $u : \beta \to \alpha$ be a function. If a set $s$ belongs to the filter $f$ and the image $u(s)$ is bounded below in $\alpha$, then the filter $f$ is bounded below under the relation $\geq$ with respect to $u$.

BddBelow.isBoundedUnder_of_range theorem

(hu : BddBelow (Set.range u)) : f.IsBoundedUnder (· ≥ ·) u

Full source

/-- A bounded below function `u` is in particular eventually bounded below. -/
lemma _root_.BddBelow.isBoundedUnder_of_range (hu : BddBelow (Set.range u)) :
    f.IsBoundedUnder (· ≥ ·) u := BddBelow.isBoundedUnder (s := univ) f.univ_mem (by simpa)

Bounded below range implies filter boundedness under $\geq$

Informal description

Let $\alpha$ be a type with a preorder, $\beta$ be another type, $f$ be a filter on $\beta$, and $u : \beta \to \alpha$ be a function. If the range of $u$ is bounded below in $\alpha$, then the filter $f$ is bounded below under the relation $\geq$ with respect to $u$.

Filter.IsBoundedUnder.le_of_finite theorem

[Nonempty α] [IsDirected α (· ≤ ·)] [Finite β] {f : Filter β} {u : β → α} : IsBoundedUnder (· ≤ ·) f u

Full source

lemma IsBoundedUnder.le_of_finite [Nonempty α] [IsDirected α (· ≤ ·)] [Finite β]
    {f : Filter β} {u : β → α} : IsBoundedUnder (· ≤ ·) f u :=
  (Set.toFinite _).bddAbove.isBoundedUnder_of_range

Finite domain implies boundedness under $\leq$ in directed preorders

Informal description

Let $\alpha$ be a nonempty directed preorder (with respect to $\leq$) and $\beta$ be a finite type. For any filter $f$ on $\beta$ and any function $u : \beta \to \alpha$, the filter $f$ is bounded under $\leq$ with respect to $u$.

Filter.IsBoundedUnder.ge_of_finite theorem

[Nonempty α] [IsDirected α (· ≥ ·)] [Finite β] {f : Filter β} {u : β → α} : IsBoundedUnder (· ≥ ·) f u

Full source

lemma IsBoundedUnder.ge_of_finite [Nonempty α] [IsDirected α (· ≥ ·)] [Finite β]
    {f : Filter β} {u : β → α} : IsBoundedUnder (· ≥ ·) f u :=
  (Set.toFinite _).bddBelow.isBoundedUnder_of_range

Finite domain implies boundedness under $\geq$ in directed preorders

Informal description

Let $\alpha$ be a nonempty type with a preorder directed with respect to $\geq$, and let $\beta$ be a finite type. For any filter $f$ on $\beta$ and any function $u : \beta \to \alpha$, the filter $f$ is bounded under $\geq$ with respect to $u$.

Monotone.isBoundedUnder_le_comp theorem

 [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Monotone v) (hl : l.IsBoundedUnder (· ≤ ·) u) :
  l.IsBoundedUnder (· ≤ ·) (v ∘ u)

Full source

theorem _root_.Monotone.isBoundedUnder_le_comp [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α}
    {v : α → β} (hv : Monotone v) (hl : l.IsBoundedUnder (· ≤ ·) u) :
    l.IsBoundedUnder (· ≤ ·) (v ∘ u) :=
  hl.comp hv

Monotonicity Preserves Upper Boundedness Under Composition

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $l$ be a filter on a type $\gamma$. Given functions $u : \gamma \to \alpha$ and $v : \alpha \to \beta$, if $v$ is monotone and $l$ is bounded under the relation $\leq$ with respect to $u$, then $l$ is also bounded under $\leq$ with respect to the composition $v \circ u$.

Monotone.isBoundedUnder_ge_comp theorem

 [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Monotone v) (hl : l.IsBoundedUnder (· ≥ ·) u) :
  l.IsBoundedUnder (· ≥ ·) (v ∘ u)

Full source

theorem _root_.Monotone.isBoundedUnder_ge_comp [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α}
    {v : α → β} (hv : Monotone v) (hl : l.IsBoundedUnder (· ≥ ·) u) :
    l.IsBoundedUnder (· ≥ ·) (v ∘ u) :=
  hl.comp (swap hv)

Monotonicity Preserves Lower Boundedness Under Composition

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $l$ be a filter on a type $\gamma$. Given a monotone function $v : \alpha \to \beta$ and a function $u : \gamma \to \alpha$, if $l$ is bounded under the relation $\geq$ with respect to $u$, then $l$ is also bounded under $\geq$ with respect to the composition $v \circ u$.

Antitone.isBoundedUnder_le_comp theorem

 [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Antitone v) (hl : l.IsBoundedUnder (· ≥ ·) u) :
  l.IsBoundedUnder (· ≤ ·) (v ∘ u)

Full source

theorem _root_.Antitone.isBoundedUnder_le_comp [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α}
    {v : α → β} (hv : Antitone v) (hl : l.IsBoundedUnder (· ≥ ·) u) :
    l.IsBoundedUnder (· ≤ ·) (v ∘ u) :=
  hl.comp (swap hv)

Antitone Functions Preserve Lower Boundedness to Upper Boundedness

Informal description

Let $\alpha$ and $\beta$ be preorders, $l$ a filter on $\gamma$, $u : \gamma \to \alpha$ a function, and $v : \alpha \to \beta$ an antitone function. If $l$ is bounded below with respect to $u$ (i.e., there exists $a \in \alpha$ such that $a \leq u(x)$ for $x$ in some set of $l$), then $l$ is bounded above with respect to $v \circ u$ (i.e., there exists $b \in \beta$ such that $(v \circ u)(x) \leq b$ for $x$ in some set of $l$).

Antitone.isBoundedUnder_ge_comp theorem

 [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Antitone v) (hl : l.IsBoundedUnder (· ≤ ·) u) :
  l.IsBoundedUnder (· ≥ ·) (v ∘ u)

Full source

theorem _root_.Antitone.isBoundedUnder_ge_comp [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α}
    {v : α → β} (hv : Antitone v) (hl : l.IsBoundedUnder (· ≤ ·) u) :
    l.IsBoundedUnder (· ≥ ·) (v ∘ u) :=
  hl.comp hv

Boundedness Under Composition with Antitone Function

Informal description

Let $\alpha$ and $\beta$ be preorders, $l$ a filter on $\gamma$, $u : \gamma \to \alpha$ a function, and $v : \alpha \to \beta$ an antitone function. If $l$ is bounded under $\leq$ with respect to $u$, then $l$ is bounded under $\geq$ with respect to the composition $v \circ u$.

Filter.not_isBoundedUnder_of_tendsto_atTop theorem

 [Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α} [l.NeBot] (hf : Tendsto f l atTop) : ¬IsBoundedUnder (· ≤ ·) l f

Full source

theorem not_isBoundedUnder_of_tendsto_atTop [Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α}
    [l.NeBot] (hf : Tendsto f l atTop) : ¬IsBoundedUnder (· ≤ ·) l f := by
  rintro ⟨b, hb⟩
  rw [eventually_map] at hb
  obtain ⟨b', h⟩ := exists_gt b
  have hb' := (tendsto_atTop.mp hf) b'
  have : { x : α | f x ≤ b }{ x : α | f x ≤ b } ∩ { x : α | b' ≤ f x } = ∅ :=
    eq_empty_of_subset_empty fun x hx => (not_le_of_lt h) (le_trans hx.2 hx.1)
  exact (nonempty_of_mem (hb.and hb')).ne_empty this

Unboundedness of Functions Tending to Infinity in Preorders without Maximal Elements

Informal description

Let $\beta$ be a preorder with no maximal elements, and let $f : \alpha \to \beta$ be a function. If $f$ tends to $\mathrm{atTop}$ (i.e., $f(x) \to +\infty$) with respect to a non-trivial filter $l$ on $\alpha$, then $f$ is not bounded above under $l$ with respect to the relation $\leq$.

Filter.not_isBoundedUnder_of_tendsto_atBot theorem

 [Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α} [l.NeBot] (hf : Tendsto f l atBot) : ¬IsBoundedUnder (· ≥ ·) l f

Full source

theorem not_isBoundedUnder_of_tendsto_atBot [Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α}
    [l.NeBot] (hf : Tendsto f l atBot) : ¬IsBoundedUnder (· ≥ ·) l f :=
  not_isBoundedUnder_of_tendsto_atTop (β := βᵒᵈ) hf

Unboundedness of Functions Tending to Negative Infinity in Preorders without Minimal Elements

Informal description

Let $\beta$ be a preorder with no minimal elements, and let $f : \alpha \to \beta$ be a function. If $f$ tends to $\mathrm{atBot}$ (i.e., $f(x) \to -\infty$) with respect to a non-trivial filter $l$ on $\alpha$, then $f$ is not bounded below under $l$ with respect to the relation $\geq$.

Filter.IsBoundedUnder.bddAbove_range_of_cofinite theorem

 [Preorder β] [IsDirected β (· ≤ ·)] {f : α → β} (hf : IsBoundedUnder (· ≤ ·) cofinite f) : BddAbove (range f)

Full source

theorem IsBoundedUnder.bddAbove_range_of_cofinite [Preorder β] [IsDirected β (· ≤ ·)] {f : α → β}
    (hf : IsBoundedUnder (· ≤ ·) cofinite f) : BddAbove (range f) := by
  rcases hf with ⟨b, hb⟩
  haveI : Nonempty β := ⟨b⟩
  rw [← image_univ, ← union_compl_self { x | f x ≤ b }, image_union, bddAbove_union]
  exact ⟨⟨b, forall_mem_image.2 fun x => id⟩, (hb.image f).bddAbove⟩

Range of a Function is Bounded Above if Eventually Bounded Under Cofinite Filter

Informal description

Let $\beta$ be a preordered type with a directed order $\leq$. For any function $f \colon \alpha \to \beta$, if the values of $f$ are eventually bounded above under the cofinite filter on $\alpha$, then the range of $f$ is bounded above in $\beta$.

Filter.IsBoundedUnder.bddBelow_range_of_cofinite theorem

 [Preorder β] [IsDirected β (· ≥ ·)] {f : α → β} (hf : IsBoundedUnder (· ≥ ·) cofinite f) : BddBelow (range f)

Full source

theorem IsBoundedUnder.bddBelow_range_of_cofinite [Preorder β] [IsDirected β (· ≥ ·)] {f : α → β}
    (hf : IsBoundedUnder (· ≥ ·) cofinite f) : BddBelow (range f) :=
  IsBoundedUnder.bddAbove_range_of_cofinite (β := βᵒᵈ) hf

Range of a Function is Bounded Below if Eventually Bounded Under Cofinite Filter

Informal description

Let $\beta$ be a preordered type with a directed order $\geq$. For any function $f \colon \alpha \to \beta$, if the values of $f$ are eventually bounded below under the cofinite filter on $\alpha$, then the range of $f$ is bounded below in $\beta$.

Filter.IsBoundedUnder.bddAbove_range theorem

 [Preorder β] [IsDirected β (· ≤ ·)] {f : ℕ → β} (hf : IsBoundedUnder (· ≤ ·) atTop f) : BddAbove (range f)

Full source

theorem IsBoundedUnder.bddAbove_range [Preorder β] [IsDirected β (· ≤ ·)] {f : ℕ → β}
    (hf : IsBoundedUnder (· ≤ ·) atTop f) : BddAbove (range f) := by
  rw [← Nat.cofinite_eq_atTop] at hf
  exact hf.bddAbove_range_of_cofinite

Range of a Function is Bounded Above if Eventually Bounded Under `atTop` Filter on Natural Numbers

Informal description

Let $\beta$ be a preordered type with a directed order $\leq$. For any function $f \colon \mathbb{N} \to \beta$, if the values of $f$ are eventually bounded above under the `atTop` filter on $\mathbb{N}$, then the range of $f$ is bounded above in $\beta$.

Filter.IsBoundedUnder.bddBelow_range theorem

 [Preorder β] [IsDirected β (· ≥ ·)] {f : ℕ → β} (hf : IsBoundedUnder (· ≥ ·) atTop f) : BddBelow (range f)

Full source

theorem IsBoundedUnder.bddBelow_range [Preorder β] [IsDirected β (· ≥ ·)] {f : ℕ → β}
    (hf : IsBoundedUnder (· ≥ ·) atTop f) : BddBelow (range f) :=
  IsBoundedUnder.bddAbove_range (β := βᵒᵈ) hf

Range of a Function is Bounded Below if Eventually Bounded Under `atTop` Filter on Natural Numbers

Informal description

Let $\beta$ be a preordered type with a directed order $\geq$. For any function $f \colon \mathbb{N} \to \beta$, if the values of $f$ are eventually bounded below under the `atTop` filter on $\mathbb{N}$, then the range of $f$ is bounded below in $\beta$.

Filter.IsCobounded.mk theorem

[IsTrans α r] (a : α) (h : ∀ s ∈ f, ∃ x ∈ s, r a x) : f.IsCobounded r

Full source

/-- 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 IsCobounded.mk [IsTrans α r] (a : α) (h : ∀ s ∈ f, ∃ x ∈ s, r a x) : f.IsCobounded r :=
  ⟨a, fun _ s =>
    let ⟨_, h₁, h₂⟩ := h _ s
    _root_.trans h₂ h₁⟩

Sufficient Condition for Filter Coboundedness via Witness Element

Informal description

Let $\alpha$ be a type with a transitive relation $r$, and let $f$ be a filter on $\alpha$. Given an element $a \in \alpha$ such that for every set $s \in f$, there exists an element $x \in s$ with $r(a, x)$, then the filter $f$ is cobounded with respect to $r$.

Filter.IsBounded.isCobounded_flip theorem

[IsTrans α r] [NeBot f] : f.IsBounded r → f.IsCobounded (flip r)

Full source

/-- A filter which is eventually bounded is in particular frequently bounded (in the opposite
direction). At least if the filter is not trivial. -/
theorem IsBounded.isCobounded_flip [IsTrans α r] [NeBot f] : f.IsBounded r → f.IsCobounded (flip r)
  | ⟨a, ha⟩ =>
    ⟨a, fun b hb =>
      let ⟨_, rxa, rbx⟩ := (ha.and hb).exists
      show r b a from _root_.trans rbx rxa⟩

Boundedness Implies Coboundedness under Flipped Relation

Informal description

Let $\alpha$ be a type equipped with a transitive relation $r$, and let $f$ be a non-trivial filter on $\alpha$. If $f$ is bounded with respect to $r$, then $f$ is cobounded with respect to the flipped relation $\text{flip}\, r$ (where $\text{flip}\, r\, x\, y := r\, y\, x$).

Filter.IsBounded.isCobounded_ge theorem

[Preorder α] [NeBot f] (h : f.IsBounded (· ≤ ·)) : f.IsCobounded (· ≥ ·)

Full source

theorem IsBounded.isCobounded_ge [Preorder α] [NeBot f] (h : f.IsBounded (· ≤ ·)) :
    f.IsCobounded (· ≥ ·) :=
  h.isCobounded_flip

Boundedness with respect to $\leq$ implies coboundedness with respect to $\geq$ for non-trivial filters

Informal description

Let $\alpha$ be a preorder and $f$ a non-trivial filter on $\alpha$. If $f$ is bounded with respect to the relation $\leq$ (i.e., there exists some $b \in \alpha$ such that eventually all elements in $f$ are $\leq b$), then $f$ is cobounded with respect to the relation $\geq$ (i.e., there exists some $a \in \alpha$ such that frequently all elements in $f$ are $\geq a$).

Filter.IsBounded.isCobounded_le theorem

[Preorder α] [NeBot f] (h : f.IsBounded (· ≥ ·)) : f.IsCobounded (· ≤ ·)

Full source

theorem IsBounded.isCobounded_le [Preorder α] [NeBot f] (h : f.IsBounded (· ≥ ·)) :
    f.IsCobounded (· ≤ ·) :=
  h.isCobounded_flip

Boundedness with respect to $\geq$ implies coboundedness with respect to $\leq$ in a preorder

Informal description

Let $\alpha$ be a preorder and $f$ a non-trivial filter on $\alpha$. If $f$ is bounded with respect to the relation $\geq$ (i.e., there exists a lower bound for the filter), then $f$ is cobounded with respect to the relation $\leq$ (i.e., there exists an upper bound that frequently holds in the filter).

Filter.IsBoundedUnder.isCoboundedUnder_flip theorem

{u : γ → α} {l : Filter γ} [IsTrans α r] [NeBot l] (h : l.IsBoundedUnder r u) : l.IsCoboundedUnder (flip r) u

Full source

theorem IsBoundedUnder.isCoboundedUnder_flip {u : γ → α} {l : Filter γ} [IsTrans α r] [NeBot l]
    (h : l.IsBoundedUnder r u) : l.IsCoboundedUnder (flip r) u :=
  h.isCobounded_flip

Boundedness under relation implies coboundedness under flipped relation for non-trivial filters

Informal description

Let $\alpha$ be a type with a transitive relation $r$, $\gamma$ a type, $u : \gamma \to \alpha$ a function, and $l$ a non-trivial filter on $\gamma$. If the filter $l$ is bounded under $r$ with respect to $u$, then $l$ is cobounded under the flipped relation $\text{flip}\, r$ (where $\text{flip}\, r\, x\, y := r\, y\, x$) with respect to $u$.

Filter.IsBoundedUnder.isCoboundedUnder_le theorem

 {u : γ → α} {l : Filter γ} [Preorder α] [NeBot l] (h : l.IsBoundedUnder (· ≥ ·) u) : l.IsCoboundedUnder (· ≤ ·) u

Full source

theorem IsBoundedUnder.isCoboundedUnder_le {u : γ → α} {l : Filter γ} [Preorder α] [NeBot l]
    (h : l.IsBoundedUnder (· ≥ ·) u) : l.IsCoboundedUnder (· ≤ ·) u :=
  h.isCoboundedUnder_flip

Boundedness under $\geq$ implies coboundedness under $\leq$ for non-trivial filters

Informal description

Let $\alpha$ be a preorder, $\gamma$ a type, $u : \gamma \to \alpha$ a function, and $l$ a non-trivial filter on $\gamma$. If the filter $l$ is bounded under the relation $\geq$ with respect to $u$, then $l$ is cobounded under the relation $\leq$ with respect to $u$.

Filter.IsBoundedUnder.isCoboundedUnder_ge theorem

 {u : γ → α} {l : Filter γ} [Preorder α] [NeBot l] (h : l.IsBoundedUnder (· ≤ ·) u) : l.IsCoboundedUnder (· ≥ ·) u

Full source

theorem IsBoundedUnder.isCoboundedUnder_ge {u : γ → α} {l : Filter γ} [Preorder α] [NeBot l]
    (h : l.IsBoundedUnder (· ≤ ·) u) : l.IsCoboundedUnder (· ≥ ·) u :=
  h.isCoboundedUnder_flip

Boundedness under $\leq$ implies coboundedness under $\geq$ for non-trivial filters

Informal description

Let $\alpha$ be a preordered type, $\gamma$ a type, $u : \gamma \to \alpha$ a function, and $l$ a non-trivial filter on $\gamma$. If the filter $l$ is bounded under the relation $\leq$ with respect to $u$, then $l$ is cobounded under the relation $\geq$ with respect to $u$.

Filter.isCoboundedUnder_le_of_eventually_le theorem

 [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α} (hf : ∀ᶠ i in l, x ≤ f i) : IsCoboundedUnder (· ≤ ·) l f

Full source

lemma isCoboundedUnder_le_of_eventually_le [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α}
    (hf : ∀ᶠ i in l, x ≤ f i) :
    IsCoboundedUnder (· ≤ ·) l f :=
  IsBoundedUnder.isCoboundedUnder_le ⟨x, hf⟩

Coboundedness under $\leq$ from eventual lower bound

Informal description

Let $\alpha$ be a preordered type, $\iota$ a type, $l$ a non-trivial filter on $\iota$, and $f : \iota \to \alpha$ a function. If there exists an element $x \in \alpha$ such that $x \leq f(i)$ holds for all $i$ in some set belonging to $l$, then the filter $l$ is cobounded under the relation $\leq$ with respect to $f$.

Filter.isCoboundedUnder_ge_of_eventually_le theorem

 [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α} (hf : ∀ᶠ i in l, f i ≤ x) : IsCoboundedUnder (· ≥ ·) l f

Full source

lemma isCoboundedUnder_ge_of_eventually_le [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α}
    (hf : ∀ᶠ i in l, f i ≤ x) :
    IsCoboundedUnder (· ≥ ·) l f :=
  IsBoundedUnder.isCoboundedUnder_ge ⟨x, hf⟩

Coboundedness under $\geq$ for eventually bounded functions

Informal description

Let $\alpha$ be a preordered type, $\iota$ a type, $f : \iota \to \alpha$ a function, and $l$ a non-trivial filter on $\iota$. If there exists a real number $x$ such that $f(i) \leq x$ holds eventually with respect to $l$, then the filter $l$ is cobounded under the relation $\geq$ with respect to $f$.

Filter.isCoboundedUnder_le_of_le theorem

 [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α} (hf : ∀ i, x ≤ f i) : IsCoboundedUnder (· ≤ ·) l f

Full source

lemma isCoboundedUnder_le_of_le [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α}
    (hf : ∀ i, x ≤ f i) :
    IsCoboundedUnder (· ≤ ·) l f :=
  isCoboundedUnder_le_of_eventually_le l (Eventually.of_forall hf)

Coboundedness under $\leq$ for uniformly lower bounded functions

Informal description

Let $\alpha$ be a preordered type, $\iota$ a type, $l$ a non-trivial filter on $\iota$, and $f : \iota \to \alpha$ a function. If there exists an element $x \in \alpha$ such that $x \leq f(i)$ holds for all $i \in \iota$, then the filter $l$ is cobounded under the relation $\leq$ with respect to $f$.

Filter.isCoboundedUnder_ge_of_le theorem

 [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α} (hf : ∀ i, f i ≤ x) : IsCoboundedUnder (· ≥ ·) l f

Full source

lemma isCoboundedUnder_ge_of_le [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α}
    (hf : ∀ i, f i ≤ x) :
    IsCoboundedUnder (· ≥ ·) l f :=
  isCoboundedUnder_ge_of_eventually_le l (Eventually.of_forall hf)

Coboundedness under $\geq$ for uniformly bounded functions

Informal description

Let $\alpha$ be a preordered type, $\iota$ a type, $f : \iota \to \alpha$ a function, and $l$ a non-trivial filter on $\iota$. If there exists an element $x \in \alpha$ such that $f(i) \leq x$ holds for all $i \in \iota$, then the filter $l$ is cobounded under the relation $\geq$ with respect to $f$.

Filter.isCobounded_bot theorem

: IsCobounded r ⊥ ↔ ∃ b, ∀ x, r b x

Full source

theorem isCobounded_bot : IsCoboundedIsCobounded r ⊥ ↔ ∃ b, ∀ x, r b x := by simp [IsCobounded]

Coboundedness of Bottom Filter: $\text{IsCobounded}\, r\, \bot \leftrightarrow \exists b, \forall x, r(b, x)$

Informal description

For any relation $r$ on a type $\alpha$, the bottom filter $\bot$ is cobounded with respect to $r$ if and only if there exists an element $b \in \alpha$ such that for all $x \in \alpha$, the relation $r(b, x)$ holds.

Filter.isCobounded_top theorem

: IsCobounded r ⊤ ↔ Nonempty α

Full source

theorem isCobounded_top : IsCoboundedIsCobounded r ⊤ ↔ Nonempty α := by
  simp +contextual [IsCobounded, eq_univ_iff_forall,
    exists_true_iff_nonempty]

Coboundedness of the Top Filter is Equivalent to Nonemptiness of the Type

Informal description

The filter consisting of all subsets of a type $\alpha$ is cobounded with respect to a relation $r$ if and only if $\alpha$ is nonempty.

Filter.isCobounded_principal theorem

(s : Set α) : (𝓟 s).IsCobounded r ↔ ∃ b, ∀ a, (∀ x ∈ s, r x a) → r b a

Full source

theorem isCobounded_principal (s : Set α) :
    (𝓟 s).IsCobounded r ↔ ∃ b, ∀ a, (∀ x ∈ s, r x a) → r b a := by simp [IsCobounded, subset_def]

Coboundedness Criterion for Principal Filters

Informal description

For any set $s$ in a type $\alpha$ and a relation $r$ on $\alpha$, the principal filter $\mathfrak{P}(s)$ is cobounded with respect to $r$ if and only if there exists an element $b \in \alpha$ such that for all $a \in \alpha$, if $r(x, a)$ holds for every $x \in s$, then $r(b, a)$ holds.

Filter.IsCobounded.mono theorem

(h : f ≤ g) : f.IsCobounded r → g.IsCobounded r

Full source

theorem IsCobounded.mono (h : f ≤ g) : f.IsCobounded r → g.IsCobounded r
  | ⟨b, hb⟩ => ⟨b, fun a ha => hb a (h ha)⟩

Monotonicity of Cobounded Filters: $f \leq g$ Implies $g$ is Cobounded if $f$ is Cobounded

Informal description

If a filter $f$ is cobounded with respect to a relation $r$ and $f \leq g$ in the partial order of filters, then $g$ is also cobounded with respect to $r$.

Filter.IsCobounded.frequently_ge theorem

[LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≤ ·) f) : ∃ l, ∃ᶠ x in f, l ≤ x

Full source

/-- For nontrivial filters in linear orders, coboundedness for `≤` implies frequent boundedness
from below. -/
lemma IsCobounded.frequently_ge [LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≤ ·) f) :
    ∃ l, ∃ᶠ x in f, l ≤ x := by
  obtain ⟨t, ht⟩ := cobdd
  rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩
  · exact ⟨t, .of_forall fun r ↦ tbot r⟩
  refine ⟨t', fun ev ↦ ?_⟩
  specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)
  exact not_lt_of_le ht ht'

Frequent Lower Boundedness from Coboundedness in Linear Orders

Informal description

Let $\alpha$ be a linearly ordered type and $f$ a non-trivial filter on $\alpha$. If $f$ is cobounded with respect to the relation $\leq$, then there exists an element $l \in \alpha$ such that the set $\{x \mid l \leq x\}$ is frequently in $f$ (i.e., $l \leq x$ holds for arbitrarily large $x$ with respect to $f$).

Filter.IsCobounded.frequently_le theorem

[LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≥ ·) f) : ∃ u, ∃ᶠ x in f, x ≤ u

Full source

/-- For nontrivial filters in linear orders, coboundedness for `≥` implies frequent boundedness
from above. -/
lemma IsCobounded.frequently_le [LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≥ ·) f) :
    ∃ u, ∃ᶠ x in f, x ≤ u :=
  cobdd.frequently_ge (α := αᵒᵈ)

Frequent Upper Boundedness from Coboundedness in Linear Orders

Informal description

Let $\alpha$ be a linearly ordered type and $f$ a non-trivial filter on $\alpha$. If $f$ is cobounded with respect to the relation $\geq$, then there exists an element $u \in \alpha$ such that the set $\{x \mid x \leq u\}$ is frequently in $f$ (i.e., $x \leq u$ holds for arbitrarily large $x$ with respect to $f$).

Filter.IsCobounded.of_frequently_ge theorem

[LinearOrder α] {l : α} (freq_ge : ∃ᶠ x in f, l ≤ x) : IsCobounded (· ≤ ·) f

Full source

/-- In linear orders, frequent boundedness from below implies coboundedness for `≤`. -/
lemma IsCobounded.of_frequently_ge [LinearOrder α] {l : α} (freq_ge : ∃ᶠ x in f, l ≤ x) :
    IsCobounded (· ≤ ·) f := by
  rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩
  · exact ⟨l, fun x _ ↦ lbot x⟩
  refine ⟨l', fun u hu ↦ ?_⟩
  obtain ⟨w, l_le_w, w_le_u⟩ := (freq_ge.and_eventually hu).exists
  exact hl'.le.trans (l_le_w.trans w_le_u)

Frequent Lower Boundedness Implies Coboundedness for $\leq$ in Linear Orders

Informal description

Let $\alpha$ be a linearly ordered type and $f$ a filter on $\alpha$. If there exists an element $l \in \alpha$ such that the set $\{x \mid l \leq x\}$ is frequently in $f$ (i.e., $\existsᶠ x \text{ in } f, l \leq x$), then the filter $f$ is cobounded with respect to the relation $\leq$.

Filter.IsCobounded.of_frequently_le theorem

[LinearOrder α] {u : α} (freq_le : ∃ᶠ r in f, r ≤ u) : IsCobounded (· ≥ ·) f

Full source

/-- In linear orders, frequent boundedness from above implies coboundedness for `≥`. -/
lemma IsCobounded.of_frequently_le [LinearOrder α] {u : α} (freq_le : ∃ᶠ r in f, r ≤ u) :
    IsCobounded (· ≥ ·) f :=
  IsCobounded.of_frequently_ge (α := αᵒᵈ) freq_le

Frequent Upper Boundedness Implies Coboundedness for $\geq$ in Linear Orders

Informal description

Let $\alpha$ be a linearly ordered type and $f$ a filter on $\alpha$. If there exists an element $u \in \alpha$ such that the set $\{x \mid x \leq u\}$ is frequently in $f$ (i.e., $\existsᶠ x \text{ in } f, x \leq u$), then the filter $f$ is cobounded with respect to the relation $\geq$.

Filter.IsCoboundedUnder.frequently_ge theorem

 [LinearOrder α] {f : Filter ι} [NeBot f] {u : ι → α} (h : IsCoboundedUnder (· ≤ ·) f u) : ∃ a, ∃ᶠ x in f, a ≤ u x

Full source

lemma IsCoboundedUnder.frequently_ge [LinearOrder α] {f : Filter ι} [NeBot f] {u : ι → α}
    (h : IsCoboundedUnder (· ≤ ·) f u) :
    ∃ a, ∃ᶠ x in f, a ≤ u x :=
  IsCobounded.frequently_ge h

Frequent Lower Boundedness from Coboundedness Under $\leq$ in Linear Orders

Informal description

Let $\alpha$ be a linearly ordered type, $f$ a non-trivial filter on a type $\iota$, and $u : \iota \to \alpha$ a function. If $f$ is cobounded under $u$ with respect to the relation $\leq$, then there exists an element $a \in \alpha$ such that the set $\{x \mid a \leq u(x)\}$ is frequently in $f$ (i.e., $a \leq u(x)$ holds for arbitrarily large $x$ with respect to $f$).

Filter.IsCoboundedUnder.frequently_le theorem

 [LinearOrder α] {f : Filter ι} [NeBot f] {u : ι → α} (h : IsCoboundedUnder (· ≥ ·) f u) : ∃ a, ∃ᶠ x in f, u x ≤ a

Full source

lemma IsCoboundedUnder.frequently_le [LinearOrder α] {f : Filter ι} [NeBot f] {u : ι → α}
    (h : IsCoboundedUnder (· ≥ ·) f u) :
    ∃ a, ∃ᶠ x in f, u x ≤ a :=
  IsCobounded.frequently_le h

Frequent Upper Boundedness from Coboundedness Under $\geq$ in Linear Orders

Informal description

Let $\alpha$ be a linearly ordered type, $f$ a non-trivial filter on a type $\iota$, and $u : \iota \to \alpha$ a function. If $f$ is cobounded under $u$ with respect to the relation $\geq$, then there exists an element $a \in \alpha$ such that the set $\{x \mid u(x) \leq a\}$ is frequently in $f$ (i.e., $u(x) \leq a$ holds for arbitrarily large $x$ with respect to $f$).

Filter.IsCoboundedUnder.of_frequently_ge theorem

 [LinearOrder α] {f : Filter ι} {u : ι → α} {a : α} (freq_ge : ∃ᶠ x in f, a ≤ u x) : IsCoboundedUnder (· ≤ ·) f u

Full source

lemma IsCoboundedUnder.of_frequently_ge [LinearOrder α] {f : Filter ι} {u : ι → α}
    {a : α} (freq_ge : ∃ᶠ x in f, a ≤ u x) :
    IsCoboundedUnder (· ≤ ·) f u :=
  IsCobounded.of_frequently_ge freq_ge

Frequent Lower Boundedness Implies Coboundedness Under $\leq$

Informal description

Let $\alpha$ be a linearly ordered type, $f$ a filter on a type $\iota$, and $u : \iota \to \alpha$ a function. If there exists an element $a \in \alpha$ such that the set $\{x \mid a \leq u(x)\}$ is frequently in $f$ (i.e., $\existsᶠ x \text{ in } f, a \leq u(x)$), then the filter $f$ is cobounded under $u$ with respect to the relation $\leq$.

Filter.IsCoboundedUnder.of_frequently_le theorem

 [LinearOrder α] {f : Filter ι} {u : ι → α} {a : α} (freq_le : ∃ᶠ x in f, u x ≤ a) : IsCoboundedUnder (· ≥ ·) f u

Full source

lemma IsCoboundedUnder.of_frequently_le [LinearOrder α] {f : Filter ι} {u : ι → α}
    {a : α} (freq_le : ∃ᶠ x in f, u x ≤ a) :
    IsCoboundedUnder (· ≥ ·) f u :=
  IsCobounded.of_frequently_le freq_le

Frequent Upper Boundedness Implies Coboundedness Under $\geq$

Informal description

Let $\alpha$ be a linearly ordered type, $f$ a filter on a type $\iota$, and $u : \iota \to \alpha$ a function. If there exists an element $a \in \alpha$ such that the set $\{x \mid u(x) \leq a\}$ is frequently in $f$ (i.e., $\existsᶠ x \text{ in } f, u(x) \leq a$), then the filter $f$ is cobounded under $u$ with respect to the relation $\geq$.

Filter.isBoundedUnder_sum theorem

 {κ : Type*} [AddCommMonoid R] {r : R → R → Prop}
  (hr : ∀ (v₁ v₂ : α → R), f.IsBoundedUnder r v₁ → f.IsBoundedUnder r v₂ → f.IsBoundedUnder r (v₁ + v₂)) (hr₀ : r 0 0)
  {u : κ → α → R} (s : Finset κ) (h : ∀ k ∈ s, f.IsBoundedUnder r (u k)) : f.IsBoundedUnder r (∑ k ∈ s, u k)

Full source

lemma isBoundedUnder_sum {κ : Type*} [AddCommMonoid R] {r : R → R → Prop}
    (hr : ∀ (v₁ v₂ : α → R), f.IsBoundedUnder r v₁ → f.IsBoundedUnder r v₂
      → f.IsBoundedUnder r (v₁ + v₂)) (hr₀ : r 0 0)
    {u : κ → α → R} (s : Finset κ) (h : ∀ k ∈ s, f.IsBoundedUnder r (u k)) :
    f.IsBoundedUnder r (∑ k ∈ s, u k) := by
  induction s using Finset.cons_induction
  case empty =>
    rw [Finset.sum_empty]
    exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩
  case cons k₀ s k₀_notin_s ih =>
    simp only [Finset.forall_mem_cons] at *
    simpa only [Finset.sum_cons] using hr _ _ h.1 (ih h.2)

Boundedness Under Relation Preserved by Finite Sums in Additive Commutative Monoids

Informal description

Let $R$ be an additive commutative monoid with a relation $r : R \to R \to \text{Prop}$ such that: 1. For any functions $v_1, v_2 : \alpha \to R$, if $f$ is bounded under $r$ with respect to $v_1$ and $v_2$, then $f$ is also bounded under $r$ with respect to $v_1 + v_2$. 2. The relation $r$ holds for the zero element, i.e., $r(0, 0)$. Given a finite set $s$ of indices $\kappa$ and a family of functions $u_k : \alpha \to R$ for $k \in s$ such that for each $k \in s$, the filter $f$ is bounded under $r$ with respect to $u_k$, then the filter $f$ is bounded under $r$ with respect to the sum $\sum_{k \in s} u_k$.

Filter.isBoundedUnder_ge_add theorem

 [Add R] [AddLeftMono R] [AddRightMono R] {u v : α → R} (u_bdd_ge : f.IsBoundedUnder (· ≥ ·) u)
  (v_bdd_ge : f.IsBoundedUnder (· ≥ ·) v) : f.IsBoundedUnder (· ≥ ·) (u + v)

Full source

lemma isBoundedUnder_ge_add [Add R] [AddLeftMono R] [AddRightMono R]
    {u v : α → R} (u_bdd_ge : f.IsBoundedUnder (· ≥ ·) u) (v_bdd_ge : f.IsBoundedUnder (· ≥ ·) v) :
    f.IsBoundedUnder (· ≥ ·) (u + v) := by
  obtain ⟨U, hU⟩ := u_bdd_ge
  obtain ⟨V, hV⟩ := v_bdd_ge
  use U + V
  simp only [eventually_map, Pi.add_apply] at hU hV ⊢
  filter_upwards [hU, hV] with a hu hv using add_le_add hu hv

Sum of Eventually Bounded Below Functions is Eventually Bounded Below

Informal description

Let $R$ be a type equipped with an addition operation and partial orders such that addition is both left- and right-monotone. Given two functions $u, v : \alpha \to R$ and a filter $f$ on $\alpha$, if the values of $u$ are eventually bounded below with respect to $f$ (i.e., $\exists b, \forallᶠ x \text{ in } f, u(x) \geq b$) and similarly for $v$, then the sum $u + v$ is also eventually bounded below with respect to $f$.

Filter.isBoundedUnder_le_add theorem

 [Add R] [AddLeftMono R] [AddRightMono R] {u v : α → R} (u_bdd_le : f.IsBoundedUnder (· ≤ ·) u)
  (v_bdd_le : f.IsBoundedUnder (· ≤ ·) v) : f.IsBoundedUnder (· ≤ ·) (u + v)

Full source

lemma isBoundedUnder_le_add [Add R] [AddLeftMono R] [AddRightMono R]
    {u v : α → R} (u_bdd_le : f.IsBoundedUnder (· ≤ ·) u) (v_bdd_le : f.IsBoundedUnder (· ≤ ·) v) :
    f.IsBoundedUnder (· ≤ ·) (u + v) := by
  obtain ⟨U, hU⟩ := u_bdd_le
  obtain ⟨V, hV⟩ := v_bdd_le
  use U + V
  simp only [eventually_map, Pi.add_apply] at hU hV ⊢
  filter_upwards [hU, hV] with a hu hv using add_le_add hu hv

Sum of Eventually Bounded Above Functions is Eventually Bounded Above

Informal description

Let $R$ be an additive type with a preorder such that addition is both left- and right-monotone (i.e., $a \leq b$ implies $a + c \leq b + c$ and $c + a \leq c + b$ for any $c$). Given two functions $u, v : \alpha \to R$ and a filter $f$ on $\alpha$, if $u$ and $v$ are eventually bounded above under $f$ (i.e., there exist $M_u, M_v \in R$ such that $\forallᶠ x \text{ in } f, u(x) \leq M_u$ and $\forallᶠ x \text{ in } f, v(x) \leq M_v$), then their sum $u + v$ is also eventually bounded above under $f$.

Filter.isBoundedUnder_le_sum theorem

 {κ : Type*} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R] {u : κ → α → R} (s : Finset κ) :
  (∀ k ∈ s, f.IsBoundedUnder (· ≤ ·) (u k)) → f.IsBoundedUnder (· ≤ ·) (∑ k ∈ s, u k)

Full source

lemma isBoundedUnder_le_sum {κ : Type*} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R]
    {u : κ → α → R} (s : Finset κ) :
    (∀ k ∈ s, f.IsBoundedUnder (· ≤ ·) (u k)) → f.IsBoundedUnder (· ≤ ·) (∑ k ∈ s, u k) :=
  fun h ↦ isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_le_add) le_rfl s h

Finite Sum of Eventually Bounded Above Functions is Eventually Bounded Above

Informal description

Let $R$ be an additive commutative monoid with a preorder such that addition is both left- and right-monotone (i.e., $a \leq b$ implies $a + c \leq b + c$ and $c + a \leq c + b$ for any $c$). Given a finite set $s$ of indices $\kappa$ and a family of functions $u_k : \alpha \to R$ for $k \in s$, if for each $k \in s$ the function $u_k$ is eventually bounded above under a filter $f$ on $\alpha$, then the sum $\sum_{k \in s} u_k$ is also eventually bounded above under $f$.

Filter.isBoundedUnder_ge_sum theorem

 {κ : Type*} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R] {u : κ → α → R} (s : Finset κ) :
  (∀ k ∈ s, f.IsBoundedUnder (· ≥ ·) (u k)) → f.IsBoundedUnder (· ≥ ·) (∑ k ∈ s, u k)

Full source

lemma isBoundedUnder_ge_sum {κ : Type*} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R]
    {u : κ → α → R} (s : Finset κ) :
    (∀ k ∈ s, f.IsBoundedUnder (· ≥ ·) (u k)) →
      f.IsBoundedUnder (· ≥ ·) (∑ k ∈ s, u k) :=
  fun h ↦ isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_ge_add) le_rfl s h

Finite Sum of Eventually Bounded Below Functions is Eventually Bounded Below

Informal description

Let $R$ be an additive commutative monoid with a partial order such that addition is both left- and right-monotone. Given a finite set $s$ of indices $\kappa$ and a family of functions $u_k : \alpha \to R$ for $k \in s$, if for each $k \in s$ the values of $u_k$ are eventually bounded below with respect to a filter $f$ on $\alpha$, then the sum $\sum_{k \in s} u_k$ is also eventually bounded below with respect to $f$.

Filter.isCoboundedUnder_ge_add theorem

(hu : f.IsBoundedUnder (· ≤ ·) u) (hv : f.IsCoboundedUnder (· ≥ ·) v) : f.IsCoboundedUnder (· ≥ ·) (u + v)

Full source

lemma isCoboundedUnder_ge_add (hu : f.IsBoundedUnder (· ≤ ·) u)
    (hv : f.IsCoboundedUnder (· ≥ ·) v) :
    f.IsCoboundedUnder (· ≥ ·) (u + v) := by
  obtain ⟨U, hU⟩ := hu.eventually_le
  obtain ⟨V, hV⟩ := hv.frequently_le
  apply IsCoboundedUnder.of_frequently_le (a := U + V)
  exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

Coboundedness of Sum under Filter for Bounded Above and Cobounded Below Functions

Informal description

Let $\alpha$ be a type with an addition operation, and let $f$ be a filter on a type $\iota$. Given functions $u, v : \iota \to \alpha$ such that: 1. $u$ is bounded above under $f$ (i.e., $\text{IsBoundedUnder}\, (\leq)\, f\, u$), and 2. $v$ is cobounded below under $f$ (i.e., $\text{IsCoboundedUnder}\, (\geq)\, f\, v$), then the sum $u + v$ is cobounded below under $f$ (i.e., $\text{IsCoboundedUnder}\, (\geq)\, f\, (u + v)$).

Filter.isCoboundedUnder_le_add theorem

(hu : f.IsBoundedUnder (· ≥ ·) u) (hv : f.IsCoboundedUnder (· ≤ ·) v) : f.IsCoboundedUnder (· ≤ ·) (u + v)

Full source

lemma isCoboundedUnder_le_add (hu : f.IsBoundedUnder (· ≥ ·) u)
    (hv : f.IsCoboundedUnder (· ≤ ·) v) :
    f.IsCoboundedUnder (· ≤ ·) (u + v) := by
  obtain ⟨U, hU⟩ := hu.eventually_ge
  obtain ⟨V, hV⟩ := hv.frequently_ge
  apply IsCoboundedUnder.of_frequently_ge (a := U + V)
  exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

Coboundedness of Sum under Filter for Bounded Below and Cobounded Above Functions

Informal description

Let $\alpha$ be a type with an addition operation, and let $f$ be a filter on a type $\iota$. Given functions $u, v : \iota \to \alpha$ such that: 1. $u$ is bounded below under $f$ (i.e., $\text{IsBoundedUnder}\, (\geq)\, f\, u$), and 2. $v$ is cobounded above under $f$ (i.e., $\text{IsCoboundedUnder}\, (\leq)\, f\, v$), then the sum $u + v$ is cobounded above under $f$ (i.e., $\text{IsCoboundedUnder}\, (\leq)\, f\, (u + v)$).

Filter.isBoundedUnder_le_mul_of_nonneg theorem

 [Preorder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {f : Filter ι} {u v : ι → α} (h₁ : ∃ᶠ x in f, 0 ≤ u x)
  (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) :
  IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)

Full source

lemma isBoundedUnder_le_mul_of_nonneg [Preorder α] [Mul α] [Zero α] [PosMulMono α]
    [MulPosMono α] {f : Filter ι} {u v : ι → α} (h₁ : ∃ᶠ x in f, 0 ≤ u x)
    (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v)
    (h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v) :
    IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v) := by
  obtain ⟨U, hU⟩ := h₂.eventually_le
  obtain ⟨V, hV⟩ := h₄.eventually_le
  refine isBoundedUnder_of_eventually_le (a := U * V) ?_
  filter_upwards [hU, hV, h₃] with x x_U x_V v_0
  have U_0 : 0 ≤ U := by
    obtain ⟨y, y_0, y_U⟩ := (h₁.and_eventually hU).exists
    exact y_0.trans y_U
  exact (mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V U_0)

Boundedness of product under filter for nonnegative functions

Informal description

Let $\alpha$ be a preordered type with a multiplication operation, zero element, and satisfying the conditions that left and right multiplication by nonnegative elements are monotone. Given a filter $f$ on a type $\iota$ and functions $u, v : \iota \to \alpha$ such that: 1. The set $\{x \mid 0 \leq u(x)\}$ is frequently in $f$, 2. $u$ is bounded above under $f$ with respect to $\leq$, 3. The set $\{x \mid 0 \leq v(x)\}$ is eventually in $f$, 4. $v$ is bounded above under $f$ with respect to $\leq$, then the product function $u \cdot v$ is bounded above under $f$ with respect to $\leq$.

Filter.isCoboundedUnder_ge_mul_of_nonneg theorem

 [LinearOrder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u)
  (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) :
  IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f (u * v)

Full source

lemma isCoboundedUnder_ge_mul_of_nonneg [LinearOrder α] [Mul α] [Zero α] [PosMulMono α]
    [MulPosMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : 0 ≤ᶠ[f] u)
    (h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u)
    (h₃ : 0 ≤ᶠ[f] v)
    (h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v) :
    IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f (u * v) := by
  obtain ⟨U, hU⟩ := h₂.eventually_le
  obtain ⟨V, hV⟩ := h₄.frequently_le
  refine IsCoboundedUnder.of_frequently_le (a := U * V) ?_
  apply (hV.and_eventually (hU.and (h₁.and h₃))).mono
  intro x ⟨x_V, x_U, u_0, v_0⟩
  exact (mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V (u_0.trans x_U))

Coboundedness of product under filter for nonnegative functions

Informal description

Let $\alpha$ be a linearly ordered type with a multiplication operation and a zero element, where left and right multiplication by nonnegative elements are monotone. Let $f$ be a non-trivial filter on a type $\iota$, and let $u, v : \iota \to \alpha$ be functions such that: 1. $u(x) \geq 0$ holds eventually under $f$, 2. $u$ is bounded above under $f$ with respect to $\leq$, 3. $v(x) \geq 0$ holds eventually under $f$, 4. $v$ is cobounded below under $f$ with respect to $\geq$. Then the product function $u \cdot v$ is cobounded below under $f$ with respect to $\geq$.

Filter.isBounded_le_atBot theorem

: (atBot : Filter α).IsBounded (· ≤ ·)

Full source

theorem isBounded_le_atBot : (atBot : Filter α).IsBounded (· ≤ ·) :=
  ‹Nonempty α›.elim fun a => ⟨a, eventually_le_atBot _⟩

Boundedness of `atBot` Filter with Respect to $\leq$

Informal description

The filter `atBot` on a preorder $\alpha$ is bounded with respect to the "less than or equal to" relation $\leq$. That is, there exists an element $b \in \alpha$ such that for all $x$ in some set belonging to `atBot`, the relation $x \leq b$ holds.

Filter.isBounded_ge_atTop theorem

: (atTop : Filter α).IsBounded (· ≥ ·)

Full source

theorem isBounded_ge_atTop : (atTop : Filter α).IsBounded (· ≥ ·) :=
  ‹Nonempty α›.elim fun a => ⟨a, eventually_ge_atTop _⟩

Boundedness of `atTop` filter with respect to $\geq$ relation

Informal description

The filter `atTop` on a preorder $\alpha$ is bounded with respect to the greater-than-or-equal-to relation $\geq$. That is, there exists an element $b \in \alpha$ such that for all sufficiently large $x$ (i.e., for all $x$ in some set belonging to `atTop`), we have $x \geq b$.

Filter.Tendsto.isBoundedUnder_le_atBot theorem

(h : Tendsto u f atBot) : f.IsBoundedUnder (· ≤ ·) u

Full source

theorem Tendsto.isBoundedUnder_le_atBot (h : Tendsto u f atBot) : f.IsBoundedUnder (· ≤ ·) u :=
  isBounded_le_atBot.mono h

Boundedness under $\leq$ for functions tending to $-\infty$

Informal description

Let $f$ be a filter on a type $\beta$, and let $u : \beta \to \alpha$ be a function where $\alpha$ is a preorder. If $u$ tends to $-\infty$ along $f$ (i.e., $\text{Tendsto } u f \text{ atBot}$), then $f$ is bounded under the relation $\leq$ with respect to $u$. That is, there exists an element $b \in \alpha$ such that for all $x$ in some set belonging to $f$, we have $u(x) \leq b$.

Filter.Tendsto.isBoundedUnder_ge_atTop theorem

(h : Tendsto u f atTop) : f.IsBoundedUnder (· ≥ ·) u

Full source

theorem Tendsto.isBoundedUnder_ge_atTop (h : Tendsto u f atTop) : f.IsBoundedUnder (· ≥ ·) u :=
  isBounded_ge_atTop.mono h

Boundedness Under $\geq$ for Functions Tending to $\infty$

Informal description

Let $\alpha$ be a type with a preorder, and let $f$ be a filter on a type $\beta$. Given a function $u : \beta \to \alpha$, if $u$ tends to $\infty$ with respect to the filter $f$ (i.e., $\text{Tendsto } u f \text{ atTop}$), then the filter $f$ is bounded under the relation $\geq$ with respect to $u$. This means there exists an element $b \in \alpha$ such that for all sufficiently large $x$ in the filter $f$, we have $u(x) \geq b$.

Filter.bddAbove_range_of_tendsto_atTop_atBot theorem

[IsDirected α (· ≤ ·)] {u : ℕ → α} (hx : Tendsto u atTop atBot) : BddAbove (Set.range u)

Full source

theorem bddAbove_range_of_tendsto_atTop_atBot [IsDirected α (· ≤ ·)] {u : ℕ → α}
    (hx : Tendsto u atTop atBot) : BddAbove (Set.range u) :=
  hx.isBoundedUnder_le_atBot.bddAbove_range

Range of a Sequence Tending to $-\infty$ is Bounded Above

Informal description

Let $\alpha$ be a type with a preorder such that the relation $\leq$ is directed. For any sequence $u \colon \mathbb{N} \to \alpha$, if $u$ tends to $-\infty$ (i.e., $\lim_{n \to \infty} u(n) = -\infty$), then the range of $u$ is bounded above in $\alpha$.

Filter.bddBelow_range_of_tendsto_atTop_atTop theorem

[IsDirected α (· ≥ ·)] {u : ℕ → α} (hx : Tendsto u atTop atTop) : BddBelow (Set.range u)

Full source

theorem bddBelow_range_of_tendsto_atTop_atTop [IsDirected α (· ≥ ·)] {u : ℕ → α}
    (hx : Tendsto u atTop atTop) : BddBelow (Set.range u) :=
  hx.isBoundedUnder_ge_atTop.bddBelow_range

Range of a Sequence Tending to $\infty$ is Bounded Below

Informal description

Let $\alpha$ be a preordered type where the relation $\geq$ is directed. For any sequence $u \colon \mathbb{N} \to \alpha$, if $u$ tends to $\infty$ (i.e., $\lim_{n \to \infty} u(n) = \infty$), then the range of $u$ is bounded below in $\alpha$.

Filter.isCobounded_le_of_bot theorem

[LE α] [OrderBot α] {f : Filter α} : f.IsCobounded (· ≤ ·)

Full source

theorem isCobounded_le_of_bot [LE α] [OrderBot α] {f : Filter α} : f.IsCobounded (· ≤ ·) :=
  ⟨⊥, fun _ _ => bot_le⟩

Coboundedness of a Filter with Bottom Element under $\leq$

Informal description

For any filter $f$ on a type $\alpha$ equipped with a preorder and a bottom element $\bot$, the filter $f$ is cobounded with respect to the "less than or equal to" relation $\leq$.

Filter.isCobounded_ge_of_top theorem

[LE α] [OrderTop α] {f : Filter α} : f.IsCobounded (· ≥ ·)

Full source

theorem isCobounded_ge_of_top [LE α] [OrderTop α] {f : Filter α} : f.IsCobounded (· ≥ ·) :=
  ⟨⊤, fun _ _ => le_top⟩

Coboundedness of Filter with Greatest Element under $\geq$ Relation

Informal description

For any type $\alpha$ with a preorder and a greatest element $\top$, and for any filter $f$ on $\alpha$, the filter $f$ is cobounded with respect to the "greater than or equal to" relation $\geq$.

Filter.isBounded_le_of_top theorem

[LE α] [OrderTop α] {f : Filter α} : f.IsBounded (· ≤ ·)

Full source

theorem isBounded_le_of_top [LE α] [OrderTop α] {f : Filter α} : f.IsBounded (· ≤ ·) :=
  ⟨⊤, Eventually.of_forall fun _ => le_top⟩

Boundedness of a Filter with Greatest Element under $\leq$

Informal description

For any filter $f$ on a type $\alpha$ equipped with a preorder and a greatest element $\top$, the filter $f$ is bounded with respect to the relation $\leq$. That is, there exists an element $b \in \alpha$ such that for all $x$ in some set belonging to $f$, we have $x \leq b$.

Filter.isBounded_ge_of_bot theorem

[LE α] [OrderBot α] {f : Filter α} : f.IsBounded (· ≥ ·)

Full source

theorem isBounded_ge_of_bot [LE α] [OrderBot α] {f : Filter α} : f.IsBounded (· ≥ ·) :=
  ⟨⊥, Eventually.of_forall fun _ => bot_le⟩

Filters with Bottom Element are Bounded Below

Informal description

For any filter $f$ on a type $\alpha$ equipped with a preorder and a bottom element $\bot$, the filter $f$ is bounded below with respect to the greater-than-or-equal relation $\geq$. That is, there exists an element $b \in \alpha$ such that for all $x$ in some set belonging to $f$, we have $x \geq b$.

OrderIso.isBoundedUnder_le_comp theorem

 [LE α] [LE β] (e : α ≃o β) {l : Filter γ} {u : γ → α} :
  (IsBoundedUnder (· ≤ ·) l fun x => e (u x)) ↔ IsBoundedUnder (· ≤ ·) l u

Full source

@[simp]
theorem _root_.OrderIso.isBoundedUnder_le_comp [LE α] [LE β] (e : α ≃o β) {l : Filter γ}
    {u : γ → α} : (IsBoundedUnder (· ≤ ·) l fun x => e (u x)) ↔ IsBoundedUnder (· ≤ ·) l u :=
  (Function.Surjective.exists e.surjective).trans <|
    exists_congr fun a => by simp only [eventually_map, e.le_iff_le]

Preservation of Boundedness Under Order Isomorphism: $e \circ u$ vs $u$

Informal description

Let $\alpha$ and $\beta$ be preordered types, and let $e : \alpha \simeq_o \beta$ be an order isomorphism. For any filter $l$ on a type $\gamma$ and any function $u : \gamma \to \alpha$, the following are equivalent: 1. The filter $l$ is bounded under the relation $\leq$ with respect to the composition $e \circ u$. 2. The filter $l$ is bounded under the relation $\leq$ with respect to $u$. In other words, the boundedness under $\leq$ is preserved under composition with an order isomorphism.

OrderIso.isBoundedUnder_ge_comp theorem

 [LE α] [LE β] (e : α ≃o β) {l : Filter γ} {u : γ → α} :
  (IsBoundedUnder (· ≥ ·) l fun x => e (u x)) ↔ IsBoundedUnder (· ≥ ·) l u

Full source

@[simp]
theorem _root_.OrderIso.isBoundedUnder_ge_comp [LE α] [LE β] (e : α ≃o β) {l : Filter γ}
    {u : γ → α} : (IsBoundedUnder (· ≥ ·) l fun x => e (u x)) ↔ IsBoundedUnder (· ≥ ·) l u :=
  OrderIso.isBoundedUnder_le_comp e.dual

Preservation of Boundedness Under Order Isomorphism: $e \circ u$ vs $u$ for $\geq$

Informal description

Let $\alpha$ and $\beta$ be preordered types, and let $e : \alpha \simeq_o \beta$ be an order isomorphism. For any filter $l$ on a type $\gamma$ and any function $u : \gamma \to \alpha$, the following are equivalent: 1. The filter $l$ is bounded under the relation $\geq$ with respect to the composition $e \circ u$. 2. The filter $l$ is bounded under the relation $\geq$ with respect to $u$. In other words, the boundedness under $\geq$ is preserved under composition with an order isomorphism.

Filter.isBoundedUnder_le_inv theorem

 [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {l : Filter β} {u : β → α} :
  (IsBoundedUnder (· ≤ ·) l fun x => (u x)⁻¹) ↔ IsBoundedUnder (· ≥ ·) l u

Full source

@[to_additive (attr := simp)]
theorem isBoundedUnder_le_inv [CommGroup α] [PartialOrder α] [IsOrderedMonoid α]
    {l : Filter β} {u : β → α} :
    (IsBoundedUnder (· ≤ ·) l fun x => (u x)⁻¹) ↔ IsBoundedUnder (· ≥ ·) l u :=
  (OrderIso.inv α).isBoundedUnder_ge_comp

Boundedness under inversion: $\leq$-boundedness of $u^{-1}$ vs $\geq$-boundedness of $u$

Informal description

Let $\alpha$ be a commutative group equipped with a partial order such that it forms an ordered monoid. For any filter $l$ on a type $\beta$ and any function $u : \beta \to \alpha$, the following are equivalent: 1. The filter $l$ is bounded under the relation $\leq$ with respect to the function $x \mapsto (u(x))^{-1}$. 2. The filter $l$ is bounded under the relation $\geq$ with respect to $u$.

Filter.isBoundedUnder_ge_inv theorem

 [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {l : Filter β} {u : β → α} :
  (IsBoundedUnder (· ≥ ·) l fun x => (u x)⁻¹) ↔ IsBoundedUnder (· ≤ ·) l u

Full source

@[to_additive (attr := simp)]
theorem isBoundedUnder_ge_inv [CommGroup α] [PartialOrder α] [IsOrderedMonoid α]
    {l : Filter β} {u : β → α} :
    (IsBoundedUnder (· ≥ ·) l fun x => (u x)⁻¹) ↔ IsBoundedUnder (· ≤ ·) l u :=
  (OrderIso.inv α).isBoundedUnder_le_comp

Boundedness under inversion: $\geq$-boundedness of $u^{-1}$ vs $\leq$-boundedness of $u$

Informal description

Let $\alpha$ be a commutative group equipped with a partial order such that it forms an ordered monoid. For any filter $l$ on a type $\beta$ and any function $u : \beta \to \alpha$, the following are equivalent: 1. The filter $l$ is bounded under the relation $\geq$ with respect to the function $x \mapsto (u(x))^{-1}$. 2. The filter $l$ is bounded under the relation $\leq$ with respect to $u$.

Filter.IsBoundedUnder.sup theorem

 [SemilatticeSup α] {f : Filter β} {u v : β → α} :
  f.IsBoundedUnder (· ≤ ·) u → f.IsBoundedUnder (· ≤ ·) v → f.IsBoundedUnder (· ≤ ·) fun a => u a ⊔ v a

Full source

theorem IsBoundedUnder.sup [SemilatticeSup α] {f : Filter β} {u v : β → α} :
    f.IsBoundedUnder (· ≤ ·) u →
      f.IsBoundedUnder (· ≤ ·) v → f.IsBoundedUnder (· ≤ ·) fun a => u a ⊔ v a
  | ⟨bu, (hu : ∀ᶠ x in f, u x ≤ bu)⟩, ⟨bv, (hv : ∀ᶠ x in f, v x ≤ bv)⟩ =>
    ⟨bu ⊔ bv, show ∀ᶠ x in f, u x ⊔ v x ≤ bu ⊔ bv
      by filter_upwards [hu, hv] with _ using sup_le_sup⟩

Boundedness under $\leq$ is preserved by pointwise suprema

Informal description

Let $\alpha$ be a join-semilattice, $f$ a filter on a type $\beta$, and $u, v : \beta \to \alpha$ two functions. If $f$ is bounded under the relation $\leq$ with respect to $u$ and $f$ is bounded under $\leq$ with respect to $v$, then $f$ is bounded under $\leq$ with respect to the pointwise supremum function $a \mapsto u(a) \sqcup v(a)$.

Filter.isBoundedUnder_le_sup theorem

 [SemilatticeSup α] {f : Filter β} {u v : β → α} :
  (f.IsBoundedUnder (· ≤ ·) fun a => u a ⊔ v a) ↔ f.IsBoundedUnder (· ≤ ·) u ∧ f.IsBoundedUnder (· ≤ ·) v

Full source

@[simp]
theorem isBoundedUnder_le_sup [SemilatticeSup α] {f : Filter β} {u v : β → α} :
    (f.IsBoundedUnder (· ≤ ·) fun a => u a ⊔ v a) ↔
      f.IsBoundedUnder (· ≤ ·) u ∧ f.IsBoundedUnder (· ≤ ·) v :=
  ⟨fun h =>
    ⟨h.mono_le <| Eventually.of_forall fun _ => le_sup_left,
      h.mono_le <| Eventually.of_forall fun _ => le_sup_right⟩,
    fun h => h.1.sup h.2⟩

Boundedness of Pointwise Supremum under $\leq$ is Equivalent to Boundedness of Both Functions

Informal description

Let $\alpha$ be a join-semilattice, $f$ a filter on a type $\beta$, and $u, v : \beta \to \alpha$ two functions. The filter $f$ is bounded under the relation $\leq$ with respect to the pointwise supremum function $a \mapsto u(a) \sqcup v(a)$ if and only if $f$ is bounded under $\leq$ with respect to both $u$ and $v$.

Filter.IsBoundedUnder.inf theorem

 [SemilatticeInf α] {f : Filter β} {u v : β → α} :
  f.IsBoundedUnder (· ≥ ·) u → f.IsBoundedUnder (· ≥ ·) v → f.IsBoundedUnder (· ≥ ·) fun a => u a ⊓ v a

Full source

theorem IsBoundedUnder.inf [SemilatticeInf α] {f : Filter β} {u v : β → α} :
    f.IsBoundedUnder (· ≥ ·) u →
      f.IsBoundedUnder (· ≥ ·) v → f.IsBoundedUnder (· ≥ ·) fun a => u a ⊓ v a :=
  IsBoundedUnder.sup (α := αᵒᵈ)

Boundedness under $\geq$ is preserved by pointwise infima

Informal description

Let $\alpha$ be a meet-semilattice, $f$ a filter on a type $\beta$, and $u, v : \beta \to \alpha$ two functions. If $f$ is bounded under the relation $\geq$ with respect to $u$ and $f$ is bounded under $\geq$ with respect to $v$, then $f$ is bounded under $\geq$ with respect to the pointwise infimum function $a \mapsto u(a) \sqcap v(a)$.

Filter.isBoundedUnder_ge_inf theorem

 [SemilatticeInf α] {f : Filter β} {u v : β → α} :
  (f.IsBoundedUnder (· ≥ ·) fun a => u a ⊓ v a) ↔ f.IsBoundedUnder (· ≥ ·) u ∧ f.IsBoundedUnder (· ≥ ·) v

Full source

@[simp]
theorem isBoundedUnder_ge_inf [SemilatticeInf α] {f : Filter β} {u v : β → α} :
    (f.IsBoundedUnder (· ≥ ·) fun a => u a ⊓ v a) ↔
      f.IsBoundedUnder (· ≥ ·) u ∧ f.IsBoundedUnder (· ≥ ·) v :=
  isBoundedUnder_le_sup (α := αᵒᵈ)

Boundedness of Pointwise Infimum under $\geq$ is Equivalent to Boundedness of Both Functions

Informal description

Let $\alpha$ be a meet-semilattice, $f$ a filter on a type $\beta$, and $u, v : \beta \to \alpha$ two functions. The filter $f$ is bounded under the relation $\geq$ with respect to the pointwise infimum function $a \mapsto u(a) \sqcap v(a)$ if and only if $f$ is bounded under $\geq$ with respect to both $u$ and $v$.

Filter.isBoundedUnder_le_abs theorem

 [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {f : Filter β} {u : β → α} :
  (f.IsBoundedUnder (· ≤ ·) fun a => |u a|) ↔ f.IsBoundedUnder (· ≤ ·) u ∧ f.IsBoundedUnder (· ≥ ·) u

Full source

theorem isBoundedUnder_le_abs [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]
    {f : Filter β} {u : β → α} :
    (f.IsBoundedUnder (· ≤ ·) fun a => |u a|) ↔
      f.IsBoundedUnder (· ≤ ·) u ∧ f.IsBoundedUnder (· ≥ ·) u :=
  isBoundedUnder_le_sup.trans <| and_congr Iff.rfl isBoundedUnder_le_neg

Boundedness of Absolute Value under $\leq$ is Equivalent to Boundedness from Above and Below

Informal description

Let $\alpha$ be an additively commutative group with a linear order and an ordered additive monoid structure, and let $f$ be a filter on a type $\beta$. For a function $u : \beta \to \alpha$, the filter $f$ is bounded under the relation $\leq$ with respect to the absolute value function $a \mapsto |u(a)|$ if and only if $f$ is bounded under $\leq$ with respect to $u$ and $f$ is bounded under $\geq$ with respect to $u$.

Filter.tacticIsBoundedDefault definition

: Lean.ParserDescr✝

Full source

macromacro "isBoundedDefault" : tactic =>
  `(tactic| first
    | apply isCobounded_le_of_bot
    | apply isCobounded_ge_of_top
    | apply isBounded_le_of_top
    | apply isBounded_ge_of_bot
    | assumption)

Automatic boundedness tactic for filters in complete lattices

Informal description

The tactic `isBoundedDefault` automatically fills in boundedness or coboundedness proofs for filters in complete lattices. It attempts to apply standard boundedness lemmas (like `isCobounded_le_of_bot`, `isCobounded_ge_of_top`, etc.) or uses the given assumption if available.

Monotone.isBoundedUnder_le_comp_iff theorem

 [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g)
  (hg' : Tendsto g atTop atTop) : IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f

Full source

theorem Monotone.isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
    {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Tendsto g atTop atTop) :
    IsBoundedUnderIsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f := by
  refine ⟨?_, fun h => h.isBoundedUnder (α := β) hg⟩
  rintro ⟨c, hc⟩; rw [eventually_map] at hc
  obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)
  exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_le hx⟩

Monotone Composition Preserves Boundedness Above: $g \circ f$ is bounded above iff $f$ is bounded above

Informal description

Let $\beta$ be a nonempty linearly ordered type, $\gamma$ a preorder with no maximal elements, $g : \beta \to \gamma$ a monotone function, $f : \alpha \to \beta$ a function, and $l$ a filter on $\alpha$. If $g$ tends to infinity as its input tends to infinity (i.e., $\lim_{x \to \infty} g(x) = \infty$), then the following are equivalent: 1. The composition $g \circ f$ is bounded above under $l$ with respect to the relation $\leq$. 2. The function $f$ is bounded above under $l$ with respect to the relation $\leq$.

Monotone.isBoundedUnder_ge_comp_iff theorem

 [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g)
  (hg' : Tendsto g atBot atBot) : IsBoundedUnder (· ≥ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f

Full source

theorem Monotone.isBoundedUnder_ge_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
    {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Tendsto g atBot atBot) :
    IsBoundedUnderIsBoundedUnder (· ≥ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f :=
  hg.dual.isBoundedUnder_le_comp_iff hg'

Monotone Composition Preserves Boundedness Below: $g \circ f$ is bounded below iff $f$ is bounded below

Informal description

Let $\beta$ be a nonempty linearly ordered type, $\gamma$ a preorder with no minimal elements, $g : \beta \to \gamma$ a monotone function, $f : \alpha \to \beta$ a function, and $l$ a filter on $\alpha$. If $g$ tends to negative infinity as its input tends to negative infinity (i.e., $\lim_{x \to -\infty} g(x) = -\infty$), then the following are equivalent: 1. The composition $g \circ f$ is bounded below under $l$ with respect to the relation $\geq$. 2. The function $f$ is bounded below under $l$ with respect to the relation $\geq$.

Antitone.isBoundedUnder_le_comp_iff theorem

 [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g)
  (hg' : Tendsto g atBot atTop) : IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f

Full source

theorem Antitone.isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
    {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Tendsto g atBot atTop) :
    IsBoundedUnderIsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f :=
  hg.dual_right.isBoundedUnder_ge_comp_iff hg'

Antitone Composition Boundedness Equivalence: $g \circ f$ bounded above iff $f$ bounded below

Informal description

Let $\beta$ be a nonempty linearly ordered type, $\gamma$ a preorder with no maximal elements, $g : \beta \to \gamma$ an antitone function, $f : \alpha \to \beta$ a function, and $l$ a filter on $\alpha$. If $g$ tends to infinity as its input tends to negative infinity (i.e., $\lim_{x \to -\infty} g(x) = \infty$), then the following are equivalent: 1. The composition $g \circ f$ is bounded above under $l$ with respect to the relation $\leq$. 2. The function $f$ is bounded below under $l$ with respect to the relation $\geq$.

Antitone.isBoundedUnder_ge_comp_iff theorem

 [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ] {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g)
  (hg' : Tendsto g atTop atBot) : IsBoundedUnder (· ≥ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f

Full source

theorem Antitone.isBoundedUnder_ge_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
    {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Tendsto g atTop atBot) :
    IsBoundedUnderIsBoundedUnder (· ≥ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f :=
  hg.dual_right.isBoundedUnder_le_comp_iff hg'

Antitone Composition Boundedness Equivalence: $g \circ f$ bounded below iff $f$ bounded above

Informal description

Let $\beta$ be a nonempty linearly ordered type, $\gamma$ a preorder with no minimal elements, $g : \beta \to \gamma$ an antitone function, $f : \alpha \to \beta$ a function, and $l$ a filter on $\alpha$. If $g$ tends to negative infinity as its input tends to infinity (i.e., $\lim_{x \to \infty} g(x) = -\infty$), then the following are equivalent: 1. The composition $g \circ f$ is bounded below under $l$ with respect to the relation $\geq$. 2. The function $f$ is bounded above under $l$ with respect to the relation $\leq$.

isCoboundedUnder_le_max theorem

 [LinearOrder β] {f : Filter α} {u v : α → β} (h : f.IsCoboundedUnder (· ≤ ·) u ∨ f.IsCoboundedUnder (· ≤ ·) v) :
  f.IsCoboundedUnder (· ≤ ·) (fun a ↦ max (u a) (v a))

Full source

theorem isCoboundedUnder_le_max [LinearOrder β] {f : Filter α} {u v : α → β}
    (h : f.IsCoboundedUnder (· ≤ ·) u ∨ f.IsCoboundedUnder (· ≤ ·) v) :
    f.IsCoboundedUnder (· ≤ ·) (fun a ↦ max (u a) (v a)) := by
  rcases h with (h' | h') <;>
  · rcases h' with ⟨b, hb⟩
    use b
    intro c hc
    apply hb c
    rw [eventually_map] at hc ⊢
    refine hc.mono (fun _ ↦ ?_)
    simp +contextual only [implies_true, max_le_iff, and_imp]

Coboundedness under pointwise maximum with respect to $\leq$

Informal description

Let $\beta$ be a linearly ordered type, $f$ a filter on a type $\alpha$, and $u, v : \alpha \to \beta$ functions. If $f$ is cobounded under $u$ or $f$ is cobounded under $v$ with respect to the relation $\leq$, then $f$ is cobounded under the pointwise maximum function $\lambda a, \max(u(a), v(a))$ with respect to $\leq$.

isBoundedUnder_le_finset_sup' theorem

 [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty)
  (h : ∀ i ∈ s, f.IsBoundedUnder (· ≤ ·) (F i)) : f.IsBoundedUnder (· ≤ ·) (fun a ↦ sup' s hs (fun i ↦ F i a))

Full source

theorem isBoundedUnder_le_finset_sup' [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β}
    {s : Finset ι} (hs : s.Nonempty) (h : ∀ i ∈ s, f.IsBoundedUnder (· ≤ ·) (F i)) :
    f.IsBoundedUnder (· ≤ ·) (fun a ↦ sup' s hs (fun i ↦ F i a)) := by
  choose! m hm using h
  use sup' s hs m
  simp only [eventually_map] at hm ⊢
  rw [← eventually_all_finset s] at hm
  refine hm.mono fun a h ↦ ?_
  simp only [Finset.sup'_apply, sup'_le_iff]
  exact fun i i_s ↦ le_trans (h i i_s) (le_sup' m i_s)

Boundedness under finite supremum with respect to $\leq$

Informal description

Let $\beta$ be a nonempty linearly ordered type, $f$ a filter on a type $\alpha$, and $F : \iota \to \alpha \to \beta$ a family of functions. Given a nonempty finite set $s \subseteq \iota$ such that for each $i \in s$, the filter $f$ is bounded under $F(i)$ with respect to the $\leq$ relation, then $f$ is bounded under the pointwise supremum $\sup'_{i \in s} F(i)$ with respect to $\leq$.

isCoboundedUnder_le_finset_sup' theorem

 [LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty)
  (h : ∃ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i)) : f.IsCoboundedUnder (· ≤ ·) (fun a ↦ sup' s hs (fun i ↦ F i a))

Full source

theorem isCoboundedUnder_le_finset_sup' [LinearOrder β] {f : Filter α} {F : ι → α → β}
    {s : Finset ι} (hs : s.Nonempty) (h : ∃ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i)) :
    f.IsCoboundedUnder (· ≤ ·) (fun a ↦ sup' s hs (fun i ↦ F i a)) := by
  rcases h with ⟨i, i_s, b, hb⟩
  use b
  refine fun c hc ↦ hb c ?_
  rw [eventually_map] at hc ⊢
  refine hc.mono fun a h ↦ ?_
  simp only [Finset.sup'_apply, sup'_le_iff] at h ⊢
  exact h i i_s

Coboundedness under finite supremum with respect to $\leq$

Informal description

Let $\beta$ be a linearly ordered type, $f$ a filter on a type $\alpha$, and $F : \iota \to \alpha \to \beta$ a family of functions. Given a nonempty finite set $s \subseteq \iota$ and an index $i \in s$ such that $f$ is cobounded under $F(i)$ with respect to the $\leq$ relation, then $f$ is cobounded under the pointwise supremum $\sup'_{i \in s} F(i)$ with respect to $\leq$.

isBoundedUnder_le_finset_sup theorem

 [LinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β} {s : Finset ι}
  (h : ∀ i ∈ s, f.IsBoundedUnder (· ≤ ·) (F i)) : f.IsBoundedUnder (· ≤ ·) (fun a ↦ sup s (fun i ↦ F i a))

Full source

theorem isBoundedUnder_le_finset_sup [LinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β}
    {s : Finset ι} (h : ∀ i ∈ s, f.IsBoundedUnder (· ≤ ·) (F i)) :
    f.IsBoundedUnder (· ≤ ·) (fun a ↦ sup s (fun i ↦ F i a)) := by
  choose! m hm using h
  use sup s m
  simp only [eventually_map] at hm ⊢
  rw [← eventually_all_finset s] at hm
  exact hm.mono fun _ h ↦ sup_mono_fun h

Boundedness under finite supremum with respect to $\leq$ in a filter

Informal description

Let $\beta$ be a linearly ordered type with a bottom element $\bot$, $f$ a filter on a type $\alpha$, and $F : \iota \to \alpha \to \beta$ a family of functions. For any finite set $s \subseteq \iota$, if for each $i \in s$ the filter $f$ is bounded under $F(i)$ with respect to the $\leq$ relation, then $f$ is bounded under the pointwise supremum $\sup_{i \in s} F(i, \cdot)$ with respect to $\leq$.

isBoundedUnder_ge_finset_inf' theorem

 [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty)
  (h : ∀ i ∈ s, f.IsBoundedUnder (· ≥ ·) (F i)) : f.IsBoundedUnder (· ≥ ·) (fun a ↦ inf' s hs (fun i ↦ F i a))

Full source

theorem isBoundedUnder_ge_finset_inf' [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β}
    {s : Finset ι} (hs : s.Nonempty) (h : ∀ i ∈ s, f.IsBoundedUnder (· ≥ ·) (F i)) :
    f.IsBoundedUnder (· ≥ ·) (fun a ↦ inf' s hs (fun i ↦ F i a)) :=
  isBoundedUnder_le_finset_sup' (β := βᵒᵈ) hs h

Boundedness under finite infimum with respect to $\geq$

Informal description

Let $\beta$ be a nonempty linearly ordered type, $f$ a filter on a type $\alpha$, and $F : \iota \to \alpha \to \beta$ a family of functions. Given a nonempty finite set $s \subseteq \iota$ such that for each $i \in s$, the filter $f$ is bounded under $F(i)$ with respect to the $\geq$ relation, then $f$ is bounded under the pointwise infimum $\inf'_{i \in s} F(i)$ with respect to $\geq$.

isCoboundedUnder_ge_finset_inf' theorem

 [LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty)
  (h : ∃ i ∈ s, f.IsCoboundedUnder (· ≥ ·) (F i)) : f.IsCoboundedUnder (· ≥ ·) (fun a ↦ inf' s hs (fun i ↦ F i a))

Full source

theorem isCoboundedUnder_ge_finset_inf' [LinearOrder β] {f : Filter α} {F : ι → α → β}
    {s : Finset ι} (hs : s.Nonempty) (h : ∃ i ∈ s, f.IsCoboundedUnder (· ≥ ·) (F i)) :
    f.IsCoboundedUnder (· ≥ ·) (fun a ↦ inf' s hs (fun i ↦ F i a)) :=
  isCoboundedUnder_le_finset_sup' (β := βᵒᵈ) hs h

Coboundedness under finite infimum with respect to $\geq$

Informal description

Let $\beta$ be a linearly ordered type, $f$ a filter on a type $\alpha$, and $F : \iota \to \alpha \to \beta$ a family of functions. Given a nonempty finite set $s \subseteq \iota$ and an index $i \in s$ such that $f$ is cobounded under $F(i)$ with respect to the $\geq$ relation, then $f$ is cobounded under the pointwise infimum $\inf'_{i \in s} F(i)$ with respect to $\geq$.

isBoundedUnder_ge_finset_inf theorem

 [LinearOrder β] [OrderTop β] {f : Filter α} {F : ι → α → β} {s : Finset ι}
  (h : ∀ i ∈ s, f.IsBoundedUnder (· ≥ ·) (F i)) : f.IsBoundedUnder (· ≥ ·) (fun a ↦ inf s (fun i ↦ F i a))

Full source

theorem isBoundedUnder_ge_finset_inf [LinearOrder β] [OrderTop β] {f : Filter α} {F : ι → α → β}
    {s : Finset ι} (h : ∀ i ∈ s, f.IsBoundedUnder (· ≥ ·) (F i)) :
    f.IsBoundedUnder (· ≥ ·) (fun a ↦ inf s (fun i ↦ F i a)) :=
  isBoundedUnder_le_finset_sup (β := βᵒᵈ) h

Boundedness under finite infimum with respect to $\geq$ in a filter

Informal description

Let $\beta$ be a linearly ordered type with a greatest element $\top$, $f$ a filter on a type $\alpha$, and $F : \iota \to \alpha \to \beta$ a family of functions. For any finite set $s \subseteq \iota$, if for each $i \in s$ the filter $f$ is bounded under $F(i)$ with respect to the $\geq$ relation, then $f$ is bounded under the pointwise infimum $\inf_{i \in s} F(i, \cdot)$ with respect to $\geq$.

Monotone.frequently_ge_map_of_frequently_ge theorem

{f : R → S} (f_incr : Monotone f) {l : R} (freq_ge : ∃ᶠ x in F, l ≤ x) : ∃ᶠ x' in F.map f, f l ≤ x'

Full source

lemma Monotone.frequently_ge_map_of_frequently_ge {f : R → S} (f_incr : Monotone f)
    {l : R} (freq_ge : ∃ᶠ x in F, l ≤ x) :
    ∃ᶠ x' in F.map f, f l ≤ x' := by
  refine fun ev ↦ freq_ge ?_
  simp only [not_le, not_lt] at ev freq_ge ⊢
  filter_upwards [ev] with z hz
  by_contra con
  exact lt_irrefl (f l) <| lt_of_le_of_lt (f_incr <| not_lt.mp con) hz

Frequent Preservation of Lower Bounds under Monotone Maps

Informal description

Let $R$ and $S$ be linearly ordered types, and let $f : R \to S$ be a monotone function. Given a filter $F$ on $R$ and an element $l \in R$, if the set $\{x \in R \mid l \leq x\}$ is frequently in $F$ (i.e., $\existsᶠ x \text{ in } F, l \leq x$), then the set $\{x' \in S \mid f(l) \leq x'\}$ is frequently in the image filter $F.map\, f$ (i.e., $\existsᶠ x' \text{ in } F.map\, f, f(l) \leq x'$).

Monotone.frequently_le_map_of_frequently_le theorem

{f : R → S} (f_incr : Monotone f) {u : R} (freq_le : ∃ᶠ x in F, x ≤ u) : ∃ᶠ y in F.map f, y ≤ f u

Full source

lemma Monotone.frequently_le_map_of_frequently_le {f : R → S} (f_incr : Monotone f)
    {u : R} (freq_le : ∃ᶠ x in F, x ≤ u) :
    ∃ᶠ y in F.map f, y ≤ f u := by
  refine fun ev ↦ freq_le ?_
  simp only [not_le, not_lt] at ev freq_le ⊢
  filter_upwards [ev] with z hz
  by_contra con
  apply lt_irrefl (f u) <| lt_of_lt_of_le hz <| f_incr (not_lt.mp con)

Frequent Preservation of Upper Bounds under Monotone Maps

Informal description

Let $F$ be a filter on a type $R$, $f : R \to S$ a monotone function, and $u \in R$. If the set $\{x \in R \mid x \leq u\}$ is frequently in $F$ (i.e., intersects every set in $F$), then the set $\{y \in S \mid y \leq f(u)\}$ is frequently in the image filter $F.map\, f$.

Antitone.frequently_le_map_of_frequently_ge theorem

{f : R → S} (f_decr : Antitone f) {l : R} (frbdd : ∃ᶠ x in F, l ≤ x) : ∃ᶠ y in F.map f, y ≤ f l

Full source

lemma Antitone.frequently_le_map_of_frequently_ge {f : R → S} (f_decr : Antitone f)
    {l : R} (frbdd : ∃ᶠ x in F, l ≤ x) :
    ∃ᶠ y in F.map f, y ≤ f l :=
  Monotone.frequently_ge_map_of_frequently_ge (S := Sᵒᵈ) f_decr frbdd

Frequent Preservation of Upper Bounds under Antitone Maps

Informal description

Let $R$ and $S$ be linearly ordered types, and let $f : R \to S$ be an antitone function. Given a filter $F$ on $R$ and an element $l \in R$, if the set $\{x \in R \mid l \leq x\}$ is frequently in $F$ (i.e., $\existsᶠ x \text{ in } F, l \leq x$), then the set $\{y \in S \mid y \leq f(l)\}$ is frequently in the image filter $F.map\, f$ (i.e., $\existsᶠ y \text{ in } F.map\, f, y \leq f(l)$).

Antitone.frequently_ge_map_of_frequently_le theorem

{f : R → S} (f_decr : Antitone f) {u : R} (frbdd : ∃ᶠ x in F, x ≤ u) : ∃ᶠ y in F.map f, f u ≤ y

Full source

lemma Antitone.frequently_ge_map_of_frequently_le {f : R → S} (f_decr : Antitone f)
    {u : R} (frbdd : ∃ᶠ x in F, x ≤ u) :
    ∃ᶠ y in F.map f, f u ≤ y :=
  Monotone.frequently_le_map_of_frequently_le (S := Sᵒᵈ) f_decr frbdd

Frequent Preservation of Lower Bounds under Antitone Maps

Informal description

Let $F$ be a filter on a type $R$, $f : R \to S$ an antitone function, and $u \in R$. If the set $\{x \in R \mid x \leq u\}$ is frequently in $F$ (i.e., intersects every set in $F$), then the set $\{y \in S \mid f(u) \leq y\}$ is frequently in the image filter $F.map\, f$.

Monotone.isCoboundedUnder_le_of_isCobounded theorem

{f : R → S} (f_incr : Monotone f) [NeBot F] (cobdd : IsCobounded (· ≤ ·) F) : F.IsCoboundedUnder (· ≤ ·) f

Full source

lemma Monotone.isCoboundedUnder_le_of_isCobounded {f : R → S} (f_incr : Monotone f)
    [NeBot F] (cobdd : IsCobounded (· ≤ ·) F) :
    F.IsCoboundedUnder (· ≤ ·) f := by
  obtain ⟨l, hl⟩ := IsCobounded.frequently_ge cobdd
  exact IsCobounded.of_frequently_ge <| f_incr.frequently_ge_map_of_frequently_ge hl

Monotone Functions Preserve Coboundedness Under $\leq$

Informal description

Let $R$ and $S$ be linearly ordered types, $F$ a non-trivial filter on $R$, and $f : R \to S$ a monotone function. If $F$ is cobounded with respect to the relation $\leq$, then the filter $F$ is cobounded under $f$ with respect to $\leq$ (i.e., $F.\text{IsCoboundedUnder}\, (\leq)\, f$ holds).

Monotone.isCoboundedUnder_ge_of_isCobounded theorem

{f : R → S} (f_incr : Monotone f) [NeBot F] (cobdd : IsCobounded (· ≥ ·) F) : F.IsCoboundedUnder (· ≥ ·) f

Full source

lemma Monotone.isCoboundedUnder_ge_of_isCobounded {f : R → S} (f_incr : Monotone f)
    [NeBot F] (cobdd : IsCobounded (· ≥ ·) F) :
    F.IsCoboundedUnder (· ≥ ·) f :=
  Monotone.isCoboundedUnder_le_of_isCobounded (R := Rᵒᵈ) (S := Sᵒᵈ) f_incr.dual cobdd

Monotone Functions Preserve Coboundedness Under $\geq$

Informal description

Let $R$ and $S$ be linearly ordered types, $F$ a non-trivial filter on $R$, and $f : R \to S$ a monotone function. If $F$ is cobounded with respect to the relation $\geq$, then the filter $F$ is cobounded under $f$ with respect to $\geq$ (i.e., $F.\text{IsCoboundedUnder}\, (\geq)\, f$ holds).

Antitone.isCoboundedUnder_le_of_isCobounded theorem

{f : R → S} (f_decr : Antitone f) [NeBot F] (cobdd : IsCobounded (· ≥ ·) F) : F.IsCoboundedUnder (· ≤ ·) f

Full source

lemma Antitone.isCoboundedUnder_le_of_isCobounded {f : R → S} (f_decr : Antitone f)
    [NeBot F] (cobdd : IsCobounded (· ≥ ·) F) :
    F.IsCoboundedUnder (· ≤ ·) f :=
  Monotone.isCoboundedUnder_le_of_isCobounded (R := Rᵒᵈ) f_decr.dual cobdd

Antitone Functions Preserve Coboundedness Under $\leq$ from $\geq$

Informal description

Let $R$ and $S$ be linearly ordered types, $F$ a non-trivial filter on $R$, and $f : R \to S$ an antitone function. If $F$ is cobounded with respect to the relation $\geq$, then the filter $F$ is cobounded under $f$ with respect to $\leq$ (i.e., $F.\text{IsCoboundedUnder}\, (\leq)\, f$ holds).

Antitone.isCoboundedUnder_ge_of_isCobounded theorem

{f : R → S} (f_decr : Antitone f) [NeBot F] (cobdd : IsCobounded (· ≤ ·) F) : F.IsCoboundedUnder (· ≥ ·) f

Full source

lemma Antitone.isCoboundedUnder_ge_of_isCobounded {f : R → S} (f_decr : Antitone f)
    [NeBot F] (cobdd : IsCobounded (· ≤ ·) F) :
    F.IsCoboundedUnder (· ≥ ·) f :=
  Monotone.isCoboundedUnder_le_of_isCobounded (S := Sᵒᵈ) f_decr cobdd

Antitone Functions Preserve Coboundedness Under $\geq$

Informal description

Let $R$ and $S$ be linearly ordered types, $F$ a non-trivial filter on $R$, and $f : R \to S$ an antitone function. If $F$ is cobounded with respect to the relation $\leq$, then the filter $F$ is cobounded under $f$ with respect to $\geq$ (i.e., $F.\text{IsCoboundedUnder}\, (\geq)\, f$ holds).