inequality from written proof

Stream: new members

[Joshua Banks]

I was wondering if anyone knew if this was provable in lean and how to go about writing the lemma for this in lean. I know there is limits as to normal distribution in mathlib and was wondering if at this point this is possible.

Image-28-02-2023-at-22.18.jpeg

[Yaël Dillies]

Can you link to a proof/give us a rundown of it? I don't know this specific lemma but this kind of inequalities starts being accessible.

[Yaël Dillies]

Personally, I will soon prove the Marcinkiewicz-Zygmund inequality.

[Joshua Banks]

Unfortunately there is no following proof for this lemma in the paper I am working from, I am trying to prove some properties of Brownian motion, the paper is http://www.math.uchicago.edu/~may/VIGRE/VIGRE2009/REUPapers/McKnight.pdf

[Kevin Buzzard]

If you're asking "can Lean magically prove something which I don't know how to prove" then the answer is "no". The way it works is that the human types in the proof that they know, and the computer checks it.