# Documentation

Mathlib.MeasureTheory.Measure.WithDensity

# Measure with a given density with respect to another measure #

For a measure μ on α and a function f : α → ℝ≥0∞, we define a new measure μ.withDensity f. On a measurable set s, that measure has value ∫⁻ a in s, f a ∂μ.

An important result about withDensity is the Radon-Nikodym theorem. It states that, given measures μ, ν, if HaveLebesgueDecomposition μ ν then μ is absolutely continuous with respect to ν if and only if there exists a measurable function f : α → ℝ≥0∞ such that μ = ν.withDensity f. See MeasureTheory.Measure.absolutelyContinuous_iff_withDensity_rnDeriv_eq.

noncomputable def MeasureTheory.Measure.withDensity {α : Type u_1} {m : } (μ : ) (f : αENNReal) :

Given a measure μ : Measure α and a function f : α → ℝ≥0∞, μ.withDensity f is the measure such that for a measurable set s we have μ.withDensity f s = ∫⁻ a in s, f a ∂μ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasureTheory.withDensity_apply {α : Type u_1} {m0 : } {μ : } (f : αENNReal) {s : Set α} (hs : ) :
s = ∫⁻ (a : α) in s, f aμ
theorem MeasureTheory.withDensity_apply_le {α : Type u_1} {m0 : } {μ : } (f : αENNReal) (s : Set α) :
∫⁻ (a : α) in s, f aμ s

In the next theorem, the s-finiteness assumption is necessary. Here is a counterexample without this assumption. Let α be an uncountable space, let x₀ be some fixed point, and consider the σ-algebra made of those sets which are countable and do not contain x₀, and of their complements. This is the σ-algebra generated by the sets {x} for x ≠ x₀. Define a measure equal to +∞ on nonempty sets. Let s = {x₀} and f the indicator of sᶜ. Then

