Radon–Nikodym densities and polar decomposition of scalar measures

For a scalar measure μ over an RCLike field and a sigma-finite positive measure ν, absolute continuity of μ.variation with respect to ν gives an integrable density scalarRNDeriv μ ν. It is assembled from the native signed Radon–Nikodym derivatives of the real and imaginary parts and agrees with the native derivatives over ℝ and ℂ.

The variation has density ‖scalarRNDeriv μ ν‖ₑ. In particular, relative to its own variation every scalar measure has a density of norm one almost everywhere. This polar decomposition supplies the phase used to recover total variation from integration pairings. No topology or regularity assumption on the underlying measurable space is needed.

References

• W. Rudin, Real and Complex Analysis, 3rd ed., Chapter 6, Radon–Nikodym theorem and polar decomposition of a complex measure.

The construction uses Mathlib's SignedMeasure.rnDeriv, SignedMeasure.withDensityᵥ_rnDeriv_eq, and Measure.variation_withDensityᵥ.

theorem MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq_of_variation {X : Type u_1} [MeasurableSpace X] (s : SignedMeasure X) (ν : Measure X) [SigmaFinite ν] (h : (VectorMeasure.variation s).AbsolutelyContinuous ν) : ν.withDensityᵥ (s.rnDeriv ν) = s

A signed measure is reconstructed by its Radon–Nikodym density when its variation is absolutely continuous with respect to the sigma-finite reference measure.

noncomputable def MeasureTheory.VectorMeasure.scalarRNDeriv {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (ν : Measure X) : X → 𝕜

The scalar Radon–Nikodym density, formed from the signed derivatives of the real and imaginary parts. It reconstructs the measure when its variation is absolutely continuous with respect to the sigma-finite reference measure.

theorem MeasureTheory.VectorMeasure.scalarRNDeriv_def {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (ν : Measure X) : μ.scalarRNDeriv ν = fun (x : X) => ↑((scalarMeasureRealPart μ).rnDeriv ν x) + RCLike.I * ↑((scalarMeasureImagPart μ).rnDeriv ν x)

Formula for the scalar density in terms of native signed derivatives.

theorem MeasureTheory.VectorMeasure.measurable_scalarRNDeriv {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] (μ : VectorMeasure X 𝕜) (ν : Measure X) : Measurable (μ.scalarRNDeriv ν)

The scalar Radon–Nikodym density is measurable.

theorem MeasureTheory.VectorMeasure.integrable_scalarRNDeriv {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (ν : Measure X) : Integrable (μ.scalarRNDeriv ν) ν

The scalar Radon–Nikodym density is integrable, even without absolute continuity.

@[simp]

theorem MeasureTheory.VectorMeasure.scalarRNDeriv_real {X : Type u_1} [MeasurableSpace X] (μ : SignedMeasure X) (ν : Measure X) : scalarRNDeriv μ ν = μ.rnDeriv ν

Over the real field, the scalar density is the native signed density.

@[simp]

theorem MeasureTheory.VectorMeasure.scalarRNDeriv_complex {X : Type u_1} [MeasurableSpace X] (μ : ComplexMeasure X) (ν : Measure X) : scalarRNDeriv μ ν = μ.rnDeriv ν

Over the complex field, the scalar density is the native complex density.

theorem MeasureTheory.VectorMeasure.withDensityᵥ_scalarRNDeriv {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (ν : Measure X) [SigmaFinite ν] (hμν : μ.variation.AbsolutelyContinuous ν) : ν.withDensityᵥ (μ.scalarRNDeriv ν) = μ

Scalar Radon–Nikodym theorem. If the variation of a scalar measure is absolutely continuous with respect to a sigma-finite measure, its scalar density reconstructs it.

theorem MeasureTheory.VectorMeasure.variation_eq_withDensity_enorm_scalarRNDeriv {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (ν : Measure X) [SigmaFinite ν] (hμν : μ.variation.AbsolutelyContinuous ν) : μ.variation = ν.withDensity fun (x : X) => ‖μ.scalarRNDeriv ν x‖ₑ

The variation of a scalar measure is obtained by taking the pointwise norm of its Radon–Nikodym density.

theorem MeasureTheory.VectorMeasure.withDensityᵥ_eq_iff_ae_eq_scalarRNDeriv {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) (ν : Measure X) [SigmaFinite ν] (hμν : μ.variation.AbsolutelyContinuous ν) {f : X → 𝕜} (hf : Integrable f ν) : ν.withDensityᵥ f = μ ↔ f =ᵐ[ν] μ.scalarRNDeriv ν

An integrable function represents a scalar measure exactly when it agrees almost everywhere with its scalar Radon–Nikodym density.

theorem MeasureTheory.VectorMeasure.ae_norm_scalarRNDeriv_variation_eq_one {X : Type u_1} {𝕜 : Type u_2} [MeasurableSpace X] [RCLike 𝕜] (μ : VectorMeasure X 𝕜) : ∀ᵐ (x : X) ∂μ.variation, ‖μ.scalarRNDeriv μ.variation x‖ = 1

The density of a scalar measure relative to its own variation has norm one almost everywhere. This includes the zero measure, whose almost-everywhere assertion is vacuous.