rnDeriv_mul_rnDeriv — Mathlib

English

If μ ≪ ν and κ are σ-finite, then multiplying the RN-derivatives with respect to ν and κ yields the RN-derivative of μ with respect to κ, almost everywhere under κ.

Русский

Если μ ≪ ν и κ -- σ–конечные, то произведение RN-дерививов μ по ν и ν по κ равно RN-дерививу μ по κ почти везде по κ.

LaTeX

$$$$ \mu.rnDeriv ν \cdot ν.rnDeriv κ =^\mathrm{ae}_{\kappa} \mu.rnDeriv κ $$$$

Lean4

theorem rnDeriv_mul_rnDeriv {κ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [SigmaFinite κ] (hμν : μ ≪ ν) :
    μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[κ] μ.rnDeriv κ :=
  by
  refine (rnDeriv_withDensity_left ?_ ?_).symm.trans ?_
  · exact (Measure.measurable_rnDeriv _ _).aemeasurable
  · exact rnDeriv_ne_top _ _
  · rw [Measure.withDensity_rnDeriv_eq _ _ hμν]

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