Algorithms

structure Learning.Algorithm (α : Type u_4) (R : Type u_5) [MeasurableSpace α] [MeasurableSpace R] : Type (max u_4 u_5)

A stochastic, sequential algorithm.

• policy (n : ℕ) : ProbabilityTheory.Kernel (↥(Finset.Iic n) → α × R) α

  Policy or sampling rule: distribution of the next action.

• h_policy (n : ℕ) : ProbabilityTheory.IsMarkovKernel (self.policy n)
• p0 : MeasureTheory.Measure α

  Distribution of the first action.

• hp0 : MeasureTheory.IsProbabilityMeasure self.p0

instance Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (alg : Algorithm α R) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (alg.policy n)

instance Learning.instIsProbabilityMeasureP0 {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (alg : Algorithm α R) : MeasureTheory.IsProbabilityMeasure alg.p0

structure Learning.Environment (α : Type u_4) (R : Type u_5) [MeasurableSpace α] [MeasurableSpace R] : Type (max u_4 u_5)

A stochastic environment.

• feedback (n : ℕ) : ProbabilityTheory.Kernel ((↥(Finset.Iic n) → α × R) × α) R

  Distribution of the next observation as function of the past history.

• h_feedback (n : ℕ) : ProbabilityTheory.IsMarkovKernel (self.feedback n)
• ν0 : ProbabilityTheory.Kernel α R

  Distribution of the first observation given the first action.

• hp0 : ProbabilityTheory.IsMarkovKernel self.ν0

instance Learning.instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedback {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (env : Environment α R) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (env.feedback n)

instance Learning.instIsMarkovKernelν0 {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (env : Environment α R) : ProbabilityTheory.IsMarkovKernel env.ν0

noncomputable def Learning.stepKernel {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : ProbabilityTheory.Kernel (↥(Finset.Iic n) → α × R) (α × R)

Kernel describing the distribution of the next action-reward pair given the history up to n.

Equations

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

instance Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdStepKernel {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (stepKernel alg env n)

Equations

• ⋯ = ⋯

@[simp]

theorem Learning.fst_stepKernel {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : (stepKernel alg env n).fst = alg.policy n

def Learning.IsAlgEnvSeq.step {α : Type u_1} {R : Type u_2} {Ω : Type u_3} (A : ℕ → Ω → α) (R' : ℕ → Ω → R) (n : ℕ) (ω : Ω) : α × R

Step of the algorithm-environment sequence: the action-reward pair at time n.

Equations

• Learning.IsAlgEnvSeq.step A R' n ω = (A n ω, R' n ω)

theorem Learning.IsAlgEnvSeq.measurable_step {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} (n : ℕ) (hA : Measurable (A n)) (hR' : Measurable (R' n)) : Measurable (step A R' n)

def Learning.IsAlgEnvSeq.hist {α : Type u_1} {R : Type u_2} {Ω : Type u_3} (A : ℕ → Ω → α) (R' : ℕ → Ω → R) (n : ℕ) (ω : Ω) : ↥(Finset.Iic n) → α × R

History of the algorithm-environment sequence up to time n.

Equations

• Learning.IsAlgEnvSeq.hist A R' n ω i = (A (↑i) ω, R' (↑i) ω)

theorem Learning.IsAlgEnvSeq.measurable_hist {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} (hA : ∀ (n : ℕ), Measurable (A n)) (hR' : ∀ (n : ℕ), Measurable (R' n)) (n : ℕ) : Measurable (hist A R' n)

theorem Learning.IsAlgEnvSeq.eval_comp_hist {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} (n : ℕ) : (fun (x : ↥(Finset.Iic n) → α × R) => x ⟨n, ⋯⟩) ∘ hist A R' n = step A R' n

theorem Learning.IsAlgEnvSeq.fst_eval_comp_hist {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} (n : ℕ) : (fun (x : ↥(Finset.Iic n) → α × R) => (x ⟨n, ⋯⟩).1) ∘ hist A R' n = A n

theorem Learning.IsAlgEnvSeq.snd_eval_comp_hist {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} (n : ℕ) : (fun (x : ↥(Finset.Iic n) → α × R) => (x ⟨n, ⋯⟩).2) ∘ hist A R' n = R' n

structure Learning.IsAlgEnvSeq {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (A : ℕ → Ω → α) (R' : ℕ → Ω → R) (alg : Algorithm α R) (env : Environment α R) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure P] : Prop

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

• measurable_A (n : ℕ) : Measurable (A n)
• measurable_R (n : ℕ) : Measurable (R' n)
• hasLaw_action_zero : ProbabilityTheory.HasLaw (fun (ω : Ω) => A 0 ω) alg.p0 P
• hasCondDistrib_reward_zero : ProbabilityTheory.HasCondDistrib (R' 0) (A 0) env.ν0 P
• hasCondDistrib_action (n : ℕ) : ProbabilityTheory.HasCondDistrib (A (n + 1)) (hist A R' n) (alg.policy n) P
• hasCondDistrib_reward (n : ℕ) : ProbabilityTheory.HasCondDistrib (R' (n + 1)) (fun (ω : Ω) => (hist A R' n ω, A (n + 1) ω)) (env.feedback n) P

theorem Learning.IsAlgEnvSeq.hasLaw_step_zero {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {alg : Algorithm α R} {env : Environment α R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (h : IsAlgEnvSeq A R' alg env P) : ProbabilityTheory.HasLaw (step A R' 0) (alg.p0.compProd env.ν0) P

theorem Learning.IsAlgEnvSeq.hasCondDistrib_step {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {alg : Algorithm α R} {env : Environment α R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) : ProbabilityTheory.HasCondDistrib (step A R' (n + 1)) (hist A R' n) (stepKernel alg env n) P

def Learning.IsAlgEnvSeq.filtration {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} (hA : ∀ (n : ℕ), Measurable (A n)) (hR' : ∀ (n : ℕ), Measurable (R' n)) : MeasureTheory.Filtration ℕ mΩ

Filtration generated by the history up to time n.

Equations

• Learning.IsAlgEnvSeq.filtration hA hR' = { seq := fun (i : ℕ) => MeasurableSpace.comap (Learning.IsAlgEnvSeq.hist A R' i) inferInstance, mono' := ⋯, le' := ⋯ }

theorem Learning.IsAlgEnvSeq.measurable_action_filtration {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} (hA : ∀ (n : ℕ), Measurable (A n)) (hR' : ∀ (n : ℕ), Measurable (R' n)) (n : ℕ) : Measurable (A n)

def Learning.IsAlgEnvSeq.filtrationAction {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} (hA : ∀ (n : ℕ), Measurable (A n)) (hR' : ∀ (n : ℕ), Measurable (R' n)) : MeasureTheory.Filtration ℕ mΩ

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.IsAlgEnvSeq.filtrationAction_zero_eq_comap {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {hA : ∀ (n : ℕ), Measurable (A n)} {hR' : ∀ (n : ℕ), Measurable (R' n)} : ↑(filtrationAction hA hR') 0 = MeasurableSpace.comap (A 0) inferInstance

theorem Learning.IsAlgEnvSeq.filtrationAction_eq_comap {α : Type u_1} {R : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {mΩ : MeasurableSpace Ω} {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {hA : ∀ (n : ℕ), Measurable (A n)} {hR' : ∀ (n : ℕ), Measurable (R' n)} (n : ℕ) (hn : n ≠ 0) : ↑(filtrationAction hA hR') n = MeasurableSpace.comap (fun (ω : Ω) => (hist A R' (n - 1) ω, A n ω)) inferInstance

noncomputable def Learning.traj {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : ProbabilityTheory.Kernel (↥(Finset.Iic n) → α × R) (ℕ → α × R)

Kernel sending a partial trajectory of the bandit Seq Iic n → α × ℝ to a measure on ℕ → α × ℝ, supported on full trajectories that start with the partial one.

Equations

• Learning.traj alg env n = ProbabilityTheory.Kernel.traj (Learning.stepKernel alg env) n

instance Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdForallTraj {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (traj alg env n)

Equations

• ⋯ = ⋯

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

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} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} (alg : Algorithm α R) (env : Environment α R) : MeasureTheory.IsProbabilityMeasure (trajMeasure alg env)

Equations

• ⋯ = ⋯

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

theorem Learning.isAlgEnvSeq_unique {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} {mR : MeasurableSpace R} {Ω : Type u_4} {Ω' : Type u_5} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] {alg : Algorithm α R} {env : Environment α R} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {A₁ : ℕ → Ω → α} {R₁ : ℕ → Ω → R} {A₂ : ℕ → Ω' → α} {R₂ : ℕ → Ω' → 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'