English
For measurable f and g, the integral of g with respect to μ.withDensity f equals the integral of f·g with respect to μ.
Русский
Для измеримых f и g интеграл g по мере μ.withDensity f равен интегралу f·g по μ.
LaTeX
$$∫⁻ a, g a d(μ.withDensity f) = ∫⁻ a, (f a) * g a dμ$$
Lean4
/-- 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 lintegral_withDensity_eq_lintegral_mul (μ : Measure α) {f : α → ℝ≥0∞} (h_mf : Measurable f) :
∀ {g : α → ℝ≥0∞}, Measurable g → ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, (f * g) a ∂μ :=
by
apply Measurable.ennreal_induction
· intro c s h_ms
simp [*, mul_comm _ c, ← indicator_mul_right]
· intro g h _ h_mea_g _ h_ind_g h_ind_h
simp [mul_add, *, Measurable.mul]
· intro g h_mea_g h_mono_g h_ind
have : Monotone fun n a => f a * g n a := fun m n hmn x => mul_le_mul_left' (h_mono_g hmn x) _
simp [lintegral_iSup, ENNReal.mul_iSup, h_mf.mul (h_mea_g _), *]
