Bayesian stationary environments

A Bayesian stationary environment is an environment that draws a parameter e : 𝓔 from a prior Q before the first round and then behaves like the stationary environment stationaryEnv (κ.sectR e). Concretely, bayesStationaryEnv Q κ : Environment 𝓔 𝓐 𝓨 announces an observation e at every round and runs against alg.comapObs (fun _ ↦ ()), for an alg : Algorithm Unit 𝓐 𝓨, an algorithm that does not use the observation.

Main definitions

• bayesStationaryEnv Q κ: the environment that draws a parameter from Q before the first round, announces it as the observation of every round, and returns feedback κ (e, a) when the parameter is e and the action is a.
• IsBayesAlgEnvSeq Q κ alg E A Y P: states that the parameter E : Ω → 𝓔 has law Q and that the sequences of actions A : ℕ → Ω → 𝓐 and feedbacks Y : ℕ → Ω → 𝓨 are generated by the algorithm alg : Algorithm Unit 𝓐 𝓨 interacting with bayesStationaryEnv Q κ, which it sees through Algorithm.comapObs (fun _ ↦ ()). Equivalently, A and Y are generated by alg interacting with the stationary environment stationaryEnv (κ.sectR (E ω)).
• bayesTrajMeasure Q κ alg: for any choice of probability measure Q : Measure 𝓔, Markov kernel κ : Kernel (𝓔 × 𝓐) 𝓨, and algorithm alg : Algorithm Unit 𝓐 𝓨, provides a probability measure P : Measure (ℕ → Round 𝓔 𝓐 𝓨) on a space that carries E, A, and Y such that IsBayesAlgEnvSeq Q κ alg E A Y P.
• bayesTrajMeasurePosterior Q κ alg n: a Kernel (Hist Unit 𝓐 𝓨 n) 𝓔 that represents the posterior over E given the history before time n (the n first rounds) 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

• IsAlgEnvSeq.isBayesAlgEnvSeq: a run of alg.comapObs (fun _ ↦ ()) against bayesStationaryEnv Q κ is a Bayesian algorithm-environment sequence for the announced parameter.
• ae_IsAlgEnvSeq h: if h : IsBayesAlgEnvSeq Q κ alg E A Y P, for Q-almost every e : 𝓔, IsAlgEnvSeq O' A' Y' alg (stationaryEnv (κ.sectR e)) (condDistrib (trajectory _ A Y) E P e) for some sequence of actions A' : ℕ → (ℕ → Round Unit 𝓐 𝓨) → 𝓐 and sequence of feedbacks Y' : ℕ → (ℕ → Round Unit 𝓐 𝓨) → 𝓨. 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.

noncomputable def Learning.bayesStationaryEnv {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) [ProbabilityTheory.IsMarkovKernel κ] : Environment 𝓔 𝓐 𝓨

The environment that draws a parameter e : 𝓔 from Q before the first round, announces it as the observation of every round, and returns a feedback drawn from κ (e, a) when the action is a. The algorithm is meant to ignore the announced parameter, that is, to run through Algorithm.comapObs (fun _ ↦ ()).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Learning.obs_bayesStationaryEnv_zero {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] : (bayesStationaryEnv Q κ).obs 0 = ProbabilityTheory.Kernel.const (Hist 𝓔 𝓐 𝓨 0) Q

@[simp]

theorem Learning.obs_bayesStationaryEnv_succ {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) : (bayesStationaryEnv Q κ).obs (n + 1) = ProbabilityTheory.Kernel.deterministic (fun (h : Hist 𝓔 𝓐 𝓨 (n + 1)) => (h 0).obs) ⋯

@[simp]

theorem Learning.feedback_bayesStationaryEnv {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) : (bayesStationaryEnv Q κ).feedback n = κ.comap (fun (p : (Hist 𝓔 𝓐 𝓨 n × 𝓔) × 𝓐) => (p.1.2, p.2)) ⋯

@[simp]

theorem Learning.obs0_bayesStationaryEnv {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] : (bayesStationaryEnv Q κ).obs0 = Q

@[simp]

theorem Learning.ν0_bayesStationaryEnv {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] : (bayesStationaryEnv Q κ).ν0 = κ

