LeanMachineLearning exposition

3.8. SequentialLearning.AlgorithmDensityBayes🔗

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.

Module LeanMachineLearning.SequentialLearning.AlgorithmDensityBayes contains 3 exposed declarations.

condDistrib_history_eq_condDistrib_hist_withDensity🔗

LemmaLearning.IsBayesAlgEnvSeq.condDistrib_history_eq_condDistrib_hist_withDensity
Details

No docstring.

🔗theorem
Learning.IsBayesAlgEnvSeq.condDistrib_history_eq_condDistrib_hist_withDensity.{u_1,
    u_2, u_3, u_4, u_5}
  {𝓐 : 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 : Algorithm.AbsolutelyContinuous alg alg₀) (n : ℕ) :
  ⇑𝓛[history A Y n | E; P] =ᵐ[Q]
    ⇑(ProbabilityTheory.Kernel.withDensity 𝓛[history A₀ Y₀ n | E₀; P₀]
        fun x => Algorithm.density alg alg₀ n)
Learning.IsBayesAlgEnvSeq.condDistrib_history_eq_condDistrib_hist_withDensity.{u_1,
    u_2, u_3, u_4, u_5}
  {𝓐 : 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 :
    Algorithm.AbsolutelyContinuous alg
      alg₀)
  (n : ℕ) :
  ⇑𝓛[history A Y n | E; P] =ᵐ[Q]
    ⇑(ProbabilityTheory.Kernel.withDensity
        𝓛[history A₀ Y₀ n | E₀; P₀]
        fun x =>
        Algorithm.density alg alg₀ n)

Code

lemma condDistrib_history_eq_condDistrib_hist_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
    (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
    condDistrib (history A Y n) E P =ᵐ[Q]
      ((condDistrib (history A₀ Y₀ n) E₀ P₀).withDensity
        (fun _ ↦ alg.density alg₀ n))
Type uses (5)
Body uses (10)
Used by (2)

Actions: Source · Open Issue

Proof
by
    filter_upwards [h.ae_IsAlgEnvSeq, h₀.ae_IsAlgEnvSeq, h.hasLaw_IT_hist n, h₀.hasLaw_IT_hist n]
      with _ hae hae₀ he he₀
    rw [Kernel.withDensity_apply _ (by fun_prop), ← he.map_eq, ← he₀.map_eq]
    exact (hae.hasLaw_history_withDensity hae₀ hc n).map_eq

hasLaw_history_withDensity🔗

LemmaLearning.IsBayesAlgEnvSeq.hasLaw_history_withDensity
Details

No docstring.

🔗theorem
Learning.IsBayesAlgEnvSeq.hasLaw_history_withDensity.{u_1, u_2, u_3,
    u_4, u_5}
  {𝓐 : 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 : Algorithm.AbsolutelyContinuous alg alg₀) (n : ℕ) :
  ProbabilityTheory.HasLaw (history A Y n)
    (MeasureTheory.Measure.withDensity
      (MeasureTheory.Measure.map (history A₀ Y₀ n) P₀)
      (Algorithm.density alg alg₀ n))
    P
Learning.IsBayesAlgEnvSeq.hasLaw_history_withDensity.{u_1,
    u_2, u_3, u_4, u_5}
  {𝓐 : 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 :
    Algorithm.AbsolutelyContinuous alg
      alg₀)
  (n : ℕ) :
  ProbabilityTheory.HasLaw (history A Y n)
    (MeasureTheory.Measure.withDensity
      (MeasureTheory.Measure.map
        (history A₀ Y₀ n) P₀)
      (Algorithm.density alg alg₀ n))
    P

Code

lemma hasLaw_history_withDensity (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
    (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
    HasLaw (history A Y n)
      ((P₀.map (history A₀ Y₀ n)).withDensity (alg.density alg₀ n)) P where
  aemeasurable
Type uses (5)
Body uses (4)
Used by (1)

Actions: Source · Open Issue

Proof
(measurable_history h.measurable_action h.measurable_feedback n).aemeasurable
  map_eq := by
    have hA := h.measurable_action
    have hY := h.measurable_feedback
    have hA₀ := h₀.measurable_action
    have hY₀ := h₀.measurable_feedback
    have hE := h.measurable_param
    have hE₀ := h₀.measurable_param
    rw [← condDistrib_comp_map hE.aemeasurable (by fun_prop), h.hasLaw_env.map_eq,
          Measure.bind_congr_right (h.condDistrib_history_eq_condDistrib_hist_withDensity h₀ hc n),
          Kernel.comp_withDensity_eq_withDensity_comp (by fun_prop),
          ← h₀.hasLaw_env.map_eq, condDistrib_comp_map hE₀.aemeasurable (by fun_prop)]

hasCondDistrib_env_history🔗

LemmaLearning.IsBayesAlgEnvSeq.hasCondDistrib_env_history
Details

No docstring.

🔗theorem
Learning.IsBayesAlgEnvSeq.hasCondDistrib_env_history.{u_1, u_2, u_3,
    u_4, u_5}
  {𝓐 : 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 : Algorithm.AbsolutelyContinuous alg alg₀) (n : ℕ) :
  ProbabilityTheory.HasCondDistrib E (history A Y n)
    𝓛[E₀ | history A₀ Y₀ n; P₀] P
Learning.IsBayesAlgEnvSeq.hasCondDistrib_env_history.{u_1,
    u_2, u_3, u_4, u_5}
  {𝓐 : 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 :
    Algorithm.AbsolutelyContinuous alg
      alg₀)
  (n : ℕ) :
  ProbabilityTheory.HasCondDistrib E
    (history A Y n)
    𝓛[E₀ | history A₀ Y₀ n; P₀] P

Code

lemma hasCondDistrib_env_history (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
    (h₀ : IsBayesAlgEnvSeq Q κ alg₀ E₀ A₀ Y₀ P₀) (hc : alg ≪ₐ alg₀) (n : ℕ) :
    HasCondDistrib E (history A Y n) (condDistrib E₀ (history A₀ Y₀ n) P₀) P where
  aemeasurable
Type uses (4)
Body uses (9)
Used by (1)

Actions: Source · Open Issue

Proof
((measurable_history h.measurable_action
    h.measurable_feedback n).prodMk h.measurable_param).aemeasurable
  map_eq := by
    have hA := h.measurable_action
    have hY := h.measurable_feedback
    have hA₀ := h₀.measurable_action
    have hY₀ := h₀.measurable_feedback
    have hE₀ := h₀.measurable_param
    rw [← map_swap_compProd_map_condDistrib (by fun_prop), h.hasLaw_env.map_eq,
      Measure.compProd_eq_compProd_withDensity_comp_snd (by fun_prop)
        (h.condDistrib_history_eq_condDistrib_hist_withDensity h₀ hc n),
      map_swap_withDensity_comp_snd (by fun_prop),
      ← h₀.hasLaw_env.map_eq, map_swap_compProd_map_condDistrib (by fun_prop),
      ← compProd_map_condDistrib (by fun_prop), ← Measure.compProd_withDensity_left (by fun_prop),
      ← (hasLaw_history_withDensity h h₀ hc n).map_eq]
  1. Learning.IsBayesAlgEnvSeq.condDistrib_history_eq_condDistrib_hist_withDensity
  2. Learning.IsBayesAlgEnvSeq.hasLaw_history_withDensity
  3. Learning.IsBayesAlgEnvSeq.hasCondDistrib_env_history