English
If HaveLebesgueDecomposition μ ν then μ HaveLebesgueDecomposition (instHSMul.hSMul r ν) for NNReal r.
Русский
Если μ имеет разложение μ ν, тогда μ имеет разложение относительно r • ν.
LaTeX
$$μ.HaveLebesgueDecomposition (instHSMul.hSMul r ν)$$
Lean4
instance haveLebesgueDecompositionSMulRight (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] (r : ℝ≥0) :
μ.HaveLebesgueDecomposition (r • ν) where
lebesgue_decomposition := by
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν
by_cases hr : r = 0
· exact ⟨⟨μ, 0⟩, measurable_const, by simp [hr], by simp⟩
refine
⟨⟨μ.singularPart ν, r⁻¹ • μ.rnDeriv ν⟩, hmeas.const_smul _,
hsing.mono_ac AbsolutelyContinuous.rfl smul_absolutelyContinuous, ?_⟩
have : r⁻¹ • rnDeriv μ ν = ((r⁻¹ : ℝ≥0) : ℝ≥0∞) • rnDeriv μ ν := by simp [ENNReal.smul_def]
rw [this, withDensity_smul _ hmeas, ENNReal.smul_def r, withDensity_smul_measure, ← smul_assoc, smul_eq_mul,
ENNReal.coe_inv hr, ENNReal.inv_mul_cancel, one_smul]
· exact hadd
· simp [hr]
· exact ENNReal.coe_ne_top
