Documentation

LeanMachineLearning.SequentialLearning.SumRewards

Sums of rewards #

source
noncomputable def Learning.sumRewards {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] (A : β„• β†’ Ξ© β†’ 𝓐) (R : β„• β†’ Ξ© β†’ 𝓨) (a : 𝓐) (t : β„•) (Ο‰ : Ξ©) :
𝓨

Sum of rewards obtained when pulling action a up to time t (exclusive).

Equations
Instances For
    source
    noncomputable def Learning.sumRewards' {π“ž : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} [DecidableEq 𝓐] [AddCommGroup 𝓨] (n : β„•) (h : Hist π“ž 𝓐 𝓨 n) (a : 𝓐) :
    𝓨

    Sum of rewards of arm a in the history before time n.

    Equations
    Instances For
      source
      noncomputable def Learning.empMean {𝓐 : Type u_2} {Ξ© : Type u_4} [DecidableEq 𝓐] (A : β„• β†’ Ξ© β†’ 𝓐) (R : β„• β†’ Ξ© β†’ ℝ) (a : 𝓐) (t : β„•) (Ο‰ : Ξ©) :
      ℝ

      Empirical mean reward obtained when pulling action a up to time t (exclusive).

      Equations
      Instances For
        source
        noncomputable def Learning.empMean' {π“ž : Type u_1} {𝓐 : Type u_2} [DecidableEq 𝓐] (n : β„•) (h : Hist π“ž 𝓐 ℝ n) (a : 𝓐) :
        ℝ

        Empirical mean of arm a in the history before time n.

        Equations
        Instances For
          source
          @[simp]
          theorem Learning.sumRewards_zero {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐} {R : β„• β†’ Ξ© β†’ 𝓨} :
          sumRewards A R a 0 = 0
          source
          theorem Learning.sumRewards_add_one {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐} {t : β„•} {Ο‰ : Ξ©} {R : β„• β†’ Ξ© β†’ 𝓨} :
          sumRewards A R a (t + 1) Ο‰ = sumRewards A R a t Ο‰ + if A t Ο‰ = a then R t Ο‰ else 0
          source
          theorem Learning.sumRewards_eq_of_pullCount_eq {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐} {Ο‰ : Ξ©} {R : β„• β†’ Ξ© β†’ 𝓨} {s t : β„•} (h_eq : pullCount A a s Ο‰ = pullCount A a t Ο‰) :
          sumRewards A R a s Ο‰ = sumRewards A R a t Ο‰
          source
          theorem Learning.sumRewards_eq_pullCount_mul_empMean {𝓐 : Type u_2} {Ξ© : Type u_4} [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐} {t : β„•} {R : β„• β†’ Ξ© β†’ ℝ} {Ο‰ : Ξ©} (h_pull : pullCount A a t Ο‰ β‰  0) :
          sumRewards A R a t Ο‰ = ↑(pullCount A a t Ο‰) * empMean A R a t Ο‰
          source
          theorem Learning.sum_rewardByCount_eq_sumRewards {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ 𝓨} (a : 𝓐) (t : β„•) (Ο‰ : Ξ© Γ— (β„• β†’ 𝓐 β†’ 𝓨)) :
          βˆ‘ m ∈ Finset.Icc 1 (pullCount A a t Ο‰.1), rewardByCount A R a m Ο‰ = sumRewards A R a t Ο‰.1
          source
          theorem Learning.sumRewards_eq_sumRewards' {π“ž : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐} {R : β„• β†’ Ξ© β†’ 𝓨} {n : β„•} {Ο‰ : Ξ©} :
          sumRewards A R a n Ο‰ = sumRewards' n (history O A R n Ο‰) a
          source
          theorem Learning.sumRewards_eq_comp_history {π“ž : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ 𝓨} (a : 𝓐) (n : β„•) :
          sumRewards A R a n = (fun (h : Hist π“ž 𝓐 𝓨 n) => sumRewards' n h a) ∘ history O A R n

          sumRewards A R a n is a function of the history before time n.

          source
          theorem Learning.empMean_eq_empMean' {π“ž : Type u_1} {𝓐 : Type u_2} {Ξ© : Type u_4} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} {n : β„•} {Ο‰ : Ξ©} :
          empMean A R a n Ο‰ = empMean' n (history O A R n Ο‰) a
          source
          theorem Learning.empMean_eq_comp_history {π“ž : Type u_1} {𝓐 : Type u_2} {Ξ© : Type u_4} [DecidableEq 𝓐] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} {R : β„• β†’ Ξ© β†’ ℝ} (a : 𝓐) (n : β„•) :
          empMean A R a n = (fun (h : Hist π“ž 𝓐 ℝ n) => empMean' n h a) ∘ history O A R n

          empMean A R a n is a function of the history before time n.

          source
          theorem Learning.sumRewards_sub_pullCount_smul_eq_sum {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} [DecidableEq 𝓐] [AddCommGroup 𝓨] {A : β„• β†’ Ξ© β†’ 𝓐} {a : 𝓐} {n : β„•} {Ο‰ : Ξ©} {R : β„• β†’ Ξ© β†’ 𝓨} (c : 𝓐 β†’ 𝓨) :
          sumRewards A R a (n + 1) Ο‰ - pullCount A a (n + 1) Ο‰ β€’ c a = βˆ‘ i ∈ Finset.range (n + 1), if A i Ο‰ = a then R i Ο‰ - c a else 0
          source
          theorem Learning.measurable_sumRewards {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] [AddCommGroup 𝓨] {A : β„• β†’ Ξ© β†’ 𝓐} [MeasurableSingletonClass 𝓐] [MeasurableAddβ‚‚ 𝓨] {R : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hR : βˆ€ (n : β„•), Measurable (R n)) (a : 𝓐) (t : β„•) :
          Measurable (sumRewards A R a t)
          source
          theorem Learning.measurable_uncurry_sumRewards_comp {𝓐 : Type u_2} {𝓨 : Type u_3} {Ξ© : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] [AddCommGroup 𝓨] {A : β„• β†’ Ξ© β†’ 𝓐} [Countable 𝓐] [MeasurableSingletonClass 𝓐] [MeasurableAddβ‚‚ 𝓨] {R : β„• β†’ Ξ© β†’ 𝓨} (hA : βˆ€ (n : β„•), Measurable (A n)) (hR : βˆ€ (n : β„•), Measurable (R n)) {f : Ξ© β†’ 𝓐} (hf : Measurable f) {g : Ξ© β†’ β„•} (hg : Measurable g) :
          Measurable fun (Ο‰ : Ξ©) => sumRewards A R (f Ο‰) (g Ο‰) Ο‰
          source
          theorem Learning.measurable_empMean {𝓐 : Type u_2} {Ξ© : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} [MeasurableSingletonClass 𝓐] {R : β„• β†’ Ξ© β†’ ℝ} (hA : βˆ€ (n : β„•), Measurable (A n)) (hR : βˆ€ (n : β„•), Measurable (R n)) (a : 𝓐) (n : β„•) :
          Measurable (empMean A R a n)
          source
          theorem Learning.measurable_uncurry_empMean_comp {𝓐 : Type u_2} {Ξ© : Type u_4} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {A : β„• β†’ Ξ© β†’ 𝓐} [Countable 𝓐] [MeasurableSingletonClass 𝓐] {R : β„• β†’ Ξ© β†’ ℝ} (hA : βˆ€ (n : β„•), Measurable (A n)) (hR : βˆ€ (n : β„•), Measurable (R n)) {f : Ξ© β†’ 𝓐} (hf : Measurable f) {g : Ξ© β†’ β„•} (hg : Measurable g) :
          Measurable fun (Ο‰ : Ξ©) => empMean A R (f Ο‰) (g Ο‰) Ο‰
          source
          theorem Learning.measurable_sumRewards' {π“ž : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [DecidableEq 𝓐] [AddCommGroup 𝓨] [MeasurableSingletonClass 𝓐] [MeasurableAddβ‚‚ 𝓨] (n : β„•) (a : 𝓐) :
          Measurable fun (x : Hist π“ž 𝓐 𝓨 n) => sumRewards' n x a
          source
          theorem Learning.measurable_uncurry_sumRewards' {π“ž : Type u_1} {𝓐 : Type u_2} {𝓨 : Type u_3} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} {m𝓨 : MeasurableSpace 𝓨} [DecidableEq 𝓐] [AddCommGroup 𝓨] [MeasurableEq 𝓐] [MeasurableAddβ‚‚ 𝓨] (n : β„•) :
          Measurable fun (p : Hist π“ž 𝓐 𝓨 n Γ— 𝓐) => sumRewards' n p.1 p.2
          source
          theorem Learning.measurable_empMean' {π“ž : Type u_1} {𝓐 : Type u_2} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [MeasurableSingletonClass 𝓐] (n : β„•) (a : 𝓐) :
          Measurable fun (x : Hist π“ž 𝓐 ℝ n) => empMean' n x a
          source
          theorem Learning.measurable_uncurry_empMean' {π“ž : Type u_1} {𝓐 : Type u_2} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} [DecidableEq 𝓐] [MeasurableEq 𝓐] (n : β„•) :
          Measurable fun (p : Hist π“ž 𝓐 ℝ n Γ— 𝓐) => empMean' n p.1 p.2
          source
          theorem Learning.IsAlgEnvSeq.isStronglyPredictable_sumRewards {π“ž : Type u_1} {𝓐 : Type u_2} {Ξ© : Type u_4} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} [MeasurableSingletonClass 𝓐] {𝓨 : Type u_5} {x✝ : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [OpensMeasurableSpace 𝓨] [SecondCountableTopology 𝓨] {R : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm π“ž 𝓐 𝓨} {env : Environment π“ž 𝓐 𝓨} (h : IsAlgEnvSeq O A R alg env P) (a : 𝓐) :
          MeasureTheory.IsStronglyPredictable h.filtration (sumRewards A R a)
          source
          theorem Learning.IsAlgEnvSeq.stronglyAdapted_sumRewards_add_one {π“ž : Type u_1} {𝓐 : Type u_2} {Ξ© : Type u_4} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} [MeasurableSingletonClass 𝓐] {𝓨 : Type u_5} {x✝ : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [OpensMeasurableSpace 𝓨] [SecondCountableTopology 𝓨] {R : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm π“ž 𝓐 𝓨} {env : Environment π“ž 𝓐 𝓨} (h : IsAlgEnvSeq O A R alg env P) (a : 𝓐) :
          MeasureTheory.StronglyAdapted h.filtration fun (n : β„•) => sumRewards A R a (n + 1)
          source
          theorem Learning.IsAlgEnvSeq.adapted_sumRewards_add_one {π“ž : Type u_1} {𝓐 : Type u_2} {Ξ© : Type u_4} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} [MeasurableSingletonClass 𝓐] {𝓨 : Type u_5} {x✝ : MeasurableSpace 𝓨} [NormedAddCommGroup 𝓨] [BorelSpace 𝓨] [SecondCountableTopology 𝓨] {R : β„• β†’ Ξ© β†’ 𝓨} {alg : Algorithm π“ž 𝓐 𝓨} {env : Environment π“ž 𝓐 𝓨} (h : IsAlgEnvSeq O A R alg env P) (a : 𝓐) :
          MeasureTheory.Adapted h.filtration fun (n : β„•) => sumRewards A R a (n + 1)
          source
          theorem Learning.IsAlgEnvSeq.isStronglyPredictable_empMean {π“ž : Type u_1} {𝓐 : Type u_2} {Ξ© : Type u_4} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} [MeasurableSingletonClass 𝓐] {R' : β„• β†’ Ξ© β†’ ℝ} {alg : Algorithm π“ž 𝓐 ℝ} {env : Environment π“ž 𝓐 ℝ} (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) :
          MeasureTheory.IsStronglyPredictable h.filtration (empMean A R' a)
          source
          theorem Learning.IsAlgEnvSeq.stronglyAdapted_empMean_add_one {π“ž : Type u_1} {𝓐 : Type u_2} {Ξ© : Type u_4} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} [MeasurableSingletonClass 𝓐] {R' : β„• β†’ Ξ© β†’ ℝ} {alg : Algorithm π“ž 𝓐 ℝ} {env : Environment π“ž 𝓐 ℝ} (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) :
          MeasureTheory.StronglyAdapted h.filtration fun (n : β„•) => empMean A R' a (n + 1)
          source
          theorem Learning.IsAlgEnvSeq.adapted_empMean_add_one {π“ž : Type u_1} {𝓐 : Type u_2} {Ξ© : Type u_4} {mπ“ž : MeasurableSpace π“ž} {m𝓐 : MeasurableSpace 𝓐} {mΞ© : MeasurableSpace Ξ©} [DecidableEq 𝓐] {P : MeasureTheory.Measure Ξ©} [MeasureTheory.IsProbabilityMeasure P] {O : β„• β†’ Ξ© β†’ π“ž} {A : β„• β†’ Ξ© β†’ 𝓐} [MeasurableSingletonClass 𝓐] {R' : β„• β†’ Ξ© β†’ ℝ} {alg : Algorithm π“ž 𝓐 ℝ} {env : Environment π“ž 𝓐 ℝ} (h : IsAlgEnvSeq O A R' alg env P) (a : 𝓐) :
          MeasureTheory.Adapted h.filtration fun (n : β„•) => empMean A R' a (n + 1)