lintegral_withDensity_eq_lintegral_mul₀

English

If f is a.e. measurable and g is a.e. measurable with respect to μ, then the lintegral of g with respect to μ having density f equals the lintegral of f·g with respect to μ.

Русский

Пусть f является a.e. измеримой относительно μ, а g — a.e. измеримой относительно μ. Тогда линтіпеременная интеграл g по мере μ с плотностью f равен линтигеральному интегралу от f·g по μ.

LaTeX

$$$\int g \, d(\mu.withDensity f) = \int (f \cdot g) \, d\mu$$$

Lean4

theorem lintegral_withDensity_eq_lintegral_mul₀ {μ : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) {g : α → ℝ≥0∞}
    (hg : AEMeasurable g μ) : ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, (f * g) a ∂μ :=
  lintegral_withDensity_eq_lintegral_mul₀' hf (hg.mono' (withDensity_absolutelyContinuous μ f))

Похожие утверждения