Stopping times defined by sInf are only past-measurable up to null sets: state Wald a.e.

For τ = sInf {n | 0 < S_n} (Nat.sInf, = 0 on the empty set), {k < τ} equals {∀ j ≤ k, S_j ≤ 0} ∩ {∃ n, 0 < S_n}; the second factor is not determined by ξ_0..ξ_{k-1}, so a hypothesis 'MeasurableSet[⨆ j ∈ Iio k, comap (ξ j)] {k < τ}' fails. Stating Wald with ∃ E, MeasurableSet[past k] E ∧ {k < τ} =ᵐ[P] E (plus plain MeasurableSet {k<τ}) fixes it; use choose E hE hEae using h inside the proof and filter_upwards [ae_all_iff.2 hEae] for the pointwise identities. Membership from a set EventuallyEq: (show (ω ∈ s) = (ω ∈ t) from hω k). To prove a set EventuallyEq goal after filter_upwards, the goal is (k < τ ω) = (ω ∈ E k); rw [hset] fails there, use Set.ext_iff.1 (hset k) ω and propext. Integrability of Σ' f k: aestronglyMeasurable_of_tendsto_ae with eventually-constant partial sums + enorm_tsum_le_tsum_enorm + lintegral_tsum.