Laws of stepsUntil and rewardByCount

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

def Bandits.«term𝓛[_|_;_]» : Lean.ParserDescr

Law of Y conditioned on the event s.

Equations

• One or more equations did not get rendered due to their size.

def Bandits.«term𝓛[_|_In_;_]» : Lean.ParserDescr

Law of Y conditioned on the event that X is in s.

Equations

• One or more equations did not get rendered due to their size.

def Bandits.«term𝓛[_|_←_;_]» : Lean.ParserDescr

Law of Y conditioned on the event that X equals x.

Equations

• One or more equations did not get rendered due to their size.

theorem Bandits.condDistrib_reward'' {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (n : ℕ) : ⇑𝓛[fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => R n ω.1 | fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => A n ω.1; P.prod (streamMeasure ν)] =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => A n ω.1) (P.prod (streamMeasure ν))] ⇑ν

theorem Bandits.reward_cond_action {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (n : ℕ) (hμa : (MeasureTheory.Measure.map (fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => A n ω.1) (P.prod (streamMeasure ν))) {a} ≠ 0) : 𝓛[fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => R n ω.1 | fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => A n ω.1 in {a}; P.prod (streamMeasure ν)] = ν a

theorem Bandits.condIndepFun_reward_stepsUntil_action' {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace Ω] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (m n : ℕ) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (A n) inferInstance) ⋯ (R n) ({ω : Ω | Learning.stepsUntil A a m ω = ↑n}.indicator fun (x : Ω) => 1) P

theorem Bandits.condIndepFun_reward_stepsUntil_action {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace Ω] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (m n : ℕ) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => A n ω.1) m𝓐) ⋯ (fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => R n ω.1) ({ω : Ω × (ℕ → 𝓐 → ℝ) | Learning.stepsUntil A a m ω.1 = ↑n}.indicator fun (x : Ω × (ℕ → 𝓐 → ℝ)) => 1) (P.prod (streamMeasure ν))

theorem Bandits.reward_cond_stepsUntil {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace Ω] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (m n : ℕ) (hm : m ≠ 0) (hμn : (P.prod (streamMeasure ν)) ((fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => Learning.stepsUntil A a m ω.1) ⁻¹' {↑n}) ≠ 0) : 𝓛[fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => R n ω.1 | fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => Learning.stepsUntil A a m ω.1 in {↑n}; P.prod (streamMeasure ν)] = ν a

theorem Bandits.condDistrib_rewardByCount_stepsUntil {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace Ω] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (m : ℕ) (hm : m ≠ 0) : ⇑𝓛[Learning.rewardByCount A R a m | fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => Learning.stepsUntil A a m ω.1; P.prod (streamMeasure ν)] =ᵐ[MeasureTheory.Measure.map (fun (ω : Ω × (ℕ → 𝓐 → ℝ)) => Learning.stepsUntil A a m ω.1) (P.prod (streamMeasure ν))] ⇑(ProbabilityTheory.Kernel.const ℕ∞ (ν a))

The conditional distribution of the reward received at the m-th pull of action a given the time at which number of pulls is m is the constant kernel with value ν a.

theorem Bandits.hasLaw_rewardByCount {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace Ω] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (m : ℕ) (hm : m ≠ 0) : ProbabilityTheory.HasLaw (Learning.rewardByCount A R a m) (ν a) (P.prod (streamMeasure ν))

The reward received at the m-th pull of action a has law ν a.

theorem Bandits.identDistrib_rewardByCount {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace Ω] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (n m : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) : ProbabilityTheory.IdentDistrib (Learning.rewardByCount A R a n) (Learning.rewardByCount A R a m) (P.prod (streamMeasure ν)) (P.prod (streamMeasure ν))

theorem Bandits.identDistrib_rewardByCount_id {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace Ω] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (n : ℕ) (hn : n ≠ 0) : ProbabilityTheory.IdentDistrib (Learning.rewardByCount A R a n) id (P.prod (streamMeasure ν)) (ν a)

theorem Bandits.identDistrib_rewardByCount_eval {𝓐 : Type u_1} {Ω : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΩ : MeasurableSpace Ω} [DecidableEq 𝓐] [StandardBorelSpace 𝓐] [Nonempty 𝓐] {A : ℕ → Ω → 𝓐} {R : ℕ → Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm 𝓐 ℝ} {ν : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel ν] [StandardBorelSpace Ω] [Countable 𝓐] (h : Learning.IsAlgEnvSeq A R alg (Learning.stationaryEnv ν) P) (a : 𝓐) (n m : ℕ) (hn : n ≠ 0) : ProbabilityTheory.IdentDistrib (Learning.rewardByCount A R a n) (fun (ω : ℕ → 𝓐 → ℝ) => ω m a) (P.prod (streamMeasure ν)) (streamMeasure ν)