English
If μ ≪ ν and Integrable llr μ ν μ, then the real-valued part of KL(μ, ν) equals the sum of the μ-integral of llr and the mass difference ν.univ − μ.univ.
Русский
Если μ ≪ ν и llr μ ν интегрируем по μ, то вещественная часть KL(μ, ν) равна интегралу llr по μ плюс разность масс ν(univ) − μ(univ).
LaTeX
$$$(klDiv\\,μ\\,ν).toReal = \\int x\\, llr\\,μ\\,ν\\,x\\,∂μ + ν.real univ - μ.real univ$$$
Lean4
theorem klDiv_eq_lintegral_klFun :
klDiv μ ν = if μ ≪ ν then ∫⁻ x, ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞ :=
by
rw [klDiv_eq_integral_klFun]
by_cases hμν : μ ≪ ν
swap; · simp [hμν]
have h_int_iff := lintegral_ofReal_ne_top_iff_integrable (f := fun x ↦ klFun (μ.rnDeriv ν x).toReal) (μ := ν) ?_ ?_
rotate_left
· exact Measurable.aestronglyMeasurable (by fun_prop)
· exact ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg
by_cases h_int : Integrable (llr μ ν) μ
· simp only [hμν, h_int, and_self, ↓reduceIte]
rw [ofReal_integral_eq_lintegral_ofReal]
· rwa [integrable_klFun_rnDeriv_iff hμν]
· exact ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg
· rw [← not_iff_not, ne_eq, Decidable.not_not] at h_int_iff
symm
simp [hμν, h_int, h_int_iff, integrable_klFun_rnDeriv_iff hμν]
