Mathlib.Order.Filter.AtTopBot.Tendsto

Filter.not_tendsto_const_atTop theorem

[Preorder α] [NoTopOrder α] (x : α) (l : Filter β) [l.NeBot] : ¬Tendsto (fun _ => x) l atTop

Full source

theorem not_tendsto_const_atTop [Preorder α] [NoTopOrder α] (x : α) (l : Filter β) [l.NeBot] :
    ¬Tendsto (fun _ => x) l atTop :=
  tendsto_const_pure.not_tendsto (disjoint_pure_atTop x)

Non-Convergence of Constant Functions to Infinity in No-Top Orders

Informal description

Let $\alpha$ be a preorder with no top element, and let $\beta$ be any type. For any element $x \in \alpha$ and any nontrivial filter $l$ on $\beta$, the constant function $f(y) = x$ does not tend to infinity in $l$ (i.e., $\lim_{y \to l} f(y) \neq \infty$).

Filter.not_tendsto_const_atBot theorem

[Preorder α] [NoBotOrder α] (x : α) (l : Filter β) [l.NeBot] : ¬Tendsto (fun _ => x) l atBot

Full source

theorem not_tendsto_const_atBot [Preorder α] [NoBotOrder α] (x : α) (l : Filter β) [l.NeBot] :
    ¬Tendsto (fun _ => x) l atBot :=
  tendsto_const_pure.not_tendsto (disjoint_pure_atBot x)

Non-Convergence of Constant Functions to Negative Infinity in No-Bottom Orders

Informal description

Let $\alpha$ be a preorder with no bottom element, and let $\beta$ be any type. For any element $x \in \alpha$ and any nontrivial filter $l$ on $\beta$, the constant function $f(y) = x$ does not tend to negative infinity in $l$ (i.e., $\lim_{y \to l} f(y) \neq -\infty$).

