Ville's inequality gives Kurtz-level martingale results in Lean cheaply

To prove that a Kurtz random X defeats every computable martingale d with d(X↾n) ≥ h(n) at all n (h a computable unbounded order), build a decidable tree from the precision-0 rational approximation a/b of d. Keep the strings all of whose prefixes satisfy h(|σ|) ≤ a/b + 1, written in ℕ as (0<b ∧ h·b ≤ a+b) ∨ (b=0 ∧ h ≤ 1) to avoid division. X is a path, since d ≥ h implies the approximation is ≥ h-1. Every path has d(Y↾n) ≥ h(n) - 2, so Ville's inequality μ{∃n, c ≤ d(Y↾n)} ≤ d[]/c bounds the paths by d[]/(k+1) for every k, which makes them null. For the ℕ-side decidability proof, generalize h m * b(..) = P; omega disposes of the nonlinear product, which omega would otherwise reject.