Computational realization of filters (experimental)

This file provides infrastructure to compute with filters.

Main declarations

• CFilter: Realization of a filter base. Note that this is in the generality of filters on lattices, while Filter is filters of sets (so corresponding to CFilter (Set α) σ).
• Filter.Realizer: Realization of a Filter. CFilter that generates the given filter.

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 instInhabitedCFilterToPartialOrder {α : Type u_1} [Inhabited α] [SemilatticeInf α] : Inhabited (CFilter α α)

Equations

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

instance CFilter.instCoeFunCFilterForAll {α : Type u_1} {σ : Type u_3} [PartialOrder α] : CoeFun (CFilter α σ) fun (x : CFilter α σ) => σ → α

Equations

• CFilter.instCoeFunCFilterForAll = { coe := CFilter.f }

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 : τ) : (CFilter.ofEquiv E F).f a = F.f (E.symm a)

def CFilter.toFilter {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) : Filter α

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

Equations

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

@[simp]

theorem CFilter.mem_toFilter_sets {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) {a : Set α} : a ∈ CFilter.toFilter F ↔ ∃ (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.

• σ : Type u_5
• F : CFilter (Set α) self.σ
• eq : CFilter.toFilter self.F = f

def CFilter.toRealizer {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) : Filter.Realizer (CFilter.toFilter F)

A CFilter realizes the filter it generates.

Equations

• CFilter.toRealizer F = { σ := σ, F := F, eq := (_ : CFilter.toFilter F = CFilter.toFilter F) }

theorem Filter.Realizer.mem_sets {α : Type u_1} {f : Filter α} (F : Filter.Realizer f) {a : Set α} : a ∈ f ↔ ∃ (b : F.σ), F.F.f b ⊆ a

def Filter.Realizer.ofEq {α : Type u_1} {f : Filter α} {g : Filter α} (e : f = g) (F : Filter.Realizer f) : Filter.Realizer g

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

Equations

• Filter.Realizer.ofEq e F = { σ := F.σ, F := F.F, eq := (_ : CFilter.toFilter F.F = g) }

def Filter.Realizer.ofFilter {α : Type u_1} (f : Filter α) : Filter.Realizer f

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 : Filter.Realizer f) (E : F.σ ≃ τ) : Filter.Realizer f

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

Equations

• Filter.Realizer.ofEquiv F E = { σ := τ, F := CFilter.ofEquiv E F.F, eq := (_ : CFilter.toFilter (CFilter.ofEquiv E F.F) = f) }

@[simp]

theorem Filter.Realizer.ofEquiv_σ {α : Type u_1} {τ : Type u_4} {f : Filter α} (F : Filter.Realizer f) (E : F.σ ≃ τ) : (Filter.Realizer.ofEquiv F E).σ = τ

@[simp]

theorem Filter.Realizer.ofEquiv_F {α : Type u_1} {τ : Type u_4} {f : Filter α} (F : Filter.Realizer f) (E : F.σ ≃ τ) (s : τ) : (Filter.Realizer.ofEquiv F E).F.f s = F.F.f (E.symm s)

def Filter.Realizer.principal {α : Type u_1} (s : Set α) : Filter.Realizer (Filter.principal s)

Unit is a realizer for the principal filter

Equations

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

@[simp]

theorem Filter.Realizer.principal_σ {α : Type u_1} (s : Set α) : (Filter.Realizer.principal s).σ = Unit

@[simp]

theorem Filter.Realizer.principal_F {α : Type u_1} (s : Set α) (u : Unit) : (Filter.Realizer.principal s).F.f u = s

instance Filter.Realizer.instInhabitedRealizerPrincipal {α : Type u_1} (s : Set α) : Inhabited (Filter.Realizer (Filter.principal s))

Equations

• Filter.Realizer.instInhabitedRealizerPrincipal s = { default := Filter.Realizer.principal s }

def Filter.Realizer.top {α : Type u_1} : Filter.Realizer ⊤

Unit is a realizer for the top filter

Equations

• Filter.Realizer.top = Filter.Realizer.ofEq (_ : Filter.principal Set.univ = ⊤) (Filter.Realizer.principal Set.univ)

@[simp]

theorem Filter.Realizer.top_σ {α : Type u_1} : Filter.Realizer.top.σ = Unit

@[simp]

theorem Filter.Realizer.top_F {α : Type u_1} (u : Unit) : Filter.Realizer.top.F.f u = Set.univ

def Filter.Realizer.bot {α : Type u_1} : Filter.Realizer ⊥

Unit is a realizer for the bottom filter

Equations

• Filter.Realizer.bot = Filter.Realizer.ofEq (_ : Filter.principal ∅ = ⊥) (Filter.Realizer.principal ∅)

@[simp]

theorem Filter.Realizer.bot_σ {α : Type u_1} : Filter.Realizer.bot.σ = Unit

@[simp]

theorem Filter.Realizer.bot_F {α : Type u_1} (u : Unit) : Filter.Realizer.bot.F.f u = ∅

def Filter.Realizer.map {α : Type u_1} {β : Type u_2} (m : α → β) {f : Filter α} (F : Filter.Realizer f) : Filter.Realizer (Filter.map m f)

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

Equations

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

@[simp]

theorem Filter.Realizer.map_σ {α : Type u_1} {β : Type u_2} (m : α → β) {f : Filter α} (F : Filter.Realizer f) : (Filter.Realizer.map m F).σ = F.σ

@[simp]

theorem Filter.Realizer.map_F {α : Type u_1} {β : Type u_2} (m : α → β) {f : Filter α} (F : Filter.Realizer f) (s : (Filter.Realizer.map m F).σ) : (Filter.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 : Filter.Realizer f) : Filter.Realizer (Filter.comap m f)

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

Equations

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

def Filter.Realizer.sup {α : Type u_1} {f : Filter α} {g : Filter α} (F : Filter.Realizer f) (G : Filter.Realizer g) : Filter.Realizer (f ⊔ g)

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 : Filter α} {g : Filter α} (F : Filter.Realizer f) (G : Filter.Realizer g) : Filter.Realizer (f ⊓ g)

Construct a realizer for the inf of two filters

Equations

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

def Filter.Realizer.cofinite {α : Type u_1} [DecidableEq α] : Filter.Realizer Filter.cofinite

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 : Filter.Realizer f) (G : (i : α) → Filter.Realizer (m i)) : Filter.Realizer (Filter.bind f m)

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 : α) → Filter.Realizer (f i)) : Filter.Realizer (⨆ (i : α), f i)

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 : Filter α} {g : Filter α} (F : Filter.Realizer f) (G : Filter.Realizer g) : Filter.Realizer (Filter.prod f g)

Construct a realizer for the product of filters

Equations

• Filter.Realizer.prod F G = Filter.Realizer.inf (Filter.Realizer.comap Prod.fst F) (Filter.Realizer.comap Prod.snd G)

theorem Filter.Realizer.le_iff {α : Type u_1} {f : Filter α} {g : Filter α} (F : Filter.Realizer f) (G : Filter.Realizer g) : 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₁ : Filter.Realizer l₁) (L₂ : Filter.Realizer l₂) : Filter.Tendsto f l₁ l₂ ↔ ∀ (b : L₂.σ), ∃ (a : L₁.σ), ∀ x ∈ L₁.F.f a, f x ∈ L₂.F.f b

theorem Filter.Realizer.ne_bot_iff {α : Type u_1} {f : Filter α} (F : Filter.Realizer f) : f ≠ ⊥ ↔ ∀ (a : F.σ), Set.Nonempty (F.F.f a)