English
Assume μ ≪ ν with a finite ENNReal scaling factor c ≠ 0, ∞. Then llr(μ, c•ν) = llr(μ, ν) − log(c.toReal) almost everywhere w.r.t μ.
Русский
Пусть μ ≪ ν и существует конечный коэффициент c ≠ 0, ∞. Тогда almost surely по μ: llr(μ, c•ν) = llr(μ, ν) − log(c.toReal).
LaTeX
$$$llr(\\mu, c\\cdot \\nu) =_{\\mu\\text{-a.e.}} llr(\\mu, \\nu) - \\log(c^{\\toReal})$$$
Lean4
theorem llr_smul_right [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_right_of_ne_top μ ν hc 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]
rw [ENNReal.toReal_inv, log_inv]
ring
