diff --git a/thys/Frequency_Moments/Frequency_Moment_0.thy b/thys/Frequency_Moments/Frequency_Moment_0.thy --- a/thys/Frequency_Moments/Frequency_Moment_0.thy +++ b/thys/Frequency_Moments/Frequency_Moment_0.thy @@ -1,1315 +1,1315 @@ section \Frequency Moment $0$\label{sec:f0}\ theory Frequency_Moment_0 imports Frequency_Moments_Preliminary_Results Median_Method.Median K_Smallest Universal_Hash_Families.Carter_Wegman_Hash_Family Frequency_Moments Landau_Ext Probability_Ext Product_PMF_Ext Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields begin text \This section contains a formalization of a new algorithm for the zero-th frequency moment inspired by ideas described in \<^cite>\"baryossef2002"\. It is a KMV-type ($k$-minimum value) algorithm with a rounding method and matches the space complexity of the best algorithm described in \<^cite>\"baryossef2002"\. In addition to the Isabelle proof here, there is also an informal hand-written proof in Appendix~\ref{sec:f0_proof}.\ type_synonym f0_state = "nat \ nat \ nat \ nat \ (nat \ nat list) \ (nat \ float set)" definition hash where "hash p = ring.hash (mod_ring p)" fun f0_init :: "rat \ rat \ nat \ f0_state pmf" where "f0_init \ \ n = do { let s = nat \-18 * ln (real_of_rat \)\; let t = nat \80 / (real_of_rat \)\<^sup>2\; let p = prime_above (max n 19); let r = nat (4 * \log 2 (1 / real_of_rat \)\ + 23); h \ prod_pmf {.._. pmf_of_set (bounded_degree_polynomials (mod_ring p) 2)); return_pmf (s, t, p, r, h, (\_ \ {0.. f0_state \ f0_state pmf" where "f0_update x (s, t, p, r, h, sketch) = return_pmf (s, t, p, r, h, \i \ {.. rat pmf" where "f0_result (s, t, p, r, h, sketch) = return_pmf (median s (\i \ {.. rat \ rat) \ real" where "f0_space_usage (n, \, \) = ( let s = nat \-18 * ln (real_of_rat \)\ in let r = nat (4 * \log 2 (1 / real_of_rat \)\ + 23) in let t = nat \80 / (real_of_rat \)\<^sup>2 \ in 6 + 2 * log 2 (real s + 1) + 2 * log 2 (real t + 1) + 2 * log 2 (real n + 21) + 2 * log 2 (real r + 1) + real s * (5 + 2 * log 2 (21 + real n) + real t * (13 + 4 * r + 2 * log 2 (log 2 (real n + 13)))))" definition encode_f0_state :: "f0_state \ bool list option" where "encode_f0_state = N\<^sub>e \\<^sub>e (\s. N\<^sub>e \\<^sub>e ( N\<^sub>e \\<^sub>e (\p. N\<^sub>e \\<^sub>e ( ([0..\<^sub>e (P\<^sub>e p 2)) \\<^sub>e ([0..\<^sub>e (S\<^sub>e F\<^sub>e))))))" lemma "inj_on encode_f0_state (dom encode_f0_state)" proof - have "is_encoding encode_f0_state" unfolding encode_f0_state_def by (intro dependent_encoding exp_golomb_encoding poly_encoding fun_encoding set_encoding float_encoding) thus ?thesis by (rule encoding_imp_inj) qed context fixes \ \ :: rat fixes n :: nat fixes as :: "nat list" fixes result assumes \_range: "\ \ {0<..<1}" assumes \_range: "\ \ {0<..<1}" assumes as_range: "set as \ {.. fold (\a state. state \ f0_update a) as (f0_init \ \ n) \ f0_result" begin private definition t where "t = nat \80 / (real_of_rat \)\<^sup>2\" private lemma t_gt_0: "t > 0" using \_range by (simp add:t_def) private definition s where "s = nat \-(18 * ln (real_of_rat \))\" private lemma s_gt_0: "s > 0" using \_range by (simp add:s_def) private definition p where "p = prime_above (max n 19)" private lemma p_prime:"Factorial_Ring.prime p" using p_def prime_above_prime by presburger private lemma p_ge_18: "p \ 18" proof - have "p \ 19" by (metis p_def prime_above_lower_bound max.bounded_iff) thus ?thesis by simp qed private lemma p_gt_0: "p > 0" using p_ge_18 by simp private lemma p_gt_1: "p > 1" using p_ge_18 by simp private lemma n_le_p: "n \ p" proof - have "n \ max n 19" by simp also have "... \ p" unfolding p_def by (rule prime_above_lower_bound) finally show ?thesis by simp qed private lemma p_le_n: "p \ 2*n + 40" proof - have "p \ 2 * (max n 19) + 2" by (subst p_def, rule prime_above_upper_bound) also have "... \ 2 * n + 40" by (cases "n \ 19", auto) finally show ?thesis by simp qed private lemma as_lt_p: "\x. x \ set as \ x < p" using as_range atLeastLessThan_iff by (intro order_less_le_trans[OF _ n_le_p]) blast private lemma as_subset_p: "set as \ {..log 2 (1 / real_of_rat \)\ + 23)" private lemma r_bound: "4 * log 2 (1 / real_of_rat \) + 23 \ r" proof - have "0 \ log 2 (1 / real_of_rat \)" using \_range by simp hence "0 \ \log 2 (1 / real_of_rat \)\" by simp hence "0 \ 4 * \log 2 (1 / real_of_rat \)\ + 23" by (intro add_nonneg_nonneg mult_nonneg_nonneg, auto) thus ?thesis by (simp add:r_def) qed private lemma r_ge_23: "r \ 23" proof - have "(23::real) = 0 + 23" by simp also have "... \ 4 * log 2 (1 / real_of_rat \) + 23" using \_range by (intro add_mono mult_nonneg_nonneg, auto) also have "... \ r" using r_bound by simp finally show "23 \ r" by simp qed private lemma two_pow_r_le_1: "0 < 1 - 2 powr - real r" proof - have a: "2 powr (0::real) = 1" by simp show ?thesis using r_ge_23 by (simp, subst a[symmetric], intro powr_less_mono, auto) qed interpretation carter_wegman_hash_family "mod_ring p" 2 rewrites "ring.hash (mod_ring p) = Frequency_Moment_0.hash p" using carter_wegman_hash_familyI[OF mod_ring_is_field mod_ring_finite] using hash_def p_prime by auto private definition tr_hash where "tr_hash x \ = truncate_down r (hash x \)" private definition sketch_rv where "sketch_rv \ = least t ((\x. float_of (tr_hash x \)) ` set as)" private definition estimate where "estimate S = (if card S < t then of_nat (card S) else of_nat t * of_nat p / rat_of_float (Max S))" private definition sketch_rv' where "sketch_rv' \ = least t ((\x. tr_hash x \) ` set as)" private definition estimate' where "estimate' S = (if card S < t then real (card S) else real t * real p / Max S)" private definition \\<^sub>0 where "\\<^sub>0 = prod_pmf {.._. pmf_of_set space)" private lemma f0_alg_sketch: defines "sketch \ fold (\a state. state \ f0_update a) as (f0_init \ \ n)" shows "sketch = map_pmf (\x. (s,t,p,r, x, \i \ {..\<^sub>0" unfolding sketch_rv_def proof (subst sketch_def, induction as rule:rev_induct) case Nil then show ?case by (simp add:s_def p_def[symmetric] map_pmf_def t_def r_def Let_def least_def restrict_def space_def \\<^sub>0_def) next case (snoc x xs) let ?sketch = "\\ xs. least t ((\a. float_of (tr_hash a \)) ` set xs)" have "fold (\a state. state \ f0_update a) (xs @ [x]) (f0_init \ \ n) = (map_pmf (\\. (s, t, p, r, \, \i \ {.. i) xs)) \\<^sub>0) \ f0_update x" by (simp add: restrict_def snoc del:f0_init.simps) also have "... = \\<^sub>0 \ (\\. f0_update x (s, t, p, r, \, \i\{.. i) xs)) " by (simp add:map_pmf_def bind_assoc_pmf bind_return_pmf del:f0_update.simps) also have "... = map_pmf (\\. (s, t, p, r, \, \i\{.. i) (xs@[x]))) \\<^sub>0" by (simp add:least_insert map_pmf_def tr_hash_def cong:restrict_cong) finally show ?case by blast qed private lemma card_nat_in_ball: fixes x :: nat fixes q :: real assumes "q \ 0" defines "A \ {k. abs (real x - real k) \ q \ k \ x}" shows "real (card A) \ 2 * q" and "finite A" proof - have a: "of_nat x \ {\real x-q\..\real x+q\}" using assms by (simp add: ceiling_le_iff) have "card A = card (int ` A)" by (rule card_image[symmetric], simp) also have "... \ card ({\real x-q\..\real x+q\} - {of_nat x})" by (intro card_mono image_subsetI, simp_all add:A_def abs_le_iff, linarith) also have "... = card {\real x-q\..\real x+q\} - 1" by (rule card_Diff_singleton, rule a) also have "... = int (card {\real x-q\..\real x+q\}) - int 1" by (intro of_nat_diff) (metis a card_0_eq empty_iff finite_atLeastAtMost_int less_one linorder_not_le) also have "... \ \q+real x\+1 -\real x-q\ - 1" using assms by (simp, linarith) also have "... \ 2*q" by linarith finally show "card A \ 2 * q" by simp have "A \ {..x + nat \q\}" by (rule subsetI, simp add:A_def abs_le_iff, linarith) thus "finite A" by (rule finite_subset, simp) qed private lemma prob_degree_lt_1: "prob {\. degree \ < 1} \ 1/real p" proof - have "space \ {\. length \ \ Suc 0} = bounded_degree_polynomials (mod_ring p) 1" by (auto simp:set_eq_iff bounded_degree_polynomials_def space_def) moreover have "field_size = p" by (simp add:mod_ring_def) hence "real (card (bounded_degree_polynomials (mod_ring p) (Suc 0))) / real (card space) = 1 / real p" by (simp add:space_def bounded_degree_polynomials_card power2_eq_square) ultimately show ?thesis by (simp add:M_def measure_pmf_of_set) qed private lemma collision_prob: assumes "c \ 1" shows "prob {\. \x \ set as. \y \ set as. x \ y \ tr_hash x \ \ c \ tr_hash x \ = tr_hash y \} \ (5/2) * (real (card (set as)))\<^sup>2 * c\<^sup>2 * 2 powr -(real r) / (real p)\<^sup>2 + 1/real p" (is "prob {\. ?l \} \ ?r1 + ?r2") proof - define \ :: real where "\ = 9/8" have rho_c_ge_0: "\ * c \ 0" unfolding \_def using assms by simp have c_ge_0: "c\0" using assms by simp have "degree \ \ 1 \ \ \ space \ degree \ = 1" for \ by (simp add:bounded_degree_polynomials_def space_def) (metis One_nat_def Suc_1 le_less_Suc_eq less_imp_diff_less list.size(3) pos2) hence a: "\\ x y. x < p \ y < p \ x \ y \ degree \ \ 1 \ \ \ space \ hash x \ \ hash y \" using inj_onD[OF inj_if_degree_1] mod_ring_carr by blast have b: "prob {\. degree \ \ 1 \ tr_hash x \ \ c \ tr_hash x \ = tr_hash y \} \ 5 * c\<^sup>2 * 2 powr (-real r) /(real p)\<^sup>2" if b_assms: "x \ set as" "y \ set as" "x < y" for x y proof - have c: "real u \ \ * c \ \real u - real v\ \ \ * c * 2 powr (-real r)" if c_assms:"truncate_down r (real u) \ c" "truncate_down r (real u) = truncate_down r (real v)" for u v proof - have "9 * 2 powr - real r \ 9 * 2 powr (- real 23)" using r_ge_23 by (intro mult_left_mono powr_mono, auto) also have "... \ 1" by simp finally have "9 * 2 powr - real r \ 1" by simp hence "1 \ \ * (1 - 2 powr (- real r))" by (simp add:\_def) hence d: "(c*1) / (1 - 2 powr (-real r)) \ c * \" using assms two_pow_r_le_1 by (simp add: pos_divide_le_eq) have "\x. truncate_down r (real x) \ c \ real x * (1 - 2 powr - real r) \ c * 1" using truncate_down_pos[OF of_nat_0_le_iff] order_trans by (simp, blast) hence "\x. truncate_down r (real x) \ c \ real x \ c * \" using two_pow_r_le_1 by (intro order_trans[OF _ d], simp add: pos_le_divide_eq) hence e: "real u \ c * \" "real v \ c * \" using c_assms by auto have " \real u - real v\ \ (max \real u\ \real v\) * 2 powr (-real r)" using c_assms by (intro truncate_down_eq, simp) also have "... \ (c * \) * 2 powr (-real r)" using e by (intro mult_right_mono, auto) finally have "\real u - real v\ \ \ * c * 2 powr (-real r)" by (simp add:algebra_simps) thus ?thesis using e by (simp add:algebra_simps) qed have "prob {\. degree \ \ 1 \ tr_hash x \ \ c \ tr_hash x \ = tr_hash y \} \ prob (\ i \ {(u,v) \ {.. {.. v \ truncate_down r u \ c \ truncate_down r u = truncate_down r v}. {\. hash x \ = fst i \ hash y \ = snd i})" using a by (intro pmf_mono[OF M_def], simp add:tr_hash_def) (metis hash_range mod_ring_carr b_assms as_subset_p lessThan_iff nat_neq_iff subset_eq) also have "... \ (\ i\ {(u,v) \ {.. {.. v \ truncate_down r u \ c \ truncate_down r u = truncate_down r v}. prob {\. hash x \ = fst i \ hash y \ = snd i})" by (intro measure_UNION_le finite_cartesian_product finite_subset[where B="{0.. {0.. (\ i\ {(u,v) \ {.. {.. v \ truncate_down r u \ c \ truncate_down r u = truncate_down r v}. prob {\. (\u \ {x,y}. hash u \ = (if u = x then (fst i) else (snd i)))})" by (intro sum_mono pmf_mono[OF M_def]) force also have "... \ (\ i\ {(u,v) \ {.. {.. v \ truncate_down r u \ c \ truncate_down r u = truncate_down r v}. 1/(real p)\<^sup>2)" using assms as_subset_p b_assms by (intro sum_mono, subst hash_prob) (auto simp add: mod_ring_def power2_eq_square) also have "... = 1/(real p)\<^sup>2 * card {(u,v) \ {0.. {0.. v \ truncate_down r u \ c \ truncate_down r u = truncate_down r v}" by simp also have "... \ 1/(real p)\<^sup>2 * card {(u,v) \ {.. {.. v \ real u \ \ * c \ abs (real u - real v) \ \ * c * 2 powr (-real r)}" using c by (intro mult_mono of_nat_mono card_mono finite_cartesian_product finite_subset[where B="{..{.. 1/(real p)\<^sup>2 * card (\u' \ {u. u < p \ real u \ \ * c}. {(u::nat,v::nat). u = u' \ abs (real u - real v) \ \ * c * 2 powr (-real r) \ v < p \ v \ u'})" by (intro mult_left_mono of_nat_mono card_mono finite_cartesian_product finite_subset[where B="{..{.. 1/(real p)\<^sup>2 * (\ u' \ {u. u < p \ real u \ \ * c}. card {(u,v). u = u' \ abs (real u - real v) \ \ * c * 2 powr (-real r) \ v < p \ v \ u'})" by (intro mult_left_mono of_nat_mono card_UN_le, auto) also have "... = 1/(real p)\<^sup>2 * (\ u' \ {u. u < p \ real u \ \ * c}. card ((\x. (u' ,x)) ` {v. abs (real u' - real v) \ \ * c * 2 powr (-real r) \ v < p \ v \ u'}))" by (intro arg_cong2[where f="(*)"] arg_cong[where f="real"] sum.cong arg_cong[where f="card"]) (auto simp add:set_eq_iff) also have "... \ 1/(real p)\<^sup>2 * (\ u' \ {u. u < p \ real u \ \ * c}. card {v. abs (real u' - real v) \ \ * c * 2 powr (-real r) \ v < p \ v \ u'})" by (intro mult_left_mono of_nat_mono sum_mono card_image_le, auto) also have "... \ 1/(real p)\<^sup>2 * (\ u' \ {u. u < p \ real u \ \ * c}. card {v. abs (real u' - real v) \ \ * c * 2 powr (-real r) \ v \ u'})" by (intro mult_left_mono sum_mono of_nat_mono card_mono card_nat_in_ball subsetI) auto also have "... \ 1/(real p)\<^sup>2 * (\ u' \ {u. u < p \ real u \ \ * c}. real (card {v. abs (real u' - real v) \ \ * c * 2 powr (-real r) \ v \ u'}))" by simp also have "... \ 1/(real p)\<^sup>2 * (\ u' \ {u. u < p \ real u \ \ * c}. 2 * (\ * c * 2 powr (-real r)))" by (intro mult_left_mono sum_mono card_nat_in_ball(1), auto) also have "... = 1/(real p)\<^sup>2 * (real (card {u. u < p \ real u \ \ * c}) * (2 * (\ * c * 2 powr (-real r))))" by simp also have "... \ 1/(real p)\<^sup>2 * (real (card {u. u \ nat (\\ * c \)}) * (2 * (\ * c * 2 powr (-real r))))" using rho_c_ge_0 le_nat_floor by (intro mult_left_mono mult_right_mono of_nat_mono card_mono subsetI) auto also have "... \ 1/(real p)\<^sup>2 * ((1+\ * c) * (2 * (\ * c * 2 powr (-real r))))" using rho_c_ge_0 by (intro mult_left_mono mult_right_mono, auto) also have "... \ 1/(real p)\<^sup>2 * (((1+\) * c) * (2 * (\ * c * 2 powr (-real r))))" using assms by (intro mult_mono, auto simp add:distrib_left distrib_right \_def) also have "... = (\ * (2 + \ * 2)) * c\<^sup>2 * 2 powr (-real r) /(real p)\<^sup>2" by (simp add:ac_simps power2_eq_square) also have "... \ 5 * c\<^sup>2 * 2 powr (-real r) /(real p)\<^sup>2" by (intro divide_right_mono mult_right_mono) (auto simp add:\_def) finally show ?thesis by simp qed have "prob {\. ?l \ \ degree \ \ 1} \ prob (\ i \ {(x,y) \ (set as) \ (set as). x < y}. {\. degree \ \ 1 \ tr_hash (fst i) \ \ c \ tr_hash (fst i) \ = tr_hash (snd i) \})" by (rule pmf_mono[OF M_def], simp, metis linorder_neqE_nat) also have "... \ (\ i \ {(x,y) \ (set as) \ (set as). x < y}. prob {\. degree \ \ 1 \ tr_hash (fst i) \ \ c \ tr_hash (fst i) \ = tr_hash (snd i) \})" unfolding M_def by (intro measure_UNION_le finite_cartesian_product finite_subset[where B="(set as) \ (set as)"]) auto also have "... \ (\ i \ {(x,y) \ (set as) \ (set as). x < y}. 5 * c\<^sup>2 * 2 powr (-real r) /(real p)\<^sup>2)" using b by (intro sum_mono, simp add:case_prod_beta) also have "... = ((5/2) * c\<^sup>2 * 2 powr (-real r) /(real p)\<^sup>2) * (2 * card {(x,y) \ (set as) \ (set as). x < y})" by simp also have "... = ((5/2) * c\<^sup>2 * 2 powr (-real r) /(real p)\<^sup>2) * (card (set as) * (card (set as) - 1))" by (subst card_ordered_pairs, auto) also have "... \ ((5/2) * c\<^sup>2 * 2 powr (-real r) /(real p)\<^sup>2) * (real (card (set as)))\<^sup>2" by (intro mult_left_mono) (auto simp add:power2_eq_square mult_left_mono) also have "... = (5/2) * (real (card (set as)))\<^sup>2 * c\<^sup>2 * 2 powr (-real r) /(real p)\<^sup>2" by (simp add:algebra_simps) finally have f:"prob {\. ?l \ \ degree \ \ 1} \ ?r1" by simp have "prob {\. ?l \} \ prob {\. ?l \ \ degree \ \ 1} + prob {\. degree \ < 1}" by (rule pmf_add[OF M_def], auto) also have "... \ ?r1 + ?r2" by (intro add_mono f prob_degree_lt_1) finally show ?thesis by simp qed private lemma of_bool_square: "(of_bool x)\<^sup>2 = ((of_bool x)::real)" by (cases x, auto) private definition Q where "Q y \ = card {x \ set as. int (hash x \) < y}" private definition m where "m = card (set as)" private lemma assumes "a \ 0" assumes "a \ int p" shows exp_Q: "expectation (\\. real (Q a \)) = real m * (of_int a) / p" and var_Q: "variance (\\. real (Q a \)) \ real m * (of_int a) / p" proof - have exp_single: "expectation (\\. of_bool (int (hash x \) < a)) = real_of_int a /real p" if a:"x \ set as" for x proof - have x_le_p: "x < p" using a as_lt_p by simp have "expectation (\\. of_bool (int (hash x \) < a)) = expectation (indicat_real {\. int (Frequency_Moment_0.hash p x \) < a})" by (intro arg_cong2[where f="integral\<^sup>L"] ext, simp_all) also have "... = prob {\. hash x \ \ {k. int k < a}}" by (simp add:M_def) also have "... = card ({k. int k < a} \ {..\. of_bool (int (hash x \) < a)) = real_of_int a /real p" by simp qed have "expectation(\\. real (Q a \)) = expectation (\\. (\x \ set as. of_bool (int (hash x \) < a)))" by (simp add:Q_def Int_def) also have "... = (\x \ set as. expectation (\\. of_bool (int (hash x \) < a)))" by (rule Bochner_Integration.integral_sum, simp) also have "... = (\ x \ set as. a /real p)" by (rule sum.cong, simp, subst exp_single, simp, simp) also have "... = real m * real_of_int a / real p" by (simp add:m_def) finally show "expectation (\\. real (Q a \)) = real m * real_of_int a / p" by simp have indep: "J \ set as \ card J = 2 \ indep_vars (\_. borel) (\i x. of_bool (int (hash i x) < a)) J" for J using as_subset_p mod_ring_carr by (intro indep_vars_compose2[where Y="\i x. of_bool (int x < a)" and M'="\_. discrete"] k_wise_indep_vars_subset[OF k_wise_indep] finite_subset[OF _ finite_set]) auto have rv: "\x. x \ set as \ random_variable borel (\\. of_bool (int (hash x \) < a))" by (simp add:M_def) have "variance (\\. real (Q a \)) = variance (\\. (\x \ set as. of_bool (int (hash x \) < a)))" by (simp add:Q_def Int_def) also have "... = (\x \ set as. variance (\\. of_bool (int (hash x \) < a)))" by (intro bienaymes_identity_pairwise_indep_2 indep rv) auto also have "... \ (\ x \ set as. a / real p)" by (rule sum_mono, simp add: variance_eq of_bool_square, simp add: exp_single) also have "... = real m * real_of_int a /real p" by (simp add:m_def) finally show "variance (\\. real (Q a \)) \ real m * real_of_int a / p" by simp qed private lemma t_bound: "t \ 81 / (real_of_rat \)\<^sup>2" proof - have "t \ 80 / (real_of_rat \)\<^sup>2 + 1" using t_def t_gt_0 by linarith also have "... \ 80 / (real_of_rat \)\<^sup>2 + 1 / (real_of_rat \)\<^sup>2" using \_range by (intro add_mono, simp, simp add:power_le_one) also have "... = 81 / (real_of_rat \)\<^sup>2" by simp finally show ?thesis by simp qed private lemma t_r_bound: "18 * 40 * (real t)\<^sup>2 * 2 powr (-real r) \ 1" proof - have "720 * (real t)\<^sup>2 * 2 powr (-real r) \ 720 * (81 / (real_of_rat \)\<^sup>2)\<^sup>2 * 2 powr (-4 * log 2 (1 / real_of_rat \) - 23)" using r_bound t_bound by (intro mult_left_mono mult_mono power_mono powr_mono, auto) also have "... \ 720 * (81 / (real_of_rat \)\<^sup>2)\<^sup>2 * (2 powr (-4 * log 2 (1 / real_of_rat \)) * 2 powr (-23))" using \_range by (intro mult_left_mono mult_mono power_mono add_mono) (simp_all add:power_le_one powr_diff) also have "... = 720 * (81\<^sup>2 / (real_of_rat \)^4) * (2 powr (log 2 ((real_of_rat \)^4)) * 2 powr (-23))" using \_range by (intro arg_cong2[where f="(*)"]) (simp_all add:power2_eq_square power4_eq_xxxx log_divide log_powr[symmetric]) also have "... = 720 * 81\<^sup>2 * 2 powr (-23)" using \_range by simp also have "... \ 1" by simp finally show ?thesis by simp qed private lemma m_eq_F_0: "real m = of_rat (F 0 as)" by (simp add:m_def F_def) private lemma estimate'_bounds: "prob {\. of_rat \ * real_of_rat (F 0 as) < \estimate' (sketch_rv' \) - of_rat (F 0 as)\} \ 1/3" proof (cases "card (set as) \ t") case True define \' where "\' = 3 * real_of_rat \ / 4" define u where "u = \real t * p / (m * (1+\'))\" define v where "v = \real t * p / (m * (1-\'))\" define has_no_collision where "has_no_collision = (\\. \x\ set as. \y \ set as. (tr_hash x \ = tr_hash y \ \ x = y) \ tr_hash x \ > v)" have "2 powr (-real r) \ 2 powr (-(4 * log 2 (1 / real_of_rat \) + 23))" using r_bound by (intro powr_mono, linarith, simp) also have "... = 2 powr (-4 * log 2 (1 /real_of_rat \) -23)" by (rule arg_cong2[where f="(powr)"], auto simp add:algebra_simps) also have "... \ 2 powr ( -1 * log 2 (1 /real_of_rat \) -4)" using \_range by (intro powr_mono diff_mono, auto) also have "... = 2 powr ( -1 * log 2 (1 /real_of_rat \)) / 16" by (simp add: powr_diff) also have "... = real_of_rat \ / 16" using \_range by (simp add:log_divide) also have "... < real_of_rat \ / 8" using \_range by (subst pos_divide_less_eq, auto) finally have r_le_\: "2 powr (-real r) < real_of_rat \ / 8" by simp have \'_gt_0: "\' > 0" using \_range by (simp add:\'_def) have "\' < 3/4" using \_range by (simp add:\'_def)+ also have "... < 1" by simp finally have \'_lt_1: "\' < 1" by simp have "t \ 81 / (real_of_rat \)\<^sup>2" using t_bound by simp also have "... = (81*9/16) / (\')\<^sup>2" by (simp add:\'_def power2_eq_square) also have "... \ 46 / \'\<^sup>2" by (intro divide_right_mono, simp, simp) finally have t_le_\': "t \ 46/ \'\<^sup>2" by simp have "80 \ (real_of_rat \)\<^sup>2 * (80 / (real_of_rat \)\<^sup>2)" using \_range by simp also have "... \ (real_of_rat \)\<^sup>2 * t" by (intro mult_left_mono, simp add:t_def of_nat_ceiling, simp) finally have "80 \ (real_of_rat \)\<^sup>2 * t" by simp hence t_ge_\': "45 \ t * \' * \'" by (simp add:\'_def power2_eq_square) have "m \ card {.. p" using n_le_p by simp finally have m_le_p: "m \ p" by simp hence t_le_m: "t \ card (set as)" using True by simp have m_ge_0: "real m > 0" using m_def True t_gt_0 by simp have "v \ real t * real p / (real m * (1 - \'))" by (simp add:v_def) also have "... \ real t * real p / (real m * (1/4))" using \'_lt_1 m_ge_0 \_range by (intro divide_left_mono mult_left_mono mult_nonneg_nonneg mult_pos_pos, simp_all add:\'_def) finally have v_ubound: "v \ 4 * real t * real p / real m" by (simp add:algebra_simps) have a_ge_1: "u \ 1" using \'_gt_0 p_gt_0 m_ge_0 t_gt_0 by (auto intro!:mult_pos_pos divide_pos_pos simp add:u_def) hence a_ge_0: "u \ 0" by simp have "real m * (1 - \') < real m" using \'_gt_0 m_ge_0 by simp also have "... \ 1 * real p" using m_le_p by simp also have "... \ real t * real p" using t_gt_0 by (intro mult_right_mono, auto) finally have " real m * (1 - \') < real t * real p" by simp hence v_gt_0: "v > 0" using mult_pos_pos m_ge_0 \'_lt_1 by (simp add:v_def) hence v_ge_1: "real_of_int v \ 1" by linarith have "real t \ real m" using True m_def by linarith also have "... < (1 + \') * real m" using \'_gt_0 m_ge_0 by force finally have a_le_p_aux: "real t < (1 + \') * real m" by simp have "u \ real t * real p / (real m * (1 + \'))+1" by (simp add:u_def) also have "... < real p + 1" using m_ge_0 \'_gt_0 a_le_p_aux a_le_p_aux p_gt_0 by (simp add: pos_divide_less_eq ac_simps) finally have "u \ real p" by (metis int_less_real_le not_less of_int_le_iff of_int_of_nat_eq) hence u_le_p: "u \ int p" by linarith have "prob {\. Q u \ \ t} \ prob {\ \ Sigma_Algebra.space M. abs (real (Q u \) - expectation (\\. real (Q u \))) \ 3 * sqrt (m * real_of_int u / p)}" proof (rule pmf_mono[OF M_def]) fix \ assume "\ \ {\. t \ Q u \}" hence t_le: "t \ Q u \" by simp have "real m * real_of_int u / real p \ real m * (real t * real p / (real m * (1 + \'))+1) / real p" using m_ge_0 p_gt_0 by (intro divide_right_mono mult_left_mono, simp_all add: u_def) also have "... = real m * real t * real p / (real m * (1+\') * real p) + real m / real p" by (simp add:distrib_left add_divide_distrib) also have "... = real t / (1+\') + real m / real p" using p_gt_0 m_ge_0 by simp also have "... \ real t / (1+\') + 1" using m_le_p p_gt_0 by (intro add_mono, auto) finally have "real m * real_of_int u / real p \ real t / (1 + \') + 1" by simp hence "3 * sqrt (real m * of_int u / real p) + real m * of_int u / real p \ 3 * sqrt (t / (1+\')+1)+(t/(1+\')+1)" by (intro add_mono mult_left_mono real_sqrt_le_mono, auto) also have "... \ 3 * sqrt (real t+1) + ((t * (1 - \' / (1+\'))) + 1)" using \'_gt_0 t_gt_0 by (intro add_mono mult_left_mono real_sqrt_le_mono) (simp_all add: pos_divide_le_eq left_diff_distrib) also have "... = 3 * sqrt (real t+1) + (t - \' * t / (1+\')) + 1" by (simp add:algebra_simps) also have "... \ 3 * sqrt (46 / \'\<^sup>2 + 1 / \'\<^sup>2) + (t - \' * t/2) + 1 / \'" using \'_gt_0 t_gt_0 \'_lt_1 add_pos_pos t_le_\' by (intro add_mono mult_left_mono real_sqrt_le_mono add_mono) (simp_all add: power_le_one pos_le_divide_eq) also have "... \ (21 / \' + (t - 45 / (2*\'))) + 1 / \'" using \'_gt_0 t_ge_\' by (intro add_mono) (simp_all add:real_sqrt_divide divide_le_cancel real_le_lsqrt pos_divide_le_eq ac_simps) also have "... \ t" using \'_gt_0 by simp also have "... \ Q u \" using t_le by simp finally have "3 * sqrt (real m * of_int u / real p) + real m * of_int u / real p \ Q u \" by simp hence " 3 * sqrt (real m * real_of_int u / real p) \ \real (Q u \) - expectation (\\. real (Q u \))\" using a_ge_0 u_le_p True by (simp add:exp_Q abs_ge_iff) thus "\ \ {\ \ Sigma_Algebra.space M. 3 * sqrt (real m * real_of_int u / real p) \ \real (Q u \) - expectation (\\. real (Q u \))\}" by (simp add: M_def) qed also have "... \ variance (\\. real (Q u \)) / (3 * sqrt (real m * of_int u / real p))\<^sup>2" using a_ge_1 p_gt_0 m_ge_0 by (intro Chebyshev_inequality, simp add:M_def, auto) also have "... \ (real m * real_of_int u / real p) / (3 * sqrt (real m * of_int u / real p))\<^sup>2" using a_ge_0 u_le_p by (intro divide_right_mono var_Q, auto) also have "... \ 1/9" using a_ge_0 by simp finally have case_1: "prob {\. Q u \ \ t} \ 1/9" by simp have case_2: "prob {\. Q v \ < t} \ 1/9" proof (cases "v \ p") case True have "prob {\. Q v \ < t} \ prob {\ \ Sigma_Algebra.space M. abs (real (Q v \) - expectation (\\. real (Q v \))) \ 3 * sqrt (m * real_of_int v / p)}" proof (rule pmf_mono[OF M_def]) fix \ assume "\ \ set_pmf (pmf_of_set space)" have "(real t + 3 * sqrt (real t / (1 - \') )) * (1 - \') = real t - \' * t + 3 * ((1-\') * sqrt( real t / (1-\') ))" by (simp add:algebra_simps) also have "... = real t - \' * t + 3 * sqrt ( (1-\')\<^sup>2 * (real t / (1-\')))" using \'_lt_1 by (subst real_sqrt_mult, simp) also have "... = real t - \' * t + 3 * sqrt ( real t * (1- \'))" by (simp add:power2_eq_square distrib_left) also have "... \ real t - 45/ \' + 3 * sqrt ( real t )" using \'_gt_0 t_ge_\' \'_lt_1 by (intro add_mono mult_left_mono real_sqrt_le_mono) (simp_all add:pos_divide_le_eq ac_simps left_diff_distrib power_le_one) also have "... \ real t - 45/ \' + 3 * sqrt ( 46 / \'\<^sup>2)" using t_le_\' \'_lt_1 \'_gt_0 by (intro add_mono mult_left_mono real_sqrt_le_mono, simp_all add:pos_divide_le_eq power_le_one) also have "... = real t + (3 * sqrt(46) - 45)/ \'" using \'_gt_0 by (simp add:real_sqrt_divide diff_divide_distrib) also have "... \ t" using \'_gt_0 by (simp add:pos_divide_le_eq real_le_lsqrt) finally have aux: "(real t + 3 * sqrt (real t / (1 - \'))) * (1 - \') \ real t " by simp assume "\ \ {\. Q v \ < t}" hence "Q v \ < t" by simp hence "real (Q v \) + 3 * sqrt (real m * real_of_int v / real p) \ real t - 1 + 3 * sqrt (real m * real_of_int v / real p)" using m_le_p p_gt_0 by (intro add_mono, auto simp add: algebra_simps add_divide_distrib) also have "... \ (real t-1) + 3 * sqrt (real m * (real t * real p / (real m * (1- \'))) / real p)" by (intro add_mono mult_left_mono real_sqrt_le_mono divide_right_mono) (auto simp add:v_def) also have "... \ real t + 3 * sqrt(real t / (1-\')) - 1" using m_ge_0 p_gt_0 by simp also have "... \ real t / (1-\')-1" using \'_lt_1 aux by (simp add: pos_le_divide_eq) also have "... \ real m * (real t * real p / (real m * (1-\'))) / real p - 1" using p_gt_0 m_ge_0 by simp also have "... \ real m * (real t * real p / (real m * (1-\'))) / real p - real m / real p" using m_le_p p_gt_0 by (intro diff_mono, auto) also have "... = real m * (real t * real p / (real m * (1-\'))-1) / real p" by (simp add: left_diff_distrib right_diff_distrib diff_divide_distrib) also have "... \ real m * real_of_int v / real p" by (intro divide_right_mono mult_left_mono, simp_all add:v_def) finally have "real (Q v \) + 3 * sqrt (real m * real_of_int v / real p) \ real m * real_of_int v / real p" by simp hence " 3 * sqrt (real m * real_of_int v / real p) \ \real (Q v \) -expectation (\\. real (Q v \))\" using v_gt_0 True by (simp add: exp_Q abs_ge_iff) thus "\ \ {\\ Sigma_Algebra.space M. 3 * sqrt (real m * real_of_int v / real p) \ \real (Q v \) - expectation (\\. real (Q v \))\}" by (simp add:M_def) qed also have "... \ variance (\\. real (Q v \)) / (3 * sqrt (real m * real_of_int v / real p))\<^sup>2" using v_gt_0 p_gt_0 m_ge_0 by (intro Chebyshev_inequality, simp add:M_def, auto) also have "... \ (real m * real_of_int v / real p) / (3 * sqrt (real m * real_of_int v / real p))\<^sup>2" using v_gt_0 True by (intro divide_right_mono var_Q, auto) also have "... = 1/9" using p_gt_0 v_gt_0 m_ge_0 by (simp add:power2_eq_square) finally show ?thesis by simp next case False have "prob {\. Q v \ < t} \ prob {\. False}" proof (rule pmf_mono[OF M_def]) fix \ assume a:"\ \ {\. Q v \ < t}" assume "\ \ set_pmf (pmf_of_set space)" hence b:"\x. x < p \ hash x \ < p" using hash_range mod_ring_carr by (simp add:M_def measure_pmf_inverse) have "t \ card (set as)" using True by simp also have "... \ Q v \" unfolding Q_def using b False as_lt_p by (intro card_mono subsetI, simp, force) also have "... < t" using a by simp finally have "False" by auto thus "\ \ {\. False}" by simp qed also have "... = 0" by auto finally show ?thesis by simp qed have "prob {\. \has_no_collision \} \ prob {\. \x \ set as. \y \ set as. x \ y \ tr_hash x \ \ real_of_int v \ tr_hash x \ = tr_hash y \}" by (rule pmf_mono[OF M_def]) (simp add:has_no_collision_def M_def, force) also have "... \ (5/2) * (real (card (set as)))\<^sup>2 * (real_of_int v)\<^sup>2 * 2 powr - real r / (real p)\<^sup>2 + 1 / real p" using collision_prob v_ge_1 by blast also have "... \ (5/2) * (real m)\<^sup>2 * (real_of_int v)\<^sup>2 * 2 powr - real r / (real p)\<^sup>2 + 1 / real p" by (intro divide_right_mono add_mono mult_right_mono mult_mono power_mono, simp_all add:m_def) also have "... \ (5/2) * (real m)\<^sup>2 * (4 * real t * real p / real m)\<^sup>2 * (2 powr - real r) / (real p)\<^sup>2 + 1 / real p" using v_def v_ge_1 v_ubound by (intro add_mono divide_right_mono mult_right_mono mult_left_mono, auto) also have "... = 40 * (real t)\<^sup>2 * (2 powr -real r) + 1 / real p" using p_gt_0 m_ge_0 t_gt_0 by (simp add:algebra_simps power2_eq_square) also have "... \ 1/18 + 1/18" using t_r_bound p_ge_18 by (intro add_mono, simp_all add: pos_le_divide_eq) also have "... = 1/9" by simp finally have case_3: "prob {\. \has_no_collision \} \ 1/9" by simp have "prob {\. real_of_rat \ * of_rat (F 0 as) < \estimate' (sketch_rv' \) - of_rat (F 0 as)\} \ prob {\. Q u \ \ t \ Q v \ < t \ \(has_no_collision \)}" proof (rule pmf_mono[OF M_def], rule ccontr) fix \ assume "\ \ set_pmf (pmf_of_set space)" assume "\ \ {\. real_of_rat \ * real_of_rat (F 0 as) < \estimate' (sketch_rv' \) - real_of_rat (F 0 as)\}" hence est: "real_of_rat \ * real_of_rat (F 0 as) < \estimate' (sketch_rv' \) - real_of_rat (F 0 as)\" by simp assume "\ \ {\. t \ Q u \ \ Q v \ < t \ \ has_no_collision \}" hence "\( t \ Q u \ \ Q v \ < t \ \ has_no_collision \)" by simp hence lb: "Q u \ < t" and ub: "Q v \ \ t" and no_col: "has_no_collision \" by simp+ define y where "y = nth_mset (t-1) {#int (hash x \). x \# mset_set (set as)#}" define y' where "y' = nth_mset (t-1) {#tr_hash x \. x \# mset_set (set as)#}" have rank_t_lb: "u \ y" unfolding y_def using True t_gt_0 lb by (intro nth_mset_bound_left, simp_all add:count_less_def swap_filter_image Q_def) have rank_t_ub: "y \ v - 1" unfolding y_def using True t_gt_0 ub by (intro nth_mset_bound_right, simp_all add:Q_def swap_filter_image count_le_def) have y_ge_0: "real_of_int y \ 0" using rank_t_lb a_ge_0 by linarith have "mono (\x. truncate_down r (real_of_int x))" by (metis truncate_down_mono mono_def of_int_le_iff) hence y'_eq: "y' = truncate_down r y" unfolding y_def y'_def using True t_gt_0 by (subst nth_mset_commute_mono[where f="(\x. truncate_down r (of_int x))"]) (simp_all add: multiset.map_comp comp_def tr_hash_def) have "real_of_int u * (1 - 2 powr -real r) \ real_of_int y * (1 - 2 powr (-real r))" using rank_t_lb of_int_le_iff two_pow_r_le_1 by (intro mult_right_mono, auto) also have "... \ y'" using y'_eq truncate_down_pos[OF y_ge_0] by simp finally have rank_t_lb': "u * (1 - 2 powr -real r) \ y'" by simp have "y' \ real_of_int y" by (subst y'_eq, rule truncate_down_le, simp) also have "... \ real_of_int (v-1)" using rank_t_ub of_int_le_iff by blast finally have rank_t_ub': "y' \ v-1" by simp have "0 < u * (1-2 powr -real r)" using a_ge_1 two_pow_r_le_1 by (intro mult_pos_pos, auto) hence y'_pos: "y' > 0" using rank_t_lb' by linarith have no_col': "\x. x \ y' \ count {#tr_hash x \. x \# mset_set (set as)#} x \ 1" using rank_t_ub' no_col by (simp add:vimage_def card_le_Suc0_iff_eq count_image_mset has_no_collision_def) force have h_1: "Max (sketch_rv' \) = y'" using True t_gt_0 no_col' by (simp add:sketch_rv'_def y'_def nth_mset_max) have "card (sketch_rv' \) = card (least ((t-1)+1) (set_mset {#tr_hash x \. x \# mset_set (set as)#}))" using t_gt_0 by (simp add:sketch_rv'_def) also have "... = (t-1) +1" using True t_gt_0 no_col' by (intro nth_mset_max(2), simp_all add:y'_def) also have "... = t" using t_gt_0 by simp finally have "card (sketch_rv' \) = t" by simp hence h_3: "estimate' (sketch_rv' \) = real t * real p / y'" using h_1 by (simp add:estimate'_def) have "(real t) * real p \ (1 + \') * real m * ((real t) * real p / (real m * (1 + \')))" using \'_lt_1 m_def True t_gt_0 \'_gt_0 by auto also have "... \ (1+\') * m * u" using \'_gt_0 by (intro mult_left_mono, simp_all add:u_def) also have "... < ((1 + real_of_rat \)*(1-real_of_rat \/8)) * m * u" using True m_def t_gt_0 a_ge_1 \_range by (intro mult_strict_right_mono, auto simp add:\'_def right_diff_distrib) also have "... \ ((1 + real_of_rat \)*(1-2 powr (-r))) * m * u" using r_le_\ \_range a_ge_0 by (intro mult_right_mono mult_left_mono, auto) also have "... = (1 + real_of_rat \) * m * (u * (1-2 powr -real r))" by simp also have "... \ (1 + real_of_rat \) * m * y'" using \_range by (intro mult_left_mono rank_t_lb', simp) finally have "real t * real p < (1 + real_of_rat \) * m * y'" by simp hence f_1: "estimate' (sketch_rv' \) < (1 + real_of_rat \) * m" using y'_pos by (simp add: h_3 pos_divide_less_eq) have "(1 - real_of_rat \) * m * y' \ (1 - real_of_rat \) * m * v" using \_range rank_t_ub' y'_pos by (intro mult_mono rank_t_ub', simp_all) also have "... = (1-real_of_rat \) * (real m * v)" by simp also have "... < (1-\') * (real m * v)" using \_range m_ge_0 v_ge_1 by (intro mult_strict_right_mono mult_pos_pos, simp_all add:\'_def) also have "... \ (1-\') * (real m * (real t * real p / (real m * (1-\'))))" using \'_gt_0 \'_lt_1 by (intro mult_left_mono, auto simp add:v_def) also have "... = real t * real p" using \'_gt_0 \'_lt_1 t_gt_0 p_gt_0 m_ge_0 by auto finally have "(1 - real_of_rat \) * m * y' < real t * real p" by simp hence f_2: "estimate' (sketch_rv' \) > (1 - real_of_rat \) * m" using y'_pos by (simp add: h_3 pos_less_divide_eq) have "abs (estimate' (sketch_rv' \) - real_of_rat (F 0 as)) < real_of_rat \ * (real_of_rat (F 0 as))" using f_1 f_2 by (simp add:abs_less_iff algebra_simps m_eq_F_0) thus "False" using est by linarith qed also have "... \ 1/9 + (1/9 + 1/9)" by (intro pmf_add_2[OF M_def] case_1 case_2 case_3) also have "... = 1/3" by simp finally show ?thesis by simp next case False have "prob {\. real_of_rat \ * of_rat (F 0 as) < \estimate' (sketch_rv' \) - of_rat (F 0 as)\} \ prob {\. \x \ set as. \y \ set as. x \ y \ tr_hash x \ \ real p \ tr_hash x \ = tr_hash y \}" proof (rule pmf_mono[OF M_def]) fix \ assume a:"\ \ {\. real_of_rat \ * real_of_rat (F 0 as) < \estimate' (sketch_rv' \) - real_of_rat (F 0 as)\}" assume b:"\ \ set_pmf (pmf_of_set space)" have c: "card (set as) < t" using False by auto hence "card ((\x. tr_hash x \) ` set as) < t" using card_image_le order_le_less_trans by blast hence d:"card (sketch_rv' \) = card ((\x. tr_hash x \) ` (set as))" by (simp add:sketch_rv'_def card_least) have "card (sketch_rv' \) < t" by (metis List.finite_set c d card_image_le order_le_less_trans) hence "estimate' (sketch_rv' \) = card (sketch_rv' \)" by (simp add:estimate'_def) hence "card (sketch_rv' \) \ real_of_rat (F 0 as)" using a \_range by simp (metis abs_zero cancel_comm_monoid_add_class.diff_cancel of_nat_less_0_iff pos_prod_lt zero_less_of_rat_iff) hence "card (sketch_rv' \) \ card (set as)" using m_def m_eq_F_0 by linarith hence "\inj_on (\x. tr_hash x \) (set as)" using card_image d by auto moreover have "tr_hash x \ \ real p" if a:"x \ set as" for x proof - have "hash x \ < p" using hash_range as_lt_p a b by (simp add:mod_ring_carr M_def) thus "tr_hash x \ \ real p" using truncate_down_le by (simp add:tr_hash_def) qed ultimately show "\ \ {\. \x \ set as. \y \ set as. x \ y \ tr_hash x \ \ real p \ tr_hash x \ = tr_hash y \}" by (simp add:inj_on_def, blast) qed also have "... \ (5/2) * (real (card (set as)))\<^sup>2 * (real p)\<^sup>2 * 2 powr - real r / (real p)\<^sup>2 + 1 / real p" using p_gt_0 by (intro collision_prob, auto) also have "... = (5/2) * (real (card (set as)))\<^sup>2 * 2 powr (- real r) + 1 / real p" using p_gt_0 by (simp add:ac_simps power2_eq_square) also have "... \ (5/2) * (real t)\<^sup>2 * 2 powr (-real r) + 1 / real p" using False by (intro add_mono mult_right_mono mult_left_mono power_mono, auto) also have "... \ 1/6 + 1/6" using t_r_bound p_ge_18 by (intro add_mono, simp_all) also have "... \ 1/3" by simp finally show ?thesis by simp qed private lemma median_bounds: "\

(\ in measure_pmf \\<^sub>0. \median s (\i. estimate (sketch_rv (\ i))) - F 0 as\ \ \ * F 0 as) \ 1 - real_of_rat \" proof - have "strict_mono_on A real_of_float" for A by (meson less_float.rep_eq strict_mono_onI) hence real_g_2: "\\. sketch_rv' \ = real_of_float ` sketch_rv \" by (simp add: sketch_rv'_def sketch_rv_def tr_hash_def least_mono_commute image_comp) moreover have "inj_on real_of_float A" for A using real_of_float_inject by (simp add:inj_on_def) ultimately have card_eq: "\\. card (sketch_rv \) = card (sketch_rv' \)" using real_g_2 by (auto intro!: card_image[symmetric]) have "Max (sketch_rv' \) = real_of_float (Max (sketch_rv \))" if a:"card (sketch_rv' \) \ t" for \ proof - have "mono real_of_float" using less_eq_float.rep_eq mono_def by blast moreover have "finite (sketch_rv \)" by (simp add:sketch_rv_def least_def) moreover have " sketch_rv \ \ {}" using card_eq[symmetric] card_gt_0_iff t_gt_0 a by (simp, force) ultimately show ?thesis by (subst mono_Max_commute[where f="real_of_float"], simp_all add:real_g_2) qed hence real_g: "\\. estimate' (sketch_rv' \) = real_of_rat (estimate (sketch_rv \))" by (simp add:estimate_def estimate'_def card_eq of_rat_divide of_rat_mult of_rat_add real_of_rat_of_float) have indep: "prob_space.indep_vars (measure_pmf \\<^sub>0) (\_. borel) (\i \. estimate' (sketch_rv' (\ i))) {0..\<^sub>0_def by (rule indep_vars_restrict_intro', auto simp add:restrict_dfl_def lessThan_atLeast0) moreover have "- (18 * ln (real_of_rat \)) \ real s" using of_nat_ceiling by (simp add:s_def) blast moreover have "i < s \ measure \\<^sub>0 {\. of_rat \ * of_rat (F 0 as) < \estimate' (sketch_rv' (\ i)) - of_rat (F 0 as)\} \ 1/3" for i using estimate'_bounds unfolding \\<^sub>0_def M_def by (subst prob_prod_pmf_slice, simp_all) ultimately have "1-real_of_rat \ \ \

(\ in measure_pmf \\<^sub>0. \median s (\i. estimate' (sketch_rv' (\ i))) - real_of_rat (F 0 as)\ \ real_of_rat \ * real_of_rat (F 0 as))" using \_range prob_space_measure_pmf by (intro prob_space.median_bound_2) auto also have "... = \

(\ in measure_pmf \\<^sub>0. \median s (\i. estimate (sketch_rv (\ i))) - F 0 as\ \ \ * F 0 as)" using s_gt_0 median_rat[symmetric] real_g by (intro arg_cong2[where f="measure"]) (simp_all add:of_rat_diff[symmetric] of_rat_mult[symmetric] of_rat_less_eq) finally show "\

(\ in measure_pmf \\<^sub>0. \median s (\i. estimate (sketch_rv (\ i))) - F 0 as\ \ \ * F 0 as) \ 1-real_of_rat \" by blast qed lemma f0_alg_correct': "\

(\ in measure_pmf result. \\ - F 0 as\ \ \ * F 0 as) \ 1 - of_rat \" proof - have f0_result_elim: "\x. f0_result (s, t, p, r, x, \i\{..i. estimate (sketch_rv (x i))))" by (simp add:estimate_def, rule median_cong, simp) have "result = map_pmf (\x. (s, t, p, r, x, \i\{..\<^sub>0 \ f0_result" by (subst result_def, subst f0_alg_sketch, simp) also have "... = \\<^sub>0 \ (\x. return_pmf (s, t, p, r, x, \i\{.. f0_result" by (simp add:t_def p_def r_def s_def map_pmf_def) also have "... = \\<^sub>0 \ (\x. return_pmf (median s (\i. estimate (sketch_rv (x i)))))" by (subst bind_assoc_pmf, subst bind_return_pmf, subst f0_result_elim) simp finally have a:"result = \\<^sub>0 \ (\x. return_pmf (median s (\i. estimate (sketch_rv (x i)))))" by simp show ?thesis using median_bounds by (simp add: a map_pmf_def[symmetric]) qed private lemma f_subset: assumes "g ` A \ h ` B" shows "(\x. f (g x)) ` A \ (\x. f (h x)) ` B" using assms by auto lemma f0_exact_space_usage': defines "\ \ fold (\a state. state \ f0_update a) as (f0_init \ \ n)" shows "AE \ in \. bit_count (encode_f0_state \) \ f0_space_usage (n, \, \)" proof - have log_2_4: "log 2 4 = 2" by (metis log2_of_power_eq mult_2 numeral_Bit0 of_nat_numeral power2_eq_square) have a: "bit_count (F\<^sub>e (float_of (truncate_down r y))) \ ereal (12 + 4 * real r + 2 * log 2 (log 2 (n+13)))" if a_1:"y \ {.. 1") case True have aux_1: " 0 < 2 + log 2 (real y)" using True by (intro add_pos_nonneg, auto) have aux_2: "0 < 2 + log 2 (real p)" using p_gt_1 by (intro add_pos_nonneg, auto) have "bit_count (F\<^sub>e (float_of (truncate_down r y))) \ ereal (10 + 4 * real r + 2 * log 2 (2 + \log 2 \real y\\))" by (rule truncate_float_bit_count) also have "... = ereal (10 + 4 * real r + 2 * log 2 (2 + (log 2 (real y))))" using True by simp also have "... \ ereal (10 + 4 * real r + 2 * log 2 (2 + log 2 p))" using aux_1 aux_2 True p_gt_0 a_1 by simp also have "... \ ereal (10 + 4 * real r + 2 * log 2 (log 2 4 + log 2 (2 * n + 40)))" using log_2_4 p_le_n p_gt_0 - by (intro ereal_mono add_mono mult_left_mono log_mono of_nat_mono add_pos_nonneg, auto) + by (simp add: Transcendental.log_mono aux_2) also have "... = ereal (10 + 4 * real r + 2 * log 2 (log 2 (8 * n + 160)))" by (simp add:log_mult[symmetric]) also have "... \ ereal (10 + 4 * real r + 2 * log 2 (log 2 ((n+13) powr 2)))" - by (intro ereal_mono add_mono mult_left_mono log_mono of_nat_mono add_pos_nonneg) + by (intro ereal_mono add_mono mult_left_mono Transcendental.log_mono of_nat_mono add_pos_nonneg) (auto simp add:power2_eq_square algebra_simps) also have "... = ereal (10 + 4 * real r + 2 * log 2 (log 2 4 * log 2 (n + 13)))" by (subst log_powr, simp_all add:log_2_4) also have "... = ereal (12 + 4 * real r + 2 * log 2 (log 2 (n + 13)))" by (subst log_mult, simp_all add:log_2_4) finally show ?thesis by simp next case False hence "y = 0" using a_1 by simp then show ?thesis by (simp add:float_bit_count_zero) qed have "bit_count (encode_f0_state (s, t, p, r, x, \i\{.. f0_space_usage (n, \, \)" if b: "x \ {..\<^sub>E space" for x proof - have c: "x \ extensional {.. (\k. float_of (truncate_down r k)) ` {.. (\xa. float_of (truncate_down r (hash xa (x y)))) ` set as" using least_subset by (auto simp add:sketch_rv_def tr_hash_def) also have "... \ (\k. float_of (truncate_down r (real k))) ` {..y. y < s \ finite (sketch_rv (x y))" unfolding sketch_rv_def by (rule finite_subset[OF least_subset], simp) moreover have card_sketch: "\y. y < s \ card (sketch_rv (x y)) \ t " by (simp add:sketch_rv_def card_least) moreover have "\y z. y < s \ z \ sketch_rv (x y) \ bit_count (F\<^sub>e z) \ ereal (12 + 4 * real r + 2 * log 2 (log 2 (real n + 13)))" using a d by auto ultimately have e: "\y. y < s \ bit_count (S\<^sub>e F\<^sub>e (sketch_rv (x y))) \ ereal (real t) * (ereal (12 + 4 * real r + 2 * log 2 (log 2 (real (n + 13)))) + 1) + 1" using float_encoding by (intro set_bit_count_est, auto) have f: "\y. y < s \ bit_count (P\<^sub>e p 2 (x y)) \ ereal (real 2 * (log 2 (real p) + 1))" using p_gt_1 b by (intro bounded_degree_polynomial_bit_count) (simp_all add:space_def PiE_def Pi_def) have "bit_count (encode_f0_state (s, t, p, r, x, \i\{..e s) + bit_count (N\<^sub>e t) + bit_count (N\<^sub>e p) + bit_count (N\<^sub>e r) + bit_count (([0..\<^sub>e P\<^sub>e p 2) x) + bit_count (([0..\<^sub>e S\<^sub>e F\<^sub>e) (\i\{.. ereal (2* log 2 (real s + 1) + 1) + ereal (2* log 2 (real t + 1) + 1) + ereal (2* log 2 (real p + 1) + 1) + ereal (2 * log 2 (real r + 1) + 1) + (ereal (real s) * (ereal (real 2 * (log 2 (real p) + 1)))) + (ereal (real s) * ((ereal (real t) * (ereal (12 + 4 * real r + 2 * log 2 (log 2 (real (n + 13)))) + 1) + 1)))" using c e f by (intro add_mono exp_golomb_bit_count fun_bit_count_est[where xs="[0.. ereal ( 4 + 2 * log 2 (real s + 1) + 2 * log 2 (real t + 1) + 2 * log 2 (2 * (21 + real n)) + 2 * log 2 (real r + 1) + real s * (3 + 2 * log 2 (2 * (21 + real n)) + real t * (13 + (4 * real r + 2 * log 2 (log 2 (real n + 13))))))" using p_le_n p_gt_0 by (intro ereal_mono add_mono mult_left_mono, auto) also have "... = ereal (6 + 2 * log 2 (real s + 1) + 2 * log 2 (real t + 1) + 2 * log 2 (21 + real n) + 2 * log 2 (real r + 1) + real s * (5 + 2 * log 2 (21 + real n) + real t * (13 + (4 * real r + 2 * log 2 (log 2 (real n + 13))))))" by (subst (1 2) log_mult, auto) also have "... \ f0_space_usage (n, \, \)" by (simp add:s_def[symmetric] r_def[symmetric] t_def[symmetric] Let_def) (simp add:algebra_simps) finally show "bit_count (encode_f0_state (s, t, p, r, x, \i\{.. f0_space_usage (n, \, \)" by simp qed hence "\x. x \ set_pmf \\<^sub>0 \ bit_count (encode_f0_state (s, t, p, r, x, \i\{.. ereal (f0_space_usage (n, \, \))" by (simp add:\\<^sub>0_def set_prod_pmf del:f0_space_usage.simps) hence "\y. y \ set_pmf \ \ bit_count (encode_f0_state y) \ ereal (f0_space_usage (n, \, \))" by (simp add: \_def f0_alg_sketch del:f0_space_usage.simps f0_init.simps) (metis (no_types, lifting) image_iff pmf.set_map) thus ?thesis by (simp add: AE_measure_pmf_iff del:f0_space_usage.simps) qed end text \Main results of this section:\ theorem f0_alg_correct: assumes "\ \ {0<..<1}" assumes "\ \ {0<..<1}" assumes "set as \ {.. \ fold (\a state. state \ f0_update a) as (f0_init \ \ n) \ f0_result" shows "\

(\ in measure_pmf \. \\ - F 0 as\ \ \ * F 0 as) \ 1 - of_rat \" using f0_alg_correct'[OF assms(1-3)] unfolding \_def by blast theorem f0_exact_space_usage: assumes "\ \ {0<..<1}" assumes "\ \ {0<..<1}" assumes "set as \ {.. \ fold (\a state. state \ f0_update a) as (f0_init \ \ n)" shows "AE \ in \. bit_count (encode_f0_state \) \ f0_space_usage (n, \, \)" using f0_exact_space_usage'[OF assms(1-3)] unfolding \_def by blast theorem f0_asymptotic_space_complexity: "f0_space_usage \ O[at_top \\<^sub>F at_right 0 \\<^sub>F at_right 0](\(n, \, \). ln (1 / of_rat \) * (ln (real n) + 1 / (of_rat \)\<^sup>2 * (ln (ln (real n)) + ln (1 / of_rat \))))" (is "_ \ O[?F](?rhs)") proof - define n_of :: "nat \ rat \ rat \ nat" where "n_of = (\(n, \, \). n)" define \_of :: "nat \ rat \ rat \ rat" where "\_of = (\(n, \, \). \)" define \_of :: "nat \ rat \ rat \ rat" where "\_of = (\(n, \, \). \)" define t_of where "t_of = (\x. nat \80 / (real_of_rat (\_of x))\<^sup>2\)" define s_of where "s_of = (\x. nat \-(18 * ln (real_of_rat (\_of x)))\)" define r_of where "r_of = (\x. nat (4 * \log 2 (1 / real_of_rat (\_of x))\ + 23))" define g where "g = (\x. ln (1 / of_rat (\_of x)) * (ln (real (n_of x)) + 1 / (of_rat (\_of x))\<^sup>2 * (ln (ln (real (n_of x))) + ln (1 / of_rat (\_of x)))))" have evt: "(\x. 0 < real_of_rat (\_of x) \ 0 < real_of_rat (\_of x) \ 1/real_of_rat (\_of x) \ \ \ 1/real_of_rat (\_of x) \ \ \ real (n_of x) \ n \ P x) \ eventually P ?F" (is "(\x. ?prem x \ _) \ _") for \ \ n P apply (rule eventually_mono[where P="?prem" and Q="P"]) apply (simp add:\_of_def case_prod_beta' \_of_def n_of_def) apply (intro eventually_conj eventually_prod1' eventually_prod2' sequentially_inf eventually_at_right_less inv_at_right_0_inf) by (auto simp add:prod_filter_eq_bot) have exp_pos: "exp k \ real x \ x > 0" for k x using exp_gt_zero gr0I by force have exp_gt_1: "exp 1 \ (1::real)" by simp have 1: "(\_. 1) \ O[?F](\x. ln (1 / real_of_rat (\_of x)))" by (auto intro!:landau_o.big_mono evt[where \="exp 1"] iffD2[OF ln_ge_iff] simp add:abs_ge_iff) have 2: "(\_. 1) \ O[?F](\x. ln (1 / real_of_rat (\_of x)))" by (auto intro!:landau_o.big_mono evt[where \="exp 1"] iffD2[OF ln_ge_iff] simp add:abs_ge_iff) have 3: " (\x. 1) \ O[?F](\x. ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x)))" using exp_pos by (intro landau_sum_2 2 evt[where n="exp 1" and \="1"] ln_ge_zero iffD2[OF ln_ge_iff], auto) have 4: "(\_. 1) \ O[?F](\x. 1 / (real_of_rat (\_of x))\<^sup>2)" using one_le_power by (intro landau_o.big_mono evt[where \="1"], auto simp add:power_one_over[symmetric]) have "(\x. 80 * (1 / (real_of_rat (\_of x))\<^sup>2)) \ O[?F](\x. 1 / (real_of_rat (\_of x))\<^sup>2)" by (subst landau_o.big.cmult_in_iff, auto) hence 5: "(\x. real (t_of x)) \ O[?F](\x. 1 / (real_of_rat (\_of x))\<^sup>2)" unfolding t_of_def by (intro landau_real_nat landau_ceil 4, auto) have "(\x. ln (real_of_rat (\_of x))) \ O[?F](\x. ln (1 / real_of_rat (\_of x)))" by (intro landau_o.big_mono evt[where \="1"], auto simp add:ln_div) hence 6: "(\x. real (s_of x)) \ O[?F](\x. ln (1 / real_of_rat (\_of x)))" unfolding s_of_def by (intro landau_nat_ceil 1, simp) have 7: " (\x. 1) \ O[?F](\x. ln (real (n_of x)))" using exp_pos by (auto intro!: landau_o.big_mono evt[where n="exp 1"] iffD2[OF ln_ge_iff] simp: abs_ge_iff) have 8:" (\_. 1) \ O[?F](\x. ln (real (n_of x)) + 1 / (real_of_rat (\_of x))\<^sup>2 * (ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x))))" using order_trans[OF exp_gt_1] exp_pos by (intro landau_sum_1 7 evt[where n="exp 1" and \="1"] ln_ge_zero iffD2[OF ln_ge_iff] mult_nonneg_nonneg add_nonneg_nonneg) auto have "(\x. ln (real (s_of x) + 1)) \ O[?F](\x. ln (1 / real_of_rat (\_of x)))" by (intro landau_ln_3 sum_in_bigo 6 1, simp) hence 9: "(\x. log 2 (real (s_of x) + 1)) \ O[?F](g)" unfolding g_def by (intro landau_o.big_mult_1 8, auto simp:log_def) have 10: "(\x. 1) \ O[?F](g)" unfolding g_def by (intro landau_o.big_mult_1 8 1) have "(\x. ln (real (t_of x) + 1)) \ O[?F](\x. 1 / (real_of_rat (\_of x))\<^sup>2 * (ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x))))" using 5 by (intro landau_o.big_mult_1 3 landau_ln_3 sum_in_bigo 4, simp_all) hence " (\x. log 2 (real (t_of x) + 1)) \ O[?F](\x. ln (real (n_of x)) + 1 / (real_of_rat (\_of x))\<^sup>2 * (ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x))))" using order_trans[OF exp_gt_1] exp_pos by (intro landau_sum_2 evt[where n="exp 1" and \="1"] ln_ge_zero iffD2[OF ln_ge_iff] mult_nonneg_nonneg add_nonneg_nonneg) (auto simp add:log_def) hence 11: "(\x. log 2 (real (t_of x) + 1)) \ O[?F](g)" unfolding g_def by (intro landau_o.big_mult_1' 1, auto) have " (\x. 1) \ O[?F](\x. real (n_of x))" by (intro landau_o.big_mono evt[where n="1"], auto) hence "(\x. ln (real (n_of x) + 21)) \ O[?F](\x. ln (real (n_of x)))" by (intro landau_ln_2[where a="2"] evt[where n="2"] sum_in_bigo, auto) hence 12: "(\x. log 2 (real (n_of x) + 21)) \ O[?F](g)" unfolding g_def using exp_pos order_trans[OF exp_gt_1] by (intro landau_o.big_mult_1' 1 landau_sum_1 evt[where n="exp 1" and \="1"] ln_ge_zero iffD2[OF ln_ge_iff] mult_nonneg_nonneg add_nonneg_nonneg) (auto simp add:log_def) have "(\x. ln (1 / real_of_rat (\_of x))) \ O[?F](\x. 1 / (real_of_rat (\_of x))\<^sup>2)" by (intro landau_ln_3 evt[where \="1"] landau_o.big_mono) (auto simp add:power_one_over[symmetric] self_le_power) hence " (\x. real (nat (4*\log 2 (1 / real_of_rat (\_of x))\+23))) \ O[?F](\x. 1 / (real_of_rat (\_of x))\<^sup>2)" using 4 by (auto intro!: landau_real_nat sum_in_bigo landau_ceil simp:log_def) hence " (\x. ln (real (r_of x) + 1)) \ O[?F](\x. 1 / (real_of_rat (\_of x))\<^sup>2)" unfolding r_of_def by (intro landau_ln_3 sum_in_bigo 4, auto) hence " (\x. log 2 (real (r_of x) + 1)) \ O[?F](\x. (1 / (real_of_rat (\_of x))\<^sup>2) * (ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x))))" by (intro landau_o.big_mult_1 3, simp add:log_def) hence " (\x. log 2 (real (r_of x) + 1)) \ O[?F](\x. ln (real (n_of x)) + 1 / (real_of_rat (\_of x))\<^sup>2 * (ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x))))" using exp_pos order_trans[OF exp_gt_1] by (intro landau_sum_2 evt[where n="exp 1" and \="1"] ln_ge_zero iffD2[OF ln_ge_iff] add_nonneg_nonneg mult_nonneg_nonneg) (auto) hence 13: "(\x. log 2 (real (r_of x) + 1)) \ O[?F](g)" unfolding g_def by (intro landau_o.big_mult_1' 1, auto) have 14: "(\x. 1) \ O[?F](\x. real (n_of x))" by (intro landau_o.big_mono evt[where n="1"], auto) have "(\x. ln (real (n_of x) + 13)) \ O[?F](\x. ln (real (n_of x)))" using 14 by (intro landau_ln_2[where a="2"] evt[where n="2"] sum_in_bigo, auto) hence "(\x. ln (log 2 (real (n_of x) + 13))) \ O[?F](\x. ln (ln (real (n_of x))))" using exp_pos by (intro landau_ln_2[where a="2"] iffD2[OF ln_ge_iff] evt[where n="exp 2"]) (auto simp add:log_def) hence "(\x. log 2 (log 2 (real (n_of x) + 13))) \ O[?F](\x. ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x)))" using exp_pos by (intro landau_sum_1 evt[where n="exp 1" and \="1"] ln_ge_zero iffD2[OF ln_ge_iff]) (auto simp add:log_def) moreover have "(\x. real (r_of x)) \ O[?F](\x. ln (1 / real_of_rat (\_of x)))" unfolding r_of_def using 2 by (auto intro!: landau_real_nat sum_in_bigo landau_ceil simp:log_def) hence "(\x. real (r_of x)) \ O[?F](\x. ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x)))" using exp_pos by (intro landau_sum_2 evt[where n="exp 1" and \="1"] ln_ge_zero iffD2[OF ln_ge_iff], auto) ultimately have 15:" (\x. real (t_of x) * (13 + 4 * real (r_of x) + 2 * log 2 (log 2 (real (n_of x) + 13)))) \ O[?F](\x. 1 / (real_of_rat (\_of x))\<^sup>2 * (ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x))))" using 5 3 by (intro landau_o.mult sum_in_bigo, auto) have "(\x. 5 + 2 * log 2 (21 + real (n_of x)) + real (t_of x) * (13 + 4 * real (r_of x) + 2 * log 2 (log 2 (real (n_of x) + 13)))) \ O[?F](\x. ln (real (n_of x)) + 1 / (real_of_rat (\_of x))\<^sup>2 * (ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x))))" proof - have "\\<^sub>F x in ?F. 0 \ ln (real (n_of x))" by (intro evt[where n="1"] ln_ge_zero, auto) moreover have "\\<^sub>F x in ?F. 0 \ 1 / (real_of_rat (\_of x))\<^sup>2 * (ln (ln (real (n_of x))) + ln (1 / real_of_rat (\_of x)))" using exp_pos by (intro evt[where n="exp 1" and \="1"] mult_nonneg_nonneg add_nonneg_nonneg ln_ge_zero iffD2[OF ln_ge_iff]) auto moreover have " (\x. ln (21 + real (n_of x))) \ O[?F](\x. ln (real (n_of x)))" using 14 by (intro landau_ln_2[where a="2"] sum_in_bigo evt[where n="2"], auto) hence "(\x. 5 + 2 * log 2 (21 + real (n_of x))) \ O[?F](\x. ln (real (n_of x)))" using 7 by (intro sum_in_bigo, auto simp add:log_def) ultimately show ?thesis using 15 by (rule landau_sum) qed hence 16: "(\x. real (s_of x) * (5 + 2 * log 2 (21 + real (n_of x)) + real (t_of x) * (13 + 4 * real (r_of x) + 2 * log 2 (log 2 (real (n_of x) + 13))))) \ O[?F](g)" unfolding g_def by (intro landau_o.mult 6, auto) have "f0_space_usage = (\x. f0_space_usage (n_of x, \_of x, \_of x))" by (simp add:case_prod_beta' n_of_def \_of_def \_of_def) also have "... \ O[?F](g)" using 9 10 11 12 13 16 by (simp add:fun_cong[OF s_of_def[symmetric]] fun_cong[OF t_of_def[symmetric]] fun_cong[OF r_of_def[symmetric]] Let_def) (intro sum_in_bigo, auto) also have "... = O[?F](?rhs)" by (simp add:case_prod_beta' g_def n_of_def \_of_def \_of_def) finally show ?thesis by simp qed end diff --git a/thys/Frequency_Moments/Frequency_Moments_Preliminary_Results.thy b/thys/Frequency_Moments/Frequency_Moments_Preliminary_Results.thy --- a/thys/Frequency_Moments/Frequency_Moments_Preliminary_Results.thy +++ b/thys/Frequency_Moments/Frequency_Moments_Preliminary_Results.thy @@ -1,464 +1,461 @@ section \Preliminary Results\ theory Frequency_Moments_Preliminary_Results imports "HOL.Transcendental" "HOL-Computational_Algebra.Primes" "HOL-Library.Extended_Real" "HOL-Library.Multiset" "HOL-Library.Sublist" Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators Bertrands_Postulate.Bertrand Expander_Graphs.Expander_Graphs_Multiset_Extras begin text \This section contains various preliminary results.\ lemma card_ordered_pairs: fixes M :: "('a ::linorder) set" assumes "finite M" shows "2 * card {(x,y) \ M \ M. x < y} = card M * (card M - 1)" proof - have a: "finite (M \ M)" using assms by simp have inj_swap: "inj (\x. (snd x, fst x))" by (rule inj_onI, simp add: prod_eq_iff) have "2 * card {(x,y) \ M \ M. x < y} = card {(x,y) \ M \ M. x < y} + card ((\x. (snd x, fst x))`{(x,y) \ M \ M. x < y})" by (simp add: card_image[OF inj_on_subset[OF inj_swap]]) also have "... = card {(x,y) \ M \ M. x < y} + card {(x,y) \ M \ M. y < x}" by (auto intro: arg_cong[where f="card"] simp add:set_eq_iff image_iff) also have "... = card ({(x,y) \ M \ M. x < y} \ {(x,y) \ M \ M. y < x})" by (intro card_Un_disjoint[symmetric] a finite_subset[where B="M \ M"] subsetI) auto also have "... = card ((M \ M) - {(x,y) \ M \ M. x = y})" by (auto intro: arg_cong[where f="card"] simp add:set_eq_iff) also have "... = card (M \ M) - card {(x,y) \ M \ M. x = y}" by (intro card_Diff_subset a finite_subset[where B="M \ M"] subsetI) auto also have "... = card M ^ 2 - card ((\x. (x,x)) ` M)" using assms by (intro arg_cong2[where f="(-)"] arg_cong[where f="card"]) (auto simp:power2_eq_square set_eq_iff image_iff) also have "... = card M ^ 2 - card M" by (intro arg_cong2[where f="(-)"] card_image inj_onI, auto) also have "... = card M * (card M - 1)" by (cases "card M \ 0", auto simp:power2_eq_square algebra_simps) finally show ?thesis by simp qed lemma ereal_mono: "x \ y \ ereal x \ ereal y" by simp -lemma log_mono: "a > 1 \ x \ y \ 0 < x \ log a x \ log a y" - by (subst log_le_cancel_iff, auto) - lemma abs_ge_iff: "((x::real) \ abs y) = (x \ y \ x \ -y)" by linarith lemma count_list_gr_1: "(x \ set xs) = (count_list xs x \ 1)" by (induction xs, simp, simp) lemma count_list_append: "count_list (xs@ys) v = count_list xs v + count_list ys v" by (induction xs, simp, simp) lemma count_list_lt_suffix: assumes "suffix a b" assumes "x \ {b ! i| i. i < length b - length a}" shows "count_list a x < count_list b x" proof - have "length a \ length b" using assms(1) by (simp add: suffix_length_le) hence "x \ set (nths b {i. i < length b - length a})" using assms diff_commute by (auto simp add:set_nths) hence a:"x \ set (take (length b - length a) b)" by (subst (asm) lessThan_def[symmetric], simp) have "b = (take (length b - length a) b)@drop (length b - length a) b" by simp also have "... = (take (length b - length a) b)@a" using assms(1) suffix_take by auto finally have b:"b = (take (length b - length a) b)@a" by simp have "count_list a x < 1 + count_list a x" by simp also have "... \ count_list (take (length b - length a) b) x + count_list a x" using a count_list_gr_1 by (intro add_mono, fast, simp) also have "... = count_list b x" using b count_list_append by metis finally show ?thesis by simp qed lemma suffix_drop_drop: assumes "x \ y" shows "suffix (drop x a) (drop y a)" proof - have "drop y a = take (x - y) (drop y a)@drop (x- y) (drop y a)" by (subst append_take_drop_id, simp) also have " ... = take (x-y) (drop y a)@drop x a" using assms by simp finally have "drop y a = take (x-y) (drop y a)@drop x a" by simp thus ?thesis by (auto simp add:suffix_def) qed lemma count_list_card: "count_list xs x = card {k. k < length xs \ xs ! k = x}" proof - have "count_list xs x = length (filter ((=) x) xs)" by (induction xs, simp, simp) also have "... = card {k. k < length xs \ xs ! k = x}" by (subst length_filter_conv_card, metis) finally show ?thesis by simp qed lemma card_gr_1_iff: assumes "finite S" "x \ S" "y \ S" "x \ y" shows "card S > 1" using assms card_le_Suc0_iff_eq leI by auto lemma count_list_ge_2_iff: assumes "y < z" assumes "z < length xs" assumes "xs ! y = xs ! z" shows "count_list xs (xs ! y) > 1" proof - have " 1 < card {k. k < length xs \ xs ! k = xs ! y}" using assms by (intro card_gr_1_iff[where x="y" and y="z"], auto) thus ?thesis by (simp add: count_list_card) qed text \Results about multisets and sorting\ lemmas disj_induct_mset = disj_induct_mset lemma prod_mset_conv: fixes f :: "'a \ 'b::{comm_monoid_mult}" shows "prod_mset (image_mset f A) = prod (\x. f x^(count A x)) (set_mset A)" proof (induction A rule: disj_induct_mset) case 1 then show ?case by simp next case (2 n M x) moreover have "count M x = 0" using 2 by (simp add: count_eq_zero_iff) moreover have "\y. y \ set_mset M \ y \ x" using 2 by blast ultimately show ?case by (simp add:algebra_simps) qed text \There is a version @{thm [source] sum_list_map_eq_sum_count} but it doesn't work if the function maps into the reals.\ lemma sum_list_eval: fixes f :: "'a \ 'b::{ring,semiring_1}" shows "sum_list (map f xs) = (\x \ set xs. of_nat (count_list xs x) * f x)" proof - define M where "M = mset xs" have "sum_mset (image_mset f M) = (\x \ set_mset M. of_nat (count M x) * f x)" proof (induction "M" rule:disj_induct_mset) case 1 then show ?case by simp next case (2 n M x) have a:"\y. y \ set_mset M \ y \ x" using 2(2) by blast show ?case using 2 by (simp add:a count_eq_zero_iff[symmetric]) qed moreover have "\x. count_list xs x = count (mset xs) x" by (induction xs, simp, simp) ultimately show ?thesis by (simp add:M_def sum_mset_sum_list[symmetric]) qed lemma prod_list_eval: fixes f :: "'a \ 'b::{ring,semiring_1,comm_monoid_mult}" shows "prod_list (map f xs) = (\x \ set xs. (f x)^(count_list xs x))" proof - define M where "M = mset xs" have "prod_mset (image_mset f M) = (\x \ set_mset M. f x ^ (count M x))" proof (induction "M" rule:disj_induct_mset) case 1 then show ?case by simp next case (2 n M x) have a:"\y. y \ set_mset M \ y \ x" using 2(2) by blast have b:"count M x = 0" using 2 by (subst count_eq_zero_iff) blast show ?case using 2 by (simp add:a b mult.commute) qed moreover have "\x. count_list xs x = count (mset xs) x" by (induction xs, simp, simp) ultimately show ?thesis by (simp add:M_def prod_mset_prod_list[symmetric]) qed lemma sorted_sorted_list_of_multiset: "sorted (sorted_list_of_multiset M)" by (induction M, auto simp:sorted_insort) lemma count_mset: "count (mset xs) a = count_list xs a" by (induction xs, auto) lemma swap_filter_image: "filter_mset g (image_mset f A) = image_mset f (filter_mset (g \ f) A)" by (induction A, auto) lemma list_eq_iff: assumes "mset xs = mset ys" assumes "sorted xs" assumes "sorted ys" shows "xs = ys" using assms properties_for_sort by blast lemma sorted_list_of_multiset_image_commute: assumes "mono f" shows "sorted_list_of_multiset (image_mset f M) = map f (sorted_list_of_multiset M)" proof - have "sorted (sorted_list_of_multiset (image_mset f M))" by (simp add:sorted_sorted_list_of_multiset) moreover have " sorted_wrt (\x y. f x \ f y) (sorted_list_of_multiset M)" by (rule sorted_wrt_mono_rel[where P="\x y. x \ y"]) (auto intro: monoD[OF assms] sorted_sorted_list_of_multiset) hence "sorted (map f (sorted_list_of_multiset M))" by (subst sorted_wrt_map) ultimately show ?thesis by (intro list_eq_iff, auto) qed text \Results about rounding and floating point numbers\ lemma round_down_ge: "x \ round_down prec x + 2 powr (-prec)" using round_down_correct by (simp, meson diff_diff_eq diff_eq_diff_less_eq) lemma truncate_down_ge: "x \ truncate_down prec x + abs x * 2 powr (-prec)" proof (cases "abs x > 0") case True have "x \ round_down (int prec - \log 2 \x\\) x + 2 powr (-real_of_int(int prec - \log 2 \x\\))" by (rule round_down_ge) also have "... \ truncate_down prec x + 2 powr ( \log 2 \x\\) * 2 powr (-real prec)" by (rule add_mono, simp_all add:powr_add[symmetric] truncate_down_def) also have "... \ truncate_down prec x + \x\ * 2 powr (-real prec)" using True by (intro add_mono mult_right_mono, simp_all add:le_log_iff[symmetric]) finally show ?thesis by simp next case False then show ?thesis by simp qed lemma truncate_down_pos: assumes "x \ 0" shows "x * (1 - 2 powr (-prec)) \ truncate_down prec x" by (simp add:right_diff_distrib diff_le_eq) (metis truncate_down_ge assms abs_of_nonneg) lemma truncate_down_eq: assumes "truncate_down r x = truncate_down r y" shows "abs (x-y) \ max (abs x) (abs y) * 2 powr (-real r)" proof - have "x - y \ truncate_down r x + abs x * 2 powr (-real r) - y" by (rule diff_right_mono, rule truncate_down_ge) also have "... \ y + abs x * 2 powr (-real r) - y" using truncate_down_le by (intro diff_right_mono add_mono, subst assms(1), simp_all) also have "... \ abs x * 2 powr (-real r)" by simp also have "... \ max (abs x) (abs y) * 2 powr (-real r)" by simp finally have a:"x - y \ max (abs x) (abs y) * 2 powr (-real r)" by simp have "y - x \ truncate_down r y + abs y * 2 powr (-real r) - x" by (rule diff_right_mono, rule truncate_down_ge) also have "... \ x + abs y * 2 powr (-real r) - x" using truncate_down_le by (intro diff_right_mono add_mono, subst assms(1)[symmetric], auto) also have "... \ abs y * 2 powr (-real r)" by simp also have "... \ max (abs x) (abs y) * 2 powr (-real r)" by simp finally have b:"y - x \ max (abs x) (abs y) * 2 powr (-real r)" by simp show ?thesis using abs_le_iff a b by linarith qed definition rat_of_float :: "float \ rat" where "rat_of_float f = of_int (mantissa f) * (if exponent f \ 0 then 2 ^ (nat (exponent f)) else 1 / 2 ^ (nat (-exponent f)))" lemma real_of_rat_of_float: "real_of_rat (rat_of_float x) = real_of_float x" proof - have "real_of_rat (rat_of_float x) = mantissa x * (2 powr (exponent x))" by (simp add:rat_of_float_def of_rat_mult of_rat_divide of_rat_power powr_realpow[symmetric] powr_minus_divide) also have "... = real_of_float x" using mantissa_exponent by simp finally show ?thesis by simp qed lemma log_est: "log 2 (real n + 1) \ n" proof - have "1 + real n = real (n + 1)" by simp also have "... \ real (2 ^ n)" by (intro of_nat_mono suc_n_le_2_pow_n) also have "... = 2 powr (real n)" by (simp add:powr_realpow) finally have "1 + real n \ 2 powr (real n)" by simp thus ?thesis by (simp add: Transcendental.log_le_iff) qed lemma truncate_mantissa_bound: "abs (\x * 2 powr (real r - real_of_int \log 2 \x\\)\) \ 2 ^ (r+1)" (is "?lhs \ _") proof - define q where "q = \x * 2 powr (real r - real_of_int (\log 2 \x\\))\" have "abs q \ 2 ^ (r + 1)" if a:"x > 0" proof - have "abs q = q" using a by (intro abs_of_nonneg, simp add:q_def) also have "... \ x * 2 powr (real r - real_of_int \log 2 \x\\)" unfolding q_def using of_int_floor_le by blast also have "... = x * 2 powr real_of_int (int r - \log 2 \x\\)" by auto also have "... = 2 powr (log 2 x + real_of_int (int r - \log 2 \x\\))" using a by (simp add:powr_add) also have "... \ 2 powr (real r + 1)" using a by (intro powr_mono, linarith+) also have "... = 2 ^ (r+1)" by (subst powr_realpow[symmetric], simp_all add:add.commute) finally show "abs q \ 2 ^ (r+1)" by (metis of_int_le_iff of_int_numeral of_int_power) qed moreover have "abs q \ (2 ^ (r + 1))" if a: "x < 0" proof - have "-(2 ^ (r+1) + 1) = -(2 powr (real r + 1)+1)" by (subst powr_realpow[symmetric], simp_all add: add.commute) also have "... < -(2 powr (log 2 (- x) + (r - \log 2 \x\\)) + 1)" using a by (simp, linarith) also have "... = x * 2 powr (r - \log 2 \x\\) - 1" using a by (simp add:powr_add) also have "... \ q" by (simp add:q_def) also have "... = - abs q" using a by (subst abs_of_neg, simp_all add: mult_pos_neg2 q_def) finally have "-(2 ^ (r+1)+1) < - abs q" using of_int_less_iff by fastforce hence "-(2 ^ (r+1)) \ - abs q" by linarith thus "abs q \ 2^(r+1)" by linarith qed moreover have "x = 0 \ abs q \ 2^(r+1)" by (simp add:q_def) ultimately have "abs q \ 2^(r+1)" by fastforce thus ?thesis using q_def by blast qed lemma truncate_float_bit_count: "bit_count (F\<^sub>e (float_of (truncate_down r x))) \ 10 + 4 * real r + 2*log 2 (2 + \log 2 \x\\)" (is "?lhs \ ?rhs") proof - define m where "m = \x * 2 powr (real r - real_of_int \log 2 \x\\)\" define e where "e = \log 2 \x\\ - int r" have a: "(real_of_int \log 2 \x\\ - real r) = e" by (simp add:e_def) have "abs m + 2 \ 2 ^ (r + 1) + 2^1" using truncate_mantissa_bound by (intro add_mono, simp_all add:m_def) also have "... \ 2 ^ (r+2)" by simp finally have b:"abs m + 2 \ 2 ^ (r+2)" by simp hence "real_of_int (\m\ + 2) \ real_of_int (4 * 2 ^ r)" by (subst of_int_le_iff, simp) hence "\real_of_int m\ + 2 \ 4 * 2 ^ r" by simp hence c:"log 2 (real_of_int (\m\ + 2)) \ r+2" by (simp add: Transcendental.log_le_iff powr_add powr_realpow) have "real_of_int (abs e + 1) \ real_of_int \\log 2 \x\\\ + real_of_int r + 1" by (simp add:e_def) also have "... \ 1 + abs (log 2 (abs x)) + real_of_int r + 1" by (simp add:abs_le_iff, linarith) also have "... \ (real_of_int r+ 1) * (2 + abs (log 2 (abs x)))" by (simp add:distrib_left distrib_right) finally have d:"real_of_int (abs e + 1) \ (real_of_int r+ 1) * (2 + abs (log 2 (abs x)))" by simp have "log 2 (real_of_int (abs e + 1)) \ log 2 (real_of_int r + 1) + log 2 (2 + abs (log 2 (abs x)))" using d by (simp add: log_mult[symmetric]) also have "... \ r + log 2 (2 + abs (log 2 (abs x)))" using log_est by (intro add_mono, simp_all add:add.commute) finally have e: "log 2 (real_of_int (abs e + 1)) \ r + log 2 (2 + abs (log 2 (abs x)))" by simp have "?lhs = bit_count (F\<^sub>e (float_of (real_of_int m * 2 powr real_of_int e)))" by (simp add:truncate_down_def round_down_def m_def[symmetric] a) also have "... \ ereal (6 + (2 * log 2 (real_of_int (\m\ + 2)) + 2 * log 2 (real_of_int (\e\ + 1))))" using float_bit_count_2 by simp also have "... \ ereal (6 + (2 * real (r+2) + 2 * (r + log 2 (2 + abs (log 2 (abs x))))))" using c e by (subst ereal_less_eq, intro add_mono mult_left_mono, linarith+) also have "... = ?rhs" by simp finally show ?thesis by simp qed definition prime_above :: "nat \ nat" where "prime_above n = (SOME x. x \ {n..(2*n+2)} \ prime x)" text \The term @{term"prime_above n"} returns a prime between @{term "n::nat"} and @{term "2*(n::nat)+2"}. Because of Bertrand's postulate there always is such a value. In a refinement of the algorithms, it may make sense to replace this with an algorithm, that finds such a prime exactly or approximately. The definition is intentionally inexact, to allow refinement with various algorithms, without modifying the high-level mathematical correctness proof.\ lemma ex_subset: assumes "\x \ A. P x" assumes "A \ B" shows "\x \ B. P x" using assms by auto lemma shows prime_above_prime: "prime (prime_above n)" and prime_above_range: "prime_above n \ {n..(2*n+2)}" proof - define r where "r = (\x. x \ {n..(2*n+2)} \ prime x)" have "\x. r x" proof (cases "n>2") case True hence "n-1 > 1" by simp hence "\x \ {(n-1)<..<(2*(n-1))}. prime x" using bertrand by simp moreover have "{n - 1<..<2 * (n - 1)} \ {n..2 * n + 2}" by (intro subsetI, auto) ultimately have "\x \ {n..(2*n+2)}. prime x" by (rule ex_subset) then show ?thesis by (simp add:r_def Bex_def) next case False hence "2 \ {n..(2*n+2)}" by simp moreover have "prime (2::nat)" using two_is_prime_nat by blast ultimately have "r 2" using r_def by simp then show ?thesis by (rule exI) qed moreover have "prime_above n = (SOME x. r x)" by (simp add:prime_above_def r_def) ultimately have a:"r (prime_above n)" using someI_ex by metis show "prime (prime_above n)" using a unfolding r_def by blast show "prime_above n \ {n..(2*n+2)}" using a unfolding r_def by blast qed lemma prime_above_min: "prime_above n \ 2" using prime_above_prime by (simp add: prime_ge_2_nat) lemma prime_above_lower_bound: "prime_above n \ n" using prime_above_range by simp lemma prime_above_upper_bound: "prime_above n \ 2*n+2" using prime_above_range by simp end diff --git a/thys/MDP-Algorithms/Splitting_Methods_Fin.thy b/thys/MDP-Algorithms/Splitting_Methods_Fin.thy --- a/thys/MDP-Algorithms/Splitting_Methods_Fin.thy +++ b/thys/MDP-Algorithms/Splitting_Methods_Fin.thy @@ -1,772 +1,777 @@ theory Splitting_Methods_Fin imports "MDP-Rewards.Blinfun_Util" MDP_fin Splitting_Methods begin subsection \Util\ definition upper_triangular_blin :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real) \ bool" where "upper_triangular_blin X \ (\u v i. (\j \ i. apply_bfun v j = apply_bfun u j) \ X v i = X u i)" definition strict_upper_triangular_blin :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real) \ bool" where "strict_upper_triangular_blin X \ (\u v i. (\j > i. apply_bfun v j = apply_bfun u j) \ X v i = X u i)" lemma upper_triangularD: fixes X :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real)" and u v :: "'a \\<^sub>b real" assumes "upper_triangular_blin X" and "\j. i \ j \ v j = u j" shows "X v i = X u i" using assms by (auto simp: upper_triangular_blin_def) lemma upper_triangularI[intro]: fixes X :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real)" assumes "\i u v. (\j. i \ j \ apply_bfun v j = apply_bfun u j) \ X v i = X u i" shows "upper_triangular_blin X" using assms by (fastforce simp: upper_triangular_blin_def) lemma strict_upper_triangularD: fixes X :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real)" and u v :: "'a \\<^sub>b real" assumes "strict_upper_triangular_blin X" and "\j. i < j \ v j = u j" shows "X v i = X u i" using assms by (auto simp: strict_upper_triangular_blin_def) lemma strict_imp_upper_triangular_blin: "strict_upper_triangular_blin X \ upper_triangular_blin X" unfolding strict_upper_triangular_blin_def upper_triangular_blin_def by auto definition lower_triangular_blin :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real) \ bool" where "lower_triangular_blin X \ (\u v i. (\j \ i. apply_bfun v j = apply_bfun u j) \ X v i = X u i)" definition strict_lower_triangular_blin :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real) \ bool" where "strict_lower_triangular_blin X \ (\u v i. (\j < i. apply_bfun v j = apply_bfun u j) \ X v i = X u i)" lemma lower_triangularD: fixes X :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real)" and u v :: "'a \\<^sub>b real" assumes "lower_triangular_blin X" and "\j. i \ j \ v j = u j" shows "X v i = X u i" using assms by (auto simp: lower_triangular_blin_def) lemma lower_triangularI[intro]: fixes X :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real)" assumes "\i u v. (\j. i \ j \ apply_bfun v j = apply_bfun u j) \ X v i = X u i" shows "lower_triangular_blin X" using assms by (fastforce simp: lower_triangular_blin_def) lemma strict_lower_triangularI[intro]: fixes X :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real)" assumes "\i u v. (\j. i > j \ apply_bfun v j = apply_bfun u j) \ X v i = X u i" shows "strict_lower_triangular_blin X" using assms by (fastforce simp: strict_lower_triangular_blin_def) lemma strict_lower_triangularD: fixes X :: "('a::linorder \\<^sub>b real) \\<^sub>L ('a \\<^sub>b real)" and u v :: "'a \\<^sub>b real" assumes "strict_lower_triangular_blin X" and "\j. i > j \ v j = u j" shows "X v i = X u i" using assms by (auto simp: strict_lower_triangular_blin_def) lemma strict_imp_lower_triangular_blin: "strict_lower_triangular_blin X \ lower_triangular_blin X" unfolding strict_lower_triangular_blin_def lower_triangular_blin_def by auto lemma all_imp_Max: assumes "finite X" "X \ {}" "\x \ X. P (f x)" shows "P (MAX x \ X. f x)" proof - have "(MAX x \ X. f x) \ f ` X" using assms by auto thus ?thesis using assms by force qed lemma bounded_mult: assumes "bounded ((f :: 'c \ real) ` X)" "bounded (g ` X)" shows "bounded ((\x. f x * g x) ` X)" using assms mult_mono by (fastforce simp: bounded_iff abs_mult intro!: mult_mono) context MDP_nat_disc begin subsection \Gauss Seidel Splitting\ lemma \

\<^sub>1_det: "\

\<^sub>1 (mk_dec_det d) v s = measure_pmf.expectation (K (s, d s)) v" by (auto simp: mk_dec_det_def \

\<^sub>1.rep_eq K_st_def bind_return_pmf) lift_definition \

\<^sub>U :: "(nat \ nat) \ (nat \\<^sub>b real) \\<^sub>L nat \\<^sub>b real" is "\d (v :: nat \\<^sub>b real). (Bfun (\s. (\

\<^sub>1 (mk_dec_det d) (bfun_if (\s'. s' < s) 0 v) s)))" proof (standard, goal_cases) let ?vl = "\v s. (bfun_if (\s'. s' < s) 0 v)" have norm_bfun_if_le: "norm (?vl v s) \ norm v" for v :: "nat \\<^sub>b real" and s by (auto simp: norm_bfun_def' bfun_if.rep_eq intro!: cSUP_mono bounded_imp_bdd_above) hence is_bfun2: "(\s. \

\<^sub>1 (mk_dec_det d) (?vl v s) s) \ bfun" for v :: "nat \\<^sub>b real" and d by (intro bfun_normI) (fastforce intro: order.trans[OF norm_blinfun] order.trans[OF norm_le_norm_bfun]) case (1 d u v) have *: "\

\<^sub>1 (mk_dec_det d) (?vl (u + v) x) x = \

\<^sub>1 (mk_dec_det d) (?vl u x) x + \

\<^sub>1 (mk_dec_det d) (?vl v x) x " for x by (auto simp: bfun_if_zero_add blinfun.add_right) show ?case by (simp add: * eq_onp_same_args is_bfun2 plus_bfun.abs_eq) case (2 d r v) have "?vl (r *\<^sub>R v) x = r *\<^sub>R ?vl v x" for x by (auto simp: bfun_if.rep_eq) hence *: "r * \

\<^sub>1 (mk_dec_det d) (?vl v x) x = \

\<^sub>1 (mk_dec_det d) (?vl (r *\<^sub>R v) x) x" for x by (auto simp: blinfun.scaleR_right) show ?case using is_bfun2 by (auto simp: *) case (3 d) have [simp]: "(\s. \apply_bfun x s\) \ bfun" for x :: "nat \\<^sub>b real" unfolding bfun_def by (auto intro!: boundedI abs_le_norm_bfun) have *: "\(\

\<^sub>1 (mk_dec_det d)) (?vl v n) n\ \ \

\<^sub>1 (mk_dec_det d) (bfun.Bfun (\s. \apply_bfun v s\)) n" for v n unfolding \

\<^sub>1_det by (subst Bfun_inverse) (auto simp: bfun_if.rep_eq abs_le_norm_bfun intro!: order.trans[OF integral_abs_bound] integral_mono AE_pmfI measure_pmf.integrable_const_bound[of _ "norm v"]) have "norm (bfun.Bfun (\s. ((\

\<^sub>1 (mk_dec_det d)) (bfun_if (\s'. s' < s) 0 x)) s)) \ norm x" for x by (fastforce simp: norm_bfun_def' Bfun_inverse[OF is_bfun2] intro: cSUP_least order.trans[OF *[of _ x]] order.trans[OF le_norm_bfun] order.trans[OF norm_blinfun]) thus ?case by (auto intro: exI[of _ 1]) qed lift_definition \

\<^sub>L :: "(nat \ nat) \ (nat \\<^sub>b real) \\<^sub>L nat \\<^sub>b real" is "\d (v :: nat \\<^sub>b real). Bfun (\s. (\

\<^sub>1 (mk_dec_det d) (bfun_if (\s'. s' \ s) 0 v) s))" proof (standard, goal_cases) let ?vl = "\v s. (bfun_if (\s'. s' \ s) 0 v)" have "norm (?vl v s) \ norm v" for v :: "nat \\<^sub>b real" and s by (auto simp: norm_bfun_def' bfun_if.rep_eq intro!: cSUP_mono bounded_imp_bdd_above) hence is_bfun2: "(\s. \

\<^sub>1 (mk_dec_det d) (?vl v s) s) \ bfun" for v :: "nat \\<^sub>b real" and d by (intro bfun_normI) (fastforce intro: order.trans[OF norm_blinfun] order.trans[OF norm_le_norm_bfun]) case (1 d u v) have *: "\

\<^sub>1 (mk_dec_det d) (?vl (u + v) x) x = \

\<^sub>1 (mk_dec_det d) (?vl u x) x + \

\<^sub>1 (mk_dec_det d) (?vl v x) x " for x by (auto simp: bfun_if_zero_add blinfun.add_right) show ?case by (simp add: * eq_onp_same_args is_bfun2 plus_bfun.abs_eq) case (2 d r v) have "?vl (r *\<^sub>R v) x = r *\<^sub>R ?vl v x" for x by (auto simp: bfun_if.rep_eq) hence *: "r * \

\<^sub>1 (mk_dec_det d) (?vl v x) x = \

\<^sub>1 (mk_dec_det d) (?vl (r *\<^sub>R v) x) x" for x by (auto simp: blinfun.scaleR_right) show ?case using is_bfun2 by (auto simp: *) case (3 d) have [simp]: "(\s. \apply_bfun x s\) \ bfun" for x :: "nat \\<^sub>b real" unfolding bfun_def by (auto intro!: boundedI abs_le_norm_bfun) have *: "\(\

\<^sub>1 (mk_dec_det d)) (?vl v n) n\ \ \

\<^sub>1 (mk_dec_det d) (bfun.Bfun (\s. \apply_bfun v s\)) n" for v n unfolding \

\<^sub>1_det by (subst Bfun_inverse) (auto simp: bfun_if.rep_eq abs_le_norm_bfun intro!: order.trans[OF integral_abs_bound] integral_mono AE_pmfI measure_pmf.integrable_const_bound[of _ "norm v"]) have "norm (bfun.Bfun (\s. ((\

\<^sub>1 (mk_dec_det d)) (bfun_if (\s'. s' \ s) 0 x)) s)) \ norm x" for x by (fastforce simp: norm_bfun_def' Bfun_inverse[OF is_bfun2] intro!: cSUP_least order.trans[OF *[of _ x]] order.trans[OF le_norm_bfun] order.trans[OF norm_blinfun]) thus ?case by (auto intro: exI[of _ 1]) qed lemma is_bfun_\

_raw[simp]: fixes v :: "nat \\<^sub>b real" and d shows "(\s. \

\<^sub>1 (mk_dec_det d) (bfun_if (\s'. s' \ s) 0 v) s) \ bfun" (is ?t1) "(\s. \

\<^sub>1 (mk_dec_det d) (bfun_if (\s'. s' < s) 0 v) s) \ bfun" (is ?t2) proof - have *: "norm ((bfun_if (\s'. s' \ s) 0 v)) \ norm v" "norm ((bfun_if (\s'. s' < s) 0 v)) \ norm v" for v :: "nat \\<^sub>b real" and s by (auto simp: norm_bfun_def' bfun_if.rep_eq intro!: cSUP_mono bounded_imp_bdd_above) thus ?t1 ?t2 by (fastforce intro!: bfun_normI order.trans[OF norm_blinfun] order.trans[OF norm_le_norm_bfun])+ qed lemma \

\<^sub>U_rep_eq': "\

\<^sub>U d v s = \

\<^sub>1 (mk_dec_det d) (bfun_if ((>) s) 0 v) s" by (auto simp: \

\<^sub>U.rep_eq) lemma \

\<^sub>L_rep_eq': "\

\<^sub>L d v s = \

\<^sub>1 (mk_dec_det d) (bfun_if ((\) s) 0 v) s" by (auto simp: \

\<^sub>L.rep_eq) lemma apply_bfun_plus: "apply_bfun f a + apply_bfun g a = apply_bfun (f + g) a" by auto lemma \

\<^sub>1_sum_lower_upper: "\

\<^sub>1 (mk_dec_det d) = \

\<^sub>L d + \

\<^sub>U d" proof - have bfun_if_sum: "bfun_if ((\) s) 0 v + bfun_if (\s'. s' < s) 0 v = v" for s and v :: "nat \\<^sub>b real" by (auto simp: bfun_if.rep_eq) show ?thesis by (fastforce intro: blinfun_eqI simp: blinfun.add_left \

\<^sub>L_rep_eq' \

\<^sub>U_rep_eq' apply_bfun_plus blinfun.add_right[symmetric] bfun_if_sum) qed lemma nonneg_\

\<^sub>U: "nonneg_blinfun (\

\<^sub>U d)" using \

\<^sub>1_nonneg is_bfun_\

_raw by (auto simp: nonneg_blinfun_def \

\<^sub>U.rep_eq bfun_if.rep_eq less_eq_bfun_def) lemma nonneg_\

\<^sub>L: "nonneg_blinfun (\

\<^sub>L d)" using \

\<^sub>1_nonneg is_bfun_\

_raw by (auto simp: nonneg_blinfun_def \

\<^sub>L.rep_eq bfun_if.rep_eq less_eq_bfun_def) lemma norm_\

\<^sub>L_le: "norm (\

\<^sub>L d) \ norm (\

\<^sub>1 (mk_dec_det d))" using nonneg_\

\<^sub>L \

\<^sub>1_mono by (fastforce intro!: matrix_le_norm_mono simp: bfun_if.rep_eq nonneg_blinfun_def blinfun.diff_left \

\<^sub>L.rep_eq less_eq_bfun_def) lemma norm_\

\<^sub>U_le: "norm (\

\<^sub>U d) \ norm (\

\<^sub>1 (mk_dec_det d))" using nonneg_\

