# mathlibdocumentation

measure_theory.decomposition.radon_nikodym

# Radon-Nikodym theorem #

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 #

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

theorem measure_theory.measure.with_density_rn_deriv_to_real_eq {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (h : μ.absolutely_continuous ν) {i : set α} (hi : measurable_set i) :
(x : α) in i, (μ.rn_deriv ν x).to_real ν = (μ i).to_real

The Radon-Nikodym theorem for signed measures.