Documentation

LeanPool.QuasiBorelSpaces.Functor

LeanPool.QuasiBorelSpaces.Functor #

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Functor.

source
class QuasiBorelSpace.Functor (F : (A : Type u_2) β†’ [QuasiBorelSpace A] β†’ Type u_1) :
Type (max u_1 (u_2 + 1))

A QuasiBorelSpace Functor is a function F : Type β†’ Type such that:

Instances
    source
    @[simp]
    theorem QuasiBorelSpace.Functor.map_comp_coe {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2} [Functor F] {A : Type u_1} [QuasiBorelSpace A] {B : Type u_1} [QuasiBorelSpace B] {C : Type u_1} [QuasiBorelSpace C] (f : B →𝒒 C) (g : A →𝒒 B) (x : F A) :
    (map f) ((map g) x) = (map (f.comp g)) x
    source
    class QuasiBorelSpace.Sequence (S : β„• β†’ Type u_1) :
    Type u_1

    A Sequence is a sequence of types S : β„• β†’ Type such that:

    Instances
      source
      structure QuasiBorelSpace.Comp (F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2) [Functor F] (S : β„• β†’ Type u_1) [Sequence S] (n : β„•) :
      Type u_2

      The composition of a Functor with a Sequence.

      • get : F (S n)

        The underlying element of F (S n).

      Instances For
        source
        theorem QuasiBorelSpace.Comp.ext {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2} [Functor F] {S : β„• β†’ Type u_1} [Sequence S] {n : β„•} {x y : Comp F S n} (h : x.get = y.get) :
        x = y
        source
        theorem QuasiBorelSpace.Comp.ext_iff {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2} [Functor F] {S : β„• β†’ Type u_1} [Sequence S] {n : β„•} {x y : Comp F S n} :
        x = y ↔ x.get = y.get
        source
        @[instance_reducible]
        instance QuasiBorelSpace.Comp.inst {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2} [Functor F] {S : β„• β†’ Type u_1} [Sequence S] {n : β„•} :
        QuasiBorelSpace (Comp F S n)
        Equations
        source
        theorem QuasiBorelSpace.Comp.isHom_mk {F : (A : Type u_2) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {S : β„• β†’ Type u_2} [Sequence S] {n : β„•} :
        IsHom QuasiBorelSpace.Comp.mk✝
        source
        theorem QuasiBorelSpace.Comp.isHom_get {F : (A : Type u_2) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {S : β„• β†’ Type u_2} [Sequence S] {n : β„•} :
        IsHom get
        source
        @[instance_reducible]
        instance QuasiBorelSpace.Comp.instSequence {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2} [Functor F] {S : β„• β†’ Type u_1} [Sequence S] :
        Sequence (Comp F S)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem QuasiBorelSpace.Comp.project_def {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2} [Functor F] {S : β„• β†’ Type u_1} [Sequence S] (n : β„•) :
        Sequence.project n = { toFun := fun (x : Comp F S (n + 1)) => { get := (Functor.map (Sequence.project n)) x.get }, property := β‹― }
        source
        structure QuasiBorelSpace.Limit (S : β„• β†’ Type u_1) [Sequence S] :
        Type u_1

        The Limit of a Sequence S consists of:

        • toFun (n : β„•) : S n
          1. A sequence of elements, one from each S n.
        • property (n : β„•) : (Sequence.project n) (self.toFun (n + 1)) = self.toFun n
          1. A proof that every element is the projection of its successor.
        Instances For
          source
          @[instance_reducible]
          instance QuasiBorelSpace.Limit.instDFunLikeNat {S : β„• β†’ Type u_1} [Sequence S] :
          DFunLike (Limit S) β„• S
          Equations
          source
          def QuasiBorelSpace.Limit.Simps.coe {S : β„• β†’ Type u_1} [Sequence S] (f : Limit S) (n : β„•) :
          S n

          A simps projection for function coercion.

          Equations
          Instances For
            source
            theorem QuasiBorelSpace.Limit.ext {S : β„• β†’ Type u_1} [Sequence S] {f g : Limit S} (h : βˆ€ (x : β„•), f x = g x) :
            f = g
            source
            theorem QuasiBorelSpace.Limit.ext_iff {S : β„• β†’ Type u_1} [Sequence S] {f g : Limit S} :
            f = g ↔ βˆ€ (x : β„•), f x = g x
            source
            def QuasiBorelSpace.Limit.copy {S : β„• β†’ Type u_1} [Sequence S] (f : Limit S) (f' : (n : β„•) β†’ S n) (h : f' = ⇑f) :
            Limit S

            Copy of a QuasiBorelHom with a new toFun equal to the old one. Useful to fix definitional equalities.

            Equations
            • f.copy f' h = { toFun := f', property := β‹― }
            Instances For
              source
              @[simp]
              theorem QuasiBorelSpace.Limit.coe_mk {S : β„• β†’ Type u_1} [Sequence S] {f : (n : β„•) β†’ S n} (hf : βˆ€ (n : β„•), (Sequence.project n) (f (n + 1)) = f n) :
              ⇑{ toFun := f, property := hf } = f
              source
              @[simp]
              theorem QuasiBorelSpace.Limit.eta {S : β„• β†’ Type u_1} [Sequence S] (f : Limit S) :
              { toFun := ⇑f, property := β‹― } = f
              source
              @[simp]
              theorem QuasiBorelSpace.Limit.toFun_eq_coe {S : β„• β†’ Type u_1} [Sequence S] (f : Limit S) :
              f.toFun = ⇑f
              source
              @[simp]
              theorem QuasiBorelSpace.Limit.project_coe {S : β„• β†’ Type u_1} [Sequence S] (n : β„•) (f : Limit S) :
              (Sequence.project n) (f (n + 1)) = f n
              source
              @[instance_reducible]
              instance QuasiBorelSpace.Limit.inst {S : β„• β†’ Type u_1} [Sequence S] :
              QuasiBorelSpace (Limit S)
              Equations
              source
              theorem QuasiBorelSpace.Limit.isHom_mk {A : Type u_2} [QuasiBorelSpace A] {S : β„• β†’ Type u_1} [Sequence S] {f : A β†’ (n : β„•) β†’ S n} (hf₁ : IsHom f) (hfβ‚‚ : βˆ€ (x : A) (n : β„•), (Sequence.project n) (f x (n + 1)) = f x n) :
              IsHom fun (x : A) => { toFun := f x, property := β‹― }
              source
              theorem QuasiBorelSpace.Limit.isHom_coe {A : Type u_2} [QuasiBorelSpace A] {S : β„• β†’ Type u_1} [Sequence S] {f : A β†’ Limit S} (hf : IsHom f) {n : β„•} :
              IsHom fun (x : A) => (f x) n
              source
              structure QuasiBorelSpace.Iter (F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1) [Functor F] (n : β„•) :
              Type u_1

              The Sequence obtained by iterating a Functor.

              Instances For
                source
                @[instance_reducible]
                instance QuasiBorelSpace.Iter.inst {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {n : β„•} :
                QuasiBorelSpace (Iter F n)
                Equations
                source
                @[simp]
                theorem QuasiBorelSpace.Iter.isHom_get {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {n : β„•} :
                IsHom get
                source
                @[simp]
                theorem QuasiBorelSpace.Iter.isHom_mk {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {n : β„•} :
                IsHom QuasiBorelSpace.Iter.mk✝
                source
                def QuasiBorelSpace.Iter.zero {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] :
                Iter F 0

                Zero element constructor.

                Equations
                Instances For
                  source
                  instance QuasiBorelSpace.Iter.instSubsingletonOfNatNat {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] :
                  Subsingleton (Iter F 0)
                  source
                  def QuasiBorelSpace.Iter.succ {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {n : β„•} :
                  F (Iter F n) →𝒒 Iter F (n + 1)

                  Successor element constructor.

                  Equations
                  Instances For
                    source
                    def QuasiBorelSpace.Iter.unsucc {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {n : β„•} :
                    Iter F (n + 1) →𝒒 F (Iter F n)

                    Successor element destructor.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem QuasiBorelSpace.Iter.succ_unsucc {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {n : β„•} (x : Iter F (n + 1)) :
                      succ (unsucc x) = x
                      source
                      @[simp]
                      theorem QuasiBorelSpace.Iter.unsucc_succ {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {n : β„•} (x : F (Iter F n)) :
                      unsucc (succ x) = x
                      source
                      theorem QuasiBorelSpace.Iter.succ_injective {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] {n : β„•} {x y : F (Iter F n)} (h : succ x = succ y) :
                      x = y
                      source
                      @[instance_reducible]
                      instance QuasiBorelSpace.Iter.instSequence {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] :
                      Sequence (Iter F)
                      Equations
                      source
                      @[simp]
                      theorem QuasiBorelSpace.Iter.project_zero {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] :
                      Sequence.project 0 = { toFun := fun (x : Iter F (0 + 1)) => zero, property := β‹― }
                      source
                      @[simp]
                      theorem QuasiBorelSpace.Iter.project_succ {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] {n : β„•} :
                      Sequence.project (n + 1) = succ.comp ((Functor.map (Sequence.project n)).comp unsucc)
                      source
                      def QuasiBorelSpace.Iter.unfold {A : Type} [QuasiBorelSpace A] {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] (f : A →𝒒 F A) (n : β„•) :
                      A →𝒒 Iter F n

                      Constructs an Iterated sequence of a Functor from an unfolding function.

                      Equations
                      Instances For
                        source
                        class QuasiBorelSpace.Continuous (F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2) [Functor F] :
                        Type (max (u_1 + 1) u_2)

                        A functor F is continuous if it preserves Limits.

                        Instances
                          source
                          @[simp]
                          theorem QuasiBorelSpace.Continuous.seq_unseq_coe {F : (A : Type u_2) β†’ [QuasiBorelSpace A] β†’ Type u_1} [Functor F] [Continuous F] {S : β„• β†’ Type u_2} [Sequence S] (x : Limit (Comp F S)) :
                          seq (unseq x) = x
                          source
                          @[simp]
                          theorem QuasiBorelSpace.Continuous.unseq_seq_coe {F : (A : Type u_1) β†’ [QuasiBorelSpace A] β†’ Type u_2} [Functor F] [Continuous F] {S : β„• β†’ Type u_1} [Sequence S] (x : F (Limit S)) :
                          unseq (seq x) = x
                          source
                          structure QuasiBorelSpace.Nu (F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type) [Functor F] :
                          Type

                          The greatest fixed point of a Functor.

                          • get : Limit (Iter F)

                            The underlying compatible sequence of finite iterates.

                          Instances For
                            source
                            @[instance_reducible]
                            instance QuasiBorelSpace.Nu.inst {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] :
                            QuasiBorelSpace (Nu F)
                            Equations
                            source
                            @[simp]
                            theorem QuasiBorelSpace.Nu.isHom_get {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] :
                            IsHom get
                            source
                            @[simp]
                            theorem QuasiBorelSpace.Nu.isHom_mk {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] :
                            IsHom QuasiBorelSpace.Nu.mk✝
                            source
                            def QuasiBorelSpace.Nu.roll {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] [Continuous F] :
                            F (Nu F) →𝒒 Nu F

                            Rolls a Functor into a Nu.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def QuasiBorelSpace.Nu.unroll {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] [Continuous F] :
                              Nu F →𝒒 F (Nu F)

                              Unrolls a Functor out of a Nu.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                @[simp]
                                theorem QuasiBorelSpace.Nu.roll_unroll {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] [Continuous F] (x : Nu F) :
                                roll (unroll x) = x
                                source
                                @[simp]
                                theorem QuasiBorelSpace.Nu.unroll_roll {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] [Continuous F] (x : F (Nu F)) :
                                unroll (roll x) = x
                                source
                                def QuasiBorelSpace.Nu.unfold {A : Type} [QuasiBorelSpace A] {F : (A : Type) β†’ [QuasiBorelSpace A] β†’ Type} [Functor F] (f : A →𝒒 F A) :
                                A →𝒒 Nu F

                                Constructs a Nu from an unfolding.

                                Equations
                                Instances For