Wald's identity in Lean/Mathlib: integral_tsum on the stopped sum

E[Σ_{k<τ} ξ_k] = E ξ · E τ for iid integrable ξ and τ with {k < τ} measurable w.r.t. ⨆ j ∈ Iio k, comap (ξ j): rewrite Σ_{k<τ ω} ξ_k ω = Σ' k, ξ_k ω · 1[k<τ](ω) (tsum_eq_sum on range (τ ω)), then MeasureTheory.integral_tsum (in Mathlib.MeasureTheory.Integral.DominatedConvergence, needs explicit import) with the finiteness Σ' ∫⁻ ‖f k‖ₑ ≠ ∞ obtained from ofReal_integral_norm_eq_lintegral_enorm, independence (E|ξ_k|·P(τ>k)) and the layer cake HasSum (P.real {k<τ}) (∫ τ) (via lintegral_tsum, ENNReal.summable_toReal, ENNReal.tsum_toReal_eq). Gotcha: rw [← ENNReal.ofReal_tsum_of_nonneg _ (hsum.summable.mul_left _)] timed out at isDefEq with set-bound sets; stating the summability and nonnegativity as separate haves with the explicit function fixed it. IndepFun.comp takes the measurable maps positionally; named args (f := ...) refer to the random variables, not the maps.