Documentation

LeanMachineLearning.SequentialLearning.Algorithm

Algorithms and environments #

We define structures for stochastic, sequential algorithms and environments, and the notion of an algorithm-environment sequence, which is a sequence of actions and feedbacks generated by an algorithm interacting with an environment.

Main definitions #

source
structure Learning.Algorithm (𝓐 : Type u_4) (𝓨 : Type u_5) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
Type (max u_4 u_5)

A stochastic, sequential algorithm.

Instances For
    source
    instance Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) (n : β„•) :
    ProbabilityTheory.IsMarkovKernel (alg.policy n)
    source
    instance Learning.instIsProbabilityMeasureP0 {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) :
    MeasureTheory.IsProbabilityMeasure alg.p0
    source
    def Learning.Algorithm.prodLeft {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (𝓧 : Type u_4) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) :
    Algorithm 𝓐 (𝓧 Γ— 𝓨)

    An algorithm with observations in 𝓧 Γ— 𝓨 obtained from an algorithm with observations in 𝓨 by ignoring the 𝓧 component of each observation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Learning.Algorithm.prodLeft_p0 {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (𝓧 : Type u_4) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) :
      (prodLeft 𝓧 alg).p0 = alg.p0
      source
      @[simp]
      theorem Learning.Algorithm.prodLeft_policy {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (𝓧 : Type u_4) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) (n : β„•) :
      (prodLeft 𝓧 alg).policy n = (alg.policy n).comap (fun (h : β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓧 Γ— 𝓨) (i : β†₯(Finset.Iic n)) => ((h i).1, (h i).2.2)) β‹―
      source
      structure Learning.Environment (𝓐 : Type u_4) (𝓨 : Type u_5) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] :
      Type (max u_4 u_5)

      A stochastic environment.

      Instances For
        source
        instance Learning.instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedback {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓐 𝓨) (n : β„•) :
        ProbabilityTheory.IsMarkovKernel (env.feedback n)
        source
        instance Learning.instIsMarkovKernelΞ½0 {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓐 𝓨) :
        ProbabilityTheory.IsMarkovKernel env.Ξ½0
        source
        noncomputable def Learning.stepKernel {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
        ProbabilityTheory.Kernel (β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨) (𝓐 Γ— 𝓨)

        Kernel describing the distribution of the next action-feedback pair given the history up to n.

        Equations
        Instances For
          source
          instance Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdStepKernel {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
          ProbabilityTheory.IsMarkovKernel (stepKernel alg env n)
          source
          theorem Learning.stepKernel_def {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
          stepKernel alg env n = (alg.policy n).compProd (env.feedback n)
          source
          @[simp]
          theorem Learning.fst_stepKernel {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
          (stepKernel alg env n).fst = alg.policy n
          source
          def Learning.step {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) :
          𝓐 Γ— 𝓨

          Step of the algorithm-environment sequence: the action-feedback pair at time n.

          Equations
          Instances For
            source
            theorem Learning.measurable_step {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) (hA : Measurable (A n)) (hY : Measurable (Y n)) :
            Measurable (step A Y n)
            source
            def Learning.trajectory {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (Ο‰ : Ξ©) :
            β„• β†’ 𝓐 Γ— 𝓨

            A random variable that gives the sequence of action-feedback pairs.

            Equations
            Instances For
              source
              theorem Learning.measurable_trajectory {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hR : βˆ€ (n : β„•), Measurable (Y n)) :
              Measurable (trajectory A Y)
              source
              def Learning.history {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) :
              β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨

              History of the algorithm-environment sequence up to time n.

              Equations
              Instances For
                source
                theorem Learning.measurable_history {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hY : βˆ€ (n : β„•), Measurable (Y n)) (n : β„•) :
                Measurable (history A Y n)
                source
                theorem Learning.eval_comp_history {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
                (fun (x : β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨) => x ⟨n, β‹―βŸ©) ∘ history A Y n = step A Y n
                source
                theorem Learning.fst_eval_comp_history {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
                (fun (x : β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨) => (x ⟨n, β‹―βŸ©).1) ∘ history A Y n = A n
                source
                theorem Learning.snd_eval_comp_history {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
                (fun (x : β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨) => (x ⟨n, β‹―βŸ©).2) ∘ history A Y n = Y n
                source
                structure Learning.IsAlgEnvSeq {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (P : MeasureTheory.Measure Ξ©) [MeasureTheory.IsFiniteMeasure P] :
                Prop

                An algorithm-environment sequence: a sequence of actions and feedbacks generated by an algorithm interacting with an environment.

                Instances For
                  source
                  structure Learning.IsAlgEnvSeqUntil {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (P : MeasureTheory.Measure Ξ©) [MeasureTheory.IsFiniteMeasure P] (N : β„•) :
                  Prop

                  An algorithm-environment sequence: a sequence of actions and feedbacks generated by an algorithm interacting with an environment.

                  Instances For
                    source
                    theorem Learning.IsAlgEnvSeqUntil.mono {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] {N : β„•} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeqUntil A Y alg env P N) {N' : β„•} (hN : N' ≀ N) :
                    IsAlgEnvSeqUntil A Y alg env P N'
                    source
                    theorem Learning.IsAlgEnvSeq.isAlgEnvSeqUntil {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg env P) (N : β„•) :
                    IsAlgEnvSeqUntil A Y alg env P N
                    source
                    theorem Learning.IsAlgEnvSeq.measurable_step {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg env P) (n : β„•) :
                    Measurable (step A Y n)
                    source
                    theorem Learning.IsAlgEnvSeq.measurable_history {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg env P) (n : β„•) :
                    Measurable (history A Y n)
                    source
                    theorem Learning.IsAlgEnvSeq.hasLaw_step_zero {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg env P) :
                    ProbabilityTheory.HasLaw (step A Y 0) (alg.p0.compProd env.Ξ½0) P
                    source
                    theorem Learning.IsAlgEnvSeqUntil.hasLaw_step_zero {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] {N : β„•} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeqUntil A Y alg env P N) :
                    ProbabilityTheory.HasLaw (step A Y 0) (alg.p0.compProd env.Ξ½0) P
                    source
                    theorem Learning.IsAlgEnvSeq.hasCondDistrib_step {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg env P) (n : β„•) :
                    ProbabilityTheory.HasCondDistrib (step A Y (n + 1)) (history A Y n) (stepKernel alg env n) P
                    source
                    theorem Learning.IsAlgEnvSeqUntil.hasCondDistrib_step {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] {N : β„•} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeqUntil A Y alg env P N) (n : β„•) (hn : n < N) :
                    ProbabilityTheory.HasCondDistrib (step A Y (n + 1)) (history A Y n) (stepKernel alg env n) P
                    source
                    theorem Learning.IsAlgEnvSeq.hasLaw_history_zero {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg env P) :
                    ProbabilityTheory.HasLaw (history A Y 0) (MeasureTheory.Measure.map (⇑(MeasurableEquiv.piUnique fun (x : β†₯(Finset.Iic 0)) => 𝓐 Γ— 𝓨).symm) (MeasureTheory.Measure.map (step A Y 0) P)) P
                    source
                    theorem Learning.IsAlgEnvSeq.hasLaw_history_succ {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsAlgEnvSeq A Y alg env P) (n : β„•) :
                    ProbabilityTheory.HasLaw (history A Y (n + 1)) (MeasureTheory.Measure.map (⇑(MeasurableEquiv.IicSuccProd (fun (x : β„•) => 𝓐 Γ— 𝓨) n).symm) ((MeasureTheory.Measure.map (history A Y n) P).compProd 𝓛[step A Y (n + 1) | history A Y n; P])) P
                    source
                    def Learning.IsAlgEnvSeq.filtration {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hY : βˆ€ (n : β„•), Measurable (Y n)) :
                    MeasureTheory.Filtration β„• mΞ©

                    Filtration generated by the history up to time n.

                    Equations
                    Instances For
                      source
                      theorem Learning.IsAlgEnvSeq.adapted_history {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hY : βˆ€ (n : β„•), Measurable (Y n)) :
                      MeasureTheory.Adapted (filtration hA hY) (history A Y)
                      source
                      theorem Learning.IsAlgEnvSeq.adapted_step {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hY : βˆ€ (n : β„•), Measurable (Y n)) :
                      MeasureTheory.Adapted (filtration hA hY) (step A Y)
                      source
                      theorem Learning.IsAlgEnvSeq.adapted_action {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hY : βˆ€ (n : β„•), Measurable (Y n)) :
                      MeasureTheory.Adapted (filtration hA hY) A
                      source
                      theorem Learning.IsAlgEnvSeq.adapted_feedback {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hY : βˆ€ (n : β„•), Measurable (Y n)) :
                      MeasureTheory.Adapted (filtration hA hY) Y
                      source
                      def Learning.IsAlgEnvSeq.filtrationAction {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hY : βˆ€ (n : β„•), Measurable (Y n)) :
                      MeasureTheory.Filtration β„• mΞ©

                      Filtration generated by the history at time n-1 together with the action at time n.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem Learning.IsAlgEnvSeq.filtrationAction_zero_eq_comap {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {hA : βˆ€ (n : β„•), Measurable (A n)} {hY : βˆ€ (n : β„•), Measurable (Y n)} :
                        ↑(filtrationAction hA hY) 0 = MeasurableSpace.comap (A 0) inferInstance
                        source
                        theorem Learning.IsAlgEnvSeq.filtrationAction_eq_comap {𝓐 : Type u_1} {𝓨 : Type u_2} {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} {hA : βˆ€ (n : β„•), Measurable (A n)} {hY : βˆ€ (n : β„•), Measurable (Y n)} (n : β„•) (hn : n β‰  0) :
                        ↑(filtrationAction hA hY) n = MeasurableSpace.comap (fun (Ο‰ : Ξ©) => (history A Y (n - 1) Ο‰, A n Ο‰)) inferInstance