Documentation

Mathlib.Data.Analysis.Filter

Computational realization of filters (experimental) #

This file provides infrastructure to compute with filters.

Main declarations #

structure CFilter (α : Type u_1) (σ : Type u_2) [PartialOrder α] :
Type (max u_1 u_2)

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.

  • 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
instance instInhabitedCFilter {α : Type u_1} [Inhabited α] [SemilatticeInf α] :
Equations
instance CFilter.instCoeFunForall {α : Type u_1} {σ : Type u_3} [PartialOrder α] :
CoeFun (CFilter α σ) fun (x : CFilter α σ) => σα
Equations
theorem CFilter.coe_mk {α : Type u_1} {σ : Type u_3} [PartialOrder α] (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₂ }.f a = f a
def CFilter.ofEquiv {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [PartialOrder α] (E : σ τ) :
CFilter α σCFilter α τ

Map a CFilter to an equivalent representation type.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem CFilter.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [PartialOrder α] (E : σ τ) (F : CFilter α σ) (a : τ) :
(ofEquiv E F).f a = F.f (E.symm a)
def CFilter.toFilter {α : 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
  • F.toFilter = { sets := {a : Set α | ∃ (b : σ), F.f b a}, univ_sets := , sets_of_superset := , inter_sets := }
@[simp]
theorem CFilter.mem_toFilter_sets {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) {a : Set α} :
a F.toFilter ∃ (b : σ), F.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.

def CFilter.toRealizer {α : 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.f b a
def Filter.Realizer.ofEq {α : 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.ofFilter {α : Type u_1} (f : Filter α) :

A filter realizes itself.

Equations
  • One or more equations did not get rendered due to their size.
def Filter.Realizer.ofEquiv {α : 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.ofEquiv_σ {α : Type u_1} {τ : Type u_4} {f : Filter α} (F : f.Realizer) (E : F.σ τ) :
(F.ofEquiv E).σ = τ
@[simp]
theorem Filter.Realizer.ofEquiv_F {α : Type u_1} {τ : Type u_4} {f : Filter α} (F : f.Realizer) (E : F.σ τ) (s : τ) :
(F.ofEquiv E).F.f s = F.F.f (E.symm s)
def Filter.Realizer.principal {α : Type u_1} (s : Set α) :

Unit is a realizer for the principal filter

Equations
@[simp]
@[simp]
theorem Filter.Realizer.principal_F {α : Type u_1} (s : Set α) (u : Unit) :
@[simp]
theorem Filter.Realizer.top_F {α : Type u_1} (u : Unit) :
@[simp]
theorem Filter.Realizer.bot_F {α : Type u_1} (u : Unit) :
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 : (Realizer.map m F).σ) :
(Realizer.map m F).F.f s = m '' F.F.f s
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
def Filter.Realizer.sup {α : Type u_1} {f g : Filter α} (F : f.Realizer) (G : g.Realizer) :
(fg).Realizer

Construct a realizer for the sup of two filters

Equations
  • One or more equations did not get rendered due to their size.
def Filter.Realizer.inf {α : Type u_1} {f g : Filter α} (F : f.Realizer) (G : g.Realizer) :
(fg).Realizer

Construct a realizer for the inf of two filters

Equations
  • One or more equations did not get rendered due to their size.

Construct a realizer for the cofinite filter

Equations
  • One or more equations did not get rendered due to their size.
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
  • One or more equations did not get rendered due to their size.
def Filter.Realizer.iSup {α : Type u_1} {β : Type u_2} {f : αFilter β} (F : (i : α) → (f i).Realizer) :
(⨆ (i : α), f i).Realizer

Construct a realizer for indexed supremum

Equations
  • One or more equations did not get rendered due to their size.
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.f a G.F.f b
theorem Filter.Realizer.tendsto_iff {α : Type u_1} {β : Type u_2} (f : αβ) {l₁ : Filter α} {l₂ : Filter β} (L₁ : l₁.Realizer) (L₂ : l₂.Realizer) :
Tendsto f l₁ l₂ ∀ (b : L₂.σ), ∃ (a : L₁.σ), xL₁.F.f a, f x L₂.F.f b
theorem Filter.Realizer.ne_bot_iff {α : Type u_1} {f : Filter α} (F : f.Realizer) :
f ∀ (a : F.σ), (F.F.f a).Nonempty