Algorithms and environments

We define structures for stochastic, sequential algorithms and environments, and the notion of an algorithm-environment sequence, which is a sequence of observations, actions and feedbacks generated by an algorithm interacting with an environment.

A round of interaction consists of an observation in 𝓞, an action in 𝓐 and a feedback in 𝓨, in that order: it is an element of Round 𝓞 𝓐 𝓨 = 𝓞 × 𝓐 × 𝓨. At time n, the algorithm has seen the n complete rounds at times 0, ..., n - 1. That history is an element of Hist 𝓞 𝓐 𝓨 n = Fin n → Round 𝓞 𝓐 𝓨. The environment then draws an observation O n given the history, the algorithm chooses an action A n according to its policy applied to the history and O n, and the environment returns a feedback Y n given the history, O n and A n. In particular, the first observation is drawn according to the observation kernel at time 0, applied to the empty history (the unique element of Hist 𝓞 𝓐 𝓨 0).

Main definitions

• Round 𝓞 𝓐 𝓨: one round of interaction, an observation-action-feedback triple.
• Hist 𝓞 𝓐 𝓨 n: a history of n complete rounds.
• Algorithm 𝓞 𝓐 𝓨: a stochastic, sequential algorithm.
• Environment 𝓞 𝓐 𝓨: a stochastic environment.
• history O A Y n: the history before time n, a random variable with values in Hist 𝓞 𝓐 𝓨 n.
• IsAlgEnvSeq O A Y alg env P: an algorithm-environment sequence. That is, a sequence of observations O, actions A and feedbacks Y that have the correct conditional distributions to be generated by an algorithm alg interacting with an environment env, defined on a probability space (Ω, P).
• IsAlgEnvSeqUntil O A Y alg env P N: O, A and Y form an algorithm-environment sequence for the times n < N.

@[instance_reducible]

instance Prod.instUnique {α : Type u_1} {β : Type u_2} [Unique α] [Unique β] : Unique (α × β)

Equations

• Prod.instUnique = { default := (default, default), uniq := ⋯ }

@[reducible, inline]

abbrev Learning.Round (𝓞 : Type u_5) (𝓐 : Type u_6) (𝓨 : Type u_7) : Type (max u_5 u_7 u_6)

One round of interaction: an observation, then an action, then a feedback.

Equations

• Learning.Round 𝓞 𝓐 𝓨 = (𝓞 × 𝓐 × 𝓨)

def Learning.Round.obs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (r : Round 𝓞 𝓐 𝓨) : 𝓞

The observation of a round.

Equations

• r.obs = r.1

