Documentation

LeanMachineLearning.SequentialLearning.Deterministic

Deterministic algorithms and environments #

A deterministic algorithm chooses its action in a deterministic way. That is, that action is given by a measurable function of the history and of the current observation instead of a general Markov kernel. Similarly, a deterministic environment gives feedback in a deterministic way.

Main definitions #

We introduce two typeclasses IsDeterministicAlg and IsDeterministicEnv to express that an algorithm or an environment is deterministic. We also give definitions for the initial action and the next action of a deterministic algorithm, and for the feedback functions of a deterministic environment. Finally, we give a construction of a deterministic algorithm and environment from measurable functions.

IsDeterministicAlg alg: a typeclass expressing that the algorithm alg is deterministic.
IsDeterministicEnv env: a typeclass expressing that the environment env is deterministic.
nextAction alg n: the function that gives the action of a deterministic algorithm alg at step n, as a function of the history before n and of the observation at step n.
actionZero alg: the initial action of a deterministic algorithm alg, as a function of the first observation. This is nextAction alg 0 applied to the empty history.
feedbackFun env n: the function that gives the feedback of a deterministic environment env at step n, as a function of the history, the current observation and the current action.
feedbackFunZero env: the function that gives the initial feedback of a deterministic environment env. This is feedbackFun env 0 applied to the empty history.
detAlgorithm nextA h_next: a deterministic algorithm that chooses its action according to the measurable function nextA (with proof of measurability h_next). The initial action is fun o ↦ nextA 0 (default, o).
detEnvironment obs f hf: a deterministic environment with observation kernels obs, that gives feedback according to the measurable function f (with proof of measurability hf).

class Learning.IsDeterministicAlg {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) :

An algorithm is deterministic if its actions are determined by measurable functions of the history and of the current observation (and not possibly random kernels).

exists_nextAction (n : ℕ) : ∃ (nextAction : Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐) (h_meas : Measurable nextAction), alg.policy n = ProbabilityTheory.Kernel.deterministic nextAction h_meas

Instances

noncomputable def Learning.nextAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) [h_det : IsDeterministicAlg alg] (n : ℕ) :

Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐

The action of a deterministic algorithm at step n, as a function of the history before n and of the observation at step n.

Equations

Learning.nextAction alg n = ⋯.choose

Instances For

noncomputable def Learning.actionZero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] :

𝓞 → 𝓐

The initial action of a deterministic algorithm, as a function of the first observation.

Equations

Learning.actionZero alg o = Learning.nextAction alg 0 (default , o)

Instances For

theorem Learning.measurable_nextAction {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] (n : ℕ) :

Measurable (nextAction alg n)

theorem Learning.measurable_actionZero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] :

Measurable (actionZero alg)

theorem Learning.policy_eq_deterministic {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) [h_det : IsDeterministicAlg alg] (n : ℕ) :

alg.policy n = ProbabilityTheory.Kernel.deterministic (nextAction alg n) ⋯

theorem Learning.nextAction_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] (h : Hist 𝓞 𝓐 𝓨 0) (o : 𝓞) :

nextAction alg 0 (h, o) = actionZero alg o

theorem Learning.p0_eq_deterministic {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (alg : Algorithm 𝓞 𝓐 𝓨) [IsDeterministicAlg alg] :

alg.p0 = ProbabilityTheory.Kernel.deterministic (actionZero alg) ⋯

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

A n =ᵐ[P] fun (ω : Ω) => nextAction alg n (history O A Y n ω, O n ω)

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

A 0 =ᵐ[P] fun (ω : Ω) => actionZero alg (O 0 ω)

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

ProbabilityTheory.HasCondDistrib (A 0) (O 0) (ProbabilityTheory.Kernel.deterministic (actionZero alg) ⋯) P

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

ProbabilityTheory.HasCondDistrib (A 0) (O 0) (ProbabilityTheory.Kernel.deterministic (actionZero alg) ⋯) P

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

A n =ᵐ[P] fun (ω : Ω) => nextAction alg n (history O A Y n ω, O n ω)

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

A 0 =ᵐ[P] fun (ω : Ω) => actionZero alg (O 0 ω)

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

∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), A n ω = nextAction alg n (history O A Y n ω, O n ω)

class Learning.IsDeterministicEnv {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) :

An environment is deterministic if its feedbacks are determined by measurable functions of the history, the observation and the action (and not possibly random kernels).

