by
  let s : Set (ℕ × ℝ) := {(m, x) | 0 < m ∧ (ν a)[id] ≤ x / m - √(2 * (c * σ2) * log (↑n + 1) / m)}
  have hs : MeasurableSet s := by
    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOfPred, s]
    fun_prop
  classical
  calc P {h | 0 < pullCount A a n h ∧ (ν a)[id] ≤ empMean A R a n h - ucbWidth A (c * σ2) a n h}
  _ ≤ ∑ k ∈ range (n + 1) with k ∈ Prod.fst '' s,
      (streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} :=
    prob_pullCount_prod_sumRewards_mem_le h hs
  _ ≤ ∑ k ∈ Icc 1 n,
      (streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by
    refine Finset.sum_le_sum_of_subset_of_nonneg (fun m ↦ ?_) fun _ _ _ ↦ by positivity
    simp [s]
    grind
  _ = ∑ k ∈ Icc 1 n,
      (streamMeasure ν)
        {ω | (ν a)[id] ≤ (∑ i ∈ range k, ω i a) / k - √(2 * c * σ2 * log (↑n + 1) / k)} := by
    refine Finset.sum_congr rfl fun k hk ↦ ?_
    congr with ω
    have hk : 0 < k := by grind
    simp only [id_eq, Nat.cast_nonneg, sqrt_div', Set.preimage_ofPred_eq, hk, true_and,
      Set.mem_ofPred_eq, s]
    grind
  _ ≤ ∑ k ∈ Icc 1 n, (1 : ℝ≥0∞) / (n + 1) ^ c := by
    gcongr with k hk
    exact prob_avg_sub_sqrt_log_ge hν hσ2 hc a n k (by grind)
  _ ≤ (n + 1) * (1 : ℝ≥0∞) / (n + 1) ^ c := by
    simp only [one_div, sum_const, Nat.card_Icc, add_tsub_cancel_right, nsmul_eq_mul, mul_one]
    rw [div_eq_mul_inv ((n : ℝ≥0∞) + 1)]
    gcongr
    exact le_self_add
  _ = 1 / (n + 1) ^ (c - 1) := by
    simp only [mul_one, one_div]
    rw [ENNReal.rpow_sub _ _ (by simp) (by finiteness), ENNReal.rpow_one, div_eq_mul_inv,
      ENNReal.div_eq_inv_mul, ENNReal.mul_inv (by simp) (by simp), inv_inv]