Commit 2026-08-13 01:49 bc06ce9f

feat(Analysis): generalise eVariationOn to WeakPseudoEMetricSpace (#42662) Generalize the definition of eVariationOn for the underlying space E to be a WeakPseudoEMetricSpace (as well as theorems about/using the variation). In particular, now E can be ENNReal for example. Some theorems can not be generalised from PseudoEMetricSpace to WeakPseudoEMetricSpace of course. Most of them seem to be related to convergence and continuity. This is not surprising, since for instance EMetric.tendsto_nhds does not hold for WeakPseudoEMetricSpace (again think of ENNReal). Maybe with some effort more can be generalized, but I havent looked into that. I used the letter M(etric) instead of E for those who couldnt be generalized, as F was already used in the main file.... (The main changes live in Mathlib/Topology, but eVariationOn arguably belongs more to Analysis, which is why I added it in the PR title, maybe the file should even be moved)