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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) : MeasureTheory.Measure α

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

• μ.withDensity f = MeasureTheory.Measure.ofMeasurable (fun (s : Set α) (x : MeasurableSet s) => ∫⁻ (a : α) in s, f a ∂μ) ⋯ ⋯

@[simp]

theorem MeasureTheory.withDensity_apply {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {s : Set α} (hs : MeasurableSet s) : ↑↑(μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ

theorem MeasureTheory.withDensity_apply_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) (s : Set α) : ∫⁻ (a : α) in s, f a ∂μ ≤ ↑↑(μ.withDensity f) 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 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (f : α → ENNReal) (s : Set α) : ↑↑(μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ

@[simp]

theorem MeasureTheory.withDensity_zero_left {α : Type u_1} {m0 : MeasurableSpace α} (f : α → ENNReal) : 0.withDensity f = 0

theorem MeasureTheory.withDensity_congr_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {g : α → ENNReal} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) : μ.withDensity f = μ.withDensity g

theorem MeasureTheory.withDensity_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {g : α → ENNReal} (hfg : f ≤ᶠ[MeasureTheory.Measure.ae μ] g) : μ.withDensity f ≤ μ.withDensity g

theorem MeasureTheory.withDensity_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) (g : α → ENNReal) : μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

theorem MeasureTheory.withDensity_add_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) {g : α → ENNReal} (hg : Measurable g) : μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

theorem MeasureTheory.withDensity_add_measure {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (f : α → ENNReal) : (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f

theorem MeasureTheory.withDensity_sum {α : Type u_1} {ι : Type u_2} {m : MeasurableSpace α} (μ : ι → MeasureTheory.Measure α) (f : α → ENNReal) : (MeasureTheory.Measure.sum μ).withDensity f = MeasureTheory.Measure.sum fun (n : ι) => (μ n).withDensity f

theorem MeasureTheory.withDensity_smul {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) {f : α → ENNReal} (hf : Measurable f) : μ.withDensity (r • f) = r • μ.withDensity f

theorem MeasureTheory.withDensity_smul' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal) (hr : r ≠ ⊤) : μ.withDensity (r • f) = r • μ.withDensity f

theorem MeasureTheory.withDensity_smul_measure {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (r : ENNReal) (f : α → ENNReal) : (r • μ).withDensity f = r • μ.withDensity f

theorem MeasureTheory.isFiniteMeasure_withDensity {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : ∫⁻ (a : α), f a ∂μ ≠ ⊤) : MeasureTheory.IsFiniteMeasure (μ.withDensity f)

theorem MeasureTheory.withDensity_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) : MeasureTheory.Measure.AbsolutelyContinuous (μ.withDensity f) μ

@[simp]

theorem MeasureTheory.withDensity_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : μ.withDensity 0 = 0

@[simp]

theorem MeasureTheory.withDensity_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} : μ.withDensity 1 = μ

@[simp]

theorem MeasureTheory.withDensity_const {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (c : ENNReal) : (μ.withDensity fun (x : α) => c) = c • μ

theorem MeasureTheory.withDensity_tsum {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (h : ∀ (i : ℕ), Measurable (f i)) : μ.withDensity (∑' (n : ℕ), f n) = MeasureTheory.Measure.sum fun (n : ℕ) => μ.withDensity (f n)

theorem MeasureTheory.withDensity_indicator {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ENNReal) : μ.withDensity (Set.indicator s f) = (μ.restrict s).withDensity f

theorem MeasureTheory.withDensity_indicator_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) : μ.withDensity (Set.indicator s 1) = μ.restrict s

theorem MeasureTheory.withDensity_ofReal_mutuallySingular {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : Measurable f) : MeasureTheory.Measure.MutuallySingular (μ.withDensity fun (x : α) => ENNReal.ofReal (f x)) (μ.withDensity fun (x : α) => ENNReal.ofReal (-f x))

theorem MeasureTheory.restrict_withDensity {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (f : α → ENNReal) : (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

theorem MeasureTheory.restrict_withDensity' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (s : Set α) (f : α → ENNReal) : (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

theorem MeasureTheory.trim_withDensity {α : Type u_1} {m : MeasurableSpace α} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal} (hf : Measurable f) : (μ.withDensity f).trim hm = (μ.trim hm).withDensity f

theorem MeasureTheory.Measure.MutuallySingular.withDensity {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ENNReal} (h : MeasureTheory.Measure.MutuallySingular μ ν) : MeasureTheory.Measure.MutuallySingular (μ.withDensity f) ν

theorem MeasureTheory.withDensity_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (h : μ.withDensity f = 0) : f =ᶠ[MeasureTheory.Measure.ae μ] 0

@[simp]

theorem MeasureTheory.withDensity_eq_zero_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) : μ.withDensity f = 0 ↔ f =ᶠ[MeasureTheory.Measure.ae μ] 0

theorem MeasureTheory.withDensity_apply_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α} (hf : Measurable f) : ↑↑(μ.withDensity f) s = 0 ↔ ↑↑μ ({x : α | f x ≠ 0} ∩ s) = 0

theorem MeasureTheory.ae_withDensity_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {f : α → ENNReal} (hf : Measurable f) : (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x

theorem MeasureTheory.ae_withDensity_iff_ae_restrict {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {f : α → ENNReal} (hf : Measurable f) : (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}, p x

theorem MeasureTheory.aemeasurable_withDensity_ennreal_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → NNReal} (hf : Measurable f) {g : α → ENNReal} : AEMeasurable g (μ.withDensity fun (x : α) => ↑(f x)) ↔ AEMeasurable (fun (x : α) => ↑(f x) * g x) μ

theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} (h_mf : Measurable f) {g : α → ENNReal} : Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} {g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) {s : Set α} (hs : MeasurableSet s) : ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ

theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {g : α → ENNReal} (hg : AEMeasurable g (μ.withDensity f)) : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (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.set_lintegral_withDensity_eq_lintegral_mul₀' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {g : α → ENNReal} (hg : AEMeasurable g (μ.withDensity f)) {s : Set α} (hs : MeasurableSet s) : ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {g : α → ENNReal} (hg : AEMeasurable g μ) : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

theorem MeasureTheory.set_lintegral_withDensity_eq_lintegral_mul₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) {g : α → ENNReal} (hg : AEMeasurable g μ) {s : Set α} (hs : MeasurableSet s) : ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

theorem MeasureTheory.lintegral_withDensity_le_lintegral_mul {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} (f_meas : Measurable f) (g : α → ENNReal) : ∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ

theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} (f_meas : Measurable f) (hf : ∀ᵐ (x : α) ∂μ, f x < ⊤) (g : α → ENNReal) : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} (f_meas : Measurable f) (g : α → ENNReal) {s : Set α} (hs : MeasurableSet s) (hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤) : ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} (hf : AEMeasurable f μ) (h'f : ∀ᵐ (x : α) ∂μ, f x < ⊤) (g : α → ENNReal) : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ

theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} {s : Set α} (hf : AEMeasurable f (μ.restrict s)) (g : α → ENNReal) (hs : MeasurableSet s) (h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤) : ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀' {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] {f : α → ENNReal} (s : Set α) (hf : AEMeasurable f (μ.restrict s)) (g : α → ENNReal) (h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤) : ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

