rnDeriv_smul_left_of_ne_top' — Mathlib

English

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

Русский

Если ν₂ ⟂ₘ μ, то (ν₁ + ν₂).rnDeriv μ =ᵐ μ ν₁.rnDeriv μ.

LaTeX

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

Lean4

/-- Radon-Nikodym derivative of the scalar multiple of a measure.
See also `rnDeriv_smul_left_of_ne_top`, which has no hypothesis on `μ` but requires finite `ν`. -/
theorem rnDeriv_smul_left_of_ne_top' (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ] {r : ℝ≥0∞} (hr : r ≠ ∞) :
    (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ :=
  by
  have h : (r.toNNReal • ν).rnDeriv μ =ᵐ[μ] r.toNNReal • ν.rnDeriv μ := rnDeriv_smul_left' ν μ r.toNNReal
  simpa [ENNReal.smul_def, ENNReal.coe_toNNReal hr] using h

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