Array-of-rewards probability space for stochastic bandits

We build a particular probability space for stochastic bandits, called the "array model", in which an infinite array of i.i.d. rewards is first produced for all actions. When the algorithm chooses action a for the nth time, it receives the reward in the row a of the array and column n.

Some statements about bandit algorithms are easier to prove in this space, and can then be transferred to any other probability space using the fact that the conditional distributions of the arms and rewards specified in the bandit model determine their laws uniquely.

Main definitions

• streamMeasure ν: probability measure on the space of infinite arrays of rewards, where the rewards in each row are i.i.d. according to ν.
• probSpace 𝓐 𝓡: probability space for the array model of stochastic bandits with action space 𝓐 and reward space 𝓡.
• arrayMeasure ν: probability measure on probSpace 𝓐 𝓡 for the array model of stochastic bandits with reward kernel ν.

noncomputable def Bandits.streamMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) : MeasureTheory.Measure (ℕ → 𝓐 → 𝓡)

Measure of an infinite stream of rewards from each action.

Equations

• Bandits.streamMeasure ν = MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.Measure.infinitePi ⇑ν

instance Bandits.instIsProbabilityMeasureForallNatForallStreamMeasureOfIsMarkovKernel {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : MeasureTheory.IsProbabilityMeasure (streamMeasure ν)

theorem Bandits.hasLaw_eval_streamMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.HasLaw (fun (h : ℕ → 𝓐 → 𝓡) => h n) (MeasureTheory.Measure.infinitePi ⇑ν) (streamMeasure ν)

theorem Bandits.hasLaw_eval_eval_streamMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : ProbabilityTheory.HasLaw (fun (h : ℕ → 𝓐 → 𝓡) => h n a) (ν a) (streamMeasure ν)

theorem Bandits.hasLaw_snd_apply_prod_streamMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : ProbabilityTheory.HasLaw (fun (ω : Ω × (ℕ → 𝓐 → 𝓡)) => ω.2 n a) (ν a) (μ.prod (streamMeasure ν))

Under a product measure μ.prod (streamMeasure ν), the entry (n, a) of the reward array has law ν a.

theorem Bandits.identDistrib_eval_eval_id_streamMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : ProbabilityTheory.IdentDistrib (fun (h : ℕ → 𝓐 → 𝓡) => h n a) id (streamMeasure ν) (ν a)

theorem Bandits.integrable_eval_streamMeasure {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} (ν : ProbabilityTheory.Kernel 𝓐 ℝ) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) (a : 𝓐) (h_int : MeasureTheory.Integrable id (ν a)) : MeasureTheory.Integrable (fun (h : ℕ → 𝓐 → ℝ) => h n a) (streamMeasure ν)

theorem Bandits.integral_eval_streamMeasure {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} (ν : ProbabilityTheory.Kernel 𝓐 ℝ) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : ∫ (h : ℕ → 𝓐 → ℝ), h n a ∂streamMeasure ν = ∫ (x : ℝ), id x ∂ν a

theorem Bandits.iIndepFun_eval_streamMeasure' {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : ProbabilityTheory.iIndepFun (fun (n : ℕ) (ω : ℕ → 𝓐 → 𝓡) => ω n) (streamMeasure ν)

theorem Bandits.iIndepFun_eval_streamMeasure'' {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) : ProbabilityTheory.iIndepFun (fun (n : ℕ) (ω : ℕ → 𝓐 → 𝓡) => ω n a) (streamMeasure ν)

theorem Bandits.iIndepFun_eval_streamMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : ProbabilityTheory.iIndepFun (fun (p : ℕ × 𝓐) (ω : ℕ → 𝓐 → 𝓡) => ω p.1 p.2) (streamMeasure ν)

theorem Bandits.indepFun_eval_streamMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] {n m : ℕ} {a b : 𝓐} (h : n ≠ m ∨ a ≠ b) : ProbabilityTheory.IndepFun (fun (ω : ℕ → 𝓐 → 𝓡) => ω n a) (fun (ω : ℕ → 𝓐 → 𝓡) => ω m b) (streamMeasure ν)

theorem Bandits.indepFun_eval_streamMeasure' {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] {a b : 𝓐} (h : a ≠ b) : ProbabilityTheory.IndepFun (fun (ω : ℕ → 𝓐 → 𝓡) (n : ℕ) => ω n a) (fun (ω : ℕ → 𝓐 → 𝓡) (n : ℕ) => ω n b) (streamMeasure ν)

theorem Bandits.iIndepFun_snd_apply_prod_streamMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : ProbabilityTheory.iIndepFun (fun (p : ℕ × 𝓐) (ω : Ω × (ℕ → 𝓐 → 𝓡)) => ω.2 p.1 p.2) (μ.prod (streamMeasure ν))

Under a product measure μ.prod (streamMeasure ν), the entries of the reward array are independent.

theorem Bandits.indepFun_snd_apply_prod_streamMeasure_update {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [DecidableEq 𝓐] {Ω : Type u_3} {mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (m : ℕ) (a : 𝓐) (x : 𝓡) : ProbabilityTheory.IndepFun (fun (ω : Ω × (ℕ → 𝓐 → 𝓡)) => ω.2 m a) (fun (ω : Ω × (ℕ → 𝓐 → 𝓡)) => (ω.1, fun (i : ℕ) (b : 𝓐) => if i = m ∧ b = a then x else ω.2 i b)) (μ.prod (streamMeasure ν))

Under a product measure μ.prod (streamMeasure ν), the entry (m, a) of the reward array is independent of the pair formed by the first coordinate and the reward array in which the entry (m, a) is replaced by a constant x.

@[reducible, inline]

abbrev Bandits.ArrayModel.probSpace (𝓐 : Type u_1) (𝓡 : Type u_2) : Type (max u_1 u_2)

Probability space for the array model of stochastic bandits.

Equations

• Bandits.ArrayModel.probSpace 𝓐 𝓡 = ((ℕ → ↑unitInterval) × (ℕ → 𝓐 → 𝓡))

noncomputable def Bandits.ArrayModel.arrayMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) : MeasureTheory.Measure (probSpace 𝓐 𝓡)

Probability measure for the array model of stochastic bandits.

Equations

• Bandits.ArrayModel.arrayMeasure ν = (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume).prod (Bandits.streamMeasure ν)

instance Bandits.ArrayModel.instIsProbabilityMeasureProbSpaceArrayMeasureOfIsMarkovKernel {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : MeasureTheory.IsProbabilityMeasure (arrayMeasure ν)

theorem Bandits.ArrayModel.hasLaw_fst_apply_arrayMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.HasLaw (fun (ω : probSpace 𝓐 𝓡) => ω.1 n) MeasureTheory.volume (arrayMeasure ν)

theorem Bandits.ArrayModel.hasLaw_snd_apply_arrayMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : ProbabilityTheory.HasLaw (fun (ω : probSpace 𝓐 𝓡) => ω.2 n a) (ν a) (arrayMeasure ν)

theorem Bandits.ArrayModel.map_snd_apply_arrayMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} {ν : ProbabilityTheory.Kernel 𝓐 𝓡} [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) (a : 𝓐) : MeasureTheory.Measure.map (fun (ω : probSpace 𝓐 𝓡) => ω.2 n a) (arrayMeasure ν) = ν a

def Bandits.ArrayModel.truncRow {𝓐 : Type u_1} {𝓡 : Type u_2} [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) (ω : probSpace 𝓐 𝓡) : probSpace 𝓐 𝓡

Modification of ω in which the rewards of action a are read only up to index m - 1: in row a of the reward array, the entry at index i is kept if i < m and replaced by the entry at index m + 1 + i otherwise. The result does not depend on the coordinate (m, a) of the array.

Equations

• Bandits.ArrayModel.truncRow a m ω = (ω.1, fun (i : ℕ) (b : 𝓐) => if b = a then ω.2 (if i < m then i else m + 1 + i) b else ω.2 i b)

theorem Bandits.ArrayModel.measurable_truncRow {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓡 : MeasurableSpace 𝓡} [DecidableEq 𝓐] (a : 𝓐) (m : ℕ) : Measurable (truncRow a m)

noncomputable def Bandits.ArrayModel.algFunction {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : Learning.Hist Unit 𝓐 𝓡 n → ↑unitInterval → 𝓐

The next action is the image of the history and a uniform random variable by this function.

Equations

• Bandits.ArrayModel.algFunction alg n = ⋯.choose

theorem Bandits.ArrayModel.algFunction_map {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) (h : Learning.Hist Unit 𝓐 𝓡 n) : MeasureTheory.Measure.map (algFunction alg n h) MeasureTheory.volume = (alg.policy n) (h, ())

theorem Bandits.ArrayModel.algFunction_zero_map {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) : MeasureTheory.Measure.map (algFunction alg 0 default) MeasureTheory.volume = alg.p0 ()

The initial action is the image of a uniform random variable by algFunction alg 0 default.

theorem Bandits.ArrayModel.measurable_algFunction {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : Measurable (Function.uncurry (algFunction alg n))

noncomputable def Bandits.ArrayModel.hist {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : Learning.Hist Unit 𝓐 𝓡 n

History of actions and rewards before time n in the array model.

Equations

• One or more equations did not get rendered due to their size.
• Bandits.ArrayModel.hist alg ω 0 = default

@[simp]

theorem Bandits.ArrayModel.hist_zero {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) : hist alg ω 0 = default

theorem Bandits.ArrayModel.hist_add_one {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω (n + 1) = Fin.snoc (hist alg ω n) ((), algFunction alg n (hist alg ω n) (ω.1 n), ω.2 (Learning.pullCount' n (hist alg ω n) (algFunction alg n (hist alg ω n) (ω.1 n))) (algFunction alg n (hist alg ω n) (ω.1 n)))

theorem Bandits.ArrayModel.hist_add_one_eq_finSuccProd' {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω (n + 1) = (MeasurableEquiv.finSuccProd (Learning.Round Unit 𝓐 𝓡) n).symm (hist alg ω n, (), algFunction alg n (hist alg ω n) (ω.1 n), ω.2 (Learning.pullCount' n (hist alg ω n) (algFunction alg n (hist alg ω n) (ω.1 n))) (algFunction alg n (hist alg ω n) (ω.1 n)))

noncomputable def Bandits.ArrayModel.action {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) (ω : probSpace 𝓐 𝓡) : 𝓐

Action taken at time n in the array model.

Equations

• Bandits.ArrayModel.action alg n ω = Bandits.ArrayModel.algFunction alg n (Bandits.ArrayModel.hist alg ω n) (ω.1 n)

theorem Bandits.ArrayModel.action_eq {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : action alg n = fun (ω : probSpace 𝓐 𝓡) => algFunction alg n (hist alg ω n) (ω.1 n)

theorem Bandits.ArrayModel.action_zero {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) : action alg 0 = fun (ω : probSpace 𝓐 𝓡) => algFunction alg 0 default (ω.1 0)

noncomputable def Bandits.ArrayModel.reward {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) (ω : probSpace 𝓐 𝓡) : 𝓡

Reward received at time n in the array model.

Equations

• Bandits.ArrayModel.reward alg n ω = (Bandits.ArrayModel.hist alg ω (n + 1) (Fin.last n)).feedback

theorem Bandits.ArrayModel.reward_eq' {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) (ω : probSpace 𝓐 𝓡) : reward alg n ω = ω.2 (Learning.pullCount' n (hist alg ω n) (action alg n ω)) (action alg n ω)

theorem Bandits.ArrayModel.hist_succ {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω (n + 1) = Fin.snoc (hist alg ω n) ((), action alg n ω, reward alg n ω)

theorem Bandits.ArrayModel.hist_succ_eq_finSuccProd {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω (n + 1) = (MeasurableEquiv.finSuccProd (Learning.Round Unit 𝓐 𝓡) n).symm (hist alg ω n, (), action alg n ω, reward alg n ω)

theorem Bandits.ArrayModel.hist_apply_last {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω (n + 1) (Fin.last n) = ((), action alg n ω, reward alg n ω)

theorem Bandits.ArrayModel.hist_eq {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω n = fun (i : Fin n) => ((), action alg (↑i) ω, reward alg (↑i) ω)

theorem Bandits.ArrayModel.hist_eq_history {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ω : probSpace 𝓐 𝓡) (n : ℕ) : hist alg ω n = Learning.history (Learning.noObs (probSpace 𝓐 𝓡)) (action alg) (reward alg) n ω

The history in the array model is the history of the action and reward processes.

theorem Bandits.ArrayModel.pullCount_action_eq {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (n : ℕ) (ω : probSpace 𝓐 𝓡) : Learning.pullCount (action alg) a n ω = Learning.pullCount' n (hist alg ω n) a

theorem Bandits.ArrayModel.pullCount_action_eq_comp {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (n : ℕ) : Learning.pullCount (action alg) a n = (fun (h : Learning.Hist Unit 𝓐 𝓡 n) => Learning.pullCount' n h a) ∘ fun (x : probSpace 𝓐 𝓡) => hist alg x n

theorem Bandits.ArrayModel.reward_eq {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : reward alg n = fun (ω : probSpace 𝓐 𝓡) => ω.2 (Learning.pullCount (action alg) (action alg n ω) n ω) (action alg n ω)

theorem Bandits.ArrayModel.sumRewards_eq {𝓐 : Type u_1} {m𝓐 : MeasurableSpace 𝓐} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 ℝ) (a : 𝓐) (n : ℕ) (ω : probSpace 𝓐 ℝ) : Learning.sumRewards (action alg) (reward alg) a n ω = ∑ i ∈ Finset.range (Learning.pullCount (action alg) a n ω), ω.2 i a

theorem Bandits.ArrayModel.measurable_action' {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] {alg : Learning.Algorithm Unit 𝓐 𝓡} (n : ℕ) (h : Measurable fun (x : probSpace 𝓐 𝓡) => hist alg x n) : Measurable fun (x : probSpace 𝓐 𝓡) => algFunction alg n (hist alg x n) (x.1 n)

theorem Bandits.ArrayModel.measurable_pullCount'_action {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] {alg : Learning.Algorithm Unit 𝓐 𝓡} (n : ℕ) (h_hist : Measurable fun (x : probSpace 𝓐 𝓡) => hist alg x n) : Measurable fun (x : probSpace 𝓐 𝓡) => Learning.pullCount' n (hist alg x n) (algFunction alg n (hist alg x n) (x.1 n))

theorem Bandits.ArrayModel.measurable_hist {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : Measurable fun (ω : probSpace 𝓐 𝓡) => hist alg ω n

theorem Bandits.ArrayModel.measurable_action {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : Measurable (action alg n)

theorem Bandits.ArrayModel.measurable_reward {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : Measurable (reward alg n)

theorem Bandits.ArrayModel.measurable_pullCount_action {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : Measurable fun (ω : probSpace 𝓐 𝓡) => Learning.pullCount (action alg) (action alg n ω) n ω

theorem Bandits.ArrayModel.hist_congr {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) {ω ω' : probSpace 𝓐 𝓡} (hω1 : ∀ i < n, ω.1 i = ω'.1 i) (hω2 : ∀ (i : ℕ) (a : 𝓐), i < Learning.pullCount (action alg) a n ω → ω.2 i a = ω'.2 i a) : hist alg ω n = hist alg ω' n

theorem Bandits.ArrayModel.action_eq_and_pullCount_eq_congr_aux {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (m n : ℕ) {ω ω' : probSpace 𝓐 𝓡} (hω1 : ∀ (i : ℕ), ω.1 i = ω'.1 i) (hω2_ne : ∀ (i : ℕ) (b : 𝓐), b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ (i : ℕ), i + 1 ≤ m → ω.2 i a = ω'.2 i a) (h_eq : action alg n ω = a ∧ Learning.pullCount (action alg) a n ω = m) : action alg n ω' = a ∧ Learning.pullCount (action alg) a n ω' = m

theorem Bandits.ArrayModel.action_eq_and_pullCount_eq_congr {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (m n : ℕ) {ω ω' : probSpace 𝓐 𝓡} (hω1 : ∀ (i : ℕ), ω.1 i = ω'.1 i) (hω2_ne : ∀ (i : ℕ) (b : 𝓐), b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ (i : ℕ), i + 1 ≤ m → ω.2 i a = ω'.2 i a) : action alg n ω = a ∧ Learning.pullCount (action alg) a n ω = m ↔ action alg n ω' = a ∧ Learning.pullCount (action alg) a n ω' = m

theorem Bandits.ArrayModel.indicator_action_eq_and_pullCount_eq_congr {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (m n : ℕ) {ω ω' : probSpace 𝓐 𝓡} (hω1 : ∀ (i : ℕ), ω.1 i = ω'.1 i) (hω2_ne : ∀ (i : ℕ) (b : 𝓐), b ≠ a → ω.2 i b = ω'.2 i b) (hω2_eq : ∀ (i : ℕ), i + 1 ≤ m → ω.2 i a = ω'.2 i a) : {ω : probSpace 𝓐 𝓡 | action alg n ω = a ∧ Learning.pullCount (action alg) a n ω = m}.indicator (fun (x : probSpace 𝓐 𝓡) => 1) ω = {ω : probSpace 𝓐 𝓡 | action alg n ω = a ∧ Learning.pullCount (action alg) a n ω = m}.indicator (fun (x : probSpace 𝓐 𝓡) => 1) ω'

theorem Bandits.ArrayModel.measurable_hist_comap {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : Measurable fun (x : probSpace 𝓐 𝓡) => hist alg x n

noncomputable def Bandits.ArrayModel.truncRowPullCount {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (n : ℕ) (ω : probSpace 𝓐 𝓡) : probSpace 𝓐 𝓡

truncRow at the number of pulls of a before time n: the rewards of action a that have not been observed before time n are replaced. The history before time n is measurable with respect to this function (see measurable_hist_truncRowPullCount), and on the event pullCount (action alg) a n = m it coincides with truncRow a m.

Equations

• Bandits.ArrayModel.truncRowPullCount alg a n ω = Bandits.ArrayModel.truncRow a (Learning.pullCount (Bandits.ArrayModel.action alg) a n ω) ω

theorem Bandits.ArrayModel.measurable_hist_truncRowPullCount {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (n : ℕ) : Measurable fun (x : probSpace 𝓐 𝓡) => hist alg x n

theorem Bandits.ArrayModel.measurableSet_action_eq_and_pullCount_eq {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (n m : ℕ) : MeasurableSet {ω : probSpace 𝓐 𝓡 | action alg n ω = a ∧ Learning.pullCount (action alg) a n ω = m}

theorem Bandits.ArrayModel.preimage_action_pullCount_eq {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (n m : ℕ) : (fun (ω : probSpace 𝓐 𝓡) => (action alg n ω, Learning.pullCount (action alg) (action alg n ω) n ω)) ⁻¹' {(a, m)} = ({ω : probSpace 𝓐 𝓡 | action alg n ω = a ∧ Learning.pullCount (action alg) a n ω = m}.indicator fun (x : probSpace 𝓐 𝓡) => 1) ⁻¹' {1}

theorem Bandits.ArrayModel.measurable_indicator_action_eq_and_pullCount_eq {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (a : 𝓐) (m n : ℕ) : Measurable ({ω : probSpace 𝓐 𝓡 | action alg n ω = a ∧ Learning.pullCount (action alg) a n ω = m}.indicator fun (x : probSpace 𝓐 𝓡) => 1)

theorem Bandits.ArrayModel.measurable_pullCount_action_hist {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (n : ℕ) : Measurable fun (ω : probSpace 𝓐 𝓡) => Learning.pullCount (action alg) (action alg n ω) n ω

theorem Bandits.ArrayModel.indepFun_fst_snd {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : ProbabilityTheory.IndepFun Prod.fst Prod.snd (arrayMeasure ν)

theorem Bandits.ArrayModel.indepFun_fst_zero_snd_zero_action {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) : ProbabilityTheory.IndepFun (fun (ω : probSpace 𝓐 𝓡) => ω.1 0) (fun (ω : probSpace 𝓐 𝓡) => ω.2 0 a) (arrayMeasure ν)

theorem Bandits.ArrayModel.indepFun_fst_aux {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.IndepFun (fun (ω : probSpace 𝓐 𝓡) => ω.1 n) (fun (ω : probSpace 𝓐 𝓡) => (fun (i : Fin n) => ω.1 ↑i, ω.2)) (arrayMeasure ν)

theorem Bandits.ArrayModel.indepFun_fst_hist {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.IndepFun (fun (ω : probSpace 𝓐 𝓡) => ω.1 n) (fun (x : probSpace 𝓐 𝓡) => hist alg x n) (arrayMeasure ν)

theorem Bandits.ArrayModel.indepFun_snd_apply_truncRow {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [DecidableEq 𝓐] (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) (m : ℕ) : ProbabilityTheory.IndepFun (fun (ω : probSpace 𝓐 𝓡) => ω.2 m a) (truncRow a m) (arrayMeasure ν)

The reward ω.2 m a is independent of truncRow a m, which reads only other coordinates.

theorem Bandits.ArrayModel.indepFun_snd_apply_pullCount_action {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) (m n : ℕ) : ProbabilityTheory.IndepFun (fun (ω : probSpace 𝓐 𝓡) => ω.2 m a) ({ω : probSpace 𝓐 𝓡 | action alg n ω = a ∧ Learning.pullCount (action alg) a n ω = m}.indicator fun (x : probSpace 𝓐 𝓡) => 1) (arrayMeasure ν)

theorem Bandits.ArrayModel.indepFun_snd_hist_cond {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (a : 𝓐) (n m : ℕ) : ProbabilityTheory.IndepFun (fun (ω : probSpace 𝓐 𝓡) => ω.2 m a) (fun (x : probSpace 𝓐 𝓡) => hist alg x n) (arrayMeasure ν)[|(fun (ω : probSpace 𝓐 𝓡) => (action alg n ω, Learning.pullCount (action alg) (action alg n ω) n ω)) ⁻¹' {(a, m)}]

theorem Bandits.ArrayModel.hasCondDistrib_action' {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.HasCondDistrib (action alg n) (fun (x : probSpace 𝓐 𝓡) => hist alg x n) ((alg.policy n).sectL ()) (arrayMeasure ν)

theorem Bandits.ArrayModel.reward_ae_eq_cond {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) (a : 𝓐) (n m : ℕ) : reward alg n =ᵐ[(arrayMeasure ν)[|(fun (ω : probSpace 𝓐 𝓡) => (action alg n ω, Learning.pullCount (action alg) (action alg n ω) n ω)) ⁻¹' {(a, m)}]] fun (ω : probSpace 𝓐 𝓡) => ω.2 m a

theorem Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.HasCondDistrib (reward alg n) (fun (ω : probSpace 𝓐 𝓡) => (hist alg ω n, action alg n ω, Learning.pullCount (action alg) (action alg n ω) n ω)) (ProbabilityTheory.Kernel.prodMkLeft (Learning.Hist Unit 𝓐 𝓡 n) (ProbabilityTheory.Kernel.prodMkRight ℕ ν)) (arrayMeasure ν)

The conditional distribution of the reward at time n, given the history before time n, the action at time n, and the number of times that action has been pulled before time n, is equal to the kernel ν.

theorem Bandits.ArrayModel.condIndepFun_reward_hist {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (fun (ω : probSpace 𝓐 𝓡) => (action alg n ω, Learning.pullCount (action alg) (action alg n ω) n ω)) inferInstance) ⋯ (reward alg n) (fun (x : probSpace 𝓐 𝓡) => hist alg x n) (arrayMeasure ν)

The reward at time n is conditionally independent of the history before time n, given the action at time n and the number of times that action has been pulled before time n.

theorem Bandits.ArrayModel.hasCondDistrib_reward' {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.HasCondDistrib (reward alg n) (fun (ω : probSpace 𝓐 𝓡) => (hist alg ω n, action alg n ω)) (ProbabilityTheory.Kernel.prodMkLeft (Learning.Hist Unit 𝓐 𝓡 n) ν) (arrayMeasure ν)

The conditional distribution of the reward at time n, given the history before time n and the action at time n, is equal to the kernel ν.

theorem Bandits.ArrayModel.hasCondDistrib_action {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.HasCondDistrib (action alg n) (fun (ω : probSpace 𝓐 𝓡) => (Learning.history (Learning.noObs (probSpace 𝓐 𝓡)) (action alg) (reward alg) n ω, Learning.noObs (probSpace 𝓐 𝓡) n ω)) (alg.policy n) (arrayMeasure ν)

theorem Bandits.ArrayModel.hasCondDistrib_reward {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] (n : ℕ) : ProbabilityTheory.HasCondDistrib (reward alg n) (fun (ω : probSpace 𝓐 𝓡) => ((Learning.history (Learning.noObs (probSpace 𝓐 𝓡)) (action alg) (reward alg) n ω, Learning.noObs (probSpace 𝓐 𝓡) n ω), action alg n ω)) ((Learning.stationaryEnv ν).feedback n) (arrayMeasure ν)

theorem Bandits.ArrayModel.isAlgEnvSeq_arrayMeasure {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : Learning.IsAlgEnvSeq (Learning.noObs (probSpace 𝓐 𝓡)) (action alg) (reward alg) alg (Learning.stationaryEnv ν) (arrayMeasure ν)

theorem Bandits.ArrayModel.hasLaw_action_zero {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : ProbabilityTheory.HasLaw (action alg 0) (alg.p0 ()) (arrayMeasure ν)

theorem Bandits.ArrayModel.hasCondDistrib_reward_zero {𝓐 : Type u_1} {𝓡 : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {m𝓡 : MeasurableSpace 𝓡} [Nonempty 𝓐] [StandardBorelSpace 𝓐] [DecidableEq 𝓐] [Countable 𝓐] [StandardBorelSpace 𝓡] [Nonempty 𝓡] (alg : Learning.Algorithm Unit 𝓐 𝓡) (ν : ProbabilityTheory.Kernel 𝓐 𝓡) [ProbabilityTheory.IsMarkovKernel ν] : ProbabilityTheory.HasCondDistrib (reward alg 0) (action alg 0) ν (arrayMeasure ν)