Probability space for algorithm-environment interactions

For any algorithm and environment, we construct a probability space on which we can define a sequence of random variables representing the actions and feedback generated by the interaction of the algorithm and the environment. The main ingredient of the construction is the Ionescu-Tulcea theorem.

Main statements

• isAlgEnvSeq_unique: the law of the sequence of rounds generated by an algorithm-environment pair is unique: it does not depend on the probability space used. If O₁, A₁, R₁ and O₂, A₂, R₂ are two algorithm-environment sequences generated by the same algorithm-environment pair on probability spaces (Ω, P) and (Ω', P'), then P.map (trajectory O₁ A₁ R₁) = P'.map (trajectory O₂ A₂ R₂).

noncomputable def Learning.trajMeasure {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) : MeasureTheory.Measure (ℕ → Round 𝓞 𝓐 𝓨)

Measure on the sequence of rounds generated by the algorithm/environment.

Equations

• Learning.trajMeasure alg env = ProbabilityTheory.Kernel.trajMeasureFin (Learning.stepKernel alg env)

instance Learning.instIsProbabilityMeasureForallNatRoundTrajMeasure {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) : MeasureTheory.IsProbabilityMeasure (trajMeasure alg env)

def Learning.IT.step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) (h : ℕ → Round 𝓞 𝓐 𝓨) : Round 𝓞 𝓐 𝓨

The round at step n.

Equations

• Learning.IT.step n h = h n

def Learning.IT.obs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) (h : ℕ → Round 𝓞 𝓐 𝓨) : 𝓞

obs n is the observation at time n. This is a random variable on the measurable space ℕ → Round 𝓞 𝓐 𝓨.

Equations

• Learning.IT.obs n h = (h n).obs

def Learning.IT.action {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) (h : ℕ → Round 𝓞 𝓐 𝓨) : 𝓐

action n is the action pulled at time n. This is a random variable on the measurable space ℕ → Round 𝓞 𝓐 𝓨.

Equations

• Learning.IT.action n h = (h n).action

def Learning.IT.feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) (h : ℕ → Round 𝓞 𝓐 𝓨) : 𝓨

feedback n is the feedback at time n. This is a random variable on the measurable space ℕ → Round 𝓞 𝓐 𝓨.

Equations

• Learning.IT.feedback n h = (h n).feedback

def Learning.IT.hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) (h : ℕ → Round 𝓞 𝓐 𝓨) : Hist 𝓞 𝓐 𝓨 n

hist n is the history before time n: the rounds at times 0, ..., n - 1. This is a random variable on the measurable space ℕ → Round 𝓞 𝓐 𝓨.

Equations

• Learning.IT.hist n h i = h ↑i

theorem Learning.IT.fst_comp_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) : Prod.fst ∘ step n = obs n

theorem Learning.IT.history_obs_action_feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) : history obs action feedback n = hist n

@[simp]

theorem Learning.IT.hist_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} : hist 0 = fun (x : ℕ → Round 𝓞 𝓐 𝓨) => default

theorem Learning.IT.measurable_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (step n)

theorem Learning.IT.measurable_step_prod {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : Measurable fun (p : ℕ × (ℕ → Round 𝓞 𝓐 𝓨)) => step p.1 p.2

theorem Learning.IT.measurable_obs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (obs n)

theorem Learning.IT.measurable_obs_prod {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : Measurable fun (p : ℕ × (ℕ → Round 𝓞 𝓐 𝓨)) => obs p.1 p.2

theorem Learning.IT.measurable_action {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (action n)

theorem Learning.IT.measurable_action_prod {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : Measurable fun (p : ℕ × (ℕ → Round 𝓞 𝓐 𝓨)) => action p.1 p.2

theorem Learning.IT.measurable_feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (feedback n)

theorem Learning.IT.measurable_feedback_prod {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : Measurable fun (p : ℕ × (ℕ → Round 𝓞 𝓐 𝓨)) => feedback p.1 p.2

theorem Learning.IT.measurable_hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (hist n)

theorem Learning.IT.hist_succ_eq_comp_frestrictLe {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : hist (n + 1) = ⇑(MeasurableEquiv.finSuccPiIic (fun (x : ℕ) => Round 𝓞 𝓐 𝓨) n).symm ∘ Preorder.frestrictLe n

theorem Learning.IT.frestrictLe_eq_comp_hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Preorder.frestrictLe n = ⇑(MeasurableEquiv.finSuccPiIic (fun (x : ℕ) => Round 𝓞 𝓐 𝓨) n) ∘ hist (n + 1)

theorem Learning.IT.step_eq_eval_comp_hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) : step n = (fun (x : Hist 𝓞 𝓐 𝓨 (n + 1)) => x (Fin.last n)) ∘ hist (n + 1)

theorem Learning.IT.obs_eq_eval_comp_hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) : obs n = (fun (x : Hist 𝓞 𝓐 𝓨 (n + 1)) => (x (Fin.last n)).obs) ∘ hist (n + 1)

theorem Learning.IT.action_eq_eval_comp_hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) : action n = (fun (x : Hist 𝓞 𝓐 𝓨 (n + 1)) => (x (Fin.last n)).action) ∘ hist (n + 1)

theorem Learning.IT.feedback_eq_eval_comp_hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (n : ℕ) : feedback n = (fun (x : Hist 𝓞 𝓐 𝓨 (n + 1)) => (x (Fin.last n)).feedback) ∘ hist (n + 1)

theorem Learning.IT.hist_eq_comp_hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m n : ℕ} (hmn : m ≤ n) : hist m = (fun (h : Hist 𝓞 𝓐 𝓨 n) (i : Fin m) => h (Fin.castLE hmn i)) ∘ hist n

The history before time m is a restriction of the history before time n ≥ m.

theorem Learning.IsAlgEnvSeq.map_trajectory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O₁ : ℕ → Ω → 𝓞} {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq O₁ A₁ R₁ alg env P) : MeasureTheory.Measure.map (trajectory O₁ A₁ R₁) P = trajMeasure alg env

theorem Learning.IsAlgEnvSeq.hasLaw_trajectory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O₁ : ℕ → Ω → 𝓞} {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq O₁ A₁ R₁ alg env P) : ProbabilityTheory.HasLaw (trajectory O₁ A₁ R₁) (trajMeasure alg env) P