theorem MeasureTheory.withDensity_mul₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : μ.withDensity (f * g) = (μ.withDensity f).withDensity g

theorem MeasureTheory.withDensity_mul {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal} {g : α → ENNReal} (hf : Measurable f) (hg : Measurable g) : μ.withDensity (f * g) = (μ.withDensity f).withDensity g

theorem MeasureTheory.withDensity_inv_same_le {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) : (μ.withDensity f).withDensity f⁻¹ ≤ μ

theorem MeasureTheory.withDensity_inv_same₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : ((μ.withDensity f).withDensity fun (x : α) => (f x)⁻¹) = μ

theorem MeasureTheory.withDensity_inv_same {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : Measurable f) (hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : ((μ.withDensity f).withDensity fun (x : α) => (f x)⁻¹) = μ

theorem MeasureTheory.withDensity_absolutelyContinuous' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) (hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : MeasureTheory.Measure.AbsolutelyContinuous μ (μ.withDensity f)

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

theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ∃ (ν : MeasureTheory.Measure α), MeasureTheory.IsFiniteMeasure ν ∧ MeasureTheory.Measure.AbsolutelyContinuous μ ν

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

theorem MeasureTheory.SigmaFinite.withDensity {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → NNReal} (hf : AEMeasurable f μ) : MeasureTheory.SigmaFinite (μ.withDensity fun (x : α) => ↑(f x))

theorem MeasureTheory.SigmaFinite.withDensity_of_ne_top' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ENNReal} (hf : AEMeasurable f μ) (hf_ne_top : ∀ (x : α), f x ≠ ⊤) : MeasureTheory.SigmaFinite (μ.withDensity f)

theorem MeasureTheory.SigmaFinite.withDensity_of_ne_top {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ENNReal} (hf : AEMeasurable f μ) (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : MeasureTheory.SigmaFinite (μ.withDensity f)

theorem MeasureTheory.SigmaFinite.withDensity_ofReal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ℝ} (hf : AEMeasurable f μ) : MeasureTheory.SigmaFinite (μ.withDensity fun (x : α) => ENNReal.ofReal (f x))

theorem MeasureTheory.IsLocallyFiniteMeasure.withDensity_coe {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [OpensMeasurableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → NNReal} (hf : Continuous f) : MeasureTheory.IsLocallyFiniteMeasure (μ.withDensity fun (x : α) => ↑(f x))

theorem MeasureTheory.IsLocallyFiniteMeasure.withDensity_ofReal {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [TopologicalSpace α] [OpensMeasurableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : α → ℝ} (hf : Continuous f) : MeasureTheory.IsLocallyFiniteMeasure (μ.withDensity fun (x : α) => ENNReal.ofReal (f x))