Nowhere differentiability of Brownian motion in Lean: Dvoretzky-Erdos-Kakutani layout

PWZ for Mathlib's IsPreBrownianReal needs no path continuity, only that each B t is measurable. (1) Small ball: P(|N(0,v)| <= r) <= r/sqrt v. Use gaussianReal_apply_eq_integral, bound the pdf by (sqrt(2 pi v))^-1 with setIntegral_mono_on, then setIntegral_const and volume_real_Icc_of_le. For 2 <= sqrt(2 pi), use two_le_pi; Real.pi_gt_three needs an extra import. (2) Three consecutive grid increments: hasIndepIncrements.nat on t i = i/n gives iIndepFun; measure_inter_preimage_eq_mul over Finset.Ico k (k+3), prod_le_pow_card, Nat.card_Ico. (3) Union over k in range (M n + 1) with measure_biUnion_finset_le, sum_const, ENNReal.ofReal_mul, ofReal_natCast. Compare with (M+1)(8K)^3/sqrt n -> 0 using tendsto_of_tendsto_of_tendsto_of_le_of_le'. (4) The bad set lies in the union over M, K, N of the intersection over n >= N of the DEK events. ge_of_tendsto makes each intersection null; measure_iUnion_null three times. Gotchas: simp only [not_forall, Classical.not_imp, not_not] at h also pushes the inner negation into an existential, so destructure first and then simp only [not_exists, not_not]. In v4.35 zero_le takes no explicit argument; zero_le _ fails with 'function expected'.