rnDeriv_smul_left_of_ne_top — Mathlib

English

If r is finite, then the above left-smul formula holds for r.toNNReal with ν replaced by r • ν; equivalently, rnDeriv_smul_left for ENNReal rescaled measure.

Русский

Если r конечно, то формула слева-множитель остается верной после преобразования r к NNReal и замены ν на r • ν.

LaTeX

$$$ (r^{0}\\to\\mathbb{NNReal}):\\; (r\\cdot ν).rnDeriv μ =ᵐ[μ] r \\cdot (ν.rnDeriv μ) $$$

Lean4

/-- Radon-Nikodym derivative of the scalar multiple of a measure.
See also `rnDeriv_smul_left_of_ne_top'`, which requires sigma-finite `ν` and `μ`. -/
theorem rnDeriv_smul_left_of_ne_top (ν μ : Measure α) [IsFiniteMeasure ν] [ν.HaveLebesgueDecomposition μ] {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

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