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

Equations

• instInhabitedCFilter = { default := { f := id, pt := default, inf := fun (x1 x2 : α) => x1 ⊓ x2, inf_le_left := ⋯, inf_le_right := ⋯ } }

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

Equations

• CFilter.instCoeFunForall = { 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

• 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.

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

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

A CFilter realizes the filter it generates.

Equations

• F.toRealizer = { σ := σ, F := F, eq := ⋯ }

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) : g.Realizer

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 := ⋯ }

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

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

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

Equations

• F.ofEquiv E = { σ := τ, F := CFilter.ofEquiv E F.F, eq := ⋯ }

@[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 α) : (Filter.principal s).Realizer

Unit is a realizer for the principal filter

Equations

• Filter.Realizer.principal s = { σ := Unit, F := { f := fun (x : Unit) => s, pt := (), inf := fun (x x : Unit) => (), inf_le_left := ⋯, inf_le_right := ⋯ }, eq := ⋯ }

@[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.instInhabitedPrincipal {α : Type u_1} (s : Set α) : Inhabited (Filter.principal s).Realizer

Equations

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

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

Unit is a realizer for the top filter

Equations

• Filter.Realizer.top = Filter.Realizer.ofEq ⋯ (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} : ⊥.Realizer

Unit is a realizer for the bottom filter

Equations

• Filter.Realizer.bot = Filter.Realizer.ofEq ⋯ (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 : f.Realizer) : (Filter.map m f).Realizer

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

Equations

• Filter.Realizer.map m F = { σ := F.σ, F := { f := fun (s : F.σ) => m '' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }, eq := ⋯ }

@[simp]

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

@[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.f s = m '' F.F.f s

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

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

Equations

• Filter.Realizer.comap m F = { σ := F.σ, F := { f := fun (s : F.σ) => m ⁻¹' F.F.f s, pt := F.F.pt, inf := F.F.inf, inf_le_left := ⋯, inf_le_right := ⋯ }, eq := ⋯ }

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

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.cofinite.Realizer

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) : (f.bind m).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) : (f.prod g).Realizer

Construct a realizer for the product of filters

Equations

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

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) : 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 : f.Realizer) : f ≠ ⊥ ↔ ∀ (a : F.σ), (F.F.f a).Nonempty