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

source
theorem measure_theory.measure.with_density_rn_deriv_eq {α : Type u_1} {m : measurable_space α} (μ ν : measure_theory.measure α) [μ.have_lebesgue_decomposition ν] (h : μ.absolutely_continuous ν) :
ν.with_density (μ.rn_deriv ν) = μ
source
theorem measure_theory.measure.absolutely_continuous_iff_with_density_rn_deriv_eq {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [μ.have_lebesgue_decomposition ν] :
μ.absolutely_continuous ν ↔ ν.with_density (μ.rn_deriv ν) = μ

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

source
theorem measure_theory.measure.with_density_rn_deriv_to_real_eq {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} [measure_theory.is_finite_measure μ] [μ.have_lebesgue_decomposition ν] (h : μ.absolutely_continuous ν) {i : set α} (hi : measurable_set i) :
∫ (x : α) in i, (μ.rn_deriv ν x).to_real ∂ν = (⇑μ i).to_real
source
theorem measure_theory.signed_measure.with_densityᵥ_rn_deriv_eq {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] (h : measure_theory.vector_measure.absolutely_continuous s μ.to_ennreal_vector_measure) :
μ.with_densityᵥ (s.rn_deriv μ) = s
source
theorem measure_theory.signed_measure.absolutely_continuous_iff_with_densityᵥ_rn_deriv_eq {α : Type u_1} {m : measurable_space α} (s : measure_theory.signed_measure α) (μ : measure_theory.measure α) [measure_theory.sigma_finite μ] :
measure_theory.vector_measure.absolutely_continuous s μ.to_ennreal_vector_measure ↔ μ.with_densityᵥ (s.rn_deriv μ) = s

The Radon-Nikodym theorem for signed measures.