def Learning.Round.action {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (r : Round 𝓞 𝓐 𝓨) : 𝓐

The action of a round.

Equations

• r.action = r.2.1

def Learning.Round.feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (r : Round 𝓞 𝓐 𝓨) : 𝓨

The feedback of a round.

Equations

• r.feedback = r.2.2

@[simp]

theorem Learning.Round.obs_mk {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (o : 𝓞) (a : 𝓐) (y : 𝓨) : obs (o, a, y) = o

@[simp]

theorem Learning.Round.action_mk {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (o : 𝓞) (a : 𝓐) (y : 𝓨) : action (o, a, y) = a

@[simp]

theorem Learning.Round.feedback_mk {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (o : 𝓞) (a : 𝓐) (y : 𝓨) : feedback (o, a, y) = y

@[simp]

theorem Learning.Round.mk_obs_action_feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (r : Round 𝓞 𝓐 𝓨) : (r.obs, r.action, r.feedback) = r

theorem Learning.Round.obs_eq_fst {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (r : Round 𝓞 𝓐 𝓨) : r.obs = r.1

theorem Learning.Round.action_eq_snd_fst {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (r : Round 𝓞 𝓐 𝓨) : r.action = r.2.1

theorem Learning.Round.feedback_eq_snd_snd {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} (r : Round 𝓞 𝓐 𝓨) : r.feedback = r.2.2

theorem Learning.Round.measurable_obs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : Measurable obs

theorem Learning.Round.measurable_action {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : Measurable action

theorem Learning.Round.measurable_feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : Measurable feedback

@[reducible, inline]

abbrev Learning.Hist (𝓞 : Type u_5) (𝓐 : Type u_6) (𝓨 : Type u_7) (n : ℕ) : Type (max (max u_7 u_6) u_5)

History of n complete rounds; n = 0 is the empty history.

Equations

• Learning.Hist 𝓞 𝓐 𝓨 n = (Fin n → Learning.Round 𝓞 𝓐 𝓨)

structure Learning.Algorithm (𝓞 : Type u_5) (𝓐 : Type u_6) (𝓨 : Type u_7) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : Type (max (max u_5 u_6) u_7)

A stochastic, sequential algorithm. At each round, it sees an observation in 𝓞, then takes an action in 𝓐, and finally receives feedback in 𝓨. The action is a random function of the past rounds and the current observation.

• policy (n : ℕ) : ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n × 𝓞) 𝓐

  Law of the action of round n given the past rounds and the current observation.

• isMarkovKernel_policy (n : ℕ) : ProbabilityTheory.IsMarkovKernel (self.policy n)

  The policy is a Markov kernel.

theorem Learning.Algorithm.ext {𝓞 : Type u_5} {𝓐 : Type u_6} {𝓨 : Type u_7} {inst✝ : MeasurableSpace 𝓞} {inst✝¹ : MeasurableSpace 𝓐} {inst✝² : MeasurableSpace 𝓨} {x y : Algorithm 𝓞 𝓐 𝓨} (policy : x.policy = y.policy) : x = y

theorem Learning.Algorithm.ext_iff {𝓞 : Type u_5} {𝓐 : Type u_6} {𝓨 : Type u_7} {inst✝ : MeasurableSpace 𝓞} {inst✝¹ : MeasurableSpace 𝓐} {inst✝² : MeasurableSpace 𝓨} {x y : Algorithm 𝓞 𝓐 𝓨} : x = y ↔ x.policy = y.policy

instance Learning.instIsMarkovKernelProdHistPolicy {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (alg.policy n)

@[instance_reducible]

instance Learning.instMeasurableSpaceAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : MeasurableSpace (Algorithm 𝓞 𝓐 𝓨)

Equations

• Learning.instMeasurableSpaceAlgorithm = MeasurableSpace.comap (fun (alg : Learning.Algorithm 𝓞 𝓐 𝓨) => alg.policy) inferInstance

theorem Learning.measurable_algorithm_iff {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} (f : Ω → Algorithm 𝓞 𝓐 𝓨) : Measurable f ↔ ∀ (n : ℕ), Measurable fun (x : Ω) => (f x).policy n

structure Learning.Environment (𝓞 : Type u_5) (𝓐 : Type u_6) (𝓨 : Type u_7) [MeasurableSpace 𝓞] [MeasurableSpace 𝓐] [MeasurableSpace 𝓨] : Type (max (max u_5 u_6) u_7)

A stochastic environment. At each round, an observation is drawn prior to the algorithm taking an action. Then the environment provides feedback based on the observation and the action.

• obs (n : ℕ) : ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞

  Law of the observation of round n given the past rounds.

• feedback (n : ℕ) : ProbabilityTheory.Kernel ((Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐) 𝓨

  Law of the feedback of round n given the past rounds, the observation and the action.

• isMarkovKernel_obs (n : ℕ) : ProbabilityTheory.IsMarkovKernel (self.obs n)

  The observation kernel is a Markov kernel.

• isMarkovKernel_feedback (n : ℕ) : ProbabilityTheory.IsMarkovKernel (self.feedback n)

  The feedback kernel is a Markov kernel.

theorem Learning.Environment.ext {𝓞 : Type u_5} {𝓐 : Type u_6} {𝓨 : Type u_7} {inst✝ : MeasurableSpace 𝓞} {inst✝¹ : MeasurableSpace 𝓐} {inst✝² : MeasurableSpace 𝓨} {x y : Environment 𝓞 𝓐 𝓨} (obs : x.obs = y.obs) (feedback : x.feedback = y.feedback) : x = y

theorem Learning.Environment.ext_iff {𝓞 : Type u_5} {𝓐 : Type u_6} {𝓨 : Type u_7} {inst✝ : MeasurableSpace 𝓞} {inst✝¹ : MeasurableSpace 𝓐} {inst✝² : MeasurableSpace 𝓨} {x y : Environment 𝓞 𝓐 𝓨} : x = y ↔ x.obs = y.obs ∧ x.feedback = y.feedback

instance Learning.instIsMarkovKernelHistObs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (env.obs n)

instance Learning.instIsMarkovKernelProdHistFeedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (env.feedback n)

@[instance_reducible]

instance Learning.instMeasurableSpaceEnvironment {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} : MeasurableSpace (Environment 𝓞 𝓐 𝓨)

Equations

• Learning.instMeasurableSpaceEnvironment = MeasurableSpace.comap (fun (env : Learning.Environment 𝓞 𝓐 𝓨) => (env.obs, env.feedback)) inferInstance

theorem Learning.measurable_environment_iff {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} (f : Ω → Environment 𝓞 𝓐 𝓨) : Measurable f ↔ ∀ (n : ℕ), (Measurable fun (x : Ω) => (f x).obs n) ∧ Measurable fun (x : Ω) => (f x).feedback n

def Learning.Environment.obs0 {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : MeasureTheory.Measure 𝓞

Distribution of the first observation: the observation kernel at time 0 applied to the empty history.

Equations

• env.obs0 = (env.obs 0) default

instance Learning.Environment.instIsProbabilityMeasureObs0 {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : MeasureTheory.IsProbabilityMeasure env.obs0

theorem Learning.Environment.obs0_def {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : env.obs0 = (env.obs 0) default

theorem Learning.Environment.obs_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (h : Hist 𝓞 𝓐 𝓨 0) : (env.obs 0) h = env.obs0

noncomputable def Learning.Algorithm.p0 {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) : ProbabilityTheory.Kernel 𝓞 𝓐

Distribution of the first action given the first observation: the policy at time 0 applied to the empty history.

Equations

• alg.p0 = (alg.policy 0).sectR default

instance Learning.Algorithm.instIsMarkovKernelP0 {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) : ProbabilityTheory.IsMarkovKernel alg.p0

theorem Learning.Algorithm.p0_def {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) : alg.p0 = (alg.policy 0).sectR default

theorem Learning.Algorithm.p0_apply {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (o : 𝓞) : alg.p0 o = (alg.policy 0) (default, o)

theorem Learning.Algorithm.policy_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (h : Hist 𝓞 𝓐 𝓨 0) (o : 𝓞) : (alg.policy 0) (h, o) = alg.p0 o

noncomputable def Learning.Environment.ν0 {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : ProbabilityTheory.Kernel (𝓞 × 𝓐) 𝓨

Distribution of the first feedback given the first observation and action: the feedback kernel at time 0 applied to the empty history.

Equations

• env.ν0 = (env.feedback 0).comap (fun (p : 𝓞 × 𝓐) => ((default, p.1), p.2)) ⋯

instance Learning.Environment.instIsMarkovKernelProdν0 {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : ProbabilityTheory.IsMarkovKernel env.ν0

theorem Learning.Environment.ν0_def {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) : env.ν0 = (env.feedback 0).comap (fun (p : 𝓞 × 𝓐) => ((default, p.1), p.2)) ⋯

theorem Learning.Environment.ν0_apply {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (o : 𝓞) (a : 𝓐) : env.ν0 (o, a) = (env.feedback 0) ((default, o), a)

theorem Learning.Environment.feedback_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) (h : Hist 𝓞 𝓐 𝓨 0) (o : 𝓞) (a : 𝓐) : (env.feedback 0) ((h, o), a) = env.ν0 (o, a)

noncomputable def Learning.stepKernel {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) (Round 𝓞 𝓐 𝓨)

Kernel describing the distribution of the round at time n given the history before n.

Equations

• Learning.stepKernel alg env n = (env.obs n).compProd ((alg.policy n).compProd (env.feedback n))

instance Learning.instIsMarkovKernelHistProdStepKernel {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (stepKernel alg env n)

theorem Learning.stepKernel_def {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : stepKernel alg env n = (env.obs n).compProd ((alg.policy n).compProd (env.feedback n))

@[simp]

theorem Learning.fst_stepKernel {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (n : ℕ) : (stepKernel alg env n).fst = env.obs n

theorem Learning.stepKernel_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (h : Hist 𝓞 𝓐 𝓨 0) : (stepKernel alg env 0) h = env.obs0.compProd (alg.p0.compProd env.ν0)

def Learning.step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : Round 𝓞 𝓐 𝓨

Step of the algorithm-environment sequence: the round at time n.

Equations

• Learning.step O A Y n ω = (O n ω, A n ω, Y n ω)

@[simp]

theorem Learning.obs_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) (ω : Ω) : (step O A Y n ω).obs = O n ω

@[simp]

theorem Learning.action_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) (ω : Ω) : (step O A Y n ω).action = A n ω

@[simp]

theorem Learning.feedback_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) (ω : Ω) : (step O A Y n ω).feedback = Y n ω

theorem Learning.measurable_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) (hO : Measurable (O n)) (hA : Measurable (A n)) (hY : Measurable (Y n)) : Measurable (step O A Y n)

def Learning.trajectory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (ω : Ω) : ℕ → Round 𝓞 𝓐 𝓨

A random variable that gives the sequence of rounds.

Equations

• Learning.trajectory O A Y ω n = (O n ω, A n ω, Y n ω)

theorem Learning.measurable_trajectory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (hO : ∀ (n : ℕ), Measurable (O n)) (hA : ∀ (n : ℕ), Measurable (A n)) (hR : ∀ (n : ℕ), Measurable (Y n)) : Measurable (trajectory O A Y)

def Learning.history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (n : ℕ) (ω : Ω) : Hist 𝓞 𝓐 𝓨 n

History of the algorithm-environment sequence before time n: the rounds at times 0, ..., n - 1.

Equations

• Learning.history O A Y n ω i = (O (↑i) ω, A (↑i) ω, Y (↑i) ω)

theorem Learning.history_apply {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) (ω : Ω) (i : Fin n) : history O A Y n ω i = (O (↑i) ω, A (↑i) ω, Y (↑i) ω)

@[simp]

theorem Learning.history_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} : history O A Y 0 = fun (x : Ω) => default

theorem Learning.measurable_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (hO : ∀ (n : ℕ), Measurable (O n)) (hA : ∀ (n : ℕ), Measurable (A n)) (hY : ∀ (n : ℕ), Measurable (Y n)) (n : ℕ) : Measurable (history O A Y n)

theorem Learning.history_congr {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {O' : ℕ → Ω → 𝓞} {A' : ℕ → Ω → 𝓐} {Y' : ℕ → Ω → 𝓨} {P : MeasureTheory.Measure Ω} (hO : ∀ (n : ℕ), O' n =ᵐ[P] O n) (hA : ∀ (n : ℕ), A' n =ᵐ[P] A n) (hY : ∀ (n : ℕ), Y' n =ᵐ[P] Y n) (n : ℕ) : history O' A' Y' n =ᵐ[P] history O A Y n

theorem Learning.eval_comp_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) : (fun (x : Hist 𝓞 𝓐 𝓨 (n + 1)) => x (Fin.last n)) ∘ history O A Y (n + 1) = step O A Y n

theorem Learning.obs_eval_comp_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) : (fun (x : Hist 𝓞 𝓐 𝓨 (n + 1)) => (x (Fin.last n)).obs) ∘ history O A Y (n + 1) = O n

theorem Learning.action_eval_comp_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) : (fun (x : Hist 𝓞 𝓐 𝓨 (n + 1)) => (x (Fin.last n)).action) ∘ history O A Y (n + 1) = A n

theorem Learning.feedback_eval_comp_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) : (fun (x : Hist 𝓞 𝓐 𝓨 (n + 1)) => (x (Fin.last n)).feedback) ∘ history O A Y (n + 1) = Y n

theorem Learning.history_eq_comp_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {m n : ℕ} (hmn : m ≤ n) : history O A Y m = (fun (h : Hist 𝓞 𝓐 𝓨 n) (i : Fin m) => h (Fin.castLE hmn i)) ∘ history O A Y n

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

theorem Learning.history_succ {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (n : ℕ) : history O A Y (n + 1) = ⇑(MeasurableEquiv.finSuccProd (Round 𝓞 𝓐 𝓨) n).symm ∘ fun (ω : Ω) => (history O A Y n ω, step O A Y n ω)

structure Learning.IsAlgEnvSeq {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] : Prop

An algorithm-environment sequence: a sequence of observations, actions and feedbacks generated by an algorithm interacting with an environment.

• measurable_obs (n : ℕ) : Measurable (O n)

  The observation sequence is measurable.

• measurable_action (n : ℕ) : Measurable (A n)

  The action sequence is measurable.

• measurable_feedback (n : ℕ) : Measurable (Y n)

  The feedback sequence is measurable.

• hasCondDistrib_obs (n : ℕ) : ProbabilityTheory.HasCondDistrib (O n) (history O A Y n) (env.obs n) P

  The observation at time n has the correct conditional distribution given the history.

• hasCondDistrib_action (n : ℕ) : ProbabilityTheory.HasCondDistrib (A n) (fun (ω : Ω) => (history O A Y n ω, O n ω)) (alg.policy n) P

  The action at time n has the correct conditional distribution given the history and the observation at time n.

• hasCondDistrib_feedback (n : ℕ) : ProbabilityTheory.HasCondDistrib (Y n) (fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) (env.feedback n) P

  The feedback at time n has the correct conditional distribution given the history, the observation and the action at time n.

structure Learning.IsAlgEnvSeqUntil {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) (alg : Algorithm 𝓞 𝓐 𝓨) (env : Environment 𝓞 𝓐 𝓨) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] (N : ℕ) : Prop

An algorithm-environment sequence until time N: a sequence of observations, actions and feedbacks such that the rounds at times n < N are generated by an algorithm interacting with an environment. In particular, the law of history O A Y N is determined.

• measurable_obs (n : ℕ) : Measurable (O n)

  The observation sequence is measurable.

• measurable_action (n : ℕ) : Measurable (A n)

  The action sequence is measurable.

• measurable_feedback (n : ℕ) : Measurable (Y n)

  The feedback sequence is measurable.

• hasCondDistrib_obs (n : ℕ) (hn : n < N) : ProbabilityTheory.HasCondDistrib (O n) (history O A Y n) (env.obs n) P

  The observation at time n < N has the correct conditional distribution given the history.

• hasCondDistrib_action (n : ℕ) (hn : n < N) : ProbabilityTheory.HasCondDistrib (A n) (fun (ω : Ω) => (history O A Y n ω, O n ω)) (alg.policy n) P

  The action at time n < N has the correct conditional distribution given the history and the observation at time n.

• hasCondDistrib_feedback (n : ℕ) (hn : n < N) : ProbabilityTheory.HasCondDistrib (Y n) (fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) (env.feedback n) P

  The feedback at time n < N has the correct conditional distribution given the history, the observation and the action at time n.

theorem Learning.IsAlgEnvSeqUntil.mono {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (h : IsAlgEnvSeqUntil O A Y alg env P N) {N' : ℕ} (hN : N' ≤ N) : IsAlgEnvSeqUntil O A Y alg env P N'

theorem Learning.IsAlgEnvSeq.isAlgEnvSeqUntil {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (N : ℕ) : IsAlgEnvSeqUntil O A Y alg env P N

theorem Learning.IsAlgEnvSeq.isAlgEnvSeqUntil_of_policy_eq {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} {alg' : Algorithm 𝓞 𝓐 𝓨} (h : IsAlgEnvSeq O A Y alg env P) (h_eq : ∀ n < N, alg.policy n = alg'.policy n) : IsAlgEnvSeqUntil O A Y alg' env P N

If two algorithms have the same policy before time N, then a sequence generated by the first one interacting with an environment is a sequence generated by the second one until time N.

theorem Learning.IsAlgEnvSeq.congr {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {O' : ℕ → Ω → 𝓞} {A' : ℕ → Ω → 𝓐} {Y' : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq O A Y alg env P) (hO' : ∀ (n : ℕ), Measurable (O' n)) (hA' : ∀ (n : ℕ), Measurable (A' n)) (hY' : ∀ (n : ℕ), Measurable (Y' n)) (hO : ∀ (n : ℕ), O' n =ᵐ[P] O n) (hA : ∀ (n : ℕ), A' n =ᵐ[P] A n) (hY : ∀ (n : ℕ), Y' n =ᵐ[P] Y n) : IsAlgEnvSeq O' A' Y' alg env P

IsAlgEnvSeq only depends on the almost everywhere equivalence classes of the processes.

theorem Learning.isAlgEnvSeq_iff_forall_isAlgEnvSeqUntil {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] : IsAlgEnvSeq O A Y alg env P ↔ ∀ (N : ℕ), IsAlgEnvSeqUntil O A Y alg env P N

theorem Learning.IsAlgEnvSeq.measurable_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : Measurable (step O A Y n)

theorem Learning.IsAlgEnvSeq.measurable_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : Measurable (history O A Y n)

theorem Learning.IsAlgEnvSeq.measurable_trajectory {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : Measurable (trajectory O A Y)

theorem Learning.IsAlgEnvSeqUntil.measurable_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (h : IsAlgEnvSeqUntil O A Y alg env P N) (n : ℕ) : Measurable (step O A Y n)

theorem Learning.IsAlgEnvSeqUntil.measurable_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (h : IsAlgEnvSeqUntil O A Y alg env P N) (n : ℕ) : Measurable (history O A Y n)

theorem Learning.IsAlgEnvSeq.hasCondDistrib_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (step O A Y n) (history O A Y n) (stepKernel alg env n) P

theorem Learning.IsAlgEnvSeqUntil.hasCondDistrib_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (h : IsAlgEnvSeqUntil O A Y alg env P N) (n : ℕ) (hn : n < N) : ProbabilityTheory.HasCondDistrib (step O A Y n) (history O A Y n) (stepKernel alg env n) P

Laws at time 0

At time 0 the history is the unique element of Hist 𝓞 𝓐 𝓨 0: conditioning on it is the same as not conditioning. Note that those results need P to be a probability measure.

theorem Learning.hasLaw_history_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (O : ℕ → Ω → 𝓞) (A : ℕ → Ω → 𝓐) (Y : ℕ → Ω → 𝓨) : ProbabilityTheory.HasLaw (history O A Y 0) (MeasureTheory.Measure.dirac default) P

The history before time 0 is a constant.

theorem Learning.IsAlgEnvSeqUntil.hasLaw_obs_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} [MeasureTheory.IsProbabilityMeasure P] (h : IsAlgEnvSeqUntil O A Y alg env P N) (hN : 0 < N) : ProbabilityTheory.HasLaw (O 0) env.obs0 P

theorem Learning.IsAlgEnvSeq.hasLaw_obs_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsProbabilityMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : ProbabilityTheory.HasLaw (O 0) env.obs0 P

theorem Learning.IsAlgEnvSeqUntil.hasCondDistrib_action_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (h : IsAlgEnvSeqUntil O A Y alg env P N) (hN : 0 < N) : ProbabilityTheory.HasCondDistrib (A 0) (O 0) alg.p0 P

theorem Learning.IsAlgEnvSeq.hasCondDistrib_action_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : ProbabilityTheory.HasCondDistrib (A 0) (O 0) alg.p0 P

theorem Learning.IsAlgEnvSeqUntil.hasCondDistrib_feedback_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} (h : IsAlgEnvSeqUntil O A Y alg env P N) (hN : 0 < N) : ProbabilityTheory.HasCondDistrib (Y 0) (fun (ω : Ω) => (O 0 ω, A 0 ω)) env.ν0 P

theorem Learning.IsAlgEnvSeq.hasCondDistrib_feedback_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : ProbabilityTheory.HasCondDistrib (Y 0) (fun (ω : Ω) => (O 0 ω, A 0 ω)) env.ν0 P

theorem Learning.IsAlgEnvSeqUntil.hasLaw_step_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {N : ℕ} [MeasureTheory.IsProbabilityMeasure P] (h : IsAlgEnvSeqUntil O A Y alg env P N) (hN : 0 < N) : ProbabilityTheory.HasLaw (step O A Y 0) (env.obs0.compProd (alg.p0.compProd env.ν0)) P

theorem Learning.IsAlgEnvSeq.hasLaw_step_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsProbabilityMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : ProbabilityTheory.HasLaw (step O A Y 0) (env.obs0.compProd (alg.p0.compProd env.ν0)) P

theorem Learning.IsAlgEnvSeq.hasLaw_obs_comp {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ProbabilityTheory.HasLaw (O n) ((MeasureTheory.Measure.map (history O A Y n) P).bind ⇑(env.obs n)) P

theorem Learning.IsAlgEnvSeq.hasLaw_action_comp {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ProbabilityTheory.HasLaw (A n) ((MeasureTheory.Measure.map (fun (ω : Ω) => (history O A Y n ω, O n ω)) P).bind ⇑(alg.policy n)) P

theorem Learning.IsAlgEnvSeq.hasLaw_feedback_comp {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ProbabilityTheory.HasLaw (Y n) ((MeasureTheory.Measure.map (fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) P).bind ⇑(env.feedback n)) P

theorem Learning.IsAlgEnvSeq.hasLaw_step_comp {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ProbabilityTheory.HasLaw (step O A Y n) ((MeasureTheory.Measure.map (history O A Y n) P).bind ⇑(stepKernel alg env n)) P

theorem Learning.IsAlgEnvSeq.hasLaw_feedback_zero_cond {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] [MeasurableSingletonClass 𝓞] [MeasurableSingletonClass 𝓐] (h : IsAlgEnvSeq O A Y alg env P) {p : 𝓞 × 𝓐} (hP : P ((fun (ω : Ω) => (O 0 ω, A 0 ω)) ⁻¹' {p}) ≠ 0) : ProbabilityTheory.HasLaw (Y 0) (env.ν0 p) P[|(fun (ω : Ω) => (O 0 ω, A 0 ω)) ⁻¹' {p}]

Conditionally on the event (O 0, A 0) = p, the first feedback has law env.ν0 p.

def Learning.IsAlgEnvSeq.filtration {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Filtration ℕ mΩ

Filtration generated by the history up to time n (included): h.filtration n is the σ-algebra generated by history O A Y (n + 1), that is by the rounds at times 0, ..., n.

Equations

• h.filtration = { seq := fun (n : ℕ) => MeasurableSpace.comap (Learning.history O A Y (n + 1)) inferInstance, mono' := ⋯, le' := ⋯ }

theorem Learning.IsAlgEnvSeq.filtration_eq_comap {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ↑h.filtration n = MeasurableSpace.comap (history O A Y (n + 1)) inferInstance

theorem Learning.IsAlgEnvSeq.measurable_history_succ_filtration {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : Measurable (history O A Y (n + 1))

theorem Learning.IsAlgEnvSeq.adapted_history {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtration (history O A Y)

theorem Learning.IsAlgEnvSeq.adapted_step {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtration (step O A Y)

theorem Learning.IsAlgEnvSeq.adapted_obs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtration O

theorem Learning.IsAlgEnvSeq.adapted_action {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtration A

theorem Learning.IsAlgEnvSeq.adapted_feedback {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtration Y

def Learning.IsAlgEnvSeq.filtrationObs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Filtration ℕ mΩ

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

Equations

• h.filtrationObs = { seq := fun (n : ℕ) => MeasurableSpace.comap (fun (ω : Ω) => (Learning.history O A Y n ω, O n ω)) inferInstance, mono' := ⋯, le' := ⋯ }

theorem Learning.IsAlgEnvSeq.filtrationObs_eq_comap {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ↑h.filtrationObs n = MeasurableSpace.comap (fun (ω : Ω) => (history O A Y n ω, O n ω)) inferInstance

def Learning.IsAlgEnvSeq.filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Filtration ℕ mΩ

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

Equations

• h.filtrationAction = { seq := fun (n : ℕ) => MeasurableSpace.comap (fun (ω : Ω) => ((Learning.history O A Y n ω, O n ω), A n ω)) inferInstance, mono' := ⋯, le' := ⋯ }

theorem Learning.IsAlgEnvSeq.filtrationAction_eq_comap {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ↑h.filtrationAction n = MeasurableSpace.comap (fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) inferInstance

theorem Learning.IsAlgEnvSeq.filtrationObs_zero_eq_comap {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : ↑h.filtrationObs 0 = MeasurableSpace.comap (O 0) inferInstance

theorem Learning.IsAlgEnvSeq.filtrationAction_zero_eq_comap {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : ↑h.filtrationAction 0 = MeasurableSpace.comap (fun (ω : Ω) => (O 0 ω, A 0 ω)) inferInstance

theorem Learning.IsAlgEnvSeq.measurable_history_filtrationObs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : Measurable (history O A Y n)

theorem Learning.IsAlgEnvSeq.measurable_history_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : Measurable (history O A Y n)

theorem Learning.IsAlgEnvSeq.filtrationObs_le_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ↑h.filtrationObs n ≤ ↑h.filtrationAction n

theorem Learning.IsAlgEnvSeq.filtration_le_filtrationObs_succ {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ↑h.filtration n ≤ ↑h.filtrationObs (n + 1)

theorem Learning.IsAlgEnvSeq.filtration_le_filtrationAction_succ {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ↑h.filtration n ≤ ↑h.filtrationAction (n + 1)

theorem Learning.IsAlgEnvSeq.filtrationAction_le_filtration {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ↑h.filtrationAction n ≤ ↑h.filtration n

theorem Learning.IsAlgEnvSeq.filtrationObs_le_filtration {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) (n : ℕ) : ↑h.filtrationObs n ≤ ↑h.filtration n

theorem Learning.IsAlgEnvSeq.adapted_obs_filtrationObs {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtrationObs O

theorem Learning.IsAlgEnvSeq.adapted_obs_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtrationAction O

theorem Learning.IsAlgEnvSeq.adapted_action_filtrationAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) : MeasureTheory.Adapted h.filtrationAction A

theorem Learning.IsAlgEnvSeq.measurable_feedback_filtrationObs_of_lt {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) {m n : ℕ} (hmn : m < n) : Measurable (Y m)

theorem Learning.IsAlgEnvSeq.measurable_feedback_filtrationAction_of_lt {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ω : Type u_4} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΩ : MeasurableSpace Ω} {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {alg : Algorithm 𝓞 𝓐 𝓨} {env : Environment 𝓞 𝓐 𝓨} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] (h : IsAlgEnvSeq O A Y alg env P) {m n : ℕ} (hmn : m < n) : Measurable (Y m)

Environments without observations

An environment with 𝓞 = Unit provides no information to the algorithm before it takes its action: the algorithm only sees the past rounds. Since Unit carries a unique probability measure, the observation kernels of such an environment are all equal to Kernel.const _ (Measure.dirac ()), and the observation process of an algorithm-environment sequence is noObs.

theorem Learning.Kernel.eq_const_dirac_unit {α : Type u_5} {mα : MeasurableSpace α} (κ : ProbabilityTheory.Kernel α Unit) [ProbabilityTheory.IsMarkovKernel κ] : κ = ProbabilityTheory.Kernel.const α (MeasureTheory.Measure.dirac ())

Every Markov kernel with codomain Unit is the constant kernel at Measure.dirac ().

theorem Learning.hasCondDistrib_unit {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {α : Type u_5} {mα : MeasurableSpace α} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : Ω → α} (hX : AEMeasurable X P) (U : Ω → Unit) (κ : ProbabilityTheory.Kernel α Unit) [ProbabilityTheory.IsMarkovKernel κ] : ProbabilityTheory.HasCondDistrib U X κ P

A random variable with values in Unit admits any Markov kernel as conditional distribution.

def Learning.noObs (Ω : Type u_5) : ℕ → Ω → Unit

The observation process of an algorithm-environment sequence without observations.

Equations

• Learning.noObs Ω x✝¹ x✝ = ()

@[simp]

theorem Learning.noObs_apply {Ω : Type u_4} (n : ℕ) (ω : Ω) : noObs Ω n ω = ()

theorem Learning.measurable_noObs {Ω : Type u_4} {mΩ : MeasurableSpace Ω} (n : ℕ) : Measurable (noObs Ω n)