English
For finite measures μ ≪ ν with llr μ ν integrable, the integral of klFun of the RN-derivative equals LLr plus total masses difference: ∫ klFun((μ.rnDeriv ν x).toReal) dν = ∫ llr μ ν x dμ + ν(ℝ) − μ(ℝ).
Русский
При конечных мерах μ ≪ ν и интегрируемой llr μ ν имеем интеграл klFun от rn-deriv равен интегралу llr μ ν по μ плюс разность масс ν и μ: ∫ klFun((μ.rnDeriv ν x).toReal) dν = ∫ llr μ ν x dμ + ν(ℝ) − μ(ℝ).
LaTeX
$$$\\int_{\mathbb{R}} \\mathrm{klFun}( (\\mu \\triangleright_{\\mathrm{rn}} \\nu)(x) ) \\, d\nu(x) = \\int_{\\mathbb{R}} \\mathrm{llr}(\\mu,\\nu)(x) \\, d\\mu(x) + \\nu(\\mathbb{R}) - \\mu(\\mathbb{R})$$$
Lean4
theorem integral_klFun_rnDeriv (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν = ∫ x, llr μ ν x ∂μ + ν.real univ - μ.real univ :=
by
unfold klFun
rw [integral_sub, integral_add, integral_const, Measure.integral_toReal_rnDeriv hμν, smul_eq_mul, mul_one]
· congr 2
exact integral_rnDeriv_smul hμν
· rwa [integrable_rnDeriv_mul_log_iff hμν]
· fun_prop
· refine Integrable.add ?_ (integrable_const _)
rwa [integrable_rnDeriv_mul_log_iff hμν]
· fun_prop
