rnDeriv_withDensity_rnDeriv — Mathlib

English

If μ ≪ ν and both μ and ν are σ-finite, then μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᵐ[μ] μ.rnDeriv ν.

Русский

Если μ ≪ ν и μ, ν — σ-конечны, то μ.rnDeriv(μ.withDensity(ν.rnDeriv μ)) =μ.rnDeriv ν почти наверху μ.

LaTeX

$$$μ.rnDeriv(μ.withDensity(ν.rnDeriv μ)) =_{μ}^{ae} μ.rnDeriv ν$$$

Lean4

theorem rnDeriv_withDensity_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)) =ᵐ[μ] μ.rnDeriv ν :=
  by
  conv_rhs => rw [ν.haveLebesgueDecomposition_add μ, add_comm]
  refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_eq ?_
  exact (rnDeriv_add_right_of_mutuallySingular (Measure.mutuallySingular_singularPart ν μ).symm.withDensity).symm

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