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 actions and observations generated by an algorithm-environment pair is unique: it does not depend on the probability space used. If A₁, R₁ and A₂, R₂ are two algorithm-environment sequences generated by the same algorithm-environment pair on probability spaces (Ω, P) and (Ω', P'), then P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)).

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

Measure on the sequence of actions and observations generated by the algorithm/environment.

Equations

• Learning.trajMeasure alg env = ProbabilityTheory.Kernel.trajMeasure (alg.p0.compProd env.ν0) (Learning.stepKernel alg env)

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

theorem Learning.eq_trajMeasure_of_isAlgEnvSeq {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq A₁ R₁ alg env P) : MeasureTheory.Measure.map (fun (ω : Ω) (n : ℕ) => (A₁ n ω, R₁ n ω)) P = trajMeasure alg env

theorem Learning.eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {N : ℕ} (h : IsAlgEnvSeqUntil A₁ R₁ alg env P N) : MeasureTheory.Measure.map (fun (ω : Ω) (n : ↥(Finset.Iic N)) => (A₁ (↑n) ω, R₁ (↑n) ω)) P = MeasureTheory.Measure.map (Preorder.frestrictLe N) (trajMeasure alg env)

theorem Learning.isAlgEnvSeq_unique {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4} {Ω' : Type u_5} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} (h1 : IsAlgEnvSeq A₁ R₁ alg env P) (h2 : IsAlgEnvSeq A₂ R₂ alg env P') : MeasureTheory.Measure.map (fun (ω : Ω) (n : ℕ) => (A₁ n ω, R₁ n ω)) P = MeasureTheory.Measure.map (fun (ω : Ω') (n : ℕ) => (A₂ n ω, R₂ n ω)) P'

The law of the sequence of actions and observations 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} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4} {Ω' : Type u_5} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} (h1 : IsAlgEnvSeq A₁ R₁ alg env P) (h2 : IsAlgEnvSeq A₂ R₂ alg env P') : ProbabilityTheory.IdentDistrib (fun (ω : Ω) (n : ℕ) => (A₁ n ω, R₁ n ω)) (fun (ω' : Ω') (n : ℕ) => (A₂ n ω', R₂ n ω')) P P'

The law of the sequence of actions and observations 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} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {Ω : Type u_4} {Ω' : Type u_5} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace 𝓨] [Nonempty 𝓨] {alg : Algorithm 𝓐 𝓨} {env : Environment 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {A₁ : ℕ → Ω → 𝓐} {R₁ : ℕ → Ω → 𝓨} {A₂ : ℕ → Ω' → 𝓐} {R₂ : ℕ → Ω' → 𝓨} {N : ℕ} (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N) (h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) : MeasureTheory.Measure.map (fun (ω : Ω) (n : ↥(Finset.Iic N)) => (A₁ (↑n) ω, R₁ (↑n) ω)) P = MeasureTheory.Measure.map (fun (ω : Ω') (n : ↥(Finset.Iic N)) => (A₂ (↑n) ω, R₂ (↑n) ω)) P'

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

Action and feedback at step n.

Equations

• Learning.IT.step n h = h n

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

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

Equations

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

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

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

Equations

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

def Learning.IT.hist {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : ↥(Finset.Iic n) → 𝓐 × 𝓨

hist n is the history up to time n. This is a random variable on the measurable space ℕ → 𝓐 × 𝓨.

Equations

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

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

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

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

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

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

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

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

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

theorem Learning.IT.hist_eq_frestrictLe {𝓐 : Type u_1} {𝓨 : Type u_2} : hist = Preorder.frestrictLe

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

Filtration of the algorithm Seq.

Equations

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

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

theorem Learning.IT.step_eq_eval_comp_hist {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ) : step n = (fun (x : ↥(Finset.Iic n) → 𝓐 × 𝓨) => x ⟨n, ⋯⟩) ∘ hist n

theorem Learning.IT.action_eq_eval_comp_hist {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ) : action n = (fun (x : ↥(Finset.Iic n) → 𝓐 × 𝓨) => (x ⟨n, ⋯⟩).1) ∘ hist n

theorem Learning.IT.feedback_eq_eval_comp_hist {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ℕ) : feedback n = (fun (x : ↥(Finset.Iic n) → 𝓐 × 𝓨) => (x ⟨n, ⋯⟩).2) ∘ hist n

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

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

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

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

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

Filtration generated by the history at time n-1 together with the action at time n.

Equations

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

theorem Learning.IT.filtrationAction_zero_eq_comap {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : ↑(filtrationAction 𝓐 𝓨) 0 = MeasurableSpace.comap (action 0) inferInstance

theorem Learning.IT.filtrationAction_eq_comap {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) (hn : n ≠ 0) : ↑(filtrationAction 𝓐 𝓨) n = MeasurableSpace.comap (fun (ω : ℕ → 𝓐 × 𝓨) => (hist (n - 1) ω, action n ω)) inferInstance

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

theorem Learning.IT.filtration_le_filtrationAction {𝓐 : Type u_1} {𝓨 : Type u_2} {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} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (n : ℕ) : ↑(filtrationAction 𝓐 𝓨) n ≤ ↑(IT.filtration 𝓐 𝓨) n

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

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

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

theorem Learning.IT.hasLaw_action_zero {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) : ProbabilityTheory.HasLaw (action 0) alg.p0 (trajMeasure alg env)

theorem Learning.IT.condDistrib_feedback_zero {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) : ⇑𝓛[feedback 0 | action 0; trajMeasure alg env] =ᵐ[MeasureTheory.Measure.map (action 0) (trajMeasure alg env)] ⇑env.ν0

theorem Learning.IT.condDistrib_step {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] [StandardBorelSpace 𝓐] [Nonempty 𝓐] (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : ⇑𝓛[step (n + 1) | hist n; trajMeasure alg env] =ᵐ[MeasureTheory.Measure.map (hist n) (trajMeasure alg env)] ⇑(stepKernel alg env n)

theorem Learning.IT.condDistrib_action {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] [StandardBorelSpace 𝓐] [Nonempty 𝓐] (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : ⇑𝓛[action (n + 1) | hist n; trajMeasure alg env] =ᵐ[MeasureTheory.Measure.map (hist n) (trajMeasure alg env)] ⇑(alg.policy n)

theorem Learning.IT.condDistrib_feedback {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] [StandardBorelSpace 𝓐] [Nonempty 𝓐] (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) (n : ℕ) : ⇑𝓛[feedback (n + 1) | fun (ω : ℕ → 𝓐 × 𝓨) => (hist n ω, action (n + 1) ω); trajMeasure alg env] =ᵐ[MeasureTheory.Measure.map (fun (ω : ℕ → 𝓐 × 𝓨) => (hist n ω, action (n + 1) ω)) (trajMeasure alg env)] ⇑(env.feedback n)

theorem Learning.IT.isAlgEnvSeq_trajMeasure {𝓐 : Type u_1} {𝓨 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [StandardBorelSpace 𝓨] [Nonempty 𝓨] [StandardBorelSpace 𝓐] [Nonempty 𝓐] (alg : Algorithm 𝓐 𝓨) (env : Environment 𝓐 𝓨) : IsAlgEnvSeq action feedback alg env (trajMeasure alg env)