# 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`.

Input filter | `Ixx = Set.Icc` | `Ixx = Set.Ico` | `Ixx = Set.Ioc` | `Ixx = Set.Ioo`
--- | --- | --- | --- | ---
`Filter.atTop` | `Filter.atTop` | `Filter.atTop` | `Filter.atTop` | `Filter.atTop`
`Filter.atBot` | `Filter.atBot` | `Filter.atBot` | `Filter.atBot` | `Filter.atBot`
`pure a` | `pure a` | `⊥` | `⊥` | `⊥`
`𝓟 (Set.Iic a)` | `𝓟 (Set.Iic a)` | `𝓟 (Set.Iio a)` | `𝓟 (Set.Iic a)` | `𝓟 (Set.Iio a)`
`𝓟 (Set.Ici a)` | `𝓟 (Set.Ici a)` | `𝓟 (Set.Ici a)` | `𝓟 (Set.Ioi a)` | `𝓟 (Set.Ioi a)`
`𝓟 (Set.Ioi a)` | `𝓟 (Set.Ioi a)` | `𝓟 (Set.Ioi a)` | `𝓟 (Set.Ioi a)` | `𝓟 (Set.Ioi a)`
`𝓟 (Set.Iio a)` | `𝓟 (Set.Iio a)` | `𝓟 (Set.Iio a)` | `𝓟 (Set.Iio a)` | `𝓟 (Set.Iio a)`
`𝓝 a` | `𝓝 a` | `𝓝 a` | `𝓝 a` | `𝓝 a`
`𝓝[Set.Iic a] b` | `𝓝[Set.Iic a] b` | `𝓝[Set.Iio a] b` | `𝓝[Set.Iic a] b` | `𝓝[Set.Iio a] b`
`𝓝[Set.Ici a] b` | `𝓝[Set.Ici a] b` | `𝓝[Set.Ici a] b` | `𝓝[Set.Ioi a] b` | `𝓝[Set.Ioi a] b`
`𝓝[Set.Ioi a] b` | `𝓝[Set.Ioi a] b` | `𝓝[Set.Ioi a] b` | `𝓝[Set.Ioi a] b` | `𝓝[Set.Ioi a] b`
`𝓝[Set.Iio a] b` | `𝓝[Set.Iio a] b` | `𝓝[Set.Iio a] b` | `𝓝[Set.Iio a] b` | `𝓝[Set.Iio a] b`

source
class Filter.TendstoIxxClass {α : Type u_1} (Ixx : α → α → Set α) (l₁ : Filter α) (l₂ : outParam (Filter α)) :
Prop

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₂`.

- tendsto_Ixx : Tendsto (fun (p : α × α) => Ixx p.1 p.2) (l₁ ×ˢ l₁) l₂.smallSets

  `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.

Instances

