rnDeriv_withDensity₀ — Mathlib

English

The singular part is additive in μ: (μ1 + μ2).singularPart ν = μ1.singularPart ν + μ2.singularPart ν.

Русский

Сингулярная часть аддитивна по μ: (μ1 + μ2).singularPart ν = μ1.singularPart ν + μ2.singularPart ν.

LaTeX

$$$ (μ_1 + μ_2).singularPart ν = μ_1.singularPart ν + μ_2.singularPart ν $$$

Lean4

/-- The Radon-Nikodym derivative of `f ν` with respect to `ν` is `f`. -/
theorem rnDeriv_withDensity₀ (ν : Measure α) [SigmaFinite ν] {f : α → ℝ≥0∞} (hf : AEMeasurable f ν) :
    (ν.withDensity f).rnDeriv ν =ᵐ[ν] f :=
  have : ν.withDensity f = 0 + ν.withDensity f := by rw [zero_add]
  (eq_rnDeriv₀ hf MutuallySingular.zero_left this).symm

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