LeanMachineLearning exposition

3.2.Β 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

  • Algorithm 𝓐 𝓨: a stochastic, sequential algorithm.

  • Environment 𝓐 𝓨: a stochastic environment.

  • IsAlgEnvSeq A 𝓨 alg env P: an algorithm-environment sequence. That is, a sequence of actions A and feedback Y that have the correct conditional distributions to be generated by an algorithm alg interacting with an environment env, defined on a probability space (Ξ©, P).

  • IsAlgEnvSeqUntil A Y alg env P N: A and Y form an algorithm-environment sequence until time N.

  • prod_left alg: an Algorithm 𝓐 (𝓧 Γ— 𝓨) obtained from an algorithm alg : Algorithm 𝓐 𝓨 by ignoring the 𝓧 component of each observation.

Module LeanMachineLearning.SequentialLearning.Algorithm contains 42 exposed declarations.

AlgorithmπŸ”—

StructureLearning.Algorithm
Details

A stochastic, sequential algorithm.

πŸ”—structure
Learning.Algorithm.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : Type (max u_4 u_5)
Learning.Algorithm.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] : Type (max u_4 u_5)

Code

structure Algorithm (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Policy or sampling rule: distribution of the next action. -/
  policy : (n : β„•) β†’ Kernel (Iic n β†’ 𝓐 Γ— 𝓨) 𝓐
  /-- The policy is a Markov kernel. -/
  [h_policy : βˆ€ n, IsMarkovKernel (policy n)]
  /-- Distribution of the first action. -/
  p0 : Measure 𝓐
  /-- The first action distribution is a probability measure. -/
  [hp0 : IsProbabilityMeasure p0]
Used by (216)

Actions: Source Β· Open Issue

instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicyπŸ”—

InstanceLearning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy
Details

No docstring.

πŸ”—theorem
Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.IsMarkovKernel (Algorithm.policy alg n)
Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.IsMarkovKernel
    (Algorithm.policy alg n)

Code

instance (alg : Algorithm 𝓐 𝓨) (n : β„•) : IsMarkovKernel (alg.policy n)
Type uses (1)
Used by (14)

Actions: Source Β· Open Issue

Proof
alg.h_policy n

instIsProbabilityMeasureP0πŸ”—

InstanceLearning.instIsProbabilityMeasureP0
Details

No docstring.

πŸ”—theorem
Learning.instIsProbabilityMeasureP0.{u_1, u_2} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) :
  MeasureTheory.IsProbabilityMeasure (Algorithm.p0 alg)
Learning.instIsProbabilityMeasureP0.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) :
  MeasureTheory.IsProbabilityMeasure
    (Algorithm.p0 alg)

Code

instance (alg : Algorithm 𝓐 𝓨) : IsProbabilityMeasure alg.p0
Type uses (1)
Used by (13)

Actions: Source Β· Open Issue

Proof
alg.hp0

prodLeftπŸ”—

DefinitionLearning.Algorithm.prodLeft
Details

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

πŸ”—def
Learning.Algorithm.prodLeft.{u_1, u_2, u_4} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (𝓧 : Type u_4) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) :
  Algorithm 𝓐 (𝓧 Γ— 𝓨)
Learning.Algorithm.prodLeft.{u_1, u_2,
    u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (𝓧 : Type u_4)
  [MeasurableSpace 𝓧]
  (alg : Algorithm 𝓐 𝓨) :
  Algorithm 𝓐 (𝓧 Γ— 𝓨)

Code

def Algorithm.prodLeft (𝓧 : Type*) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) :
    Algorithm 𝓐 (𝓧 Γ— 𝓨) where
  policy n := (alg.policy n).comap (fun h i ↦ ((h i).1, (h i).2.2)) (by fun_prop)
  p0 := alg.p0
Type uses (1)
Body uses (2)
Used by (6)

Actions: Source Β· Open Issue

prodLeft_p0πŸ”—

LemmaLearning.Algorithm.prodLeft_p0
Details

No docstring.

πŸ”—theorem
Learning.Algorithm.prodLeft_p0.{u_1, u_2, u_4} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (𝓧 : Type u_4) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) :
  p0 (prodLeft 𝓧 alg) = p0 alg
