withDensity_rnDeriv — Mathlib

English

If ν has Lebesgue decomposition with μ, then ν.withDensity(μ.rnDer ν) is absolutely continuous with respect to μ.withDensity(ν.rnDer μ).

Русский

Если ν имеет разложение Лебега относительно μ, то ν.withDensity(μ.rnDer ν) абсолютносопряжено по отношению к μ.withDensity(ν.rnDer μ).

LaTeX

$$$$ ν.withDensity(μ.rnDer ν) \ll μ.withDensity(ν.rnDer μ) $$$$

Lean4

theorem withDensity_rnDeriv {ξ : Measure α} [μ.HaveLebesgueDecomposition ν] (hξμ : ξ ≪ μ) (hξν : ξ ≪ ν) :
    ξ ≪ ν.withDensity (μ.rnDeriv ν) :=
  by
  conv_rhs at hξμ => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
  refine absolutelyContinuous_of_add_of_mutuallySingular hξμ ?_
  exact MutuallySingular.mono_ac (mutuallySingular_singularPart μ ν).symm hξν .rfl

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