Densities against a common measure, and normalizing a density

Let λ be a measure and let ν₁ i, ν₂ i be finitely many pairs of measures on a σ-compact topological space, all finite on compact sets. The sum ρ = λ + ∑ i, (ν₁ i + ν₂ i) is finite on compact sets and dominates all of them, so each signed difference ν₁ i - ν₂ i has a real density dν₁ i/dρ - dν₂ i/dρ with respect to ρ, integrable on compact sets (MeasureTheory.Measure.exists_common_density_sub).

This is how a vector-valued functional, given componentwise as differences of measures, is represented by a single vector-valued density against one measure ρ which also dominates a prescribed variation measure λ. Its pointwise norm is then compared with the density of λ with respect to ρ, as in a polar decomposition.

The file also contains the normalization step of a polar decomposition (MeasureTheory.Measure.exists_norm_le_one_toReal_rnDeriv_smul_eq): a measurable field g dominated by the density dλ/dρ of λ ≪ ρ agrees ρ-almost everywhere with (dλ/dρ).toReal • σ, where σ is a measurable field of norm at most one λ-almost everywhere. This σ is the unit field of the polar decomposition.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §1.8 (the Riesz representation theorem for vector-valued functionals).

theorem MeasureTheory.Measure.exists_common_density_sub {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [SigmaCompactSpace X] [MeasurableSpace X] [Finite ι] (lam : Measure X) [IsFiniteMeasureOnCompacts lam] (ν₁ ν₂ : ι → Measure X) [∀ (i : ι), IsFiniteMeasureOnCompacts (ν₁ i)] [∀ (i : ι), IsFiniteMeasureOnCompacts (ν₂ i)] : ∃ (ρ : Measure X), IsFiniteMeasureOnCompacts ρ ∧ lam.AbsolutelyContinuous ρ ∧ ∃ (f : ι → X → ℝ), (∀ (i : ι), Measurable (f i)) ∧ (∀ (i : ι) (K : Set X), IsCompact K → IntegrableOn (f i) K ρ) ∧ ∀ (i : ι) (ψ : X → ℝ), Integrable ψ (ν₁ i) → Integrable ψ (ν₂ i) → Integrable (fun (x : X) => f i x * ψ x) ρ ∧ ∫ (x : X), f i x * ψ x ∂ρ = ∫ (x : X), ψ x ∂ν₁ i - ∫ (x : X), ψ x ∂ν₂ i

Common densities. For a measure λ and finitely many pairs of measures ν₁ i, ν₂ i, all finite on compact sets of a σ-compact space, there is a measure ρ, finite on compact sets and dominating λ, with respect to which each signed difference ν₁ i - ν₂ i has a measurable density f i, integrable on compact sets: ∫ ψ dν₁ i - ∫ ψ dν₂ i = ∫ f i ψ dρ for every ψ integrable for ν₁ i and ν₂ i.

theorem MeasureTheory.Measure.exists_norm_le_one_toReal_rnDeriv_smul_eq {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {lam ρ : Measure X} [SigmaFinite lam] (hlam : lam.AbsolutelyContinuous ρ) {g : X → E} (hgm : Measurable g) (hbound : ∀ᵐ (x : X) ∂ρ, ‖g x‖ₑ ≤ lam.rnDeriv ρ x) : ∃ (σ : X → E), Measurable σ ∧ (∀ᵐ (x : X) ∂lam, ‖σ x‖ ≤ 1) ∧ ∀ᵐ (x : X) ∂ρ, (lam.rnDeriv ρ x).toReal • σ x = g x

Normalizing a density. If a measurable field g has pointwise norm at most the density dλ/dρ of a measure λ ≪ ρ (up to a ρ-null set), then g agrees ρ-almost everywhere with (dλ/dρ).toReal • σ for a measurable field σ of norm at most one λ-almost everywhere.