Integrals of continuous functions with respect to regular measures #
When a measure is regular, one may express the measure of compact sets and of open sets in terms of the integral of continuous functions equal to 1 on the compact set, or to 0 outside of the open set respectively.
theorem
IsCompact.measure_eq_biInf_integral_hasCompactSupport
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
[BorelSpace X]
{k : Set X}
(hk : IsCompact k)
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsFiniteMeasureOnCompacts μ]
[μ.InnerRegularCompactLTTop]
[LocallyCompactSpace X]
[RegularSpace X]
:
μ k = ⨅ (f : X → ℝ),
⨅ (_ : Continuous f),
⨅ (_ : HasCompactSupport f), ⨅ (_ : Set.EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ)
In a locally compact regular space with an inner regular measure, the measure of a compact
set k is the infimum of the integrals of compactly supported functions equal to 1 on k.
theorem
IsOpen.measure_eq_biSup_integral_continuous
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
[BorelSpace X]
[T2Space X]
{U : Set X}
(hU : IsOpen U)
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsFiniteMeasure μ]
[μ.InnerRegularCompactLTTop]
[NormalSpace X]
:
Given an inner regular finite measure, the measure of an open set is the supremum of the
integrals of nonnegative continuous functions supported in this set and bounded by 1.