English
A set S of measures on a fixed space is tight if and only if for every ε > 0 there exists a compact K such that every μ ∈ S satisfies μ(K^c) ≤ ε.
Русский
Множество мер S на данном пространстве плотное тогда и только тогда, когда для каждого ε > 0 существует компактное K, такое что для каждой μ ∈ S выполняется μ(K^c) ≤ ε.
LaTeX
$$$\text{IsTightMeasureSet}(S) \iff \forall \varepsilon > 0, \exists K \text{ IsCompact}, \forall \mu \in S, \mu(K^c) \le \varepsilon$$$
Lean4
/-- A set of measures `S` is tight if for all `0 < ε`, there exists a compact set `K` such that
for all `μ ∈ S`, `μ Kᶜ ≤ ε`.
This is formulated in terms of filters, and proven equivalent to the definition above
in `IsTightMeasureSet_iff_exists_isCompact_measure_compl_le`. -/
def IsTightMeasureSet (S : Set (Measure 𝓧)) : Prop :=
Tendsto (⨆ μ ∈ S, μ) (cocompact 𝓧).smallSets (𝓝 0)
