∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop)
  {s : ℕ → Set α} {M : ℝ},
  0 < M →
    ∀ {r₁ r₂ : ℕ → ℝ},
      Filter.Tendsto r₁ Filter.atTop (nhdsWithin 0 (Set.Ioi 0)) →
        (∀ᶠ (i : ℕ) in Filter.atTop, M * r₁ i ≤ r₂ i) →
          Filter.blimsup (fun i => Metric.cthickening (r₁ i) (s i)) Filter.atTop p ≤ᵐ[μ]
            Filter.blimsup (fun i => Metric.cthickening (r₂ i) (s i)) Filter.atTop p