Filter.Tendsto.eventually_gt_atTop theorem

 [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, c < f x

Full source

protected theorem Tendsto.eventually_gt_atTop [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α}
    (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, c < f x :=
  hf.eventually (eventually_gt_atTop c)

Eventual Strict Lower Bound for Functions Tending to Infinity

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder and no top element. Given a function $f : \alpha \to \beta$ and a filter $l$ on $\alpha$, if $f$ tends to infinity in $l$ (i.e., $\lim_{x \to l} f(x) = \infty$), then for any constant $c \in \beta$, eventually for all $x$ in $l$, we have $c < f(x)$.

Filter.Tendsto.eventually_ge_atTop theorem

[Preorder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, c ≤ f x

Full source

protected theorem Tendsto.eventually_ge_atTop [Preorder β] {f : α → β} {l : Filter α}
    (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, c ≤ f x :=
  hf.eventually (eventually_ge_atTop c)

Eventual Lower Bound for Functions Tending to Infinity

Informal description

Let $\alpha$ and $\beta$ be preorders, $f : \alpha \to \beta$ a function, and $l$ a filter on $\alpha$. If $f$ tends to $\infty$ in $l$ (i.e., $\text{Tendsto}\, f\, l\, \text{atTop}$), then for any $c \in \beta$, eventually for all $x$ in $l$, we have $c \leq f(x)$.

Filter.Tendsto.eventually_ne_atTop theorem

 [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, f x ≠ c

Full source

protected theorem Tendsto.eventually_ne_atTop [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α}
    (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, f x ≠ c :=
  hf.eventually (eventually_ne_atTop c)

Eventual Distinctness from Constant for Functions Tending to Infinity

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is equipped with a preorder and has no top element. Given a function $f : \alpha \to \beta$ and a filter $l$ on $\alpha$, if $f$ tends to infinity in $l$ (i.e., $\lim_{x \to l} f(x) = \infty$), then for any constant $c \in \beta$, eventually for all $x$ in $l$, we have $f(x) \neq c$.

Filter.Tendsto.eventually_ne_atTop' theorem

 [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop) (c : α) : ∀ᶠ x in l, x ≠ c

Full source

protected theorem Tendsto.eventually_ne_atTop' [Preorder β] [NoTopOrder β] {f : α → β}
    {l : Filter α} (hf : Tendsto f l atTop) (c : α) : ∀ᶠ x in l, x ≠ c :=
  (hf.eventually_ne_atTop (f c)).mono fun _ => ne_of_apply_ne f

Eventual Distinctness from Constant in Domain for Functions Tending to Infinity

Informal description

Let $\alpha$ and $\beta$ be types, where $\beta$ is equipped with a preorder and has no top element. Given a function $f : \alpha \to \beta$ and a filter $l$ on $\alpha$, if $f$ tends to infinity in $l$ (i.e., $\lim_{x \to l} f(x) = \infty$), then for any constant $c \in \alpha$, eventually for all $x$ in $l$, we have $x \neq c$.

Filter.Tendsto.eventually_lt_atBot theorem

 [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x < c

Full source

protected theorem Tendsto.eventually_lt_atBot [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α}
    (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x < c :=
  hf.eventually (eventually_lt_atBot c)

Eventual Strict Lower Bound for Functions Tending to Negative Infinity

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder and no bottom element. Given a function $f : \alpha \to \beta$ and a filter $l$ on $\alpha$, if $f$ tends to $-\infty$ (i.e., $\lim_{x \to l} f(x) = -\infty$), then for any $c \in \beta$, the strict inequality $f(x) < c$ holds eventually for $x$ in $l$.

Filter.Tendsto.eventually_le_atBot theorem

[Preorder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x ≤ c

Full source

protected theorem Tendsto.eventually_le_atBot [Preorder β] {f : α → β} {l : Filter α}
    (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x ≤ c :=
  hf.eventually (eventually_le_atBot c)

Eventual Upper Bound for Functions Tending to Negative Infinity

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder. Given a function $f : \alpha \to \beta$ and a filter $l$ on $\alpha$, if $f$ tends to $-\infty$ (i.e., $\text{Tendsto}\, f\, l\, \text{atBot}$), then for any $c \in \beta$, the inequality $f(x) \leq c$ holds eventually for $x$ in $l$.

Filter.Tendsto.eventually_ne_atBot theorem

 [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x ≠ c

Full source

protected theorem Tendsto.eventually_ne_atBot [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α}
    (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x ≠ c :=
  hf.eventually (eventually_ne_atBot c)

Eventual Non-Equality for Functions Tending to Negative Infinity

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder and no bottom element. Given a function $f : \alpha \to \beta$ and a filter $l$ on $\alpha$, if $f$ tends to $-\infty$ (i.e., $\lim_{x \to l} f(x) = -\infty$), then for any $c \in \beta$, the inequality $f(x) \neq c$ holds eventually for $x$ in $l$.

Filter.OrderTop.atTop_eq theorem

(α) [PartialOrder α] [OrderTop α] : (atTop : Filter α) = pure ⊤

Full source

theorem OrderTop.atTop_eq (α) [PartialOrder α] [OrderTop α] : (atTop : Filter α) = pure ⊤ := by
  rw [isTop_top.atTop_eq, Ici_top, principal_singleton]

Characterization of `atTop` Filter for Partial Order with Top Element: $\text{atTop} = \{\top\}$

Informal description

For a partially ordered set $\alpha$ with a greatest element $\top$, the filter `atTop` is equal to the principal filter generated by $\{\top\}$.

Filter.OrderBot.atBot_eq theorem

(α) [PartialOrder α] [OrderBot α] : (atBot : Filter α) = pure ⊥

Full source

theorem OrderBot.atBot_eq (α) [PartialOrder α] [OrderBot α] : (atBot : Filter α) = pure ⊥ :=
  @OrderTop.atTop_eq αᵒᵈ _ _

Characterization of `atBot` Filter for Partial Order with Bottom Element: $\text{atBot} = \{\bot\}$

Informal description

For a partially ordered set $\alpha$ with a least element $\bot$, the filter `atBot` is equal to the principal filter generated by $\{\bot\}$.

Filter.tendsto_atTop_pure theorem

[PartialOrder α] [OrderTop α] (f : α → β) : Tendsto f atTop (pure <| f ⊤)

Full source

theorem tendsto_atTop_pure [PartialOrder α] [OrderTop α] (f : α → β) :
    Tendsto f atTop (pure <| f ⊤) :=
  (OrderTop.atTop_eq α).symm ▸ tendsto_pure_pure _ _

Limit at Top for Functions on Ordered Sets with Top Element: $f \to f(\top)$ at $\top$

Informal description

For a function $f$ from a partially ordered set $\alpha$ with a greatest element $\top$ to a type $\beta$, the limit of $f$ at $\mathrm{atTop}$ (the filter representing positive infinity) is the principal filter generated by $f(\top)$. In other words, $f$ tends to $f(\top)$ as the input tends to $\top$.

Filter.tendsto_atBot_pure theorem

[PartialOrder α] [OrderBot α] (f : α → β) : Tendsto f atBot (pure <| f ⊥)

Full source

theorem tendsto_atBot_pure [PartialOrder α] [OrderBot α] (f : α → β) :
    Tendsto f atBot (pure <| f ⊥) :=
  @tendsto_atTop_pure αᵒᵈ _ _ _ _

Limit at Bottom for Functions on Ordered Sets with Bottom Element: $f \to f(\bot)$ at $\bot$

Informal description

For a function $f$ from a partially ordered set $\alpha$ with a least element $\bot$ to a type $\beta$, the limit of $f$ at $\mathrm{atBot}$ (the filter representing negative infinity) is the principal filter generated by $f(\bot)$. In other words, $f$ tends to $f(\bot)$ as the input tends to $\bot$.

Filter.tendsto_atTop theorem

[Preorder β] {m : α → β} {f : Filter α} : Tendsto m f atTop ↔ ∀ b, ∀ᶠ a in f, b ≤ m a

Full source

theorem tendsto_atTop [Preorder β] {m : α → β} {f : Filter α} :
    TendstoTendsto m f atTop ↔ ∀ b, ∀ᶠ a in f, b ≤ m a := by
  simp only [atTop, tendsto_iInf, tendsto_principal, mem_Ici]

Characterization of Tendency to Positive Infinity via Filters

Informal description

For a function $m : \alpha \to \beta$ between preorders and a filter $f$ on $\alpha$, the function $m$ tends to $\mathrm{atTop}$ (the filter representing the limit at positive infinity in $\beta$) with respect to $f$ if and only if for every element $b \in \beta$, the set $\{a \in \alpha \mid b \leq m a\}$ is eventually in $f$.

Filter.tendsto_atBot theorem

[Preorder β] {m : α → β} {f : Filter α} : Tendsto m f atBot ↔ ∀ b, ∀ᶠ a in f, m a ≤ b

Full source

theorem tendsto_atBot [Preorder β] {m : α → β} {f : Filter α} :
    TendstoTendsto m f atBot ↔ ∀ b, ∀ᶠ a in f, m a ≤ b :=
  @tendsto_atTop α βᵒᵈ _ m f

Characterization of Tendency to Negative Infinity via Filters

Informal description

For a function $m : \alpha \to \beta$ between preordered types and a filter $f$ on $\alpha$, the function $m$ tends to $\mathrm{atBot}$ (the filter representing the limit at negative infinity in $\beta$) with respect to $f$ if and only if for every element $b \in \beta$, the set $\{a \in \alpha \mid m a \leq b\}$ is eventually in $f$.

Filter.tendsto_atTop_mono' theorem

 [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₁ ≤ᶠ[l] f₂) (h₁ : Tendsto f₁ l atTop) : Tendsto f₂ l atTop

Full source

theorem tendsto_atTop_mono' [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₁ ≤ᶠ[l] f₂)
    (h₁ : Tendsto f₁ l atTop) : Tendsto f₂ l atTop :=
  tendsto_atTop.2 fun b => by filter_upwards [tendsto_atTop.1 h₁ b, h] with x using le_trans

Monotonicity of Tendency to Positive Infinity under Eventual Inequality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder. Given a filter $l$ on $\alpha$ and functions $f_1, f_2 : \alpha \to \beta$ such that $f_1 \leq f_2$ eventually with respect to $l$, if $f_1$ tends to $\mathrm{atTop}$ (the filter representing the limit at positive infinity in $\beta$) with respect to $l$, then $f_2$ also tends to $\mathrm{atTop}$ with respect to $l$.

Filter.tendsto_atBot_mono' theorem

 [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₁ ≤ᶠ[l] f₂) : Tendsto f₂ l atBot → Tendsto f₁ l atBot

Full source

theorem tendsto_atBot_mono' [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₁ ≤ᶠ[l] f₂) :
    Tendsto f₂ l atBot → Tendsto f₁ l atBot :=
  @tendsto_atTop_mono' _ βᵒᵈ _ _ _ _ h

Monotonicity of Tendency to Negative Infinity under Eventual Inequality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder. Given a filter $l$ on $\alpha$ and functions $f_1, f_2 : \alpha \to \beta$ such that $f_1 \leq f_2$ eventually with respect to $l$, if $f_2$ tends to $\mathrm{atBot}$ (the filter representing the limit at negative infinity in $\beta$) with respect to $l$, then $f_1$ also tends to $\mathrm{atBot}$ with respect to $l$.

Filter.tendsto_atTop_mono theorem

[Preorder β] {l : Filter α} {f g : α → β} (h : ∀ n, f n ≤ g n) : Tendsto f l atTop → Tendsto g l atTop

Full source

theorem tendsto_atTop_mono [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ n, f n ≤ g n) :
    Tendsto f l atTop → Tendsto g l atTop :=
  tendsto_atTop_mono' l <| Eventually.of_forall h

Monotonicity of Tendency to Positive Infinity under Pointwise Inequality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder. Given a filter $l$ on $\alpha$ and functions $f, g : \alpha \to \beta$ such that $f(n) \leq g(n)$ for all $n \in \alpha$, if $f$ tends to $\mathrm{atTop}$ (the filter representing the limit at positive infinity in $\beta$) with respect to $l$, then $g$ also tends to $\mathrm{atTop}$ with respect to $l$.

Filter.tendsto_atBot_mono theorem

[Preorder β] {l : Filter α} {f g : α → β} (h : ∀ n, f n ≤ g n) : Tendsto g l atBot → Tendsto f l atBot

Full source

theorem tendsto_atBot_mono [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ n, f n ≤ g n) :
    Tendsto g l atBot → Tendsto f l atBot :=
  @tendsto_atTop_mono _ βᵒᵈ _ _ _ _ h

Monotonicity of Tendency to Negative Infinity under Pointwise Inequality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder. Given a filter $l$ on $\alpha$ and functions $f, g : \alpha \to \beta$ such that $f(n) \leq g(n)$ for all $n \in \alpha$, if $g$ tends to $\mathrm{atBot}$ (the filter representing the limit at negative infinity in $\beta$) with respect to $l$, then $f$ also tends to $\mathrm{atBot}$ with respect to $l$.

StrictMono.tendsto_atTop theorem

{φ : ℕ → ℕ} (h : StrictMono φ) : Tendsto φ atTop atTop

Full source

theorem _root_.StrictMono.tendsto_atTop {φ : ℕ → ℕ} (h : StrictMono φ) : Tendsto φ atTop atTop :=
  tendsto_atTop_mono h.id_le tendsto_id

Strictly Monotone Sequences Tend to Infinity

Informal description

For any strictly monotone function $\varphi : \mathbb{N} \to \mathbb{N}$, the limit of $\varphi(n)$ as $n$ tends to infinity is infinity. In other words, $\varphi$ tends to $\mathrm{atTop}$ with respect to the $\mathrm{atTop}$ filter on $\mathbb{N}$.

Monotone.upperBounds_range_comp_tendsto_atTop theorem

 [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atTop) :
  upperBounds (range (f ∘ g)) = upperBounds (range f)

Full source

/-- If `f` is a monotone function and `g` tends to `atTop` along a nontrivial filter.
then the upper bounds of the range of `f ∘ g`
are the same as the upper bounds of the range of `f`.

This lemma together with `exists_seq_monotone_tendsto_atTop_atTop` below
is useful to reduce a statement
about a monotone family indexed by a type with countably generated `atTop` (e.g., `ℝ`)
to the case of a family indexed by natural numbers. -/
theorem _root_.Monotone.upperBounds_range_comp_tendsto_atTop [Preorder β] [Preorder γ]
    {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atTop) :
    upperBounds (range (f ∘ g)) = upperBounds (range f) := by
  refine Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)
  rintro c hc _ ⟨b, rfl⟩
  obtain ⟨a, ha⟩ : ∃ a, b ≤ g a := (hg.eventually_ge_atTop b).exists
  exact (hf ha).trans <| hc <| mem_range_self _

Upper Bounds of Monotone Function Composed with a Tending-to-Infinity Function

Informal description

Let $\beta$ and $\gamma$ be preorders, and let $l$ be a nontrivial filter on a type $\alpha$. Suppose $f \colon \beta \to \gamma$ is a monotone function and $g \colon \alpha \to \beta$ is a function such that $g$ tends to $\mathrm{atTop}$ in $l$. Then the set of upper bounds of the range of $f \circ g$ is equal to the set of upper bounds of the range of $f$. In other words: \[ \mathrm{upperBounds}(\mathrm{range}(f \circ g)) = \mathrm{upperBounds}(\mathrm{range}(f)). \]

Monotone.lowerBounds_range_comp_tendsto_atBot theorem

 [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atBot) :
  lowerBounds (range (f ∘ g)) = lowerBounds (range f)

Full source

/-- If `f` is a monotone function and `g` tends to `atBot` along a nontrivial filter.
then the lower bounds of the range of `f ∘ g`
are the same as the lower bounds of the range of `f`. -/
theorem _root_.Monotone.lowerBounds_range_comp_tendsto_atBot [Preorder β] [Preorder γ]
    {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atBot) :
    lowerBounds (range (f ∘ g)) = lowerBounds (range f) :=
  hf.dual.upperBounds_range_comp_tendsto_atTop hg

Lower Bounds of Monotone Function Composed with a Tending-to-Negative-Infinity Function

Informal description

Let $\beta$ and $\gamma$ be preorders, and let $l$ be a nontrivial filter on a type $\alpha$. If $f \colon \beta \to \gamma$ is a monotone function and $g \colon \alpha \to \beta$ is a function such that $g$ tends to $\mathrm{atBot}$ in $l$, then the set of lower bounds of the range of $f \circ g$ is equal to the set of lower bounds of the range of $f$. In other words: \[ \mathrm{lowerBounds}(\mathrm{range}(f \circ g)) = \mathrm{lowerBounds}(\mathrm{range}(f)). \]

Antitone.lowerBounds_range_comp_tendsto_atTop theorem

 [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atTop) :
  lowerBounds (range (f ∘ g)) = lowerBounds (range f)

Full source

/-- If `f` is an antitone function and `g` tends to `atTop` along a nontrivial filter.
then the upper bounds of the range of `f ∘ g`
are the same as the upper bounds of the range of `f`. -/
theorem _root_.Antitone.lowerBounds_range_comp_tendsto_atTop [Preorder β] [Preorder γ]
    {l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atTop) :
    lowerBounds (range (f ∘ g)) = lowerBounds (range f) :=
  hf.dual_left.lowerBounds_range_comp_tendsto_atBot hg

Lower Bounds of Antitone Function Composed with a Tending-to-Infinity Function

Informal description

Let $\beta$ and $\gamma$ be preorders, and let $l$ be a nontrivial filter on a type $\alpha$. If $f \colon \beta \to \gamma$ is an antitone function and $g \colon \alpha \to \beta$ is a function such that $g$ tends to $\mathrm{atTop}$ in $l$, then the set of lower bounds of the range of $f \circ g$ is equal to the set of lower bounds of the range of $f$. In other words: \[ \mathrm{lowerBounds}(\mathrm{range}(f \circ g)) = \mathrm{lowerBounds}(\mathrm{range}(f)). \]

Antitone.upperBounds_range_comp_tendsto_atBot theorem

 [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atBot) :
  upperBounds (range (f ∘ g)) = upperBounds (range f)

Full source

/-- If `f` is an antitone function and `g` tends to `atBot` along a nontrivial filter.
then the upper bounds of the range of `f ∘ g`
are the same as the upper bounds of the range of `f`. -/
theorem _root_.Antitone.upperBounds_range_comp_tendsto_atBot [Preorder β] [Preorder γ]
    {l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atBot) :
    upperBounds (range (f ∘ g)) = upperBounds (range f) :=
  hf.dual.lowerBounds_range_comp_tendsto_atTop hg

Upper Bounds of Antitone Function Composed with a Tending-to-Negative-Infinity Function

Informal description

Let $\beta$ and $\gamma$ be preorders, and let $l$ be a nontrivial filter on a type $\alpha$. If $f \colon \beta \to \gamma$ is an antitone function and $g \colon \alpha \to \beta$ is a function such that $g$ tends to $\mathrm{atBot}$ in $l$, then the set of upper bounds of the range of $f \circ g$ is equal to the set of upper bounds of the range of $f$. In other words: \[ \mathrm{upperBounds}(\mathrm{range}(f \circ g)) = \mathrm{upperBounds}(\mathrm{range}(f)). \]

Filter.tendsto_atTop_atTop_of_monotone theorem

[Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (h : ∀ b, ∃ a, b ≤ f a) : Tendsto f atTop atTop

Full source

theorem tendsto_atTop_atTop_of_monotone [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f)
    (h : ∀ b, ∃ a, b ≤ f a) : Tendsto f atTop atTop :=
  tendsto_iInf.2 fun b =>
    tendsto_principal.2 <|
      let ⟨a, ha⟩ := h b
      mem_of_superset (mem_atTop a) fun _a' ha' => le_trans ha (hf ha')

Monotone Functions Preserve Limits at Positive Infinity

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be a monotone function. If for every $b \in \beta$ there exists $a \in \alpha$ such that $b \leq f(a)$, then $f$ tends to $\mathrm{atTop}$ in $\beta$ as its input tends to $\mathrm{atTop}$ in $\alpha$. In other words, the function $f$ preserves limits at positive infinity.

Filter.tendsto_atTop_atBot_of_antitone theorem

[Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) (h : ∀ b, ∃ a, f a ≤ b) : Tendsto f atTop atBot

Full source

theorem tendsto_atTop_atBot_of_antitone [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f)
    (h : ∀ b, ∃ a, f a ≤ b) : Tendsto f atTop atBot :=
  @tendsto_atTop_atTop_of_monotone _ βᵒᵈ _ _ _ hf h

Antitone Functions Map Limits at Positive Infinity to Negative Infinity

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be an antitone function. If for every $b \in \beta$ there exists $a \in \alpha$ such that $f(a) \leq b$, then $f$ tends to $\mathrm{atBot}$ in $\beta$ as its input tends to $\mathrm{atTop}$ in $\alpha$. In other words, the function $f$ maps limits at positive infinity to limits at negative infinity.

Filter.tendsto_atBot_atBot_of_monotone theorem

[Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (h : ∀ b, ∃ a, f a ≤ b) : Tendsto f atBot atBot

Full source

theorem tendsto_atBot_atBot_of_monotone [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f)
    (h : ∀ b, ∃ a, f a ≤ b) : Tendsto f atBot atBot :=
  tendsto_iInf.2 fun b => tendsto_principal.2 <|
    let ⟨a, ha⟩ := h b; mem_of_superset (mem_atBot a) fun _a' ha' => le_trans (hf ha') ha

Monotone functions preserve limits at negative infinity

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be a monotone function. If for every $b \in \beta$ there exists $a \in \alpha$ such that $f(a) \leq b$, then $f$ tends to $\mathrm{atBot}$ in $\beta$ as its input tends to $\mathrm{atBot}$ in $\alpha$. In other words, the function $f$ preserves limits at negative infinity.

Filter.tendsto_atBot_atTop_of_antitone theorem

[Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) (h : ∀ b, ∃ a, b ≤ f a) : Tendsto f atBot atTop

Full source

theorem tendsto_atBot_atTop_of_antitone [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f)
    (h : ∀ b, ∃ a, b ≤ f a) : Tendsto f atBot atTop :=
  @tendsto_atBot_atBot_of_monotone _ βᵒᵈ _ _ _ hf h

Antitone Functions Map Limits at Negative Infinity to Positive Infinity

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be an antitone function. If for every $b \in \beta$ there exists $a \in \alpha$ such that $b \leq f(a)$, then $f$ tends to $\mathrm{atTop}$ in $\beta$ as its input tends to $\mathrm{atBot}$ in $\alpha$. In other words, the function $f$ maps limits at negative infinity to limits at positive infinity.

Filter.comap_embedding_atTop theorem

 [Preorder β] [Preorder γ] {e : β → γ} (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, c ≤ e b) :
  comap e atTop = atTop

Full source

theorem comap_embedding_atTop [Preorder β] [Preorder γ] {e : β → γ}
    (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, c ≤ e b) : comap e atTop = atTop :=
  le_antisymm
    (le_iInf fun b =>
      le_principal_iff.2 <| mem_comap.2 ⟨Ici (e b), mem_atTop _, fun _ => (hm _ _).1⟩)
    (tendsto_atTop_atTop_of_monotone (fun _ _ => (hm _ _).2) hu).le_comap

Preimage of `atTop` under an Order Embedding Equals `atTop`

Informal description

Let $\beta$ and $\gamma$ be preorders, and let $e : \beta \to \gamma$ be an embedding (i.e., for all $b_1, b_2 \in \beta$, $e(b_1) \leq e(b_2)$ if and only if $b_1 \leq b_2$). If for every $c \in \gamma$ there exists $b \in \beta$ such that $c \leq e(b)$, then the preimage filter of $\mathrm{atTop}$ under $e$ is equal to $\mathrm{atTop}$ on $\beta$.

Filter.comap_embedding_atBot theorem

 [Preorder β] [Preorder γ] {e : β → γ} (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, e b ≤ c) :
  comap e atBot = atBot

Full source

theorem comap_embedding_atBot [Preorder β] [Preorder γ] {e : β → γ}
    (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, e b ≤ c) : comap e atBot = atBot :=
  @comap_embedding_atTop βᵒᵈ γᵒᵈ _ _ e (Function.swap hm) hu

Preimage of `atBot` under an Order Embedding Equals `atBot`

Informal description

Let $\beta$ and $\gamma$ be preorders, and let $e : \beta \to \gamma$ be an order embedding (i.e., for all $b_1, b_2 \in \beta$, $e(b_1) \leq e(b_2)$ if and only if $b_1 \leq b_2$). If for every $c \in \gamma$ there exists $b \in \beta$ such that $e(b) \leq c$, then the preimage filter of $\mathrm{atBot}$ under $e$ is equal to $\mathrm{atBot}$ on $\beta$.

Filter.tendsto_atTop_embedding theorem

 [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α} (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂)
  (hu : ∀ c, ∃ b, c ≤ e b) : Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop

Full source

theorem tendsto_atTop_embedding [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α}
    (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, c ≤ e b) :
    TendstoTendsto (e ∘ f) l atTop ↔ Tendsto f l atTop := by
  rw [← comap_embedding_atTop hm hu, tendsto_comap_iff]

Tendsto Composition with Order Embedding Preserves `atTop` Limit

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types with preorders, and let $f : \alpha \to \beta$ and $e : \beta \to \gamma$ be functions. Suppose that $e$ is an order embedding (i.e., for all $b_1, b_2 \in \beta$, $e(b_1) \leq e(b_2)$ if and only if $b_1 \leq b_2$) and that for every $c \in \gamma$ there exists $b \in \beta$ such that $c \leq e(b)$. Then, the composition $e \circ f$ tends to $\mathrm{atTop}$ along a filter $l$ on $\alpha$ if and only if $f$ tends to $\mathrm{atTop}$ along $l$.

Filter.tendsto_atBot_embedding theorem

 [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α} (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂)
  (hu : ∀ c, ∃ b, e b ≤ c) : Tendsto (e ∘ f) l atBot ↔ Tendsto f l atBot

Full source

/-- A function `f` goes to `-∞` independent of an order-preserving embedding `e`. -/
theorem tendsto_atBot_embedding [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α}
    (hm : ∀ b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ c, ∃ b, e b ≤ c) :
    TendstoTendsto (e ∘ f) l atBot ↔ Tendsto f l atBot :=
  @tendsto_atTop_embedding α βᵒᵈ γᵒᵈ _ _ f e l (Function.swap hm) hu

Composition with Order Embedding Preserves `atBot` Limit

Informal description

Let $\beta$ and $\gamma$ be preorders, and let $f : \alpha \to \beta$ and $e : \beta \to \gamma$ be functions. Suppose that $e$ is an order embedding (i.e., for all $b_1, b_2 \in \beta$, $e(b_1) \leq e(b_2)$ if and only if $b_1 \leq b_2$) and that for every $c \in \gamma$ there exists $b \in \beta$ such that $e(b) \leq c$. Then, the composition $e \circ f$ tends to $-\infty$ along a filter $l$ on $\alpha$ if and only if $f$ tends to $-\infty$ along $l$.

Filter.tendsto_atTop_atTop_of_monotone' theorem

[Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u) (H : ¬BddAbove (range u)) : Tendsto u atTop atTop

Full source

/-- If `u` is a monotone function with linear ordered codomain and the range of `u` is not bounded
above, then `Tendsto u atTop atTop`. -/
theorem tendsto_atTop_atTop_of_monotone' [Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u)
    (H : ¬BddAbove (range u)) : Tendsto u atTop atTop := by
  apply h.tendsto_atTop_atTop
  intro b
  rcases not_bddAbove_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩
  exact ⟨N, le_of_lt hN⟩

Monotone unbounded functions tend to infinity at infinity

Informal description

Let $\iota$ be a preorder and $\alpha$ be a linear order. If $u : \iota \to \alpha$ is a monotone function whose range is not bounded above, then $u$ tends to $\infty$ in $\alpha$ as its input tends to $\infty$ in $\iota$. In other words, $\lim_{x \to \infty} u(x) = \infty$.

Filter.tendsto_atBot_atBot_of_monotone' theorem

[Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u) (H : ¬BddBelow (range u)) : Tendsto u atBot atBot

Full source

/-- If `u` is a monotone function with linear ordered codomain and the range of `u` is not bounded
below, then `Tendsto u atBot atBot`. -/
theorem tendsto_atBot_atBot_of_monotone' [Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u)
    (H : ¬BddBelow (range u)) : Tendsto u atBot atBot :=
  @tendsto_atTop_atTop_of_monotone' ιᵒᵈ αᵒᵈ _ _ _ h.dual H

Monotone unbounded functions tend to negative infinity at negative infinity

Informal description

Let $\iota$ be a preorder and $\alpha$ be a linear order. If $u : \iota \to \alpha$ is a monotone function whose range is not bounded below, then $u$ tends to $-\infty$ in $\alpha$ as its input tends to $-\infty$ in $\iota$. In other words, $\lim_{x \to -\infty} u(x) = -\infty$.

Filter.tendsto_atTop_of_monotone_of_filter theorem

 [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α} (h : Monotone u) [NeBot l] (hu : Tendsto u l atTop) :
  Tendsto u atTop atTop

Full source

/-- If a monotone function `u : ι → α` tends to `atTop` along *some* non-trivial filter `l`, then
it tends to `atTop` along `atTop`. -/
theorem tendsto_atTop_of_monotone_of_filter [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α}
    (h : Monotone u) [NeBot l] (hu : Tendsto u l atTop) : Tendsto u atTop atTop :=
  h.tendsto_atTop_atTop fun b => (hu.eventually (mem_atTop b)).exists

Monotone functions tending to infinity along a filter also tend to infinity at infinity

Informal description

Let $\iota$ and $\alpha$ be preorders, $l$ be a non-trivial filter on $\iota$, and $u : \iota \to \alpha$ be a monotone function. If $u$ tends to $\mathrm{atTop}$ along $l$, then $u$ tends to $\mathrm{atTop}$ along $\mathrm{atTop}$.

Filter.tendsto_atBot_of_monotone_of_filter theorem

 [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α} (h : Monotone u) [NeBot l] (hu : Tendsto u l atBot) :
  Tendsto u atBot atBot

Full source

/-- If a monotone function `u : ι → α` tends to `atBot` along *some* non-trivial filter `l`, then
it tends to `atBot` along `atBot`. -/
theorem tendsto_atBot_of_monotone_of_filter [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α}
    (h : Monotone u) [NeBot l] (hu : Tendsto u l atBot) : Tendsto u atBot atBot :=
  @tendsto_atTop_of_monotone_of_filter ιᵒᵈ αᵒᵈ _ _ _ _ h.dual _ hu

Monotone functions tending to negative infinity along a filter also tend to negative infinity at negative infinity

Informal description

Let $\iota$ and $\alpha$ be preorders, $l$ be a non-trivial filter on $\iota$, and $u : \iota \to \alpha$ be a monotone function. If $u$ tends to $\mathrm{atBot}$ along $l$, then $u$ tends to $\mathrm{atBot}$ along $\mathrm{atBot}$.

Filter.tendsto_atTop_of_monotone_of_subseq theorem

 [Preorder ι] [Preorder α] {u : ι → α} {φ : ι' → ι} (h : Monotone u) {l : Filter ι'} [NeBot l]
  (H : Tendsto (u ∘ φ) l atTop) : Tendsto u atTop atTop

Full source

theorem tendsto_atTop_of_monotone_of_subseq [Preorder ι] [Preorder α] {u : ι → α} {φ : ι' → ι}
    (h : Monotone u) {l : Filter ι'} [NeBot l] (H : Tendsto (u ∘ φ) l atTop) :
    Tendsto u atTop atTop :=
  tendsto_atTop_of_monotone_of_filter h (tendsto_map' H)

Monotone functions with subsequences tending to infinity also tend to infinity at infinity

Informal description

Let $\iota$ and $\alpha$ be preorders, $u : \iota \to \alpha$ be a monotone function, and $\varphi : \iota' \to \iota$ be a sequence. If the composition $u \circ \varphi$ tends to $\mathrm{atTop}$ along a non-trivial filter $l$ on $\iota'$, then $u$ tends to $\mathrm{atTop}$ along $\mathrm{atTop}$.

Filter.tendsto_atBot_of_monotone_of_subseq theorem

 [Preorder ι] [Preorder α] {u : ι → α} {φ : ι' → ι} (h : Monotone u) {l : Filter ι'} [NeBot l]
  (H : Tendsto (u ∘ φ) l atBot) : Tendsto u atBot atBot

Full source

theorem tendsto_atBot_of_monotone_of_subseq [Preorder ι] [Preorder α] {u : ι → α} {φ : ι' → ι}
    (h : Monotone u) {l : Filter ι'} [NeBot l] (H : Tendsto (u ∘ φ) l atBot) :
    Tendsto u atBot atBot :=
  tendsto_atBot_of_monotone_of_filter h (tendsto_map' H)

Monotone functions with subsequences tending to negative infinity also tend to negative infinity at negative infinity

Informal description

Let $\iota$ and $\alpha$ be preorders, $u : \iota \to \alpha$ be a monotone function, and $\varphi : \iota' \to \iota$ be a sequence. If the composition $u \circ \varphi$ tends to negative infinity along a non-trivial filter $l$ on $\iota'$, then $u$ tends to negative infinity along the filter at negative infinity.