diff -r 532156e8f15f -r 6dec6b1f31f5 src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Sun Jul 07 22:25:34 2024 +0100 +++ b/src/HOL/Probability/Information.thy Mon Jul 08 22:27:50 2024 +0100 @@ -10,15 +10,6 @@ Independent_Family begin - -lemma log_mult_nz: - "x\0 \ y\0 \ log a (x * y) = log a x + log a y" - by (simp add: log_def ln_mult divide_inverse distrib_right) - -lemma log_divide_nz: - "x\0 \ y\0 \ log a (x / y) = log a x - log a y" - by (simp add: diff_divide_distrib ln_div log_def) - subsection "Information theory" locale information_space = prob_space + @@ -554,11 +545,8 @@ show "AE x in S \\<^sub>M T. Pxy x * log b (Pxy x) - Pxy x * log b (Px (fst x)) - Pxy x * log b (Py (snd x)) = f x" - using A B unfolding f_def - - apply (auto simp: f_def field_simps space_pair_measure Px_nn Py_nn Pxy_nn - less_le ) - by (smt (verit, del_insts) AE_I2 distrib_left log_divide log_mult mult_eq_0_iff) + using A B + by (auto simp: f_def field_simps space_pair_measure log_mult log_divide) qed show "0 \ ?M" unfolding M @@ -1097,9 +1085,7 @@ have "integrable (S \\<^sub>M T \\<^sub>M P) (\x. Pxyz x * - log b (?f x))" apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3]) using ae1 ae2 ae3 ae4 - apply (auto simp: log_divide log_mult zero_le_mult_iff zero_less_mult_iff zero_less_divide_iff field_simps - less_le space_pair_measure split: prod.split) - by (smt (verit, best) AE_I2 fst_conv log_divide mult_cancel_left mult_minus_right snd_conv) + by (auto simp: log_mult log_divide field_simps) then show "integrable ?P (\x. - log b (?f x))" by (subst integrable_real_density) (auto simp: space_pair_measure) @@ -1112,9 +1098,7 @@ apply simp apply (intro integral_cong_AE) using ae1 ae2 ae3 ae4 - apply (auto simp: zero_less_mult_iff zero_less_divide_iff field_simps - space_pair_measure less_le split: prod.split) - by (smt (verit, best) AE_I2 fst_conv log_divide mult_eq_0_iff mult_minus_right snd_conv) + by (auto simp: field_simps log_divide) finally show ?nonneg by simp qed @@ -1214,10 +1198,7 @@ ultimately have I1: "integrable (S \\<^sub>M T \\<^sub>M P) (\(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Px x * Pyz (y, z))))" apply (rule integrable_cong_AE_imp) using ae1 ae4 Px_nn Pyz_nn Pxyz_nn - apply (auto simp: log_divide log_mult field_simps zero_less_mult_iff space_pair_measure less_le - split: prod.split) - apply (intro AE_I2) - by (smt (verit, best) distrib_left divide_eq_0_iff fst_conv log_mult mult.commute nonzero_mult_div_cancel_left snd_conv times_divide_eq_right) + by (auto simp: log_divide log_mult field_simps) have "integrable (S \\<^sub>M T \\<^sub>M P) (\x. Pxyz x * log b (Pxz (fst x, snd (snd x))) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pz (snd (snd x))))" using finite_entropy_integrable_transform[OF Fxz Pxyz Pxyz_nn, of "\x. (fst x, snd (snd x))"] @@ -1230,42 +1211,8 @@ ultimately have I2: "integrable (S \\<^sub>M T \\<^sub>M P) (\(x, y, z). Pxyz (x, y, z) * log b (Pxz (x, z) / (Px x * Pz z)))" apply (rule integrable_cong_AE_imp) using ae1 ae2 ae3 ae4 Px_nn Pz_nn Pxz_nn Pyz_nn Pxyz_nn - apply(auto simp: field_simps zero_less_mult_iff less_le space_pair_measure split: prod.split) - apply (intro AE_I2) - apply clarify - proof - - fix a :: 'c and aa :: 'd and ba :: 'e and x1 :: 'c and ab :: 'd and baa :: 'e - assume a1: "Pxz (fst (x1, ab, baa), snd (snd (x1, ab, baa))) = 0 \ Pxyz (x1, ab, baa) = 0" - assume a2: "Pz (snd (snd (x1, ab, baa))) = 0 \ Pxyz (x1, ab, baa) = 0" - assume a3: "Px (fst (x1, ab, baa)) = 0 \ Pxyz (x1, ab, baa) = 0" - have f4: "\r ra rb. (ra::real) * (rb + r) = rb * ra + ra * r" - by (simp add: vector_space_over_itself.scale_right_distrib) - have f5: "0 \ Px x1 \ 0 = Pxyz (x1, ab, baa)" - using a3 by auto - have f6: "0 \ Pz baa \ 0 = Pxyz (x1, ab, baa)" - using a2 by force - have f7: "\r. (0::real) = 0 * r" - by simp - have "0 = Px x1 * Pz baa \ Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa)))" - using f6 f5 by simp - moreover - { assume "0 \ Px x1 * Pz baa" - moreover - { assume "0 \ Px x1 * Pz baa \ 0 \ Pxyz (x1, ab, baa)" - then have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1 * Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \ 0 \ Pxz (x1, baa) / (Px x1 * Pz baa)" - using a1 by (metis (no_types) divide_eq_0_iff fst_eqD log_mult_nz mult.commute nonzero_eq_divide_eq snd_eqD) - moreover - { assume "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + (log b 0 + log b 0)) \ 0 \ Pxz (x1, baa) / (Px x1 * Pz baa) \ Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pz baa * (Pxz (x1, baa) / (Px x1 * Pz baa)))" - then have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))" - using f7 f4 by (metis (no_types) divide_eq_0_iff log_mult_nz mult.commute) } - ultimately have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \ Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))" - using f4 by (simp add: log_mult_nz) } - ultimately have "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa) + log b (Pxz (x1, baa) / (Px x1 * Pz baa))) \ Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = Pxyz (x1, ab, baa) * (log b (Px x1) + log b (Pz baa)) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)) \ Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))" - using f7 by (metis (no_types)) } - ultimately show "Pxyz (x1, ab, baa) * log b (Pxz (x1, baa)) = log b (Px x1) * Pxyz (x1, ab, baa) + (log b (Pz baa) * Pxyz (x1, ab, baa) + Pxyz (x1, ab, baa) * log b (Pxz (x1, baa) / (Px x1 * Pz baa)))" - by argo - qed - + apply(auto simp: field_simps log_divide log_mult) + done from ae I1 I2 show ?eq unfolding conditional_mutual_information_def mi_eq apply (subst mutual_information_distr[OF S TP Px Px_nn Pyz Pyz_nn Pxyz Pxyz_nn]; simp add: space_pair_measure) @@ -1372,14 +1319,8 @@ have "integrable (S \\<^sub>M T \\<^sub>M P) (\x. Pxyz x * - log b (?f x))" apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ I3]) using Pz_nn Pxz_nn Pyz_nn Pxyz_nn ae2 ae3 ae4 - apply (auto simp: log_divide_nz log_mult_nz zero_le_mult_iff zero_less_mult_iff - zero_less_divide_iff field_simps space_pair_measure less_le split: prod.split) - apply (intro AE_I2) - apply (auto simp: ) - by (smt (verit, best) log_divide minus_mult_minus mult_minus_left no_zero_divisors) - - then - show "integrable ?P (\x. - log b (?f x))" + by (auto simp: log_divide field_simps) + then show "integrable ?P (\x. - log b (?f x))" using Pxyz_nn by (auto simp: integrable_real_density) qed (auto simp: b_gt_1 minus_log_convex) also have "\ = conditional_mutual_information b S T P X Y Z" @@ -1391,10 +1332,7 @@ apply simp apply (intro integral_cong_AE) using ae1 ae2 ae3 ae4 - apply (auto simp: log_divide_pos zero_less_mult_iff zero_less_divide_iff - field_simps space_pair_measure less_le integral_cong_AE split: prod.split) - apply (intro AE_I2) - by (metis divide_divide_eq_right log_recip mult_1 mult_minus_right) + by (auto simp: log_divide zero_less_mult_iff field_simps) finally show ?nonneg by simp qed