Densities of norm one from lower bounds on open sets #
Let μ be a locally finite measure on a second countable topological space and let g be a
weight with g ≤ 1 almost everywhere. If every open set V satisfies μ V ≤ ∫⁻ x in V, g x ∂μ,
then g = 1 almost everywhere (TauCeti.ae_eq_one_of_measure_le_setLIntegral). This is the last
step of a polar decomposition T = σ ‖T‖: once the density σ of a functional with respect to its
variation measure ‖T‖ has norm at most one, testing the supremum that defines ‖T‖ V against the
representation gives the lower bound on open sets, so ‖σ‖ = 1 almost everywhere.
References #
- L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §1.8 (the polar decomposition in the Riesz representation theorem).
theorem
TauCeti.ae_eq_one_of_measure_le_setLIntegral
{X : Type u_1}
[TopologicalSpace X]
[SecondCountableTopology X]
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{g : X → ENNReal}
(hg1 : ∀ᵐ (x : X) ∂μ, g x ≤ 1)
(hg : ∀ (V : Set X), IsOpen V → μ V ≤ ∫⁻ (x : X) in V, g x ∂μ)
:
A weight g ≤ 1 whose integral over every open set V is at least μ V equals one almost
everywhere, for a locally finite measure μ on a second countable space.