• ∫⁻ a in s, f a ∂μ = 0. Indeed, consider a simple function g ≤ f. It vanishes on s. Then ∫⁻ a in s, g a ∂μ = 0. Taking the supremum over g gives the claim.
• μ.withDensity f s = +∞. Indeed, this is the infimum of μ.withDensity f t over measurable sets t containing s. As s is not measurable, such a set t contains a point x ≠ x₀. Then μ.withDensity f t ≥ μ.withDensity f {x} = ∫⁻ a in {x}, f a ∂μ = μ {x} = +∞. One checks that μ.withDensity f = μ, while μ.restrict s gives zero mass to sets not containing x₀, and infinite mass to those that contain it.
theorem MeasureTheory.withDensity_apply' {α : Type u_1} {m0 : } {μ : } (f : αENNReal) (s : Set α) :
s = ∫⁻ (a : α) in s, f aμ
@[simp]
theorem MeasureTheory.withDensity_zero_left {α : Type u_1} {m0 : } (f : αENNReal) :
theorem MeasureTheory.withDensity_congr_ae {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (h : ) :
theorem MeasureTheory.withDensity_mono {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hfg : ) :
theorem MeasureTheory.withDensity_add_left {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) (g : αENNReal) :
theorem MeasureTheory.withDensity_add_right {α : Type u_1} {m0 : } {μ : } (f : αENNReal) {g : αENNReal} (hg : ) :
theorem MeasureTheory.withDensity_add_measure {α : Type u_1} {m : } (μ : ) (ν : ) (f : αENNReal) :
theorem MeasureTheory.withDensity_sum {α : Type u_1} {ι : Type u_2} {m : } (μ : ) (f : αENNReal) :
= MeasureTheory.Measure.sum fun (n : ι) =>
theorem MeasureTheory.withDensity_smul {α : Type u_1} {m0 : } {μ : } (r : ENNReal) {f : αENNReal} (hf : ) :
theorem MeasureTheory.withDensity_smul' {α : Type u_1} {m0 : } {μ : } (r : ENNReal) (f : αENNReal) (hr : r ) :
theorem MeasureTheory.withDensity_smul_measure {α : Type u_1} {m0 : } {μ : } (r : ENNReal) (f : αENNReal) :
theorem MeasureTheory.isFiniteMeasure_withDensity {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ∫⁻ (a : α), f aμ ) :
theorem MeasureTheory.withDensity_absolutelyContinuous {α : Type u_1} {m : } (μ : ) (f : αENNReal) :
@[simp]
theorem MeasureTheory.withDensity_zero {α : Type u_1} {m0 : } {μ : } :
@[simp]
theorem MeasureTheory.withDensity_one {α : Type u_1} {m0 : } {μ : } :
@[simp]
theorem MeasureTheory.withDensity_const {α : Type u_1} {m0 : } {μ : } (c : ENNReal) :
(MeasureTheory.Measure.withDensity μ fun (x : α) => c) = c μ
theorem MeasureTheory.withDensity_tsum {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (h : ∀ (i : ), Measurable (f i)) :
theorem MeasureTheory.withDensity_indicator {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) (f : αENNReal) :
theorem MeasureTheory.withDensity_indicator_one {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) :
theorem MeasureTheory.restrict_withDensity {α : Type u_1} {m0 : } {μ : } {s : Set α} (hs : ) (f : αENNReal) :
theorem MeasureTheory.restrict_withDensity' {α : Type u_1} {m0 : } {μ : } (s : Set α) (f : αENNReal) :
theorem MeasureTheory.Measure.MutuallySingular.withDensity {α : Type u_1} {m0 : } {μ : } {ν : } {f : αENNReal} :
theorem MeasureTheory.withDensity_eq_zero {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) (h : ) :
@[simp]
theorem MeasureTheory.withDensity_eq_zero_iff {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) :
theorem MeasureTheory.withDensity_apply_eq_zero {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {s : Set α} (hf : ) :
s = 0 μ ({x : α | f x 0} s) = 0
theorem MeasureTheory.ae_withDensity_iff {α : Type u_1} {m0 : } {μ : } {p : αProp} {f : αENNReal} (hf : ) :
(∀ᵐ (x : α) ∂, p x) ∀ᵐ (x : α) ∂μ, f x 0p x
theorem MeasureTheory.ae_withDensity_iff_ae_restrict {α : Type u_1} {m0 : } {μ : } {p : αProp} {f : αENNReal} (hf : ) :
(∀ᵐ (x : α) ∂, p x) ∀ᵐ (x : α) ∂MeasureTheory.Measure.restrict μ {x : α | f x 0}, p x
theorem MeasureTheory.aemeasurable_withDensity_ennreal_iff {α : Type u_1} {m0 : } {μ : } {f : αNNReal} (hf : ) {g : αENNReal} :
AEMeasurable fun (x : α) => (f x) * g x
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (h_mf : ) {g : αENNReal} :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ

This is Exercise 1.2.1 from [tao2010]. It allows you to express integration of a measurable function with respect to (μ.withDensity f) as an integral with respect to μ, called the base measure. μ is often the Lebesgue measure, and in this circumstance f is the probability density function, and (μ.withDensity f) represents any continuous random variable as a probability measure, such as the uniform distribution between 0 and 1, the Gaussian distribution, the exponential distribution, the Beta distribution, or the Cauchy distribution (see Section 2.4 of [wasserman2004]). Thus, this method shows how to one can calculate expectations, variances, and other moments as a function of the probability density function.

theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) {s : Set α} (hs : ) :
∫⁻ (x : α) in s, g x = ∫⁻ (x : α) in s, (f * g) xμ
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀' {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) {g : αENNReal} (hg : ) :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ

The Lebesgue integral of g with respect to the measure μ.withDensity f coincides with the integral of f * g. This version assumes that g is almost everywhere measurable. For a version without conditions on g but requiring that f is almost everywhere finite, see lintegral_withDensity_eq_lintegral_mul_non_measurable

theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀ {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) {g : αENNReal} (hg : ) :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ
theorem MeasureTheory.lintegral_withDensity_le_lintegral_mul {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (f_meas : ) (g : αENNReal) :
∫⁻ (a : α), g a ∫⁻ (a : α), (f * g) aμ
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (f_meas : ) (hf : ∀ᵐ (x : α) ∂μ, f x < ) (g : αENNReal) :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ
theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (f_meas : ) (g : αENNReal) {s : Set α} (hs : ) (hf : ∀ᵐ (x : α) ∂, f x < ) :
∫⁻ (a : α) in s, g a = ∫⁻ (a : α) in s, (f * g) aμ
theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀ {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (hf : ) (h'f : ∀ᵐ (x : α) ∂μ, f x < ) (g : αENNReal) :
∫⁻ (a : α), g a = ∫⁻ (a : α), (f * g) aμ
theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀ {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} {s : Set α} (hf : ) (g : αENNReal) (hs : ) (h'f : ∀ᵐ (x : α) ∂, f x < ) :
∫⁻ (a : α) in s, g a = ∫⁻ (a : α) in s, (f * g) aμ
theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀' {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} (s : Set α) (hf : ) (g : αENNReal) (h'f : ∀ᵐ (x : α) ∂, f x < ) :
∫⁻ (a : α) in s, g a = ∫⁻ (a : α) in s, (f * g) aμ
theorem MeasureTheory.withDensity_mul₀ {α : Type u_1} {m0 : } {μ : } {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) :
theorem MeasureTheory.withDensity_mul {α : Type u_1} {m0 : } (μ : ) {f : αENNReal} {g : αENNReal} (hf : ) (hg : ) :
theorem MeasureTheory.withDensity_inv_same_le {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) :
theorem MeasureTheory.withDensity_inv_same₀ {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) (hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x 0) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ) :
(MeasureTheory.Measure.withDensity fun (x : α) => (f x)⁻¹) = μ
theorem MeasureTheory.withDensity_inv_same {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) (hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x 0) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ) :
(MeasureTheory.Measure.withDensity fun (x : α) => (f x)⁻¹) = μ
theorem MeasureTheory.withDensity_absolutelyContinuous' {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) (hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x 0) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ) :

If f is almost everywhere positive and finite, then μ ≪ μ.withDensity f. See also withDensity_absolutelyContinuous for the reverse direction, which always holds.

A sigma-finite measure is absolutely continuous with respect to some finite measure.

theorem MeasureTheory.SigmaFinite.withDensity {α : Type u_1} {m0 : } {μ : } {f : αNNReal} (hf : ) :
theorem MeasureTheory.SigmaFinite.withDensity_of_ne_top' {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) (hf_ne_top : ∀ (x : α), f x ) :
theorem MeasureTheory.SigmaFinite.withDensity_of_ne_top {α : Type u_1} {m0 : } {μ : } {f : αENNReal} (hf : ) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ) :
theorem MeasureTheory.SigmaFinite.withDensity_ofReal {α : Type u_1} {m0 : } {μ : } {f : α} (hf : ) :
theorem MeasureTheory.IsLocallyFiniteMeasure.withDensity_coe {α : Type u_1} {m0 : } {μ : } [] {f : αNNReal} (hf : ) :