English
If r ≠ 0, then μ.singularPart (r ν) = μ.singularPart ν.
Русский
При r ≠ 0 сингулярная часть μ относительно r ν совпадает с сингулярной частью μ относительно ν.
LaTeX
$$$ (r\\ge 0),\\; r\\neq 0 \\Rightarrow μ.singularPart (r·ν) = μ.singularPart ν $$$
Lean4
theorem singularPart_smul_right (μ ν : Measure α) (r : ℝ≥0) (hr : r ≠ 0) : μ.singularPart (r • ν) = μ.singularPart ν :=
by
by_cases hl : HaveLebesgueDecomposition μ ν
· refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm
· exact (mutuallySingular_singularPart μ ν).mono_ac AbsolutelyContinuous.rfl smul_absolutelyContinuous
· rw [ENNReal.smul_def r, withDensity_smul_measure, ← withDensity_smul]
swap; · exact (measurable_rnDeriv _ _).const_smul _
convert haveLebesgueDecomposition_add μ ν
ext x
simp only [Pi.smul_apply]
rw [← ENNReal.smul_def, smul_inv_smul₀ hr]
· rw [singularPart, singularPart, dif_neg hl, dif_neg]
refine fun hl' ↦ hl ?_
rw [← inv_smul_smul₀ hr ν]
infer_instance
