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 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (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
Instances For
    @[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

    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μ
    theorem MeasureTheory.withDensity_congr_ae {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} {g : αENNReal} (h : f =ᵐ[μ] g) :
    μ.withDensity f = μ.withDensity g
    theorem MeasureTheory.withDensity_mono {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} {g : αENNReal} (hfg : f ≤ᵐ[μ] 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μ ) :
    theorem MeasureTheory.withDensity_absolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : αENNReal) :
    (μ.withDensity f).AbsolutelyContinuous μ
    @[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 (s.indicator f) = (μ.restrict s).withDensity f
    theorem MeasureTheory.withDensity_indicator_one {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) :
    μ.withDensity (s.indicator 1) = μ.restrict s
    theorem MeasureTheory.withDensity_ofReal_mutuallySingular {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α} (hf : Measurable f) :
    (μ.withDensity fun (x : α) => ENNReal.ofReal (f x)).MutuallySingular (μ.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 : μ.MutuallySingular ν) :
    (μ.withDensity f).MutuallySingular ν
    theorem MeasureTheory.withDensity_eq_zero {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hf : AEMeasurable f μ) (h : μ.withDensity f = 0) :
    f =ᵐ[μ] 0
    @[simp]
    theorem MeasureTheory.withDensity_eq_zero_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} (hf : AEMeasurable f μ) :
    μ.withDensity f = 0 f =ᵐ[μ] 0
    theorem MeasureTheory.withDensity_apply_eq_zero' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : αENNReal} {s : Set α} (hf : AEMeasurable f μ) :
    (μ.withDensity f) s = 0 μ ({x : α | f x 0} s) = 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 : AEMeasurable f μ) :
    (∀ᵐ (x : α) ∂μ.withDensity f, p x) ∀ᵐ (x : α) ∂μ, f x 0p x
    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 0p x
    theorem MeasureTheory.ae_withDensity_iff_ae_restrict' {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : αProp} {f : αENNReal} (hf : AEMeasurable f μ) :
    (∀ᵐ (x : α) ∂μ.withDensity f, p x) ∀ᵐ (x : α) ∂μ.restrict {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 : AEMeasurable f μ) {g : αENNReal} :
    AEMeasurable g (μ.withDensity fun (x : α) => (f x)) AEMeasurable (fun (x : α) => (f x) * g 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.setLIntegral_withDensity_eq_setLIntegral_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μ
    @[deprecated MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul]
    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μ

    Alias of MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul.

    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.setLIntegral_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μ
    @[deprecated MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀']
    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μ

    Alias of MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀'.

    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.setLIntegral_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μ
    @[deprecated MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀]
    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μ

    Alias of MeasureTheory.setLIntegral_withDensity_eq_lintegral_mul₀.

    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.setLIntegral_withDensity_eq_setLIntegral_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μ
    @[deprecated MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable]
    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μ

    Alias of MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable.

    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.setLIntegral_withDensity_eq_setLIntegral_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μ
    @[deprecated MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀]
    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μ

    Alias of MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀.

    theorem MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_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μ
    @[deprecated MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀']
    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μ

    Alias of MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀'.

    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) :
    μ.AbsolutelyContinuous (μ.withDensity f)

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

    theorem MeasureTheory.withDensity_ae_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type} {f : αβ} {g : αβ} {d : αENNReal} (hd : AEMeasurable d μ) (h_ae_nonneg : ∀ᵐ (x : α) ∂μ, d x 0) :
    f =ᵐ[μ.withDensity d] g f =ᵐ[μ] g

    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))

    If μ is s-finite and f is measurable, then μ.withDensity f is s-finite. TODO: extend this to all functions and make it an instance.