def Learning.announceHist {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (e : 𝓔) {n : ℕ} (h : Hist Unit 𝓐 𝓨 n) : Hist 𝓔 𝓐 𝓨 n

Insert an announced parameter e as the observation of every round of an observable history.

Equations

• Learning.announceHist e h i = (e, (h i).action, (h i).feedback)

theorem Learning.measurable_announceHist {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] (n : ℕ) : Measurable fun (p : 𝓔 × Hist Unit 𝓐 𝓨 n) => announceHist p.1 p.2

def Learning.IsBayesAlgEnvSeq {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (alg : Algorithm Unit 𝓐 𝓨) (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure 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 Unit 𝓐 𝓨 interacting with an underlying environment that depends on E and κ (stationaryEnv (κ.sectR (E ω))).

This is IsAlgEnvSeq for the announcing environment bayesStationaryEnv Q κ and the algorithm alg.comapObs (fun _ ↦ ()) that ignores the announced parameter: the observation at every round is E ω.

Equations

• Learning.IsBayesAlgEnvSeq Q κ alg E A Y P = Learning.IsAlgEnvSeq (fun (x : ℕ) => E) A Y (alg.comapObs (fun (x : 𝓔) => ()) ⋯) (Learning.bayesStationaryEnv Q κ) P

theorem Learning.IsBayesAlgEnvSeq.isAlgEnvSeq {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : IsAlgEnvSeq (fun (x : ℕ) => E) A Y (alg.comapObs (fun (x : 𝓔) => ()) ⋯) (bayesStationaryEnv Q κ) P

A Bayesian algorithm-environment sequence is an algorithm-environment sequence for the announcing environment bayesStationaryEnv Q κ.

theorem Learning.IsBayesAlgEnvSeq.measurable_param {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : Measurable E

theorem Learning.IsBayesAlgEnvSeq.measurable_action {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : Measurable (A n)

theorem Learning.IsBayesAlgEnvSeq.measurable_feedback {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : Measurable (Y n)

theorem Learning.IsBayesAlgEnvSeq.hasLaw_env {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : ProbabilityTheory.HasLaw E Q P

The parameter has law Q.

theorem Learning.IsBayesAlgEnvSeq.hasCondDistrib_action {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (A n) (fun (ω : Ω) => (E ω, history (noObs Ω) A Y n ω, noObs Ω n ω)) (ProbabilityTheory.Kernel.prodMkLeft 𝓔 (alg.policy n)) P

The action at time n has the correct conditional distribution given the parameter and the history: it depends only on the history.

theorem Learning.IsBayesAlgEnvSeq.hasCondDistrib_feedback {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (Y n) (fun (ω : Ω) => ((history (noObs Ω) A Y n ω, noObs Ω n ω), E ω, A n ω)) (ProbabilityTheory.Kernel.prodMkLeft (Hist Unit 𝓐 𝓨 n × Unit) κ) P

The feedback at time n has the correct conditional distribution given the history, the parameter and the action at time n: it depends only on the parameter and the action.

theorem Learning.IsBayesAlgEnvSeq.hasCondDistrib_action' {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (A n) (fun (ω : Ω) => (history (noObs Ω) A Y n ω, noObs Ω n ω)) (alg.policy n) P

theorem Learning.IsBayesAlgEnvSeq.hasCondDistrib_feedback' {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (Y n) (fun (ω : Ω) => (E ω, A n ω)) κ P

theorem Learning.IsBayesAlgEnvSeq.hasLaw_action_zero {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : ProbabilityTheory.HasLaw (A 0) (alg.p0 ()) P

theorem Learning.IsBayesAlgEnvSeq.hasCondDistrib_action_zero {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : ProbabilityTheory.HasCondDistrib (A 0) E (ProbabilityTheory.Kernel.const 𝓔 (alg.p0 ())) P

The first action is independent of the parameter E, and has law alg.p0 ().

theorem Learning.IsBayesAlgEnvSeq.condDistrib_param_history_zero {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [StandardBorelSpace 𝓔] [Nonempty 𝓔] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : 𝓛[E | history (noObs Ω) A Y 0; P] = ProbabilityTheory.Kernel.const (Hist Unit 𝓐 𝓨 0) Q

The posterior over the parameter given the empty history is the prior.

theorem Learning.IsBayesAlgEnvSeq.hasCondDistrib_IT_obs {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (_h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : ∀ᵐ (e : 𝓔) ∂Q, ProbabilityTheory.HasCondDistrib (IT.obs n) (IT.hist n) (ProbabilityTheory.Kernel.const (Hist Unit 𝓐 𝓨 n) (MeasureTheory.Measure.dirac ())) (𝓛[trajectory (noObs Ω) A Y | E; P] e)

theorem Learning.IsBayesAlgEnvSeq.hasCondDistrib_IT_action {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : ∀ᵐ (e : 𝓔) ∂Q, ProbabilityTheory.HasCondDistrib (IT.action n) (fun (τ : ℕ → Round Unit 𝓐 𝓨) => (IT.hist n τ, IT.obs n τ)) (alg.policy n) (𝓛[trajectory (noObs Ω) A Y | E; P] e)

theorem Learning.IsBayesAlgEnvSeq.hasCondDistrib_IT_feedback {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : ∀ᵐ (e : 𝓔) ∂Q, ProbabilityTheory.HasCondDistrib (IT.feedback n) (fun (τ : ℕ → Round Unit 𝓐 𝓨) => ((IT.hist n τ, IT.obs n τ), IT.action n τ)) (ProbabilityTheory.Kernel.prodMkLeft (Hist Unit 𝓐 𝓨 n × Unit) (κ.sectR e)) (𝓛[trajectory (noObs Ω) A Y | E; P] e)

theorem Learning.IsBayesAlgEnvSeq.hasLaw_IT_hist {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) : ∀ᵐ (e : 𝓔) ∂Q, ProbabilityTheory.HasLaw (IT.hist n) (𝓛[history (noObs Ω) A Y n | E; P] e) (𝓛[trajectory (noObs Ω) A Y | E; P] e)

theorem Learning.IsBayesAlgEnvSeq.ae_IsAlgEnvSeq {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) : ∀ᵐ (e : 𝓔) ∂Q, IsAlgEnvSeq IT.obs IT.action IT.feedback alg (stationaryEnv (κ.sectR e)) (𝓛[trajectory (noObs Ω) A Y | E; P] e)

theorem Learning.IsAlgEnvSeq.ae_obs_eq_obs_zero {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {O : ℕ → Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] [StandardBorelSpace 𝓔] (h : IsAlgEnvSeq O A Y (alg.comapObs (fun (x : 𝓔) => ()) ⋯) (bayesStationaryEnv Q κ) P) (n : ℕ) : O 0 =ᵐ[P] O n

Under bayesStationaryEnv Q κ, the announced parameter is almost surely the same at every round.

theorem Learning.IsAlgEnvSeq.isBayesAlgEnvSeq {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔} [MeasureTheory.IsProbabilityMeasure Q] {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} [ProbabilityTheory.IsMarkovKernel κ] {alg : Algorithm Unit 𝓐 𝓨} {O : ℕ → Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] [StandardBorelSpace 𝓔] (h : IsAlgEnvSeq O A Y (alg.comapObs (fun (x : 𝓔) => ()) ⋯) (bayesStationaryEnv Q κ) P) : IsBayesAlgEnvSeq Q κ alg (O 0) A Y P

A run of alg.comapObs (fun _ ↦ ()) against the announcing environment bayesStationaryEnv Q κ is a Bayesian algorithm-environment sequence for the announced parameter.

noncomputable def Learning.IT.bayesTrajMeasure {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (alg : Algorithm Unit 𝓐 𝓨) : MeasureTheory.Measure (ℕ → Round 𝓔 𝓐 𝓨)

A measure P on a measurable space that carries random variables E, A, and Y such that IsBayesAlgEnvSeq Q κ alg E A Y P. The parameter is the observation of the first round, IT.obs 0.

Equations

• Learning.IT.bayesTrajMeasure Q κ alg = Learning.trajMeasure (alg.comapObs (fun (x : 𝓔) => ()) ⋯) (Learning.bayesStationaryEnv Q κ)

instance Learning.IT.instIsProbabilityMeasureForallNatRoundBayesTrajMeasure {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (alg : Algorithm Unit 𝓐 𝓨) : MeasureTheory.IsProbabilityMeasure (bayesTrajMeasure Q κ alg)

theorem Learning.IT.isBayesAlgEnvSeq_bayesTrajMeasure {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [StandardBorelSpace 𝓔] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (alg : Algorithm Unit 𝓐 𝓨) : IsBayesAlgEnvSeq Q κ alg (obs 0) action feedback (bayesTrajMeasure Q κ alg)

noncomputable def Learning.IT.bayesTrajMeasurePosterior {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [StandardBorelSpace 𝓔] [Nonempty 𝓔] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (alg : Algorithm Unit 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.Kernel (Hist Unit 𝓐 𝓨 n) 𝓔

A kernel that represents the posterior over E given the history before time n.

Equations

• One or more equations did not get rendered due to their size.

instance Learning.IT.instIsMarkovKernelHistUnitBayesTrajMeasurePosterior {𝓔 : Type u_3} {𝓐 : Type u_1} {𝓨 : Type u_2} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [StandardBorelSpace 𝓔] [Nonempty 𝓔] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (alg : Algorithm Unit 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (bayesTrajMeasurePosterior Q κ alg n)

theorem Learning.IT.bayesTrajMeasurePosterior_zero {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] [StandardBorelSpace 𝓔] [Nonempty 𝓔] (Q : MeasureTheory.Measure 𝓔) [MeasureTheory.IsProbabilityMeasure Q] (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨) [ProbabilityTheory.IsMarkovKernel κ] (alg : Algorithm Unit 𝓐 𝓨) : bayesTrajMeasurePosterior Q κ alg 0 = ProbabilityTheory.Kernel.const (Hist Unit 𝓐 𝓨 0) Q

The posterior given the empty history is the prior.