Bandit

def MeasurableEquiv.piIicZero (α : Type u_1) [MeasurableSpace α] : ({ x : ℕ // x ∈ Finset.Iic 0 } → α) ≃ᵐ α

Measurable equivalence between Iic 0 → α and α.

Equations

• MeasurableEquiv.piIicZero α = MeasurableEquiv.funUnique { x : ℕ // x ∈ Finset.Iic 0 } α

structure Bandits.Bandit (α : Type u_2) [MeasurableSpace α] : Type u_2

A bandit interaction between an agent described by a policy and an environment given by reward distributions.

• ν : ProbabilityTheory.Kernel α ℝ

  Conditional distribution of the rewards given the arm pulled.

• hν : ProbabilityTheory.IsMarkovKernel self.ν
• policy (n : ℕ) : ProbabilityTheory.Kernel ({ x : ℕ // x ∈ Finset.Iic n } → α × ℝ) α

  Policy or sampling rule: distribution of the next pull.

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

  Distribution of the first pull.

• hp0 : MeasureTheory.IsProbabilityMeasure self.p0

instance Bandits.instIsMarkovKernelRealν {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) : ProbabilityTheory.IsMarkovKernel b.ν

instance Bandits.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdRealPolicy {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (b.policy n)

instance Bandits.instIsProbabilityMeasureP0 {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) : MeasureTheory.IsProbabilityMeasure b.p0

noncomputable def Bandits.Bandit.stepKernel {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) (n : ℕ) : ProbabilityTheory.Kernel ({ x : ℕ // x ∈ Finset.Iic n } → α × ℝ) (α × ℝ)

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

Equations

• b.stepKernel n = (b.policy n).compProd (ProbabilityTheory.Kernel.prodMkLeft ({ x : ℕ // x ∈ Finset.Iic n } → α × ℝ) b.ν)

instance Bandits.Bandit.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdRealStepKernel {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (b.stepKernel n)

@[simp]

theorem Bandits.Bandit.fst_stepKernel {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) (n : ℕ) : (b.stepKernel n).fst = b.policy n

@[simp]

theorem Bandits.Bandit.snd_stepKernel {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) (n : ℕ) : (b.stepKernel n).snd = b.ν.comp (b.policy n)

noncomputable def Bandits.Bandit.traj {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) (n : ℕ) : ProbabilityTheory.Kernel ({ x : ℕ // x ∈ Finset.Iic n } → α × ℝ) (ℕ → α × ℝ)

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

Equations

• b.traj n = ProbabilityTheory.Kernel.traj b.stepKernel n

instance Bandits.Bandit.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdRealForallTraj {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) (n : ℕ) : ProbabilityTheory.IsMarkovKernel (b.traj n)

noncomputable def Bandits.Bandit.measure {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) : MeasureTheory.Measure (ℕ → α × ℝ)

Measure on the sequence of arms pulled and rewards observed generated by the bandit.

Equations

• b.measure = (MeasureTheory.Measure.map (⇑(MeasurableEquiv.piIicZero (α × ℝ)).symm) (b.p0.compProd b.ν)).bind ⇑(b.traj 0)

instance Bandits.Bandit.instIsProbabilityMeasureForallNatProdRealMeasure {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) : MeasureTheory.IsProbabilityMeasure b.measure

def Bandits.arm {α : Type u_1} (n : ℕ) (h : ℕ → α × ℝ) : α

arm n is the arm pulled at time n. This is a random variable on the measurable space ℕ → α × ℝ.

Equations

• Bandits.arm n h = (h n).1

def Bandits.reward {α : Type u_1} (n : ℕ) (h : ℕ → α × ℝ) : ℝ

reward n is the reward at time n. This is a random variable on the measurable space ℕ → α × ℝ.

Equations

• Bandits.reward n h = (h n).2

def Bandits.hist {α : Type u_1} (n : ℕ) (h : ℕ → α × ℝ) : { x : ℕ // x ∈ Finset.Iic n } → α × ℝ

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

Equations

• Bandits.hist n h i = h ↑i

def Bandits.ℱ (α : Type u_2) [MeasurableSpace α] : MeasureTheory.Filtration ℕ inferInstance

Equations

• Bandits.ℱ α = MeasureTheory.Filtration.piLE

theorem Bandits.condDistrib_arm_reward {α : Type u_1} {mα : MeasurableSpace α} [StandardBorelSpace α] [Nonempty α] (b : Bandit α) (n : ℕ) : ProbabilityTheory.condDistrib (fun (h : ℕ → α × ℝ) => (arm n h, reward n h)) (hist n) b.measure = b.stepKernel n

theorem Bandits.condDistrib_reward {α : Type u_1} {mα : MeasurableSpace α} (b : Bandit α) (n : ℕ) : ProbabilityTheory.condDistrib (reward n) (arm n) b.measure = b.ν

theorem Bandits.condDistrib_arm {α : Type u_1} {mα : MeasurableSpace α} [StandardBorelSpace α] [Nonempty α] (b : Bandit α) (n : ℕ) : ProbabilityTheory.condDistrib (arm n) (hist n) b.measure = b.policy n