LeanMachineLearning exposition

Learning.trajMeasure๐Ÿ”—

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

trajMeasure๐Ÿ”—

DefinitionLearning.trajMeasure
Details

Measure on the sequence of actions and observations generated by the algorithm/environment.

๐Ÿ”—def
Learning.trajMeasure.{u_1, u_2} {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“} {m๐“จ : MeasurableSpace ๐“จ}
  (alg : Algorithm ๐“ ๐“จ) (env : Environment ๐“ ๐“จ) :
  MeasureTheory.Measure (โ„• โ†’ ๐“ ร— ๐“จ)
Learning.trajMeasure.{u_1, u_2}
  {๐“ : Type u_1} {๐“จ : Type u_2}
  {m๐“ : MeasurableSpace ๐“}
  {m๐“จ : MeasurableSpace ๐“จ}
  (alg : Algorithm ๐“ ๐“จ)
  (env : Environment ๐“ ๐“จ) :
  MeasureTheory.Measure (โ„• โ†’ ๐“ ร— ๐“จ)

Code

noncomputable
def trajMeasure (alg : Algorithm ๐“ ๐“จ) (env : Environment ๐“ ๐“จ) :
    Measure (โ„• โ†’ ๐“ ร— ๐“จ) :=
  Kernel.trajMeasure (alg.p0 โŠ—โ‚˜ env.ฮฝ0) (stepKernel alg env)
deriving IsProbabilityMeasure
Type uses (2)
Body uses (2)
Used by (19)

Actions: Source ยท Open Issue

Dependency graph

Type dependencies (2)

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

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

All dependencies, transitively (4)

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

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

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

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