Decidable lim sup and Borel–Cantelli-like lemmas for random sequences

We prove computable versions of limsuplimsup events and Borel–Cantelli-like results for algorithmically random sequences using a coefficient from Kolmogorov complexity. In particular we show that under suitable conditions on events, limsuplimsup is layerwise decidable.