absolutelyContinuous_withDensity_rnDeriv_swap

English

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

Русский

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

LaTeX

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

Lean4

theorem absolutelyContinuous_withDensity_rnDeriv_swap [ν.HaveLebesgueDecomposition μ] :
    ν.withDensity (μ.rnDeriv ν) ≪ μ.withDensity (ν.rnDeriv μ) :=
  (withDensity_absolutelyContinuous ν (μ.rnDeriv ν)).withDensity_rnDeriv
    (absolutelyContinuous_of_le (withDensity_rnDeriv_le _ _))

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