English
If μ is regular, then for every compact K, μ.measure(↑K) = μ(K).
Русский
Если μ регулярен, то для каждого компактного K верно μ.measure(↑K) = μ(K).
LaTeX
$$$$\\forall K \\in \\mathrm{Compacts}(G): \\mu.measure(K) = μ(K).$$$$
Lean4
/-- If `μ` is a regular content, then the measure induced by `μ` will agree with `μ`
on compact sets. -/
theorem measure_eq_content_of_regular (H : MeasureTheory.Content.ContentRegular μ) (K : TopologicalSpace.Compacts G) :
μ.measure ↑K = μ K := by
refine le_antisymm ?_ ?_
· apply ENNReal.le_of_forall_pos_le_add
intro ε εpos _
obtain ⟨K', K'_hyp⟩ := contentRegular_exists_compact μ H K (ne_bot_of_gt εpos)
calc
μ.measure ↑K ≤ μ.measure (interior ↑K') := measure_mono K'_hyp.1
_ ≤ μ K' := by
rw [μ.measure_apply (IsOpen.measurableSet isOpen_interior)]
exact μ.outerMeasure_interior_compacts K'
_ ≤ μ K + ε := K'_hyp.right
·
calc
μ K ≤ μ ⟨closure K, K.2.closure⟩ := μ.mono _ _ subset_closure
_ ≤ μ.measure (closure K) := by
rw [μ.measure_apply (isClosed_closure.measurableSet)]
exact μ.le_outerMeasure_compacts _
_ = μ.measure K := K.2.measure_closure _
