LeanMachineLearning

3.5.Β SequentialLearning.BayesStationaryEnvπŸ”—

Bayesian stationary environments

This file defines the structure IsBayesAlgEnvSeq and provides its basic properties.

Main definitions

  • IsBayesAlgEnvSeq Q ΞΊ alg E A Y P: states that there is a measure P : Measure Ξ© such that the parameter E : Ξ© β†’ 𝓔 has law Q and that the sequences of actions A : β„• β†’ Ξ© β†’ 𝓐 and feedbacks Y : β„• β†’ Ξ© β†’ 𝓨 are generated by the algorithm alg : Algorithm 𝓐 𝓨 interacting with an underlying environment that depends on E and ΞΊ (stationaryEnv (ΞΊ.sectR (E Ο‰))).

  • bayesTrajMeasure Q ΞΊ alg: for any choice of probability measure Q : Measure 𝓔, Markov kernel ΞΊ : Kernel (𝓔 Γ— 𝓐) 𝓨, and algorithm alg : Algorithm 𝓐 𝓨, provides a probability measure P : Measure (β„• β†’ 𝓐 Γ— 𝓔 Γ— 𝓨) on a space that carries E, A, and Y such that IsBayesAlgEnvSeq Q ΞΊ alg E A Y P.

  • bayesTrajMeasurePosterior Q ΞΊ alg n: a Kernel (Iic n β†’ 𝓐 Γ— 𝓨) 𝓔 that represents the posterior over E given the history up to time n under the prior Q and the algorithm alg, assuming that the kernel ΞΊ specifies how E gives rise to the underlying (stationary) environment. See also LeanMachineLearning/SequentialLearning/AlgorithmDensityBayes.lean.

Main results

  • ae_IsAlgEnvSeq h: if h : IsBayesAlgEnvSeq Q ΞΊ alg E A Y P, for Q-almost every e : 𝓔, IsAlgEnvSeq A' Y' alg (stationaryEnv (ΞΊ.sectR e)) (condDistrib (trajectory A Y) E P e) for some sequence of actions A' : β„• β†’ (β„• β†’ 𝓐 Γ— 𝓨) β†’ 𝓐 and sequence of feedbacks Y' : β„• β†’ (β„• β†’ 𝓐 Γ— 𝓨) β†’ 𝓨. Intuitively, if the observable trajectory is generated by an underlying parameter e : 𝓔, the measure that carries the IsBayesAlgEnvSeq structure reveals a measure that carries an IsAlgEnvSeq structure under the environment stationaryEnv (ΞΊ.sectR e) and the same algorithm. This allows transferring results from the IsAlgEnvSeq structure to the IsBayesAlgEnvSeq structure.

Module LeanMachineLearning.SequentialLearning.BayesStationaryEnv contains 17 exposed declarations.