theorem Learning.IsAlgEnvSeqUntil.map_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O₁ : ℕ → Ω → 𝓞} {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {N : ℕ} (h : IsAlgEnvSeqUntil O₁ A₁ R₁ alg env P N) : MeasureTheory.Measure.map (history O₁ A₁ R₁ N) P = MeasureTheory.Measure.map (IT.hist N) (trajMeasure alg env)

theorem Learning.IsAlgEnvSeq.map_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5} {mΩ : MeasurableSpace Ω} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O₁ : ℕ → Ω → 𝓞} {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq O₁ A₁ R₁ alg env P) (n : ℕ) : MeasureTheory.Measure.map (history O₁ A₁ R₁ n) P = MeasureTheory.Measure.map (IT.hist n) (trajMeasure alg env)

theorem Learning.isAlgEnvSeq_unique {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5} {Ω' : Type u_6} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {O₁ : ℕ → Ω → 𝓞} {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {O₂ : ℕ → Ω' → 𝓞} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} (h1 : IsAlgEnvSeq O₁ A₁ R₁ alg env P) (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg env P') : MeasureTheory.Measure.map (trajectory O₁ A₁ R₁) P = MeasureTheory.Measure.map (trajectory O₂ A₂ R₂) P'

The law of the sequence of rounds generated by an algorithm-environment pair is unique: it does not depend on the probability space used.

theorem Learning.IsAlgEnvSeq.identDistrib_trajectory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5} {Ω' : Type u_6} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {O₁ : ℕ → Ω → 𝓞} {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {O₂ : ℕ → Ω' → 𝓞} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} (h1 : IsAlgEnvSeq O₁ A₁ R₁ alg env P) (h2 : IsAlgEnvSeq O₂ A₂ R₂ alg env P') : ProbabilityTheory.IdentDistrib (trajectory O₁ A₁ R₁) (trajectory O₂ A₂ R₂) P P'

The law of the sequence of rounds generated by an algorithm-environment pair is unique: it does not depend on the probability space used.

theorem Learning.isAlgEnvSeqUntil_unique {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_5} {Ω' : Type u_6} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {O₁ : ℕ → Ω → 𝓞} {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {O₂ : ℕ → Ω' → 𝓞} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} {N : ℕ} (h1 : IsAlgEnvSeqUntil O₁ A₁ R₁ alg env P N) (h2 : IsAlgEnvSeqUntil O₂ A₂ R₂ alg env P' N) : MeasureTheory.Measure.map (history O₁ A₁ R₁ N) P = MeasureTheory.Measure.map (history O₂ A₂ R₂ N) P'

The law of the history before time N is determined by the algorithm-environment pair, provided that the sequence is an algorithm-environment sequence until time N.

def Learning.IT.filtration (𝓞 : Type u_5) (𝓐 : Type u_6) (𝓨 : Type u_7) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : MeasureTheory.Filtration ℕ inferInstance

Filtration of the algorithm Seq: IT.filtration 𝓞 𝓐 𝓨 n is the σ-algebra generated by the rounds at times 0, ..., n, that is by hist (n + 1).

Equations

• Learning.IT.filtration 𝓞 𝓐 𝓨 = MeasureTheory.Filtration.piLE

theorem Learning.IT.filtration_eq_comap {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : ↑(IT.filtration 𝓞 𝓐 𝓨) n = MeasurableSpace.comap (hist (n + 1)) inferInstance

theorem Learning.IT.adapted_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : MeasureTheory.Adapted (IT.filtration 𝓞 𝓐 𝓨) step

theorem Learning.IT.adapted_obs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : MeasureTheory.Adapted (IT.filtration 𝓞 𝓐 𝓨) obs

theorem Learning.IT.measurable_hist_succ_filtration {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (hist (n + 1))

theorem Learning.IT.adapted_hist {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : MeasureTheory.Adapted (IT.filtration 𝓞 𝓐 𝓨) hist

theorem Learning.IT.adapted_action {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : MeasureTheory.Adapted (IT.filtration 𝓞 𝓐 𝓨) action

theorem Learning.IT.adapted_feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : MeasureTheory.Adapted (IT.filtration 𝓞 𝓐 𝓨) feedback

def Learning.IT.filtrationAction (𝓞 : Type u_5) (𝓐 : Type u_6) (𝓨 : Type u_7) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : MeasureTheory.Filtration ℕ inferInstance

Filtration generated by the history before time n together with the observation and the action at time n.

Equations

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

theorem Learning.IT.filtrationAction_eq_comap {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : ↑(filtrationAction 𝓞 𝓐 𝓨) n = MeasurableSpace.comap (fun (ω : ℕ → Round 𝓞 𝓐 𝓨) => ((hist n ω, obs n ω), action n ω)) inferInstance

theorem Learning.IT.filtrationAction_zero_eq_comap {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : ↑(filtrationAction 𝓞 𝓐 𝓨) 0 = MeasurableSpace.comap (fun (ω : ℕ → Round 𝓞 𝓐 𝓨) => (obs 0 ω, action 0 ω)) inferInstance

theorem Learning.IT.measurable_hist_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (hist n)

theorem Learning.IT.filtration_le_filtrationAction_add_one {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : ↑(IT.filtration 𝓞 𝓐 𝓨) n ≤ ↑(filtrationAction 𝓞 𝓐 𝓨) (n + 1)

theorem Learning.IT.filtration_le_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m n : ℕ} (h : n < m) : ↑(IT.filtration 𝓞 𝓐 𝓨) n ≤ ↑(filtrationAction 𝓞 𝓐 𝓨) m

theorem Learning.IT.filtrationAction_le_filtration_self {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : ↑(filtrationAction 𝓞 𝓐 𝓨) n ≤ ↑(IT.filtration 𝓞 𝓐 𝓨) n

theorem Learning.IT.filtrationAction_le_filtration {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {m n : ℕ} (h : m ≤ n) : ↑(filtrationAction 𝓞 𝓐 𝓨) m ≤ ↑(IT.filtration 𝓞 𝓐 𝓨) n

theorem Learning.IT.measurable_obs_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (obs n)

theorem Learning.IT.measurable_action_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : Measurable (action n)

theorem Learning.IT.hasCondDistrib_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.HasCondDistrib (step n) (hist n) (stepKernel alg env n) (trajMeasure alg env)

theorem Learning.IT.hasCondDistrib_obs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.HasCondDistrib (obs n) (hist n) (env.obs n) (trajMeasure alg env)

theorem Learning.IT.hasCondDistrib_action_feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.HasCondDistrib (fun (ω : ℕ → Round 𝓞 𝓐 𝓨) => (action n ω, feedback n ω)) (fun (ω : ℕ → Round 𝓞 𝓐 𝓨) => (hist n ω, obs n ω)) ((alg.policy n).compProd (env.feedback n)) (trajMeasure alg env)

The action and the feedback at time n, given the history and the observation at time n.

theorem Learning.IT.hasCondDistrib_action {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.HasCondDistrib (action n) (fun (ω : ℕ → Round 𝓞 𝓐 𝓨) => (hist n ω, obs n ω)) (alg.policy n) (trajMeasure alg env)

theorem Learning.IT.hasCondDistrib_feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.HasCondDistrib (feedback n) (fun (ω : ℕ → Round 𝓞 𝓐 𝓨) => ((hist n ω, obs n ω), action n ω)) (env.feedback n) (trajMeasure alg env)

theorem Learning.IT.isAlgEnvSeq_trajMeasure {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) : IsAlgEnvSeq obs action feedback alg env (trajMeasure alg env)

theorem Learning.IT.hasLaw_step_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) : ProbabilityTheory.HasLaw (step 0) (env.obs0.compProd (alg.p0.compProd env.ν0)) (trajMeasure alg env)

theorem Learning.IT.hasLaw_obs_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) : ProbabilityTheory.HasLaw (obs 0) env.obs0 (trajMeasure alg env)

theorem Learning.IT.hasCondDistrib_action_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) : ProbabilityTheory.HasCondDistrib (action 0) (obs 0) alg.p0 (trajMeasure alg env)

theorem Learning.IT.hasCondDistrib_feedback_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) : ProbabilityTheory.HasCondDistrib (feedback 0) (fun (ω : ℕ → Round 𝓞 𝓐 𝓨) => (obs 0 ω, action 0 ω)) env.ν0 (trajMeasure alg env)