rnDeriv_withDensity — Mathlib

English

Restricting μ and ν to s preserves the singularPart relation: (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s.

Русский

Ограничение μ и ν до s сохраняет отношение сингулярной части: (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s.

LaTeX

$$$ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s $$$

Lean4

/-- The Radon-Nikodym derivative of `f ν` with respect to `ν` is `f`. -/
theorem rnDeriv_withDensity (ν : Measure α) [SigmaFinite ν] {f : α → ℝ≥0∞} (hf : Measurable f) :
    (ν.withDensity f).rnDeriv ν =ᵐ[ν] f :=
  rnDeriv_withDensity₀ ν hf.aemeasurable

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