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
Instances For
    theorem CFilter.inf_le_left {α : Type u_1} {σ : Type u_2} [PartialOrder α] (self : CFilter α σ) (a : σ) (b : σ) :
    self.f (self.inf a b) self.f a
    theorem CFilter.inf_le_right {α : Type u_1} {σ : Type u_2} [PartialOrder α] (self : CFilter α σ) (a : σ) (b : σ) :
    self.f (self.inf a b) self.f b
    instance instInhabitedCFilter {α : Type u_1} [Inhabited α] [SemilatticeInf α] :
    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.
    Instances For
      @[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 α) σ) :

      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 := }
      Instances For
        @[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.

        Instances For
          theorem Filter.Realizer.eq {α : Type u_1} {f : Filter α} (self : f.Realizer) :
          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 := }
          Instances For
            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 : Filter α} {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
            Instances For
              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.
              Instances For
                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
                Instances For
                  @[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
                  Instances For
                    @[simp]
                    @[simp]
                    theorem Filter.Realizer.principal_F {α : Type u_1} (s : Set α) (u : Unit) :
                    def Filter.Realizer.top {α : Type u_1} :
                    .Realizer

                    Unit is a realizer for the top filter

                    Equations
                    Instances For
                      @[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
                      Instances For
                        @[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 := }
                        Instances For
                          @[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 := }
                          Instances For
                            def Filter.Realizer.sup {α : Type u_1} {f : Filter α} {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.
                            Instances For
                              def Filter.Realizer.inf {α : Type u_1} {f : Filter α} {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.
                              Instances For
                                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.
                                Instances For
                                  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.
                                  Instances For
                                    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.
                                    Instances For
                                      def Filter.Realizer.prod {α : Type u_1} {f : Filter α} {g : Filter α} (F : f.Realizer) (G : g.Realizer) :
                                      (f.prod g).Realizer

                                      Construct a realizer for the product of filters

                                      Equations
                                      Instances For
                                        theorem Filter.Realizer.le_iff {α : Type u_1} {f : Filter α} {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₁), 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