3.4. SequentialLearning.BayesStationaryEnv🔗

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.

Module LeanMachineLearning.SequentialLearning.BayesStationaryEnv contains 17 exposed declarations.

`IsBayesAlgEnvSeq`🔗

StructureLearning.IsBayesAlgEnvSeq

Details

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

structure

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

Code

structure IsBayesAlgEnvSeq
    (Q : Measure 𝓔) (κ : Kernel (𝓔 × 𝓐) 𝓨) (alg : Algorithm 𝓐 𝓨)
    (E : Ω → 𝓔) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨)
    (P : Measure Ω) [IsFiniteMeasure P] : Prop where
  measurable_param : Measurable E := by fun_prop
  measurable_action n : Measurable (A n) := by fun_prop
  measurable_feedback n : Measurable (Y n) := by fun_prop
  hasLaw_env : HasLaw E Q P
  hasCondDistrib_action_zero : HasCondDistrib (A 0) E (Kernel.const _ alg.p0) P
  hasCondDistrib_feedback_zero : HasCondDistrib (Y 0) (fun ω ↦ (E ω, A 0 ω)) κ P
  hasCondDistrib_action n :
    HasCondDistrib (A (n + 1)) (fun ω ↦ (E ω, history A Y n ω))
      ((alg.policy n).prodMkLeft _) P
  hasCondDistrib_feedback n :
    HasCondDistrib (Y (n + 1)) (fun ω ↦ (history A Y n ω, E ω, A (n + 1) ω))
      (κ.prodMkLeft _) P

Type uses (2)

Used by (22)

Actions: Source · Open Issue

`hasLaw_action_zero`🔗

LemmaLearning.IsBayesAlgEnvSeq.hasLaw_action_zero

Details

No docstring.

theorem

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

Code

lemma hasLaw_action_zero [IsProbabilityMeasure P] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
    HasLaw (A 0) alg.p0 P

Type uses (2)

Body uses (1)

instIsProbabilityMeasureP0

Actions: Source · Open Issue

Proof

h.hasCondDistrib_action_zero.hasLaw_of_const

`hasCondDistrib_action'`🔗

LemmaLearning.IsBayesAlgEnvSeq.hasCondDistrib_action'

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.hasCondDistrib_action'.{u_1, u_2, u_3, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} {alg : Algorithm 𝓐 𝓨}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P]
  (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
  ProbabilityTheory.HasCondDistrib (A (n + 1)) (history A Y n)
    (Algorithm.policy alg n) P
Learning.IsBayesAlgEnvSeq.hasCondDistrib_action'.{u_1,
    u_2, u_3, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] [MeasurableSpace Ω]
  {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨}
  {alg : Algorithm 𝓐 𝓨} {E : Ω → 𝓔}
  {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P]
  (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
  (n : ℕ) :
  ProbabilityTheory.HasCondDistrib
    (A (n + 1)) (history A Y n)
    (Algorithm.policy alg n) P

Code

lemma hasCondDistrib_action' (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
    HasCondDistrib (A (n + 1)) (history A Y n) (alg.policy n) P

Type uses (3)

Body uses (1)

instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy

Used by (1)

hasCondDistrib_action

Actions: Source · Open Issue

Proof

(h.hasCondDistrib_action n).comp_right

`hasCondDistrib_feedback'`🔗

LemmaLearning.IsBayesAlgEnvSeq.hasCondDistrib_feedback'

Details

No docstring.

theorem

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

Code

lemma hasCondDistrib_feedback' [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
    HasCondDistrib (Y (n + 1)) (fun ω ↦ (E ω, A (n + 1) ω)) κ P

Type uses (2)

Body uses (1)

history

Actions: Source · Open Issue

Proof

(h.hasCondDistrib_feedback n).comp_right

`hasLaw_IT_action_zero`🔗

LemmaLearning.IsBayesAlgEnvSeq.hasLaw_IT_action_zero

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.hasLaw_IT_action_zero.{u_1, u_2, u_3, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} {alg : Algorithm 𝓐 𝓨}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P]
  [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨]
  [Nonempty 𝓨] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
  ∀ᵐ (e : 𝓔) ∂Q,
    ProbabilityTheory.HasLaw (IT.action 0) (Algorithm.p0 alg)
      (𝓛[trajectory A Y | E; P] e)
