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
class Filter.TendstoIxxClass {α : Type u_1} (Ixx : ααSet α) (l₁ : ) (l₂ : outParam (Filter α)) :

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 : Filter.Tendsto (fun (p : α × α) => Ixx p.1 p.2) (l₁ ×ˢ l₁) (Filter.smallSets l₂)

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
theorem Filter.TendstoIxxClass.tendsto_Ixx {α : Type u_1} {Ixx : ααSet α} {l₁ : } {l₂ : outParam (Filter α)} [self : Filter.TendstoIxxClass Ixx l₁ l₂] :
Filter.Tendsto (fun (p : α × α) => Ixx p.1 p.2) (l₁ ×ˢ l₁) (Filter.smallSets l₂)

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.

theorem Filter.tendstoIxxClass_principal {α : Type u_1} {s : Set α} {t : Set α} {Ixx : ααSet α} :
xs, ys, Ixx x y t
theorem Filter.tendstoIxxClass_inf {α : Type u_1} {l₁ : } {l₁' : } {l₂ : } {l₂' : } {Ixx : ααSet α} [h : Filter.TendstoIxxClass Ixx l₁ l₂] [h' : Filter.TendstoIxxClass Ixx l₁' l₂'] :
Filter.TendstoIxxClass Ixx (l₁ l₁') (l₂ l₂')
theorem Filter.tendstoIxxClass_of_subset {α : Type u_1} {l₁ : } {l₂ : } {Ixx : ααSet α} {Ixx' : ααSet α} (h : ∀ (a b : α), Ixx a b Ixx' a b) [h' : Filter.TendstoIxxClass Ixx' l₁ l₂] :
theorem Filter.HasBasis.tendstoIxxClass {α : Type u_1} {ι : Type u_3} {p : ιProp} {s : ιSet α} {l : } (hl : l.HasBasis p s) {Ixx : ααSet α} (H : ∀ (i : ι), p ixs i, ys i, Ixx x y s i) :
theorem Filter.Tendsto.Icc {α : Type u_1} {β : Type u_2} [] {l₁ : } {l₂ : } [Filter.TendstoIxxClass Set.Icc l₁ l₂] {lb : } {u₁ : βα} {u₂ : βα} (h₁ : Filter.Tendsto u₁ lb l₁) (h₂ : Filter.Tendsto u₂ lb l₁) :
Filter.Tendsto (fun (x : β) => Set.Icc (u₁ x) (u₂ x)) lb l₂.smallSets
theorem Filter.Tendsto.Ioc {α : Type u_1} {β : Type u_2} [] {l₁ : } {l₂ : } [Filter.TendstoIxxClass Set.Ioc l₁ l₂] {lb : } {u₁ : βα} {u₂ : βα} (h₁ : Filter.Tendsto u₁ lb l₁) (h₂ : Filter.Tendsto u₂ lb l₁) :
Filter.Tendsto (fun (x : β) => Set.Ioc (u₁ x) (u₂ x)) lb l₂.smallSets
theorem Filter.Tendsto.Ico {α : Type u_1} {β : Type u_2} [] {l₁ : } {l₂ : } [Filter.TendstoIxxClass Set.Ico l₁ l₂] {lb : } {u₁ : βα} {u₂ : βα} (h₁ : Filter.Tendsto u₁ lb l₁) (h₂ : Filter.Tendsto u₂ lb l₁) :
Filter.Tendsto (fun (x : β) => Set.Ico (u₁ x) (u₂ x)) lb l₂.smallSets
theorem Filter.Tendsto.Ioo {α : Type u_1} {β : Type u_2} [] {l₁ : } {l₂ : } [Filter.TendstoIxxClass Set.Ioo l₁ l₂] {lb : } {u₁ : βα} {u₂ : βα} (h₁ : Filter.Tendsto u₁ lb l₁) (h₂ : Filter.Tendsto u₂ lb l₁) :
Filter.Tendsto (fun (x : β) => Set.Ioo (u₁ x) (u₂ x)) lb l₂.smallSets
instance Filter.tendsto_Icc_atTop_atTop {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Icc Filter.atTop Filter.atTop
Equations
• =
instance Filter.tendsto_Ico_atTop_atTop {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ico Filter.atTop Filter.atTop
Equations
• =
instance Filter.tendsto_Ioc_atTop_atTop {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ioc Filter.atTop Filter.atTop
Equations
• =
instance Filter.tendsto_Ioo_atTop_atTop {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ioo Filter.atTop Filter.atTop
Equations
• =
instance Filter.tendsto_Icc_atBot_atBot {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Icc Filter.atBot Filter.atBot
Equations
• =
instance Filter.tendsto_Ico_atBot_atBot {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ico Filter.atBot Filter.atBot
Equations
• =
instance Filter.tendsto_Ioc_atBot_atBot {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ioc Filter.atBot Filter.atBot
Equations
• =
instance Filter.tendsto_Ioo_atBot_atBot {α : Type u_1} [] :
Filter.TendstoIxxClass Set.Ioo Filter.atBot Filter.atBot
Equations
• =
instance Filter.OrdConnected.tendsto_Icc {α : Type u_1} [] {s : Set α} [hs : s.OrdConnected] :
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
instance Filter.tendsto_Icc_Icc_Icc {α : Type u_1} [] {a : α} {b : α} :
Equations
• =
instance Filter.tendsto_Ioc_Icc_Icc {α : Type u_1} [] {a : α} {b : α} :
Equations
• =
instance Filter.tendsto_Icc_pure_pure {α : Type u_1} [] {a : α} :
Equations
• =
instance Filter.tendsto_Ico_pure_bot {α : Type u_1} [] {a : α} :
Equations
• =
instance Filter.tendsto_Ioc_pure_bot {α : Type u_1} [] {a : α} :
Equations
• =
instance Filter.tendsto_Ioo_pure_bot {α : Type u_1} [] {a : α} :
Equations
• =
instance Filter.tendsto_Icc_uIcc_uIcc {α : Type u_1} [] {a : α} {b : α} :
Equations
• =
instance Filter.tendsto_Ioc_uIcc_uIcc {α : Type u_1} [] {a : α} {b : α} :
Equations
• =
instance Filter.tendsto_uIcc_of_Icc {α : Type u_1} [] {l : } [Filter.TendstoIxxClass Set.Icc l l] :
Equations
• =
theorem Filter.Tendsto.uIcc {α : Type u_1} {β : Type u_2} [] {l : } [Filter.TendstoIxxClass Set.Icc l l] {f : βα} {g : βα} {lb : } (hf : Filter.Tendsto f lb l) (hg : Filter.Tendsto g lb l) :
Filter.Tendsto (fun (x : β) => Set.uIcc (f x) (g x)) lb l.smallSets