English
Equivalently, IsTightMeasureSet S holds if and only if for every ε > 0 there exists a compact K with the same property relative to all μ ∈ S.
Русский
Эквивалентно, что IsTightMeasureSet S выполняется тогда и только тогда, когда для каждого ε > 0 существует компактное K с тем же свойством относительно всех μ ∈ S.
LaTeX
$$$IsTightMeasureSet(S) \iff \forall \varepsilon > 0, \exists K, IsCompact(K) \land \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ᶜ ≤ ε`. -/
theorem IsTightMeasureSet_iff_exists_isCompact_measure_compl_le :
IsTightMeasureSet S ↔ ∀ ε, 0 < ε → ∃ K : Set 𝓧, IsCompact K ∧ ∀ μ ∈ S, μ (Kᶜ) ≤ ε :=
by
simp only [IsTightMeasureSet, ENNReal.tendsto_nhds ENNReal.zero_ne_top, gt_iff_lt, zero_add, iSup_apply, mem_Icc,
tsub_le_iff_right, zero_le, iSup_le_iff, true_and, eventually_smallSets, mem_cocompact]
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
· obtain ⟨A, ⟨K, h1, h2⟩, hA⟩ := h ε hε
exact ⟨K, h1, hA Kᶜ h2⟩
· obtain ⟨K, h1, h2⟩ := h ε hε
exact ⟨Kᶜ, ⟨K, h1, subset_rfl⟩, fun A hA μ hμS ↦ (μ.mono hA).trans (h2 μ hμS)⟩