Learning.IsBayesAlgEnvSeq.hasLaw_IT_action_zero.{u_1,
    u_2, u_3, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] [MeasurableSpace Ω]
  {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨}
  {alg : Algorithm 𝓐 𝓨} {E : Ω → 𝓔}
  {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P]
  [StandardBorelSpace 𝓐] [Nonempty 𝓐]
  [StandardBorelSpace 𝓨] [Nonempty 𝓨]
  (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
  ∀ᵐ (e : 𝓔) ∂Q,
    ProbabilityTheory.HasLaw (IT.action 0)
      (Algorithm.p0 alg)
      (𝓛[trajectory A Y | E; P] e)

Code

lemma hasLaw_IT_action_zero (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
    ∀ᵐ e ∂Q, HasLaw (IT.action 0) alg.p0 (condDistrib (trajectory A Y) E P e)

Type uses (4)

Body uses (4)

Used by (1)

ae_IsAlgEnvSeq

Actions: Source · Open Issue

Proof

by
  rw [← h.hasLaw_env.map_eq]
  filter_upwards [condDistrib_comp E
      ((measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable)
      (IT.measurable_action (𝓐 := 𝓐) (𝓨 := 𝓨) 0),
    h.hasCondDistrib_action_zero.condDistrib_eq] with _ hc hcd
  exact ⟨(IT.measurable_action 0).aemeasurable, by
    rw [← Kernel.map_apply _ (IT.measurable_action 0), ← hc,
      show IT.action 0 ∘ trajectory A Y = A 0 from rfl, hcd, Kernel.const_apply]⟩

`hasCondDistrib_IT_feedback_zero`🔗

LemmaLearning.IsBayesAlgEnvSeq.hasCondDistrib_IT_feedback_zero

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.hasCondDistrib_IT_feedback_zero.{u_1, u_2,
    u_3, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} {alg : Algorithm 𝓐 𝓨}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P]
  [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨]
  [Nonempty 𝓨] [ProbabilityTheory.IsFiniteKernel κ]
  (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
  ∀ᵐ (e : 𝓔) ∂Q,
    ProbabilityTheory.HasCondDistrib (IT.feedback 0) (IT.action 0)
      (ProbabilityTheory.Kernel.sectR κ e) (𝓛[trajectory A Y | E; P] e)
Learning.IsBayesAlgEnvSeq.hasCondDistrib_IT_feedback_zero.{u_1,
    u_2, u_3, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] [MeasurableSpace Ω]
  {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨}
  {alg : Algorithm 𝓐 𝓨} {E : Ω → 𝓔}
  {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P]
  [StandardBorelSpace 𝓐] [Nonempty 𝓐]
  [StandardBorelSpace 𝓨] [Nonempty 𝓨]
  [ProbabilityTheory.IsFiniteKernel κ]
  (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
  ∀ᵐ (e : 𝓔) ∂Q,
    ProbabilityTheory.HasCondDistrib
      (IT.feedback 0) (IT.action 0)
      (ProbabilityTheory.Kernel.sectR κ e)
      (𝓛[trajectory A Y | E; P] e)

Code

lemma hasCondDistrib_IT_feedback_zero [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
    ∀ᵐ e ∂Q, HasCondDistrib (IT.feedback 0) (IT.action 0) (κ.sectR e)
      (condDistrib (trajectory A Y) E P e)

Type uses (5)

Body uses (4)

Used by (1)

ae_IsAlgEnvSeq

Actions: Source · Open Issue

Proof

by
  rw [← h.hasLaw_env.map_eq]
  exact h.hasCondDistrib_feedback_zero.hasCondDistrib_sectR
    (IT.measurable_action 0) (IT.measurable_feedback 0)
    (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable

`hasCondDistrib_IT_action`🔗

LemmaLearning.IsBayesAlgEnvSeq.hasCondDistrib_IT_action

Details

No docstring.

theorem

Learning.IsBayesAlgEnvSeq.hasCondDistrib_IT_action.{u_1, u_2, u_3, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  [MeasurableSpace Ω] {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨} {alg : Algorithm 𝓐 𝓨}
  {E : Ω → 𝓔} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P]
  [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨]
  [Nonempty 𝓨] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
  ∀ᵐ (e : 𝓔) ∂Q,
    ProbabilityTheory.HasCondDistrib (IT.action (n + 1)) (IT.hist n)
      (Algorithm.policy alg n) (𝓛[trajectory A Y | E; P] e)
Learning.IsBayesAlgEnvSeq.hasCondDistrib_IT_action.{u_1,
    u_2, u_3, u_4}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} {Ω : Type u_4}
  [MeasurableSpace 𝓔] [MeasurableSpace 𝓐]
  [MeasurableSpace 𝓨] [MeasurableSpace Ω]
  {Q : MeasureTheory.Measure 𝓔}
  {κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨}
  {alg : Algorithm 𝓐 𝓨} {E : Ω → 𝓔}
  {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure P]
  [StandardBorelSpace 𝓐] [Nonempty 𝓐]
  [StandardBorelSpace 𝓨] [Nonempty 𝓨]
  (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
  (n : ℕ) :
  ∀ᵐ (e : 𝓔) ∂Q,
    ProbabilityTheory.HasCondDistrib
      (IT.action (n + 1)) (IT.hist n)
      (Algorithm.policy alg n)
      (𝓛[trajectory A Y | E; P] e)

Code

lemma hasCondDistrib_IT_action (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
    ∀ᵐ e ∂Q, HasCondDistrib (IT.action (n + 1)) (IT.hist n) (alg.policy n)
      (condDistrib (trajectory A Y) E P e)

Type uses (5)

Body uses (6)

Used by (1)

ae_IsAlgEnvSeq

Actions: Source · Open Issue

Proof

by
  rw [← h.hasLaw_env.map_eq]
  filter_upwards [(h.hasCondDistrib_action n).hasCondDistrib_sectR
    (IT.measurable_hist n) (IT.measurable_action (n + 1))
    (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable] with _ he
  rwa [Kernel.sectR_prodMkLeft] at he

`hasCondDistrib_IT_feedback`🔗

LemmaLearning.IsBayesAlgEnvSeq.hasCondDistrib_IT_feedback

Details

No docstring.

theorem

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

Code

lemma hasCondDistrib_IT_feedback [IsFiniteKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P)
    (n : ℕ) :
    ∀ᵐ e ∂Q, HasCondDistrib (IT.feedback (n + 1)) (fun τ ↦ (IT.hist n τ, IT.action (n + 1) τ))
      ((κ.sectR e).prodMkLeft _) (condDistrib (trajectory A Y) E P e)

Type uses (6)

Body uses (6)

Used by (1)

ae_IsAlgEnvSeq

Actions: Source · Open Issue

Proof

by
  rw [← h.hasLaw_env.map_eq]
  have hc : HasCondDistrib (Y (n + 1))
      (fun ω ↦ (E ω, history A Y n ω, A (n + 1) ω))
      (κ.comap (fun (e, _, a) ↦ (e, a)) (by fun_prop)) P :=
    (h.hasCondDistrib_feedback n).measurableEquiv_comp_right (MeasurableEquiv.prodAssoc.symm.trans
      ((MeasurableEquiv.prodCongr .prodComm (.refl _)).trans .prodAssoc))
  exact hc.hasCondDistrib_sectR ((IT.measurable_hist n).prodMk
    (IT.measurable_action (n + 1))) (IT.measurable_feedback (n + 1))
    (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable

`hasLaw_IT_hist`🔗

LemmaLearning.IsBayesAlgEnvSeq.hasLaw_IT_hist

Details

No docstring.

theorem

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

Code

lemma hasLaw_IT_hist (h : IsBayesAlgEnvSeq Q κ alg E A Y P) (n : ℕ) :
    ∀ᵐ e ∂Q, HasLaw (IT.hist n) (condDistrib (history A Y n) E P e)
      (condDistrib (trajectory A Y) E P e)

Type uses (5)

Body uses (2)

Used by (1)

condDistrib_history_eq_condDistrib_hist_withDensity

Actions: Source · Open Issue

Proof

by
  rw [← h.hasLaw_env.map_eq, show history A Y n = IT.hist n ∘ trajectory A Y from rfl]
  filter_upwards [condDistrib_comp E
    (measurable_trajectory h.measurable_action h.measurable_feedback).aemeasurable
    (IT.measurable_hist n)] with _ he
  exact ⟨(IT.measurable_hist n).aemeasurable, by
    rw [← Kernel.map_apply _ (IT.measurable_hist n), he]⟩

`ae_IsAlgEnvSeq`🔗

LemmaLearning.IsBayesAlgEnvSeq.ae_IsAlgEnvSeq

Details

No docstring.

theorem

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

Code

lemma ae_IsAlgEnvSeq [IsMarkovKernel κ] (h : IsBayesAlgEnvSeq Q κ alg E A Y P) :
    ∀ᵐ e ∂Q, IsAlgEnvSeq IT.action IT.feedback alg (stationaryEnv (κ.sectR e))
      (condDistrib (trajectory A Y) E P e)

Type uses (7)

Body uses (9)

Used by (3)

Actions: Source · Open Issue

Proof

by
  filter_upwards [hasLaw_IT_action_zero h, hasCondDistrib_IT_feedback_zero h,
    ae_all_iff.2 (hasCondDistrib_IT_action h), ae_all_iff.2 (hasCondDistrib_IT_feedback h)]
    with _ ha0 hr0 hA hR
  exact ⟨IT.measurable_action, IT.measurable_feedback, ha0, hr0, hA, hR⟩

`bayesStationaryEnv`🔗

DefinitionLearning.bayesStationaryEnv

Details

An environment with observations in 𝓔 × 𝓨. The first element e of an observation is sampled from Q once and remains constant. The second element of an observation is sampled from κ (e, a), where a is the corresponding action.

def

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

Code

noncomputable
def bayesStationaryEnv (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨)
    [IsMarkovKernel κ] : Environment 𝓐 (𝓔 × 𝓨) where
  feedback n :=
    let g : (Iic n → 𝓐 × 𝓔 × 𝓨) × 𝓐 → 𝓔 × 𝓐 := fun (h, a) => ((h ⟨0, by simp⟩).2.1, a)
    (Kernel.deterministic (Prod.fst ∘ g) (by fun_prop)) ×ₖ (κ.comap g (by fun_prop))
  ν0 := (Kernel.const _ Q) ⊗ₖ κ.swapLeft

Type uses (1)

Environment

Used by (4)

Actions: Source · Open Issue

`isBayesAlgEnvSeq`🔗

LemmaLearning.IsAlgEnvSeq.isBayesAlgEnvSeq

Details

No docstring.

theorem

Learning.IsAlgEnvSeq.isBayesAlgEnvSeq.{u_1, u_2, u_3, u_4}
  {𝓔 : 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 𝓐 𝓨}
  {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓔 × 𝓨} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  (h :
    IsAlgEnvSeq A Y (Algorithm.prodLeft 𝓔 alg) (bayesStationaryEnv Q κ)
      P) :
  IsBayesAlgEnvSeq Q κ alg (fun ω => Prod.fst (Y 0 ω)) A
    (fun n ω => Prod.snd (Y n ω)) P
Learning.IsAlgEnvSeq.isBayesAlgEnvSeq.{u_1,
    u_2, u_3, u_4}
  {𝓔 : 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 𝓐 𝓨} {A : ℕ → Ω → 𝓐}
  {Y : ℕ → Ω → 𝓔 × 𝓨}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  (h :
    IsAlgEnvSeq A Y
      (Algorithm.prodLeft 𝓔 alg)
      (bayesStationaryEnv Q κ) P) :
  IsBayesAlgEnvSeq Q κ alg
    (fun ω => Prod.fst (Y 0 ω)) A
    (fun n ω => Prod.snd (Y n ω)) P

Code

lemma IsAlgEnvSeq.isBayesAlgEnvSeq
    (h : IsAlgEnvSeq A Y (alg.prodLeft 𝓔) (bayesStationaryEnv Q κ) P) :
    IsBayesAlgEnvSeq Q κ alg (fun ω ↦ (Y 0 ω).1) A (fun n ω ↦ (Y n ω).2) P where
  measurable_param

Type uses (5)

Body uses (6)

Used by (1)

isBayesAlgEnvSeq_bayesTrajMeasure

Actions: Source · Open Issue

Proof

(h.measurable_feedback 0).fst
  measurable_action := h.measurable_action
  measurable_feedback n := (h.measurable_feedback n).snd
  hasLaw_env := by
    apply HasCondDistrib.hasLaw_of_const
    simpa [bayesStationaryEnv] using h.hasCondDistrib_feedback_zero.fst
  hasCondDistrib_action_zero := by
    have hc : HasCondDistrib (fun ω ↦ (Y 0 ω).1) (A 0) (Kernel.const _ Q) P := by
      simpa [bayesStationaryEnv] using h.hasCondDistrib_feedback_zero.fst
    simpa [h.hasLaw_action_zero.map_eq, Algorithm.prodLeft] using hc.const_map_of_const
  hasCondDistrib_feedback_zero :=
    h.hasCondDistrib_feedback_zero.of_compProd.measurableEquiv_comp_right MeasurableEquiv.prodComm
  hasCondDistrib_action n := by
    let f : (Iic n → 𝓐 × 𝓔 × 𝓨) → 𝓔 × (Iic n → 𝓐 × 𝓨) :=
      fun h ↦ ((h ⟨0, by simp⟩).2.1, fun i ↦ ((h i).1, (h i).2.2))
    have hc : HasCondDistrib (A (n + 1)) (history A Y n)
        (((alg.policy n).comap Prod.snd (by fun_prop)).comap f (by fun_prop)) P :=
      h.hasCondDistrib_action n
    exact hc.comp_right (f := f)
  hasCondDistrib_feedback n := by
    let f : (Iic n → 𝓐 × 𝓔 × 𝓨) × 𝓐 → (Iic n → 𝓐 × 𝓨) × 𝓔 × 𝓐 :=
      fun p ↦ ((fun i ↦ ((p.1 i).1, (p.1 i).2.2)), (p.1 ⟨0, by simp⟩).2.1, p.2)
    have hc : HasCondDistrib (fun ω ↦ (Y (n + 1) ω).2)
        (fun ω ↦ (history A Y n ω, A (n + 1) ω))
        ((Kernel.prodMkLeft ((Iic n) → 𝓐 × 𝓨) κ).comap f (by fun_prop)) P := by
      simpa [bayesStationaryEnv, Kernel.prodMkLeft, ← Kernel.comap_comp_right, Function.comp_def]
        using (h.hasCondDistrib_feedback n).snd
    exact hc.comp_right

`bayesTrajMeasure`🔗

DefinitionLearning.IT.bayesTrajMeasure

Details

A measure P on a measurable space that carries random variables E, A, and Y such that IsBayesAlgEnvSeq Q κ alg E A Y P.

def

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

Code

noncomputable
def bayesTrajMeasure (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨)
    [IsMarkovKernel κ] (alg : Algorithm 𝓐 𝓨) : Measure (ℕ → 𝓐 × 𝓔 × 𝓨) :=
  trajMeasure (alg.prodLeft 𝓔) (bayesStationaryEnv Q κ)
deriving IsProbabilityMeasure

Type uses (1)

Algorithm

Body uses (3)

Used by (5)

Actions: Source · Open Issue

`instIsProbabilityMeasureForallNatProdBayesTrajMeasure`🔗

InstanceLearning.IT.instIsProbabilityMeasureForallNatProdBayesTrajMeasure

Details

No docstring.

theorem

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

Code

deriving IsProbabilityMeasure

Type uses (2)

Body uses (3)

Used by (4)

Actions: Source · Open Issue

Proof

deriving IsProbabilityMeasure

`isBayesAlgEnvSeq_bayesTrajMeasure`🔗

LemmaLearning.IT.isBayesAlgEnvSeq_bayesTrajMeasure

Details

No docstring.

theorem

Learning.IT.isBayesAlgEnvSeq_bayesTrajMeasure.{u_1, u_2, u_3}
  {𝓔 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] (Q : MeasureTheory.Measure 𝓔)
  [MeasureTheory.IsProbabilityMeasure Q]
  (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨)
  [ProbabilityTheory.IsMarkovKernel κ] (alg : Algorithm 𝓐 𝓨) :
  IsBayesAlgEnvSeq Q κ alg (fun ω => Prod.fst (Prod.snd (ω 0))) action
    (fun n ω => Prod.snd (Prod.snd (ω n))) (bayesTrajMeasure Q κ alg)
Learning.IT.isBayesAlgEnvSeq_bayesTrajMeasure.{u_1,
    u_2, u_3}
  {𝓔 : Type u_1} {𝓐 : Type u_2}
  {𝓨 : Type u_3} [MeasurableSpace 𝓔]
  [MeasurableSpace 𝓐] [MeasurableSpace 𝓨]
  (Q : MeasureTheory.Measure 𝓔)
  [MeasureTheory.IsProbabilityMeasure Q]
  (κ : ProbabilityTheory.Kernel (𝓔 × 𝓐) 𝓨)
  [ProbabilityTheory.IsMarkovKernel κ]
  (alg : Algorithm 𝓐 𝓨) :
  IsBayesAlgEnvSeq Q κ alg
    (fun ω => Prod.fst (Prod.snd (ω 0)))
    action
    (fun n ω => Prod.snd (Prod.snd (ω n)))
    (bayesTrajMeasure Q κ alg)

Code

lemma isBayesAlgEnvSeq_bayesTrajMeasure
    (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨) [IsMarkovKernel κ]
    (alg : Algorithm 𝓐 𝓨) :
    IsBayesAlgEnvSeq Q κ alg (fun ω ↦ (ω 0).2.1) action (fun n ω ↦ (ω n).2.2)
       (bayesTrajMeasure Q κ alg)

Type uses (5)

Body uses (7)

Used by (1)

hasCondDistrib_action

Actions: Source · Open Issue

Proof

(isAlgEnvSeq_trajMeasure _ _).isBayesAlgEnvSeq

`bayesTrajMeasurePosterior`🔗

DefinitionLearning.IT.bayesTrajMeasurePosterior

Details

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

def

Learning.IT.bayesTrajMeasurePosterior.{u_1, u_2, u_3} {𝓔 : 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 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.Kernel (↥(Finset.Iic n) → 𝓐 × 𝓨) 𝓔
Learning.IT.bayesTrajMeasurePosterior.{u_1,
    u_2, u_3}
  {𝓔 : 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 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.Kernel
    (↥(Finset.Iic n) → 𝓐 × 𝓨) 𝓔

Code

noncomputable
def bayesTrajMeasurePosterior [StandardBorelSpace 𝓔] [Nonempty 𝓔]
    (Q : Measure 𝓔) [IsProbabilityMeasure Q] (κ : Kernel (𝓔 × 𝓐) 𝓨) [IsMarkovKernel κ]
    (alg : Algorithm 𝓐 𝓨) (n : ℕ) : Kernel (Iic n → 𝓐 × 𝓨) 𝓔 :=
  condDistrib (fun ω ↦ (ω 0).2.1) (history action (fun n ω ↦ (ω n).2.2) n)
    (bayesTrajMeasure Q κ alg)
deriving IsMarkovKernel

Type uses (1)

Algorithm

Body uses (4)

Used by (4)

Actions: Source · Open Issue

`instIsMarkovKernelForallSubtypeNatMemFinsetIicProdBayesTrajMeasurePosterior`🔗

InstanceLearning.IT.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdBayesTrajMeasurePosterior

Details

No docstring.

theorem

Learning.IT.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdBayesTrajMeasurePosterior.{u_1,
    u_2, u_3}
  {𝓔 : 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 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.IsMarkovKernel (bayesTrajMeasurePosterior Q κ alg n)
Learning.IT.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdBayesTrajMeasurePosterior.{u_1,
    u_2, u_3}
  {𝓔 : 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 𝓐 𝓨) (n : ℕ) :
  ProbabilityTheory.IsMarkovKernel
    (bayesTrajMeasurePosterior Q κ alg n)

Code

deriving IsMarkovKernel

Type uses (2)

Body uses (4)

Used by (1)

instIsMarkovKernelForallSubtypeNatMemFinsetIicProdFinRealPolicy

Actions: Source · Open Issue

Proof

deriving IsMarkovKernel

3.4. SequentialLearning.BayesStationaryEnv🔗

IsBayesAlgEnvSeq🔗

hasLaw_action_zero🔗

hasCondDistrib_action'🔗

hasCondDistrib_feedback'🔗

hasLaw_IT_action_zero🔗

hasCondDistrib_IT_feedback_zero🔗

hasCondDistrib_IT_action🔗

hasCondDistrib_IT_feedback🔗

hasLaw_IT_hist🔗

ae_IsAlgEnvSeq🔗

bayesStationaryEnv🔗

isBayesAlgEnvSeq🔗

bayesTrajMeasure🔗

instIsProbabilityMeasureForallNatProdBayesTrajMeasure🔗

isBayesAlgEnvSeq_bayesTrajMeasure🔗

bayesTrajMeasurePosterior🔗

instIsMarkovKernelForallSubtypeNatMemFinsetIicProdBayesTrajMeasurePosterior🔗

`IsBayesAlgEnvSeq`🔗

`hasLaw_action_zero`🔗

`hasCondDistrib_action'`🔗

`hasCondDistrib_feedback'`🔗

`hasLaw_IT_action_zero`🔗

`hasCondDistrib_IT_feedback_zero`🔗

`hasCondDistrib_IT_action`🔗

`hasCondDistrib_IT_feedback`🔗

`hasLaw_IT_hist`🔗

`ae_IsAlgEnvSeq`🔗

`bayesStationaryEnv`🔗

`isBayesAlgEnvSeq`🔗

`bayesTrajMeasure`🔗

`instIsProbabilityMeasureForallNatProdBayesTrajMeasure`🔗

`isBayesAlgEnvSeq_bayesTrajMeasure`🔗

`bayesTrajMeasurePosterior`🔗

`instIsMarkovKernelForallSubtypeNatMemFinsetIicProdBayesTrajMeasurePosterior`🔗