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.

structure Learning.IsBayesAlgEnvSeq {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (Q : MeasureTheory.Measure 𝓔) (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) (alg : Algorithm 𝓐 𝓨) (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] :

Prop

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 ω))).

measurable_param : Measurable E
measurable_action (n : ℕ) : Measurable (A n)
measurable_feedback (n : ℕ) : Measurable (Y n)
hasLaw_env : ProbabilityTheory.HasLaw E Q P
hasCondDistrib_action_zero : ProbabilityTheory.HasCondDistrib (A 0) E (ProbabilityTheory.Kernel.const 𝓔 alg.p0) P
hasCondDistrib_feedback_zero : ProbabilityTheory.HasCondDistrib (Y 0) (fun (ω : Ω) => (E ω, A 0 ω)) κ P
hasCondDistrib_action (n : ℕ) : ProbabilityTheory.HasCondDistrib (A (n + 1)) (fun (ω : Ω) => (E ω, history A Y n ω)) (ProbabilityTheory.Kernel.prodMkLeft 𝓔 (alg.policy n)) P
hasCondDistrib_feedback (n : ℕ) : ProbabilityTheory.HasCondDistrib (Y (n + 1)) (fun (ω : Ω) => (history A Y n ω, E ω, A (n + 1) ω)) (ProbabilityTheory.Kernel.prodMkLeft (↥(Finset.Iic n) → 𝓐 × 𝓨) κ) P

Instances For