\<^sub>U \

\<^sub>1_mono by (fastforce intro!: matrix_le_norm_mono simp: bfun_if.rep_eq nonneg_blinfun_def blinfun.diff_left \

\<^sub>U.rep_eq less_eq_bfun_def) lemma norm_\

\<^sub>L_le_one: "norm (\

\<^sub>L d) \ 1" using norm_\

\<^sub>L_le norm_\

\<^sub>1 by auto lemma norm_\

\<^sub>U_le_one: "norm (\

\<^sub>U d) \ 1" using norm_\

\<^sub>U_le norm_\

\<^sub>1 by auto lemma norm_\

\<^sub>L_less_one: "norm (l *\<^sub>R \

\<^sub>L d) < 1" using order.strict_trans1[OF mult_left_le disc_lt_one] zero_le_disc norm_\

\<^sub>L_le_one by auto lemma norm_\

\<^sub>U_less_one: "norm (l *\<^sub>R \

\<^sub>U d) < 1" using order.strict_trans1[OF mult_left_le disc_lt_one] zero_le_disc norm_\

\<^sub>U_le_one by auto lemma \

\<^sub>L_le_\

\<^sub>1: "0 \ v \ \

\<^sub>L d v \ \

\<^sub>1 (mk_dec_det d) v" using \

