Learning.fst_stepKernel
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.
fst_stepKernelπ
Learning.fst_stepKernelNo docstring.
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 nLearning.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 nType uses (3)
Body uses (2)
Used by (1)
Actions: Source Β· Open Issue
Proof
by rw [stepKernel, Kernel.fst_compProd]
Dependency graph
Type dependencies (3)
Algorithmπ
Learning.AlgorithmA stochastic, sequential algorithm.
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π
Learning.EnvironmentA stochastic environment.
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]
Actions: Source Β· Open Issue
stepKernelπ
Learning.stepKernel
Kernel describing the distribution of the next action-feedback pair given the history
up to 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) β π Γ π¨) (π Γ π¨)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 IsMarkovKernelType uses (2)
Actions: Source Β· Open Issue