English
Assume μ has finite measure and μ ≪ ν with a finite ENNReal scaling factor c ≠ 0, ∞. Then llr[c•μ, ν] = llr[μ, ν] + log(c.toReal) almost everywhere w.r.t μ.
Русский
Пусть μ — конечная мера и μ ≪ ν, с ненулевым и конечным коэффициентом масштабирования c. Тогда почти везде по μ выполняется: llr(c•μ, ν) = llr(μ, ν) + log(c.toReal).
LaTeX
$$$llr(c\\cdot \\mu, \\nu) =_{\\mu\\text{-a.e.}} llr(\\mu, \\nu) + \\log(c^{\\toReal})$$$
Lean4
theorem llr_smul_left [IsFiniteMeasure μ] [Measure.HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) (c : ℝ≥0∞) (hc : c ≠ 0)
(hc_ne_top : c ≠ ∞) : llr (c • μ) ν =ᵐ[μ] fun x ↦ llr μ ν x + log c.toReal :=
by
simp only [llr, llr_def]
have h := Measure.rnDeriv_smul_left_of_ne_top μ ν hc_ne_top
filter_upwards [hμν.ae_le h, Measure.rnDeriv_pos hμν, hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx_eq hx_pos
hx_ne_top
rw [hx_eq]
simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul]
rw [log_mul]
rotate_left
· rw [ENNReal.toReal_ne_zero]
simp [hc, hc_ne_top]
· rw [ENNReal.toReal_ne_zero]
simp [hx_pos.ne', hx_ne_top.ne]
ring
