English
Scaling the first measure by a nonnegative real scales its singular part by the same factor: (r μ).singularPart ν = r μ.singularPart ν.
Русский
Умножение меры μ на неотрицательное число r масштабирует её сингулярную часть относительно ν тем же множителем: (r μ).singularPart ν = r μ.singularPart ν.
LaTeX
$$$ (r\\ge 0)\\;\\; (r\\cdot μ).singularPart ν = r\\cdot (μ.singularPart ν) $$$
Lean4
theorem singularPart_smul (μ ν : Measure α) (r : ℝ≥0) : (r • μ).singularPart ν = r • μ.singularPart ν :=
by
by_cases hr : r = 0
· rw [hr, zero_smul, zero_smul, singularPart_zero]
by_cases hl : HaveLebesgueDecomposition μ ν
· refine
(eq_singularPart ((measurable_rnDeriv μ ν).const_smul (r : ℝ≥0∞))
(MutuallySingular.smul r (mutuallySingular_singularPart _ _)) ?_).symm
rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add, ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]
· rw [singularPart, singularPart, dif_neg hl, dif_neg, smul_zero]
refine fun hl' ↦ hl ?_
rw [← inv_smul_smul₀ hr μ]
infer_instance
