withDensityᵥ_rnDeriv_smul — Mathlib

English

For a signed measure s and μ with Lebesgue decomposition, RN-derivative respect scaling: (r · s).rnDeriv μ =^{{μ}}_{a.e.} r · s.rnDeriv μ.

Русский

Для знаковой меры s и μ с разложением Лебега производная RN respects масштабирование: (r·s).rnDeriv μ = a.e. (r·s.rnDeriv μ).

LaTeX

$$$ (r \\cdot s).rnDeriv μ =^{{\\mu}}_{a.e.} r \\cdot s.rnDeriv μ $$$

Lean4

theorem withDensityᵥ_rnDeriv_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ ν : Measure α}
    [μ.HaveLebesgueDecomposition ν] [SigmaFinite μ] {f : α → E} (hμν : μ ≪ ν) (hf : Integrable f μ) :
    ν.withDensityᵥ (fun x ↦ (μ.rnDeriv ν x).toReal • f x) = μ.withDensityᵥ f := by
  rw [withDensityᵥ_smul_eq_withDensityᵥ_withDensity' (measurable_rnDeriv μ ν).aemeasurable (rnDeriv_lt_top μ ν)
      ((integrable_rnDeriv_smul_iff hμν).mpr hf),
    withDensity_rnDeriv_eq μ ν hμν]

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