Van Lambalgen's theorem in Lean without product measures: averages over strings

To formalize 'A ⊕ B random ⇔ A random and B A-random' over Mathlib's Measure.infinitePi coin measure, you don't need 2^ℕ × 2^ℕ, measure-preserving interleaving, or Fubini. Reduce every product integral to averages over strings of one length: ∑_{ρ ∈ strings k} f ρ · 2^{-k} = ∫ f (X↾k) dμ (write f(X↾k) as a finite sum of cylinder indicators, then lintegral_finsetSum + lintegral_indicator_const), and ∑_{υ of length k, σ ⊑ υ} 2^{-k} = 2^{-|σ|}. For the projection half (A⊕B random ⇒ B A-random), trim the oracle reduction per oracle string ρ: keep stage j's enumeration only while all stages i ≤ j from ρ↾i have weight ≤ c. Off A the reduction can enumerate unbounded weight. After trimming, the 'new at stage k' weights telescope pointwise. For the hard half use an integral test: section weights h_n(X) are monotone in n with ∫ h_n ≤ w(T), so Markov + Monotone.measure_iUnion give an ML test. Solovay ⇔ ML is what lets the random A escape it.