Theorems · Theorem · measure theory

MeasureTheory.lintegral_withDensity_eq_lintegral_mul

∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
  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.

Defined in

Mathlib.MeasureTheory.Measure.WithDensity

Cited by

5 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound