data.analysis.filter - mathlib3 docs

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

cfilter.has_sizeof_inst
cfilter.inhabited
cfilter.has_coe_to_fun

source

@[protected, instance]

def cfilter.inhabited {α : Type u_1} [inhabited α] [semilattice_inf α] :

inhabited (cfilter α α)

Equations

cfilter.inhabited = {default := {f := id α, pt := inhabited.default _inst_1, inf := has_inf.inf (semilattice_inf.to_has_inf α), inf_le_left := _, inf_le_right := _}}

source

@[protected, instance]

def cfilter.has_coe_to_fun {α : Type u_1} {σ : Type u_3} [partial_order α] :

has_coe_to_fun (cfilter α σ) (λ (_x : cfilter α σ), σ → α)

Equations

cfilter.has_coe_to_fun = {coe := cfilter.f _inst_1}

source

@[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

source

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

cfilter.of_equiv E {f := f, pt := p, inf := g, inf_le_left := h₁, inf_le_right := h₂} = {f := λ (a : τ), f (⇑(E.symm) a), pt := ⇑E p, inf := λ (a b : τ), ⇑E (g (⇑(E.symm) a) (⇑(E.symm) b)), inf_le_left := _, inf_le_right := _}

source

@[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)

source

def cfilter.to_filter {α : 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.to_filter = {sets := {a : set α | ∃ (b : σ), ⇑F b ⊆ a}, univ_sets := _, sets_of_superset := _, inter_sets := _}

source

@[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

source

structure filter.realizer {α : Type u_1} (f : filter α) :

Type (max u_1 (u_5+1))

σ : Type ?
F : cfilter (set α) self.σ
eq : self.F.to_filter = f

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

Instances for filter.realizer

filter.realizer.has_sizeof_inst
filter.realizer.realizer.inhabited

source

@[protected]

def cfilter.to_realizer {α : Type u_1} {σ : Type u_3} (F : cfilter (set α) σ) :

F.to_filter.realizer

A cfilter realizes the filter it generates.

Equations

F.to_realizer = {σ := σ, F := F, eq := _}

source

theorem filter.realizer.mem_sets {α : Type u_1} {f : filter α} (F : f.realizer) {a : set α} :

a ∈ f ↔ ∃ (b : F.σ), ⇑(F.F) b ⊆ a

source

def filter.realizer.of_eq {α : 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.of_eq e F = {σ := F.σ, F := F.F, eq := _}

source

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

f.realizer

A filter realizes itself.

Equations

filter.realizer.of_filter f = {σ := ↥(f.sets), F := {f := subtype.val (λ (x : set α), x ∈ f.sets), pt := ⟨set.univ α, _⟩, inf := λ (_x : ↥(f.sets)), filter.realizer.of_filter._match_2 f _x, inf_le_left := _, inf_le_right := _}, eq := _}
filter.realizer.of_filter._match_2 f ⟨x, h₁⟩ = λ (_x : ↥(f.sets)), filter.realizer.of_filter._match_1 f x h₁ _x
filter.realizer.of_filter._match_1 f x h₁ ⟨y, h₂⟩ = ⟨x ∩ y, _⟩

source

def filter.realizer.of_equiv {α : 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.of_equiv E = {σ := τ, F := cfilter.of_equiv E F.F, eq := _}

source

@[simp]

theorem filter.realizer.of_equiv_σ {α : Type u_1} {τ : Type u_4} {f : filter α} (F : f.realizer) (E : F.σ ≃ τ) :

(F.of_equiv E).σ = τ

source

@[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)

source

@[protected]

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 := λ (_x : unit), s, pt := unit.star(), inf := λ (_x _x : unit), unit.star(), inf_le_left := _, inf_le_right := _}, eq := _}

source

@[simp]

theorem filter.realizer.principal_σ {α : Type u_1} (s : set α) :

(filter.realizer.principal s).σ = unit

source

@[simp]

theorem filter.realizer.principal_F {α : Type u_1} (s : set α) (u : unit) :

⇑((filter.realizer.principal s).F) u = s

source

@[protected, instance]

def filter.realizer.realizer.inhabited {α : Type u_1} (s : set α) :

inhabited (filter.principal s).realizer

Equations

filter.realizer.realizer.inhabited s = {default := filter.realizer.principal s}

source

@[protected]

def filter.realizer.top {α : Type u_1} :

⊤.realizer

unit is a realizer for the top filter

Equations

filter.realizer.top = filter.realizer.of_eq filter.principal_univ (filter.realizer.principal set.univ)

source

@[simp]

theorem filter.realizer.top_σ {α : Type u_1} :

filter.realizer.top.σ = unit

source

@[simp]

theorem filter.realizer.top_F {α : Type u_1} (u : unit) :

⇑(filter.realizer.top.F) u = set.univ

source

@[protected]

def filter.realizer.bot {α : Type u_1} :

⊥.realizer

unit is a realizer for the bottom filter

Equations

filter.realizer.bot = filter.realizer.of_eq filter.principal_empty (filter.realizer.principal ∅)

source

@[simp]

theorem filter.realizer.bot_σ {α : Type u_1} :

filter.realizer.bot.σ = unit

source

@[simp]

theorem filter.realizer.bot_F {α : Type u_1} (u : unit) :

⇑(filter.realizer.bot.F) u = ∅

source

@[protected]

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 := λ (s : F.σ), m '' ⇑(F.F) s, pt := F.F.pt, inf := F.F.inf, inf_le_left := _, inf_le_right := _}, eq := _}

source

@[simp]

theorem filter.realizer.map_σ {α : Type u_1} {β : Type u_2} (m : α → β) {f : filter α} (F : f.realizer) :

(filter.realizer.map m F).σ = F.σ

source

@[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

source

@[protected]

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 := λ (s : F.σ), m ⁻¹' ⇑(F.F) s, pt := F.F.pt, inf := F.F.inf, inf_le_left := _, inf_le_right := _}, eq := _}

source

@[protected]

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

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')

source

@[protected]

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

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')

source

@[protected]

def filter.realizer.cofinite {α : Type u_1} [decidable_eq α] :

filter.cofinite.realizer

Construct a realizer for the cofinite filter

Equations

filter.realizer.cofinite = {σ := finset α, F := {f := λ (s : finset α), {a : α | a ∉ s}, pt := ∅, inf := has_union.union finset.has_union, inf_le_left := _, inf_le_right := _}, eq := _}

source

@[protected]

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

F.bind G = {σ := Σ (s : F.σ), Π (i : α), i ∈ ⇑(F.F) s → (G i).σ, F := {f := λ (_x : Σ (s : F.σ), Π (i : α), i ∈ ⇑(F.F) s → (G i).σ), filter.realizer.bind._match_1 F G _x, pt := ⟨F.F.pt, λ (i : α) (H : i ∈ ⇑(F.F) F.F.pt), (G i).F.pt⟩, inf := λ (_x : Σ (s : F.σ), Π (i : α), i ∈ ⇑(F.F) s → (G i).σ), filter.realizer.bind._match_3 F G _x, inf_le_left := _, inf_le_right := _}, eq := _}
filter.realizer.bind._match_1 F G ⟨s, f_1⟩ = ⋃ (i : α) (H : i ∈ ⇑(F.F) s), ⇑((G i).F) (f_1 i H)
filter.realizer.bind._match_3 F G ⟨a, f_1⟩ = λ (_x : Σ (s : F.σ), Π (i : α), i ∈ ⇑(F.F) s → (G i).σ), filter.realizer.bind._match_2 F G a f_1 _x
filter.realizer.bind._match_2 F G a f_1 ⟨b, f'⟩ = ⟨F.F.inf a b, λ (i : α) (h : i ∈ ⇑(F.F) (F.F.inf a b)), (G i).F.inf (f_1 i _) (f' i _)⟩

source

@[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

filter.realizer.Sup F = let F' : (⨆ (i : α), f i).realizer := filter.realizer.of_eq filter.realizer.Sup._proof_1 (filter.realizer.top.bind F) in F'.of_equiv (show (Σ (u : unit), Π (i : α), true → (F i).σ) ≃ Π (i : α), (F i).σ, from {to_fun := λ (_x : Σ (u : unit), Π (i : α), true → (F i).σ), filter.realizer.Sup._match_1 F _x, inv_fun := λ (f_1 : Π (i : α), (F i).σ), ⟨unit.star(), λ (i : α) (_x : true), f_1 i⟩, left_inv := _, right_inv := _})
filter.realizer.Sup._match_1 F ⟨_x, f_1⟩ = λ (i : α), f_1 i true.intro

source

@[protected]

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)

source

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

source

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

source

theorem filter.realizer.ne_bot_iff {α : Type u_1} {f : filter α} (F : f.realizer) :

f ≠ ⊥ ↔ ∀ (a : F.σ), (⇑(F.F) a).nonempty

mathlib3 documentation

Computational realization of filters (experimental) #

Main declarations #