Learning.Algorithm.prodLeft_p0.{u_1, u_2,
    u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (𝓧 : Type u_4)
  [MeasurableSpace 𝓧]
  (alg : Algorithm 𝓐 𝓨) :
  p0 (prodLeft 𝓧 alg) = p0 alg

Code

theorem prodLeft_p0 : βˆ€ {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (𝓧 : Type u_4)
  [inst : MeasurableSpace 𝓧] (alg : Learning.Algorithm 𝓐 𝓨), (Learning.Algorithm.prodLeft 𝓧 alg).p0 = alg.p0
Type uses (2)

Actions: Source Β· Open Issue

Proof
@[simps]

prodLeft_policyπŸ”—

LemmaLearning.Algorithm.prodLeft_policy
Details

No docstring.

πŸ”—theorem
Learning.Algorithm.prodLeft_policy.{u_1, u_2, u_4} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (𝓧 : Type u_4) [MeasurableSpace 𝓧] (alg : Algorithm 𝓐 𝓨) (n : β„•) :
  policy (prodLeft 𝓧 alg) n =
    ProbabilityTheory.Kernel.comap (policy alg n)
      (fun h i => (Prod.fst (h i), Prod.snd (Prod.snd (h i)))) β‹―
Learning.Algorithm.prodLeft_policy.{u_1,
    u_2, u_4}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (𝓧 : Type u_4)
  [MeasurableSpace 𝓧]
  (alg : Algorithm 𝓐 𝓨) (n : β„•) :
  policy (prodLeft 𝓧 alg) n =
    ProbabilityTheory.Kernel.comap
      (policy alg n)
      (fun h i =>
        (Prod.fst (h i),
          Prod.snd (Prod.snd (h i))))
      β‹―

Code

theorem prodLeft_policy : βˆ€ {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (𝓧 : Type u_4)
  [inst : MeasurableSpace 𝓧] (alg : Learning.Algorithm 𝓐 𝓨) (n : β„•),
  (Learning.Algorithm.prodLeft 𝓧 alg).policy n = (alg.policy n).comap (fun h i => ((h i).1, (h i).2.2)) β‹―
Type uses (2)

Actions: Source Β· Open Issue

Proof
@[simps]

EnvironmentπŸ”—

StructureLearning.Environment
Details

A stochastic environment.

πŸ”—structure
Learning.Environment.{u_4, u_5} (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : Type (max u_4 u_5)
Learning.Environment.{u_4, u_5}
  (𝓐 : Type u_4) (𝓨 : Type u_5)
  [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] : Type (max u_4 u_5)

Code

structure Environment (𝓐 𝓨 : Type*) [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] where
  /-- Distribution of the next observation as function of the past history. -/
  feedback : (n : β„•) β†’ Kernel ((Iic n β†’ 𝓐 Γ— 𝓨) Γ— 𝓐) 𝓨
  /-- The feedback kernels are Markov kernels. -/
  [h_feedback : βˆ€ n, IsMarkovKernel (feedback n)]
  /-- Distribution of the first observation given the first action. -/
  Ξ½0 : Kernel 𝓐 𝓨
  /-- The initial observation kernel is a Markov kernel. -/
  [hp0 : IsMarkovKernel Ξ½0]
Used by (128)

Actions: Source Β· Open Issue

instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedbackπŸ”—

InstanceLearning.instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedback
Details

No docstring.

πŸ”—theorem
Learning.instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedback.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.IsMarkovKernel (Environment.feedback env n)
Learning.instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedback.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (env : Environment 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.IsMarkovKernel
    (Environment.feedback env n)

Code

instance (env : Environment 𝓐 𝓨) (n : β„•) : IsMarkovKernel (env.feedback n)
Type uses (1)
Used by (5)

Actions: Source Β· Open Issue

Proof
env.h_feedback n

instIsMarkovKernelΞ½0πŸ”—

InstanceLearning.instIsMarkovKernelΞ½0
Details

No docstring.

πŸ”—theorem
Learning.instIsMarkovKernelΞ½0.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (env : Environment 𝓐 𝓨) :
  ProbabilityTheory.IsMarkovKernel (Environment.Ξ½0 env)
Learning.instIsMarkovKernelΞ½0.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (env : Environment 𝓐 𝓨) :
  ProbabilityTheory.IsMarkovKernel
    (Environment.Ξ½0 env)

Code

instance (env : Environment 𝓐 𝓨) : IsMarkovKernel env.Ξ½0
Type uses (1)
Used by (8)

Actions: Source Β· Open Issue

Proof
env.hp0

stepKernelπŸ”—

DefinitionLearning.stepKernel
Details

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

πŸ”—def
Learning.stepKernel.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.Kernel (β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨) (𝓐 Γ— 𝓨)
Learning.stepKernel.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.Kernel
    (β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨) (𝓐 Γ— 𝓨)

Code

noncomputable
def stepKernel (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
    Kernel (Iic n β†’ 𝓐 Γ— 𝓨) (𝓐 Γ— 𝓨) :=
  alg.policy n βŠ—β‚– env.feedback n
deriving IsMarkovKernel
Type uses (2)
Used by (17)

Actions: Source Β· Open Issue

instIsMarkovKernelForallSubtypeNatMemFinsetIicProdStepKernelπŸ”—

InstanceLearning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdStepKernel
Details

No docstring.

πŸ”—theorem
Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdStepKernel.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨)
  (n : β„•) : ProbabilityTheory.IsMarkovKernel (stepKernel alg env n)
Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdStepKernel.{u_1,
    u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.IsMarkovKernel
    (stepKernel alg env n)

Code

deriving IsMarkovKernel
Type uses (3)
Body uses (2)
Used by (10)

Actions: Source Β· Open Issue

Proof
deriving IsMarkovKernel

stepKernel_defπŸ”—

LemmaLearning.stepKernel_def
Details

No docstring.

πŸ”—theorem
Learning.stepKernel_def.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
  stepKernel alg env n =
    ProbabilityTheory.Kernel.compProd (Algorithm.policy alg n)
      (Environment.feedback env n)
Learning.stepKernel_def.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : β„•) :
  stepKernel alg env n =
    ProbabilityTheory.Kernel.compProd
      (Algorithm.policy alg n)
      (Environment.feedback env n)

Code

lemma stepKernel_def (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
    stepKernel alg env n = alg.policy n βŠ—β‚– env.feedback n
Type uses (3)

Actions: Source Β· Open Issue

Proof
rfl

fst_stepKernelπŸ”—

LemmaLearning.fst_stepKernel
Details

No docstring.

πŸ”—theorem
Learning.fst_stepKernel.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.Kernel.fst (stepKernel alg env n) =
    Algorithm.policy alg n
Learning.fst_stepKernel.{u_1, u_2}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨}
  (alg : Algorithm 𝓐 𝓨)
  (env : Environment 𝓐 𝓨) (n : β„•) :
  ProbabilityTheory.Kernel.fst
      (stepKernel alg env n) =
    Algorithm.policy alg n

Code

lemma fst_stepKernel (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : β„•) :
    (stepKernel alg env n).fst = alg.policy n
Type uses (3)
Body uses (2)
Used by (1)

Actions: Source Β· Open Issue

Proof
by
  rw [stepKernel, Kernel.fst_compProd]

stepπŸ”—

DefinitionLearning.step
Details

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

πŸ”—def
Learning.step.{u_1, u_2, u_3} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) : 𝓐 Γ— 𝓨
Learning.step.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐)
  (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) : 𝓐 Γ— 𝓨

Code

def step (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) : 𝓐 Γ— 𝓨 :=
  (A n Ο‰, Y n Ο‰)
Used by (12)

Actions: Source Β· Open Issue

measurable_stepπŸ”—

LemmaLearning.measurable_step
Details

No docstring.

πŸ”—theorem
Learning.measurable_step.{u_1, u_2, u_3} {𝓐 : 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)
Learning.measurable_step.{u_1, u_2, u_3}
  {𝓐 : 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)

Code

lemma measurable_step (n : β„•) (hA : Measurable (A n)) (hY : Measurable (Y n)) :
    Measurable (step A Y n)
Type uses (1)
Used by (2)

Actions: Source Β· Open Issue

Proof
by
  unfold step
  fun_prop

trajectoryπŸ”—

DefinitionLearning.trajectory
Details

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

πŸ”—def
Learning.trajectory.{u_1, u_2, u_3} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (Ο‰ : Ξ©) : β„• β†’ 𝓐 Γ— 𝓨
Learning.trajectory.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐)
  (Y : β„• β†’ Ξ© β†’ 𝓨) (Ο‰ : Ξ©) : β„• β†’ 𝓐 Γ— 𝓨

Code

def trajectory (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (Ο‰ : Ξ©) : β„• β†’ 𝓐 Γ— 𝓨 := fun n ↦ (A n Ο‰, Y n Ο‰)
Used by (18)

Actions: Source Β· Open Issue

measurable_trajectoryπŸ”—

LemmaLearning.measurable_trajectory
Details

No docstring.

πŸ”—theorem
Learning.measurable_trajectory.{u_1, u_2, u_3} {𝓐 : 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)
Learning.measurable_trajectory.{u_1, u_2,
    u_3}
  {𝓐 : 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)

Code

lemma measurable_trajectory {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ n, Measurable (A n))
    (hR : βˆ€ n, Measurable (Y n)) : Measurable (trajectory A Y)
Type uses (1)
Used by (8)

Actions: Source Β· Open Issue

Proof
by
  unfold trajectory
  fun_prop

historyπŸ”—

DefinitionLearning.history
Details

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

πŸ”—def
Learning.history.{u_1, u_2, u_3} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) :
  β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨
Learning.history.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} (A : β„• β†’ Ξ© β†’ 𝓐)
  (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) :
  β†₯(Finset.Iic n) β†’ 𝓐 Γ— 𝓨

Code

def history (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (n : β„•) (Ο‰ : Ξ©) : Iic n β†’ 𝓐 Γ— 𝓨 :=
  fun i ↦ (A i Ο‰, Y i Ο‰)
Used by (72)

Actions: Source Β· Open Issue

measurable_historyπŸ”—

LemmaLearning.measurable_history
Details

No docstring.

πŸ”—theorem
Learning.measurable_history.{u_1, u_2, u_3} {𝓐 : 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)
Learning.measurable_history.{u_1, u_2,
    u_3}
  {𝓐 : 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)

Code

lemma measurable_history (hA : βˆ€ n, Measurable (A n))
    (hY : βˆ€ n, Measurable (Y n)) (n : β„•) :
    Measurable (history A Y n)
Type uses (1)
Used by (10)

Actions: Source Β· Open Issue

Proof
by
  unfold history
  fun_prop

eval_comp_historyπŸ”—

LemmaLearning.eval_comp_history
Details

No docstring.

πŸ”—theorem
Learning.eval_comp_history.{u_1, u_2, u_3} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
  (fun x => x ⟨n, β‹―βŸ©) ∘ history A Y n = step A Y n
Learning.eval_comp_history.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
  (fun x => x ⟨n, β‹―βŸ©) ∘ history A Y n =
    step A Y n

Code

lemma eval_comp_history (n : β„•) :
    (fun x ↦ x ⟨n, by simp⟩) ∘ (history A Y n) = step A Y n
Type uses (2)

Actions: Source Β· Open Issue

Proof
rfl

fst_eval_comp_historyπŸ”—

LemmaLearning.fst_eval_comp_history
Details

No docstring.

πŸ”—theorem
Learning.fst_eval_comp_history.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨}
  (n : β„•) : (fun x => Prod.fst (x ⟨n, β‹―βŸ©)) ∘ history A Y n = A n
Learning.fst_eval_comp_history.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
  (fun x => Prod.fst (x ⟨n, β‹―βŸ©)) ∘
      history A Y n =
    A n

Code

lemma fst_eval_comp_history (n : β„•) :
    (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (history A Y n) = A n
Type uses (1)

Actions: Source Β· Open Issue

Proof
rfl

snd_eval_comp_historyπŸ”—

LemmaLearning.snd_eval_comp_history
Details

No docstring.

πŸ”—theorem
Learning.snd_eval_comp_history.{u_1, u_2, u_3} {𝓐 : Type u_1}
  {𝓨 : Type u_2} {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨}
  (n : β„•) : (fun x => Prod.snd (x ⟨n, β‹―βŸ©)) ∘ history A Y n = Y n
Learning.snd_eval_comp_history.{u_1, u_2,
    u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
  (fun x => Prod.snd (x ⟨n, β‹―βŸ©)) ∘
      history A Y n =
    Y n

Code

lemma snd_eval_comp_history (n : β„•) :
    (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (history A Y n) = Y n
Type uses (1)

Actions: Source Β· Open Issue

Proof
rfl

history_succπŸ”—

LemmaLearning.history_succ
Details

No docstring.

πŸ”—theorem
Learning.history_succ.{u_1, u_2, u_3} {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨}
  {A : β„• β†’ Ξ© β†’ 𝓐} {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
  history A Y (n + 1) =
    ⇑(MeasurableEquiv.symm
          (MeasurableEquiv.IicSuccProd
            (fun x =>
              match x with
              | Nat => 𝓐 Γ— 𝓨)
            n)) ∘
      fun Ο‰ => (history A Y n Ο‰, step A Y (n + 1) Ο‰)
Learning.history_succ.{u_1, u_2, u_3}
  {𝓐 : Type u_1} {𝓨 : Type u_2}
  {Ξ© : Type u_3} {m𝓐 : MeasurableSpace 𝓐}
  {m𝓨 : MeasurableSpace 𝓨} {A : β„• β†’ Ξ© β†’ 𝓐}
  {Y : β„• β†’ Ξ© β†’ 𝓨} (n : β„•) :
  history A Y (n + 1) =
    ⇑(MeasurableEquiv.symm
          (MeasurableEquiv.IicSuccProd
            (fun x =>
              match x with
              | Nat => 𝓐 Γ— 𝓨)
            n)) ∘
      fun Ο‰ =>
      (history A Y n Ο‰,
        step A Y (n + 1) Ο‰)

Code

lemma history_succ (n : β„•) :
    history A Y (n + 1) =
      (MeasurableEquiv.IicSuccProd (fun β„• ↦ 𝓐 Γ— 𝓨) n).symm ∘
        (fun Ο‰ ↦ (history A Y n Ο‰, step A Y (n + 1) Ο‰))
Type uses (3)
Used by (2)

Actions: Source Β· Open Issue

Proof
by
  funext Ο‰
  symm
  exact (MeasurableEquiv.IicSuccProd (fun _ ↦ 𝓐 Γ— 𝓨) n).symm_apply_apply (history A Y (n + 1) Ο‰)

IsAlgEnvSeqπŸ”—

StructureLearning.IsAlgEnvSeq
Details

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

πŸ”—structure
Learning.IsAlgEnvSeq.{u_1, u_2, u_3} {𝓐 : 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] : Prop
Learning.IsAlgEnvSeq.{u_1, u_2, u_3}
  {𝓐 : 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] : Prop

Code

structure IsAlgEnvSeq
    (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨)
    (P : Measure Ξ©) [IsFiniteMeasure P] : Prop where
  /-- The action sequence is measurable. -/
  measurable_action n : Measurable (A n) := by fun_prop
  /-- The feedback sequence is measurable. -/
  measurable_feedback n : Measurable (Y n) := by fun_prop
  /-- The first action has the correct law. -/
  hasLaw_action_zero : HasLaw (fun Ο‰ ↦ (A 0 Ο‰)) alg.p0 P
  /-- The first feedback has the correct conditional distribution. -/
  hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (A 0) env.Ξ½0 P
  /-- The next action has the correct conditional distribution given the history. -/
  hasCondDistrib_action n :
    HasCondDistrib (A (n + 1)) (history A Y n) (alg.policy n) P
  /-- The next feedback has the correct conditional distribution given the history and
  next action. -/
  hasCondDistrib_feedback n :
    HasCondDistrib (Y (n + 1)) (fun Ο‰ ↦ (history A Y n Ο‰, A (n + 1) Ο‰))
      (env.feedback n) P
Type uses (3)
Used by (111)

Actions: Source Β· Open Issue

IsAlgEnvSeqUntilπŸ”—

StructureLearning.IsAlgEnvSeqUntil
Details

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

πŸ”—structure
Learning.IsAlgEnvSeqUntil.{u_1, u_2, u_3} {𝓐 : 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 : β„•) : Prop
Learning.IsAlgEnvSeqUntil.{u_1, u_2, u_3}
  {𝓐 : 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 : β„•) : Prop

Code

structure IsAlgEnvSeqUntil
    (A : β„• β†’ Ξ© β†’ 𝓐) (Y : β„• β†’ Ξ© β†’ 𝓨) (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨)
    (P : Measure Ξ©) [IsFiniteMeasure P] (N : β„•) : Prop where
  /-- The action sequence is measurable. -/
  measurable_action n : Measurable (A n) := by fun_prop
  /-- The feedback sequence is measurable. -/
  measurable_feedback n : Measurable (Y n) := by fun_prop
  /-- The first action has the correct law. -/
  hasLaw_action_zero : HasLaw (fun Ο‰ ↦ (A 0 Ο‰)) alg.p0 P
  /-- The first feedback has the correct conditional distribution. -/
  hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (A 0) env.Ξ½0 P
  /-- The next action has the correct conditional distribution given the history. -/
  hasCondDistrib_action n (hn : n < N) :
    HasCondDistrib (A (n + 1)) (history A Y n) (alg.policy n) P
  /-- The next feedback has the correct conditional distribution given the history and
  next action. -/
  hasCondDistrib_feedback n (hn : n < N) :
    HasCondDistrib (Y (n + 1)) (fun Ο‰ ↦ (history A Y n Ο‰, A (n + 1) Ο‰))
      (env.feedback n) P
Type uses (3)
Used by (22)

Actions: Source Β· Open Issue

monoπŸ”—

LemmaLearning.IsAlgEnvSeqUntil.mono
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeqUntil.mono.{u_1, u_2, u_3} {𝓐 : 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 : β„•} (h : IsAlgEnvSeqUntil A Y alg env P N) {N' : β„•}
  (hN : N' ≀ N) : IsAlgEnvSeqUntil A Y alg env P N'
Learning.IsAlgEnvSeqUntil.mono.{u_1, u_2,
    u_3}
  {𝓐 : 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 : β„•}
  (h : IsAlgEnvSeqUntil A Y alg env P N)
  {N' : β„•} (hN : N' ≀ N) :
  IsAlgEnvSeqUntil A Y alg env P N'

Code

lemma IsAlgEnvSeqUntil.mono (h : IsAlgEnvSeqUntil A Y alg env P N) {N' : β„•} (hN : N' ≀ N) :
    IsAlgEnvSeqUntil A Y alg env P N' where
  measurable_action
Type uses (3)
Body uses (1)
Used by (4)

Actions: Source Β· Open Issue

Proof
h.measurable_action
  measurable_feedback := h.measurable_feedback
  hasLaw_action_zero := h.hasLaw_action_zero
  hasCondDistrib_feedback_zero := h.hasCondDistrib_feedback_zero
  hasCondDistrib_action n hn := h.hasCondDistrib_action n (hn.trans_le hN)
  hasCondDistrib_feedback n hn := h.hasCondDistrib_feedback n (hn.trans_le hN)

isAlgEnvSeqUntilπŸ”—

LemmaLearning.IsAlgEnvSeq.isAlgEnvSeqUntil
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.isAlgEnvSeqUntil.{u_1, u_2, u_3} {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P) (N : β„•) :
  IsAlgEnvSeqUntil A Y alg env P N
Learning.IsAlgEnvSeq.isAlgEnvSeqUntil.{u_1,
    u_2, u_3}
  {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P)
  (N : β„•) :
  IsAlgEnvSeqUntil A Y alg env P N

Code

lemma IsAlgEnvSeq.isAlgEnvSeqUntil (h : IsAlgEnvSeq A Y alg env P) (N : β„•) :
    IsAlgEnvSeqUntil A Y alg env P N where
  measurable_action
Type uses (4)
Body uses (1)
Used by (2)

Actions: Source Β· Open Issue

Proof
h.measurable_action
  measurable_feedback := h.measurable_feedback
  hasLaw_action_zero := h.hasLaw_action_zero
  hasCondDistrib_feedback_zero := h.hasCondDistrib_feedback_zero
  hasCondDistrib_action n _ := h.hasCondDistrib_action n
  hasCondDistrib_feedback n _ := h.hasCondDistrib_feedback n

measurable_stepπŸ”—

LemmaLearning.IsAlgEnvSeq.measurable_step
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.measurable_step.{u_1, u_2, u_3} {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P) (n : β„•) : Measurable (step A Y n)
Learning.IsAlgEnvSeq.measurable_step.{u_1,
    u_2, u_3}
  {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P)
  (n : β„•) : Measurable (step A Y n)

Code

lemma IsAlgEnvSeq.measurable_step (h : IsAlgEnvSeq A Y alg env P) (n : β„•) :
    Measurable (step A Y n)
Type uses (4)
Body uses (1)
Used by (2)

Actions: Source Β· Open Issue

Proof
by
  have hA := h.measurable_action
  have hY := h.measurable_feedback
  fun_prop

measurable_historyπŸ”—

LemmaLearning.IsAlgEnvSeq.measurable_history
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.measurable_history.{u_1, u_2, u_3} {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P) (n : β„•) : Measurable (history A Y n)
Learning.IsAlgEnvSeq.measurable_history.{u_1,
    u_2, u_3}
  {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P)
  (n : β„•) : Measurable (history A Y n)

Code

lemma IsAlgEnvSeq.measurable_history (h : IsAlgEnvSeq A Y alg env P) (n : β„•) :
    Measurable (history A Y n)
Type uses (4)
Body uses (1)
Used by (4)

Actions: Source Β· Open Issue

Proof
by
  have hA := h.measurable_action
  have hY := h.measurable_feedback
  fun_prop

hasLaw_step_zeroπŸ”—

LemmaLearning.IsAlgEnvSeq.hasLaw_step_zero
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.hasLaw_step_zero.{u_1, u_2, u_3} {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P) :
  ProbabilityTheory.HasLaw (step A Y 0)
    (MeasureTheory.Measure.compProd (Algorithm.p0 alg)
      (Environment.Ξ½0 env))
    P
Learning.IsAlgEnvSeq.hasLaw_step_zero.{u_1,
    u_2, u_3}
  {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P) :
  ProbabilityTheory.HasLaw (step A Y 0)
    (MeasureTheory.Measure.compProd
      (Algorithm.p0 alg)
      (Environment.Ξ½0 env))
    P

Code

lemma IsAlgEnvSeq.hasLaw_step_zero (h : IsAlgEnvSeq A Y alg env P) :
    HasLaw (step A Y 0) (alg.p0 βŠ—β‚˜ env.Ξ½0) P
Type uses (4)
Body uses (1)
Used by (3)

Actions: Source Β· Open Issue

Proof
HasLaw.prod_of_hasCondDistrib h.hasLaw_action_zero h.hasCondDistrib_feedback_zero

hasLaw_step_zeroπŸ”—

LemmaLearning.IsAlgEnvSeqUntil.hasLaw_step_zero
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeqUntil.hasLaw_step_zero.{u_1, u_2, u_3}
  {𝓐 : 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 : β„•} (h : IsAlgEnvSeqUntil A Y alg env P N) :
  ProbabilityTheory.HasLaw (step A Y 0)
    (MeasureTheory.Measure.compProd (Algorithm.p0 alg)
      (Environment.Ξ½0 env))
    P
Learning.IsAlgEnvSeqUntil.hasLaw_step_zero.{u_1,
    u_2, u_3}
  {𝓐 : 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 : β„•}
  (h : IsAlgEnvSeqUntil A Y alg env P N) :
  ProbabilityTheory.HasLaw (step A Y 0)
    (MeasureTheory.Measure.compProd
      (Algorithm.p0 alg)
      (Environment.Ξ½0 env))
    P

Code

lemma IsAlgEnvSeqUntil.hasLaw_step_zero (h : IsAlgEnvSeqUntil A Y alg env P N) :
    HasLaw (step A Y 0) (alg.p0 βŠ—β‚˜ env.Ξ½0) P
Type uses (4)
Body uses (1)
Used by (1)

Actions: Source Β· Open Issue

Proof
HasLaw.prod_of_hasCondDistrib h.hasLaw_action_zero h.hasCondDistrib_feedback_zero

hasCondDistrib_stepπŸ”—

LemmaLearning.IsAlgEnvSeq.hasCondDistrib_step
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.hasCondDistrib_step.{u_1, u_2, u_3} {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P) (n : β„•) :
  ProbabilityTheory.HasCondDistrib (step A Y (n + 1)) (history A Y n)
    (stepKernel alg env n) P
Learning.IsAlgEnvSeq.hasCondDistrib_step.{u_1,
    u_2, u_3}
  {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P)
  (n : β„•) :
  ProbabilityTheory.HasCondDistrib
    (step A Y (n + 1)) (history A Y n)
    (stepKernel alg env n) P

Code

lemma IsAlgEnvSeq.hasCondDistrib_step (h : IsAlgEnvSeq A Y alg env P) (n : β„•) :
    HasCondDistrib (step A Y (n + 1)) (history A Y n) (stepKernel alg env n) P
Type uses (6)
Body uses (1)
Used by (3)

Actions: Source Β· Open Issue

Proof
HasCondDistrib.prod (h.hasCondDistrib_action n) (h.hasCondDistrib_feedback n)

hasCondDistrib_stepπŸ”—

LemmaLearning.IsAlgEnvSeqUntil.hasCondDistrib_step
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeqUntil.hasCondDistrib_step.{u_1, u_2, u_3}
  {𝓐 : 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 : β„•} (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
Learning.IsAlgEnvSeqUntil.hasCondDistrib_step.{u_1,
    u_2, u_3}
  {𝓐 : 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 : β„•}
  (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

Code

lemma IsAlgEnvSeqUntil.hasCondDistrib_step (h : IsAlgEnvSeqUntil A Y alg env P N)
    (n : β„•) (hn : n < N) :
    HasCondDistrib (step A Y (n + 1)) (history A Y n)
      (stepKernel alg env n) P
Type uses (6)
Body uses (1)
Used by (1)

Actions: Source Β· Open Issue

Proof
HasCondDistrib.prod (h.hasCondDistrib_action n hn) (h.hasCondDistrib_feedback n hn)

hasLaw_history_zeroπŸ”—

LemmaLearning.IsAlgEnvSeq.hasLaw_history_zero
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.hasLaw_history_zero.{u_1, u_2, u_3} {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P) :
  ProbabilityTheory.HasLaw (history A Y 0)
    (MeasureTheory.Measure.map
      (⇑(MeasurableEquiv.symm
          (MeasurableEquiv.piUnique fun x => 𝓐 Γ— 𝓨)))
      (MeasureTheory.Measure.map (step A Y 0) P))
    P
Learning.IsAlgEnvSeq.hasLaw_history_zero.{u_1,
    u_2, u_3}
  {𝓐 : 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]
  (h : IsAlgEnvSeq A Y alg env P) :
  ProbabilityTheory.HasLaw (history A Y 0)
    (MeasureTheory.Measure.map
      (⇑(MeasurableEquiv.symm
          (MeasurableEquiv.piUnique
            fun x => 𝓐 Γ— 𝓨)))
      (MeasureTheory.Measure.map
        (step A Y 0) P))
    P

Code

lemma IsAlgEnvSeq.hasLaw_history_zero (h : IsAlgEnvSeq A Y alg env P) : HasLaw (history A Y 0)
    ((P.map (step A Y 0)).map (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ 𝓐 Γ— 𝓨)).symm) P where
  aemeasurable
Type uses (5)
Body uses (2)
Used by (2)

Actions: Source Β· Open Issue

Proof
(h.measurable_history 0).aemeasurable
  map_eq := by
    have he : (MeasurableEquiv.piUnique (fun _ : Iic 0 ↦ 𝓐 Γ— 𝓨)).symm ∘ step A Y 0 =
        history A Y 0 := by
      funext _ ⟨0, _⟩
      rfl
    rw [← he]
    have hA := h.measurable_action
    have hY := h.measurable_feedback
    exact (Measure.map_map (by fun_prop) (by fun_prop)).symm

filtrationπŸ”—

DefinitionLearning.IsAlgEnvSeq.filtration
Details

Filtration generated by the history up to time n.

πŸ”—def
Learning.IsAlgEnvSeq.filtration.{u_1, u_2, u_3} {𝓐 : 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Ξ©
Learning.IsAlgEnvSeq.filtration.{u_1, u_2,
    u_3}
  {𝓐 : 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Ξ©

Code

def IsAlgEnvSeq.filtration (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Filtration β„• mΞ© where
  seq i := MeasurableSpace.comap (history A Y i) inferInstance
  mono' i j hij := by
    simp only
    rw [← measurable_iff_comap_le]
    have : history A Y i = (fun h k ↦ h ⟨k.1, by grind⟩) ∘ history A Y j := rfl
    rw [this]
    exact measurable_comp_comap _ (by fun_prop)
  le' i := by
    rw [← measurable_iff_comap_le]
    exact Learning.measurable_history hA hY i
Body uses (3)
Used by (18)

Actions: Source Β· Open Issue

adapted_historyπŸ”—

LemmaLearning.IsAlgEnvSeq.adapted_history
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.adapted_history.{u_1, u_2, u_3} {𝓐 : 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)
Learning.IsAlgEnvSeq.adapted_history.{u_1,
    u_2, u_3}
  {𝓐 : 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)

Code

lemma IsAlgEnvSeq.adapted_history
    (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Adapted (filtration hA hY) (history A Y)
Type uses (2)

Actions: Source Β· Open Issue

Proof
fun _ ↦ measurable_iff_comap_le.mpr le_rfl

adapted_stepπŸ”—

LemmaLearning.IsAlgEnvSeq.adapted_step
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.adapted_step.{u_1, u_2, u_3} {𝓐 : 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)
Learning.IsAlgEnvSeq.adapted_step.{u_1,
    u_2, u_3}
  {𝓐 : 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)

Code

lemma IsAlgEnvSeq.adapted_step
    (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Adapted (filtration hA hY) (step A Y)
Type uses (2)
Body uses (2)

Actions: Source Β· Open Issue

Proof
by
  intro n
  have : step A Y n = (fun h ↦ (h ⟨n, by simp⟩)) ∘ (history A Y n) := by
    ext Ο‰ : 1
    simp [history, step]
  rw [this]
  exact measurable_comp_comap _ (by fun_prop)

adapted_actionπŸ”—

LemmaLearning.IsAlgEnvSeq.adapted_action
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.adapted_action.{u_1, u_2, u_3} {𝓐 : 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
Learning.IsAlgEnvSeq.adapted_action.{u_1,
    u_2, u_3}
  {𝓐 : 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

Code

lemma IsAlgEnvSeq.adapted_action
    (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Adapted (filtration hA hY) A
Type uses (1)
Body uses (2)
Used by (3)

Actions: Source Β· Open Issue

Proof
by
  intro n
  have : A n = (fun h ↦ (h ⟨n, by simp⟩).1) ∘ (history A Y n) := by
    ext Ο‰ : 1
    simp [history]
  rw [this]
  exact measurable_comp_comap _ (by fun_prop)

adapted_feedbackπŸ”—

LemmaLearning.IsAlgEnvSeq.adapted_feedback
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.adapted_feedback.{u_1, u_2, u_3} {𝓐 : 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
Learning.IsAlgEnvSeq.adapted_feedback.{u_1,
    u_2, u_3}
  {𝓐 : 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

Code

lemma IsAlgEnvSeq.adapted_feedback
    (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Adapted (filtration hA hY) Y
Type uses (1)
Body uses (2)
Used by (1)

Actions: Source Β· Open Issue

Proof
by
  intro n
  have : Y n = (fun h ↦ (h ⟨n, by simp⟩).2) ∘ (history A Y n) := by
    ext Ο‰ : 1
    simp [history]
  rw [this]
  exact measurable_comp_comap _ (by fun_prop)

filtrationActionπŸ”—

DefinitionLearning.IsAlgEnvSeq.filtrationAction
Details

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

πŸ”—def
Learning.IsAlgEnvSeq.filtrationAction.{u_1, u_2, u_3} {𝓐 : 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Ξ©
Learning.IsAlgEnvSeq.filtrationAction.{u_1,
    u_2, u_3}
  {𝓐 : 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Ξ©

Code

def IsAlgEnvSeq.filtrationAction
    (hA : βˆ€ n, Measurable (A n)) (hY : βˆ€ n, Measurable (Y n)) :
    Filtration β„• mΞ© where
  seq n := if n = 0 then MeasurableSpace.comap (A 0) inferInstance
    else IsAlgEnvSeq.filtration hA hY (n - 1) βŠ” MeasurableSpace.comap (A n) inferInstance
  mono' n m hnm := by
    simp only
    by_cases hn : n = 0
    Β· by_cases hm : m = 0
      Β· simp [hn, hm]
      Β· simp only [hn, ↓reduceIte, hm]
        refine le_sup_of_le_left ?_
        rw [← measurable_iff_comap_le]
        suffices Measurable[IsAlgEnvSeq.filtration hA hY 0] (A 0) from
          this.mono ((IsAlgEnvSeq.filtration hA hY).mono zero_le) le_rfl
        exact adapted_action hA hY 0
    have hm : m β‰  0 := by grind
    simp only [hn, hm, ↓reduceIte]
    have hnm' : n - 1 ≀ m - 1 := by grind
    simp only [sup_le_iff]
    constructor
    Β· refine le_sup_of_le_left ?_
      exact (IsAlgEnvSeq.filtration hA hY).mono hnm'
    Β· rcases eq_or_lt_of_le hnm with rfl | hlt
      Β· exact le_sup_of_le_right le_rfl
      refine le_sup_of_le_left ?_
      rw [← measurable_iff_comap_le]
      have h_le : n ≀ m - 1 := by grind
      suffices Measurable[IsAlgEnvSeq.filtration hA hY n] (A n) from
        this.mono ((IsAlgEnvSeq.filtration hA hY).mono h_le) le_rfl
      exact adapted_action hA hY n
  le' n := by
    by_cases hn : n = 0
    Β· simp only [hn, ↓reduceIte]
      rw [← measurable_iff_comap_le]
      fun_prop
    simp only [hn, ↓reduceIte, sup_le_iff]
    constructor
    Β· exact (IsAlgEnvSeq.filtration hA hY).le _
    Β· rw [← measurable_iff_comap_le]
      fun_prop
Body uses (2)
Used by (3)

Actions: Source Β· Open Issue

filtrationAction_zero_eq_comapπŸ”—

LemmaLearning.IsAlgEnvSeq.filtrationAction_zero_eq_comap
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.filtrationAction_zero_eq_comap.{u_1, u_2, u_3}
  {𝓐 : 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
Learning.IsAlgEnvSeq.filtrationAction_zero_eq_comap.{u_1,
    u_2, u_3}
  {𝓐 : 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

Code

lemma IsAlgEnvSeq.filtrationAction_zero_eq_comap
    {hA : βˆ€ n, Measurable (A n)} {hY : βˆ€ n, Measurable (Y n)} :
    filtrationAction hA hY 0 = MeasurableSpace.comap (A 0) inferInstance
Type uses (1)
Body uses (1)

Actions: Source Β· Open Issue

Proof
by
  simp [filtrationAction]

filtrationAction_eq_comapπŸ”—

LemmaLearning.IsAlgEnvSeq.filtrationAction_eq_comap
Details

No docstring.

πŸ”—theorem
Learning.IsAlgEnvSeq.filtrationAction_eq_comap.{u_1, u_2, u_3}
  {𝓐 : 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
Learning.IsAlgEnvSeq.filtrationAction_eq_comap.{u_1,
    u_2, u_3}
  {𝓐 : 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

Code

lemma IsAlgEnvSeq.filtrationAction_eq_comap
    {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
Type uses (2)
Body uses (2)
Used by (1)

Actions: Source Β· Open Issue

Proof
by
  simp only [filtrationAction, filtration, ← MeasurableSpace.comap_prodMk, hn, ↓reduceIte]
  rfl
  1. Learning.Algorithm
  2. Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy
  3. Learning.instIsProbabilityMeasureP0
  4. Learning.Algorithm.prodLeft
  5. Learning.Algorithm.prodLeft_p0
  6. Learning.Algorithm.prodLeft_policy
  7. Learning.Environment
  8. Learning.instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedback
  9. Learning.instIsMarkovKernelΞ½0
  10. Learning.stepKernel
  11. Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdStepKernel
  12. Learning.stepKernel_def
  13. Learning.fst_stepKernel
  14. Learning.step
  15. Learning.measurable_step
  16. Learning.trajectory
  17. Learning.measurable_trajectory
  18. Learning.history
  19. Learning.measurable_history
  20. Learning.eval_comp_history
  21. Learning.fst_eval_comp_history
  22. Learning.snd_eval_comp_history
  23. Learning.history_succ
  24. Learning.IsAlgEnvSeq
  25. Learning.IsAlgEnvSeqUntil
  26. Learning.IsAlgEnvSeqUntil.mono
  27. Learning.IsAlgEnvSeq.isAlgEnvSeqUntil
  28. Learning.IsAlgEnvSeq.measurable_step
  29. Learning.IsAlgEnvSeq.measurable_history
  30. Learning.IsAlgEnvSeq.hasLaw_step_zero
  31. Learning.IsAlgEnvSeqUntil.hasLaw_step_zero
  32. Learning.IsAlgEnvSeq.hasCondDistrib_step
  33. Learning.IsAlgEnvSeqUntil.hasCondDistrib_step
  34. Learning.IsAlgEnvSeq.hasLaw_history_zero
  35. Learning.IsAlgEnvSeq.filtration
  36. Learning.IsAlgEnvSeq.adapted_history
  37. Learning.IsAlgEnvSeq.adapted_step
  38. Learning.IsAlgEnvSeq.adapted_action
  39. Learning.IsAlgEnvSeq.adapted_feedback
  40. Learning.IsAlgEnvSeq.filtrationAction
  41. Learning.IsAlgEnvSeq.filtrationAction_zero_eq_comap
  42. Learning.IsAlgEnvSeq.filtrationAction_eq_comap