Bandits.UCB.pullCount_ae_le_add_two.{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} [Nonempty (Fin K)]
  (h :
    Learning.IsAlgEnvSeq A R (ucbAlgorithm hK (c * ↑σ2))
      (Learning.stationaryEnv ν) P)
  (hc : 0 ≤ c) (a : Fin K) (h_gap : 0 < gap ν a) (n C : ℕ) (hC : C ≠ 0)
  (hC' : 8 * c * ↑σ2 * Real.log (↑n + 1) / gap ν a ^ 2 ≤ ↑C) :
  ∀ᵐ (ω : Ω) ∂P,
    Learning.pullCount A a n ω ≤
      C + 1 +
          ∑ s ∈ Finset.range n,
            Set.indicator
              {s |
                0 < Learning.pullCount A (bestArm ν) s ω ∧
                  Learning.empMean A R (bestArm ν) s ω +
                      ucbWidth A (c * ↑σ2) (bestArm ν) s ω <
                    ∫ (x : ℝ), id x ∂ν (bestArm ν)}
              1 s +
        ∑ s ∈ Finset.range n,
          Set.indicator
            {s |
              0 < Learning.pullCount A a s ω ∧
                ∫ (x : ℝ), id x ∂ν a <
                  Learning.empMean A R a s ω -
                    ucbWidth A (c * ↑σ2) a s ω}
            1 s
Bandits.UCB.pullCount_ae_le_add_two.{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} [Nonempty (Fin K)]
  (h :
    Learning.IsAlgEnvSeq A R
      (ucbAlgorithm hK (c * ↑σ2))
      (Learning.stationaryEnv ν) P)
  (hc : 0 ≤ c) (a : Fin K)
  (h_gap : 0 < gap ν a) (n C : ℕ)
  (hC : C ≠ 0)
  (hC' :
    8 * c * ↑σ2 * Real.log (↑n + 1) /
        gap ν a ^ 2 ≤
      ↑C) :
  ∀ᵐ (ω : Ω) ∂P,
    Learning.pullCount A a n ω ≤
      C + 1 +
          ∑ s ∈ Finset.range n,
            Set.indicator
              {s |
                0 <
                    Learning.pullCount A
                      (bestArm ν) s ω ∧
                  Learning.empMean A R
                        (bestArm ν) s ω +
                      ucbWidth A (c * ↑σ2)
                        (bestArm ν) s ω <
                    ∫ (x : ℝ),
                      id x ∂ν (bestArm ν)}
              1 s +
        ∑ s ∈ Finset.range n,
          Set.indicator
            {s |
              0 <
                  Learning.pullCount A a s
                    ω ∧
                ∫ (x : ℝ), id x ∂ν a <
                  Learning.empMean A R a s
                      ω -
                    ucbWidth A (c * ↑σ2) a
                      s ω}
            1 s