Mathlib.Order.Filter.Tendsto

Filter.tendsto_def theorem

{f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁

Full source

theorem tendsto_def {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    TendstoTendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁ :=
  Iff.rfl

Characterization of Filter Convergence via Preimages

Informal description

For a function $f : \alpha \to \beta$ and filters $l_1$ on $\alpha$ and $l_2$ on $\beta$, the statement $\text{Tendsto } f l_1 l_2$ holds if and only if for every set $s$ in the filter $l_2$, the preimage $f^{-1}(s)$ belongs to the filter $l_1$.

Filter.tendsto_iff_eventually theorem

 {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
  Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ y in l₂, p y) → ∀ᶠ x in l₁, p (f x)

Full source

theorem tendsto_iff_eventually {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    TendstoTendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ y in l₂, p y) → ∀ᶠ x in l₁, p (f x) :=
  Iff.rfl

Characterization of Filter Convergence via Eventual Properties

Informal description

For a function $f : \alpha \to \beta$ and filters $l_1$ on $\alpha$ and $l_2$ on $\beta$, the following are equivalent: 1. The function $f$ tends to $l_2$ along $l_1$ (i.e., $\text{Tendsto}\, f\, l_1\, l_2$). 2. For every predicate $p : \beta \to \text{Prop}$, if $p$ holds eventually with respect to $l_2$ (i.e., $\forallᶠ y \text{ in } l_2, p y$), then $p \circ f$ holds eventually with respect to $l_1$ (i.e., $\forallᶠ x \text{ in } l_1, p (f x)$).

Filter.tendsto_iff_forall_eventually_mem theorem

 {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, ∀ᶠ x in l₁, f x ∈ s

Full source

theorem tendsto_iff_forall_eventually_mem {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    TendstoTendsto f l₁ l₂ ↔ ∀ s ∈ l₂, ∀ᶠ x in l₁, f x ∈ s :=
  Iff.rfl

Characterization of Filter Convergence via Eventual Membership

Informal description

For a function $f : \alpha \to \beta$ and filters $l_1$ on $\alpha$ and $l_2$ on $\beta$, the following are equivalent: 1. The function $f$ tends to $l_2$ along $l_1$ (i.e., $\text{Tendsto}\, f\, l_1\, l_2$). 2. For every set $s$ in the filter $l_2$, the set of points $x$ in $\alpha$ such that $f(x) \in s$ is eventually in $l_1$ (i.e., $\forall s \in l_2, \forallᶠ x \text{ in } l_1, f(x) \in s$).

Filter.Tendsto.eventually_mem theorem

 {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {s : Set β} (hf : Tendsto f l₁ l₂) (h : s ∈ l₂) : ∀ᶠ x in l₁, f x ∈ s

Full source

lemma Tendsto.eventually_mem {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {s : Set β}
    (hf : Tendsto f l₁ l₂) (h : s ∈ l₂) : ∀ᶠ x in l₁, f x ∈ s :=
  hf h

Eventual Membership under Filter Convergence

Informal description

Let $f : \alpha \to \beta$ be a function, and let $l_1$ and $l_2$ be filters on $\alpha$ and $\beta$ respectively. If $f$ tends to $l_2$ with respect to $l_1$ (i.e., $\text{Tendsto}\, f\, l_1\, l_2$ holds) and $s$ is a set in the filter $l_2$, then for $l_1$-eventually all $x \in \alpha$, the image $f(x)$ belongs to $s$.

Filter.Tendsto.eventually theorem

 {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop} (hf : Tendsto f l₁ l₂) (h : ∀ᶠ y in l₂, p y) :
  ∀ᶠ x in l₁, p (f x)

Full source

theorem Tendsto.eventually {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop}
    (hf : Tendsto f l₁ l₂) (h : ∀ᶠ y in l₂, p y) : ∀ᶠ x in l₁, p (f x) :=
  hf h

Eventual Preservation of Properties under Filter Limits

Informal description

Let $f : \alpha \to \beta$ be a function, and let $l_1$ and $l_2$ be filters on $\alpha$ and $\beta$ respectively. If $f$ tends to $l_2$ along $l_1$ (i.e., $\text{Tendsto}\, f\, l_1\, l_2$ holds) and a property $p : \beta \to \text{Prop}$ holds eventually with respect to $l_2$, then the composition $p \circ f$ holds eventually with respect to $l_1$. In other words, if $\forallᶠ y \text{ in } l_2, p y$, then $\forallᶠ x \text{ in } l_1, p (f x)$.

Filter.not_tendsto_iff_exists_frequently_nmem theorem

 {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : ¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ x in l₁, f x ∉ s

Full source

theorem not_tendsto_iff_exists_frequently_nmem {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    ¬Tendsto f l₁ l₂¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ x in l₁, f x ∉ s := by
  simp only [tendsto_iff_forall_eventually_mem, not_forall, exists_prop, not_eventually]

Characterization of Non-Convergence via Frequently Failing Membership

Informal description

For a function $f : \alpha \to \beta$ and filters $l_1$ on $\alpha$ and $l_2$ on $\beta$, the following are equivalent: 1. $f$ does not tend to $l_2$ along $l_1$ (i.e., $\neg \text{Tendsto}\, f\, l_1\, l_2$). 2. There exists a set $s \in l_2$ such that $f(x) \notin s$ holds frequently in $l_1$ (i.e., $\exists s \in l_2, \existsᶠ x \text{ in } l_1, f x \notin s$).

Filter.Tendsto.frequently theorem

 {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop} (hf : Tendsto f l₁ l₂) (h : ∃ᶠ x in l₁, p (f x)) :
  ∃ᶠ y in l₂, p y

Full source

theorem Tendsto.frequently {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop}
    (hf : Tendsto f l₁ l₂) (h : ∃ᶠ x in l₁, p (f x)) : ∃ᶠ y in l₂, p y :=
  mt hf.eventually h

Frequent Property Preservation under Filter Limits

Informal description

Let $f : \alpha \to \beta$ be a function, and let $l_1$ and $l_2$ be filters on $\alpha$ and $\beta$ respectively. If $f$ tends to $l_2$ along $l_1$ (i.e., $\text{Tendsto}\, f\, l_1\, l_2$ holds) and a property $p : \beta \to \text{Prop}$ holds frequently for $f(x)$ with respect to $l_1$ (i.e., $\existsᶠ x \text{ in } l_1, p (f x)$), then $p$ holds frequently with respect to $l_2$ (i.e., $\existsᶠ y \text{ in } l_2, p y$).

Filter.Tendsto.frequently_map theorem

 {l₁ : Filter α} {l₂ : Filter β} {p : α → Prop} {q : β → Prop} (f : α → β) (c : Filter.Tendsto f l₁ l₂)
  (w : ∀ x, p x → q (f x)) (h : ∃ᶠ x in l₁, p x) : ∃ᶠ y in l₂, q y

Full source

theorem Tendsto.frequently_map {l₁ : Filter α} {l₂ : Filter β} {p : α → Prop} {q : β → Prop}
    (f : α → β) (c : Filter.Tendsto f l₁ l₂) (w : ∀ x, p x → q (f x)) (h : ∃ᶠ x in l₁, p x) :
    ∃ᶠ y in l₂, q y :=
  c.frequently (h.mono w)

Frequent Property Mapping under Filter Limits

Informal description

Let $f : \alpha \to \beta$ be a function, and let $l_1$ and $l_2$ be filters on $\alpha$ and $\beta$ respectively. Suppose that $f$ tends to $l_2$ along $l_1$ (i.e., $\text{Tendsto}\, f\, l_1\, l_2$ holds). Let $p : \alpha \to \text{Prop}$ and $q : \beta \to \text{Prop}$ be predicates such that for all $x \in \alpha$, $p(x)$ implies $q(f(x))$. If $p$ holds frequently with respect to $l_1$ (i.e., $\existsᶠ x \text{ in } l_1, p x$), then $q$ holds frequently with respect to $l_2$ (i.e., $\existsᶠ y \text{ in } l_2, q y$).

Filter.tendsto_bot theorem

{f : α → β} {l : Filter β} : Tendsto f ⊥ l

Full source

@[simp]
theorem tendsto_bot {f : α → β} {l : Filter β} : Tendsto f ⊥ l := by simp [Tendsto]

Every Function Tends to Any Filter Along the Bottom Filter

Informal description

For any function $f : \alpha \to \beta$ and any filter $l$ on $\beta$, the function $f$ tends to $l$ along the bottom filter $\bot$ on $\alpha$.

Filter.Tendsto.of_neBot_imp theorem

{f : α → β} {la : Filter α} {lb : Filter β} (h : NeBot la → Tendsto f la lb) : Tendsto f la lb

Full source

theorem Tendsto.of_neBot_imp {f : α → β} {la : Filter α} {lb : Filter β}
    (h : NeBot la → Tendsto f la lb) : Tendsto f la lb := by
  rcases eq_or_neBot la with rfl | hla
  · exact tendsto_bot
  · exact h hla

Limit Preservation Under Non-Trivial Filter Condition

Informal description

Let $f : \alpha \to \beta$ be a function, and let $l_a$ and $l_b$ be filters on $\alpha$ and $\beta$ respectively. If the implication "whenever $l_a$ is a non-trivial filter, $f$ tends to $l_b$ along $l_a$" holds, then $f$ tends to $l_b$ along $l_a$.

Filter.tendsto_top theorem

{f : α → β} {l : Filter α} : Tendsto f l ⊤

Full source

@[simp] theorem tendsto_top {f : α → β} {l : Filter α} : Tendsto f l ⊤ := le_top

Every Function Tends to the Top Filter

Informal description

For any function $f : \alpha \to \beta$ and any filter $l$ on $\alpha$, the function $f$ tends to the top filter $\top$ on $\beta$ with respect to $l$. In other words, the preimage of any subset of $\beta$ under $f$ belongs to $l$.

Filter.le_map_of_right_inverse theorem

 {mab : α → β} {mba : β → α} {f : Filter α} {g : Filter β} (h₁ : mab ∘ mba =ᶠ[g] id) (h₂ : Tendsto mba g f) :
  g ≤ map mab f

Full source

theorem le_map_of_right_inverse {mab : α → β} {mba : β → α} {f : Filter α} {g : Filter β}
    (h₁ : mab ∘ mbamab ∘ mba =ᶠ[g] id) (h₂ : Tendsto mba g f) : g ≤ map mab f := by
  rw [← @map_id _ g, ← map_congr h₁, ← map_map]
  exact map_mono h₂

Filter Inequality via Right Inverse and Tendsto Condition

Informal description

Let $m_{ab} : \alpha \to \beta$ and $m_{ba} : \beta \to \alpha$ be functions, $f$ be a filter on $\alpha$, and $g$ be a filter on $\beta$. If: 1. The composition $m_{ab} \circ m_{ba}$ is eventually equal to the identity function on $\beta$ with respect to $g$ (i.e., $m_{ab}(m_{ba}(y)) = y$ for all $y$ in some set belonging to $g$), and 2. The function $m_{ba}$ tends to $f$ along $g$ (i.e., for every set $s \in f$, the preimage $m_{ba}^{-1}(s)$ belongs to $g$), then the filter $g$ is less than or equal to the image filter $\text{map } m_{ab} f$ (i.e., every set in $\text{map } m_{ab} f$ is also in $g$).

Filter.eventuallyEq_of_left_inv_of_right_inv theorem

 {f : α → β} {g₁ g₂ : β → α} {fa : Filter α} {fb : Filter β} (hleft : ∀ᶠ x in fa, g₁ (f x) = x)
  (hright : ∀ᶠ y in fb, f (g₂ y) = y) (htendsto : Tendsto g₂ fb fa) : g₁ =ᶠ[fb] g₂

Full source

theorem eventuallyEq_of_left_inv_of_right_inv {f : α → β} {g₁ g₂ : β → α} {fa : Filter α}
    {fb : Filter β} (hleft : ∀ᶠ x in fa, g₁ (f x) = x) (hright : ∀ᶠ y in fb, f (g₂ y) = y)
    (htendsto : Tendsto g₂ fb fa) : g₁ =ᶠ[fb] g₂ :=
  (htendsto.eventually hleft).mp <| hright.mono fun _ hr hl => (congr_arg g₁ hr.symm).trans hl

Eventual Equality of Left and Right Inverses under Filter Conditions

Informal description

Let $f : \alpha \to \beta$ be a function, $g_1, g_2 : \beta \to \alpha$ be its left and right inverses respectively, and $fa$, $fb$ be filters on $\alpha$ and $\beta$. If: 1. For all $x$ eventually in $fa$, $g_1(f(x)) = x$, 2. For all $y$ eventually in $fb$, $f(g_2(y)) = y$, 3. The function $g_2$ tends to $fa$ along $fb$, then $g_1$ and $g_2$ are eventually equal with respect to $fb$, i.e., $g_1(y) = g_2(y)$ for all $y$ eventually in $fb$.

Filter.tendsto_iff_comap theorem

{f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Tendsto f l₁ l₂ ↔ l₁ ≤ l₂.comap f

Full source

theorem tendsto_iff_comap {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    TendstoTendsto f l₁ l₂ ↔ l₁ ≤ l₂.comap f :=
  map_le_iff_le_comap

Characterization of Tendsto via Preimage Filter: $\text{Tendsto } f l_1 l_2 \leftrightarrow l_1 \leq l_2.\text{comap } f$

Informal description

For a function $f : \alpha \to \beta$ and filters $l_1$ on $\alpha$ and $l_2$ on $\beta$, the following are equivalent: 1. The function $f$ tends to $l_2$ with respect to $l_1$ (i.e., $\text{Tendsto } f l_1 l_2$ holds). 2. The filter $l_1$ is finer than the preimage filter $l_2.\text{comap } f$ (i.e., $l_1 \leq l_2.\text{comap } f$).

Filter.Tendsto.disjoint theorem

 {f : α → β} {la₁ la₂ : Filter α} {lb₁ lb₂ : Filter β} (h₁ : Tendsto f la₁ lb₁) (hd : Disjoint lb₁ lb₂)
  (h₂ : Tendsto f la₂ lb₂) : Disjoint la₁ la₂

Full source

protected theorem Tendsto.disjoint {f : α → β} {la₁ la₂ : Filter α} {lb₁ lb₂ : Filter β}
    (h₁ : Tendsto f la₁ lb₁) (hd : Disjoint lb₁ lb₂) (h₂ : Tendsto f la₂ lb₂) : Disjoint la₁ la₂ :=
  (disjoint_comap hd).mono h₁.le_comap h₂.le_comap

Disjointness Preservation under Filter Convergence: $\text{Tendsto } f la_1 lb_1 \land \text{Disjoint } lb_1 lb_2 \land \text{Tendsto } f la_2 lb_2 \to \text{Disjoint } la_1 la_2$

Informal description

Let $f : \alpha \to \beta$ be a function, and let $la_1, la_2$ be filters on $\alpha$ and $lb_1, lb_2$ be filters on $\beta$. If: 1. $f$ tends to $lb_1$ with respect to $la_1$, 2. The filters $lb_1$ and $lb_2$ are disjoint, 3. $f$ tends to $lb_2$ with respect to $la_2$, then the filters $la_1$ and $la_2$ are also disjoint.

Filter.tendsto_congr' theorem

 {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) : Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂

Full source

theorem tendsto_congr' {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) :
    TendstoTendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂ := by rw [Tendsto, Tendsto, map_congr hl]

Equivalence of Tendsto for Eventually Equal Functions: $\text{Tendsto } f_1 l_1 l_2 \leftrightarrow \text{Tendsto } f_2 l_1 l_2$ when $f_1 =_{l_1} f_2$

Informal description

Let $f_1, f_2 : \alpha \to \beta$ be functions and $l_1$, $l_2$ be filters on $\alpha$ and $\beta$ respectively. If $f_1$ and $f_2$ are eventually equal with respect to $l_1$ (i.e., $f_1(x) = f_2(x)$ for all $x$ in some set belonging to $l_1$), then the following are equivalent: 1. $f_1$ tends to $l_2$ with respect to $l_1$ (i.e., $\text{Tendsto } f_1 l_1 l_2$ holds). 2. $f_2$ tends to $l_2$ with respect to $l_1$ (i.e., $\text{Tendsto } f_2 l_1 l_2$ holds).

Filter.Tendsto.congr' theorem

 {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) (h : Tendsto f₁ l₁ l₂) : Tendsto f₂ l₁ l₂

Full source

theorem Tendsto.congr' {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂)
    (h : Tendsto f₁ l₁ l₂) : Tendsto f₂ l₁ l₂ :=
  (tendsto_congr' hl).1 h

Preservation of Filter Limit under Eventually Equal Functions

Informal description

Let $f_1, f_2 : \alpha \to \beta$ be functions and $l_1$, $l_2$ be filters on $\alpha$ and $\beta$ respectively. If $f_1$ and $f_2$ are eventually equal with respect to $l_1$ (i.e., $f_1(x) = f_2(x)$ for all $x$ in some set belonging to $l_1$), and $f_1$ tends to $l_2$ with respect to $l_1$, then $f_2$ also tends to $l_2$ with respect to $l_1$.

Filter.tendsto_congr theorem

 {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ x, f₁ x = f₂ x) : Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂

Full source

theorem tendsto_congr {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ x, f₁ x = f₂ x) :
    TendstoTendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂ :=
  tendsto_congr' (univ_mem' h)

Tendsto equivalence for pointwise equal functions: $\text{Tendsto } f_1 l_1 l_2 \leftrightarrow \text{Tendsto } f_2 l_1 l_2$ when $f_1 = f_2$

Informal description

For any functions $f_1, f_2 : \alpha \to \beta$ and filters $l_1$ on $\alpha$, $l_2$ on $\beta$, if $f_1(x) = f_2(x)$ for all $x \in \alpha$, then the following are equivalent: 1. $f_1$ tends to $l_2$ with respect to $l_1$ (i.e., $\text{Tendsto } f_1 l_1 l_2$ holds). 2. $f_2$ tends to $l_2$ with respect to $l_1$ (i.e., $\text{Tendsto } f_2 l_1 l_2$ holds).

Filter.Tendsto.congr theorem

 {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ x, f₁ x = f₂ x) : Tendsto f₁ l₁ l₂ → Tendsto f₂ l₁ l₂

Full source

theorem Tendsto.congr {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ x, f₁ x = f₂ x) :
    Tendsto f₁ l₁ l₂ → Tendsto f₂ l₁ l₂ :=
  (tendsto_congr h).1

Limit Preservation under Pointwise Equal Functions

Informal description

For any functions $ f_1, f_2 : \alpha \to \beta $ and filters $ l_1 $ on $ \alpha $, $ l_2 $ on $ \beta $, if $ f_1(x) = f_2(x) $ for all $ x \in \alpha $, then the limit of $ f_1 $ with respect to $ l_1 $ and $ l_2 $ implies the limit of $ f_2 $ with respect to $ l_1 $ and $ l_2 $.

Filter.tendsto_id' theorem

{x y : Filter α} : Tendsto id x y ↔ x ≤ y

Full source

theorem tendsto_id' {x y : Filter α} : TendstoTendsto id x y ↔ x ≤ y :=
  Iff.rfl

Identity Tendsto Condition: $\text{Tendsto id } x y \leftrightarrow x \leq y$

Informal description

For any two filters $x$ and $y$ on a type $\alpha$, the identity function $\text{id}$ tends to $y$ with respect to $x$ if and only if $x$ is finer than $y$, i.e., $x \leq y$.

Filter.tendsto_id theorem

{x : Filter α} : Tendsto id x x

Full source

theorem tendsto_id {x : Filter α} : Tendsto id x x :=
  le_refl x

Identity Function Preserves Filter

Informal description

For any filter $x$ on a type $\alpha$, the identity function $\text{id} : \alpha \to \alpha$ tends to $x$ with respect to $x$ itself. In other words, the identity function preserves the filter $x$.

Filter.Tendsto.comp theorem

 {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} (hg : Tendsto g y z) (hf : Tendsto f x y) :
  Tendsto (g ∘ f) x z

Full source

theorem Tendsto.comp {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ}
    (hg : Tendsto g y z) (hf : Tendsto f x y) : Tendsto (g ∘ f) x z := fun _ hs => hf (hg hs)

Composition of Tendsto Functions Preserves Filter Limits

Informal description

Given functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, and filters $x$ on $\alpha$, $y$ on $\beta$, and $z$ on $\gamma$, if $f$ tends to $y$ along $x$ and $g$ tends to $z$ along $y$, then the composition $g \circ f$ tends to $z$ along $x$.

Filter.Tendsto.iterate theorem

{f : α → α} {l : Filter α} (h : Tendsto f l l) : ∀ n, Tendsto (f^[n]) l l

Full source

protected theorem Tendsto.iterate {f : α → α} {l : Filter α} (h : Tendsto f l l) :
    ∀ n, Tendsto (f^[n]) l l
  | 0 => tendsto_id
  | (n + 1) => (h.iterate n).comp h

Iterates Preserve Filter Limits

Informal description

Let $f : \alpha \to \alpha$ be a function and $l$ a filter on $\alpha$. If $f$ tends to $l$ along $l$, then for every natural number $n$, the $n$-th iterate $f^{[n]}$ of $f$ also tends to $l$ along $l$.

Filter.Tendsto.mono_left theorem

{f : α → β} {x y : Filter α} {z : Filter β} (hx : Tendsto f x z) (h : y ≤ x) : Tendsto f y z

Full source

theorem Tendsto.mono_left {f : α → β} {x y : Filter α} {z : Filter β} (hx : Tendsto f x z)
    (h : y ≤ x) : Tendsto f y z :=
  (map_mono h).trans hx

Monotonicity of Tendsto with Respect to the Source Filter

Informal description

Let $f \colon \alpha \to \beta$ be a function, and let $x, y$ be filters on $\alpha$ and $z$ a filter on $\beta$. If $f$ tends to $z$ along $x$ and $y \leq x$ in the partial order of filters on $\alpha$, then $f$ tends to $z$ along $y$.

Filter.Tendsto.mono_right theorem

{f : α → β} {x : Filter α} {y z : Filter β} (hy : Tendsto f x y) (hz : y ≤ z) : Tendsto f x z

Full source

theorem Tendsto.mono_right {f : α → β} {x : Filter α} {y z : Filter β} (hy : Tendsto f x y)
    (hz : y ≤ z) : Tendsto f x z :=
  le_trans hy hz

Monotonicity of Tendsto with Respect to the Target Filter

Informal description

Let $f : \alpha \to \beta$ be a function, and let $x$ be a filter on $\alpha$. If $f$ tends to $y$ with respect to $x$ and $y \leq z$ in the partial order of filters on $\beta$, then $f$ tends to $z$ with respect to $x$.

Filter.Tendsto.neBot theorem

{f : α → β} {x : Filter α} {y : Filter β} (h : Tendsto f x y) [hx : NeBot x] : NeBot y

Full source

theorem Tendsto.neBot {f : α → β} {x : Filter α} {y : Filter β} (h : Tendsto f x y) [hx : NeBot x] :
    NeBot y :=
  (hx.map _).mono h

Non-triviality of the limit filter under a non-trivial source filter

Informal description

Let $f \colon \alpha \to \beta$ be a function, and let $x$ be a non-trivial filter on $\alpha$. If $f$ tends to a filter $y$ on $\beta$ with respect to $x$, then $y$ is also non-trivial.

Filter.tendsto_map theorem

{f : α → β} {x : Filter α} : Tendsto f x (map f x)

Full source

theorem tendsto_map {f : α → β} {x : Filter α} : Tendsto f x (map f x) :=
  le_refl (map f x)

Function Tends to its Image Filter

Informal description

For any function $f : \alpha \to \beta$ and any filter $x$ on $\alpha$, the function $f$ tends to the image filter $\text{map } f x$ with respect to $x$.

Filter.tendsto_map'_iff theorem

{f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ} : Tendsto f (map g x) y ↔ Tendsto (f ∘ g) x y

Full source

@[simp]
theorem tendsto_map'_iff {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ} :
    TendstoTendsto f (map g x) y ↔ Tendsto (f ∘ g) x y := by
  rw [Tendsto, Tendsto, map_map]

Equivalence of Tendency Conditions via Composition and Image Filter

Informal description

For any function $f \colon \beta \to \gamma$, any function $g \colon \alpha \to \beta$, any filter $x$ on $\alpha$, and any filter $y$ on $\gamma$, the following are equivalent: 1. The function $f$ tends to $y$ with respect to the image filter $\text{map } g x$ on $\beta$. 2. The composition $f \circ g$ tends to $y$ with respect to the filter $x$ on $\alpha$.

Filter.tendsto_comap theorem

{f : α → β} {x : Filter β} : Tendsto f (comap f x) x

Full source

theorem tendsto_comap {f : α → β} {x : Filter β} : Tendsto f (comap f x) x :=
  map_comap_le

Function Tends to Filter via Preimage Filter

Informal description

For any function $f \colon \alpha \to \beta$ and any filter $x$ on $\beta$, the function $f$ tends to $x$ with respect to the preimage filter $\text{comap } f x$ on $\alpha$.

Filter.tendsto_comap_iff theorem

{f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ} : Tendsto f a (c.comap g) ↔ Tendsto (g ∘ f) a c

Full source

@[simp]
theorem tendsto_comap_iff {f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ} :
    TendstoTendsto f a (c.comap g) ↔ Tendsto (g ∘ f) a c :=
  ⟨fun h => tendsto_comap.comp h, fun h => map_le_iff_le_comap.mp <| by rwa [map_map]⟩

Equivalence of Tendency Conditions via Composition and Preimage Filter

Informal description

For any function $f \colon \alpha \to \beta$, any function $g \colon \beta \to \gamma$, any filter $a$ on $\alpha$, and any filter $c$ on $\gamma$, the following are equivalent: 1. The function $f$ tends to the preimage filter $\text{comap } g c$ along $a$. 2. The composition $g \circ f$ tends to $c$ along $a$.

Filter.tendsto_comap'_iff theorem

 {m : α → β} {f : Filter α} {g : Filter β} {i : γ → α} (h : range i ∈ f) : Tendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g

Full source

theorem tendsto_comap'_iff {m : α → β} {f : Filter α} {g : Filter β} {i : γ → α} (h : rangerange i ∈ f) :
    TendstoTendsto (m ∘ i) (comap i f) g ↔ Tendsto m f g := by
  rw [Tendsto, ← map_compose]
  simp only [(· ∘ ·), map_comap_of_mem h, Tendsto]

Equivalence of Tendency Conditions via Composition and Preimage Filter with Range Condition

Informal description

Let $m : \alpha \to \beta$ be a function, $f$ a filter on $\alpha$, $g$ a filter on $\beta$, and $i : \gamma \to \alpha$ a function such that the range of $i$ belongs to $f$. Then the following are equivalent: 1. The composition $m \circ i$ tends to $g$ with respect to the preimage filter $\text{comap } i f$ on $\gamma$. 2. The function $m$ tends to $g$ with respect to the filter $f$ on $\alpha$.

Filter.Tendsto.of_tendsto_comp theorem

 {f : α → β} {g : β → γ} {a : Filter α} {b : Filter β} {c : Filter γ} (hfg : Tendsto (g ∘ f) a c) (hg : comap g c ≤ b) :
  Tendsto f a b

Full source

theorem Tendsto.of_tendsto_comp {f : α → β} {g : β → γ} {a : Filter α} {b : Filter β} {c : Filter γ}
    (hfg : Tendsto (g ∘ f) a c) (hg : comap g c ≤ b) : Tendsto f a b := by
  rw [tendsto_iff_comap] at hfg ⊢
  calc
    a ≤ comap (g ∘ f) c := hfg
    _ ≤ comap f b := by simpa [comap_comap] using comap_mono hg

Tendsto Preservation under Composition and Preimage Filter Condition

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be functions, and let $a$ be a filter on $\alpha$, $b$ a filter on $\beta$, and $c$ a filter on $\gamma$. If the composition $g \circ f$ tends to $c$ along $a$ (i.e., $\text{Tendsto } (g \circ f) a c$ holds) and the preimage filter $\text{comap } g c$ is finer than $b$ (i.e., $\text{comap } g c \leq b$), then $f$ tends to $b$ along $a$ (i.e., $\text{Tendsto } f a b$ holds).

Filter.comap_eq_of_inverse theorem

 {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : ψ ∘ φ = id) (hφ : Tendsto φ f g) (hψ : Tendsto ψ g f) :
  comap φ g = f

Full source

theorem comap_eq_of_inverse {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : ψ ∘ φ = id)
    (hφ : Tendsto φ f g) (hψ : Tendsto ψ g f) : comap φ g = f := by
  refine ((comap_mono <| map_le_iff_le_comap.1 hψ).trans ?_).antisymm (map_le_iff_le_comap.1 hφ)
  rw [comap_comap, eq, comap_id]

Preimage Filter Equality via Left Inverse and Tendency Conditions

Informal description

Let $f$ be a filter on $\alpha$, $g$ a filter on $\beta$, and $\varphi \colon \alpha \to \beta$ a function. Suppose there exists a function $\psi \colon \beta \to \alpha$ such that: 1. $\psi \circ \varphi = \text{id}_\alpha$ (i.e., $\psi$ is a left inverse of $\varphi$), 2. $\varphi$ tends to $g$ with respect to $f$ (i.e., $\text{Tendsto } \varphi f g$), 3. $\psi$ tends to $f$ with respect to $g$ (i.e., $\text{Tendsto } \psi g f$). Then the preimage filter of $g$ under $\varphi$ equals $f$, i.e., $\text{comap } \varphi g = f$.

Filter.map_eq_of_inverse theorem

 {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : φ ∘ ψ = id) (hφ : Tendsto φ f g) (hψ : Tendsto ψ g f) :
  map φ f = g

Full source

theorem map_eq_of_inverse {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α) (eq : φ ∘ ψ = id)
    (hφ : Tendsto φ f g) (hψ : Tendsto ψ g f) : map φ f = g := by
  refine le_antisymm hφ (le_trans ?_ (map_mono hψ))
  rw [map_map, eq, map_id]

Image Filter Equality via Left Inverse and Tendsto Conditions

Informal description

Let $f$ be a filter on $\alpha$, $g$ a filter on $\beta$, and $\varphi \colon \alpha \to \beta$ a function. Suppose there exists a function $\psi \colon \beta \to \alpha$ such that: 1. $\varphi \circ \psi = \text{id}_\beta$ (i.e., $\varphi$ is a left inverse of $\psi$), 2. $\varphi$ tends to $g$ with respect to $f$ (i.e., $\text{Tendsto } \varphi f g$), 3. $\psi$ tends to $f$ with respect to $g$ (i.e., $\text{Tendsto } \psi g f$). Then the image filter of $f$ under $\varphi$ equals $g$, i.e., $\text{map } \varphi f = g$.

Filter.tendsto_inf theorem

 {f : α → β} {x : Filter α} {y₁ y₂ : Filter β} : Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂

Full source

theorem tendsto_inf {f : α → β} {x : Filter α} {y₁ y₂ : Filter β} :
    TendstoTendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂ := by
  simp only [Tendsto, le_inf_iff]

Tendsto to Infimum Filter iff Tendsto to Both Filters

Informal description

For any function $f \colon \alpha \to \beta$, a filter $x$ on $\alpha$, and filters $y_1, y_2$ on $\beta$, the following are equivalent: 1. $f$ tends to the infimum filter $y_1 \sqcap y_2$ with respect to $x$. 2. $f$ tends to $y_1$ with respect to $x$ and $f$ tends to $y_2$ with respect to $x$. In other words, $\text{Tendsto } f x (y_1 \sqcap y_2)$ holds if and only if both $\text{Tendsto } f x y_1$ and $\text{Tendsto } f x y_2$ hold.

Filter.tendsto_inf_left theorem

{f : α → β} {x₁ x₂ : Filter α} {y : Filter β} (h : Tendsto f x₁ y) : Tendsto f (x₁ ⊓ x₂) y

Full source

theorem tendsto_inf_left {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} (h : Tendsto f x₁ y) :
    Tendsto f (x₁ ⊓ x₂) y :=
  le_trans (map_mono inf_le_left) h

Tendsto Preserved Under Infimum in Left Argument

Informal description

Let $f \colon \alpha \to \beta$ be a function, and let $x_1, x_2$ be filters on $\alpha$ and $y$ a filter on $\beta$. If $f$ tends to $y$ with respect to $x_1$ (i.e., $\text{Tendsto } f x_1 y$), then $f$ also tends to $y$ with respect to the infimum filter $x_1 \sqcap x_2$.

Filter.tendsto_inf_right theorem

{f : α → β} {x₁ x₂ : Filter α} {y : Filter β} (h : Tendsto f x₂ y) : Tendsto f (x₁ ⊓ x₂) y

Full source

theorem tendsto_inf_right {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} (h : Tendsto f x₂ y) :
    Tendsto f (x₁ ⊓ x₂) y :=
  le_trans (map_mono inf_le_right) h

Tendsto Preserved Under Infimum in Right Argument

Informal description

For any function $f : \alpha \to \beta$ and filters $x_1, x_2$ on $\alpha$ and $y$ on $\beta$, if $f$ tends to $y$ along $x_2$, then $f$ also tends to $y$ along the infimum filter $x_1 \sqcap x_2$.

Filter.Tendsto.inf theorem

 {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β} (h₁ : Tendsto f x₁ y₁) (h₂ : Tendsto f x₂ y₂) :
  Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂)

Full source

theorem Tendsto.inf {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β} (h₁ : Tendsto f x₁ y₁)
    (h₂ : Tendsto f x₂ y₂) : Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂) :=
  tendsto_inf.2 ⟨tendsto_inf_left h₁, tendsto_inf_right h₂⟩

Tendsto Preserves Infima in Both Domain and Codomain Filters

Informal description

Let $f \colon \alpha \to \beta$ be a function, and let $x_1, x_2$ be filters on $\alpha$ and $y_1, y_2$ filters on $\beta$. If $f$ tends to $y_1$ along $x_1$ and $f$ tends to $y_2$ along $x_2$, then $f$ tends to the infimum filter $y_1 \sqcap y_2$ along the infimum filter $x_1 \sqcap x_2$.

Filter.tendsto_iInf theorem

{f : α → β} {x : Filter α} {y : ι → Filter β} : Tendsto f x (⨅ i, y i) ↔ ∀ i, Tendsto f x (y i)

Full source

@[simp]
theorem tendsto_iInf {f : α → β} {x : Filter α} {y : ι → Filter β} :
    TendstoTendsto f x (⨅ i, y i) ↔ ∀ i, Tendsto f x (y i) := by
  simp only [Tendsto, le_iInf_iff]

Characterization of Tendsto to Infimum Filter: $f \to \bigsqcap_i y_i$ iff $\forall i, f \to y_i$

Informal description

For a function $f : \alpha \to \beta$, a filter $x$ on $\alpha$, and a family of filters $(y_i)_{i \in \iota}$ on $\beta$, the following are equivalent: 1. The function $f$ tends to the infimum filter $\bigsqcap_i y_i$ with respect to $x$. 2. For every index $i \in \iota$, the function $f$ tends to $y_i$ with respect to $x$. In other words, $f$ converges to the infimum of the family $(y_i)$ if and only if it converges to each $y_i$ individually.

Filter.tendsto_iInf' theorem

{f : α → β} {x : ι → Filter α} {y : Filter β} (i : ι) (hi : Tendsto f (x i) y) : Tendsto f (⨅ i, x i) y

Full source

theorem tendsto_iInf' {f : α → β} {x : ι → Filter α} {y : Filter β} (i : ι)
    (hi : Tendsto f (x i) y) : Tendsto f (⨅ i, x i) y :=
  hi.mono_left <| iInf_le _ _

Tendsto Preserved Under Infimum of Filters

Informal description

Let $f \colon \alpha \to \beta$ be a function, $\{x_i\}_{i \in \iota}$ a family of filters on $\alpha$, and $y$ a filter on $\beta$. If for some index $i \in \iota$, the function $f$ tends to $y$ along the filter $x_i$, then $f$ tends to $y$ along the infimum filter $\bigsqcap_i x_i$.

Filter.tendsto_iInf_iInf theorem

 {f : α → β} {x : ι → Filter α} {y : ι → Filter β} (h : ∀ i, Tendsto f (x i) (y i)) : Tendsto f (iInf x) (iInf y)

Full source

theorem tendsto_iInf_iInf {f : α → β} {x : ι → Filter α} {y : ι → Filter β}
    (h : ∀ i, Tendsto f (x i) (y i)) : Tendsto f (iInf x) (iInf y) :=
  tendsto_iInf.2 fun i => tendsto_iInf' i (h i)

Tendsto Preserves Infimum of Filters: $f \colon \bigsqcap_i x_i \to \bigsqcap_i y_i$ when $\forall i, f \colon x_i \to y_i$

Informal description

Let $f \colon \alpha \to \beta$ be a function, and let $\{x_i\}_{i \in \iota}$ and $\{y_i\}_{i \in \iota}$ be families of filters on $\alpha$ and $\beta$ respectively. If for every index $i \in \iota$, the function $f$ tends to $y_i$ along the filter $x_i$, then $f$ tends to the infimum filter $\bigsqcap_i y_i$ along the infimum filter $\bigsqcap_i x_i$.

Filter.tendsto_sup theorem

 {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} : Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y

Full source

@[simp]
theorem tendsto_sup {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} :
    TendstoTendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y := by
  simp only [Tendsto, map_sup, sup_le_iff]

Tendsto Condition for Supremum of Filters: $f \text{ tends to } y \text{ along } x_1 \sqcup x_2 \leftrightarrow (f \text{ tends to } y \text{ along } x_1) \land (f \text{ tends to } y \text{ along } x_2)$

Informal description

For any function $f \colon \alpha \to \beta$ and filters $x_1, x_2$ on $\alpha$ and $y$ on $\beta$, the function $f$ tends to $y$ along the supremum filter $x_1 \sqcup x_2$ if and only if $f$ tends to $y$ along both $x_1$ and $x_2$ individually. In other words: $$f \text{ tends to } y \text{ along } x_1 \sqcup x_2 \leftrightarrow (f \text{ tends to } y \text{ along } x_1) \land (f \text{ tends to } y \text{ along } x_2).$$

Filter.Tendsto.sup theorem

 {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} : Tendsto f x₁ y → Tendsto f x₂ y → Tendsto f (x₁ ⊔ x₂) y

Full source

theorem Tendsto.sup {f : α → β} {x₁ x₂ : Filter α} {y : Filter β} :
    Tendsto f x₁ y → Tendsto f x₂ y → Tendsto f (x₁ ⊔ x₂) y := fun h₁ h₂ => tendsto_sup.mpr ⟨h₁, h₂⟩

Tendsto Preserves Supremum of Filters: $f \colon x_1 \sqcup x_2 \to y$ when $f \colon x_1 \to y$ and $f \colon x_2 \to y$

Informal description

For any function $f \colon \alpha \to \beta$ and filters $x_1, x_2$ on $\alpha$ and $y$ on $\beta$, if $f$ tends to $y$ along $x_1$ and $f$ tends to $y$ along $x_2$, then $f$ tends to $y$ along the supremum filter $x_1 \sqcup x_2$.

Filter.Tendsto.sup_sup theorem

 {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β} (h₁ : Tendsto f x₁ y₁) (h₂ : Tendsto f x₂ y₂) :
  Tendsto f (x₁ ⊔ x₂) (y₁ ⊔ y₂)

Full source

theorem Tendsto.sup_sup {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β}
    (h₁ : Tendsto f x₁ y₁) (h₂ : Tendsto f x₂ y₂) : Tendsto f (x₁ ⊔ x₂) (y₁ ⊔ y₂) :=
  tendsto_sup.mpr ⟨h₁.mono_right le_sup_left, h₂.mono_right le_sup_right⟩

Tendsto preserves suprema in both domain and codomain filters

Informal description

For any function $f \colon \alpha \to \beta$ and filters $x_1, x_2$ on $\alpha$ and $y_1, y_2$ on $\beta$, if $f$ tends to $y_1$ along $x_1$ and $f$ tends to $y_2$ along $x_2$, then $f$ tends to $y_1 \sqcup y_2$ along $x_1 \sqcup x_2$.

Filter.tendsto_iSup theorem

{f : α → β} {x : ι → Filter α} {y : Filter β} : Tendsto f (⨆ i, x i) y ↔ ∀ i, Tendsto f (x i) y

Full source

@[simp]
theorem tendsto_iSup {f : α → β} {x : ι → Filter α} {y : Filter β} :
    TendstoTendsto f (⨆ i, x i) y ↔ ∀ i, Tendsto f (x i) y := by simp only [Tendsto, map_iSup, iSup_le_iff]

Characterization of Tendsto with Respect to Supremum of Filters: $f \to y$ along $\bigsqcup_i x_i$ $\leftrightarrow$ $\forall i, f \to y$ along $x_i$

Informal description

For a function $f : \alpha \to \beta$, a family of filters $\{x_i\}_{i \in \iota}$ on $\alpha$, and a filter $y$ on $\beta$, the following are equivalent: 1. The function $f$ tends to $y$ with respect to the supremum filter $\bigsqcup_i x_i$. 2. For every index $i \in \iota$, the function $f$ tends to $y$ with respect to the filter $x_i$.

Filter.tendsto_iSup_iSup theorem

 {f : α → β} {x : ι → Filter α} {y : ι → Filter β} (h : ∀ i, Tendsto f (x i) (y i)) : Tendsto f (iSup x) (iSup y)

Full source

theorem tendsto_iSup_iSup {f : α → β} {x : ι → Filter α} {y : ι → Filter β}
    (h : ∀ i, Tendsto f (x i) (y i)) : Tendsto f (iSup x) (iSup y) :=
  tendsto_iSup.2 fun i => (h i).mono_right <| le_iSup _ _

Tendsto Preserves Suprema of Filters: $f \to \bigsqcup_i y_i$ along $\bigsqcup_i x_i$ given $\forall i, f \to y_i$ along $x_i$

Informal description

For a function $f : \alpha \to \beta$ and families of filters $\{x_i\}_{i \in \iota}$ on $\alpha$ and $\{y_i\}_{i \in \iota}$ on $\beta$, if for every index $i \in \iota$ the function $f$ tends to $y_i$ with respect to $x_i$, then $f$ tends to the supremum filter $\bigsqcup_i y_i$ with respect to the supremum filter $\bigsqcup_i x_i$.

Filter.tendsto_principal theorem

{f : α → β} {l : Filter α} {s : Set β} : Tendsto f l (𝓟 s) ↔ ∀ᶠ a in l, f a ∈ s

Full source

@[simp] theorem tendsto_principal {f : α → β} {l : Filter α} {s : Set β} :
    TendstoTendsto f l (𝓟 s) ↔ ∀ᶠ a in l, f a ∈ s := by
  simp only [Tendsto, le_principal_iff, mem_map', Filter.Eventually]

Characterization of Tendsto with Respect to Principal Filter: $f \to \mathfrak{P}(s) \leftrightarrow \forall^l a, f(a) \in s$

Informal description

For a function $f : \alpha \to \beta$, a filter $l$ on $\alpha$, and a subset $s \subseteq \beta$, the following are equivalent: 1. The function $f$ tends to the principal filter $\mathfrak{P}(s)$ (i.e., the filter of all supersets of $s$) with respect to $l$. 2. The set $\{a \in \alpha \mid f(a) \in s\}$ belongs to the filter $l$ (i.e., $f(a) \in s$ holds "eventually" with respect to $l$).

Filter.tendsto_principal_principal theorem

{f : α → β} {s : Set α} {t : Set β} : Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t

Full source

theorem tendsto_principal_principal {f : α → β} {s : Set α} {t : Set β} :
    TendstoTendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t := by
  simp

Tendsto Condition for Principal Filters: $\text{Tendsto}\, f\, (\text{principal}\, s)\, (\text{principal}\, t) \leftrightarrow (\forall a \in s, f(a) \in t)$

Informal description

For any function $f : \alpha \to \beta$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the function $f$ tends to the principal filter generated by $t$ with respect to the principal filter generated by $s$ if and only if for every $a \in s$, the image $f(a)$ belongs to $t$. In other words, $\text{Tendsto}\, f\, (\text{principal}\, s)\, (\text{principal}\, t) \leftrightarrow (\forall a \in s, f(a) \in t)$.

Filter.tendsto_pure theorem

{f : α → β} {a : Filter α} {b : β} : Tendsto f a (pure b) ↔ ∀ᶠ x in a, f x = b

Full source

@[simp] theorem tendsto_pure {f : α → β} {a : Filter α} {b : β} :
    TendstoTendsto f a (pure b) ↔ ∀ᶠ x in a, f x = b := by
  simp only [Tendsto, le_pure_iff, mem_map', mem_singleton_iff, Filter.Eventually]

Characterization of Tendsto with Respect to a Singleton Filter

Informal description

For a function $f : \alpha \to \beta$, a filter $a$ on $\alpha$, and an element $b \in \beta$, the following are equivalent: 1. The function $f$ tends to $b$ with respect to the filters $a$ and $\text{pure } b$ (the principal filter generated by $\{b\}$). 2. The set of points $x \in \alpha$ such that $f(x) = b$ belongs to the filter $a$. In other words, $f$ tends to $b$ with respect to $a$ and $\text{pure } b$ if and only if $f(x) = b$ holds for all $x$ in some set belonging to $a$.

Filter.tendsto_pure_pure theorem

(f : α → β) (a : α) : Tendsto f (pure a) (pure (f a))

Full source

theorem tendsto_pure_pure (f : α → β) (a : α) : Tendsto f (pure a) (pure (f a)) :=
  tendsto_pure.2 rfl

Limit of a Function at a Point with Singleton Filters: $\lim_{x \to a} f(x) = f(a)$

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the function $f$ tends to $f(a)$ with respect to the principal filter $\{a\}$ on $\alpha$ and the principal filter $\{f(a)\}$ on $\beta$. In other words, the limit of $f$ at $a$ (with respect to the singleton filters) is $f(a)$.

Filter.tendsto_const_pure theorem

{a : Filter α} {b : β} : Tendsto (fun _ => b) a (pure b)

Full source

theorem tendsto_const_pure {a : Filter α} {b : β} : Tendsto (fun _ => b) a (pure b) :=
  tendsto_pure.2 <| univ_mem' fun _ => rfl

Constant Function Tends to Its Value in Principal Filter

Informal description

For any filter $a$ on a type $\alpha$ and any element $b$ of type $\beta$, the constant function $f(x) = b$ tends to $b$ with respect to the filters $a$ and the principal filter $\{b\}$ (i.e., $\text{Tendsto}\, (\lambda x.\, b)\, a\, (\text{pure}\, b)$ holds).

Filter.pure_le_iff theorem

{a : α} {l : Filter α} : pure a ≤ l ↔ ∀ s ∈ l, a ∈ s

Full source

theorem pure_le_iff {a : α} {l : Filter α} : purepure a ≤ l ↔ ∀ s ∈ l, a ∈ s :=
  Iff.rfl

Principal Filter Containment Criterion: $\{a\} \subseteq l \leftrightarrow \forall s \in l, a \in s$

Informal description

For any element $a$ of type $\alpha$ and any filter $l$ on $\alpha$, the principal filter $\{a\}$ is contained in $l$ if and only if every set $s$ in $l$ contains $a$. In other words, $\{a\} \subseteq l \leftrightarrow \forall s \in l, a \in s$.

Filter.tendsto_pure_left theorem

{f : α → β} {a : α} {l : Filter β} : Tendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s

Full source

theorem tendsto_pure_left {f : α → β} {a : α} {l : Filter β} :
    TendstoTendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s :=
  Iff.rfl

Characterization of Tendsto at a Point via Pure Filter

Informal description

For a function $f : \alpha \to \beta$, a point $a \in \alpha$, and a filter $l$ on $\beta$, the following are equivalent: 1. The function $f$ tends to $l$ along the filter $\text{pure } a$ (the principal filter generated by $\{a\}$). 2. For every set $s$ in the filter $l$, the image $f(a)$ belongs to $s$. In other words, $\text{Tendsto } f (\text{pure } a) l \leftrightarrow (\forall s \in l, f(a) \in s)$.

Filter.map_inf_principal_preimage theorem

{f : α → β} {s : Set β} {l : Filter α} : map f (l ⊓ 𝓟 (f ⁻¹' s)) = map f l ⊓ 𝓟 s

Full source

@[simp]
theorem map_inf_principal_preimage {f : α → β} {s : Set β} {l : Filter α} :
    map f (l ⊓ 𝓟 (f ⁻¹' s)) = mapmap f l ⊓ 𝓟 s :=
  Filter.ext fun t => by simp only [mem_map', mem_inf_principal, mem_setOf_eq, mem_preimage]

Image Filter of Infimum with Principal Preimage Equals Infimum of Image Filter with Principal Set

Informal description

For any function $f : \alpha \to \beta$, subset $s \subseteq \beta$, and filter $l$ on $\alpha$, the image filter of the infimum of $l$ and the principal filter generated by the preimage $f^{-1}(s)$ is equal to the infimum of the image filter of $l$ and the principal filter generated by $s$. In symbols: $$\text{map } f (l \sqcap \mathcal{P}(f^{-1}(s))) = \text{map } f l \sqcap \mathcal{P}(s)$$

Filter.Tendsto.not_tendsto theorem

 {f : α → β} {a : Filter α} {b₁ b₂ : Filter β} (hf : Tendsto f a b₁) [NeBot a] (hb : Disjoint b₁ b₂) : ¬Tendsto f a b₂

Full source

/-- If two filters are disjoint, then a function cannot tend to both of them along a non-trivial
filter. -/
theorem Tendsto.not_tendsto {f : α → β} {a : Filter α} {b₁ b₂ : Filter β} (hf : Tendsto f a b₁)
    [NeBot a] (hb : Disjoint b₁ b₂) : ¬Tendsto f a b₂ := fun hf' =>
  (tendsto_inf.2 ⟨hf, hf'⟩).neBot.ne hb.eq_bot

Non-convergence to disjoint filters

Informal description

Let $f \colon \alpha \to \beta$ be a function, $a$ a non-trivial filter on $\alpha$, and $b_1, b_2$ filters on $\beta$. If $f$ tends to $b_1$ along $a$ and $b_1$ is disjoint from $b_2$, then $f$ does not tend to $b_2$ along $a$.

Filter.Tendsto.if theorem

 {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {p : α → Prop} [∀ x, Decidable (p x)]
  (h₀ : Tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂) (h₁ : Tendsto g (l₁ ⊓ 𝓟 {x | ¬p x}) l₂) :
  Tendsto (fun x => if p x then f x else g x) l₁ l₂

Full source

protected theorem Tendsto.if {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {p : α → Prop}
    [∀ x, Decidable (p x)] (h₀ : Tendsto f (l₁ ⊓ 𝓟 { x | p x }) l₂)
    (h₁ : Tendsto g (l₁ ⊓ 𝓟 { x | ¬p x }) l₂) :
    Tendsto (fun x => if p x then f x else g x) l₁ l₂ := by
  simp only [tendsto_def, mem_inf_principal] at *
  intro s hs
  filter_upwards [h₀ s hs, h₁ s hs] with x hp₀ hp₁
  rw [mem_preimage]
  split_ifs with h
  exacts [hp₀ h, hp₁ h]

Limit of Piecewise Function via Filter Convergence

Informal description

Let $l_1$ be a filter on a type $\alpha$, $l_2$ a filter on a type $\beta$, and $f, g \colon \alpha \to \beta$ functions. Given a decidable predicate $p \colon \alpha \to \text{Prop}$, if: 1. The function $f$ tends to $l_2$ along the filter $l_1 \sqcap \mathcal{P}\{x \mid p x\}$, and 2. The function $g$ tends to $l_2$ along the filter $l_1 \sqcap \mathcal{P}\{x \mid \neg p x\}$, then the piecewise-defined function $x \mapsto \text{if } p x \text{ then } f x \text{ else } g x$ tends to $l_2$ along $l_1$.

Filter.Tendsto.if' theorem

 {α β : Type*} {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {p : α → Prop} [DecidablePred p] (hf : Tendsto f l₁ l₂)
  (hg : Tendsto g l₁ l₂) : Tendsto (fun a => if p a then f a else g a) l₁ l₂

Full source

protected theorem Tendsto.if' {α β : Type*} {l₁ : Filter α} {l₂ : Filter β} {f g : α → β}
    {p : α → Prop} [DecidablePred p] (hf : Tendsto f l₁ l₂) (hg : Tendsto g l₁ l₂) :
    Tendsto (fun a => if p a then f a else g a) l₁ l₂ :=
  (tendsto_inf_left hf).if (tendsto_inf_left hg)

Convergence of Piecewise Function When Both Cases Converge

Informal description

Let $\alpha$ and $\beta$ be types, $l_1$ a filter on $\alpha$, $l_2$ a filter on $\beta$, and $f, g \colon \alpha \to \beta$ functions. Given a decidable predicate $p \colon \alpha \to \text{Prop}$, if both $f$ and $g$ tend to $l_2$ along $l_1$, then the piecewise-defined function $x \mapsto \text{if } p x \text{ then } f x \text{ else } g x$ also tends to $l_2$ along $l_1$.

Filter.Tendsto.piecewise theorem

 {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {s : Set α} [∀ x, Decidable (x ∈ s)] (h₀ : Tendsto f (l₁ ⊓ 𝓟 s) l₂)
  (h₁ : Tendsto g (l₁ ⊓ 𝓟 sᶜ) l₂) : Tendsto (piecewise s f g) l₁ l₂

Full source

protected theorem Tendsto.piecewise {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {s : Set α}
    [∀ x, Decidable (x ∈ s)] (h₀ : Tendsto f (l₁ ⊓ 𝓟 s) l₂) (h₁ : Tendsto g (l₁ ⊓ 𝓟 sᶜ) l₂) :
    Tendsto (piecewise s f g) l₁ l₂ :=
  Tendsto.if h₀ h₁

Convergence of Piecewise Function via Filter Limits

Informal description

Let $l_1$ be a filter on a type $\alpha$, $l_2$ a filter on a type $\beta$, and $f, g \colon \alpha \to \beta$ functions. Given a decidable subset $s \subseteq \alpha$, if: 1. The function $f$ tends to $l_2$ along the filter $l_1 \sqcap \mathcal{P}(s)$, and 2. The function $g$ tends to $l_2$ along the filter $l_1 \sqcap \mathcal{P}(s^c)$, then the piecewise-defined function $\text{piecewise}\ s\ f\ g$ tends to $l_2$ along $l_1$.

Set.MapsTo.tendsto theorem

{s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) : Filter.Tendsto f (𝓟 s) (𝓟 t)

Full source

theorem Set.MapsTo.tendsto {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) :
    Filter.Tendsto f (𝓟 s) (𝓟 t) :=
  Filter.tendsto_principal_principal.2 h

Mapping to a Set Implies Tendsto with Principal Filters

Informal description

For any function $f : \alpha \to \beta$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, if $f$ maps every element of $s$ into $t$ (i.e., $\forall x \in s, f(x) \in t$), then $f$ tends to the principal filter generated by $t$ with respect to the principal filter generated by $s$.

Filter.EventuallyEq.comp_tendsto theorem

 {l : Filter α} {f : α → β} {f' : α → β} (H : f =ᶠ[l] f') {g : γ → α} {lc : Filter γ} (hg : Tendsto g lc l) :
  f ∘ g =ᶠ[lc] f' ∘ g

Full source

theorem Filter.EventuallyEq.comp_tendsto {l : Filter α} {f : α → β} {f' : α → β}
    (H : f =ᶠ[l] f') {g : γ → α} {lc : Filter γ} (hg : Tendsto g lc l) :
    f ∘ gf ∘ g =ᶠ[lc] f' ∘ g :=
  hg.eventually H

Composition Preserves Eventual Equality under Filter Limits

Informal description

Let $l$ be a filter on a type $\alpha$, and let $f, f' : \alpha \to \beta$ be functions that are eventually equal with respect to $l$ (i.e., $f = f'$ holds on some set in $l$). Let $g : \gamma \to \alpha$ be a function and $lc$ a filter on $\gamma$. If $g$ tends to $l$ along $lc$ (i.e., $\text{Tendsto}\, g\, lc\, l$), then the compositions $f \circ g$ and $f' \circ g$ are eventually equal with respect to $lc$.

Filter.map_mapsTo_Iic_iff_tendsto theorem

{m : α → β} : MapsTo (map m) (Iic F) (Iic G) ↔ Tendsto m F G

Full source

theorem Filter.map_mapsTo_Iic_iff_tendsto {m : α → β} :
    MapsToMapsTo (map m) (Iic F) (Iic G) ↔ Tendsto m F G :=
  ⟨fun hm ↦ hm right_mem_Iic, fun hm _ ↦ hm.mono_left⟩

Equivalence of Filter Map Preservation and Tendsto Condition

Informal description

For any function $m \colon \alpha \to \beta$ and filters $F$ on $\alpha$ and $G$ on $\beta$, the following are equivalent: 1. The image filter map operation $(\text{map } m)$ sends every filter $F' \leq F$ to a filter $G' \leq G$ (i.e., $\text{map } m$ maps the interval $(-\infty, F]$ in the filter lattice to $(-\infty, G]$). 2. The function $m$ tends to $G$ along $F$ (i.e., $\text{Tendsto } m F G$ holds).

Filter.map_mapsTo_Iic_iff_mapsTo theorem

{s : Set α} {t : Set β} {m : α → β} : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 t) ↔ MapsTo m s t

Full source

theorem Filter.map_mapsTo_Iic_iff_mapsTo {s : Set α} {t : Set β} {m : α → β} :
    MapsToMapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 t) ↔ MapsTo m s t := by
  rw [map_mapsTo_Iic_iff_tendsto, tendsto_principal_principal, MapsTo]

Equivalence of Filter Map Preservation and Function Restriction for Principal Filters

Informal description

For any function $m \colon \alpha \to \beta$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the following are equivalent: 1. The image filter map operation $\text{map } m$ sends every principal filter $\text{principal } s'$ with $s' \subseteq s$ to a principal filter $\text{principal } t'$ with $t' \subseteq t$. 2. The function $m$ maps every element of $s$ into $t$ (i.e., $\forall x \in s, m(x) \in t$).