English
For a probability measure μ and sigma-finite ν, the integral of llr with respect to μ is expressible in terms of llr μ ν and the exponential of f, via tilted constructions.
Русский
При вероятностной мере μ и сигма-конечной ν интеграл llr(μ, ν) по μ выражается через llr μ ν и экспоненту f с использованием сдвинутой меры.
LaTeX
$$$\\int \\llr(\\mu, \\nu) \\, dμ = \\int \\llr(\\mu, ν) \\, dμ + \\int f \\, dμ - \\log\\left(\\int e^{f} \\, dμ\\right)$$$
Lean4
theorem integral_llr_tilted_right [IsProbabilityMeasure μ] [SigmaFinite ν] (hμν : μ ≪ ν) (hfμ : Integrable f μ)
(hfν : Integrable (fun x ↦ exp (f x)) ν) (h_int : Integrable (llr μ ν) μ) :
∫ x, llr μ (ν.tilted f) x ∂μ = ∫ x, llr μ ν x ∂μ - ∫ x, f x ∂μ + log (∫ x, exp (f x) ∂ν) := by
calc
∫ x, llr μ (ν.tilted f) x ∂μ = ∫ x, -f x + log (∫ x, exp (f x) ∂ν) + llr μ ν x ∂μ :=
integral_congr_ae (llr_tilted_right hμν hfν)
_ = -∫ x, f x ∂μ + log (∫ x, exp (f x) ∂ν) + ∫ x, llr μ ν x ∂μ :=
by
rw [← integral_neg, integral_add ?_ h_int]
swap; · exact hfμ.neg.add (integrable_const _)
rw [integral_add ?_ (integrable_const _)]
swap; · exact hfμ.neg
simp only [integral_const, measureReal_univ_eq_one, smul_eq_mul, one_mul]
_ = ∫ x, llr μ ν x ∂μ - ∫ x, f x ∂μ + log (∫ x, exp (f x) ∂ν) := by abel