\<^sub>1_mono by (auto simp: bfun_if.rep_eq \

\<^sub>L_rep_eq' less_eq_bfun_def intro!:) lemma \

\<^sub>U_le_\

\<^sub>1: "0 \ v \ \

\<^sub>U d v \ \

\<^sub>1 (mk_dec_det d) v" using \

\<^sub>1_mono by (auto simp: bfun_if.rep_eq \

\<^sub>U_rep_eq' less_eq_bfun_def intro!:) lemma \

\<^sub>U_indep: "d s = d' s \ \

\<^sub>U d v s = \

\<^sub>U d' v s" unfolding \

\<^sub>U_rep_eq' \

\<^sub>1_det by simp lemma \

\<^sub>L_indep: "d s = d' s \ \

\<^sub>L d v s = \

\<^sub>L d' v s" unfolding \

\<^sub>L_rep_eq' \

\<^sub>1_det by simp lemma \

\<^sub>U_indep2: assumes "d s = d' s" "(\s'. s' \ s \ apply_bfun v s' = apply_bfun v' s')" shows "\

\<^sub>U d v s = \

\<^sub>U d' v' s" using assms by (auto simp: \

\<^sub>U_rep_eq' \

\<^sub>1_det bfun_if.rep_eq cong: if_cong) lemma \

\<^sub>L_indep2: "d s = d' s \ (\s'. s' < s \ apply_bfun v s' = apply_bfun v' s') \ \

\<^sub>L d v s = \

\<^sub>L d' v' s" by (auto simp: \

\<^sub>L_rep_eq' \

\<^sub>1_det bfun_if.rep_eq cong: if_cong) lemma \

