haveLebesgueDecompositionSMul' — Mathlib

English

If HaveLebesgueDecomposition μ ν then (r • μ). HaveLebesgueDecomposition ν for ENNReal r.

Русский

Если μ имеет разложение Лебега относительно ν, то (r • μ) имеет разложение относительно ν для r ∈ ℕℝ.

LaTeX

$$HaveLebesgueDecomposition (r • μ) ν$$

Lean4

instance haveLebesgueDecompositionSMul' (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] (r : ℝ≥0∞) :
    (r • μ).HaveLebesgueDecomposition ν where
  lebesgue_decomposition := by
    obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
    refine ⟨⟨r • μ.singularPart ν, r • μ.rnDeriv ν⟩, hmeas.const_smul _, hsing.smul _, ?_⟩
    simp only
    rw [withDensity_smul _ hmeas, ← smul_add, ← hadd]

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