exists_f (n : ℕ) : ∃ (f : (Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐 → 𝓨) (hf : Measurable f), env.feedback n = ProbabilityTheory.Kernel.deterministic f hf

Instances

noncomputable def Learning.feedbackFun {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) [h_det : IsDeterministicEnv env] (n : ℕ) :

(Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐 → 𝓨

The feedback function of a deterministic environment at step n.

Equations

Learning.feedbackFun env n = ⋯.choose

Instances For

theorem Learning.measurable_feedbackFun {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] (n : ℕ) :

Measurable (feedbackFun env n)

theorem Learning.feedback_eq_deterministic {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] (n : ℕ) :

env.feedback n = ProbabilityTheory.Kernel.deterministic (feedbackFun env n) ⋯

noncomputable def Learning.feedbackFunZero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] :

𝓞 × 𝓐 → 𝓨

The initial feedback function of a deterministic environment, as a function of the first observation and the first action.

Equations

Learning.feedbackFunZero env p = Learning.feedbackFun env 0 ((default , p.1), p.2)

Instances For

theorem Learning.measurable_feedbackFunZero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] :

Measurable (feedbackFunZero env)

theorem Learning.feedbackFun_zero {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] (h : Hist 𝓞 𝓐 𝓨 0) (o : 𝓞) (a : 𝓐) :

feedbackFun env 0 ((h, o), a) = feedbackFunZero env (o, a)

theorem Learning.ν0_eq_deterministic {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (env : Environment 𝓞 𝓐 𝓨) [IsDeterministicEnv env] :

env.ν0 = ProbabilityTheory.Kernel.deterministic (feedbackFunZero env) ⋯

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

ProbabilityTheory.HasCondDistrib (Y n) (fun (ω : Ω) => ((history O A Y n ω, O n ω), A n ω)) (ProbabilityTheory.Kernel.deterministic (feedbackFun env n) ⋯) P

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

ProbabilityTheory.HasCondDistrib (Y 0) (fun (ω : Ω) => (O 0 ω, A 0 ω)) (ProbabilityTheory.Kernel.deterministic (feedbackFunZero env) ⋯) P

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

Y n =ᵐ[P] fun (ω : Ω) => feedbackFun env n ((history O A Y n ω, O n ω), A n ω)

noncomputable def Learning.detAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐) (h_next : ∀ (n : ℕ), Measurable (nextA n)) :

Algorithm 𝓞 𝓐 𝓨

A deterministic algorithm, which chooses the action given by the function nextA. The initial action is fun o ↦ nextA 0 (default, o).

Equations

Learning.detAlgorithm nextA h_next = { policy := fun (n : ℕ) => ProbabilityTheory.Kernel.deterministic (nextA n) ⋯, isMarkovKernel_policy := ⋯ }

Instances For

@[simp]

theorem Learning.detAlgorithm_policy {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐) (h_next : ∀ (n : ℕ), Measurable (nextA n)) (n : ℕ) :

(detAlgorithm nextA h_next).policy n = ProbabilityTheory.Kernel.deterministic (nextA n) ⋯

instance Learning.instIsDeterministicAlgDetAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} :

IsDeterministicAlg (detAlgorithm nextA h_next)

@[simp]

theorem Learning.p0_detAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} :

(detAlgorithm nextA h_next).p0 = ProbabilityTheory.Kernel.deterministic (fun (o : 𝓞) => nextA 0 (default , o)) ⋯

@[simp]

theorem Learning.nextAction_detAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} [MeasurableSpace.SeparatesPoints 𝓐] (n : ℕ) :

nextAction (detAlgorithm nextA h_next) n = nextA n

@[simp]

theorem Learning.actionZero_detAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} [MeasurableSpace.SeparatesPoints 𝓐] :

actionZero (detAlgorithm nextA h_next) = fun (o : 𝓞) => nextA 0 (default , o)

noncomputable def Learning.detEnvironment {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} (obs : (n : ℕ) → ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (obs n)] (f : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐 → 𝓨) (hf : ∀ (n : ℕ), Measurable (f n)) :

Environment 𝓞 𝓐 𝓨

A deterministic environment, where the feedback is given by evaluating fixed measurable functions.

Equations

Learning.detEnvironment obs f hf = { obs := obs, feedback := fun (n : ℕ) => ProbabilityTheory.Kernel.deterministic (f n) ⋯, isMarkovKernel_obs := inst✝, isMarkovKernel_feedback := ⋯ }

Instances For

@[simp]

