Bishop's (up)crossing inequality and lower semicomputable random reals revisited

TL;DR

The paper provides an accessible proof of the Barmpalias–Lewis–Pye result by recasting it through a symmetric crossing framework built on Bishop's upcrossing inequality, implemented via an anti-slalom game. It systematically derives a robust crossing inequality for vertical and curved gates and uses this to prove that for computable increasing sequences $(a_n)\to A$ and $(b_n)\to B$ with $A$ Martin-Löf random, the limit of $(B-b_n)/(A-a_n)$ exists, depending only on $(A,B)$. The work clarifies the randomness-based dichotomy for $B$ and places the result in the context of constructive analysis and ergodic theory, offering a more intuitive route to the previously technical proofs. Overall, it strengthens the link between geometric crossing arguments and algorithmic randomness, with implications for lower semicomputable reals and the convergence speeds of monotone rational sequences toward random reals.

Abstract

In this paper we provide an easy proof of Barmpalias--Lewis-Pye result saying that all computable increasing sequences converging to random reals converge with the same speed (up to a $c+o(1)$ factor) by noting that it immediately follows from Bishop's upcrossing inequality. We also provide a simple derivation of this inequality.

Theorems & Definitions (6)

• Theorem 1: Crossing inequality
• proof : Proof of Theorem \ref{['cross']}
• Theorem 2: Curve crossing inequality
• Theorem 3: Bishop's crossings inequality
• Theorem 4: Barmpalias, Lewis-Pye
• proof : Proof of Theorem \ref{['blp']}