mathlib documentation

topology.uniform_space.cauchy

Theory of Cauchy filters in uniform spaces. Complete uniform spaces. Totally bounded subsets.

def cauchy {α : Type u} [uniform_space α] :
filter α → Prop

A filter f is Cauchy if for every entourage r, there exists an s ∈ f such that s × s ⊆ r. This is a generalization of Cauchy sequences, because if a : ℕ → α then the filter of sets containing cofinitely many of the a n is Cauchy iff a is a Cauchy sequence.

Equations
def is_complete {α : Type u} [uniform_space α] :
set α → Prop

A set s is called complete, if any Cauchy filter f such that s ∈ f has a limit in s (formally, it satisfies f ≤ 𝓝 x for some x ∈ s).

Equations
theorem filter.has_basis.cauchy_iff {α : Type u} {β : Type v} [uniform_space α] {p : β → Prop} {s : β → set × α)} (h : (𝓤 α).has_basis p s) {f : filter α} :
cauchy f f.ne_bot ∀ (i : β), p i(∃ (t : set α) (H : t f), ∀ (x y : α), x ty t(x, y) s i)

theorem cauchy_iff' {α : Type u} [uniform_space α] {f : filter α} :
cauchy f f.ne_bot ∀ (s : set × α)), s 𝓤 α(∃ (t : set α) (H : t f), ∀ (x y : α), x ty t(x, y) s)

theorem cauchy_iff {α : Type u} [uniform_space α] {f : filter α} :
cauchy f f.ne_bot ∀ (s : set × α)), s 𝓤 α(∃ (t : set α) (H : t f), t.prod t s)

theorem cauchy_map_iff {α : Type u} {β : Type v} [uniform_space α] {l : filter β} {f : β → α} :
cauchy (filter.map f l) l.ne_bot filter.tendsto (λ (p : β × β), (f p.fst, f p.snd)) (l ×ᶠ l) (𝓤 α)

theorem cauchy_map_iff' {α : Type u} {β : Type v} [uniform_space α] {l : filter β} [hl : l.ne_bot] {f : β → α} :
cauchy (filter.map f l) filter.tendsto (λ (p : β × β), (f p.fst, f p.snd)) (l ×ᶠ l) (𝓤 α)

theorem cauchy.mono {α : Type u} [uniform_space α] {f g : filter α} [hg : g.ne_bot] :
cauchy fg fcauchy g

theorem cauchy.mono' {α : Type u} [uniform_space α] {f g : filter α} :
cauchy fg.ne_botg fcauchy g

theorem cauchy_nhds {α : Type u} [uniform_space α] {a : α} :

theorem cauchy_pure {α : Type u} [uniform_space α] {a : α} :

theorem filter.tendsto.cauchy_map {α : Type u} {β : Type v} [uniform_space α] {l : filter β} [l.ne_bot] {f : β → α} {a : α} :

theorem le_nhds_of_cauchy_adhp_aux {α : Type u} [uniform_space α] {f : filter α} {x : α} :
(∀ (s : set × α)), s 𝓤 α(∃ (t : set α) (H : t f), t.prod t s ∃ (y : α), (x, y) s y t))f 𝓝 x

The common part of the proofs of le_nhds_of_cauchy_adhp and sequentially_complete.le_nhds_of_seq_tendsto_nhds: if for any entourage s one can choose a set t ∈ f of diameter s such that it contains a point y with (x, y) ∈ s, then f converges to x.

theorem le_nhds_of_cauchy_adhp {α : Type u} [uniform_space α] {f : filter α} {x : α} :
cauchy fcluster_pt x ff 𝓝 x

If x is an adherent (cluster) point for a Cauchy filter f, then it is a limit point for f.

theorem le_nhds_iff_adhp_of_cauchy {α : Type u} [uniform_space α] {f : filter α} {x : α} :
cauchy f(f 𝓝 x cluster_pt x f)

theorem cauchy.map {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : filter α} {m : α → β} :

theorem cauchy.comap {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : filter β} {m : α → β} (hf : cauchy f) (hm : filter.comap (λ (p : α × α), (m p.fst, m p.snd)) (𝓤 β) 𝓤 α) [(filter.comap m f).ne_bot] :

theorem cauchy.comap' {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : filter β} {m : α → β} :
cauchy ffilter.comap (λ (p : α × α), (m p.fst, m p.snd)) (𝓤 β) 𝓤 α(filter.comap m f).ne_botcauchy (filter.comap m f)

def cauchy_seq {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] :
(β → α) → Prop

Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that is general enough to cover both ℕ and ℝ, which are the main motivating examples.

Equations
theorem cauchy_seq.mem_entourage {α : Type u} [uniform_space α] {ι : Type u_1} [nonempty ι] [linear_order ι] {u : ι → α} (h : cauchy_seq u) {V : set × α)} :
V 𝓤 α(∃ (k₀ : ι), ∀ (i j : ι), k₀ ik₀ j(u i, u j) V)

