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
- μ.withDensity f = MeasureTheory.Measure.ofMeasurable (fun (s : Set α) (x : MeasurableSet s) => ∫⁻ (a : α) in s, f a ∂μ) ⋯ ⋯
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
∫⁻ a in s, f a ∂μ = 0. Indeed, consider a simple functiong ≤ f. It vanishes ons. Then∫⁻ a in s, g a ∂μ = 0. Taking the supremum overggives the claim.μ.withDensity f s = +∞. Indeed, this is the infimum ofμ.withDensity f tover measurable setstcontainings. Assis not measurable, such a settcontains a pointx ≠ x₀. Thenμ.withDensity f t ≥ μ.withDensity f {x} = ∫⁻ a in {x}, f a ∂μ = μ {x} = +∞. One checks thatμ.withDensity f = μ, whileμ.restrict sgives zero mass to sets not containingx₀, 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)
:
theorem
MeasureTheory.withDensity_congr_ae
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f g : α → ENNReal}
(h : f =ᵐ[μ] g)
:
μ.withDensity f = μ.withDensity g
theorem
MeasureTheory.withDensity_mono
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f 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)
:
theorem
MeasureTheory.withDensity_add_right
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(f : α → ENNReal)
{g : α → ENNReal}
(hg : Measurable g)
:
theorem
MeasureTheory.withDensity_add_measure
{α : Type u_1}
{m : MeasurableSpace α}
(μ ν : MeasureTheory.Measure α)
(f : α → ENNReal)
:
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)
:
theorem
MeasureTheory.withDensity_smul'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(r : ENNReal)
(f : α → ENNReal)
(hr : r ≠ ⊤)
:
theorem
MeasureTheory.withDensity_smul_measure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
(r : ENNReal)
(f : α → ENNReal)
:
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)
:
(μ.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)
:
theorem
MeasureTheory.withDensity_tsum
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{ι : Type u_2}
[Countable ι]
{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 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 α}
{f : α → ENNReal}
(h : μ.MutuallySingular ν)
:
(μ.withDensity f).MutuallySingular ν
@[simp]
theorem
MeasureTheory.withDensity_eq_zero_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.withDensity_eq_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : AEMeasurable f μ)
:
Alias of the forward direction of MeasureTheory.withDensity_eq_zero_iff.
theorem
MeasureTheory.withDensity_apply_eq_zero'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
{s : Set α}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.withDensity_apply_eq_zero
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
{s : Set α}
(hf : Measurable f)
:
theorem
MeasureTheory.ae_withDensity_iff'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : α → Prop}
{f : α → ENNReal}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.ae_withDensity_iff
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : α → Prop}
{f : α → ENNReal}
(hf : Measurable f)
:
theorem
MeasureTheory.ae_withDensity_iff_ae_restrict'
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : α → Prop}
{f : α → ENNReal}
(hf : AEMeasurable f μ)
:
theorem
MeasureTheory.ae_withDensity_iff_ae_restrict
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{p : α → Prop}
{f : α → ENNReal}
(hf : Measurable f)
:
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 [Tao10]. 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 g : α → ENNReal}
(hf : Measurable f)
(hg : Measurable g)
{s : Set α}
(hs : MeasurableSet s)
:
@[deprecated MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul]
theorem
MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{f g : α → ENNReal}
(hf : Measurable f)
(hg : Measurable g)
{s : Set α}
(hs : MeasurableSet s)
:
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))
:
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)
:
@[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)
:
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 μ)
:
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)
:
@[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)
:
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)
:
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)
:
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 < ⊤)
:
@[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 < ⊤)
:
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)
:
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 < ⊤)
:
@[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 < ⊤)
:
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 < ⊤)
:
@[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 < ⊤)
:
Alias of MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀'.
theorem
MeasureTheory.withDensity_mul₀
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f g : α → ENNReal}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
theorem
MeasureTheory.withDensity_mul
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
{f g : α → ENNReal}
(hf : Measurable f)
(hg : Measurable g)
:
theorem
MeasureTheory.withDensity_inv_same_le
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{f : α → ENNReal}
(hf : AEMeasurable 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 ≠ ⊤)
:
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 ≠ ⊤)
:
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)
:
instance
MeasureTheory.SigmaFinite.withDensity
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
(f : α → NNReal)
:
MeasureTheory.SigmaFinite (μ.withDensity fun (x : α) => ↑(f x))
If μ is a σ-finite measure, then so is μ.withDensity fun x ↦ f x
for any ℝ≥0-valued function f.
theorem
MeasureTheory.SigmaFinite.withDensity_of_ne_top
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
{f : α → ENNReal}
(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_ne_top : ∀ (x : α), f x ≠ ⊤)
:
MeasureTheory.SigmaFinite (μ.withDensity f)
instance
MeasureTheory.SigmaFinite.withDensity_ofReal
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SigmaFinite μ]
(f : α → ℝ)
:
MeasureTheory.SigmaFinite (μ.withDensity fun (x : α) => ENNReal.ofReal (f x))
theorem
MeasureTheory.exists_measurable_le_withDensity_eq
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(f : α → ENNReal)
:
instance
MeasureTheory.Measure.withDensity.instSFinite
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
{f : α → ENNReal}
:
MeasureTheory.SFinite (μ.withDensity f)
If μ is an s-finite measure, then so is μ.withDensity f.
@[deprecated MeasureTheory.Measure.withDensity.instSFinite]
theorem
MeasureTheory.sFinite_withDensity_of_sigmaFinite_of_measurable
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SigmaFinite μ]
{f : α → ENNReal}
(_hf : Measurable f)
:
MeasureTheory.SFinite (μ.withDensity f)
@[deprecated MeasureTheory.Measure.withDensity.instSFinite]
theorem
MeasureTheory.sFinite_withDensity_of_measurable
{α : Type u_1}
{m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
{f : α → ENNReal}
(_hf : Measurable f)
:
MeasureTheory.SFinite (μ.withDensity f)
instance
MeasureTheory.instSFiniteHSMulENNRealMeasure
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.SFinite μ]
(c : ENNReal)
:
MeasureTheory.SFinite (c • μ)
theorem
MeasureTheory.sFinite_of_absolutelyContinuous
{α : Type u_1}
{m0 : MeasurableSpace α}
{μ ν : MeasureTheory.Measure α}
[MeasureTheory.SFinite ν]
(hμν : μ.AbsolutelyContinuous ν)
:
If μ ≪ ν and ν is s-finite, then μ is s-finite.
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))