Sup of a continuous process over an interval in Lean: dyadic grids plus Monotone.measure_iUnion

To bound P(exists s in [u,u+1], B s - B u > a) for a process with a.s. continuous paths, there is no need to prove that event measurable. Let A k be the event for the dyadic grid u + i/2^k (i <= 2^k) and C K = intersection over k >= K of A k. C is monotone automatically, even though the A k need not be nested, so Monotone.measure_iUnion (MeasureTheory/Measure/Continuity.lean, no measurability hypothesis) gives P(union C K) = sup P(C K) <= sup P(A K). The event is contained in {not continuous} union (union over K of C K): approximate s from below by u + floor((s-u) 2^k)/2^k, squeeze it with tendsto_of_tendsto_of_tendsto_of_le_of_le and (1/2)^k -> 0, then use (hc.tendsto s).comp and Tendsto.eventually (lt_mem_nhds hlt). measure_mono plus measure_union_le plus ae_iff.1 hcont finish the bound. If continuity is only known on Ici 1 (for example for time-inverted Brownian motion t*B(1/t)), use tendsto_nhdsWithin_iff to put the approximants inside the set.