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
Instances For
instance
Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
(alg : Algorithm α R)
(n : ℕ)
:
instance
Learning.instIsProbabilityMeasureP0
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
(alg : Algorithm α R)
:
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
Instances For
instance
Learning.instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedback
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
(env : Environment α R)
(n : ℕ)
:
instance
Learning.instIsMarkovKernelν0
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
(env : Environment α R)
:
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)
Instances For
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 : ℕ)
:
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) ω)
Instances For
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)
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]
:
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
Instances For
structure
Learning.IsAlgEnvSeqUntil
{α : 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]
(N : ℕ)
:
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 : ℕ) (hn : n < N) : ProbabilityTheory.HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A R' n) (alg.policy n) P
- hasCondDistrib_reward (n : ℕ) (hn : n < N) : ProbabilityTheory.HasCondDistrib (R' (n + 1)) (fun (ω : Ω) => (IsAlgEnvSeq.hist A R' n ω, A (n + 1) ω)) (env.feedback n) P
Instances For
theorem
Learning.IsAlgEnvSeqUntil.mono
{α : 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]
{N : ℕ}
[StandardBorelSpace α]
[Nonempty α]
[StandardBorelSpace R]
[Nonempty R]
(h : IsAlgEnvSeqUntil A R' alg env P N)
{N' : ℕ}
(hN : N' ≤ N)
:
IsAlgEnvSeqUntil A R' alg env P N'
theorem
Learning.IsAlgEnvSeq.isAlgEnvSeqUntil
{α : 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 : ℕ)
:
IsAlgEnvSeqUntil A R' alg env P N
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.IsAlgEnvSeqUntil.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]
{N : ℕ}
[StandardBorelSpace α]
[Nonempty α]
[StandardBorelSpace R]
[Nonempty R]
(h : IsAlgEnvSeqUntil A R' alg env P N)
:
ProbabilityTheory.HasLaw (IsAlgEnvSeq.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
theorem
Learning.IsAlgEnvSeqUntil.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]
{N : ℕ}
[StandardBorelSpace α]
[Nonempty α]
[StandardBorelSpace R]
[Nonempty R]
(h : IsAlgEnvSeqUntil A R' alg env P N)
(n : ℕ)
(hn : n < N)
:
ProbabilityTheory.HasCondDistrib (IsAlgEnvSeq.step A R' (n + 1)) (IsAlgEnvSeq.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))
:
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' := ⋯ }
Instances For
theorem
Learning.IsAlgEnvSeq.adapted_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))
:
MeasureTheory.Adapted (filtration hA hR') (hist A R')
theorem
Learning.IsAlgEnvSeq.adapted_step
{α : 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.Adapted (filtration hA hR') (step A R')
theorem
Learning.IsAlgEnvSeq.adapted_action
{α : 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.Adapted (filtration hA hR') A
theorem
Learning.IsAlgEnvSeq.adapted_reward
{α : 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.Adapted (filtration hA hR') R'
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))
:
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.
Instances For
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)}
:
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
Instances For
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)
Instances For
instance
Learning.instIsProbabilityMeasureForallNatProdTrajMeasure
{α : Type u_1}
{R : Type u_2}
{mα : MeasurableSpace α}
{mR : MeasurableSpace R}
(alg : Algorithm α R)
(env : Environment α R)
:
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)
:
theorem
Learning.eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil
{α : 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}
{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}
{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')
:
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}
{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}
{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'