Commit 2025-04-07 13:30 7548d2a7

feat(MeasureTheory): tightness criterion in finite dimensional inner product spaces (#23534) In a finite-dimensional inner product space, a set of measures S is tight if and only if the function r ↦ ⨆ μ ∈ S, μ {x | r < |⟪y, x⟫|} tends to 0 at infinity for all y.