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)

• f : σ → α
• pt : σ
• inf : σ → σ → σ
• inf_le_left : ∀ (a b : σ), CFilter.f s (CFilter.inf s a b) ≤ CFilter.f s a
• inf_le_right : ∀ (a b : σ), CFilter.f s (CFilter.inf s a b) ≤ CFilter.f s 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.

instance instInhabitedCFilterToPartialOrder {α : Type u_1} [Inhabited α] [SemilatticeInf α] : Inhabited (CFilter α α)

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

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 : σ) : CFilter.f { f := f, pt := pt, inf := inf, inf_le_left := h₁, inf_le_right := h₂ } 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.

@[simp]

theorem CFilter.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} [PartialOrder α] (E : σ ≃ τ) (F : CFilter α σ) (a : τ) : CFilter.f (CFilter.ofEquiv E F) a = CFilter.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.

@[simp]

theorem CFilter.mem_toFilter_sets {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) {a : Set α} : a ∈ CFilter.toFilter F ↔ ∃ b, CFilter.f F b ⊆ a

structure Filter.Realizer {α : Type u_1} (f : Filter α) : Type (max u_1 (u_5 + 1))

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

A realizer for filter f is a cfilter which generates 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.

theorem Filter.Realizer.mem_sets {α : Type u_1} {f : Filter α} (F : Filter.Realizer f) {a : Set α} : a ∈ f ↔ ∃ b, CFilter.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.

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

A filter realizes itself.

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.

@[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 : τ) : CFilter.f (Filter.Realizer.ofEquiv F E).F s = CFilter.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

@[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) : CFilter.f (Filter.Realizer.principal s).F u = s

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

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

Unit is a realizer for the top filter

@[simp]

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

@[simp]

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

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

Unit is a realizer for the bottom filter

@[simp]

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

@[simp]

theorem Filter.Realizer.bot_F {α : Type u_1} (u : Unit) : CFilter.f Filter.Realizer.bot.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

@[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).σ) : CFilter.f (Filter.Realizer.map m F).F s = m '' CFilter.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

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

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

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

Construct a realizer for the cofinite filter

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

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

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

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, CFilter.f F.F a ≤ CFilter.f G.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, ∀ (x : α), x ∈ CFilter.f L₁.F a → f x ∈ CFilter.f L₂.F b

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