rnDeriv_add_of_mutuallySingular — Mathlib

English

If ν₂ ⟂ₘ μ, then (ν₁ + ν₂).rnDeriv μ =ᵐ μ ν₁.rnDeriv μ.

Русский

Если ν₂ взаимно-сингулярна μ, то сумма производных равна производной ν₁.

LaTeX

$$$$ (\\nu_1 + \\nu_2).rnDeriv \\mu =^{a.e.}_{\\mu} \\nu_1.rnDeriv \\mu. $$$$

Lean4

theorem rnDeriv_add_of_mutuallySingular (ν₁ ν₂ μ : Measure α) [SigmaFinite ν₁] [SigmaFinite ν₂] [SigmaFinite μ]
    (h : ν₂ ⟂ₘ μ) : (ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ :=
  by
  filter_upwards [rnDeriv_add' ν₁ ν₂ μ, (rnDeriv_eq_zero ν₂ μ).mpr h] with x hx_add hx_zero
  simp [hx_add, hx_zero]

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