L^p-mean convergence of random variable sequences

Stream: new members

[Scott Howard]

Does mathlib have convergence of sequences of random variables "in the pth mean"---defined to mean that E[|X_n - X|^p] -> 0---anywhere? I imagine that there's some way to talk about this notion with what's already present, but I was thinking that it could be useful to add a direct way to talk about it to the API, particularly because the mean-square version (p = 2) is extremely useful for the Ito calculus, which itself might be worthwhile to add at some point.

[Heather Macbeth]

@Scott Howard Mathlib has L^p convergence of functions: see docs#measure_theory.Lp. (Take the counting measure on $\mathbb{N}$ to get sequences, as you asked for.) I don't believe there's a version of this for measures available; @Rémy Degenne would be the person to ask.

[Heather Macbeth]

(Oh, I see, you don't necessarily want the measure space to be $\mathbb{N}$, you just want to characterise the topology by discussing convergence of sequences ... but the rest of my answer still applies.)

[Scott Howard]

Looking now, thanks!