Bandits.UCB.pullCount_le_add_three_ae.{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 : ℕ → Ω → ℝ} [Nonempty (Fin K)]
  (h :
    Learning.IsAlgEnvSeq A R (ucbAlgorithm hK c)
      (Learning.stationaryEnv ν) P)
  (a : Fin K) (n C : ℕ) (hC : C ≠ 0) :
  ∀ᵐ (ω : Ω) ∂P,
    Learning.pullCount A a n ω ≤
      C + 1 +
            ∑ s ∈ Finset.range n,
              Set.indicator
                {s |
                  A s ω = a ∧
                    C < Learning.pullCount A a s ω ∧
                      ∫ (x : ℝ), id x ∂ν (bestArm ν) ≤
                          Learning.empMean A R (bestArm ν) s ω +
                            ucbWidth A c (bestArm ν) s ω ∧
                        Learning.empMean A R (A s ω) s ω -
                            ucbWidth A c (A s ω) s ω ≤
                          ∫ (x : ℝ), id x ∂ν (A s ω)}
                1 s +
          ∑ s ∈ Finset.range n,
            Set.indicator
              {s |
                0 < Learning.pullCount A (bestArm ν) s ω ∧
                  Learning.empMean A R (bestArm ν) s ω +
                      ucbWidth A c (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 a s ω}
            1 s
Bandits.UCB.pullCount_le_add_three_ae.{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 : ℕ → Ω → ℝ}
  [Nonempty (Fin K)]
  (h :
    Learning.IsAlgEnvSeq A R
      (ucbAlgorithm hK c)
      (Learning.stationaryEnv ν) P)
  (a : Fin K) (n C : ℕ) (hC : C ≠ 0) :
  ∀ᵐ (ω : Ω) ∂P,
    Learning.pullCount A a n ω ≤
      C + 1 +
            ∑ s ∈ Finset.range n,
              Set.indicator
                {s |
                  A s ω = a ∧
                    C <
                        Learning.pullCount
                          A a s ω ∧
                      ∫ (x : ℝ),
                            id
                              x ∂ν
                              (bestArm
                                ν) ≤
                          Learning.empMean
                              A R
                              (bestArm ν)
                              s ω +
                            ucbWidth A c
                              (bestArm ν)
                              s ω ∧
                        Learning.empMean A
                              R (A s ω) s
                              ω -
                            ucbWidth A c
                              (A s ω) s
                              ω ≤
                          ∫ (x : ℝ),
                            id
                              x ∂ν
                              (A s ω)}
                1 s +
          ∑ s ∈ Finset.range n,
            Set.indicator
              {s |
                0 <
                    Learning.pullCount A
                      (bestArm ν) s ω ∧
                  Learning.empMean A R
                        (bestArm ν) s ω +
                      ucbWidth A c
                        (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 a s ω}
            1 s