Mathlib.Order.Filter.Interval

Module docstring

{"# Convergence of intervals

Motivation

If a function tends to infinity somewhere, then its derivative is not integrable around this place. One should be careful about this statement: \"somewhere\" could mean a point, but also convergence from the left or from the right, or it could also be infinity, and \"around this place\" will refer to these directed neighborhoods. Therefore, the above theorem has many variants. Instead of stating all these variants, one can look for the common abstraction and have a single version. One has to be careful: if one considers convergence along a sequence, then the function may tend to infinity but have a derivative which is small along the sequence (with big jumps in between), so in the end the derivative may be integrable on a neighborhood of the sequence. What really matters for such calculus issues in terms of derivatives is that whole intervals are included in the sets we consider.

The right common abstraction is provided in this file, as the TendstoIxxClass typeclass. It takes as parameters a class of bounded intervals and two real filters l₁ and l₂. An instance TendstoIxxClass Icc l₁ l₂ registers that, if aₙ and bₙ are converging towards the filter l₁, then the intervals Icc aₙ bₙ are eventually contained in any given set belonging to l₂. For instance, for l₁ = 𝓝[>] x and l₂ = 𝓝[≥] x, the strict and large right neighborhoods of x respectively, then given any large right neighborhood s ∈ 𝓝[≥] x and any two sequences xₙ and yₙ converging strictly to the right of x, then the interval [xₙ, yₙ] is eventually contained in s. Therefore, the instance TendstoIxxClass Icc (𝓝[>] x) (𝓝[≥] x) holds. Note that one could have taken as well l₂ = 𝓝[>] x, but that l₁ = 𝓝[≥] x and l₂ = 𝓝[>] x wouldn't work.

With this formalism, the above theorem would read: if TendstoIxxClass Icc l l and f tends to infinity along l, then its derivative is not integrable on any element of l. Beyond this simple example, this typeclass plays a prominent role in generic formulations of the fundamental theorem of calculus.

Main definition

If both a and b tend to some filter l₁, sometimes this implies that Ixx a b tends to l₂.smallSets, i.e., for any s ∈ l₂ eventually Ixx a b becomes a subset of s. Here and below Ixx is one of Set.Icc, Set.Ico, Set.Ioc, and Set.Ioo. We define Filter.TendstoIxxClass Ixx l₁ l₂ to be a typeclass representing this property.

The instances provide the best l₂ for a given l₁. In many cases l₁ = l₂ but sometimes we can drop an endpoint from an interval: e.g., we prove Filter.TendstoIxxClass Set.Ico (𝓟 (Set.Iic a)) (𝓟 (Set.Iio a)), i.e., if u₁ n and u₂ n belong eventually to Set.Iic a, then the interval Set.Ico (u₁ n) (u₂ n) is eventually included in Set.Iio a.

The next table shows “output” filters l₂ for different values of Ixx and l₁. The instances that need topology are defined in Mathlib/Topology/Algebra/Ordered.

Filter.TendstoIxxClass structure

(Ixx : α → α → Set α) (l₁ : Filter α) (l₂ : outParam <| Filter α)

Full source

/-- A pair of filters `l₁`, `l₂` has `TendstoIxxClass Ixx` property if `Ixx a b` tends to
`l₂.small_sets` as `a` and `b` tend to `l₁`. In all instances `Ixx` is one of `Set.Icc`, `Set.Ico`,
`Set.Ioc`, or `Set.Ioo`. The instances provide the best `l₂` for a given `l₁`. In many cases
`l₁ = l₂` but sometimes we can drop an endpoint from an interval: e.g., we prove
`TendstoIxxClass Set.Ico (𝓟 (Set.Iic a)) (𝓟 (Set.Iio a))`, i.e., if `u₁ n` and `u₂ n` belong
eventually to `Set.Iic a`, then the interval `Set.Ico (u₁ n) (u₂ n)` is eventually included in
`Set.Iio a`.

We mark `l₂` as an `outParam` so that Lean can automatically find an appropriate `l₂` based on
`Ixx` and `l₁`. This way, e.g., `tendsto.Ico h₁ h₂` works without specifying explicitly `l₂`. -/
class TendstoIxxClass (Ixx : α → α → Set α) (l₁ : Filter α) (l₂ : outParam <| Filter α) : Prop where
  /-- `Function.uncurry Ixx` tends to `l₂.smallSets` along `l₁ ×ˢ l₁`. In other words, for any
  `s ∈ l₂` there exists `t ∈ l₁` such that `Ixx x y ⊆ s` whenever `x ∈ t` and `y ∈ t`.

  Use lemmas like `Filter.Tendsto.Icc` instead. -/
  tendsto_Ixx : Tendsto (fun p : α × α => Ixx p.1 p.2) (l₁ ×ˢ l₁) l₂.smallSets

Convergence of intervals to a filter

Informal description

Given a type $\alpha$ and a function `Ixx` that maps two elements of $\alpha$ to a subset of $\alpha$ (typically representing an interval like `Icc`, `Ico`, `Ioc`, or `Ioo`), the structure `TendstoIxxClass Ixx l₁ l₂` captures the property that as two sequences $a_n$ and $b_n$ converge to the filter $l₁$, the sets `Ixx a_n b_n` eventually lie within any set belonging to the filter $l₂$. In other words, for any $s \in l₂$, there exists a point beyond which all intervals `Ixx a_n b_n` are contained in $s$. The filter $l₂$ is automatically inferred based on $Ixx$ and $l₁$ in most cases.

Filter.tendstoIxxClass_principal theorem

 {s t : Set α} {Ixx : α → α → Set α} : TendstoIxxClass Ixx (𝓟 s) (𝓟 t) ↔ ∀ᵉ (x ∈ s) (y ∈ s), Ixx x y ⊆ t

Full source

theorem tendstoIxxClass_principal {s t : Set α} {Ixx : α → α → Set α} :
    TendstoIxxClassTendstoIxxClass Ixx (𝓟 s) (𝓟 t) ↔ ∀ᵉ (x ∈ s) (y ∈ s), Ixx x y ⊆ t :=
  Iff.trans ⟨fun h => h.1, fun h => ⟨h⟩⟩ <| by
    simp only [smallSets_principal, prod_principal_principal, tendsto_principal_principal,
      forall_prod_set, mem_powerset_iff, mem_principal]

Characterization of Interval Convergence for Principal Filters: $Ixx$ Preserves Convergence iff Intervals are Contained

Informal description

For any sets $s$ and $t$ in a type $\alpha$ and any interval constructor $Ixx : \alpha \to \alpha \to \text{Set } \alpha$, the following are equivalent: 1. The interval constructor $Ixx$ satisfies the `TendstoIxxClass` property with respect to the principal filters $\mathcal{P}(s)$ and $\mathcal{P}(t)$. 2. For all $x, y \in s$, the interval $Ixx(x, y)$ is a subset of $t$. In other words, $Ixx$ preserves convergence to $\mathcal{P}(t)$ when applied to sequences converging to $\mathcal{P}(s)$ if and only if every interval constructed from elements of $s$ lies entirely within $t$.

Filter.tendstoIxxClass_inf theorem

 {l₁ l₁' l₂ l₂' : Filter α} {Ixx} [h : TendstoIxxClass Ixx l₁ l₂] [h' : TendstoIxxClass Ixx l₁' l₂'] :
  TendstoIxxClass Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂')

Full source

theorem tendstoIxxClass_inf {l₁ l₁' l₂ l₂' : Filter α} {Ixx} [h : TendstoIxxClass Ixx l₁ l₂]
    [h' : TendstoIxxClass Ixx l₁' l₂'] : TendstoIxxClass Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂') :=
  ⟨by simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1⟩

Preservation of Interval Convergence Under Filter Infima

Informal description

Let $Ixx$ be a function that maps two elements of a type $\alpha$ to a subset of $\alpha$ (typically an interval construction like $Icc$, $Ico$, $Ioc$, or $Ioo$). Given two pairs of filters $(l_1, l_2)$ and $(l_1', l_2')$ on $\alpha$ such that $TendstoIxxClass$ holds for $Ixx$ with respect to both pairs, then $TendstoIxxClass$ also holds for $Ixx$ with respect to the infima filters $(l_1 \sqcap l_1', l_2 \sqcap l_2')$. In other words, if for any sequences $(a_n)$ and $(b_n)$ converging to $l_1$ (resp. $l_1'$), the sets $Ixx a_n b_n$ are eventually contained in any set of $l_2$ (resp. $l_2'$), then for sequences converging to $l_1 \sqcap l_1'$, the sets $Ixx a_n b_n$ will eventually be contained in any set of $l_2 \sqcap l_2'$.

Filter.tendstoIxxClass_of_subset theorem

 {l₁ l₂ : Filter α} {Ixx Ixx' : α → α → Set α} (h : ∀ a b, Ixx a b ⊆ Ixx' a b) [h' : TendstoIxxClass Ixx' l₁ l₂] :
  TendstoIxxClass Ixx l₁ l₂

Full source

theorem tendstoIxxClass_of_subset {l₁ l₂ : Filter α} {Ixx Ixx' : α → α → Set α}
    (h : ∀ a b, Ixx a b ⊆ Ixx' a b) [h' : TendstoIxxClass Ixx' l₁ l₂] : TendstoIxxClass Ixx l₁ l₂ :=
  ⟨h'.1.smallSets_mono <| Eventually.of_forall <| Prod.forall.2 h⟩

Subset Preservation of Interval Convergence in Filters

Informal description

Let $l₁$ and $l₂$ be filters on a type $\alpha$, and let $Ixx$ and $Ixx'$ be functions from $\alpha \times \alpha$ to $\text{Set } \alpha$ such that for all $a, b \in \alpha$, the set $Ixx(a, b)$ is a subset of $Ixx'(a, b)$. If there exists an instance of `TendstoIxxClass Ixx' l₁ l₂`, then there also exists an instance of `TendstoIxxClass Ixx l₁ l₂$.

Filter.HasBasis.tendstoIxxClass theorem

 {ι : Type*} {p : ι → Prop} {s} {l : Filter α} (hl : l.HasBasis p s) {Ixx : α → α → Set α}
  (H : ∀ i, p i → ∀ x ∈ s i, ∀ y ∈ s i, Ixx x y ⊆ s i) : TendstoIxxClass Ixx l l

Full source

theorem HasBasis.tendstoIxxClass {ι : Type*} {p : ι → Prop} {s} {l : Filter α}
    (hl : l.HasBasis p s) {Ixx : α → α → Set α}
    (H : ∀ i, p i → ∀ x ∈ s i, ∀ y ∈ s i, Ixx x y ⊆ s i) : TendstoIxxClass Ixx l l :=
  ⟨(hl.prod_self.tendsto_iff hl.smallSets).2 fun i hi => ⟨i, hi, fun _ h => H i hi _ h.1 _ h.2⟩⟩

Basis Criterion for Interval Convergence to a Filter

Informal description

Let $\alpha$ be a type, $l$ a filter on $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p_i$, and $Ixx : \alpha \to \alpha \to \text{Set } \alpha$ an interval constructor (such as $Icc$, $Ico$, $Ioc$, or $Ioo$). If for every index $i$ satisfying $p_i$ and any two elements $x, y \in s_i$, the interval $Ixx(x, y)$ is contained in $s_i$, then the `TendstoIxxClass Ixx l l` instance holds. This means that for any sequences $a_n$ and $b_n$ converging to $l$, the intervals $Ixx(a_n, b_n)$ eventually lie within any set belonging to $l$.

Filter.Tendsto.Icc theorem

 {l₁ l₂ : Filter α} [TendstoIxxClass Icc l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁)
  (h₂ : Tendsto u₂ lb l₁) : Tendsto (fun x => Icc (u₁ x) (u₂ x)) lb l₂.smallSets

Full source

protected theorem Tendsto.Icc {l₁ l₂ : Filter α} [TendstoIxxClass Icc l₁ l₂] {lb : Filter β}
    {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) :
    Tendsto (fun x => Icc (u₁ x) (u₂ x)) lb l₂.smallSets :=
  (@TendstoIxxClass.tendsto_Ixx α Set.Icc _ _ _).comp <| h₁.prodMk h₂

Convergence of Closed Intervals under Filter Limits

Informal description

Let $\alpha$ and $\beta$ be types with $l_1$ and $l_2$ filters on $\alpha$, and $lb$ a filter on $\beta$. Suppose that the `TendstoIxxClass Icc l₁ l₂` instance holds, meaning that for any sequences $a_n$ and $b_n$ converging to $l_1$, the closed intervals $[a_n, b_n]$ eventually lie in any set belonging to $l_2$. Given functions $u_1, u_2 : \beta \to \alpha$ such that $u_1$ and $u_2$ both tend to $l_1$ with respect to $lb$, then the function mapping $x$ to the closed interval $[u_1(x), u_2(x)]$ tends to $l_2.\text{smallSets}$ with respect to $lb$. In other words, for any set $s \in l_2$, the set $\{x \in \beta \mid [u_1(x), u_2(x)] \subseteq s\}$ eventually belongs to $lb$.

Filter.Tendsto.Ioc theorem

 {l₁ l₂ : Filter α} [TendstoIxxClass Ioc l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁)
  (h₂ : Tendsto u₂ lb l₁) : Tendsto (fun x => Ioc (u₁ x) (u₂ x)) lb l₂.smallSets

Full source

protected theorem Tendsto.Ioc {l₁ l₂ : Filter α} [TendstoIxxClass Ioc l₁ l₂] {lb : Filter β}
    {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) :
    Tendsto (fun x => Ioc (u₁ x) (u₂ x)) lb l₂.smallSets :=
  (@TendstoIxxClass.tendsto_Ixx α Set.Ioc _ _ _).comp <| h₁.prodMk h₂

Convergence of left-open right-closed intervals to small sets under filter limits

Informal description

Let $\alpha$ be a type with a preorder, and let $l_1$ and $l_2$ be filters on $\alpha$ such that the `TendstoIxxClass Ioc l₁ l₂` instance holds. Given a filter $lb$ on a type $\beta$ and two functions $u_1, u_2 : \beta \to \alpha$, if both $u_1$ and $u_2$ tend to $l_1$ with respect to $lb$, then the function mapping $x$ to the left-open right-closed interval $\text{Ioc}(u_1(x), u_2(x))$ tends to the filter of small sets of $l_2$ with respect to $lb$. In other words, for any set $s \in l_2$, there exists a set $t \in lb$ such that for all $x \in t$, the interval $\text{Ioc}(u_1(x), u_2(x))$ is contained in $s$.

Filter.Tendsto.Ico theorem

 {l₁ l₂ : Filter α} [TendstoIxxClass Ico l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁)
  (h₂ : Tendsto u₂ lb l₁) : Tendsto (fun x => Ico (u₁ x) (u₂ x)) lb l₂.smallSets

Full source

protected theorem Tendsto.Ico {l₁ l₂ : Filter α} [TendstoIxxClass Ico l₁ l₂] {lb : Filter β}
    {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) :
    Tendsto (fun x => Ico (u₁ x) (u₂ x)) lb l₂.smallSets :=
  (@TendstoIxxClass.tendsto_Ixx α Set.Ico _ _ _).comp <| h₁.prodMk h₂

Convergence of Left-Closed Right-Open Intervals to Small Sets

Informal description

Let $\alpha$ be a type with a preorder, and let $l_1$ and $l_2$ be filters on $\alpha$ such that the `TendstoIxxClass` property holds for the left-closed right-open interval `Ico` with respect to $l_1$ and $l_2$. Given a filter $lb$ on a type $\beta$ and two functions $u_1, u_2 : \beta \to \alpha$ such that $u_1$ tends to $l_1$ and $u_2$ tends to $l_1$ with respect to $lb$, then the function $x \mapsto \text{Ico}(u_1(x), u_2(x))$ tends to the filter of small sets of $l_2$ with respect to $lb$. In other words, for any set $s \in l_2$, there exists a set $t \in lb$ such that for all $x \in t$, the interval $\text{Ico}(u_1(x), u_2(x))$ is a subset of $s$.

Filter.Tendsto.Ioo theorem

 {l₁ l₂ : Filter α} [TendstoIxxClass Ioo l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁)
  (h₂ : Tendsto u₂ lb l₁) : Tendsto (fun x => Ioo (u₁ x) (u₂ x)) lb l₂.smallSets

Full source

protected theorem Tendsto.Ioo {l₁ l₂ : Filter α} [TendstoIxxClass Ioo l₁ l₂] {lb : Filter β}
    {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) :
    Tendsto (fun x => Ioo (u₁ x) (u₂ x)) lb l₂.smallSets :=
  (@TendstoIxxClass.tendsto_Ixx α Set.Ioo _ _ _).comp <| h₁.prodMk h₂

Convergence of Open Intervals to a Filter's Small Sets

Informal description

Let $\alpha$ be a type with a preorder, and let $l_1$, $l_2$ be filters on $\alpha$ such that the `TendstoIxxClass Ioo l₁ l₂` instance holds. Given a filter $lb$ on a type $\beta$ and functions $u_1, u_2 : \beta \to \alpha$ such that $u_1$ and $u_2$ both tend to $l_1$ with respect to $lb$, then the function mapping $x$ to the open interval $(u_1(x), u_2(x))$ tends to $l_2.\text{smallSets}$ with respect to $lb$. In other words, if $u_1$ and $u_2$ converge to $l_1$, then the open intervals $(u_1(x), u_2(x))$ eventually lie within any set belonging to the filter $l_2$.

Filter.tendsto_Icc_atTop_atTop instance

: TendstoIxxClass Icc (atTop : Filter α) atTop

Full source

instance tendsto_Icc_atTop_atTop : TendstoIxxClass Icc (atTop : Filter α) atTop :=
  (hasBasis_iInf_principal_finite _).tendstoIxxClass fun _ _ =>
    Set.OrdConnected.out <| ordConnected_biInter fun _ _ => ordConnected_Ici

Convergence of Closed Intervals to Positive Infinity

Informal description

For any preorder $\alpha$, the filter `atTop` (representing convergence to positive infinity) satisfies the `TendstoIxxClass` property for closed intervals `Icc`. This means that if two sequences $a_n$ and $b_n$ tend to `atTop`, then the closed intervals $[a_n, b_n]$ eventually lie within any set belonging to `atTop`.

Filter.tendsto_Ico_atTop_atTop instance

: TendstoIxxClass Ico (atTop : Filter α) atTop

Full source

instance tendsto_Ico_atTop_atTop : TendstoIxxClass Ico (atTop : Filter α) atTop :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Convergence of Left-Closed Right-Open Intervals to Positive Infinity

Informal description

For any preorder $\alpha$, the filter `atTop` (representing convergence to positive infinity) satisfies the `TendstoIxxClass` property for left-closed right-open intervals `Ico`. This means that if two sequences $a_n$ and $b_n$ tend to `atTop`, then the intervals $[a_n, b_n)$ eventually lie within any set belonging to `atTop$.

Filter.tendsto_Ioc_atTop_atTop instance

: TendstoIxxClass Ioc (atTop : Filter α) atTop

Full source

instance tendsto_Ioc_atTop_atTop : TendstoIxxClass Ioc (atTop : Filter α) atTop :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Convergence of Left-Open Right-Closed Intervals to Positive Infinity

Informal description

For any preorder $\alpha$, the left-open right-closed interval operation $\mathrm{Ioc}$ satisfies the property that if two sequences $a_n$ and $b_n$ tend to the filter $\mathrm{atTop}$ (positive infinity), then the intervals $(a_n, b_n]$ eventually lie within any set belonging to $\mathrm{atTop}$. In other words, the intervals $(a_n, b_n]$ themselves tend to $\mathrm{atTop}$ in the filter sense.

Filter.tendsto_Ioo_atTop_atTop instance

: TendstoIxxClass Ioo (atTop : Filter α) atTop

Full source

instance tendsto_Ioo_atTop_atTop : TendstoIxxClass Ioo (atTop : Filter α) atTop :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

Convergence of Open Intervals to Positive Infinity

Informal description

For any preorder $\alpha$, the open interval operation $\mathrm{Ioo}$ satisfies the property that if two sequences $a_n$ and $b_n$ tend to the filter $\mathrm{atTop}$ (positive infinity), then the open intervals $(a_n, b_n)$ eventually lie within any set belonging to $\mathrm{atTop}$. In other words, the intervals $(a_n, b_n)$ themselves tend to $\mathrm{atTop}$ in the filter sense.

Filter.tendsto_Icc_atBot_atBot instance

: TendstoIxxClass Icc (atBot : Filter α) atBot

Full source

instance tendsto_Icc_atBot_atBot : TendstoIxxClass Icc (atBot : Filter α) atBot :=
  (hasBasis_iInf_principal_finite _).tendstoIxxClass fun _ _ =>
    Set.OrdConnected.out <| ordConnected_biInter fun _ _ => ordConnected_Iic

Convergence of Closed Intervals to Negative Infinity

Informal description

For any preorder $\alpha$, the closed interval operation $\mathrm{Icc}$ satisfies the property that if two sequences $a_n$ and $b_n$ tend to the filter $\mathrm{atBot}$ (negative infinity), then the closed intervals $[a_n, b_n]$ eventually lie within any set belonging to $\mathrm{atBot}$. In other words, the intervals $[a_n, b_n]$ themselves tend to $\mathrm{atBot}$ in the filter sense.

Filter.tendsto_Ico_atBot_atBot instance

: TendstoIxxClass Ico (atBot : Filter α) atBot

Full source

instance tendsto_Ico_atBot_atBot : TendstoIxxClass Ico (atBot : Filter α) atBot :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Convergence of Left-Closed Right-Open Intervals to Negative Infinity

Informal description

For any preorder $\alpha$, the left-closed right-open interval operation $\mathrm{Ico}$ satisfies the property that if two sequences $a_n$ and $b_n$ tend to the filter $\mathrm{atBot}$ (negative infinity), then the intervals $[a_n, b_n)$ eventually lie within any set belonging to $\mathrm{atBot}$. In other words, the intervals $[a_n, b_n)$ themselves tend to $\mathrm{atBot}$ in the filter sense.

Filter.tendsto_Ioc_atBot_atBot instance

: TendstoIxxClass Ioc (atBot : Filter α) atBot

Full source

instance tendsto_Ioc_atBot_atBot : TendstoIxxClass Ioc (atBot : Filter α) atBot :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Convergence of Left-Open Right-Closed Intervals to Negative Infinity

Informal description

For any preorder $\alpha$, the left-open right-closed interval operation $\mathrm{Ioc}$ satisfies the property that if two sequences $a_n$ and $b_n$ tend to the filter $\mathrm{atBot}$ (negative infinity), then the intervals $(a_n, b_n]$ eventually lie within any set belonging to $\mathrm{atBot}$. In other words, the intervals $(a_n, b_n]$ themselves tend to $\mathrm{atBot}$ in the filter sense.

Filter.tendsto_Ioo_atBot_atBot instance

: TendstoIxxClass Ioo (atBot : Filter α) atBot

Full source

instance tendsto_Ioo_atBot_atBot : TendstoIxxClass Ioo (atBot : Filter α) atBot :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

Convergence of Open Intervals to Negative Infinity

Informal description

For any preorder $\alpha$, the open interval operation $\mathrm{Ioo}$ satisfies the property that if two sequences $a_n$ and $b_n$ tend to the filter $\mathrm{atBot}$ (negative infinity), then the open intervals $(a_n, b_n)$ eventually lie within any set belonging to $\mathrm{atBot}$. In other words, the intervals $(a_n, b_n)$ themselves tend to $\mathrm{atBot}$ in the filter sense.

Filter.OrdConnected.tendsto_Icc instance

{s : Set α} [hs : OrdConnected s] : TendstoIxxClass Icc (𝓟 s) (𝓟 s)

Full source

instance OrdConnected.tendsto_Icc {s : Set α} [hs : OrdConnected s] :
    TendstoIxxClass Icc (𝓟 s) (𝓟 s) :=
  tendstoIxxClass_principal.2 hs.out

Convergence of Intervals in Order-Connected Sets

Informal description

For any order-connected set $s$ in a preorder $\alpha$, the closed interval operation $\mathrm{Icc}$ satisfies the convergence property that for any two sequences $(a_n)$ and $(b_n)$ in $s$ converging to the principal filter $\mathcal{P}(s)$, the intervals $[a_n, b_n]$ eventually lie within any subset of $s$ in $\mathcal{P}(s)$. In other words, if $s$ is order-connected (meaning for any $x, y \in s$ we have $[x, y] \subseteq s$), then the intervals formed by pairs of elements in $s$ will always remain within $s$ as the elements vary within $s$.

Filter.tendsto_Ico_Ici_Ici instance

{a : α} : TendstoIxxClass Ico (𝓟 (Ici a)) (𝓟 (Ici a))

Full source

instance tendsto_Ico_Ici_Ici {a : α} : TendstoIxxClass Ico (𝓟 (Ici a)) (𝓟 (Ici a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Convergence of Left-Closed Right-Open Intervals in $[a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-open interval constructor $\operatorname{Ico}$ satisfies the property that for any two sequences converging to the principal filter of the left-closed right-infinite interval $[a, \infty)$, the intervals $\operatorname{Ico}(x_n, y_n)$ eventually lie within any set in the principal filter of $[a, \infty)$. In other words, if $x_n, y_n \in [a, \infty)$ for all sufficiently large $n$, then $\operatorname{Ico}(x_n, y_n) \subseteq [a, \infty)$ for all sufficiently large $n$.

Filter.tendsto_Ico_Ioi_Ioi instance

{a : α} : TendstoIxxClass Ico (𝓟 (Ioi a)) (𝓟 (Ioi a))

Full source

instance tendsto_Ico_Ioi_Ioi {a : α} : TendstoIxxClass Ico (𝓟 (Ioi a)) (𝓟 (Ioi a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Convergence of Left-Closed Right-Open Intervals in $(a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-open interval constructor $\operatorname{Ico}$ satisfies the property that for any two sequences converging to the principal filter of the left-open right-infinite interval $(a, \infty)$, the intervals $\operatorname{Ico}(x_n, y_n)$ eventually lie within any set in the principal filter of $(a, \infty)$. In other words, if $x_n, y_n \in (a, \infty)$ for all sufficiently large $n$, then $\operatorname{Ico}(x_n, y_n) \subseteq (a, \infty)$ for all sufficiently large $n$.

Filter.tendsto_Ico_Iic_Iio instance

{a : α} : TendstoIxxClass Ico (𝓟 (Iic a)) (𝓟 (Iio a))

Full source

instance tendsto_Ico_Iic_Iio {a : α} : TendstoIxxClass Ico (𝓟 (Iic a)) (𝓟 (Iio a)) :=
  tendstoIxxClass_principal.2 fun _ _ _ h₁ _ h₂ => lt_of_lt_of_le h₂.2 h₁

Convergence of Left-Closed Right-Open Intervals from $(-\infty, a]$ to $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-open interval constructor $\operatorname{Ico}$ satisfies the property that for any two sequences converging to the principal filter of the left-infinite right-closed interval $(-\infty, a]$, the intervals $\operatorname{Ico}(x_n, y_n)$ eventually lie within any set in the principal filter of the left-infinite right-open interval $(-\infty, a)$. In other words, if $x_n, y_n \in (-\infty, a]$ for all sufficiently large $n$, then $\operatorname{Ico}(x_n, y_n) \subseteq (-\infty, a)$ for all sufficiently large $n$.

Filter.tendsto_Ico_Iio_Iio instance

{a : α} : TendstoIxxClass Ico (𝓟 (Iio a)) (𝓟 (Iio a))

Full source

instance tendsto_Ico_Iio_Iio {a : α} : TendstoIxxClass Ico (𝓟 (Iio a)) (𝓟 (Iio a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Convergence of Left-Closed Right-Open Intervals in $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-open interval constructor $\operatorname{Ico}$ satisfies the property that for any two sequences converging to the principal filter of the left-infinite right-open interval $(-\infty, a)$, the intervals $\operatorname{Ico}(x_n, y_n)$ eventually lie within any set in the principal filter of $(-\infty, a)$. In other words, if $x_n, y_n \in (-\infty, a)$ for all sufficiently large $n$, then $\operatorname{Ico}(x_n, y_n) \subseteq (-\infty, a)$ for all sufficiently large $n$.

Filter.tendsto_Ioc_Ici_Ioi instance

{a : α} : TendstoIxxClass Ioc (𝓟 (Ici a)) (𝓟 (Ioi a))

Full source

instance tendsto_Ioc_Ici_Ioi {a : α} : TendstoIxxClass Ioc (𝓟 (Ici a)) (𝓟 (Ioi a)) :=
  tendstoIxxClass_principal.2 fun _ h₁ _ _ _ h₂ => lt_of_le_of_lt h₁ h₂.1

Convergence of Left-Open Right-Closed Intervals from $[a, \infty)$ to $(a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-closed interval constructor $\text{Ioc}$ satisfies the convergence property that if two sequences converge to the principal filter generated by the left-closed right-infinite interval $[a, \infty)$, then the intervals $\text{Ioc}(x_n, y_n)$ eventually lie within any set belonging to the principal filter generated by the left-open right-infinite interval $(a, \infty)$. In other words, for any $x, y \in [a, \infty)$, the interval $\text{Ioc}(x, y)$ is contained in $(a, \infty)$.

Filter.tendsto_Ioc_Iic_Iic instance

{a : α} : TendstoIxxClass Ioc (𝓟 (Iic a)) (𝓟 (Iic a))

Full source

instance tendsto_Ioc_Iic_Iic {a : α} : TendstoIxxClass Ioc (𝓟 (Iic a)) (𝓟 (Iic a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Convergence of Left-Open Right-Closed Intervals in $(-\infty, a]$

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-closed interval constructor $\text{Ioc}$ satisfies the convergence property that if two sequences converge to the principal filter generated by the left-infinite right-closed interval $(-\infty, a]$, then the intervals $\text{Ioc}(x_n, y_n)$ eventually lie within any set belonging to the principal filter generated by $(-\infty, a]$. In other words, for any $x, y \in (-\infty, a]$, the interval $\text{Ioc}(x, y) = (x, y]$ is contained in $(-\infty, a]$.

Filter.tendsto_Ioc_Iio_Iio instance

{a : α} : TendstoIxxClass Ioc (𝓟 (Iio a)) (𝓟 (Iio a))

Full source

instance tendsto_Ioc_Iio_Iio {a : α} : TendstoIxxClass Ioc (𝓟 (Iio a)) (𝓟 (Iio a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Convergence of Left-Open Right-Closed Intervals in $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-closed interval constructor $\text{Ioc}$ satisfies the convergence property that if two sequences converge to the principal filter generated by the left-infinite right-open interval $(-\infty, a)$, then the intervals $\text{Ioc}(x_n, y_n)$ eventually lie within any set belonging to the principal filter generated by $(-\infty, a)$. In other words, for any $x, y \in (-\infty, a)$, the interval $\text{Ioc}(x, y)$ is contained in $(-\infty, a)$.

Filter.tendsto_Ioc_Ioi_Ioi instance

{a : α} : TendstoIxxClass Ioc (𝓟 (Ioi a)) (𝓟 (Ioi a))

Full source

instance tendsto_Ioc_Ioi_Ioi {a : α} : TendstoIxxClass Ioc (𝓟 (Ioi a)) (𝓟 (Ioi a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Convergence of Left-Open Right-Closed Intervals in Open Upper Intervals

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-closed interval operation $\mathrm{Ioc}$ satisfies the convergence property that for any two sequences $(a_n)$ and $(b_n)$ in the open upper interval $(a, \infty)$ converging to the principal filter $\mathcal{P}((a, \infty))$, the intervals $(a_n, b_n]$ eventually lie within any subset of $(a, \infty)$ in $\mathcal{P}((a, \infty))$.

Filter.tendsto_Ioo_Ici_Ioi instance

{a : α} : TendstoIxxClass Ioo (𝓟 (Ici a)) (𝓟 (Ioi a))

Full source

instance tendsto_Ioo_Ici_Ioi {a : α} : TendstoIxxClass Ioo (𝓟 (Ici a)) (𝓟 (Ioi a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ioc_self

Convergence of Open Intervals from $[a, \infty)$ to $(a, \infty)$

Informal description

For any element $a$ in a preorder $\alpha$, the open interval constructor $\text{Ioo}$ satisfies the convergence property that if two sequences converge to the principal filter generated by the left-closed right-infinite interval $[a, \infty)$, then the intervals $\text{Ioo}(x_n, y_n)$ eventually lie within any set belonging to the principal filter generated by the left-open right-infinite interval $(a, \infty)$. In other words, for any $x, y \in [a, \infty)$, the interval $\text{Ioo}(x, y)$ is contained in $(a, \infty)$.

Filter.tendsto_Ioo_Iic_Iio instance

{a : α} : TendstoIxxClass Ioo (𝓟 (Iic a)) (𝓟 (Iio a))

Full source

instance tendsto_Ioo_Iic_Iio {a : α} : TendstoIxxClass Ioo (𝓟 (Iic a)) (𝓟 (Iio a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ico_self

Convergence of Open Intervals from $(-\infty, a]$ to $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the open interval constructor $\operatorname{Ioo}$ satisfies the property that for any two sequences converging to the principal filter of the left-infinite right-closed interval $(-\infty, a]$, the intervals $\operatorname{Ioo}(x_n, y_n)$ eventually lie within any set in the principal filter of the left-infinite right-open interval $(-\infty, a)$. In other words, if $x_n, y_n \in (-\infty, a]$ for all sufficiently large $n$, then $\operatorname{Ioo}(x_n, y_n) \subseteq (-\infty, a)$ for all sufficiently large $n$.

Filter.tendsto_Ioo_Ioi_Ioi instance

{a : α} : TendstoIxxClass Ioo (𝓟 (Ioi a)) (𝓟 (Ioi a))

Full source

instance tendsto_Ioo_Ioi_Ioi {a : α} : TendstoIxxClass Ioo (𝓟 (Ioi a)) (𝓟 (Ioi a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ioc_self

Convergence of Open Intervals in Open Upper Intervals

Informal description

For any element $a$ in a preorder $\alpha$, the open interval constructor $\text{Ioo}$ satisfies the convergence property that if two sequences converge to the principal filter generated by the left-open right-infinite interval $(a, \infty)$, then the intervals $\text{Ioo}(x_n, y_n)$ eventually lie within any set belonging to the principal filter generated by $(a, \infty)$. In other words, for any $x, y \in (a, \infty)$, the interval $\text{Ioo}(x, y)$ is contained in $(a, \infty)$.

Filter.tendsto_Ioo_Iio_Iio instance

{a : α} : TendstoIxxClass Ioo (𝓟 (Iio a)) (𝓟 (Iio a))

Full source

instance tendsto_Ioo_Iio_Iio {a : α} : TendstoIxxClass Ioo (𝓟 (Iio a)) (𝓟 (Iio a)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Ioc_self

Convergence of Open Intervals in $(-\infty, a)$

Informal description

For any element $a$ in a preorder $\alpha$, the open interval constructor $\text{Ioo}$ satisfies the convergence property that if two sequences converge to the principal filter generated by the left-infinite right-open interval $(-\infty, a)$, then the intervals $\text{Ioo}(x_n, y_n)$ eventually lie within any set belonging to the principal filter generated by $(-\infty, a)$. In other words, for any $x, y \in (-\infty, a)$, the open interval $(x, y)$ is contained in $(-\infty, a)$.

Filter.tendsto_Icc_Icc_Icc instance

{a b : α} : TendstoIxxClass Icc (𝓟 (Icc a b)) (𝓟 (Icc a b))

Full source

instance tendsto_Icc_Icc_Icc {a b : α} : TendstoIxxClass Icc (𝓟 (Icc a b)) (𝓟 (Icc a b)) :=
  tendstoIxxClass_principal.mpr fun _x hx _y hy => Icc_subset_Icc hx.1 hy.2

Convergence of Closed Intervals within Closed Intervals

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the interval constructor $\text{Icc}$ (closed intervals) satisfies the convergence property that for any sequences $(x_n)$ and $(y_n)$ converging to the principal filter $\mathcal{P}([a, b])$, the intervals $[x_n, y_n]$ eventually lie within any set belonging to $\mathcal{P}([a, b])$.

Filter.tendsto_Ioc_Icc_Icc instance

{a b : α} : TendstoIxxClass Ioc (𝓟 (Icc a b)) (𝓟 (Icc a b))

Full source

instance tendsto_Ioc_Icc_Icc {a b : α} : TendstoIxxClass Ioc (𝓟 (Icc a b)) (𝓟 (Icc a b)) :=
  tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Convergence of Left-Open Right-Closed Intervals within Closed Intervals

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the left-open right-closed interval constructor $\text{Ioc}$ satisfies the convergence property that for any sequences $(x_n)$ and $(y_n)$ converging to the principal filter $\mathcal{P}([a, b])$, the intervals $(x_n, y_n]$ eventually lie within any set belonging to $\mathcal{P}([a, b])$.

Filter.tendsto_Icc_pure_pure instance

{a : α} : TendstoIxxClass Icc (pure a) (pure a : Filter α)

Full source

instance tendsto_Icc_pure_pure {a : α} : TendstoIxxClass Icc (pure a) (pure a : Filter α) := by
  rw [← principal_singleton]
  exact tendstoIxxClass_principal.2 ordConnected_singleton.out

Convergence of Closed Intervals to a Point

Informal description

For any element $a$ in a preorder $\alpha$, the closed intervals $\text{Icc}(a_n, b_n)$ converge to the singleton $\{a\}$ as $a_n$ and $b_n$ converge to $a$ (with respect to the pure filter). That is, for any sequences $a_n \to a$ and $b_n \to a$, the intervals $\text{Icc}(a_n, b_n)$ are eventually contained in any neighborhood of $a$.

Filter.tendsto_Ico_pure_bot instance

{a : α} : TendstoIxxClass Ico (pure a) ⊥

Full source

instance tendsto_Ico_pure_bot {a : α} : TendstoIxxClass Ico (pure a) ⊥ :=
  ⟨by simp⟩

Convergence of Left-Closed Right-Open Intervals to Empty Set at Point

Informal description

For any element $a$ in a preorder $\alpha$, the left-closed right-open intervals $\text{Ico}(a_n, b_n)$ converge to the empty set as $a_n$ and $b_n$ converge to $a$ (with respect to the pure filter). That is, for any sequences $a_n \to a$ and $b_n \to a$, the intervals $\text{Ico}(a_n, b_n)$ are eventually empty.

Filter.tendsto_Ioc_pure_bot instance

{a : α} : TendstoIxxClass Ioc (pure a) ⊥

Full source

instance tendsto_Ioc_pure_bot {a : α} : TendstoIxxClass Ioc (pure a) ⊥ :=
  ⟨by simp⟩

Convergence of Left-Open Right-Closed Intervals to Empty Set at Point

Informal description

For any element $a$ in a preorder $\alpha$, the left-open right-closed intervals $\text{Ioc}(a_n, b_n)$ converge to the empty set as $a_n$ and $b_n$ converge to $a$ (with respect to the pure filter). That is, for any sequences $a_n \to a$ and $b_n \to a$, the intervals $\text{Ioc}(a_n, b_n)$ are eventually empty.

Filter.tendsto_Ioo_pure_bot instance

{a : α} : TendstoIxxClass Ioo (pure a) ⊥

Full source

instance tendsto_Ioo_pure_bot {a : α} : TendstoIxxClass Ioo (pure a) ⊥ :=
  ⟨by simp⟩

Convergence of Open Intervals to Empty Set at a Point

Informal description

For any element $a$ in a preorder $\alpha$, the open intervals $\text{Ioo}(a_n, b_n)$ converge to the empty set as $a_n$ and $b_n$ converge to $a$ (with respect to the pure filter). That is, for any sequences $a_n \to a$ and $b_n \to a$, the intervals $\text{Ioo}(a_n, b_n)$ are eventually empty.

Filter.tendsto_Icc_uIcc_uIcc instance

{a b : α} : TendstoIxxClass Icc (𝓟 [[a, b]]) (𝓟 [[a, b]])

Full source

instance tendsto_Icc_uIcc_uIcc {a b : α} : TendstoIxxClass Icc (𝓟 [[a, b]]) (𝓟 [[a, b]]) :=
  Filter.tendsto_Icc_Icc_Icc

Convergence of Closed Intervals within Unordered Intervals

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the closed intervals $[x, y]$ converge to the principal filter generated by the unordered interval $[[a, b]]$ as $x$ and $y$ converge to this filter. Specifically, if sequences $(x_n)$ and $(y_n)$ are eventually in $[[a, b]]$, then the intervals $[x_n, y_n]$ are eventually contained in any set belonging to the principal filter $\mathcal{P}([[a, b]])$.

Filter.tendsto_Ioc_uIcc_uIcc instance

{a b : α} : TendstoIxxClass Ioc (𝓟 [[a, b]]) (𝓟 [[a, b]])

Full source

instance tendsto_Ioc_uIcc_uIcc {a b : α} : TendstoIxxClass Ioc (𝓟 [[a, b]]) (𝓟 [[a, b]]) :=
  Filter.tendsto_Ioc_Icc_Icc

Convergence of Left-Open Right-Closed Intervals within Unordered Intervals

Informal description

For any two elements $a$ and $b$ in a lattice $\alpha$, the left-open right-closed intervals $\text{Ioc}(x, y)$ converge to the principal filter generated by the unordered interval $[[a, b]]$ as $x$ and $y$ converge to this filter. Specifically, if sequences $(x_n)$ and $(y_n)$ are eventually in $[[a, b]]$, then the intervals $(x_n, y_n]$ are eventually contained in any set belonging to the principal filter $\mathcal{P}([[a, b]])$.

Filter.tendsto_uIcc_of_Icc instance

{l : Filter α} [TendstoIxxClass Icc l l] : TendstoIxxClass uIcc l l

Full source

instance tendsto_uIcc_of_Icc {l : Filter α} [TendstoIxxClass Icc l l] :
    TendstoIxxClass uIcc l l := by
  refine ⟨fun s hs => mem_map.2 <| mem_prod_self_iff.2 ?_⟩
  obtain ⟨t, htl, hts⟩ : ∃ t ∈ l, ∀ p ∈ (t : Set α) ×ˢ t, Icc (p : α × α).1 p.2 ∈ s :=
    mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs))
  refine ⟨t, htl, fun p hp => ?_⟩
  rcases le_total p.1 p.2 with h | h
  · rw [mem_preimage, uIcc_of_le h]
    exact hts p hp
  · rw [mem_preimage, uIcc_of_ge h]
    exact hts ⟨p.2, p.1⟩ ⟨hp.2, hp.1⟩

Convergence of Unordered Intervals from Closed Intervals

Informal description

For any filter $l$ on a type $\alpha$ with a linear order, if the convergence of closed intervals $[a, b]$ to $l$ implies their eventual containment in any set belonging to $l$ (i.e., `TendstoIxxClass Icc l l` holds), then the same property holds for unordered closed intervals $[[a, b]]$ (i.e., `TendstoIxxClass uIcc l l` holds). In other words, if two sequences $a_n$ and $b_n$ tend to $l$, then the unordered intervals $[[a_n, b_n]]$ eventually lie within any set in $l$.

Filter.Tendsto.uIcc theorem

 {l : Filter α} [TendstoIxxClass Icc l l] {f g : β → α} {lb : Filter β} (hf : Tendsto f lb l) (hg : Tendsto g lb l) :
  Tendsto (fun x => [[f x, g x]]) lb l.smallSets

Full source

protected theorem Tendsto.uIcc {l : Filter α} [TendstoIxxClass Icc l l] {f g : β → α}
    {lb : Filter β} (hf : Tendsto f lb l) (hg : Tendsto g lb l) :
    Tendsto (fun x => [[f x, g x]]) lb l.smallSets :=
  (@TendstoIxxClass.tendsto_Ixx α Set.uIcc _ _ _).comp <| hf.prodMk hg

Convergence of Unordered Intervals under Tendency to a Filter

Informal description

Let $\alpha$ be a type with a linear order, and let $l$ be a filter on $\alpha$ such that the convergence of closed intervals $[a, b]$ to $l$ implies their eventual containment in any set belonging to $l$ (i.e., `TendstoIxxClass Icc l l` holds). For any two functions $f, g : \beta \to \alpha$ and a filter $lb$ on $\beta$, if $f$ and $g$ tend to $l$ with respect to $lb$, then the function mapping $x$ to the unordered closed interval $[[f(x), g(x)]]$ tends to the filter of small sets of $l$ with respect to $lb$. In other words, if $f(x)$ and $g(x)$ converge to $l$ as $x$ tends to $lb$, then the intervals $[[f(x), g(x)]]$ eventually lie within any set in $l$.