equal
deleted
inserted
replaced
192 assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" |
192 assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" |
193 shows "KL_divergence b M (density M f) = (\<integral>x. f x * log b (f x) \<partial>M)" |
193 shows "KL_divergence b M (density M f) = (\<integral>x. f x * log b (f x) \<partial>M)" |
194 unfolding KL_divergence_def |
194 unfolding KL_divergence_def |
195 proof (subst integral_density) |
195 proof (subst integral_density) |
196 show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M" |
196 show "entropy_density b M (density M (\<lambda>x. ereal (f x))) \<in> borel_measurable M" |
197 using f `1 < b` |
197 using f |
198 by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density) |
198 by (auto simp: comp_def entropy_density_def intro!: borel_measurable_log borel_measurable_RN_deriv_density) |
199 have "density M (RN_deriv M (density M f)) = density M f" |
199 have "density M (RN_deriv M (density M f)) = density M f" |
200 using f by (intro density_RN_deriv_density) auto |
200 using f by (intro density_RN_deriv_density) auto |
201 then have eq: "AE x in M. RN_deriv M (density M f) x = f x" |
201 then have eq: "AE x in M. RN_deriv M (density M f) x = f x" |
202 using f |
202 using f |