theorem Learning.obs_detEnvironment {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {obs : (n : ℕ) → ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞} [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (obs n)] {f : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐 → 𝓨} {hf : ∀ (n : ℕ), Measurable (f n)} (n : ℕ) :

(detEnvironment obs f hf).obs n = obs n

@[simp]

theorem Learning.feedback_detEnvironment {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {obs : (n : ℕ) → ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞} [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (obs n)] {f : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐 → 𝓨} {hf : ∀ (n : ℕ), Measurable (f n)} (n : ℕ) :

(detEnvironment obs f hf).feedback n = ProbabilityTheory.Kernel.deterministic (f n) ⋯

instance Learning.instIsDeterministicEnvDetEnvironment {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {obs : (n : ℕ) → ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞} [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (obs n)] {f : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐 → 𝓨} {hf : ∀ (n : ℕ), Measurable (f n)} :

IsDeterministicEnv (detEnvironment obs f hf)

@[simp]

theorem Learning.feedbackFun_detEnvironment {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {obs : (n : ℕ) → ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞} [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (obs n)] {f : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐 → 𝓨} {hf : ∀ (n : ℕ), Measurable (f n)} [MeasurableSpace.SeparatesPoints 𝓨] (n : ℕ) :

feedbackFun (detEnvironment obs f hf) n = f n

@[simp]

theorem Learning.feedbackFunZero_detEnvironment {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {obs : (n : ℕ) → ProbabilityTheory.Kernel (Hist 𝓞 𝓐 𝓨 n) 𝓞} [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (obs n)] {f : (n : ℕ) → (Hist 𝓞 𝓐 𝓨 n × 𝓞) × 𝓐 → 𝓨} {hf : ∀ (n : ℕ), Measurable (f n)} [MeasurableSpace.SeparatesPoints 𝓨] :

feedbackFunZero (detEnvironment obs f hf) = fun (p : 𝓞 × 𝓐) => f 0 ((default , p.1), p.2)

theorem Learning.IsAlgEnvSeq.hasCondDistrib_action_zero_detAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} {env : Environment 𝓞 𝓐 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} (h : IsAlgEnvSeq O A Y (detAlgorithm nextA h_next) env P) :

ProbabilityTheory.HasCondDistrib (A 0) (O 0) (ProbabilityTheory.Kernel.deterministic (fun (o : 𝓞) => nextA 0 (default , o)) ⋯) P

theorem Learning.IsAlgEnvSeq.action_detAlgorithm_ae_eq {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} {env : Environment 𝓞 𝓐 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [MeasurableEq 𝓐] (h : IsAlgEnvSeq O A Y (detAlgorithm nextA h_next) env P) (n : ℕ) :

A n =ᵐ[P] fun (ω : Ω) => nextA n (history O A Y n ω, O n ω)

theorem Learning.IsAlgEnvSeq.action_zero_detAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} {env : Environment 𝓞 𝓐 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [MeasurableEq 𝓐] (h : IsAlgEnvSeq O A Y (detAlgorithm nextA h_next) env P) :

A 0 =ᵐ[P] fun (ω : Ω) => nextA 0 (default , O 0 ω)

theorem Learning.IsAlgEnvSeq.action_detAlgorithm_ae_all_eq {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} {env : Environment 𝓞 𝓐 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} [MeasurableEq 𝓐] (h : IsAlgEnvSeq O A Y (detAlgorithm nextA h_next) env P) :

∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), A n ω = nextA n (history O A Y n ω, O n ω)

theorem Learning.IsAlgEnvSeqUntil.hasCondDistrib_action_zero_detAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} {env : Environment 𝓞 𝓐 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {N : ℕ} (h : IsAlgEnvSeqUntil O A Y (detAlgorithm nextA h_next) env P N) (hN : 0 < N) :

ProbabilityTheory.HasCondDistrib (A 0) (O 0) (ProbabilityTheory.Kernel.deterministic (fun (o : 𝓞) => nextA 0 (default , o)) ⋯) P

theorem Learning.IsAlgEnvSeqUntil.action_detAlgorithm_ae_eq {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} {env : Environment 𝓞 𝓐 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {N n : ℕ} [MeasurableEq 𝓐] (h : IsAlgEnvSeqUntil O A Y (detAlgorithm nextA h_next) env P N) (hn : n < N) :

A n =ᵐ[P] fun (ω : Ω) => nextA n (history O A Y n ω, O n ω)

theorem Learning.IsAlgEnvSeqUntil.action_zero_detAlgorithm {𝓞 : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {m𝓞 : MeasurableSpace 𝓞} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {nextA : (n : ℕ) → Hist 𝓞 𝓐 𝓨 n × 𝓞 → 𝓐} {h_next : ∀ (n : ℕ), Measurable (nextA n)} {env : Environment 𝓞 𝓐 𝓨} {Ω : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {O : ℕ → Ω → 𝓞} {A : ℕ → Ω → 𝓐} {Y : ℕ → Ω → 𝓨} {N : ℕ} [MeasurableEq 𝓐] (h : IsAlgEnvSeqUntil O A Y (detAlgorithm nextA h_next) env P N) (hN : 0 < N) :

A 0 =ᵐ[P] fun (ω : Ω) => nextA 0 (default , O 0 ω)