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 (Fin n → 𝓐 × 𝓨) 𝓔 that represents the posterior over E given the history before time n (the n first action-feedback pairs) 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 21 exposed declarations.