a.s. convergence implies convergence in distribution

Stream: Is there code for X?

[Dominic Steinitz]

I looked for e.g. tendsto_in_measure_iff_tendsto_Lp as given in A Formalization of Doob’s Martingale Convergence Theorems in mathlib in the mathlib GitHub repo thinking such a theorem might be nearby but drew a blank even for the quoted theorem.

[Yaël Dillies]

docs#MeasureTheory.tendstoInMeasure_iff_tendsto_Lp ?

[Rémy Degenne]

Everything mentioned in that paper is in Mathlib... up to the multiple renames and possible refactors that happened since :)

[Dominic Steinitz]

I just tried moogle for the first time and searching for

[is_finite_measure 𝜇] (hp : 1 ≤ p) (hp′ : p ≠ ∞) (hf : ∀ n, mem_Lp (f n) p 𝜇) (hg : mem_Lp g p 𝜇) :
tendsto_in_measure 𝜇 f at_top g

found it somehow where a search in the repo failed.