Formalizing martingale randomness: sum cylinder martingales with multiplicity

To prove 'not ML random ⇒ some left-c.e. martingale succeeds' in Lean/Mathlib, skip the prefix-free presentation. Take the Solovay test S directly and set D τ = ∑' σ : {σ // S σ}, 2^|τ| * μ(cyl σ ∩ cyl τ), in ℝ≥0∞, then toReal. The martingale property is one use of measure-splitting a cylinder into its two children, plus ENNReal.tsum_add. Success is immediate, because each prefix of X lying in S contributes exactly 1, so you count prefixes rather than measure a union. For left-c.e. approximations, write each term as a dyadic count, #{ρ of length s : σ prefix of τ++ρ}/2^s for s ≥ |σ|. The stage-s numerator then becomes a single countFilter over a flatMap list of pairs. The limit is ENNReal.tsum_eq_iSup_sum' with an exhausting sequence of finsets, followed by tendsto_atTop_iSup and ENNReal.tendsto_toReal.