\<^sub>1_indep: "d s = d' s \ \

\<^sub>1 d v s = \

\<^sub>1 d' v s" by (simp add: K_st_def \

\<^sub>1.rep_eq) lemma \

\<^sub>U_upper: "upper_triangular_blin (\

\<^sub>U d)" using \

\<^sub>U_indep2 by fastforce lemma \

\<^sub>L_strict_lower: "strict_lower_triangular_blin (\

\<^sub>L d)" using \

\<^sub>L_indep2 by fastforce definition "Q_GS d = id_blinfun - l *\<^sub>R \

\<^sub>L d" definition "R_GS d = l *\<^sub>R \

\<^sub>U d" lemma nonneg_R_GS: "nonneg_blinfun (R_GS d)" by (simp add: R_GS_def nonneg_\

\<^sub>U nonneg_blinfun_scaleR) lemma splitting_gauss: "is_splitting_blin (id_blinfun - l *\<^sub>R \

\<^sub>1 (mk_dec_det d)) (Q_GS d) (R_GS d)" unfolding is_splitting_blin_def proof safe show "nonneg_blinfun (R_GS d)" using nonneg_R_GS. next show "id_blinfun - l *\<^sub>R \

\<^sub>1 (mk_dec_det d) = Q_GS d - R_GS d" using \

\<^sub>1_sum_lower_upper unfolding Q_GS_def R_GS_def by (auto simp: algebra_simps scaleR_add_right[symmetric] simp del: scaleR_add_right) next have n_le: "norm (l *\<^sub>R \

\<^sub>L d) < 1" using mult_left_le[OF norm_\

\<^sub>L_le_one[of d] zero_le_disc] order.strict_trans1 by (auto intro: disc_lt_one) thus "invertible\<^sub>L (Q_GS d)" by (simp add: Q_GS_def invertible\<^sub>L_inf_sum) have "inv\<^sub>L (Q_GS d) = (\i. (l *\<^sub>R \

\<^sub>L d) ^^ i)" using inv\<^sub>L_inf_sum n_le unfolding Q_GS_def by blast have "nonneg_blinfun (R_GS d ^^ i)" for i using nonneg_R_GS by (auto simp: nonneg_blinfun_def intro: blinfunpow_nonneg) have s: "summable (\k. ((l *\<^sub>R \

\<^sub>L d)^^k))" using summable_inv_Q[of "Q_GS d"] norm_\

\<^sub>L_less_one by (simp add: Q_GS_def algebra_simps blinfun.scaleR_left blincomp_scaleR_right) hence s': "summable (\k. ((l *\<^sub>R \

\<^sub>L d)^^k) v)" for v using tendsto_blinfun_apply by (auto simp: summable_def sums_def blinfun.sum_left[symmetric]) hence s'': "summable (\k. ((l *\<^sub>R \

\<^sub>L d)^^k) v s)" for v s by (fastforce simp: summable_def sums_def sum_apply_bfun[symmetric] intro: bfun_tendsto_apply_bfun) have "0 \ (\k. ((l *\<^sub>R \

\<^sub>L d)^^k) v s)" if "v \ 0" for v s by (rule suminf_nonneg[OF s'']) (metis blinfunpow_nonneg that less_eq_bfun_def nonneg_\

\<^sub>L nonneg_blinfun_nonneg nonneg_blinfun_scaleR zero_bfun.rep_eq zero_le_disc) hence "0 \ (\k. ((l *\<^sub>R \

\<^sub>L d)^^k) v)" if "v \ 0" for v using that unfolding less_eq_bfun_def suminf_apply_bfun[OF s'] by auto hence "nonneg_blinfun (\k. ((l *\<^sub>R \

\<^sub>L d)^^k))" unfolding nonneg_blinfun_def by (simp add: blinfun_apply_suminf s) thus "nonneg_blinfun (inv\<^sub>L (Q_GS d))" by (simp add: \inv\<^sub>L (Q_GS d) = (\i. (l *\<^sub>R \

\<^sub>L d) ^^ i)\) qed abbreviation "r_det\<^sub>b d \ r_dec\<^sub>b (mk_dec_det d)" definition "GS_inv d v = inv\<^sub>L (Q_GS d) (r_dec\<^sub>b (mk_dec_det d) + R_GS d v)" text \@{term Q_GS} can be expressed as an infinite sum of @{const \

\<^sub>L}.\ lemma inv_Q_suminf: "inv\<^sub>L (Q_GS d) = (\k. (l *\<^sub>R (\

\<^sub>L d)) ^^ k)" unfolding Q_GS_def using inv\<^sub>L_inf_sum norm_\

\<^sub>L_less_one by blast text \This recursive definition mimics the computation of the GS iteration.\ lemma GS_inv_rec: "GS_inv d v = r_det\<^sub>b d + l *\<^sub>R (\

\<^sub>U d v + \

\<^sub>L d (GS_inv d v))" proof - have "Q_GS d (GS_inv d v) = r_det\<^sub>b d + R_GS d v" using splitting_gauss[of d] unfolding GS_inv_def is_splitting_blin_def by simp thus ?thesis unfolding R_GS_def Q_GS_def by (auto simp: algebra_simps blinfun.diff_left blinfun.scaleR_left) qed text \As a result, also @{term GS_inv} is independent of lower actions.\ lemma GS_indep_high_states: assumes "\s'. s' \ s \ d s' = d' s'" shows "GS_inv d v s = GS_inv d' v s" using assms proof (induction s arbitrary: d d' v rule: less_induct) case (less x) have "r_det\<^sub>b d x = r_det\<^sub>b d' x" by (simp add: less.prems) moreover have "\

\<^sub>U d v x = \

\<^sub>U d' v x" by (meson \

\<^sub>U_indep le_refl less.prems) moreover have "\

\<^sub>L d (GS_inv d v) x = \

\<^sub>L d' (GS_inv d' v) x" using \

\<^sub>L_indep2 less.IH less.prems by fastforce ultimately show ?case by (subst GS_inv_rec[of d], subst GS_inv_rec[of d']) auto qed lemma is_am_GS_inv_extend: assumes "\s. s < k \ is_arg_max (\d. GS_inv d v s) (\d. d \ D\<^sub>D) d" and "is_arg_max (\a. GS_inv (d (k := a)) v k) (\a. a \ A k) a" and "s \ k" and "d \ D\<^sub>D" shows "is_arg_max (\d. GS_inv d v s) (\d. d \ D\<^sub>D) (d (k := a))" proof - have "is_arg_max (\d. GS_inv d v k) (\d. d \ D\<^sub>D) (d (k := a))" proof (rule is_arg_max_linorderI) fix y assume "y \ D\<^sub>D" let ?d = "d(k := y k)" have "GS_inv y v k \ GS_inv ?d v k" proof - have "\

\<^sub>L y (GS_inv y v) k = (\

\<^sub>L ?d (GS_inv y v)) k" by (auto intro!: \

\<^sub>L_indep2 GS_indep_high_states) also have "\ \ (\

\<^sub>L ?d (bfun_if (\s. s < k) (GS_inv d v) (GS_inv y v))) k" using assms(1) \y \ D\<^sub>D\ by (fastforce intro!: nonneg_blinfun_mono[THEN less_eq_bfunD] simp: bfun_if.rep_eq less_eq_bfun_def nonneg_\

\<^sub>L) also have "\ = (\

\<^sub>L ?d (GS_inv d v)) k" by (metis (no_types, lifting) \

\<^sub>L_strict_lower bfun_if.rep_eq strict_lower_triangularD) also have "\ = \

\<^sub>L ?d (GS_inv ?d v) k" using GS_indep_high_states \

\<^sub>L_strict_lower by (fastforce intro: strict_lower_triangularD[OF \

\<^sub>L_strict_lower]) finally have "\

\<^sub>L y (GS_inv y v) k \ \

\<^sub>L ?d (GS_inv ?d v) k". thus ?thesis by (subst GS_inv_rec[of y], subst GS_inv_rec[of ?d]) (auto simp: \

\<^sub>U_indep[of y _ ?d] intro!: mult_left_mono) qed thus "GS_inv y v k \ GS_inv (d(k := a)) v k" using is_arg_max_linorderD[OF assms(2)] \y \ D\<^sub>D\ is_dec_det_def by fastforce next show "d(k := a) \ D\<^sub>D" using assms by (auto simp: is_dec_det_def is_arg_max_linorder) qed thus ?thesis using assms GS_indep_high_states[of s "d (k := a)" d] by (cases "s < k") fastforce+ qed lemma is_am_GS_inv_extend': assumes "\s. s < k \ is_arg_max (\d. GS_inv d v s) (\d. d \ D\<^sub>D) d" and "is_arg_max (\a. GS_inv (d (k := a)) v k) (\a. a \ A k) (d k)" and "s \ k" and "d \ D\<^sub>D" shows "is_arg_max (\d. GS_inv d v s) (\d. d \ D\<^sub>D) d" using assms is_am_GS_inv_extend[of k _ d "d k"] by auto lemma norm_\

\<^sub>L_pow: "norm ((\k. (l *\<^sub>R \

\<^sub>L d) ^^ k)) \ 1 / (1-l)" by (fastforce simp: norm_\

\<^sub>L_le_one mult_left_le power_mono suminf_geometric intro: order.trans[OF summable_norm] summable_comparison_test'[of "\n :: nat. l ^ n" 0] order.trans[OF suminf_le[of _ "\n. l^n"]] order.trans[OF norm_blinfunpow_le]) lemma summable_disc_\

\<^sub>L: "summable (\i. ((l *\<^sub>R \

\<^sub>L d)^^i))" by (metis add_diff_cancel_left' diff_add_cancel norm_\

\<^sub>L_less_one summable_inv_Q) lemma norm_\

\<^sub>L_pow_elem: "norm ((\k. (l *\<^sub>R \

\<^sub>L d) ^^ k) v) \ norm v / (1-l)" using norm_\

\<^sub>L_le_one by (subst blinfun_apply_suminf[symmetric, OF summable_disc_\

\<^sub>L]) (auto simp: blincomp_scaleR_right blinfun.scaleR_left intro!: power_le_one sum_disc_bound' order.trans[OF norm_blinfunpow_le] order.trans[OF norm_blinfun] mult_left_le_one_le) lemma norm_Q_GS: "norm (inv\<^sub>L (Q_GS d) v) \ norm v / (1-l)" using inv_Q_suminf norm_\

\<^sub>L_pow_elem by auto lemma norm_GS_inv_le: "norm (GS_inv d v) \ (r\<^sub>M + l * norm v) / (1 - l)" proof - have "0 < (1 - l)" using disc_lt_one by auto thus ?thesis unfolding GS_inv_def inv_Q_suminf R_GS_def using norm_r_dec_le norm_\

\<^sub>U_le_one order.strict_implies_order[OF disc_lt_one] by (intro order.trans[OF norm_\

\<^sub>L_pow_elem]) (auto simp: blinfun.scaleR_left intro!: mult_left_le_one_le order.trans[OF norm_blinfun] mult_left_mono divide_right_mono order.trans[OF norm_triangle_ineq] add_mono) qed lemma GS_inv_elem_eq: "GS_inv d v s = (r_det\<^sub>b d + l *\<^sub>R (\

\<^sub>1 (mk_dec_det d) (bfun_if (\s'. s \ s') v (GS_inv d v)))) s" proof - have "bfun_if (\s'. s' < s) 0 v + bfun_if ((\) s) 0 (GS_inv d v) = bfun_if ((\) s) v (GS_inv d v)" by (auto simp: bfun_if.rep_eq) thus ?thesis by (subst GS_inv_rec) (auto simp: \

\<^sub>U_rep_eq' \

\<^sub>L_rep_eq' apply_bfun_plus blinfun.add_right[symmetric]) qed subsection \Maximizing Decision Rule for GS\ lemma ex_GS_inv_arg_max: "\a. is_arg_max (\a. GS_inv (d(s:= a)) v s) (\a. a \ A s) a" proof - have "\a. is_arg_max (\a. (r_det\<^sub>b (d(s := a)) + l *\<^sub>R (\

\<^sub>1 (mk_dec_det (d(s := a))) (bfun_if (\s'. s \ s') v (GS_inv d v)))) s) (\a. a \ A s) a" using Sup_att by (auto simp: \

\<^sub>1_det max_L_ex_def has_arg_max_def) moreover have"(bfun_if (\s'. s \ s') v (GS_inv (d(s := a)) v)) = (bfun_if (\s'. s \ s') v (GS_inv d v))" for a using GS_indep_high_states by (fastforce simp: bfun_if.rep_eq) ultimately show ?thesis by (auto simp: GS_inv_elem_eq) qed text \This shows that there always exists a decision rule that maximized @{const GS_inv} for all states simultaneously.\ abbreviation "some_dec \ (SOME d. d \ D\<^sub>D)" fun d_GS_least :: "(nat \\<^sub>b real) \ nat \ nat" where "d_GS_least v (0::nat) = (LEAST a. is_arg_max (\a. GS_inv (some_dec(0 := a)) v 0) (\a. a \ A 0) a)" | "d_GS_least v (Suc n) = (LEAST a. is_arg_max (\a. GS_inv ((\s. if s < Suc n then d_GS_least v s else SOME a. a \ A s)(Suc n:= a)) v (Suc n)) (\a. a \ A (Suc n)) a)" lemma d_GS_least_is_dec: "d_GS_least v \ D\<^sub>D" unfolding is_dec_det_def proof safe fix s show "d_GS_least v s \ A s" using LeastI_ex[OF ex_GS_inv_arg_max] by (cases s) auto qed lemma d_GS_least_eq: "d_GS_least v n = (LEAST a. is_arg_max (\a. GS_inv ((d_GS_least v)(n := a)) v n) (\a. a \ A n) a)" proof (induction n) case 0 have aux: "apply_bfun (GS_inv ((d_GS_least v)(0 := a)) v) 0 = GS_inv (some_dec(0 := a)) v 0" for a by (auto intro: GS_indep_high_states) show ?case unfolding aux by auto next case (Suc n) have aux: "GS_inv ((\s. if s < Suc n then d_GS_least v s else SOME a. a \ A s)(Suc n := a)) v (Suc n) = (GS_inv ((d_GS_least v)(Suc n := a)) v) (Suc n)" for a using GS_indep_high_states by fastforce show ?case unfolding aux[symmetric] by simp qed lemma d_GS_least_is_arg_max: "is_arg_max (\d. GS_inv d v s) (\d. d \ D\<^sub>D) (d_GS_least v)" proof (induction s rule: nat_less_induct) case (1 n) assume "\md. apply_bfun (GS_inv d v) m) (\d. d \ D\<^sub>D) (d_GS_least v)" show ?case using is_am_GS_inv_extend'[of n _ "(d_GS_least v)"] 1 d_GS_least_is_dec by (fastforce simp: ex_GS_inv_arg_max d_GS_least_eq[of v n] LeastI_ex) qed subsection \Gauss-Seidel is a Valid Regular Splitting\ lemma norm_GS_QR_le_disc: "norm (inv\<^sub>L (Q_GS d) o\<^sub>L R_GS d) \ l" proof - have "norm (inv\<^sub>L (Q_GS d) o\<^sub>L R_GS d) \ norm (inv\<^sub>L ((\_. id_blinfun) d) o\<^sub>L (l *\<^sub>R \

\<^sub>1 (mk_dec_det d))) " proof (rule norm_splitting_le[of "mk_dec_det d"], goal_cases) case 1 then show ?case unfolding is_splitting_blin_def nonneg_blinfun_def by (auto simp: \

\<^sub>1_pos blinfun.scaleR_left scaleR_nonneg_nonneg) next case 3 then show ?case by (simp add: R_GS_def \

\<^sub>U_le_\

\<^sub>1 blinfun_le_iff scaleR_blinfun.rep_eq scaleR_left_mono) qed (auto simp: splitting_gauss blinfun_le_iff) also have "\ \ l" by auto finally show ?thesis. qed lemma ex_GS_arg_max_all: "\d. is_arg_max (\d. GS_inv d v s) (\d. d \ D\<^sub>D) d" using d_GS_least_is_arg_max by blast sublocale GS: MDP_QR A K r l Q_GS R_GS proof - have "(\d\D\<^sub>D. norm (inv\<^sub>L (Q_GS d) o\<^sub>L R_GS d)) < 1" using norm_GS_QR_le_disc ex_dec_det by (fastforce intro: le_less_trans[of _ l 1] intro!: cSUP_least) thus "MDP_QR A K r l Q_GS R_GS" using norm_GS_QR_le_disc norm_\

\<^sub>L_pow d_GS_least_is_arg_max by unfold_locales (fastforce intro!: bdd_above.I2 simp: splitting_gauss bounded_iff inv_Q_suminf GS_inv_def)+ qed subsection \Termination\ lemma dist_\\<^sub>b_split_lt_dist_opt: "dist v (GS.\\<^sub>b_split v) \ 2 * dist v \\<^sub>b_opt" proof - have le1: "dist v (GS.\\<^sub>b_split v) \ dist v \\<^sub>b_opt + dist (GS.\\<^sub>b_split v) \\<^sub>b_opt" by (simp add: dist_triangle dist_commute) have le2: "dist (GS.\\<^sub>b_split v) \\<^sub>b_opt \ GS.QR_disc * dist v \\<^sub>b_opt" using GS.\\<^sub>b_split_contraction GS.\\<^sub>b_split_fix by (metis (no_types, lifting)) show ?thesis using mult_right_mono[of GS.QR_disc 1] GS.QR_contraction by (fastforce intro!: order.trans[OF le2] order.trans[OF le1]) qed lemma GS_QR_disc_le_disc: "GS.QR_disc \ l" using norm_GS_QR_le_disc ex_dec_det by (fastforce intro!: cSUP_least) text \ The distance between an estimate for the value and the optimal value can be bounded with respect to the distance between the estimate and the result of applying it to @{const \\<^sub>b} \ lemma gs_rel_dec: assumes "l \ 0" "GS.\\<^sub>b_split v \ \\<^sub>b_opt" shows "\log (1 / l) (dist (GS.\\<^sub>b_split v) \\<^sub>b_opt) - c\ < \log (1 / l) (dist v \\<^sub>b_opt) - c\" proof - have "log (1 / l) (dist (GS.\\<^sub>b_split v) \\<^sub>b_opt) - c \ log (1 / l) (l * dist v \\<^sub>b_opt) - c" - using GS.\\<^sub>b_split_contraction[of _ "\\<^sub>b_opt"] GS.QR_contraction norm_GS_QR_le_disc disc_lt_one GS_QR_disc_le_disc - by (fastforce simp: assms less_le intro!: log_le order.trans[OF GS.\\<^sub>b_split_contraction[of v "\\<^sub>b_opt", simplified]] mult_right_mono) + proof (intro Transcendental.log_mono diff_mono) + show "dist (GS.\\<^sub>b_split v) \\<^sub>b_opt \ l * dist v \\<^sub>b_opt" + using GS.\\<^sub>b_split_contraction[of _ "\\<^sub>b_opt"] + by (smt (verit, ccfv_SIG) GS.\\<^sub>b_split_fix GS_QR_disc_le_disc mult_right_mono zero_le_dist) + show "1 < 1/l" + by (metis \l \ 0\ disc_lt_one less_divide_eq_1_pos less_le zero_le_disc) + qed (use assms in auto) also have "\ = log (1 / l) l + log (1/l) (dist v \\<^sub>b_opt) - c" using assms disc_lt_one by (auto simp: less_le intro!: log_mult) also have "\ = -(log (1 / l) (1/l)) + (log (1/l) (dist v \\<^sub>b_opt)) - c" using assms disc_lt_one by (subst log_inverse[symmetric]) (auto simp: less_le right_inverse_eq) also have "\ = (log (1/l) (dist v \\<^sub>b_opt)) - 1 - c" using assms order.strict_implies_not_eq[OF disc_lt_one] by (auto intro!: log_eq_one neq_le_trans) finally have "log (1 / l) (dist (GS.\\<^sub>b_split v) \\<^sub>b_opt) - c \ log (1 / l) (dist v \\<^sub>b_opt) - 1 - c" . thus ?thesis by linarith qed abbreviation "gs_measure \ (\(eps, v). if v = \\<^sub>b_opt \ l = 0 then 0 else nat (ceiling (log (1/l) (dist v \\<^sub>b_opt) - log (1/l) (eps * (1-l) / (8 * l)))))" function gs_iteration :: "real \ (nat \\<^sub>b real) \ (nat \\<^sub>b real)" where "gs_iteration eps v = (if 2 * l * dist v (GS.\\<^sub>b_split v) < eps * (1 - l) \ eps \ 0 then GS.\\<^sub>b_split v else gs_iteration eps (GS.\\<^sub>b_split v))" by auto termination proof (relation "Wellfounded.measure gs_measure"; cases "l = 0") case False fix eps v assume h: "\ (2 * l * dist v (GS.\\<^sub>b_split v) < eps * (1 - l) \ eps \ 0)" show "((eps, GS.\\<^sub>b_split v), eps, v) \ Wellfounded.measure gs_measure" proof - have gt_zero[simp]: "l \ 0" "eps > 0" and dist_ge: "eps * (1 - l) \ dist v (GS.\\<^sub>b_split v) * (2 * l)" using h by (auto simp: algebra_simps) have v_not_opt: "v \ \\<^sub>b_opt" using h by auto have "log (1 / l) (eps * (1 - l) / (8 * l)) < log (1 / l) (dist v \\<^sub>b_opt)" proof (intro log_less) show "1 < 1 / l" by (auto intro!: mult_imp_less_div_pos intro: neq_le_trans) show "0 < eps * (1 - l) / (8 * l)" by (auto intro!: mult_imp_less_div_pos intro: neq_le_trans) show "eps * (1 - l) / (8 * l) < dist v \\<^sub>b_opt" using dist_pos_lt[OF v_not_opt] dist_\\<^sub>b_split_lt_dist_opt[of v] gt_zero zero_le_disc mult_strict_left_mono[of "dist v (GS.\\<^sub>b_split v)" "(4 * dist v \\<^sub>b_opt)" l] by (intro mult_imp_div_pos_less le_less_trans[OF dist_ge]) argo+ qed thus ?thesis using gs_rel_dec h by auto qed qed auto subsection \Optimality\ lemma THE_fix_GS: "(THE v. GS.\\<^sub>b_split v = v) = \\<^sub>b_opt" using GS.\\<^sub>b_lim(1) GS.\\<^sub>b_split_fix by blast lemma contraction_\_split_dist: "(1 - l) * dist v \\<^sub>b_opt \ dist v (GS.\\<^sub>b_split v)" using GS_QR_disc_le_disc by (fastforce simp: THE_fix_GS intro: order.trans[OF _ contraction_dist, of _ l] order.trans[OF GS.\\<^sub>b_split_contraction] mult_right_mono)+ lemma dist_\\<^sub>b_split_opt_eps: assumes "eps > 0" "2 * l * dist v (GS.\\<^sub>b_split v) < eps * (1-l)" shows "dist (GS.\\<^sub>b_split v) \\<^sub>b_opt < eps / 2" proof - have "dist v \\<^sub>b_opt \ dist v (GS.\\<^sub>b_split v) / (1 - l)" using contraction_\_split_dist by (simp add: mult.commute pos_le_divide_eq) hence "2 * l * dist v \\<^sub>b_opt \ 2 * l * (dist v (GS.\\<^sub>b_split v) / (1 - l))" using contraction_\_dist assms mult_le_cancel_left_pos[of "2 * l"] by (fastforce intro!: mult_left_mono[of _ _ "2 * l"]) hence "2 * l * dist v \\<^sub>b_opt < eps" by (auto simp: assms(2) pos_divide_less_eq intro: order.strict_trans1) hence "dist v \\<^sub>b_opt * l < eps / 2" by argo hence *: "l * dist v \\<^sub>b_opt < eps / 2" by (auto simp: algebra_simps) show "dist (GS.\\<^sub>b_split v) \\<^sub>b_opt < eps / 2" using GS.\\<^sub>b_split_contraction[of v \\<^sub>b_opt] order.trans mult_right_mono[OF GS_QR_disc_le_disc zero_le_dist] by (fastforce intro!: le_less_trans[OF _ *]) qed lemma gs_iteration_error: assumes "eps > 0" shows "dist (gs_iteration eps v) \\<^sub>b_opt < eps / 2" using assms dist_\\<^sub>b_split_opt_eps gs_iteration.simps by (induction eps v rule: gs_iteration.induct) auto lemma find_policy_error_bound_gs: assumes "eps > 0" "2 * l * dist v (GS.\\<^sub>b_split v) < eps * (1-l)" shows "dist (\\<^sub>b (mk_stationary_det (d_GS_least (GS.\\<^sub>b_split v)))) \\<^sub>b_opt < eps" proof (rule GS.find_policy_QR_error_bound[OF assms(1)]) have "2 * GS.QR_disc * dist v (GS.\\<^sub>b_split v) \ 2 * l * dist v (GS.\\<^sub>b_split v)" using GS_QR_disc_le_disc by (auto intro!: mult_right_mono) also have "\ < eps * (1-l)" using assms by auto also have "\ \ eps * (1 - GS.QR_disc)" using assms GS_QR_disc_le_disc by (auto intro!: mult_left_mono) finally show "2 * GS.QR_disc * dist v (GS.\\<^sub>b_split v) < eps * (1 - GS.QR_disc)". next obtain d where d: "is_dec_det d" using ex_dec_det by blast show "is_arg_max (\d. (GS.L_split d (GS.\\<^sub>b_split v)) s) (\d. d \ D\<^sub>D) (d_GS_least (GS.\\<^sub>b_split v))" for s unfolding GS_inv_def[symmetric] using d_GS_least_is_arg_max by auto qed definition "vi_gs_policy eps v = d_GS_least (gs_iteration eps v)" lemmas gs_iteration.simps[simp del] lemma vi_gs_policy_opt: assumes "0 < eps" shows "dist (\\<^sub>b (mk_stationary_det (vi_gs_policy eps v))) \\<^sub>b_opt < eps" unfolding vi_gs_policy_def using assms proof (induction eps v rule: gs_iteration.induct) case (1 v) then show ?case using find_policy_error_bound_gs by (subst gs_iteration.simps) auto qed section \Preparation for Codegen\ lemma \\<^sub>b_split_eq_GS_inv: "GS.\\<^sub>b_split v = GS_inv (d_GS_least v) v" using arg_max_SUP[OF d_GS_least_is_arg_max] by (auto simp: GS.\\<^sub>b_split.rep_eq GS.\_split_def GS_inv_def[symmetric]) lemma \\<^sub>b_split_GS: "GS.\\<^sub>b_split v s = (\a \ A s. r (s, a) + l * measure_pmf.expectation (K (s, a)) (bfun_if (\s'. s' < s) (GS.\\<^sub>b_split v) v))" proof - let ?d = "d_GS_least v" have "GS.\\<^sub>b_split v s = GS_inv ?d v s" using \\<^sub>b_split_eq_GS_inv by auto also have "\ = (\a \ A s. GS_inv (?d(s := a)) v s)" proof (subst arg_max_SUP[symmetric, of _ _ "?d s"]) show "is_arg_max (\a. (GS_inv (?d(s := a)) v) s) (\x. x \ A s) (?d s)" using d_GS_least_eq A_ne A_fin MDP_reward_Util.arg_max_on_in by (auto simp: LeastI_ex finite_is_arg_max) qed fastforce also have "\ = (\a \ A s. (r_det\<^sub>b (?d(s := a)) + l *\<^sub>R (\

\<^sub>U (?d(s := a)) v + \

\<^sub>L (?d(s := a)) (GS_inv (?d(s := a)) v))) s)" using GS_inv_rec by auto also have "\ = (\a \ A s. r (s, a) + l * (\

\<^sub>U (?d(s := a)) v + \

\<^sub>L (?d(s := a)) (GS_inv (?d(s := a)) v)) s)" by auto also have "\ = (\a \ A s. r (s, a) + l * (\

\<^sub>U (?d(s := a)) v + \

\<^sub>L (?d(s := a)) (GS_inv ?d v)) s)" proof - have "\

\<^sub>L (?d(s := a)) (GS_inv (?d(s := a)) v) s = \

\<^sub>L (?d(s := a)) (GS_inv (?d) v) s" for a by (fastforce intro!: GS_indep_high_states strict_lower_triangularD[OF \

\<^sub>L_strict_lower, of s _ _ "(?d(s := a))"]) thus ?thesis by auto qed also have "\ = (\a \ A s. r (s, a) + l * \

\<^sub>1 (mk_dec_det (?d(s := a))) (bfun_if (\s'. s' < s) (GS_inv ?d v) v) s)" proof - have "(bfun_if (\s'. s' < s) 0 v + bfun_if ((\) s) 0 (GS_inv ?d v)) = (bfun_if (\s'. s' < s) (GS_inv ?d v) v)" by (auto simp: bfun_if.rep_eq) thus ?thesis by (auto simp: \

\<^sub>L.rep_eq \

\<^sub>U.rep_eq blinfun.add_right[symmetric] apply_bfun_plus) qed also have "\ = (\a \ A s. r (s, a) + l * \

\<^sub>1 (mk_dec_det (?d(s := a))) (bfun_if (\s'. s' < s) (GS.\\<^sub>b_split v) v) s)" using \\<^sub>b_split_eq_GS_inv by presburger also have "\ = (\a \ A s. r (s, a) + l * measure_pmf.expectation (K (s, a)) (bfun_if (\s'. s' < s) (GS.\\<^sub>b_split v) v))" using \

\<^sub>1_det by auto finally show ?thesis. qed lemma \\<^sub>b_split_GS_iter: assumes "\s'. s' < s \ v' s' = GS.\\<^sub>b_split v s'" "\s'. s' \ s \ v' s' = v s'" shows "GS.\\<^sub>b_split v s = (\a \ A s. L\<^sub>a a v' s)" unfolding \\<^sub>b_split_GS using assms[symmetric] by (auto simp: bfun_if.rep_eq cong: if_cong) function GS_rec_upto where "GS_rec_upto n v s = ( if n \ s then v else GS_rec_upto n (v(s := (\a \ A s. r (s, a) + l * measure_pmf.expectation (K (s, a)) v))) (Suc s))" by auto termination by (relation "Wellfounded.measure (\(n,v,s). n - s)") auto lemmas GS_rec_upto.simps[simp del] lemma GS_rec_upto_ge: assumes "s' \ n" shows "GS_rec_upto n v s s' = v s'" using assms by (induction s arbitrary: s' rule: GS_rec_upto.induct) (fastforce simp add: GS_rec_upto.simps) lemma GS_rec_upto_less: assumes "s > s'" shows "GS_rec_upto n v s s' = v s'" using assms by (induction s arbitrary: s' rule: GS_rec_upto.induct) (auto simp: GS_rec_upto.simps) lemma GS_rec_upto_eq: assumes "s < n" shows "GS_rec_upto n v s s = (\a \ A s. L\<^sub>a a v s)" using assms proof (induction n v s rule: GS_rec_upto.induct) case (1 n v s) then show ?case using GS_rec_upto_less by (cases "Suc s < n") (auto simp add: GS_rec_upto.simps) qed lemma GS_rec_upto_Suc: assumes "s' < n" shows "GS_rec_upto (Suc n) v s s' = GS_rec_upto n v s s'" using assms proof (induction n v s arbitrary: s' rule: GS_rec_upto.induct) case (1 n v s) then show ?case using GS_rec_upto_less by (fastforce simp: GS_rec_upto.simps) qed lemma GS_rec_upto_Suc': assumes "s \ n" shows "GS_rec_upto (Suc n) v s n = (\a \ A n. L\<^sub>a a (GS_rec_upto n v s) n)" using assms proof (induction n v s rule: GS_rec_upto.induct) case (1 n v s) then show ?case by (fastforce simp: not_less_eq_eq GS_rec_upto.simps) qed lemma GS_rec_upto_correct: assumes "s < n" shows "GS.\\<^sub>b_split v s = GS_rec_upto n v 0 s" using assms proof (induction n arbitrary: s) case 0 then show ?case by auto next case (Suc n) then show ?case proof (cases "s < n") case True thus ?thesis using Suc.IH by (auto simp: GS_rec_upto_Suc) next case False hence "s = n" using Suc by auto thus ?thesis using Suc.IH GS_rec_upto_ge by (auto simp: GS_rec_upto_Suc' intro: \\<^sub>b_split_GS_iter) qed qed end end diff --git a/thys/Markov_Models/ex/Crowds_Protocol.thy b/thys/Markov_Models/ex/Crowds_Protocol.thy --- a/thys/Markov_Models/ex/Crowds_Protocol.thy +++ b/thys/Markov_Models/ex/Crowds_Protocol.thy @@ -1,988 +1,988 @@ (* Author: Johannes Hölzl *) section \Formalization of the Crowds-Protocol\ theory Crowds_Protocol imports "../Discrete_Time_Markov_Chain" begin lemma cond_prob_nonneg[simp]: "0 \ cond_prob M A B" by (auto simp: cond_prob_def) lemma (in MC_syntax) emeasure_suntil_geometric: assumes [measurable]: "Measurable.pred S P" assumes "s \ X" and *[simp]: "0 \ p" "0 \ r" assumes r: "\s. s \ X \ emeasure (T s) {\\space (T s). P \} = ennreal r" assumes p: "\s. s \ X \ emeasure (K s) X = ennreal p" "p < 1" assumes "\t. AE \ in T t. \ (P \ (HLD X \ nxt (HLD X suntil P))) \" shows "emeasure (T s) {\\space (T s). (HLD X suntil P) \} = r / (1 - p)" proof (subst emeasure_suntil_disj) let ?F = "\F s. emeasure (T s) {\ \ space (T s). P \} + \\<^sup>+ t. F t * indicator X t \K s" let ?f = "\x. ennreal r + ennreal p * x" have "mono ?F" "mono ?f" by (auto intro!: monoI max.mono add_mono nn_integral_mono mult_left_mono mult_right_mono simp: le_fun_def) have 1: "lfp ?f \ lfp ?F s" using \s \ X\ proof (induction arbitrary: s rule: lfp_ordinal_induct[OF \mono ?f\]) case step: (1 x) then have "?f x \ ?F (\_. x) s" by (auto simp: p r[simplified] nn_integral_cmult mult.commute[of _ x] intro!: add_mono mult_right_mono) also have "?F (\_. x) \ ?F (lfp ?F)" using step by (intro le_funI add_mono order_refl nn_integral_mono) (auto simp: split: split_indicator) finally show ?case by (subst lfp_unfold[OF \mono ?F\]) (auto simp: le_fun_def) qed (auto intro!: Sup_least) also have 2: "lfp ?F s \ r / (1 - p)" using \s \ X\ proof (induction arbitrary: s rule: lfp_ordinal_induct[OF \mono ?F\]) case (1 S) with r have "?F S s \ ennreal r + (\\<^sup>+x. ennreal (r / (1 - p)) * indicator X x \K s)" by (intro add_mono nn_integral_mono) (auto split: split_indicator) also have "\ \ ennreal r + ennreal (r * p / (1 - p))" using \s \ X\ by (simp add: nn_integral_cmult_indicator p ennreal_mult''[symmetric]) also have "\ = ennreal (r / (1 - p))" using \p < 1\ by (simp add: field_simps ennreal_plus[symmetric] del: ennreal_plus) finally show ?case . qed (auto intro!: SUP_least) finally obtain x where x: "lfp ?f = ennreal x" and [simp]: "0 \ x" by (cases "lfp ?f") (auto simp: top_unique) from \p < 1\ have "\x. x = r + p * x \ x = r / (1 - p)" by (auto simp: field_simps) with lfp_unfold[OF \mono ?f\] \p < 1\ have "lfp ?f = r / (1 - p)" unfolding x by (auto simp add: ennreal_plus[symmetric] ennreal_mult[symmetric] simp del: ennreal_plus) with 1 2 show "lfp ?F s = ennreal (r / (1 - p))" by auto qed fact+ subsection \Definition of the Crowds-Protocol\ datatype 'a state = Start | Init 'a | Mix 'a | End lemma inj_Mix[simp]: "inj_on Mix A" by (auto intro: inj_onI) lemma inj_Init[simp]: "inj_on Init A" by (auto intro: inj_onI) lemma distinct_state_image[simp]: "Start \ Mix ` A" "Init j \ Mix ` A" "End \ Mix ` A" "Mix j \ Mix ` A \ j \ A" "Start \ Init ` A" "Mix j \ Init ` A" "End \ Init ` A" "Init j \ Init ` A \ j \ A" by auto lemma Init_cut_Mix[simp]: "Init ` H \ Mix ` J = {}" by auto abbreviation "Jondo B \ Init`B \ Mix`B" locale Crowds_Protocol = fixes J :: "'a set" and C :: "'a set" and p_f :: real and p_i :: "'a \ real" assumes J_not_empty: "J \ {}" and finite_J[simp]: "finite J" assumes C_smaller: "C \ J" and C_non_empty: "C \ {}" assumes p_f: "0 < p_f" "p_f < 1" assumes p_i_nonneg[simp]: "\j. j \ J \ 0 \ p_i j" assumes p_i_distr: "(\j\J. p_i j) = 1" assumes p_i_C: "\j. j \ C \ p_i j = 0" begin abbreviation H :: "'a set" where "H \ J - C" definition "p_j = 1 / card J" lemma p_f_nonneg[simp]: "0 \ p_f" "p_f \ 1" using p_f by simp_all lemma p_j_nonneg[simp]: "0 \ p_j" by (simp add: p_j_def) definition "p_H = card H / card J" lemma p_H_nonneg[simp]: "0 \ p_H" "p_H \ 1" by (auto simp: p_H_def divide_le_eq_1 card_gt_0_iff intro!: card_mono ) definition next_prob :: "'a state \ 'a state \ real" where "next_prob s t = (case (s, t) of (Start, Init j) \ if j \ H then p_i j else 0 | (Init j, Mix j') \ if j' \ J then p_j else 0 | (Mix j, Mix j') \ if j' \ J then p_f * p_j else 0 | (Mix j, End) \ 1 - p_f | (End, End) \ 1 | _ \ 0)" definition "N s = embed_pmf (next_prob s)" interpretation MC_syntax N . abbreviation "\ \ T Start" abbreviation "E s \ set_pmf (N s)" lemma finite_C[simp]: "finite C" using C_smaller finite_J by (blast intro: finite_subset) lemma sum_p_i_C[simp]: "sum p_i C = 0" by (auto intro: sum.neutral p_i_C) lemma sum_p_i_H[simp]: "sum p_i H = 1" using C_smaller by (simp add: sum_diff p_i_distr) lemma possible_jondo: obtains j where "j \ J" "j \ C" "p_i j \ 0" proof (atomize_elim, rule ccontr) assume "\ (\j. j \ J \ j \ C \ p_i j \ 0)" with p_i_C have "\j\J. p_i j = 0" by auto with p_i_distr show False by simp qed lemma C_le_J[simp]: "card C < card J" using C_smaller by (intro psubset_card_mono) auto lemma p_H: "0 < p_H" "p_H < 1" using J_not_empty C_smaller C_non_empty by (simp_all add: p_H_def card_Diff_subset card_mono field_simps zero_less_divide_iff card_gt_0_iff) lemma p_H_p_f_pos: "0 < p_H * p_f" using p_f p_H by (simp add: zero_less_mult_iff) lemma p_H_p_f_less_1: "p_H * p_f < 1" proof - have "p_H * p_f < 1 * 1" using p_H p_f by (intro mult_strict_mono) auto then show "p_H * p_f < 1" by simp qed lemma p_j_pos: "0 < p_j" unfolding p_j_def using J_not_empty by auto lemma H_compl: "1 - p_H = real (card C) / real (card J)" using C_non_empty J_not_empty C_smaller by (simp add: p_H_def card_Diff_subset card_mono of_nat_diff divide_eq_eq field_simps) lemma H_compl2: "1 - p_H = card C * p_j" unfolding H_compl p_j_def by simp lemma H_eq2: "card H * p_j = p_H" unfolding p_j_def p_H_def by simp lemma pmf_next_pmf[simp]: "pmf (N s) t = next_prob s t" unfolding N_def proof (rule pmf_embed_pmf) show "\x. 0 \ next_prob s x" using p_j_pos p_f by (auto simp: next_prob_def intro: p_i_nonneg split: state.split) show "(\\<^sup>+ x. ennreal (next_prob s x) \count_space UNIV) = 1" using p_f J_not_empty by (subst nn_integral_count_space'[where A="Init`H \ Mix`J \ {End}"]) (auto simp: next_prob_def sum.reindex sum.union_disjoint p_i_distr p_j_def split: state.split) qed lemma next_prob_Start[simp]: "next_prob Start (Init j) = (if j \ H then p_i j else 0)" by (auto simp: next_prob_def) lemma next_prob_to_Init[simp]: "j \ H \ next_prob s (Init j) = (case s of Start \ p_i j | _ \ 0)" by (cases s) (auto simp: next_prob_def) lemma next_prob_to_Mix[simp]: "j \ J \ next_prob s (Mix j) = (case s of Init j \ p_j | Mix j \ p_f * p_j | _ \ 0)" by (cases s) (auto simp: next_prob_def) lemma next_prob_to_End[simp]: "next_prob s End = (case s of Mix j \ 1 - p_f | End \ 1 | _ \ 0)" by (cases s) (auto simp: next_prob_def) lemma next_prob_from_End[simp]: "next_prob End s = 0 \ s \ End" by (cases s) (auto simp: next_prob_def) lemma next_prob_Mix_MixI: "\j. s = Mix j \ \j\J. s' = Mix j \ next_prob s s' = p_f * p_j" by (cases s) auto lemma E_Start: "E Start = {Init j | j. j \ H \ p_i j \ 0 }" using p_i_C by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm) lemma E_Init: "E (Init j) = {Mix j | j. j \ J }" using p_j_pos C_smaller by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm) lemma E_Mix: "E (Mix j) = {Mix j | j. j \ J } \ {End}" using p_j_pos p_f by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm) lemma E_End: "E End = {End}" by (auto simp: set_pmf_iff next_prob_def split: state.splits if_split_asm) lemma enabled_End: "enabled End \ \ \ = sconst End" proof safe assume "enabled End \" then show "\ = sconst End" proof (coinduction arbitrary: \) case Eq_stream then show ?case by (auto simp: enabled.simps[of _ \] E_End) qed next show "enabled End (sconst End)" by coinduction (simp add: E_End) qed lemma AE_End: "(AE \ in T End. P \) \ P (sconst End)" proof - have "(AE \ in T End. P \) \ (AE \ in T End. P \ \ \ = sconst End)" using AE_T_enabled[of End] by (simp add: enabled_End) also have "\ = (AE \ in T End. P (sconst End) \ \ = sconst End)" by (simp add: enabled_End del: AE_conj_iff cong: rev_conj_cong) also have "\ = (AE \ in T End. P (sconst End))" using AE_T_enabled[of End] by (simp add: enabled_End) finally show ?thesis by simp qed lemma emeasure_Init_eq_Mix: assumes [measurable]: "Measurable.pred S P" assumes AE_End: "AE x in T End. \ P (End ## x)" shows "emeasure (T (Init j)) {x\space (T (Init j)). P x} = emeasure (T (Mix j)) {x\space (T (Mix j)). P x} / p_f" proof - have *: "{Mix j | j. j \ J } = Mix ` J" by auto show ?thesis using emeasure_eq_0_AE[OF AE_End] p_f apply (subst (1 2) emeasure_Collect_T) apply simp apply (subst (1 2) nn_integral_measure_pmf_finite) apply (auto simp: E_Mix E_Init * sum.reindex sum_distrib_right[symmetric] divide_ennreal ennreal_times_divide[symmetric]) done qed text \ What is the probability that the server sees a specific jondo (including the initiator) as sender. \ definition visit :: "'a set \ 'a set \ 'a state stream \ bool" where "visit I L = Init`(I \ H) \ (HLD (Mix`J) suntil (Mix`(L \ J) \ HLD {End}))" lemma visit_unique1: "visit I1 L1 \ \ visit I2 L2 \ \ I1 \ I2 \ {}" by (auto simp: visit_def HLD_iff) lemma visit_unique2: assumes "visit I1 L1 \" "visit I2 L2 \" shows "L1 \ L2 \ {}" proof - let ?U = "\L \. (HLD (Mix`J) suntil ((Mix`(L\J)) \ HLD {End})) \" have "?U L1 (stl \)" "?U L2 (stl \)" using assms by (auto simp: visit_def) then show "L1 \ L2 \ {}" proof (induction "stl \" arbitrary: \ rule: suntil_induct_strong) case base then show ?case by (auto simp add: suntil.simps[of _ _ "stl (stl \)"] suntil.simps[of _ _ "stl \"] HLD_iff) next case step show ?case proof cases assume "((Mix`(L2\J)) \ HLD {End}) (stl \)" with step.hyps show ?thesis by (auto simp: inj_Mix HLD_iff elim: suntil.cases) next assume "\ ((Mix`(L2\J)) \ HLD {End}) (stl \)" with step.prems have "?U L2 (stl (stl \))" by (auto elim: suntil.cases) then show ?thesis by (rule step.hyps(4)[OF refl]) qed qed qed lemma visit_imp_in_H: "visit {i} J \ \ i \ H" by (auto simp: visit_def HLD_iff) lemma emeasure_visit: assumes I: "I \ H" and L: "L \ J" shows "emeasure \ {\\space \. visit I L \} = (\i\I. p_i i) * (card L * p_j)" proof - let ?J = "HLD (Mix`J)" and ?E = "(Mix`L) \ HLD {End}" let ?\ = "?J aand not ?E" let ?P = "\x P. emeasure (T x) {\\space (T x). P \}" have [intro]: "finite L" using finite_J \L \ J\ by (blast intro: finite_subset) have [simp, intro]: "finite I" using finite_J \I \ H\ by (blast intro: finite_subset) { fix j assume j: "j \ H" have "?P (Mix j) (?J suntil ?E) = (p_f * p_j * (1 - p_f) * card L) / (1 - p_f)" proof (rule emeasure_suntil_geometric) fix s assume s: "s \ Mix ` J" then have "?P s ?E = (\\<^sup>+x. ennreal (1 - p_f) * indicator (Mix`L) x \N s)" by (auto simp add: emeasure_HLD_nxt emeasure_HLD AE_measure_pmf_iff emeasure_pmf_single split: state.split split_indicator simp del: space_T nxt.simps intro!: nn_integral_cong_AE) also have "\ = ennreal (1 - p_f) * emeasure (N s) (Mix`L)" using p_f by (intro nn_integral_cmult_indicator) auto also have "\ = ennreal ((1 - p_f) * card L * p_j * p_f)" using s assms by (subst emeasure_measure_pmf_finite) (auto simp: sum.reindex subset_eq ennreal_mult mult_ac) finally show "?P s ?E = p_f * p_j * (1 - p_f) * card L" by simp next show "\t. AE \ in T t. \ (?E \ (?J \ nxt (?J suntil ?E))) \" by (intro AE_I2) (auto simp: HLD_iff elim: suntil.cases) qed (insert p_f j, auto simp: emeasure_measure_pmf_finite sum.reindex p_j_def) then have "?P (Init j) (?J suntil ?E) = (p_f * p_j * (1 - p_f) * card L) / (1 - p_f) / p_f" by (subst emeasure_Init_eq_Mix) (simp_all add: suntil.simps[of _ _ "x ## s" for x s] divide_ennreal p_f) then have "?P (Init j) (?J suntil ?E) = p_j * card L" using p_f by simp } note J_suntil_E = this have "?P Start (visit I L) = (\\<^sup>+x. ?P x (?J suntil ?E) * indicator (Init`I) x \N Start)" unfolding visit_def using I L by (subst emeasure_HLD_nxt) (auto simp: Int_absorb2) also have "\ = (\\<^sup>+x. ennreal (p_j * card L) * indicator (Init`I) x \N Start)" using I J_suntil_E by (intro nn_integral_cong ennreal_mult_right_cong) (auto split: split_indicator_asm) also have "\ = ennreal ((\i\I. p_i i) * card L * p_j)" using p_j_pos assms by (subst nn_integral_cmult_indicator) (auto simp: emeasure_measure_pmf_finite sum.reindex subset_eq ennreal_mult[symmetric] sum_nonneg) finally show ?thesis by (simp add: ac_simps) qed lemma measurable_visit[measurable]: "Measurable.pred S (visit I L)" by (simp add: visit_def) lemma AE_visit: "AE \ in \. visit H J \" proof (rule T.AE_I_eq_1) show "emeasure \ {\\space \. visit H J \} = 1" using J_not_empty by (subst emeasure_visit ) (simp_all add: p_j_def) qed simp subsection \Server gets no information\ lemma server_view1: "j \ J \ \

(\ in \. visit H {j} \) = p_j" unfolding measure_def by (subst emeasure_visit) simp_all lemma server_view_indep: "L \ J \ I \ H \ \

(\ in \. visit I L \) = \

(\ in \. visit H L \) * \

(\ in \. visit I J \)" unfolding measure_def by (subst (1 2 3) emeasure_visit) (auto simp: p_j_def sum_nonneg subset_eq) lemma server_view: "\

(\ in \. \j\H. visit {j} {j} \) = p_j" using finite_J proof (subst T.prob_sum[where I="H" and P="\j. visit {j} {j}"]) show "(\j\H. \

(\ in \. visit {j} {j} \)) = p_j" by (auto simp: measure_def emeasure_visit sum_distrib_right[symmetric] simp del: space_T sets_T) show "AE x in \. (\n\H. visit {n} {n} x \ (\j\H. visit {j} {j} x)) \ ((\j\H. visit {j} {j} x) \ (\!n. n \ H \ visit {n} {n} x))" by (auto dest: visit_unique1) qed simp_all subsection \Probability that collaborators gain information\ definition "hit_C = Init`H \ ev (HLD (Mix`C))" definition "before_C B = (HLD (Jondo H)) suntil ((Jondo (B \ H)) \ HLD (Mix ` C))" lemma measurable_hit_C[measurable]: "Measurable.pred S hit_C" by (simp add: hit_C_def) lemma measurable_before_C[measurable]: "Measurable.pred S (before_C B)" by (simp add: before_C_def) lemma before_C: assumes \: "enabled Start \" shows "before_C B \ \ ((Init`H \ (HLD (Mix`H) suntil (Mix`(B \ H) \ HLD (Mix`C)))) or (Init`(B \ H) \ HLD (Mix`C))) \" proof - { fix \ s assume "((HLD (Jondo H)) suntil (Jondo (B \ H) \ HLD (Mix ` C))) \" "enabled s \" "s \ Jondo H" then have "(HLD (Mix ` H) suntil (Mix ` (B \ H) \ (HLD (Mix ` C)))) \" proof (induction arbitrary: s) case (base \) then show ?case by (auto simp: HLD_iff enabled.simps[of _ \] E_Init E_Mix intro!: suntil.intros(1)) next case (step \) from step.prems step.hyps step.IH[of "shd \"] show ?case by (auto simp: HLD_iff enabled.simps[of _ \] E_Init E_Mix suntil.simps[of _ _ \] enabled_End suntil_sconst) qed } note this[of "stl \" "shd \"] moreover { fix \ s assume "(HLD (Mix ` H) suntil (Mix ` (B \ H) \ (HLD (Mix ` C)))) \" "enabled s \" "s \ Jondo H" then have "((HLD (Jondo H)) suntil ((Jondo (B \ H)) \ HLD (Mix ` C))) \" proof (induction arbitrary: s) case (step \) from step.prems step.hyps step.IH[of "shd \"] show ?case by (auto simp: HLD_iff enabled.simps[of _ \] E_Init E_Mix suntil.simps[of _ _ \] enabled_End suntil_sconst) qed (auto intro: suntil.intros simp: HLD_iff) } note this[of "stl \" "shd \"] ultimately show ?thesis using assms using \enabled Start \\ unfolding before_C_def suntil.simps[of _ _ \] enabled.simps[of _ \] by (auto simp: E_Start HLD_iff) qed lemma before_C_unique: assumes \: "before_C I1 \" "before_C I2 \" shows "I1 \ I2 \ {}" using \ unfolding before_C_def proof induction case (base \) then show ?case by (auto simp add: suntil.simps[of _ _ \] suntil.simps[of _ _ "stl \"] HLD_iff) next case (step \) then show ?case by (auto simp add: suntil.simps[of _ _ \] suntil.simps[of _ _ "stl \"] HLD_iff) qed lemma hit_C_imp_before_C: assumes "enabled Start \" "hit_C \" shows "before_C H \" proof - let ?X = "Init`H \ Mix`H" { fix \ s assume "ev (HLD (Mix`C)) \" "s\?X" "enabled s \" then have "((HLD (Jondo H)) suntil (?X \ HLD (Mix ` C))) (s ## \)" proof (induction arbitrary: s rule: ev_induct_strong) case (step \ s) from step.IH[of "shd \"] step.prems step.hyps show ?case by (auto simp: enabled.simps[of _ \] suntil_Stream E_Init E_Mix HLD_iff enabled_End ev_sconst) qed (auto simp: suntil_Stream) } from this[of "stl \" "shd \"] assms show ?thesis by (auto simp: before_C_def hit_C_def enabled.simps[of _ \] E_Start) qed lemma before_C_single: assumes "before_C I \" shows "\i\I \ H. before_C {i} \" using assms unfolding before_C_def by induction (auto simp: HLD_iff intro: suntil.intros) lemma before_C_imp_in_H: "before_C {i} \ \ i \ H" by (auto dest: before_C_single) subsection \The probability that the sender hits a collaborator\ lemma Pr_hit_C: "\

(\ in \. hit_C \) = (1 - p_H) / (1 - p_H * p_f)" proof - let ?P = "\x P. emeasure (T x) {\\space (T x). P \}" let ?M = "HLD (Mix ` C)" and ?I = "Init`H" and ?J = "Mix`H" let ?\ = "(HLD ?J) aand not ?M" { fix s assume s: "s \ Jondo J" have "AE \ in T s. ev ?M \ \ (HLD ?J suntil ?M) \" using AE_T_enabled proof eventually_elim fix \ assume \: "enabled s \" show "ev ?M \ \ (HLD ?J suntil ?M) \" proof assume "ev ?M \" from this \ s show "(HLD ?J suntil ?M) \" proof (induct arbitrary: s rule: ev_induct_strong) case (step \) then show ?case by (auto simp: HLD_iff enabled.simps[of _ \] suntil.simps[of _ _ \] E_End E_Init E_Mix enabled_End ev_sconst) qed (auto simp: HLD_iff E_Init intro: suntil.intros) qed (rule ev_suntil) qed } note ev_eq_suntil = this have "?P Start hit_C = (\\<^sup>+x. ?P x (ev ?M) * indicator ?I x \N Start)" unfolding hit_C_def by (rule emeasure_HLD_nxt) measurable also have "\ = (\\<^sup>+x. ennreal ((1 - p_H) / (1 - p_f * p_H)) * indicator ?I x \N Start)" proof (intro nn_integral_cong ennreal_mult_right_cong refl) fix x assume "indicator (Init ` H) x \ 0" then have "x \ ?I" by (auto split: split_indicator_asm) { fix j assume j: "j \ H" with ev_eq_suntil[of "Mix j"] have "?P (Mix j) (ev ?M) = ?P (Mix j) ((HLD ?J) suntil ?M)" by (intro emeasure_eq_AE) auto also have "\ = (((1 - p_H) * p_f)) / (1 - p_H * p_f)" proof (rule emeasure_suntil_geometric) fix s assume s: "s \ Mix ` H" from s C_smaller show "?P s ?M = ennreal ((1 - p_H) * p_f)" by (subst emeasure_HLD) (auto simp add: emeasure_measure_pmf_finite sum.reindex subset_eq p_j_def H_compl) from s show "emeasure (N s) (Mix`H) = p_H * p_f" by (auto simp: emeasure_measure_pmf_finite sum.reindex p_H_def p_j_def) qed (insert j, auto simp: HLD_iff p_H_p_f_less_1) finally have "?P (Init j) (ev ?M) = (1 - p_H) / (1 - p_H * p_f)" using p_f by (subst emeasure_Init_eq_Mix) (auto simp: ev_Stream AE_End ev_sconst HLD_iff mult_le_one divide_ennreal) } then show "?P x (ev ?M) = (1 - p_H) / (1 - p_f * p_H)" using \x \ ?I\ by (auto simp: mult_ac) qed also have "\ = ennreal ((1 - p_H) / (1 - p_H * p_f))" using p_j_pos p_H p_H_p_f_less_1 by (subst nn_integral_cmult_indicator) (auto simp: emeasure_measure_pmf_finite sum.reindex subset_eq mult_ac intro!: divide_nonneg_nonneg) finally show ?thesis by (simp add: measure_def mult_le_one) qed lemma before_C_imp_hit_C: assumes "enabled Start \" "before_C B \" shows "hit_C \" proof - { fix \ j assume "((HLD (Jondo H)) suntil (Jondo (B \ H) \ HLD (Mix ` C))) \" "j \ H" "enabled (Mix j) \" then have "ev (HLD (Mix`C)) \" proof (induction arbitrary: j rule: suntil_induct_strong) case (step \) then show ?case by (auto simp: enabled.simps[of _ \] E_Mix enabled_End ev_sconst suntil_sconst HLD_iff) qed auto } from this[of "stl (stl \)"] assms show "hit_C \" by (force simp: before_C_def hit_C_def E_Start HLD_iff E_Init enabled.simps[of _ \] ev.simps[of _ \] suntil.simps[of _ _ \] enabled.simps[of _ "stl \"] ev.simps[of _ "stl \"] suntil.simps[of _ _ "stl \"]) qed lemma negE: "\ P \ P \ False" by blast lemma Pr_visit_before_C: assumes L: "L \ H" and I: "I \ H" shows "\

(\ in \. visit I J \ \ before_C L \ \ hit_C \ ) = (\i\I. p_i i) * card L * p_j * p_f + (\i\I \ L. p_i i) * (1 - p_H * p_f)" proof - let ?M = "Mix`H" let ?P = "\x P. emeasure (T x) {\\space (T x). P \}" let ?V = "(visit I J aand before_C L) aand hit_C" let ?U = "HLD ?M suntil (Mix`L \ HLD (Mix`C))" let ?L = "HLD (Mix`C)" have IJ: "x \ I \ x \ J" for x using I by auto have [simp, intro]: "finite I" "finite L" using L I by (auto dest: finite_subset) have "?P Start ?V = ?P Start ((Init`I \ ?U) or (Init`(I \ L) \ ?L))" proof (rule emeasure_Collect_eq_AE) show "AE \ in \. ?V \ \ ((Init`I \ ?U) or (Init`(I \ L) \ ?L)) \" using AE_T_enabled AE_visit proof eventually_elim case (elim \) then show ?case using before_C_imp_hit_C[of \ "L"] before_C[of \ "L"] I L by (auto simp: visit_def HLD_iff Int_absorb2) qed show "Measurable.pred \ ((Init`I \ ?U) or (Init`(I \ L) \ ?L))" by measurable qed measurable also have "\ = ?P Start (Init`I \ ?U) + ?P Start (Init`(I \ L) \ ?L)" using L I apply (subst plus_emeasure) apply (auto intro!: arg_cong2[where f=emeasure]) apply (subst (asm) suntil.simps) apply (auto simp add: HLD_iff[abs_def] elim: suntil.cases) done also have "?P Start (Init`(I \ L) \ ?L) = (\i\I\L. p_i i * (1 - p_H))" using L I C_smaller p_j_pos apply (subst emeasure_HLD_nxt emeasure_HLD, simp)+ apply (subst nn_integral_indicator_finite) apply (auto simp: emeasure_measure_pmf_finite sum.reindex next_prob_def sum.If_cases Int_absorb2 H_compl2 ennreal_mult[symmetric] sum_nonneg sum_distrib_left[symmetric] sum_distrib_right[symmetric] intro!: sum.cong sum_nonneg) apply (subst (asm) ennreal_inj) apply (auto intro!: mult_nonneg_nonneg sum_nonneg sum.mono_neutral_left elim!: negE) done also have "?P Start (Init`I \ ?U) = (\i\I. ?P (Init i) ?U * p_i i)" using I by (subst emeasure_HLD_nxt, simp) (auto simp: nn_integral_indicator_finite sum.reindex emeasure_measure_pmf_finite intro!: sum.cong[OF refl]) also have "\ = (\i\I. ennreal (p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f)) * p_i i)" proof (intro sum.cong refl arg_cong2[where f="(*)"]) fix i assume "i \ I" with I have i: "i \ H" by auto have "?P (Mix i) ?U = (p_f * p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f))" unfolding before_C_def proof (rule emeasure_suntil_geometric[where X="?M"]) show "Mix i \ ?M" using i by auto next fix s assume "s \ ?M" with p_f p_j_pos L C_smaller[THEN less_imp_le] show "?P s (Mix`L \ (HLD (Mix ` C))) = ennreal (p_f * p_f * (1 - p_H) * p_j * card L)" apply (simp add: emeasure_HLD emeasure_HLD_nxt del: nxt.simps space_T) apply (subst nn_integral_measure_pmf_support[of "Mix`L"]) apply (auto simp add: subset_eq emeasure_measure_pmf_finite sum.reindex H_compl p_j_def ennreal_mult[symmetric] ennreal_of_nat_eq_real_of_nat) done next fix s assume "s \ ?M" then show "emeasure (N s) ?M = ennreal (p_H * p_f)" by (auto simp add: emeasure_measure_pmf_finite sum.reindex H_eq2) next show "AE \ in T t. \ ((Mix ` L \ ?L) \ (HLD (Mix ` H) \ nxt ?U)) \" for t using L apply (simp add: AE_T_iff[of _ t]) apply (subst AE_T_iff; simp) apply (auto simp: HLD_iff suntil_Stream) done qed (insert L, auto simp: p_H_p_f_less_1 E_Mix) then show "?P (Init i) ?U = p_f * (1 - p_H) * p_j * card L / (1 - p_H * p_f)" by (subst emeasure_Init_eq_Mix) (auto simp: AE_End suntil_Stream divide_ennreal mult_le_one p_f) qed finally have *: "\

(\ in T Start. ?V \) = (p_f * (1 - p_H) * p_j * (card L) / (1 - p_H * p_f)) * (\i\I. p_i i) + (\i\I \ L. p_i i) * (1 - p_H)" using sum_nonneg [of "I \ L" p_i] sum_nonneg [of "I" p_i] by (simp add: mult_ac measure_def sum_distrib_right[symmetric] sum_distrib_left[symmetric] sum_divide_distrib[symmetric] IJ ennreal_mult[symmetric] mult_le_one ennreal_plus[symmetric] del: ennreal_plus) show ?thesis unfolding cond_prob_def Pr_hit_C * using * using p_f p_H p_j_pos p_H_p_f_less_1 by (simp add: divide_simps) (simp add: field_simps) qed lemma Pr_visit_eq_before_C: "\

(\ in \. \j\H. visit {j} J \ \ before_C {j} \ \ hit_C \ ) = 1 - (p_H - p_j) * p_f" proof - let ?V = "\j. visit {j} J aand before_C {j}" and ?H = "hit_C" let ?J = "H" have "\

(\ in \. (\j\?J. ?V j \) \ ?H \) = (\j\?J. \

(\ in \. (?V j aand ?H) \))" proof (rule T.prob_sum) show "AE \ in \. (\j\?J. (?V j aand ?H) \ \ ((\j\?J. ?V j \) \ ?H \)) \ (((\j\?J. ?V j \) \ ?H \) \ (\!j. j\?J \ (?V j aand ?H) \))" by (auto intro!: AE_I2 dest: visit_unique1) qed auto then have "\

(\ in \. (\j\?J. ?V j \) \ ?H \) = (\j\?J. \

(\ in \. ?V j \ \ ?H \))" by (simp add: cond_prob_def sum_divide_distrib) also have "\ = p_j * p_f + (1 - p_H * p_f)" by (simp add: Pr_visit_before_C sum_distrib_right[symmetric] sum.distrib) finally show ?thesis by (simp add: field_simps) qed lemma probably_innocent: assumes approx: "1 / (2 * (p_H - p_j)) \ p_f" and "p_H \ p_j" shows "\

(\ in \. \j\H. visit {j} J \ \ before_C {j} \ \ hit_C \ ) \ 1 / 2" unfolding Pr_visit_eq_before_C proof - have [simp]: "\n :: nat. 1 \ real n \ 1 \ n" by auto have "0 \ p_j" unfolding p_j_def by auto then have "1 * p_j \ p_H" unfolding H_eq2[symmetric] using C_smaller by (intro mult_mono) (auto simp: Suc_le_eq card_Diff_subset not_le) with \p_H \ p_j\ have "p_j < p_H" by auto with approx show "1 - (p_H - p_j) * p_f \ 1 / 2" by (auto simp add: field_simps divide_le_eq split: if_split_asm) qed lemma Pr_before_C: assumes L: "L \ H" shows "\

(\ in \. before_C L \ \ hit_C \ ) = card L * p_j * p_f + (\l\L. p_i l) * (1 - p_H * p_f)" proof - have "\

(\ in \. before_C L \ \ hit_C \ ) = \

(\ in \. visit H J \ \ before_C L \ \ hit_C \ )" using AE_visit by (auto intro!: T.cond_prob_eq_AE) also have "\ = card L * p_j * p_f + (\i\L. p_i i) * (1 - p_H * p_f)" using L by (subst Pr_visit_before_C[OF L order_refl]) (auto simp: Int_absorb1) finally show ?thesis . qed lemma P_visit: assumes I: "I \ H" shows "\

(\ in \. visit I J \ \ hit_C \ ) = (\i\I. p_i i)" proof - have "\

(\ in \. visit I J \ \ hit_C \ ) = \

(\ in \. visit I J \ \ before_C H \ \ hit_C \ )" proof (rule T.cond_prob_eq_AE) show "AE x in \. hit_C x \ visit I J x = (visit I J x \ before_C H x)" using AE_T_enabled by eventually_elim (auto intro: hit_C_imp_before_C) qed auto also have "\ = sum p_i I" using I by (subst Pr_visit_before_C[OF order_refl]) (auto simp: Int_absorb2 field_simps p_H_def p_j_def) finally show ?thesis . qed subsection \Probability space of hitting a collaborator\ definition "hC = uniform_measure \ {\\space \. hit_C \}" lemma emeasure_hit_C_not_0: "emeasure \ {\ \ space \. hit_C \} \ 0" using p_H p_H_p_f_less_1 unfolding Pr_hit_C T.emeasure_eq_measure by auto lemma measurable_hC[measurable (raw)]: "A \ sets S \ A \ sets hC" "f \ measurable M S \ f \ measurable M hC" "g \ measurable S M \ g \ measurable hC M" "A \ space S \ sets S \ A \ space hC \ sets S" unfolding hC_def uniform_measure_def by simp_all lemma vimage_Int_space_C[simp]: "f -` {x} \ space hC = {\\space S. f \ = x}" by (auto simp: hC_def) sublocale hC: information_space hC 2 proof - interpret hC: prob_space hC unfolding hC_def using emeasure_hit_C_not_0 by (intro prob_space_uniform_measure) auto show "information_space hC 2" by standard simp qed abbreviation mutual_information_Pow_CP ("\'(_ ; _')") where "\(X ; Y) \ hC.mutual_information 2 (count_space (X`space hC)) (count_space (Y`space hC)) X Y" lemma simple_functionI: assumes "finite (range f)" assumes [measurable]: "\x. {\\space S. f \ = x} \ sets S" shows "simple_function hC f" using assms unfolding simple_function_def hC_def by (simp add: vimage_def space_stream_space) subsection \Estimate the information to the collaborators\ lemma measure_hC[simp]: assumes A[measurable]: "A \ sets S" shows "measure hC A = \

(\ in \. \ \ A \ hit_C \ )" unfolding hC_def cond_prob_def using emeasure_hit_C_not_0 A by (subst measure_uniform_measure) (simp_all add: T.emeasure_eq_measure Int_def conj_ac) subsubsection \Setup random variables for mutual information\ definition "first_J \ = (THE i. visit {i} J \)" lemma first_J_eq: "visit {i} J \ \ first_J \ = i" unfolding first_J_def by (intro the_equality) (auto dest: visit_unique1) lemma AE_first_J: "AE \ in \. visit {i} J \ \ first_J \ = i" using AE_visit proof eventually_elim fix \ assume "visit H J \" then obtain j where "visit {j} J \" "j \ H" by (auto simp: visit_def HLD_iff) then show "visit {i} J \ \ first_J \ = i" by (auto dest: visit_unique1 first_J_eq) qed lemma measurbale_first_J[measurable]: "first_J \ measurable S (count_space UNIV)" unfolding first_J_def[abs_def] by (intro measurable_THE[where I=H]) (auto dest: visit_imp_in_H visit_unique1 intro: countable_finite) definition "last_H \ = (THE i. before_C {i} \)" lemma measurbale_last_H[measurable]: "last_H \ measurable S (count_space UNIV)" unfolding last_H_def[abs_def] by (intro measurable_THE[where I=H]) (auto dest: before_C_single before_C_unique intro: countable_finite) lemma last_H_eq: "before_C {i} \ \ last_H \ = i" unfolding last_H_def by (intro the_equality) (auto dest: before_C_unique) lemma last_H: assumes "enabled Start \" "hit_C \" shows "before_C {last_H \} \" "last_H \ \ H" by (metis before_C_single hit_C_imp_before_C last_H_eq Int_iff assms)+ lemma AE_last_H: "AE \ in \. hit_C \ \ before_C {i} \ \ last_H \ = i" using AE_T_enabled proof eventually_elim fix \ assume "enabled Start \" then show "hit_C \ \ before_C {i} \ = (last_H \ = i)" by (auto dest: last_H last_H_eq) qed lemma information_flow: defines "h \ real (card H)" assumes init_uniform: "\i. i \ H \ p_i i = 1 / h" shows "\(first_J ; last_H) \ (1 - (h - 1) * p_j * p_f) * log 2 h" proof - let ?il = "\i l. \

(\ in \. visit {i} J \ \ before_C {l} \ \ hit_C \ )" let ?i = "\i. \

(\ in \. visit {i} J \ \ hit_C \ )" let ?l = "\l. \

(\ in \. before_C {l} \ \ hit_C \ )" from init_uniform have init_H: "\i. i \ H \ p_i i = p_j / p_H" by (simp add: p_j_def p_H_def h_def) from h_def have "1/h = p_j/p_H" "h = p_H / p_j" "p_H = h * p_j" by (auto simp: p_H_def p_j_def field_simps) from C_smaller have h_pos: "0 < h" by (auto simp add: card_gt_0_iff h_def) let ?s = "(h - 1) * p_j" let ?f = "?s * p_f" from psubset_card_mono[OF _ C_smaller] have "1 \ card J - card C" by (simp del: C_le_J) then have "1 \ h" using C_smaller by (simp add: h_def card_Diff_subset card_mono field_simps del: C_le_J) have log_le_0: "?f * log 2 (p_H * p_f) \ ?f * log 2 1" using p_H_p_f_less_1 p_H_p_f_pos p_j_pos p_f \1 \ h\ - by (intro mult_left_mono log_le mult_nonneg_nonneg) auto + by (intro mult_left_mono log_mono mult_nonneg_nonneg) auto have "(h - 1) * p_j < 1" using \1 \ h\ C_smaller by (auto simp: h_def p_j_def divide_less_eq card_Diff_subset card_mono) then have 1: "(h - 1) * p_j * p_f < 1 * 1" using p_f by (intro mult_strict_mono) auto { fix \ have "first_J \ \ H \ first_J \ = (THE x. False)" apply (cases "\i. \ visit {i} J \") apply (simp add: first_J_def) apply (auto dest: visit_imp_in_H first_J_eq) done } then have range_fj: "range first_J \ H \ {THE x. False}" by auto have sf_fj: "simple_function hC first_J" by (rule simple_functionI) (auto intro: finite_subset[OF range_fj]) have sd_fj: "simple_distributed hC first_J ?i" apply (rule hC.simple_distributedI[OF sf_fj]) apply (auto intro!: T.cond_prob_eq_AE) apply (auto simp: space_stream_space) using AE_first_J apply eventually_elim apply auto done { fix \ have "last_H \ \ H \ last_H \ = (THE x. False)" apply (cases "\i. \ before_C {i} \") apply (simp add: last_H_def) apply (auto dest: before_C_imp_in_H last_H_eq) done } then have range_lnc: "range last_H \ H \ {THE x. False}" by auto have sf_lnc: "simple_function hC last_H" by (rule simple_functionI) (auto intro: finite_subset[OF range_lnc]) have sd_lnc: "simple_distributed hC last_H ?l" apply (rule hC.simple_distributedI[OF sf_lnc]) apply (auto intro!: T.cond_prob_eq_AE) apply (auto simp: space_stream_space) using AE_last_H apply eventually_elim apply auto done have sd_fj_lnc: "simple_distributed hC (\\. (first_J \, last_H \)) (\(i, l). ?il i l)" apply (rule hC.simple_distributedI) apply (rule simple_function_Pair[OF sf_fj sf_lnc]) apply (auto intro!: T.cond_prob_eq_AE) apply (auto simp: space_stream_space) using AE_last_H AE_first_J apply eventually_elim apply auto done define c where "c = (SOME j. j \ C)" have c: "c \ C" using C_non_empty unfolding ex_in_conv[symmetric] c_def by (rule someI_ex) let ?inner = "\i. \l\H. ?il i l * log 2 (?il i l / (?i i * ?l l))" { fix i assume i: "i \ H" with h_pos have card_idx: "real_of_nat (card (H - {i})) = p_H / p_j - 1" by (auto simp add: p_j_def p_H_def h_def) have neq0: "p_j \ 0" "p_H \ 0" unfolding p_j_def p_H_def using C_smaller i by auto from i have "?inner i = (\l\H - {i}. ?il i l * log 2 (?il i l / (?i i * ?l l))) + ?il i i * log 2 (?il i i / (?i i * ?l i))" by (simp add: sum_diff) also have "\ = (\l\H - {i}. p_j/p_H * p_j * p_f * log 2 (p_j * p_f / (p_j * p_f + p_j/p_H * (1 - p_H * p_f)))) + p_j/p_H * (p_j * p_f + (1 - p_H * p_f)) * log 2 ((p_j * p_f + (1 - p_H * p_f)) / (p_j * p_f + p_j/p_H * (1 - p_H * p_f)))" using i p_f p_j_pos p_H apply (simp add: Pr_visit_before_C P_visit init_H Pr_before_C del: sum_constant) apply (simp add: divide_simps distrib_left) apply (intro arg_cong2[where f="(*)"] refl arg_cong2[where f=log]) apply (auto simp: field_simps) done also have "\ = (?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)) / h" using neq0 p_f by (simp add: card_idx field_simps \p_H = h * p_j\) finally have "?inner i = (?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)) / h" . } then have "(\i\H. ?inner i) = ?f * log 2 (h * p_j * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)" using h_pos by (simp add: h_def[symmetric]) also have "\ = ?f * log 2 (p_H * p_f) + (1 - ?f) * log 2 ((1 - ?f) * h)" by (simp add: \h = p_H / p_j\) also have "\ \ (1 - ?f) * log 2 ((1 - ?f) * h)" using log_le_0 by simp also have "\ \ (1 - ?f) * log 2 h" using h_pos \1 \ h\ 1 p_j_pos p_f - by (intro mult_left_mono log_le mult_pos_pos mult_nonneg_nonneg) auto + by (intro mult_left_mono log_mono mult_pos_pos mult_nonneg_nonneg) auto finally have "(\i\H. ?inner i) \ (1 - ?f) * log 2 h" . also have "(\i\H. ?inner i) = (\(i, l)\(first_J`space S) \ (last_H`space S). ?il i l * log 2 (?il i l / (?i i * ?l l)))" unfolding sum.cartesian_product proof (safe intro!: sum.mono_neutral_cong_left del: DiffE DiffI) show "finite ((first_J ` space S) \ (last_H ` space S))" using sf_fj sf_lnc by (auto simp add: hC_def dest!: simple_functionD(1)) next fix i assume "i \ H" then have "visit {i} J (Init i ## Mix i ## sconst End)" "before_C {i} (Init i ## Mix c ## sconst End)" by (auto simp: before_C_def visit_def suntil_Stream HLD_iff c) then show "i \ first_J ` space S" "i \ last_H ` space S" by (auto simp: space_stream_space image_iff eq_commute dest!: first_J_eq last_H_eq) next fix i l assume "(i, l) \ first_J ` space S \ last_H ` space S - H \ H" then have H: "i \ H \ l \ H" by auto have "\

(\ in \. (visit {i} J \ \ before_C {l} \) \ hit_C \) = 0" using H by (intro T.prob_eq_0_AE) (auto dest: visit_imp_in_H before_C_imp_in_H) then show "?il i l * log 2 (?il i l / (?i i * ?l l)) = 0" by (simp add: cond_prob_def) qed also have "\ = \(first_J ; last_H)" unfolding sum.cartesian_product apply (subst hC.mutual_information_simple_distributed[OF sd_fj sd_lnc sd_fj_lnc]) apply (simp add: hC_def) proof (safe intro!: sum.mono_neutral_right imageI) show "finite ((first_J ` space S) \ (last_H ` space S))" using sf_fj sf_lnc by (auto simp add: hC_def dest!: simple_functionD(1)) next fix i l assume "(first_J i, last_H l) \ (\x. (first_J x, last_H x)) ` space S" moreover { fix i l assume "i \ H" "l \ H" then have "visit {i} J (Init i ## Mix l ## Mix c ## sconst End)" "before_C {l} (Init i ## Mix l ## Mix c ## sconst End)" using c C_smaller by (auto simp: before_C_def visit_def HLD_iff suntil_Stream) then have "first_J (Init i ## Mix l ## Mix c ## sconst End) = i" "last_H (Init i ## Mix l ## Mix c ## sconst End) = l" by (auto intro!: first_J_eq last_H_eq) } note this[of "first_J i" "last_H l"] ultimately have "(first_J i, last_H l) \ H\H" by (auto simp: space_stream_space image_iff eq_commute) metis then have "\

(\ in \. (visit {first_J i} J \ \ before_C {last_H l} \) \ hit_C \) = 0" by (intro T.prob_eq_0_AE) (auto dest: visit_imp_in_H before_C_imp_in_H) then show "?il (first_J i) (last_H l) * log 2 (?il (first_J i) (last_H l) / (?i (first_J i) * ?l (last_H l))) = 0" by (simp add: cond_prob_def) qed finally show ?thesis by simp qed end end diff --git a/thys/Probabilistic_While/Fast_Dice_Roll.thy b/thys/Probabilistic_While/Fast_Dice_Roll.thy --- a/thys/Probabilistic_While/Fast_Dice_Roll.thy +++ b/thys/Probabilistic_While/Fast_Dice_Roll.thy @@ -1,415 +1,415 @@ (* Title: Fast_Dice_Roll.thy Author: Andreas Lochbihler, ETH Zurich *) subsection \Arbitrary uniform distributions\ theory Fast_Dice_Roll imports Bernoulli While_SPMF begin text \This formalisation follows the ideas by J\'er\'emie Lumbroso \<^cite>\"Lumbroso2013arxiv"\.\ lemma sample_bits_fusion: fixes v :: nat assumes "0 < v" shows "bind_pmf (pmf_of_set {..c. bind_pmf (pmf_of_set UNIV) (\b. f (2 * c + (if b then 1 else 0)))) = bind_pmf (pmf_of_set {..<2 * v}) f" (is "?lhs = ?rhs") proof - have "?lhs = bind_pmf (map_pmf (\(c, b). (2 * c + (if b then 1 else 0))) (pair_pmf (pmf_of_set {.. i div 2" define b where "b \ odd i" have i: "i = ?f (i', b)" by(simp add: i'_def b_def) show "pmf ?l i = pmf ?r i" by(subst i; subst pmf_map_inj')(simp_all add: pmf_pair i'_def assms lessThan_empty_iff split: split_indicator) qed finally show ?thesis . qed lemma sample_bits_fusion2: fixes v :: nat assumes "0 < v" shows "bind_pmf (pmf_of_set UNIV) (\b. bind_pmf (pmf_of_set {..c. f (c + v * (if b then 1 else 0)))) = bind_pmf (pmf_of_set {..<2 * v}) f" (is "?lhs = ?rhs") proof - have "?lhs = bind_pmf (map_pmf (\(c, b). (c + v * (if b then 1 else 0))) (pair_pmf (pmf_of_set {.. UNIV)" by(auto simp add: inj_on_def) define i' where "i' \ if i \ v then i - v else i" define b where "b \ i \ v" have i: "i = ?f (i', b)" by(simp add: i'_def b_def) show "pmf ?l i = pmf ?r i" proof(cases "i < 2 * v") case True thus ?thesis by(subst i; subst pmf_map_inj)(auto simp add: pmf_pair i'_def assms lessThan_empty_iff split: split_indicator) next case False hence "i \ set_pmf ?l" "i \ set_pmf ?r" using assms by(auto simp add: lessThan_empty_iff split: if_split_asm) thus ?thesis by(simp add: set_pmf_iff del: set_map_pmf) qed qed finally show ?thesis . qed context fixes n :: nat notes [[function_internals]] begin text \ The check for @{term "v >= n"} should be done already at the start of the loop. Otherwise we do not see why this algorithm should be optimal (when we start with @{term "v = n"} and @{term "c = n - 1"}, then it can go round a few loops before it returns something). We define the algorithm as a least fixpoint. To prove termination, we later show that it is equivalent to a while loop which samples bitstrings of a given length, which could in turn be implemented as a loop. The fixpoint formulation is more elegant because we do not need to nest any loops. \ partial_function (spmf) fast_dice_roll :: "nat \ nat \ nat spmf" where "fast_dice_roll v c = (if v \ n then if c < n then return_spmf c else fast_dice_roll (v - n) (c - n) else do { b \ coin_spmf; fast_dice_roll (2 * v) (2 * c + (if b then 1 else 0)) } )" lemma fast_dice_roll_fixp_induct [case_names adm bottom step]: assumes "spmf.admissible (\fast_dice_roll. P (curry fast_dice_roll))" and "P (\v c. return_pmf None)" and "\fdr. P fdr \ P (\v c. if v \ n then if c < n then return_spmf c else fdr (v - n) (c - n) else bind_spmf coin_spmf (\b. fdr (2 * v) (2 * c + (if b then 1 else 0))))" shows "P fast_dice_roll" using assms by(rule fast_dice_roll.fixp_induct) definition fast_uniform :: "nat spmf" where "fast_uniform = fast_dice_roll 1 0" lemma spmf_fast_dice_roll_ub: assumes "0 < v" shows "spmf (bind_pmf (pmf_of_set {.. (if x < n then 1 / n else 0)" (is "?lhs \ ?rhs") proof - have "ennreal ?lhs \ ennreal ?rhs" using assms proof(induction arbitrary: v x rule: fast_dice_roll_fixp_induct) case adm thus ?case by(rule cont_intro ccpo_class.admissible_leI)+ simp_all case bottom thus ?case by simp case (step fdr) show ?case (is "?lhs \ ?rhs") proof(cases "n \ v") case le: True then have "?lhs = spmf (bind_pmf (pmf_of_set {..c. if c < n then return_spmf c else fdr (v - n) (c - n))) x" by simp also have "\ = (\\<^sup>+ c'. indicator (if x < n then {x} else {}) c' \measure_pmf (pmf_of_set {..\<^sup>+ c'. indicator {n ..< v} c' * spmf (fdr (v - n) (c' - n)) x \measure_pmf (pmf_of_set {..\<^sup>+ c'. indicator {n ..< v} c' * 1 / v * spmf (fdr (v - n) (c' - n)) x \count_space UNIV)" using step.prems by(auto simp add: nn_integral_measure_pmf lessThan_empty_iff ennreal_mult[symmetric] intro!: nn_integral_cong split: split_indicator) also have "\ = (if v = n then 0 else ennreal ((v - n) / v) * spmf (bind_pmf (pmf_of_set {n..c'. fdr (v - n) (c' - n))) x)" using le step.prems by(subst ennreal_pmf_bind)(auto simp add: ennreal_mult[symmetric] nn_integral_measure_pmf nn_integral_0_iff_AE AE_count_space nn_integral_cmult[symmetric] split: split_indicator) also { assume *: "n < v" then have "pmf_of_set {n.. (\c'. fdr (v - n) (c' - n)) = bind_pmf (pmf_of_set {.. x) \ (if x < n then 1 / n else 0)" by(rule step.IH)(simp add: *) also note calculation } then have "\ \ ennreal ((v - n) / v) * (if x < n then 1 / n else 0)" using le by(cases "v = n")(auto split del: if_split intro: divide_right_mono mult_left_mono) also have "\ = (v - n) / v * (if x < n then 1 / n else 0)" by(simp add: ennreal_mult[symmetric]) finally show ?thesis using le by(auto simp add: add_mono field_simps of_nat_diff ennreal_plus[symmetric] simp del: ennreal_plus) next case False then have "?lhs = spmf (bind_pmf (pmf_of_set {..c. bind_pmf (pmf_of_set UNIV) (\b. fdr (2 * v) (2 * c + (if b then 1 else 0))))) x" by(simp add: bind_spmf_spmf_of_set) also have "\ = spmf (bind_pmf (pmf_of_set {..<2 * v}) (fdr (2 * v))) x" using step.prems by(simp add: sample_bits_fusion[symmetric]) also have "\ \ ?rhs" using step.prems by(intro step.IH) simp finally show ?thesis . qed qed thus ?thesis by simp qed lemma spmf_fast_uniform_ub: "spmf fast_uniform x \ (if x < n then 1 / n else 0)" proof - have "{..To prove termination, we fold all the iterations that only double into one big step\ definition fdr_step :: "nat \ nat \ (nat \ nat) spmf" where "fdr_step v c = (if v = 0 then return_pmf None else let x = 2 ^ (nat \log 2 (max 1 n) - log 2 v\) in map_spmf (\bs. (x * v, x * c + bs)) (spmf_of_set {.. v then return_spmf (v, c) else do { b \ coin_spmf; fdr_step (2 * v) (2 * c + (if b then 1 else 0)) })" (is "?lhs = ?rhs" is "_ = (if _ then _ else ?else)") proof(cases "v = 0") case v: False define x where "x \ \v :: nat. 2 ^ (nat \log 2 (max 1 n) - log 2 v\) :: nat" have x_pos: "x v > 0" by(simp add: x_def) show ?thesis proof(cases "n \ v") case le: True - hence "x v = 1" using v by(simp add: x_def log_le) + hence "x v = 1" using v by(simp add: x_def log_mono) moreover have "{..<1} = {0 :: nat}" by auto ultimately show ?thesis using le v by(simp add: fdr_step_def spmf_of_set_singleton) next case less: False hence even: "even (x v)" using v by(simp add: x_def) with x_pos have x_ge_1: "x v > 1" by(cases "x v = 1") auto have *: "x (2 * v) = x v div 2" using v less unfolding x_def apply(simp add: log_mult diff_add_eq_diff_diff_swap) apply(rewrite in "_ = 2 ^ \ div _" le_add_diff_inverse2[symmetric, where b=1]) apply (simp add: Suc_leI) apply(simp del: Suc_pred) done have "?lhs = map_spmf (\bs. (x v * v, x v * c + bs)) (spmf_of_set {.. = bind_pmf (pmf_of_set {..<2 * (x v div 2)}) (\bs. return_spmf (x v * v, x v * c + bs))" by(simp add: map_spmf_conv_bind_spmf bind_spmf_spmf_of_set x_pos lessThan_empty_iff) also have "\ = bind_spmf coin_spmf (\b. bind_spmf (spmf_of_set {..c'. return_spmf (x v * v, x v * c + c' + (x v div 2) * (if b then 1 else 0))))" using x_ge_1 by(simp add: sample_bits_fusion2[symmetric] bind_spmf_spmf_of_set lessThan_empty_iff add.assoc) also have "\ = bind_spmf coin_spmf (\b. map_spmf (\bs. (x (2 * v) * (2 * v), x (2 * v) * (2 * c + (if b then 1 else 0)) + bs)) (spmf_of_set {.. = ?rhs" using v less by(simp add: fdr_step_def Let_def x_def) finally show ?thesis . qed qed(simp add: fdr_step_def) lemma fdr_step_induct [case_names fdr_step]: "(\v c. (\b. \v \ 0; v < n\ \ P (2 * v) (2 * c + (if b then 1 else 0))) \ P v c) \ P v c" apply induction_schema apply pat_completeness apply(relation "Wellfounded.measure (\(v, c). n - v)") apply simp_all done partial_function (spmf) fdr_alt :: "nat \ nat \ nat spmf" where "fdr_alt v c = do { (v', c') \ fdr_step v c; if c' < n then return_spmf c' else fdr_alt (v' - n) (c' - n) }" lemma fast_dice_roll_alt: "fdr_alt = fast_dice_roll" proof(intro ext) show "fdr_alt v c = fast_dice_roll v c" for v c proof(rule spmf.leq_antisym) show "ord_spmf (=) (fdr_alt v c) (fast_dice_roll v c)" proof(induction arbitrary: v c rule: fdr_alt.fixp_induct[case_names adm bottom step]) case adm show ?case by simp case bottom show ?case by simp case (step fdra) show ?case proof(induction v c rule: fdr_step_induct) case inner: (fdr_step v c) show ?case apply(rewrite fdr_step_unfold) apply(rewrite fast_dice_roll.simps) apply(auto intro!: ord_spmf_bind_reflI simp add: Let_def inner.IH step.IH) done qed qed have "ord_spmf (=) (fast_dice_roll v c) (fdr_alt v c)" and "fast_dice_roll 0 c = return_pmf None" proof(induction arbitrary: v c rule: fast_dice_roll_fixp_induct) case adm thus ?case by simp case bottom case 1 thus ?case by simp case bottom case 2 thus ?case by simp case (step fdr) case 1 show ?case apply(rewrite fdr_alt.simps) apply(rewrite fdr_step_unfold) apply(clarsimp simp add: Let_def) apply(auto intro!: ord_spmf_bind_reflI simp add: fdr_alt.simps[symmetric] step.IH rel_pmf_return_pmf2 set_pmf_bind_spmf o_def set_pmf_spmf_of_set split: if_split_asm) done case step case 2 from step.IH show ?case by(simp add: Let_def bind_eq_return_pmf_None) qed then show "ord_spmf (=) (fast_dice_roll v c) (fdr_alt v c)" by - qed qed lemma lossless_fdr_step [simp]: "lossless_spmf (fdr_step v c) \ v > 0" by(simp add: fdr_step_def Let_def lessThan_empty_iff) lemma fast_dice_roll_alt_conv_while: "fdr_alt v c = map_spmf snd (bind_spmf (fdr_step v c) (loop_spmf.while (\(v, c). n \ c) (\(v, c). fdr_step (v - n) (c - n))))" proof(induction arbitrary: v c rule: parallel_fixp_induct_2_1[OF partial_function_definitions_spmf partial_function_definitions_spmf fdr_alt.mono loop_spmf.while.mono fdr_alt_def loop_spmf.while_def, case_names adm bottom step]) case adm show ?case by(simp) case bottom show ?case by simp case (step fdr while) show ?case using step.IH by(auto simp add: map_spmf_bind_spmf o_def intro!: bind_spmf_cong[OF refl]) qed lemma lossless_fast_dice_roll: assumes "c < v" "v \ n" shows "lossless_spmf (fast_dice_roll v c)" proof(cases "v < n") case True let ?I = "\(v, c). c < v \ n \ v \ v < 2 * n" let ?f = "\(v, c). if n \ c then n + c - v + 1 else 0" have invar: "?I (v', c')" if step: "(v', c') \ set_spmf (fdr_step (v - n) (c - n))" and I: "c < v" "n \ v" "v < 2 * n" and c: "n \ c" for v' c' v c proof(clarsimp; safe) define x where "x = nat \log 2 (max 1 n) - log 2 (v - n)\" have **: "-1 < log 2 (real n / real (v - n))" by(rule less_le_trans[where y=0])(use I c in \auto\) from I c step obtain bs where v': "v' = 2 ^ x * (v - n)" and c': "c' = 2 ^ x * (c - n) + bs" and bs: "bs < 2 ^ x" unfolding fdr_step_def x_def[symmetric] by(auto simp add: Let_def) have "2 ^ x * (c - n) + bs < 2 ^ x * (c - n + 1)" unfolding distrib_left using bs by(intro add_strict_left_mono) simp also have "\ \ 2 ^ x * (v - n)" using I c by(intro mult_left_mono) auto finally show "c' < v'" using c' v' by simp have "v' = 2 powr x * (v - n)" by(simp add: powr_realpow v') also have "\ < 2 powr (log 2 (max 1 n) - log 2 (v - n) + 1) * (v - n)" using ** I c by(intro mult_strict_right_mono)(auto simp add: x_def log_divide) also have "\ \ 2 * n" unfolding powr_add using I c by(simp add: log_divide[symmetric] max_def) finally show "v' < 2 * n" using c' by(simp del: of_nat_add) have "log 2 (n / (v - n)) \ x" using I c ** by(auto simp add: x_def log_divide max_def) hence "2 powr log 2 (n / (v - n)) \ 2 powr x" by(rule powr_mono) simp also have "2 powr log 2 (n / (v - n)) = n / (v - n)" using I c by(simp) finally have "n \ real (2 ^ x * (v - n))" using I c by(simp add: field_simps powr_realpow) then show "n \ v'" by(simp add: v' del: of_nat_mult) qed have loop: "lossless_spmf (loop_spmf.while (\(v, c). n \ c) (\(v, c). fdr_step (v - n) (c - n)) (v, c))" if "c < 2 * n" and "n \ v" and "c < v" and "v < 2 * n" for v c proof(rule termination_variant_invar; clarify?) fix v c assume I: "?I (v, c)" and c: "n \ c" show "?f (v, c) \ n" using I c by auto define x where "x = nat \log 2 (max 1 n) - log 2 (v - n)\" define p :: real where "p \ 1 / (2 * n)" from I c have n: "0 < n" and v: "n < v" by auto from I c v n have x_pos: "x > 0" by(auto simp add: x_def max_def) have **: "-1 < log 2 (real n / real (v - n))" by(rule less_le_trans[where y=0])(use I c in \auto\) then have "x \ log 2 (real n) + 1" using v n by(auto simp add: x_def log_divide[symmetric] max_def field_simps intro: order_trans[OF of_int_ceiling_le_add_one]) hence "2 powr x \ 2 powr \" by(rule powr_mono) simp hence "p \ 1 / 2 ^ x" unfolding powr_add using n by(subst (asm) powr_realpow, simp)(subst (asm) powr_log_cancel; simp_all add: p_def field_simps) also let ?X = "{c'. n \ 2 ^ x * (c - n) + c' \ n + (2 ^ x * (c - n) + c') - 2 ^ x * (v - n) < n + c - v}" have "n + c * 2 ^ x - v * 2 ^ x < c + n - v" using I c proof(cases "n + c * 2 ^ x \ v * 2 ^ x") case True have "(int c - v) * 2 ^ x < (int c - v) * 1" using x_pos I c by(intro mult_strict_left_mono_neg) simp_all then have "int n + c * 2 ^ x - v * 2 ^ x < c + int n - v" by(simp add: algebra_simps) also have "\ = int (c + n - v)" using I c by auto also have "int n + c * 2 ^ x - v * 2 ^ x = int (n + c * 2 ^ x - v * 2 ^ x)" using True that by(simp add: of_nat_diff) finally show ?thesis by simp qed auto then have "{..<2 ^ x} \ ?X \ {}" using that n v by(auto simp add: disjoint_eq_subset_Compl Collect_neg_eq[symmetric] lessThan_subset_Collect algebra_simps intro: exI[where x=0]) then have "0 < card ({..<2 ^ x} \ ?X)" by(simp add: card_gt_0_iff) hence "1 / 2 ^ x \ \ / 2 ^ x" by(simp add: field_simps) finally show "p \ spmf (map_spmf (\s'. ?f s' < ?f (v, c)) (fdr_step (v - n) (c - n))) True" using I c unfolding fdr_step_def x_def[symmetric] by(clarsimp simp add: Let_def spmf.map_comp o_def spmf_map measure_spmf_of_set vimage_def p_def) show "lossless_spmf (fdr_step (v - n) (c - n))" using I c by simp show "?I (v', c')" if step: "(v', c') \ set_spmf (fdr_step (v - n) (c - n))" for v' c' using that by(rule invar)(use I c in auto) next show "(0 :: real) < 1 / (2 * n)" using that by(simp) show "?I (v, c)" using that by simp qed show ?thesis using assms True by(auto simp add: fast_dice_roll_alt[symmetric] fast_dice_roll_alt_conv_while intro!: loop dest: invar[of _ _ "n + v" "n + c", simplified]) next case False with assms have "v = n" by simp thus ?thesis using assms by(subst fast_dice_roll.simps) simp qed lemma fast_dice_roll_n0: assumes "n = 0" shows "fast_dice_roll v c = return_pmf None" by(induction arbitrary: v c rule: fast_dice_roll_fixp_induct)(simp_all add: assms) lemma lossless_fast_uniform [simp]: "lossless_spmf fast_uniform \ n > 0" proof(cases "n = 0") case True then show ?thesis using fast_dice_roll_n0 unfolding fast_uniform_def by(simp) next case False then show ?thesis by(simp add: fast_uniform_def lossless_fast_dice_roll) qed lemma spmf_fast_uniform: "spmf fast_uniform x = (if x < n then 1 / n else 0)" proof(cases "n > 0") case n: True show ?thesis using spmf_fast_uniform_ub proof(rule spmf_ub_tight) have "(\\<^sup>+ x. ennreal (if x < n then 1 / n else 0)) = (\\<^sup>+ x\{.. = 1" using n by(simp add: field_simps ennreal_of_nat_eq_real_of_nat ennreal_mult[symmetric]) also have "\ = weight_spmf fast_uniform" using lossless_fast_uniform n unfolding lossless_spmf_def by simp finally show "(\\<^sup>+ x. ennreal (if x < n then 1 / n else 0)) = \" . qed next case False with fast_dice_roll_n0[of 1 0] show ?thesis unfolding fast_uniform_def by(simp) qed end lemma fast_uniform_conv_uniform: "fast_uniform n = spmf_of_set {.., Lawrence Paulson , 2014 Maintainer: Quentin Hibon *) theory Source_Coding_Theorem imports "HOL-Probability.Information" begin section\Basic types\ type_synonym bit = bool type_synonym bword = "bit list" type_synonym letter = nat type_synonym 'b word = "'b list" type_synonym 'b encoder = "'b word \ bword" type_synonym 'b decoder = "bword \ 'b word option" section\Locale for the source coding theorem\ locale source_code = information_space + fixes fi :: "'b \ real" fixes X :: "'a \ 'b" assumes distr_i: "simple_distributed M X fi" assumes b_val: "b = 2" fixes enc::"'b encoder" fixes dec::"'b decoder" assumes real_code: "dec (enc x) = Some x" "enc w = [] \ w = []" "x \ [] \ enc x = enc [hd x] @ enc (tl x)" section\Source coding theorem, direct: the entropy is a lower bound of the code rate\ context source_code begin subsection\The letter set\ definition L :: "'b set" where "L \ X ` space M" lemma fin_L: "finite L" using L_def distr_i by auto lemma emp_L: "L \ {}" using L_def subprob_not_empty by auto subsection\Codes and words\ abbreviation real_word :: "'b word \ bool" where "real_word w \ (set w \ L)" abbreviation k_words :: "nat \ ('b word) set" where "k_words k \ {w. length w = k \ real_word w}" lemma rw_tail: assumes "real_word w" shows "w = [] \ real_word (tl w)" by (meson assms list.set_sel(2) subset_code(1)) definition code_word_length :: "'e encoder \ 'e \ nat" where "code_word_length e l = length (e [l])" abbreviation cw_len :: "'b \ nat" where "cw_len l \ code_word_length enc l" definition code_rate :: "'e encoder \ ('a \ 'e) \ real" where "code_rate e Xo = expectation (\a. (code_word_length e ((Xo) a)))" lemma fi_pos: "i\ L \ 0 \ fi i" using simple_distributed_nonneg[OF distr_i] L_def by auto lemma (in prob_space) simp_exp_composed: assumes X: "simple_distributed M X Px" shows "expectation (\a. f (X a)) = (\x \ X`space M. f x * Px x)" using distributed_integral[OF simple_distributed[OF X], of f] simple_distributed_nonneg[OF X] lebesgue_integral_count_space_finite[OF simple_distributed_finite[OF X], of "\x. f x * Px x"] by (simp add: ac_simps) lemma cr_rw: "code_rate enc X = (\i \ X ` space M. fi i * cw_len i)" using simp_exp_composed[OF distr_i, of "cw_len"] by (simp add: mult.commute code_rate_def) abbreviation cw_len_concat :: "'b word \ nat" where "cw_len_concat w \ foldr (\x s. (cw_len x) + s) w 0" lemma cw_len_length: "cw_len_concat w = length (enc w)" proof (induction w) case Nil show ?case using real_code by simp case (Cons a w) have "cw_len_concat (a # w) = cw_len a + cw_len_concat w" by simp thus ?case using code_word_length_def real_code Cons by (metis length_append list.distinct(1) list.sel(1) list.sel(3)) qed lemma maj_fold: assumes "\l. l\L \ f l \ bound" assumes "real_word w" shows "foldr (\x s. f x + s) w 0 \ length w * bound" using assms by(induction w) (simp,fastforce) definition max_len :: "nat" where "max_len = Max ((\x. cw_len x) ` L)" lemma max_cw: "l \ L \ cw_len l \ max_len" by (simp add: max_len_def fin_L) subsection\Related to the Kraft theorem\ definition \ :: "real" where "\ = (\i\L. 1 / b ^ (cw_len i))" lemma pos_cw_len: "0 < 1 / b ^ cw_len i" using b_gt_1 by simp lemma \_pos: "0 < \" using emp_L fin_L pos_cw_len sum_pos \_def by metis lemma \_pow: "\ = (\i\L. 1 / b powr cw_len i)" using powr_realpow b_gt_1 by (simp add: \_def) lemma k_words_rel: "k_words (Suc k) = {w. (hd w \ L \ tl w \ k_words k \ w \ [])}" proof fix k show "k_words (Suc k) \ {w. (hd w \ L \ tl w \ k_words k \ w \ [] )}" (is "?l \ ?r") proof fix w assume w_kw: "w \ k_words (Suc k)" hence "real_word w" by simp hence "hd w \ L" by (metis (mono_tags) w_kw hd_in_set list.size(3) mem_Collect_eq nat.distinct(1) subset_code(1)) moreover have "length w = Suc k" using w_kw by simp moreover hence "w \ []" by auto moreover have "real_word (tl w)" using \real_word w\ calculation(3) rw_tail by auto ultimately show "w \ ?r" using w_kw by simp qed next fix k show "k_words (Suc k) \ {w. (hd w \ L \ tl w \ k_words k \ w \ [])}" proof fix w assume asm: "w \ {w. hd w \ L \ tl w \ {w. length w = k \ real_word w} \ w \ []}" hence "hd w \ L \ length (tl w) = k \ real_word (tl w)" by simp hence "real_word w" by (metis empty_iff insert_subset list.collapse list.set(1) set_simps(2) subsetI) moreover hence "length w = Suc k" using asm by auto ultimately show "w \ k_words (Suc k)" by simp qed qed lemma bij_k_words: shows "bij_betw (\wi. Cons (fst wi) (snd wi)) (L \ k_words k) (k_words (Suc k))" unfolding bij_betw_def proof fix k let ?f = "(\wi. Cons (fst wi) (snd wi))" let ?S = "L \ (k_words k)" let ?T = "k_words (Suc k)" show "inj_on ?f ?S" by (simp add: inj_on_def) show "?f`?S = ?T" proof (rule ccontr) assume "?f ` ?S \ ?T" hence "\w. w\ ?T \ w \ ?f`?S" by auto then obtain w where asm: "w\ ?T \ w \ ?f`?S" by blast hence "w = ?f (hd w,tl w)" using k_words_rel by simp moreover have "(hd w,tl w) \ ?S" using k_words_rel asm by simp ultimately have "w \ ?f`?S" by blast thus "False" using asm by simp qed qed lemma finite_k_words: "finite (k_words k)" proof (induct k) case 0 show ?case by simp case (Suc n) thus ?case using bij_k_words bij_betw_finite fin_L by blast qed lemma cartesian_product: fixes f::"('c \ real)" fixes g::"('d \ real)" assumes "finite A" assumes "finite B" shows "(\b\B. g b) * (\a\A. f a) = (\ab\A\B. f (fst ab) * g (snd ab))" using bilinear_times bilinear_sum[where h="(\x y. x * y)" and f="f" and g="g"] assms by (metis (erased, lifting) sum.cong split_beta' Groups.ab_semigroup_mult_class.mult.commute) lemma \_power: shows "\^k = (\w \ (k_words k). 1 / b^(cw_len_concat w))" proof (induct k) case 0 have "k_words 0 = {[]}" by auto thus ?case by simp next case (Suc n) have " \ ^Suc n = \ ^n * \ " by simp also have "\ = (\w \ k_words n. 1 / b^cw_len_concat w) * (\i\L. 1 / b^cw_len i)" using Suc.hyps \_def by auto also have "\ = (\wi \ L \ k_words n. 1/b^cw_len (fst wi) * (1 / b^cw_len_concat (snd wi)))" using fin_L finite_k_words cartesian_product by blast also have "\ = (\wi \ L \ k_words n. 1 / b^(cw_len_concat (snd wi) + cw_len (fst wi)))" by (metis (no_types, lifting) power_add add.commute power_one_over) also have "\ = (\wi \ L \ k_words n. 1 / b^cw_len_concat (fst wi # snd wi))" by (metis (erased, lifting) add.commute comp_apply foldr.simps(2)) also have "\ = (\w \ (k_words (Suc n)). 1 / b^(cw_len_concat w))" using sum.reindex_bij_betw [OF bij_k_words] by fastforce finally show ?case by simp qed lemma bound_len_concat: shows "w \ k_words k \ cw_len_concat w \ k * max_len" using max_cw maj_fold by blast subsection\Inequality of the kraft sum (source coding theorem, direct)\ subsubsection\Sum manipulation lemmas and McMillan theorem\ lemma sum_vimage_proof: fixes g::"nat \ real" assumes "\w. f w < bd" shows "finite S \ (\w\S. g (f w)) = (\ m=0.. S) )* g m)" (is "_ \ _ = (\ m=0.. {0..h::(nat \ real). (\m=0..y\({0..m = 0..m\{0.. F) * g (f x) + g (f x)" by (simp add: semiring_normalization_rules(2), simp add: insert) ultimately have "(\m = 0..m\{0.. real" assumes bounded: "\w. w \ S \ f w < bd" and "0 < bd" assumes finite: "finite S" shows "(\w\S. g (f w)) = (\ m=0.. S) ) * g m)" (is "?s1 = ?s2") proof - let ?ff = "(\x. if x\S then f x else 0)" let ?ss1 = "(\w\S. g (?ff w))" let ?ss2 = "(\ m=0.. S) ) * g m)" have "?s1 =?ss1" by simp moreover have"\m. ?ff -`{m} \ S = f-`{m} \ S" by auto moreover hence "?s2 = ?ss2" by simp moreover have "\w . ?ff w < bd" using assms by simp moreover hence "?ss1 = ?ss2" using sum_vimage_proof[of "?ff"] finite by blast ultimately show "?s1 = ?s2" by metis qed lemma \_rw: "(\w \ (k_words k). 1 / b^(cw_len_concat w)) = (\m=0.. ((cw_len_concat) -` {m})) * (1 / b^m))" (is "?L = ?R") proof - have "\w. w \ k_words k \ cw_len_concat w < Suc ( k * max_len)" by (simp add: bound_len_concat le_imp_less_Suc) moreover have "?R = (\m = 0.. k_words k)) * (1 / b ^ m))" by (metis Int_commute) moreover have "0 < Suc (k*max_len)" by simp ultimately show ?thesis using finite_k_words sum_vimage[where f="cw_len_concat" and g = "\i. 1/ (b^i)"] by fastforce qed definition set_of_k_words_length_m :: "nat \ nat \ 'b word set" where "set_of_k_words_length_m k m = {xk. xk \ k_words k} \ (cw_len_concat)-`{m}" lemma am_inj_code: "inj_on enc ((cw_len_concat)-`{m})" (is "inj_on _ ?s") using inj_on_def[of enc "?s"] real_code by (metis option.inject) lemma img_inc: "enc`cw_len_concat-`{m} \ {bl. length bl = m}" using cw_len_length by auto lemma bool_lists_card: "card {bl::bool list. length bl = m} = b^m" using card_lists_length_eq[of "UNIV::bool set"] by (simp add: b_val) lemma bool_list_fin: "finite {bl::bool list. length bl = m}" using finite_lists_length_eq[of "UNIV::bool set"] by (simp add: b_val) lemma set_of_k_words_bound: shows "card (set_of_k_words_length_m k m) \ b^m" (is "?c \ ?b") proof - have card_w_len_m_bound: "card (cw_len_concat-`{m}) \ b^m" by (metis (no_types, lifting) am_inj_code bool_list_fin bool_lists_card card_image card_mono img_inc of_nat_le_iff) have "set_of_k_words_length_m k m \ (cw_len_concat)-`{m}" by (simp add: set_of_k_words_length_m_def) hence "card (set_of_k_words_length_m k m) \ card ((cw_len_concat)-`{m})" by (metis (no_types, lifting) am_inj_code bool_list_fin card.infinite card_0_eq card_image card_mono empty_iff finite_subset img_inc inf_img_fin_dom) thus ?thesis using card_w_len_m_bound by simp qed lemma empty_set_k_words: assumes "0 < k" shows "set_of_k_words_length_m k 0 = {}" proof(rule ccontr) assume "\ set_of_k_words_length_m k 0 = {}" hence "\x. x \ set_of_k_words_length_m k 0" by auto then obtain x where x_def: "x \ set_of_k_words_length_m k 0" by auto hence "x \ []" unfolding set_of_k_words_length_m_def using assms by auto moreover have "cw_len_concat (hd x#tl x) = cw_len_concat (tl x) + cw_len (hd x)" by (metis add.commute comp_apply foldr.simps(2)) moreover have "enc [(hd x)] \ []" using assms real_code by blast moreover hence "0 < cw_len (hd x)" unfolding code_word_length_def by simp ultimately have "x \ set_of_k_words_length_m k 0" by (simp add:set_of_k_words_length_m_def) thus "False" using x_def by simp qed lemma \_rw2: assumes "0 < k" shows "(\m=0.. (k * max_len)" proof - have "(\m=1.. (\m=1..m. (card (set_of_k_words_length_m k m))/b^m)" "\m. b^m /b^m"] by simp moreover have"(\m=1..m=1..m=1..m = 1.. k * max_len" by (metis One_nat_def card_atLeastLessThan card_eq_sum diff_Suc_Suc real_of_card) thus ?thesis using empty_set_k_words assms by (simp add: sum_shift_lb_Suc0_0_upt split: if_split_asm) qed lemma \_power_bound : assumes "0 < k" shows " \^k \ k * max_len" using assms \_power \_rw \_rw2 by (simp add: set_of_k_words_length_m_def) theorem McMillan : shows "\ \ 1" proof - have ineq: "\k. 0 < k \ \ \ root k k * root k max_len" using \_pos \_power_bound by (metis (no_types, opaque_lifting) not_less of_nat_0_le_iff of_nat_mult power_strict_mono real_root_mult real_root_pos_pos_le real_root_pos_unique real_root_power) hence "0 < max_len \ (\k. root k k * root k max_len) \ 1" by (auto intro!: tendsto_eq_intros LIMSEQ_root LIMSEQ_root_const) moreover have "\n\1. \ \ root n n * root n max_len" using ineq by simp moreover have "max_len = 0 \ \ \ 1" using ineq by fastforce ultimately show " \ \ 1" using LIMSEQ_le_const by blast qed lemma entropy_rw: "\(X) = -(\i \ L. fi i * log b (fi i))" using entropy_simple_distributed[OF distr_i] by (simp add: L_def) subsubsection\Technical lemmas about the logarithm\ lemma log_mult_ext3: "0 \ x \ 0 < y \ 0 < z \ x * log b (x*y*z) = x * log b (x*y) + x * log b z" by(cases "x=0")(simp add: log_mult_eq abs_of_pos distrib_left less_eq_real_def)+ lemma log_mult_ext2: "0 \ x \ 0 < y \ x * log b (x*y) = x * log b x + x * log b y" using log_mult_ext3[where y=1] by simp subsubsection \KL divergence and properties\ definition KL_div ::"'b set \ ('b \ real) \ ('b \ real) \ real" where "KL_div S a d = (\ i \ S. a i * log b (a i / d i))" lemma KL_div_mul: assumes "0 < d" "d \ 1" assumes "\i. i\S \ 0 \ a i" assumes "\i. i\S \ 0 < e i" shows "KL_div S a e \ KL_div S a (\i. e i / d)" unfolding KL_div_def proof - { fix i assume "i\S" hence "a i / (e i / d) \ a i / e i" using assms by (metis (no_types) div_by_1 frac_le less_imp_triv not_less) - hence "log b (a i / (e i / d)) \ log b (a i / e i)" using assms(1) - by (metis (full_types) b_gt_1 divide_divide_eq_left inverse_divide le_less_linear log_le - log_neg_const order_refl times_divide_eq_right zero_less_mult_iff) + hence "log b (a i / (e i / d)) \ log b (a i / e i)" using assms + by (smt (verit, best) Transcendental.log_mono \i \ S\ b_gt_1 diff_divide_distrib divide_pos_pos) } thus "(\i\S. a i * log b (a i / (e i / d))) \ (\i\S. a i * log b (a i / e i))" by (meson mult_left_mono assms sum_mono) qed lemma KL_div_pos: fixes a e::"'b \ real" assumes fin: "finite S" assumes nemp: "S \ {}" assumes non_null: "\i. i\S \ 0 < a i" "\i. i\ S \ 0 < e i" assumes sum_a_one: "(\ i \ S. a i) = 1" assumes sum_c_one: "(\ i \ S. e i) = 1" shows "0 \ KL_div S a e" unfolding KL_div_def proof - let ?f = "\i. e i / a i" have f_pos: "\i. i\S \ 0 < ?f i" using non_null by simp have a_pos: "\i. i\ S \ 0 \ a i" using non_null by (simp add: order.strict_implies_order) have "- log b (\i\S. a i * e i / a i) \ (\i\S. a i * - log b (e i / a i))" using convex_on_sum[OF fin nemp minus_log_convex[OF b_gt_1] sum_a_one a_pos, of "\i. e i / a i"] f_pos by simp also have "-log b (\i\S. a i * e i / a i) = -log b (\i\S. e i)" proof - from non_null(1) have "\i. i \ S \ a i * e i / a i = e i" by force thus ?thesis by simp qed finally have "0 \ (\i\S. a i * - log b (e i / a i))" by (simp add: sum_c_one) thus "0 \ (\i\S. a i * log b (a i / e i))" using b_gt_1 log_divide non_null by simp qed lemma KL_div_pos_emp: "0 \ KL_div {} a e" by (simp add: KL_div_def) lemma KL_div_pos_gen: fixes a d::"'b \ real" assumes fin: "finite S" assumes non_null: "\i. i\S \ 0 < a i" "\i. i\ S \ 0 < d i" assumes sum_a_one: "(\ i \ S. a i) = 1" assumes sum_d_one: "(\ i \ S. d i) = 1" shows "0 \ KL_div S a d" using KL_div_pos KL_div_pos_emp assms by metis theorem KL_div_pos2: fixes a d::"'b \ real" assumes fin: "finite S" assumes non_null: "\i. i\S \ 0 \ a i" "\i. i\ S \ 0 < d i" assumes sum_a_one: "(\ i \ S. a i) = 1" assumes sum_c_one: "(\ i \ S. d i) = 1" shows "0 \ KL_div S a d" proof - have "S = (S \ {i. 0 < a i}) \ (S \ {i. 0 = a i})" using non_null(1) by fastforce moreover have "(S \ {i. 0 < a i}) \ (S \ {i. 0 = a i}) = {}" by auto ultimately have eq: "KL_div S a d = KL_div (S \ {i. 0 < a i}) a d + KL_div (S \ {i. 0 = a i}) a d" unfolding KL_div_def by (metis (mono_tags, lifting) fin finite_Un sum.union_disjoint) have "KL_div (S \ {i. 0 = a i}) a d = 0" unfolding KL_div_def by simp hence "KL_div S a d = KL_div (S \ {i. 0 < a i}) a d" using eq by simp moreover have "0 \ KL_div (S \ {i. 0 < a i}) a d" proof(cases "(S \ {i. 0 < a i}) = {}") case True thus ?thesis unfolding KL_div_def by simp next case False let ?c = "\i. d i / (\j \(S \ {i. 0 < a i}). d j)" have 1: "(\i. i \ S \ {i. 0 < a i} \ 0 < a i)" by simp have 2: "(\i. i \ S \ {i. 0 < a i} \ 0 < ?c i)" by (metis False IntD1 divide_pos_pos fin finite_Int non_null(2) sum_pos) have 3: "(\i\ (S \ {i. 0 < a i}). a i) = 1" using sum.cong[of S, of S, of "(\x. if x \ {i. 0 < a i} then a x else 0)", of a] sum.inter_restrict[OF fin, of a] non_null(1) sum_a_one by fastforce have "(\i\S \ {j. 0 < a j}. ?c i) = (\i\S \ {j. 0 < a j}. d i) / (\i\S \ {j. 0 < a j}. d i)" by (metis sum_divide_distrib) hence 5: "(\i\S \ {j. 0 < a j}. ?c i) = 1" using 2 False by force hence "0 \ KL_div (S \ {j. 0 < a j}) a ?c" using KL_div_pos_gen[ OF finite_Int[OF disjI1, of S, of "{j. 0 < a j}"], of a, of ?c ] 1 2 3 by (metis fin) have fstdb: "0 < (\i\S \ {i. 0 < a i}. d i)" using non_null(2) False by (metis Int_Collect fin finite_Int sum_pos) have 6: "0 \ KL_div (S \ {i. 0 < a i}) a (\i. d i / (\i\(S \ {i. 0 < a i}). d i))" using 2 3 5 KL_div_pos_gen[ OF finite_Int[OF disjI1, OF fin], of "{i. 0 < a i}", of "a", of "?c" ] by simp hence "KL_div (S \ {j. 0 < a j}) a (\i. d i / (\i\(S \ {i. 0 < a i}). d i)) \ KL_div (S \ {j. 0 < a j}) a d" using non_null sum.inter_restrict[OF fin, of d, of "{i. 0 < a i}"] sum_mono[of S, of "(\x. if x \ {i. 0 < a i} then d x else 0)", of d] non_null(2) sum_c_one non_null(2) fstdb KL_div_mul by force moreover have "0 \ KL_div (S \ {j. 0 < a j}) a (\i. d i / (\i\(S \ {i. 0 < a i}). d i))" using KL_div_pos_gen[ OF finite_Int[OF disjI1, OF fin]] using 2 3 5 by fastforce ultimately show "0 \ KL_div (S \ {j. 0 < a j}) a d" by simp qed ultimately show ?thesis by simp qed lemma sum_div_1: fixes f::"'b \ 'c::field" assumes "(\i\A. f i) \ 0" shows "(\i\A. f i / (\j\A. f j)) = 1" by (metis (no_types) assms right_inverse_eq sum_divide_distrib) theorem rate_lower_bound: shows "\(X) \ code_rate enc X" proof - let ?cr = "code_rate enc X" let ?r = "(\i. 1 / ((b powr cw_len i) * \))" have pos_pi: "\i. i \ L \ 0 \ fi i" using fi_pos by simp { fix i assume "i \ L" hence "fi i * (log b (1 / (1 / b powr (cw_len i))) + log b (fi i)) = fi i * log b (fi i / (1 / b powr (cw_len i)))" using log_mult_ext2 [OF pos_pi, of i] b_gt_1 by simp (simp add: algebra_simps) } hence eqpi: "\i. i\ L \ fi i * (log b (1 / (1 / b powr (cw_len i))) + log b (fi i)) = fi i * log b (fi i / (1 / b powr (cw_len i)))" by simp have sum_one_L: "(\ i \ L. fi i) = 1" using simple_distributed_sum_space[OF distr_i] by (simp add: L_def) { fix i assume "i \ L" hence h1: "0 \ fi i" using pos_pi by blast have h2: "0 < \ / (1/b powr cw_len i)" using b_gt_1 \_pos by auto have h3: "0 < 1 / \" using \_pos by simp have "fi i * log b (fi i * \ / (1/b powr cw_len i) * (1/ \)) = fi i * log b (fi i * \ / (1/b powr cw_len i)) + fi i * log b (1/ \)" using log_mult_ext3[OF h1 h2 h3] by (metis times_divide_eq_right) } hence big_eq: "\i. i \ L \ fi i * log b (fi i * \ / (1/b powr cw_len i) * (1 / \)) = fi i * log b (fi i * \ / (1/b powr cw_len i)) + fi i * log b (1 / \)" by (simp add: inverse_eq_divide) have 1: "?cr - \(X) = (\i \ L. fi i * cw_len i) + (\i \ L. fi i * log b (fi i))" using \_def entropy_rw cr_rw L_def by simp also have 2: "(\i\L. fi i * cw_len i) = (\i \ L. fi i * (-log b (1/(b powr (cw_len i)))))" using b_gt_1 log_divide by simp also have "\ = -1 * (\i \ L. fi i * (log b (1/(b powr (cw_len i)))))" using sum_distrib_left[of "-1" "(\i. fi i * (- 1 * log b (1 / b powr (cw_len i))))" L] by simp finally have "?cr - \(X) = -(\i \ L. fi i * log b (1/b powr cw_len i)) + (\i \ L. fi i * log b (fi i))" by simp have "?cr - \(X) = (\i \ L. fi i * ((log b (1/ (1/(b powr (cw_len i))))) + log b (fi i)))" using b_gt_1 1 by (simp add: distrib_left sum.distrib) also have "\ = (\i \ L. fi i *((log b (fi i / (1/(b powr (cw_len i)))))))" using Finite_Cartesian_Product.sum_cong_aux[OF eqpi] by simp also from big_eq have "\ = (\i\L. fi i * (log b (fi i * \ / (1 / b powr (cw_len i))))) + (\i \ L. fi i) * log b (1/ \)" using \_pos by (simp add: sum_distrib_right sum.distrib) also have "\ = (\i\L. fi i * (log b (fi i * \ / (1 / b powr (cw_len i))))) - log b (\)" using \_pos by (simp add: log_inverse_eq divide_inverse sum_one_L) also have "\ = (\ i \ L. fi i * log b (fi i / ?r i)) - log b (\)" by (metis (mono_tags, opaque_lifting) divide_divide_eq_left divide_divide_eq_right) also have "\ = KL_div L fi ?r - log b ( \)" using b_gt_1 \_pos log_inverse KL_div_def by simp also have "\ = KL_div L fi ?r + log b (1 / \)" using log_inverse b_val \_pos by (simp add: inverse_eq_divide) finally have code_ent_kl_log: "?cr - \(X) = KL_div L fi ?r + log b (1 / \)" by simp have "(\i\L. ?r i) = 1" using sum_div_1[of "\i. 1 / (b powr (cw_len i))"] \_pos \_pow by simp moreover have "\i. 0 < ?r i" using b_gt_1 \_pos by simp moreover have "(\i\L. fi i) = 1" using sum_one_L by simp ultimately have "0 \ KL_div L fi ?r" using KL_div_pos2[OF fin_L fi_pos] by simp hence "log b (1 / \) \ ?cr - \(X)" using code_ent_kl_log by simp moreover from McMillan have "0 \ log b (1 / \)" using \_pos by (simp add: b_gt_1) ultimately show ?thesis by simp qed end end