# mathlibdocumentation

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 #

• measure_theory.measure.absolutely_continuous_iff_with_density_rn_deriv_eq : the Radon-Nikodym theorem
• measure_theory.signed_measure.absolutely_continuous_iff_with_density_rn_deriv_eq : the Radon-Nikodym theorem for signed measures

## Tags #

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 μ ν) = μ.