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 timenunderPis the law of the history at timenunderP₀with densityalg.density alg₀ n. Intuitively, the law of the history underalgcan be obtained from the law of the history underalg₀when they are interacting with underlying stationary environments drawn from the same distribution.hasCondDistrib_env_history h h₀ hc n: the conditional distribution ofEgiven the history at timenunderPis almost everywhere equal to the conditional distribution ofE₀given the history at timenunderP₀. 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 𝓔}
{κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨}
[ProbabilityTheory.IsMarkovKernel κ]
{Ω : Type u_4}
[MeasurableSpace Ω]
{E : Ω → 𝓔}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{alg : Algorithm 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{Ω₀ : Type u_5}
[MeasurableSpace Ω₀]
{E₀ : Ω₀ → 𝓔}
{A₀ : ℕ → Ω₀ → 𝓐}
{Y₀ : ℕ → Ω₀ → 𝓨}
{alg₀ : Algorithm 𝓐 𝓨}
{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.hasLaw_history_withDensity
{𝓐 : Type u_1}
{𝓨 : Type u_2}
[MeasurableSpace 𝓐]
[MeasurableSpace 𝓨]
{𝓔 : Type u_3}
[MeasurableSpace 𝓔]
[StandardBorelSpace 𝓐]
[Nonempty 𝓐]
[StandardBorelSpace 𝓨]
[Nonempty 𝓨]
{Q : MeasureTheory.Measure 𝓔}
{κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨}
[ProbabilityTheory.IsMarkovKernel κ]
{Ω : Type u_4}
[MeasurableSpace Ω]
{E : Ω → 𝓔}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{alg : Algorithm 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{Ω₀ : Type u_5}
[MeasurableSpace Ω₀]
{E₀ : Ω₀ → 𝓔}
{A₀ : ℕ → Ω₀ → 𝓐}
{Y₀ : ℕ → Ω₀ → 𝓨}
{alg₀ : Algorithm 𝓐 𝓨}
{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 : ℕ)
:
ProbabilityTheory.HasLaw (history A Y n)
((MeasureTheory.Measure.map (history A₀ Y₀ n) P₀).withDensity (alg.density alg₀ n)) P
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 𝓔}
{κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨}
[ProbabilityTheory.IsMarkovKernel κ]
{Ω : Type u_4}
[MeasurableSpace Ω]
{E : Ω → 𝓔}
{A : ℕ → Ω → 𝓐}
{Y : ℕ → Ω → 𝓨}
{alg : Algorithm 𝓐 𝓨}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{Ω₀ : Type u_5}
[MeasurableSpace Ω₀]
{E₀ : Ω₀ → 𝓔}
{A₀ : ℕ → Ω₀ → 𝓐}
{Y₀ : ℕ → Ω₀ → 𝓨}
{alg₀ : Algorithm 𝓐 𝓨}
{P₀ : MeasureTheory.Measure Ω₀}
[MeasureTheory.IsProbabilityMeasure P₀]
[StandardBorelSpace 𝓔]
[Nonempty 𝓔]
[MeasureTheory.IsProbabilityMeasure Q]
(h : IsBayesAlgEnvSeq Q κ alg E A Y P)
(h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀)
(hc : alg.AbsolutelyContinuous alg₀)
(n : ℕ)
: