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 α} (μ : Measure α) (f : α → ENNReal) : 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 α} {μ : 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 α} {μ : 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 α} {μ : Measure α} [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) : Measure.withDensity 0 f = 0

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

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

theorem MeasureTheory.withDensity_add_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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 α} {μ : 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 α} (μ ν : Measure α) (f : α → ENNReal) : (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f

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

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

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

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

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

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

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

instance MeasureTheory.noAtoms_withDensity {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [NoAtoms μ] (f : α → ENNReal) : NoAtoms (μ.withDensity f)

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem MeasureTheory.withDensity_indicator {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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 α} {μ : Measure α} {s : Set α} (hs : MeasurableSet s) : μ.withDensity (s.indicator 1) = μ.restrict s

theorem MeasureTheory.withDensity_ofReal_mutuallySingular {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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 α} {μ : 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 α} {μ : Measure α} [SFinite μ] (s : Set α) (f : α → ENNReal) : (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

theorem MeasureTheory.trim_withDensity {α : Type u_1} {m m0 : MeasurableSpace α} {μ : 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 α} {μ ν : Measure α} {f : α → ENNReal} (h : μ.MutuallySingular ν) : (μ.withDensity f).MutuallySingular ν

@[simp]

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

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

Alias of the forward direction of MeasureTheory.withDensity_eq_zero_iff.

theorem MeasureTheory.withDensity_apply_eq_zero' {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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 α} {μ : 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 α} {μ : Measure α} {p : α → Prop} {f : α → ENNReal} (hf : AEMeasurable f μ) : (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x

theorem MeasureTheory.ae_withDensity_iff {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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 α} {μ : 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 α} {μ : 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 α} {μ : 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 α} {μ : 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 α} (μ : 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 α} (μ : Measure α) {f 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 α} {μ : 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 α} {μ : 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 α} {μ : 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 α} {μ : 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 α} (μ : 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 α} (μ : 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 α} (μ : 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 α} (μ : 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 α} (μ : 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.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀' {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [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 α} {μ : Measure α} {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : μ.withDensity (f * g) = (μ.withDensity f).withDensity g

theorem MeasureTheory.withDensity_mul {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) {f 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 α} {μ : Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) : (μ.withDensity f).withDensity f⁻¹ ≤ μ

theorem MeasureTheory.withDensity_inv_same₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : 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 α} {μ : 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 α} {μ : 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 α} {μ : Measure α} {β : Type} {f g : α → β} {d : α → ENNReal} (hd : AEMeasurable d μ) (h_ae_nonneg : ∀ᵐ (x : α) ∂μ, d x ≠ 0) : f =ᶠ[ae (μ.withDensity d)] g ↔ f =ᶠ[ae μ] g

instance MeasureTheory.SigmaFinite.withDensity {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] (f : α → NNReal) : 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 α} {μ : Measure α} [SigmaFinite μ] {f : α → ENNReal} (hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : SigmaFinite (μ.withDensity f)

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

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

theorem MeasureTheory.exists_measurable_le_withDensity_eq {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) [SFinite μ] (f : α → ENNReal) : ∃ (g : α → ENNReal), Measurable g ∧ g ≤ f ∧ μ.withDensity g = μ.withDensity f

instance MeasureTheory.Measure.withDensity.instSFinite {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SFinite μ] {f : α → ENNReal} : SFinite (μ.withDensity f)

If μ is an s-finite measure, then so is μ.withDensity f.

instance MeasureTheory.instSFiniteHSMulENNRealMeasure {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [SFinite μ] (c : ENNReal) : SFinite (c • μ)

theorem MeasureTheory.sFinite_of_absolutelyContinuous {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : Measure α} [SFinite ν] (hμν : μ.AbsolutelyContinuous ν) : SFinite μ

If μ ≪ ν and ν is s-finite, then μ is s-finite.

instance MeasureTheory.instSFiniteOfCountable {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [Countable α] : SFinite μ

In a countable space, every measure is s-finite.

theorem MeasureTheory.prod_withDensity_left₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} [SFinite ν] {f : α → ENNReal} (hf : AEMeasurable f μ) : (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun (z : α × β) => f z.1

theorem MeasureTheory.prod_withDensity_left {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} [SFinite ν] {f : α → ENNReal} (hf : Measurable f) : (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun (z : α × β) => f z.1

theorem MeasureTheory.prod_withDensity_right₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} [SFinite ν] {g : β → ENNReal} (hg : AEMeasurable g ν) : μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) => g z.2

theorem MeasureTheory.prod_withDensity_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} [SFinite ν] {g : β → ENNReal} (hg : Measurable g) : μ.prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) => g z.2

theorem MeasureTheory.prod_withDensity₀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} [SFinite ν] {f : α → ENNReal} {g : β → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) : (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) => f z.1 * g z.2

theorem MeasureTheory.prod_withDensity {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} [SFinite ν] {f : α → ENNReal} {g : β → ENNReal} (hf : Measurable f) (hg : Measurable g) : (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun (z : α × β) => f z.1 * g z.2

theorem MeasureTheory.Measure.prod_smul_right {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {β : Type u_2} {mβ : MeasurableSpace β} {ν : Measure β} [SFinite ν] (c : ENNReal) : μ.prod (c • ν) = c • μ.prod ν

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

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

theorem MeasureTheory.Measure.mconv_smul_right {M : Type u_2} [Monoid M] [MeasurableSpace M] (μ ν : Measure M) [SFinite ν] (s : ENNReal) : μ.mconv (s • ν) = s • μ.mconv ν

theorem MeasureTheory.Measure.conv_smul_right {M : Type u_2} [AddMonoid M] [MeasurableSpace M] (μ ν : Measure M) [SFinite ν] (s : ENNReal) : μ.conv (s • ν) = s • μ.conv ν

theorem MeasureTheory.mconv_withDensity_eq_mlconvolution₀ {G : Type u_3} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [SFinite μ] [μ.IsMulLeftInvariant] {f g : G → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : (μ.withDensity f).mconv (μ.withDensity g) = μ.withDensity (mlconvolution f g μ)

theorem MeasureTheory.conv_withDensity_eq_mlconvolution₀ {G : Type u_3} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsAddLeftInvariant] {f g : G → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : (μ.withDensity f).conv (μ.withDensity g) = μ.withDensity (lconvolution f g μ)

theorem MeasureTheory.mconv_withDensity_eq_mlconvolution {G : Type u_3} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [SFinite μ] [μ.IsMulLeftInvariant] {f g : G → ENNReal} (hf : Measurable f) (hg : Measurable g) : (μ.withDensity f).mconv (μ.withDensity g) = μ.withDensity (mlconvolution f g μ)

theorem MeasureTheory.conv_withDensity_eq_lconvolution {G : Type u_3} [AddGroup G] {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : Measure G} [SFinite μ] [μ.IsAddLeftInvariant] {f g : G → ENNReal} (hf : Measurable f) (hg : Measurable g) : (μ.withDensity f).conv (μ.withDensity g) = μ.withDensity (lconvolution f g μ)