Learning.Ξ½0_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.
Ξ½0_stationaryEnvπ
Learning.Ξ½0_stationaryEnvNo docstring.
Learning.Ξ½0_stationaryEnv.{u_1, u_2} {π : Type u_1} {π¨ : Type u_2} {mπ : MeasurableSpace π} {mπ¨ : MeasurableSpace π¨} (Ξ½ : ProbabilityTheory.Kernel π π¨) [ProbabilityTheory.IsMarkovKernel Ξ½] : Environment.Ξ½0 (stationaryEnv Ξ½) = Ξ½Learning.Ξ½0_stationaryEnv.{u_1, u_2} {π : Type u_1} {π¨ : Type u_2} {mπ : MeasurableSpace π} {mπ¨ : MeasurableSpace π¨} (Ξ½ : ProbabilityTheory.Kernel π π¨) [ProbabilityTheory.IsMarkovKernel Ξ½] : Environment.Ξ½0 (stationaryEnv Ξ½) = Ξ½
Code
lemma Ξ½0_stationaryEnv (Ξ½ : Kernel π π¨) [IsMarkovKernel Ξ½] : (stationaryEnv Ξ½).Ξ½0 = Ξ½
Type uses (2)
Body uses (1)
Actions: Source Β· Open Issue
Proof
by simp [stationaryEnv]
Dependency graph
Type dependencies (2)
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
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