mathlib3 documentation

measure_theory.decomposition.radon_nikodym

Radon-Nikodym theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the Radon-Nikodym theorem. The Radon-Nikodym theorem states that, given measures μ, ν, if have_lebesgue_decomposition μ ν, then μ is absolutely continuous with respect to ν if and only if there exists a measurable function f : α → ℝ≥0∞ such that μ = fν. In particular, we have f = rn_deriv μ ν.

The Radon-Nikodym theorem will allow us to define many important concepts in probability theory, most notably probability cumulative functions. It could also be used to define the conditional expectation of a real function, but we take a different approach (see the file measure_theory/function/conditional_expectation).

Main results #

Tags #

Radon-Nikodym theorem

The Radon-Nikodym theorem: Given two measures μ and ν, if have_lebesgue_decomposition μ ν, then μ is absolutely continuous to ν if and only if ν.with_density (rn_deriv μ ν) = μ.