English
If μ is finite and inner regular with respect to closed compact sets, then the singleton {μ} is tight.
Русский
Если μ конечна и внутренняя регулярность относится к замкнутым компактным множествам, то одиночное множество {μ} плотное.
LaTeX
$$IsTightMeasureSet({μ})$$
Lean4
/-- Finite measures that are inner regular with respect to closed compact sets are tight. -/
theorem isTightMeasureSet_singleton_of_innerRegularWRT [OpensMeasurableSpace 𝓧] [IsFiniteMeasure μ]
(h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet) : IsTightMeasureSet { μ } :=
by
rw [IsTightMeasureSet_iff_exists_isCompact_measure_compl_le]
intro ε hε
let r := μ Set.univ
cases lt_or_ge ε r with
| inl
hεr =>
have hεr' : r - ε < r := ENNReal.sub_lt_self (measure_ne_top μ _) (zero_le'.trans_lt hεr).ne' hε.ne'
obtain ⟨K, _, ⟨hK_compact, hK_closed⟩, hKμ⟩ := h .univ (r - ε) hεr'
refine ⟨K, hK_compact, ?_⟩
simp only [mem_singleton_iff, forall_eq]
rw [measure_compl hK_closed.measurableSet (measure_ne_top μ _), tsub_le_iff_right]
rw [ENNReal.sub_lt_iff_lt_right (ne_top_of_lt hεr) hεr.le, add_comm] at hKμ
exact hKμ.le
| inr hεr => exact ⟨∅, isCompact_empty, by simpa⟩
