Algorithm density under Bayesian stationary environments #

This file provides results about Algorithm.density for the Bayesian stationary environment setting.

Main results #

Let h : IsBayesAlgEnvSeq Q κ alg E A Y P, h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀, and hc : alg ≪ₐ alg₀.

hasLaw_hist_withDensity h h₀ hc n: the law of the history at time n under P is the law of the history at time n under P₀ with density alg.density alg₀ n. Intuitively, the law of the history under alg can be obtained from the law of the history under alg₀ when they are interacting with underlying stationary environments drawn from the same distribution.
hasCondDistrib_env_history h h₀ hc n: the conditional distribution of E given the history at time n under P is almost everywhere equal to the conditional distribution of E₀ given the history at time n under P₀. Intuitively, the posterior is independent of the algorithm used to observe the history.

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

⇑𝓛[history (noObs Ω) A Y n | E; P] =ᵐ[Q] ⇑(𝓛[history (noObs Ω₀) A₀ Y₀ n | E₀; P₀].withDensity fun (x : 𝓔) => alg.density alg₀ n)

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

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