source
theorem Filter.tendstoIxxClass_principal {α : Type u_1} {s t : Set α} {Ixx : α → α → Set α} :
TendstoIxxClass Ixx (principal s) (principal t) ↔ ∀ x ∈ s, ∀ y ∈ s, Ixx x y ⊆ t
source
theorem Filter.tendstoIxxClass_inf {α : Type u_1} {l₁ l₁' l₂ l₂' : Filter α} {Ixx : α → α → Set α} [h : TendstoIxxClass Ixx l₁ l₂] [h' : TendstoIxxClass Ixx l₁' l₂'] :
TendstoIxxClass Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂')
source
theorem Filter.tendstoIxxClass_of_subset {α : Type u_1} {l₁ l₂ : Filter α} {Ixx Ixx' : α → α → Set α} (h : ∀ (a b : α), Ixx a b ⊆ Ixx' a b) [h' : TendstoIxxClass Ixx' l₁ l₂] :
TendstoIxxClass Ixx l₁ l₂
source
theorem Filter.HasBasis.tendstoIxxClass {α : Type u_1} {ι : Type u_3} {p : ι → Prop} {s : ι → Set α} {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
source
theorem Filter.Tendsto.Icc {α : Type u_1} {β : Type u_2} [Preorder α] {l₁ l₂ : Filter α} [TendstoIxxClass Set.Icc l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) :
Tendsto (fun (x : β) => Set.Icc (u₁ x) (u₂ x)) lb l₂.smallSets
source
theorem Filter.Tendsto.Ioc {α : Type u_1} {β : Type u_2} [Preorder α] {l₁ l₂ : Filter α} [TendstoIxxClass Set.Ioc l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) :
Tendsto (fun (x : β) => Set.Ioc (u₁ x) (u₂ x)) lb l₂.smallSets
source
theorem Filter.Tendsto.Ico {α : Type u_1} {β : Type u_2} [Preorder α] {l₁ l₂ : Filter α} [TendstoIxxClass Set.Ico l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) :
Tendsto (fun (x : β) => Set.Ico (u₁ x) (u₂ x)) lb l₂.smallSets
source
theorem Filter.Tendsto.Ioo {α : Type u_1} {β : Type u_2} [Preorder α] {l₁ l₂ : Filter α} [TendstoIxxClass Set.Ioo l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α} (h₁ : Tendsto u₁ lb l₁) (h₂ : Tendsto u₂ lb l₁) :
Tendsto (fun (x : β) => Set.Ioo (u₁ x) (u₂ x)) lb l₂.smallSets
source
instance Filter.tendsto_Icc_atTop_atTop {α : Type u_1} [Preorder α] :
TendstoIxxClass Set.Icc atTop atTop
source
instance Filter.tendsto_Ico_atTop_atTop {α : Type u_1} [Preorder α] :
TendstoIxxClass Set.Ico atTop atTop
source
instance Filter.tendsto_Ioc_atTop_atTop {α : Type u_1} [Preorder α] :
TendstoIxxClass Set.Ioc atTop atTop
source
instance Filter.tendsto_Ioo_atTop_atTop {α : Type u_1} [Preorder α] :
TendstoIxxClass Set.Ioo atTop atTop
source
instance Filter.tendsto_Icc_atBot_atBot {α : Type u_1} [Preorder α] :
TendstoIxxClass Set.Icc atBot atBot
source
instance Filter.tendsto_Ico_atBot_atBot {α : Type u_1} [Preorder α] :
TendstoIxxClass Set.Ico atBot atBot
source
instance Filter.tendsto_Ioc_atBot_atBot {α : Type u_1} [Preorder α] :
TendstoIxxClass Set.Ioc atBot atBot
source
instance Filter.tendsto_Ioo_atBot_atBot {α : Type u_1} [Preorder α] :
TendstoIxxClass Set.Ioo atBot atBot
source
instance Filter.OrdConnected.tendsto_Icc {α : Type u_1} [Preorder α] {s : Set α} [hs : s.OrdConnected] :
TendstoIxxClass Set.Icc (principal s) (principal s)
source
instance Filter.tendsto_Ico_Ici_Ici {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ico (principal (Set.Ici a)) (principal (Set.Ici a))
source
instance Filter.tendsto_Ico_Ioi_Ioi {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ico (principal (Set.Ioi a)) (principal (Set.Ioi a))
source
instance Filter.tendsto_Ico_Iic_Iio {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ico (principal (Set.Iic a)) (principal (Set.Iio a))
source
instance Filter.tendsto_Ico_Iio_Iio {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ico (principal (Set.Iio a)) (principal (Set.Iio a))
source
instance Filter.tendsto_Ioc_Ici_Ioi {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ioc (principal (Set.Ici a)) (principal (Set.Ioi a))
source
instance Filter.tendsto_Ioc_Iic_Iic {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ioc (principal (Set.Iic a)) (principal (Set.Iic a))
source
instance Filter.tendsto_Ioc_Iio_Iio {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ioc (principal (Set.Iio a)) (principal (Set.Iio a))
source
instance Filter.tendsto_Ioc_Ioi_Ioi {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ioc (principal (Set.Ioi a)) (principal (Set.Ioi a))
source
instance Filter.tendsto_Ioo_Ici_Ioi {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ioo (principal (Set.Ici a)) (principal (Set.Ioi a))
source
instance Filter.tendsto_Ioo_Iic_Iio {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ioo (principal (Set.Iic a)) (principal (Set.Iio a))
source
instance Filter.tendsto_Ioo_Ioi_Ioi {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ioo (principal (Set.Ioi a)) (principal (Set.Ioi a))
source
instance Filter.tendsto_Ioo_Iio_Iio {α : Type u_1} [Preorder α] {a : α} :
TendstoIxxClass Set.Ioo (principal (Set.Iio a)) (principal (Set.Iio a))
source
instance Filter.tendsto_Icc_Icc_Icc {α : Type u_1} [Preorder α] {a b : α} :
TendstoIxxClass Set.Icc (principal (Set.Icc a b)) (principal (Set.Icc a b))
source
instance Filter.tendsto_Ioc_Icc_Icc {α : Type u_1} [Preorder α] {a b : α} :
TendstoIxxClass Set.Ioc (principal (Set.Icc a b)) (principal (Set.Icc a b))
source
instance Filter.tendsto_Icc_pure_pure {α : Type u_1} [PartialOrder α] {a : α} :
TendstoIxxClass Set.Icc (pure a) (pure a)
source
instance Filter.tendsto_Ico_pure_bot {α : Type u_1} [PartialOrder α] {a : α} :
TendstoIxxClass Set.Ico (pure a) ⊥
source
instance Filter.tendsto_Ioc_pure_bot {α : Type u_1} [PartialOrder α] {a : α} :
TendstoIxxClass Set.Ioc (pure a) ⊥
source
instance Filter.tendsto_Ioo_pure_bot {α : Type u_1} [PartialOrder α] {a : α} :
TendstoIxxClass Set.Ioo (pure a) ⊥
source
instance Filter.tendsto_Icc_uIcc_uIcc {α : Type u_1} [LinearOrder α] {a b : α} :
TendstoIxxClass Set.Icc (principal (Set.uIcc a b)) (principal (Set.uIcc a b))
source
instance Filter.tendsto_Ioc_uIcc_uIcc {α : Type u_1} [LinearOrder α] {a b : α} :
TendstoIxxClass Set.Ioc (principal (Set.uIcc a b)) (principal (Set.uIcc a b))
source
instance Filter.tendsto_uIcc_of_Icc {α : Type u_1} [LinearOrder α] {l : Filter α} [TendstoIxxClass Set.Icc l l] :
TendstoIxxClass Set.uIcc l l
source
theorem Filter.Tendsto.uIcc {α : Type u_1} {β : Type u_2} [LinearOrder α] {l : Filter α} [TendstoIxxClass Set.Icc l l] {f g : β → α} {lb : Filter β} (hf : Tendsto f lb l) (hg : Tendsto g lb l) :
Tendsto (fun (x : β) => Set.uIcc (f x) (g x)) lb l.smallSets