Documentation

LeanMachineLearning.Online.Bandit.RewardByCountMeasure

Laws of stepsUntil and rewardByCount #

source
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.
Instances For
    source
    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.
    Instances For
      source
      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.
      Instances For
        source
        theorem Bandits.condDistrib_reward'' {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] (h : Learning.IsAlgEnvSeq O 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 Ξ½))] ⇑ν
        source
        theorem Bandits.reward_cond_action {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O 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
        source
        theorem Bandits.condIndepFun_reward_stepsUntil_action' {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace Ξ©] (h : Learning.IsAlgEnvSeq O 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
        source
        theorem Bandits.condIndepFun_reward_stepsUntil_action {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace Ξ©] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O 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 Ξ½))
        source
        theorem Bandits.reward_cond_stepsUntil {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace Ξ©] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O 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
        source
        theorem Bandits.condDistrib_rewardByCount_stepsUntil {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace Ξ©] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O 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.

        source
        theorem Bandits.hasLaw_rewardByCount {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace Ξ©] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O 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.

        source
        theorem Bandits.identDistrib_rewardByCount {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace Ξ©] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O 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 Ξ½))
        source
        theorem Bandits.identDistrib_rewardByCount_id {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace Ξ©] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (a : 𝓐) (n : β„•) (hn : n β‰  0) :
        ProbabilityTheory.IdentDistrib (Learning.rewardByCount A R a n) id (P.prod (streamMeasure Ξ½)) (Ξ½ a)
        source
        theorem Bandits.identDistrib_rewardByCount_eval {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [StandardBorelSpace 𝓐] [Nonempty 𝓐] [StandardBorelSpace Ξ©] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O 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 Ξ½)

        Independence of the rewards by count #

        We prove that the family (rewardByCount A R a (m + 1))_{(a, m)} is independent, with rewardByCount A R a (m + 1) distributed according to Ξ½ a.

        The proof goes through the time-truncated arrays rewardByCountUntil A R t, in which the entries corresponding to pulls that happen at time t or later are replaced by the auxiliary array. Under the product measure 𝔓, the law of rewardByCountUntil A R t does not depend on t: going from t to t + 1 replaces the entry (A t, pullCount A (A t) t), which was an auxiliary reward with law Ξ½ (A t) independent of everything else, by the reward R t, which conditionally on the history and on A t also has law Ξ½ (A t). For t = 0 the array is a sub-array of the auxiliary array, whose law is the product measure. Finally rewardByCountUntil A R t converges to rewardByCount entrywise as t β†’ ∞, which gives the law of the latter.

        source
        theorem Bandits.hasLaw_rewardByCountUntil_zero {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] (ΞΌ : MeasureTheory.Measure Ξ©) [MeasureTheory.IsProbabilityMeasure ΞΌ] :
        ProbabilityTheory.HasLaw (Learning.rewardByCountUntil A R 0) (MeasureTheory.Measure.infinitePi fun (p : 𝓐 Γ— β„•) => Ξ½ p.1) (ΞΌ.prod (streamMeasure Ξ½))

        The law of the array rewardByCountUntil A R 0, which is a sub-array of the auxiliary array, is the product measure ⨂ (a, m), Ξ½ a.

        source
        theorem Bandits.indepFun_update_rewardByCountUntil_eval {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (hA : βˆ€ (n : β„•), Measurable (A n)) (hR : βˆ€ (n : β„•), Measurable (R n)) (ΞΌ : MeasureTheory.Measure Ξ©) [MeasureTheory.IsProbabilityMeasure ΞΌ] (t : β„•) (b : 𝓐) (k : β„•) :
        ProbabilityTheory.IndepFun (fun (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) => Function.update (Learning.rewardByCountUntil A R t Ο‰) (b, k) 0) (fun (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) => Ο‰.2 (k + 1) b) (ΞΌ.prod (streamMeasure Ξ½))

        The array rewardByCountUntil A R t with the entry (b, k) erased is independent of the entry (k + 1, b) of the auxiliary array.

        source
        theorem Bandits.indepFun_history_reward_cond {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (n : β„•) (b : 𝓐) (k : β„•) :
        ProbabilityTheory.IndepFun (fun (x : Ω) => ((Learning.history O A R n x, O n x), A n x)) (R n) P[|{x : Ω | A n x = b ∧ Learning.pullCount A b n x = k}]

        Conditionally on the event that the action at time n is b and that b was pulled k times before, the reward at time n is independent of the history before time n and of the action at time n.

        source
        theorem Bandits.hasLaw_reward_cond {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (t : β„•) (b : 𝓐) (k : β„•) (hP : P {x : Ξ© | A t x = b ∧ Learning.pullCount A b t x = k} β‰  0) :
        ProbabilityTheory.HasLaw (R t) (ν b) P[|{x : Ω | A t x = b ∧ Learning.pullCount A b t x = k}]

        Conditionally on the event that the action at time t is b and that b was pulled k times before, the reward at time t has law Ξ½ b.

        source
        theorem Bandits.hasLaw_reward_cond_prod {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (t : β„•) (b : 𝓐) (k : β„•) (hP : P {x : Ξ© | A t x = b ∧ Learning.pullCount A b t x = k} β‰  0) :
        ProbabilityTheory.HasLaw (fun (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) => R t Ο‰.1) (Ξ½ b) (P[|{x : Ξ© | A t x = b ∧ Learning.pullCount A b t x = k}].prod (streamMeasure Ξ½))
        source
        theorem Bandits.indepFun_update_rewardByCountUntil_reward {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (t : β„•) (b : 𝓐) (k : β„•) :
        ProbabilityTheory.IndepFun (fun (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) => Function.update (Learning.rewardByCountUntil A R t Ο‰) (b, k) 0) (fun (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) => R t Ο‰.1) (P[|{x : Ξ© | A t x = b ∧ Learning.pullCount A b t x = k}].prod (streamMeasure Ξ½))

        Conditionally on the event that the action at time t is b and that b was pulled k times before, the array rewardByCountUntil A R t with the entry (b, k) erased is independent of the reward at time t.

        source
        theorem Bandits.identDistrib_rewardByCountUntil_add_one_cond {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (t : β„•) (b : 𝓐) (k : β„•) :
        ProbabilityTheory.IdentDistrib (Learning.rewardByCountUntil A R (t + 1)) (Learning.rewardByCountUntil A R t) (P[|{x : Ω | A t x = b ∧ Learning.pullCount A b t x = k}].prod (streamMeasure ν)) (P[|{x : Ω | A t x = b ∧ Learning.pullCount A b t x = k}].prod (streamMeasure ν))

        Conditionally on the event that the action at time t is b and that b was pulled k times before, the arrays rewardByCountUntil A R (t + 1) and rewardByCountUntil A R t have the same law: they differ only in the entry (b, k), which is R t in the first and an auxiliary reward in the second, and both are independent of the rest of the array with law Ξ½ b.

        source
        theorem Bandits.identDistrib_rewardByCountUntil_add_one {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (t : β„•) :
        ProbabilityTheory.IdentDistrib (Learning.rewardByCountUntil A R (t + 1)) (Learning.rewardByCountUntil A R t) (P.prod (streamMeasure Ξ½)) (P.prod (streamMeasure Ξ½))

        The law of rewardByCountUntil A R t under 𝔓 does not depend on t.

        source
        theorem Bandits.hasLaw_rewardByCountUntil {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (t : β„•) :
        ProbabilityTheory.HasLaw (Learning.rewardByCountUntil A R t) (MeasureTheory.Measure.infinitePi fun (p : 𝓐 Γ— β„•) => Ξ½ p.1) (P.prod (streamMeasure Ξ½))

        The law of rewardByCountUntil A R t under 𝔓 is ⨂ (a, m), Ξ½ a, for all t.

        source
        theorem Bandits.hasLaw_rewardByCount_infinitePi {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) :
        ProbabilityTheory.HasLaw (fun (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) (p : 𝓐 Γ— β„•) => Learning.rewardByCount A R p.1 (p.2 + 1) Ο‰) (MeasureTheory.Measure.infinitePi fun (p : 𝓐 Γ— β„•) => Ξ½ p.1) (P.prod (streamMeasure Ξ½))

        The array of rewards by count (a, m) ↦ rewardByCount A R a (m + 1) has law ⨂ (a, m), Ξ½ a: its entries are independent, and the entry (a, m) has law Ξ½ a.

        source
        theorem Bandits.hasLaw_rewardByCount_add_one {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (a : 𝓐) (m : β„•) :
        ProbabilityTheory.HasLaw (Learning.rewardByCount A R a (m + 1)) (Ξ½ a) (P.prod (streamMeasure Ξ½))

        The reward received at the (m + 1)-th pull of action a has law Ξ½ a.

        source
        theorem Bandits.iIndepFun_rewardByCount_add_one {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) :
        ProbabilityTheory.iIndepFun (fun (p : 𝓐 Γ— β„•) (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) => Learning.rewardByCount A R p.1 (p.2 + 1) Ο‰) (P.prod (streamMeasure Ξ½))

        The rewards by count rewardByCount A R a (m + 1) are independent over all actions a and all counts m.

        source
        theorem Bandits.iIndepFun_rewardByCount {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) :
        ProbabilityTheory.iIndepFun (fun (p : { p : 𝓐 Γ— β„• // p.2 β‰  0 }) (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) => Learning.rewardByCount A R (↑p).1 (↑p).2 Ο‰) (P.prod (streamMeasure Ξ½))

        The rewards by count rewardByCount A R a m for m β‰  0 are independent over all actions a and all counts m.

        source
        theorem Bandits.iIndepFun_rewardByCount_add_one_action {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) (a : 𝓐) :
        ProbabilityTheory.iIndepFun (fun (m : β„•) (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ ℝ)) => Learning.rewardByCount A R a (m + 1) Ο‰) (P.prod (streamMeasure Ξ½))

        For each action a, the rewards by count (rewardByCount A R a (m + 1))_m are independent (and by hasLaw_rewardByCount_add_one identically distributed with law Ξ½ a).

        source
        theorem Bandits.indepFun_rewardByCount {𝓐 : Type u_1} {Ξ© : Type u_2} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ Unit} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {alg : Learning.Algorithm Unit 𝓐 ℝ} {Ξ½ : ProbabilityTheory.Kernel 𝓐 ℝ} [ProbabilityTheory.IsMarkovKernel Ξ½] [MeasurableSingletonClass 𝓐] [Countable 𝓐] (h : Learning.IsAlgEnvSeq O A R alg (Learning.stationaryEnv Ξ½) P) {a b : 𝓐} {m n : β„•} (hm : m β‰  0) (hn : n β‰  0) (hne : (a, m) β‰  (b, n)) :
        ProbabilityTheory.IndepFun (Learning.rewardByCount A R a m) (Learning.rewardByCount A R b n) (P.prod (streamMeasure Ξ½))

        Two distinct rewards by count are independent.