Proof of komlos_norm

Stream: Brownian motion

[Jack McCarthy]

Just submitted a PR with proof of the komlos_norm lemma. Note that I needed to add the condition [CompleteSpace E], since the blueprint assumes we are working in a Hilbert space.

I'd really appreciate any feedback on my code as I'm still new to Lean4 and have lots to learn.

[Etienne Marion]

Hi! Can you take a look at https://github.com/RemyDegenne/brownian-motion/blob/master/CONTRIBUTING.md please? It explains how letting us know that you are awaiting review. In particular you should indicate on the issue you solve that you opened a PR, and indicate on the PR that you are awaiting review. Thanks!