Add Brownian quadratic variation module

[rohitmanokaran]

Refs #432.

Summary

• Add BrownianMotion.StochasticIntegral.QuadraticVariationBrownian and expose it from BrownianMotion.lean.
• Use the post-feat: Use local square-integrability for quadratic variation #469 quadraticVariation API through the normalized Doob-Meyer predictable-part dependencies from the Advance Brownian quadratic variation #463 route.
• Move the continuous-martingale local-square-integrability obligation to Martingale.isLocallySquareIntegrable_of_continuous, so the Brownian file depends on the general lemma instead of carrying Brownian-specific deterministic localization code.
• Close quadraticVariation_brownian using the Brownian square-minus-time martingale decomposition and normalized predictable-part uniqueness.

Dependency notes

• Rebased on upstream master through Blueprint update: classes of martingales #488.
• QuadraticVariationBrownian.lean has no sorry.
• Remaining placeholders are in dependency-layer APIs: continuous martingale implies locally square-integrable, and normalized Doob-Meyer existence/uniqueness.

Validation

• lake build BrownianMotion.StochasticIntegral.QuadraticVariationBrownian
• lake env lean BrownianMotion.lean

[RemyDegenne]

You should prove the more general result that a continuous martingale is locally square integrable (in a new PR).