Bandits.ETC.pullCount_add_one_of_ge.{u_1} {K : ℕ} {hK : 0 < K} {m : ℕ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {R : ℕ → Ω → ℝ}
  (h :
    Learning.IsAlgEnvSeq A R (etcAlgorithm hK m)
      (Learning.stationaryEnv ν) P)
  (a : Fin K) (hm : m ≠ 0) {n : ℕ} (hn : K * m ≤ n) :
  Learning.pullCount A a (n + 1) =ᵐ[P] fun ω =>
    Learning.pullCount A a n ω +
      Set.indicator {ω' | A (K * m) ω' = a} (fun x => 1) ω
Bandits.ETC.pullCount_add_one_of_ge.{u_1}
  {K : ℕ} {hK : 0 < K} {m : ℕ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ}
  (h :
    Learning.IsAlgEnvSeq A R
      (etcAlgorithm hK m)
      (Learning.stationaryEnv ν) P)
  (a : Fin K) (hm : m ≠ 0) {n : ℕ}
  (hn : K * m ≤ n) :
  Learning.pullCount A a (n + 1) =ᵐ[P]
    fun ω =>
    Learning.pullCount A a n ω +
      Set.indicator
        {ω' | A (K * m) ω' = a}
        (fun x => 1) ω