Bandits.UCB.expectation_pullCount_le.{u_1} {K : ℕ} {hK : 0 < K} {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  [ProbabilityTheory.IsMarkovKernel ν] {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {A : ℕ → Ω → Fin K}
  {R : ℕ → Ω → ℝ} {σ2 : NNReal}
  (h :
    Learning.IsAlgEnvSeq A R (ucbAlgorithm hK (c * ↑σ2))
      (Learning.stationaryEnv ν) P)
  (hν :
    ∀ (a : Fin K),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x => x - ∫ (x : ℝ), id x ∂ν a) σ2 (ν a))
  (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K) (h_gap : 0 < gap ν a)
  (n : ℕ) :
  ∫ (x : Ω), (fun ω => ↑(Learning.pullCount A a n ω)) x ∂P ≤
    8 * c * ↑σ2 * Real.log (↑n + 1) / gap ν a ^ 2 + 2 +
      2 * ENNReal.toReal (constSum c n)
Bandits.UCB.expectation_pullCount_le.{u_1}
  {K : ℕ} {hK : 0 < K} {c : ℝ}
  {ν : ProbabilityTheory.Kernel (Fin K) ℝ}
  [ProbabilityTheory.IsMarkovKernel ν]
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P]
  {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ}
  {σ2 : NNReal}
  (h :
    Learning.IsAlgEnvSeq A R
      (ucbAlgorithm hK (c * ↑σ2))
      (Learning.stationaryEnv ν) P)
  (hν :
    ∀ (a : Fin K),
      ProbabilityTheory.HasSubgaussianMGF
        (fun x =>
          x - ∫ (x : ℝ), id x ∂ν a)
        σ2 (ν a))
  (hσ2 : σ2 ≠ 0) (hc : 0 < c) (a : Fin K)
  (h_gap : 0 < gap ν a) (n : ℕ) :
  ∫ (x : Ω),
      (fun ω =>
          ↑(Learning.pullCount A a n ω))
        x ∂P ≤
    8 * c * ↑σ2 * Real.log (↑n + 1) /
          gap ν a ^ 2 +
        2 +
      2 * ENNReal.toReal (constSum c n)