theorem filter.tendsto.cauchy_seq {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] [nonempty β] {f : β → α} {x : α} :

theorem cauchy_seq_iff_tendsto {α : Type u} {β : Type v} [uniform_space α] [nonempty β] [semilattice_sup β] {u : β → α} :

theorem tendsto_nhds_of_cauchy_seq_of_subseq {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] {u : β → α} (hu : cauchy_seq u) {ι : Type u_1} {f : ι → β} {p : filter ι} [p.ne_bot] (hf : filter.tendsto f p filter.at_top) {a : α} :

If a Cauchy sequence has a convergent subsequence, then it converges.

@[nolint]
theorem filter.has_basis.cauchy_seq_iff {α : Type u} {β : Type v} [uniform_space α] {γ : Type u_1} [nonempty β] [semilattice_sup β] {u : β → α} {p : γ → Prop} {s : γ → set × α)} :
(𝓤 α).has_basis p s(cauchy_seq u ∀ (i : γ), p i(∃ (N : β), ∀ (m n : β), m Nn N(u m, u n) s i))

theorem filter.has_basis.cauchy_seq_iff' {α : Type u} {β : Type v} [uniform_space α] {γ : Type u_1} [nonempty β] [semilattice_sup β] {u : β → α} {p : γ → Prop} {s : γ → set × α)} :
(𝓤 α).has_basis p s(cauchy_seq u ∀ (i : γ), p i(∃ (N : β), ∀ (n : β), n N(u n, u N) s i))

theorem cauchy_seq_of_controlled {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] [nonempty β] (U : β → set × α)) (hU : ∀ (s : set × α)), s 𝓤 α(∃ (n : β), U n s)) {f : β → α} :
(∀ {N m n : β}, N mN n(f m, f n) U N)cauchy_seq f

theorem cauchy_prod {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : filter α} {g : filter β} :
cauchy fcauchy gcauchy (f ×ᶠ g)

@[instance]
def complete_space.prod {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] [complete_space α] [complete_space β] :

If univ is complete, the space is a complete space

theorem cauchy_iff_exists_le_nhds {α : Type u} [uniform_space α] [complete_space α] {l : filter α} [l.ne_bot] :
cauchy l ∃ (x : α), l 𝓝 x

theorem cauchy_map_iff_exists_tendsto {α : Type u} {β : Type v} [uniform_space α] [complete_space α] {l : filter β} {f : β → α} [l.ne_bot] :
cauchy (filter.map f l) ∃ (x : α), filter.tendsto f l (𝓝 x)

theorem cauchy_seq_tendsto_of_complete {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] [complete_space α] {u : β → α} :
cauchy_seq u(∃ (x : α), filter.tendsto u filter.at_top (𝓝 x))

A Cauchy sequence in a complete space converges

theorem cauchy_seq_tendsto_of_is_complete {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] {K : set α} (h₁ : is_complete K) {u : β → α} :
(∀ (n : β), u n K)cauchy_seq u(∃ (v : α) (H : v K), filter.tendsto u filter.at_top (𝓝 v))

If K is a complete subset, then any cauchy sequence in K converges to a point in K

theorem cauchy.le_nhds_Lim {α : Type u} [uniform_space α] [complete_space α] [nonempty α] {f : filter α} :
cauchy ff 𝓝 (Lim f)

theorem cauchy_seq.tendsto_lim {α : Type u} {β : Type v} [uniform_space α] [semilattice_sup β] [complete_space α] [nonempty α] {u : β → α} :

theorem is_closed.is_complete {α : Type u} [uniform_space α] [complete_space α] {s : set α} :

def totally_bounded {α : Type u} [uniform_space α] :
set α → Prop

A set s is totally bounded if for every entourage d there is a finite set of points t such that every element of s is d-near to some element of t.

Equations
theorem totally_bounded_iff_subset {α : Type u} [uniform_space α] {s : set α} :
totally_bounded s ∀ (d : set × α)), d 𝓤 α(∃ (t : set α) (H : t s), t.finite s ⋃ (y : α) (H : y t), {x : α | (x, y) d})

theorem totally_bounded_of_forall_symm {α : Type u} [uniform_space α] {s : set α} :
(∀ (V : set × α)), V 𝓤 αsymmetric_rel V(∃ (t : set α), t.finite s ⋃ (y : α) (H : y t), uniform_space.ball y V))totally_bounded s

theorem totally_bounded_subset {α : Type u} [uniform_space α] {s₁ s₂ : set α} :
s₁ s₂totally_bounded s₂totally_bounded s₁

theorem totally_bounded.closure {α : Type u} [uniform_space α] {s : set α} :

The closure of a totally bounded set is totally bounded.

