Commit 2026-05-29 07:38 bc415c88

feat(MeasureTheory/Function): ae convergence implies convergence in distribution (#39517) This PR introduces a theorem which concludes convergence in distribution from almost everywhere convergence. Previously, this could be done by chaining tendstoInMeasure_of_tendsto_ae and TendstoInMeasure.tendstoInDistribution. However, this is not a good way to to it since the second lemma requires a SeminormedAddCommGroup E instance (which is not needed for the statement to hold). Thus, we instead give a direct short proof which relies on dominated convergence. As a consequence, we also obtain a new proof of TendstoInMeasure.tendstoInDistribution which does not pass through tendstoInDistribution_of_tendstoInMeasure_sub and therefore does not require SeminormedAddCommGroup and SecondCountableTopology anymore. I expect this will enable significant golfing (or maybe even removal) of tendstoInDistribution_of_tendstoInMeasure_sub in the future. In order to allow for ae measurability as an assumption, it was necessary to add tendsto_lintegral_filter_of_dominated_convergence', which gives dominated convergence along a countable filter for AEMeasurable functions. Sidenote: I believe TendstoInMeasure.tendstoInDistribution should be rewritten at some point to require only a metric space (or maybe only uniform space) structure. However, even if this was done, the theorem of this PR provides the value of relying only on TopologicalSpace E.