mathlib3 documentation

data.analysis.filter

Computational realization of filters (experimental) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides infrastructure to compute with filters.

Main declarations #

structure cfilter (α : Type u_1) (σ : Type u_2) [partial_order α] :
Type (max u_1 u_2)
  • f : σ α
  • pt : σ
  • inf : σ σ σ
  • inf_le_left : (a b : σ), self.f (self.inf a b) self.f a
  • inf_le_right : (a b : σ), self.f (self.inf a b) self.f b

A cfilter α σ is a realization of a filter (base) on α, represented by a type σ together with operations for the top element and the binary inf operation.

Instances for cfilter
@[protected, instance]
def cfilter.inhabited {α : Type u_1} [inhabited α] [semilattice_inf α] :
Equations
@[protected, instance]
def cfilter.has_coe_to_fun {α : Type u_1} {σ : Type u_3} [partial_order α] :
has_coe_to_fun (cfilter α σ) (λ (_x : cfilter α σ), σ α)
Equations
@[simp]
theorem cfilter.coe_mk {α : Type u_1} {σ : Type u_3} [partial_order α] (f : σ α) (pt : σ) (inf : σ σ σ) (h₁ : (a b : σ), f (inf a b) f a) (h₂ : (a b : σ), f (inf a b) f b) (a : σ) :
{f := f, pt := pt, inf := inf, inf_le_left := h₁, inf_le_right := h₂} a = f a
def cfilter.of_equiv {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [partial_order α] (E : σ τ) :
cfilter α σ cfilter α τ

Map a cfilter to an equivalent representation type.

Equations
@[simp]
theorem cfilter.of_equiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [partial_order α] (E : σ τ) (F : cfilter α σ) (a : τ) :
(cfilter.of_equiv E F) a = F ((E.symm) a)
def cfilter.to_filter {α : Type u_1} {σ : Type u_3} (F : cfilter (set α) σ) :

The filter represented by a cfilter is the collection of supersets of elements of the filter base.

Equations
@[simp]
theorem cfilter.mem_to_filter_sets {α : Type u_1} {σ : Type u_3} (F : cfilter (set α) σ) {a : set α} :
a F.to_filter (b : σ), F b a
structure filter.realizer {α : Type u_1} (f : filter α) :
Type (max u_1 (u_5+1))

A realizer for filter f is a cfilter which generates f.

Instances for filter.realizer
@[protected]
def cfilter.to_realizer {α : Type u_1} {σ : Type u_3} (F : cfilter (set α) σ) :

A cfilter realizes the filter it generates.

Equations
theorem filter.realizer.mem_sets {α : Type u_1} {f : filter α} (F : f.realizer) {a : set α} :
a f (b : F.σ), (F.F) b a
def filter.realizer.of_eq {α : Type u_1} {f g : filter α} (e : f = g) (F : f.realizer) :

Transfer a realizer along an equality of filter. This has better definitional equalities than the eq.rec proof.

Equations
def filter.realizer.of_filter {α : Type u_1} (f : filter α) :

A filter realizes itself.

Equations
def filter.realizer.of_equiv {α : Type u_1} {τ : Type u_4} {f : filter α} (F : f.realizer) (E : F.σ τ) :

Transfer a filter realizer to another realizer on a different base type.

Equations
@[simp]
theorem filter.realizer.of_equiv_σ {α : Type u_1} {τ : Type u_4} {f : filter α} (F : f.realizer) (E : F.σ τ) :
(F.of_equiv E).σ = τ
@[simp]
theorem filter.realizer.of_equiv_F {α : Type u_1} {τ : Type u_4} {f : filter α} (F : f.realizer) (E : F.σ τ) (s : τ) :
((F.of_equiv E).F) s = (F.F) ((E.symm) s)
@[protected]

unit is a realizer for the principal filter

Equations
@[simp]
@[simp]
theorem filter.realizer.principal_F {α : Type u_1} (s : set α) (u : unit) :
@[simp]
@[protected]
def filter.realizer.bot {α : Type u_1} :

unit is a realizer for the bottom filter

Equations
@[simp]
theorem filter.realizer.bot_F {α : Type u_1} (u : unit) :
@[protected]
def filter.realizer.map {α : Type u_1} {β : Type u_2} (m : α β) {f : filter α} (F : f.realizer) :

Construct a realizer for map m f given a realizer for f

Equations
@[simp]
theorem filter.realizer.map_σ {α : Type u_1} {β : Type u_2} (m : α β) {f : filter α} (F : f.realizer) :
@[simp]
theorem filter.realizer.map_F {α : Type u_1} {β : Type u_2} (m : α β) {f : filter α} (F : f.realizer) (s : (filter.realizer.map m F).σ) :
((filter.realizer.map m F).F) s = m '' (F.F) s
@[protected]
def filter.realizer.comap {α : Type u_1} {β : Type u_2} (m : α β) {f : filter β} (F : f.realizer) :

Construct a realizer for comap m f given a realizer for f

Equations
@[protected]
def filter.realizer.sup {α : Type u_1} {f g : filter α} (F : f.realizer) (G : g.realizer) :

Construct a realizer for the sup of two filters

Equations
  • F.sup G = {σ := F.σ × G.σ, F := {f := λ (_x : F.σ × G.σ), filter.realizer.sup._match_1 F G _x, pt := (F.F.pt, G.F.pt), inf := λ (_x : F.σ × G.σ), filter.realizer.sup._match_3 F G _x, inf_le_left := _, inf_le_right := _}, eq := _}
  • filter.realizer.sup._match_1 F G (s, t) = (F.F) s (G.F) t
  • filter.realizer.sup._match_3 F G (a, a') = λ (_x : F.σ × G.σ), filter.realizer.sup._match_2 F G a a' _x
  • filter.realizer.sup._match_2 F G a a' (b, b') = (F.F.inf a b, G.F.inf a' b')
@[protected]
def filter.realizer.inf {α : Type u_1} {f g : filter α} (F : f.realizer) (G : g.realizer) :

Construct a realizer for the inf of two filters

Equations
  • F.inf G = {σ := F.σ × G.σ, F := {f := λ (_x : F.σ × G.σ), filter.realizer.inf._match_1 F G _x, pt := (F.F.pt, G.F.pt), inf := λ (_x : F.σ × G.σ), filter.realizer.inf._match_3 F G _x, inf_le_left := _, inf_le_right := _}, eq := _}
  • filter.realizer.inf._match_1 F G (s, t) = (F.F) s (G.F) t
  • filter.realizer.inf._match_3 F G (a, a') = λ (_x : F.σ × G.σ), filter.realizer.inf._match_2 F G a a' _x
  • filter.realizer.inf._match_2 F G a a' (b, b') = (F.F.inf a b, G.F.inf a' b')
@[protected]

Construct a realizer for the cofinite filter

Equations
@[protected]
def filter.realizer.bind {α : Type u_1} {β : Type u_2} {f : filter α} {m : α filter β} (F : f.realizer) (G : Π (i : α), (m i).realizer) :

Construct a realizer for filter bind

Equations
@[protected]
def filter.realizer.Sup {α : Type u_1} {β : Type u_2} {f : α filter β} (F : Π (i : α), (f i).realizer) :
( (i : α), f i).realizer

Construct a realizer for indexed supremum

Equations
@[protected]
def filter.realizer.prod {α : Type u_1} {f g : filter α} (F : f.realizer) (G : g.realizer) :

Construct a realizer for the product of filters

Equations
theorem filter.realizer.le_iff {α : Type u_1} {f g : filter α} (F : f.realizer) (G : g.realizer) :
f g (b : G.σ), (a : F.σ), (F.F) a (G.F) b
theorem filter.realizer.tendsto_iff {α : Type u_1} {β : Type u_2} (f : α β) {l₁ : filter α} {l₂ : filter β} (L₁ : l₁.realizer) (L₂ : l₂.realizer) :
filter.tendsto f l₁ l₂ (b : L₂.σ), (a : L₁.σ), (x : α), x (L₁.F) a f x (L₂.F) b
theorem filter.realizer.ne_bot_iff {α : Type u_1} {f : filter α} (F : f.realizer) :
f (a : F.σ), ((F.F) a).nonempty