theorem totally_bounded.image {α : Type u} {β : Type v} [uniform_space α] [uniform_space β] {f : α → β} {s : set α} :

The image of a totally bounded set under a unifromly continuous map is totally bounded.

theorem cauchy_of_totally_bounded_of_ultrafilter {α : Type u} [uniform_space α] {s : set α} {f : filter α} :

theorem totally_bounded_iff_filter {α : Type u} [uniform_space α] {s : set α} :
totally_bounded s ∀ (f : filter α), f.ne_botf 𝓟 s(∃ (c : filter α) (H : c f), cauchy c)

theorem totally_bounded_iff_ultrafilter {α : Type u} [uniform_space α] {s : set α} :
totally_bounded s ∀ (f : filter α), f.is_ultrafilterf 𝓟 scauchy f

@[instance]

Sequentially complete space

In this section we prove that a uniform space is complete provided that it is sequentially complete (i.e., any Cauchy sequence converges) and its uniformity filter admits a countable generating set. In particular, this applies to (e)metric spaces, see the files topology/metric_space/emetric_space and topology/metric_space/basic.

More precisely, we assume that there is a sequence of entourages U_n such that any other entourage includes one of U_n. Then any Cauchy filter f generates a decreasing sequence of sets s_n ∈ f such that s_n × s_n ⊆ U_n. Choose a sequence x_n∈s_n. It is easy to show that this is a Cauchy sequence. If this sequence converges to some a, then f ≤ 𝓝 a.

def sequentially_complete.set_seq_aux {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (n : ) :
{s // ∃ (_x : s f), s.prod s U n}

An auxiliary sequence of sets approximating a Cauchy filter.

Equations
def sequentially_complete.set_seq {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} :
(∀ (n : ), U n 𝓤 α)set α

Given a Cauchy filter f and a sequence U of entourages, set_seq provides a sequence of monotonically decreasing sets s n ∈ f such that (s n).prod (s n) ⊆ U.

Equations
theorem sequentially_complete.set_seq_mem {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (n : ) :

theorem sequentially_complete.set_seq_mono {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) ⦃m n :  :

theorem sequentially_complete.set_seq_sub_aux {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (n : ) :

theorem sequentially_complete.set_seq_prod_subset {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) {N m n : } :
N mN n(sequentially_complete.set_seq hf U_mem m).prod (sequentially_complete.set_seq hf U_mem n) U N

def sequentially_complete.seq {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} :
(∀ (n : ), U n 𝓤 α) → α

A sequence of points such that seq n ∈ set_seq n. Here set_seq is a monotonically decreasing sequence of sets set_seq n ∈ f with diameters controlled by a given sequence of entourages.

Equations
theorem sequentially_complete.seq_mem {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (n : ) :

theorem sequentially_complete.seq_pair_mem {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) ⦃N m n :  :
N mN n(sequentially_complete.seq hf U_mem m, sequentially_complete.seq hf U_mem n) U N

theorem sequentially_complete.seq_is_cauchy_seq {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) :
(∀ (s : set × α)), s 𝓤 α(∃ (n : ), U n s))cauchy_seq (sequentially_complete.seq hf U_mem)

theorem sequentially_complete.le_nhds_of_seq_tendsto_nhds {α : Type u} [uniform_space α] {f : filter α} (hf : cauchy f) {U : set × α)} (U_mem : ∀ (n : ), U n 𝓤 α) (U_le : ∀ (s : set × α)), s 𝓤 α(∃ (n : ), U n s)) ⦃a : α⦄ :

If the sequence sequentially_complete.seq converges to a, then f ≤ 𝓝 a.

theorem uniform_space.complete_of_convergent_controlled_sequences {α : Type u} [uniform_space α] (H : (𝓤 α).is_countably_generated) (U : set × α)) :
(∀ (n : ), U n 𝓤 α)(∀ (u : → α), (∀ (N m n : ), N mN n(u m, u n) U N)(∃ (a : α), filter.tendsto u filter.at_top (𝓝 a)))complete_space α

A uniform space is complete provided that (a) its uniformity filter has a countable basis; (b) any sequence satisfying a "controlled" version of the Cauchy condition converges.

theorem uniform_space.complete_of_cauchy_seq_tendsto {α : Type u} [uniform_space α] :
(𝓤 α).is_countably_generated(∀ (u : → α), cauchy_seq u(∃ (a : α), filter.tendsto u filter.at_top (𝓝 a)))complete_space α

A sequentially complete uniform space with a countable basis of the uniformity filter is complete.

A separable uniform space with countably generated uniformity filter is second countable: one obtains a countable basis by taking the balls centered at points in a dense subset, and with rational "radii" from a countable open symmetric antimono basis of 𝓤 α. We do not register this as an instance, as there is already an instance going in the other direction from second countable spaces to separable spaces, and we want to avoid loops.