Learning.stationaryEnv
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.
stationaryEnvπ
Learning.stationaryEnvA stationary environment, in which the distribution of the next feedback depends only on the last action.
Learning.stationaryEnv.{u_1, u_2} {π : Type u_1} {π¨ : Type u_2} {mπ : MeasurableSpace π} {mπ¨ : MeasurableSpace π¨} (Ξ½ : ProbabilityTheory.Kernel π π¨) [ProbabilityTheory.IsMarkovKernel Ξ½] : Environment π π¨Learning.stationaryEnv.{u_1, u_2} {π : Type u_1} {π¨ : Type u_2} {mπ : MeasurableSpace π} {mπ¨ : MeasurableSpace π¨} (Ξ½ : ProbabilityTheory.Kernel π π¨) [ProbabilityTheory.IsMarkovKernel Ξ½] : Environment π π¨
Code
def stationaryEnv (Ξ½ : Kernel π π¨) [IsMarkovKernel Ξ½] : Environment π π¨ := obliviousEnv fun _ β¦ Ξ½
Type uses (1)
Body uses (1)
Used by (81)
Actions: Source Β· Open Issue
Dependency graph
Type dependencies (1)
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
All dependencies, transitively (1)
obliviousEnvπ
Learning.obliviousEnvAn oblivious environment, in which the distribution of the next feedback depends only on the last action, but in a possibly time-dependent manner.
Learning.obliviousEnv.{u_1, u_2} {π : Type u_1} {π¨ : Type u_2} {mπ : MeasurableSpace π} {mπ¨ : MeasurableSpace π¨} (Ξ½ : β β ProbabilityTheory.Kernel π π¨) [β (n : β), ProbabilityTheory.IsMarkovKernel (Ξ½ n)] : Environment π π¨Learning.obliviousEnv.{u_1, u_2} {π : Type u_1} {π¨ : Type u_2} {mπ : MeasurableSpace π} {mπ¨ : MeasurableSpace π¨} (Ξ½ : β β ProbabilityTheory.Kernel π π¨) [β (n : β), ProbabilityTheory.IsMarkovKernel (Ξ½ n)] : Environment π π¨
Code
def obliviousEnv (Ξ½ : β β Kernel π π¨) [β n, IsMarkovKernel (Ξ½ n)] : Environment π π¨ where feedback n := (Ξ½ (n + 1)).prodMkLeft _ Ξ½0 := Ξ½ 0
Type uses (1)
Used by (10)
Actions: Source Β· Open Issue