eq_rnDeriv₀ — Mathlib

English

The singular part respects scalar multiplication by NNReal: (r μ).singularPart ν = r μ.singularPart ν.

Русский

Сингулярная часть сохраняет масштабирование NNReal: (r μ).singularPart ν = r μ.singularPart ν.

LaTeX

$$$ (r\\in\\mathbb{R}_{+}):\\; (r\\cdot μ).singularPart ν = r\\cdot (μ.singularPart ν) $$$

Lean4

theorem eq_rnDeriv₀ [SigmaFinite ν] {s : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f ν) (hs : s ⟂ₘ ν)
    (hadd : μ = s + ν.withDensity f) : f =ᵐ[ν] μ.rnDeriv ν :=
  (withDensity_eq_iff_of_sigmaFinite hf (measurable_rnDeriv _ _).aemeasurable).mp (eq_withDensity_rnDeriv₀ hf hs hadd)

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