English
Let f be integrable with respect to μ and a.e. measurable; let g be a nonnegative function a.e. measurable with respect to μ. For any measurable set s, the integral of g over s with respect to the density μ with density f equals the integral over s of f·g with respect to μ.
Русский
Пусть f интегрируемо относительно μ и a.e. измеримо; пусть g неотрицательная функция, AEMeasurable относительно μ. Для любой измеримой области s верно: линтеграл по s от g относительно μ с плотностью f равен линтегралу по s от f·g относительно μ.
LaTeX
$$$\displaystyle \iint_{a \in s} g(a) \, d\mu^{\,f} = \iint_{a \in s} (f(a) \cdot g(a)) \, d\mu$$$
Lean4
theorem setLIntegral_withDensity_eq_lintegral_mul₀' {μ : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ)
{g : α → ℝ≥0∞} (hg : AEMeasurable g (μ.withDensity f)) {s : Set α} (hs : MeasurableSet s) :
∫⁻ a in s, g a ∂μ.withDensity f = ∫⁻ a in s, (f * g) a ∂μ :=
by
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul₀' hf.restrict]
rw [← restrict_withDensity hs]
exact hg.restrict
