section ‹Random Walks\label{sec:random_walks}› theory Expander_Graphs_Walks imports Expander_Graphs_Algebra Expander_Graphs_Eigenvalues Expander_Graphs_TTS Constructive_Chernoff_Bound begin unbundle intro_cong_syntax no_notation Matrix.vec_index (infixl "$" 100) hide_const Matrix.vec_index hide_const Matrix.vec no_notation Matrix.scalar_prod (infix "∙" 70) fun walks' :: "('a,'b) pre_digraph ⇒ nat ⇒ ('a list) multiset" where "walks' G 0 = image_mset (λx. [x]) (mset_set (verts G))" | "walks' G (Suc n) = concat_mset {#{#w @[z].z∈# vertices_from G (last w)#}. w ∈# walks' G n#}" definition "walks G l = (case l of 0 ⇒ {#[]#} | Suc pl ⇒ walks' G pl)" lemma Union_image_mono: "(⋀x. x ∈ A ⟹ f x ⊆ g x) ⟹ ⋃ (f ` A) ⊆ ⋃ (g ` A)" by auto context fin_digraph begin lemma count_walks': assumes "set xs ⊆ verts G" assumes "length xs = l+1" shows "count (walks' G l) xs = (∏i ∈ {..<l}. count (edges G) (xs ! i, xs ! (i+1)))" proof - have a:"xs ≠ []" using assms(2) by auto have "count (walks' G (length xs-1)) xs = (∏i<length xs -1. count (edges G) (xs ! i, xs ! (i + 1)))" using a assms(1) proof (induction xs rule:rev_nonempty_induct) case (single x) hence "x ∈ verts G" by simp hence "count {#[x]. x ∈# mset_set (verts G)#} [x] = 1" by (subst count_image_mset_inj, auto simp add:inj_def) then show ?case by simp next case (snoc x xs) have set_xs: "set xs ⊆ verts G" using snoc by simp define l where "l = length xs - 1" have l_xs: "length xs = l + 1" unfolding l_def using snoc by simp have "count (walks' G (length (xs @ [x]) - 1)) (xs @ [x]) = (∑ys∈#walks' G l. count {#ys @ [z]. z ∈# vertices_from G (last ys)#} (xs @ [x]))" by (simp add:l_xs count_concat_mset image_mset.compositionality comp_def) also have "... = (∑ys∈#walks' G l. (if ys = xs then count {#xs @ [z]. z ∈# vertices_from G (last xs)#} (xs @ [x]) else 0))" by (intro arg_cong[where f="sum_mset"] image_mset_cong) (auto intro!: count_image_mset_0_triv) also have "... = (∑ys∈#walks' G l.(if ys=xs then count (vertices_from G (last xs)) x else 0))" by (subst count_image_mset_inj, auto simp add:inj_def) also have "... = count (walks' G l) xs * count (vertices_from G (last xs)) x" by (subst sum_mset_delta, simp) also have "... = count (walks' G l) xs * count (edges G) (last xs, x)" unfolding vertices_from_def count_mset_exp image_mset_filter_mset_swap[symmetric] filter_filter_mset by (simp add:prod_eq_iff) also have "... = count (walks' G l) xs * count (edges G) ((xs@[x])!l, (xs@[x])!(l+1))" using snoc(1) unfolding l_def nth_append last_conv_nth[OF snoc(1)] by simp also have "... = (∏i<l+1. count (edges G) ((xs@[x])!i, (xs@[x])!(i+1)))" unfolding l_def snoc(2)[OF set_xs] by (simp add:nth_append) finally have "count (walks' G (length (xs @ [x]) - 1)) (xs @ [x]) = (∏i<length (xs@[x]) - 1. count (edges G) ((xs@[x])!i, (xs@[x])!(i+1)))" unfolding l_def using snoc(1) by simp then show ?case by simp qed moreover have "l = length xs - 1" using a assms by simp ultimately show ?thesis by simp qed lemma count_walks: assumes "set xs ⊆ verts G" assumes "length xs = l" "l > 0" shows "count (walks G l) xs = (∏i ∈ {..<l-1}. count (edges G) (xs ! i, xs ! (i+1)))" using assms unfolding walks_def by (cases l, auto simp add:count_walks') lemma set_walks': "set_mset (walks' G l) ⊆ {xs. set xs ⊆ verts G ∧ length xs = (l+1)}" proof (induction l) case 0 then show ?case by auto next case (Suc l) have "set_mset (walks' G (Suc l)) = (⋃x∈set_mset (walks' G l). (λz. x @ [z]) ` set_mset (vertices_from G (last x)))" by (simp add:set_mset_concat_mset) also have "... ⊆ (⋃x∈{xs. set xs ⊆ verts G ∧ length xs = l + 1}. (λz. x @ [z]) ` set_mset (vertices_from G (last x)))" by (intro Union_mono image_mono Suc) also have "... ⊆ (⋃x∈{xs. set xs ⊆ verts G ∧ length xs = l + 1}. (λz. x @ [z]) ` verts G)" by (intro Union_image_mono image_mono set_mset_vertices_from) also have "... ⊆ {xs. set xs ⊆ verts G ∧ length xs = (Suc l + 1)}" by (intro subsetI) auto finally show ?case by simp qed lemma set_walks: "set_mset (walks G l) ⊆ {xs. set xs ⊆ verts G ∧ length xs = l}" unfolding walks_def using set_walks' by (cases l, auto) lemma set_walks_2: assumes "xs ∈# walks' G l" shows "set xs ⊆ verts G" "xs ≠ []" proof - have a:"xs ∈ set_mset (walks' G l)" using assms by simp thus "set xs ⊆ verts G" using set_walks' by auto have "length xs ≠ 0" using set_walks' a by fastforce thus "xs ≠ []" by simp qed lemma set_walks_3: assumes "xs ∈# walks G l" shows "set xs ⊆ verts G" "length xs = l" using set_walks assms by auto end lemma measure_pmf_of_multiset: assumes "A ≠ {#}" shows "measure (pmf_of_multiset A) S = real (size (filter_mset (λx. x ∈ S) A)) / size A" (is "?L = ?R") proof - have "sum (count A) (S ∩ set_mset A) = size (filter_mset (λx. x ∈ S ∩ set_mset A) A)" by (intro sum_count_2) simp also have "... = size (filter_mset (λx. x ∈ S) A)" by (intro arg_cong[where f="size"] filter_mset_cong) auto finally have a: "sum (count A) (S ∩ set_mset A) = size (filter_mset (λx. x ∈ S) A)" by simp have "?L = measure (pmf_of_multiset A) (S ∩ set_mset A)" using assms by (intro measure_eq_AE AE_pmfI) auto also have "... = sum (pmf (pmf_of_multiset A)) (S ∩ set_mset A)" by (intro measure_measure_pmf_finite) simp also have "... = (∑x ∈ S ∩ set_mset A. count A x / size A)" using assms by (intro sum.cong, auto) also have "... = (∑x ∈ S ∩ set_mset A. count A x) / size A" by (simp add:sum_divide_distrib) also have "... = ?R" using a by simp finally show ?thesis by simp qed lemma pmf_of_multiset_image_mset: assumes "A ≠ {#}" shows "pmf_of_multiset (image_mset f A) = map_pmf f (pmf_of_multiset A)" using assms by (intro pmf_eqI) (simp add:pmf_map measure_pmf_of_multiset count_mset_exp image_mset_filter_mset_swap[symmetric]) context regular_graph begin lemma size_walks': "size (walks' G l) = card (verts G) * d^l" proof (induction l) case 0 then show ?case by simp next case (Suc l) have a:"out_degree G (last x) = d" if "x ∈# walks' G l" for x proof - have "last x ∈ verts G" using set_walks_2 that by fastforce thus ?thesis using reg by simp qed have "size (walks' G (Suc l)) = (∑x∈#walks' G l. out_degree G (last x))" by (simp add:size_concat_mset image_mset.compositionality comp_def verts_from_alt out_degree_def) also have "... = (∑x∈#walks' G l. d)" by (intro arg_cong[where f="sum_mset"] image_mset_cong a) simp also have "... = size (walks' G l) * d" by simp also have "... = card (verts G) * d^(Suc l)" using Suc by simp finally show ?case by simp qed lemma size_walks: "size (walks G l) = (if l > 0 then n * d^(l-1) else 1)" using size_walks' unfolding walks_def n_def by (cases l, auto) lemma walks_nonempty: "walks G l ≠ {#}" proof - have "size (walks G l) > 0" unfolding size_walks using d_gt_0 n_gt_0 by auto thus "walks G l ≠ {#}" by auto qed end context regular_graph_tts begin lemma g_step_remains_orth: assumes "g_inner f (λ_. 1) = 0" shows "g_inner (g_step f) (λ_. 1) = 0" (is "?L = ?R") proof - have "?L = (A *v (χ i. f (enum_verts i))) ∙ 1" unfolding g_inner_conv g_step_conv one_vec_def by simp also have "... = (χ i. f (enum_verts i)) ∙ 1" by (intro markov_orth_inv markov) also have "... = g_inner f (λ_. 1)" unfolding g_inner_conv one_vec_def by simp also have "... = 0" using assms by simp finally show ?thesis by simp qed lemma spec_bound: "spec_bound A Λ⇩_{a}" proof - have "norm (A *v v) ≤ Λ⇩_{a}* norm v" if "v ∙ 1 = (0::real)" for v::"real^'n" unfolding Λ⇩_{e}_eq_Λ by (intro γ⇩_{a}_real_bound that) thus ?thesis unfolding spec_bound_def using Λ_ge_0 by auto qed text ‹A spectral expansion rule that does not require orthogonality of the vector for the stationary distribution:› lemma expansionD3: "¦g_inner f (g_step f)¦ ≤ Λ⇩_{a}* g_norm f^2 + (1-Λ⇩_{a}) * g_inner f (λ_. 1)^2 / n" (is "?L ≤ ?R") proof - define v where "v = (χ i. f (enum_verts i))" define v1 :: "real^ 'n" where "v1 = ((v ∙ 1) / n) *⇩_{R}1" define v2 :: "real^ 'n" where "v2 = v - v1" have v_eq: "v = v1 + v2" unfolding v2_def by simp have 0: "A *v v1 = v1" unfolding v1_def using markov_apply[OF markov] by (simp add:algebra_simps) have 1: "v1 v* A = v1" unfolding v1_def using markov_apply[OF markov] by (simp add:algebra_simps scaleR_vector_matrix_assoc) have "v2 ∙ 1 = v ∙ 1 - v1 ∙ 1" unfolding v2_def by (simp add:algebra_simps) also have "... = v ∙ 1 - v ∙ 1 * real CARD('n) / real n" unfolding v1_def by (simp add:inner_1_1) also have "... = 0 " using verts_non_empty unfolding card n_def by simp finally have 4:"v2 ∙ 1 = 0" by simp hence 2: "v1 ∙ v2 = 0" unfolding v1_def by (simp add:inner_commute) define f2 where "f2 i = v2 $ (enum_verts_inv i)" for i have f2_def: "v2 = (χ i. f2 (enum_verts i))" unfolding f2_def Rep_inverse by simp have 6: "g_inner f2 (λ_. 1) = 0" unfolding g_inner_conv f2_def[symmetric] one_vec_def[symmetric] 4 by simp have "¦v2 ∙ (A *v v2)¦ = ¦g_inner f2 (g_step f2)¦" unfolding f2_def g_inner_conv g_step_conv by simp also have "... ≤ Λ⇩_{a}* (g_norm f2)⇧^{2}" by (intro expansionD1 6) also have "... = Λ⇩_{a}* (norm v2)^2" unfolding g_norm_conv f2_def by simp finally have 5:"¦v2 ∙ (A *v v2)¦ ≤ Λ⇩_{a}* (norm v2)⇧^{2}" by simp have 3: "norm (1 :: real^'n)^2 = n" unfolding power2_norm_eq_inner inner_1_1 card n_def by presburger have "?L = ¦v ∙ (A *v v)¦" unfolding g_inner_conv g_step_conv v_def by simp also have "... = ¦v1 ∙ (A *v v1) + v2 ∙ (A *v v1) + v1 ∙ (A *v v2) + v2 ∙ (A *v v2)¦" unfolding v_eq by (simp add:algebra_simps) also have "... = ¦v1 ∙ v1 + v2 ∙ v1 + v1 ∙ v2 + v2 ∙ (A *v v2)¦" unfolding dot_lmul_matrix[where x="v1",symmetric] 0 1 by simp also have "... = ¦v1 ∙ v1 + v2 ∙ (A *v v2)¦" using 2 by (simp add:inner_commute) also have "... ≤ ¦norm v1^2¦ + ¦v2 ∙ (A *v v2)¦" unfolding power2_norm_eq_inner by (intro abs_triangle_ineq) also have "... ≤ norm v1^2 + Λ⇩_{a}* norm v2^2" by (intro add_mono 5) auto also have "... = Λ⇩_{a}* (norm v1^2 + norm v2^2) + (1 - Λ⇩_{a}) * norm v1^2" by (simp add:algebra_simps) also have "... = Λ⇩_{a}* norm v^2 + (1 - Λ⇩_{a}) * norm v1^2" unfolding v_eq pythagoras[OF 2] by simp also have "... = Λ⇩_{a}* norm v^2 + ((1 - Λ⇩_{a})) * ((v ∙ 1)^2*n)/n^2" unfolding v1_def by (simp add:power_divide power_mult_distrib 3) also have "... = Λ⇩_{a}* norm v^2 + ((1 - Λ⇩_{a})/n) * (v ∙ 1)^2" by (simp add:power2_eq_square) also have "... = ?R" unfolding g_norm_conv g_inner_conv v_def one_vec_def by (simp add:field_simps) finally show ?thesis by simp qed definition ind_mat where "ind_mat S = diag (ind_vec (enum_verts -` S))" lemma walk_distr: "measure (pmf_of_multiset (walks G l)) {ω. (∀i<l. ω ! i ∈ S i)} = foldl (λx M. M *v x) stat (intersperse A (map (λi. ind_mat (S i)) [0..<l]))∙1" (is "?L = ?R") proof (cases "l > 0") case True let ?n = "real n" let ?d = "real d" let ?W = "{(w::'a list). set w ⊆ verts G ∧ length w = l}" let ?V = "{(w::'n list). length w = l}" have a: "set_mset (walks G l) ⊆ ?W" using set_walks by auto have b: "finite ?W" by (intro finite_lists_length_eq) auto define lp where "lp = l - 1" define xs where "xs = map (λi. ind_mat (S i)) [0..<l]" have "xs ≠ []" unfolding xs_def using True by simp then obtain xh xt where xh_xt: "xh#xt=xs" by (cases xs, auto) have "length xs = l" unfolding xs_def by simp hence len_xt: "length xt = lp" using True unfolding xh_xt[symmetric] lp_def by simp have "xh = xs ! 0" unfolding xh_xt[symmetric] by simp also have "... = ind_mat (S 0)" using True unfolding xs_def by simp finally have xh_eq: "xh = ind_mat (S 0)" by simp have inj_map_enum_verts: "inj_on (map enum_verts) ?V" using bij_betw_imp_inj_on[OF enum_verts] inj_on_subset by (intro inj_on_mapI) auto have "card ?W = card (verts G)^l" by (intro card_lists_length_eq) simp also have "... = card {w. set w ⊆ (UNIV :: 'n set) ∧ length w = l}" unfolding card[symmetric] by (intro card_lists_length_eq[symmetric]) simp also have "... = card ?V" by (intro arg_cong[where f="card"]) auto also have "... = card (map enum_verts ` ?V)" by (intro card_image[symmetric] inj_map_enum_verts) finally have "card ?W = card (map enum_verts ` ?V)" by simp hence "map enum_verts ` ?V = ?W" using bij_betw_apply[OF enum_verts] by (intro card_subset_eq b image_subsetI) auto hence bij_map_enum_verts: "bij_betw (map enum_verts) ?V ?W" using inj_map_enum_verts unfolding bij_betw_def by auto have "?L = size {# w ∈# walks G l. ∀i<l. w ! i ∈ S i #} / (?n * ?d^(l-1))" using True unfolding size_walks measure_pmf_of_multiset[OF walks_nonempty] by simp also have "... = (∑w∈?W. real (count (walks G l) w) * of_bool (∀i<l. w!i ∈ S i))/(?n*?d^(l-1))" unfolding size_filter_mset_conv sum_mset_conv_2[OF a b] by simp also have "... = (∑w∈?W. (∏i<l-1. real (count (edges G) (w!i,w!(i+1)))) * (∏i<l. of_bool (w!i ∈ S i)))/(?n*?d^(l-1))" using True by (intro sum.cong arg_cong2[where f="(/)"]) (auto simp add: count_walks) also have "... = (∑w∈?W. (∏i<l-1. real (count (edges G) (w!i,w!(i+1)))/?d)*(∏i<l. of_bool (w!i ∈ S i)))/?n" using True unfolding prod_dividef by (simp add:sum_divide_distrib algebra_simps) also have "... = (∑w∈?V. (∏i<l-1. count (edges G) (map enum_verts w!i,map enum_verts w!(i+1)) / ?d) * (∏i<l. of_bool (map enum_verts w!i ∈ S i)))/?n" by (intro sum.reindex_bij_betw[symmetric] arg_cong2[where f="(/)"] refl bij_map_enum_verts) also have "... = (∑w∈?V. (∏i<lp. A $ w!(i+1) $ w!i) * (∏i<Suc lp. of_bool(enum_verts (w!i) ∈ S i)))/?n" unfolding A_def lp_def using True by simp also have "... = (∑w∈?V. (∏i<lp. A $ w!(i+1) $ w!i) * (∏i∈insert 0 (Suc ` {..<lp}). of_bool(enum_verts (w!i) ∈ S i)))/?n" using lessThan_Suc_eq_insert_0 by (intro sum.cong arg_cong2[where f="(/)"] arg_cong2[where f="(*)"] prod.cong) auto also have "... = (∑w∈?V. (∏i<lp. of_bool(enum_verts (w!(i+1))∈S(i+1))* A$ w!(i+1) $ w!i) * of_bool(enum_verts(w!0)∈S 0))/?n" by (simp add:prod.reindex algebra_simps prod.distrib) also have "... = (∑w∈?V. (∏i<lp. (ind_mat (S (i+1))**A) $ w!(i+1) $ w!i) * of_bool(enum_verts (w!0)∈S 0))/?n" unfolding diag_def ind_vec_def matrix_matrix_mult_def ind_mat_def by (intro sum.cong arg_cong2[where f="(/)"] arg_cong2[where f="(*)"] prod.cong refl) (simp add:if_distrib if_distribR sum.If_cases) also have "... = (∑w∈?V. (∏i<lp. (xs!(i+1)**A) $ w!(i+1) $ w!i) * of_bool(enum_verts (w!0)∈S 0))/?n" unfolding xs_def lp_def True by (intro sum.cong arg_cong2[where f="(/)"] arg_cong2[where f="(*)"] prod.cong refl) auto also have "... = (∑w∈?V. (∏i<lp. (xt ! i ** A) $ w!(i+1) $ w!i) * of_bool(enum_verts (w!0)∈S 0))/?n" unfolding xh_xt[symmetric] by auto also have "... = (∑w∈?V. (∏i<lp. (xt!i**A)$ w!(i+1) $ w!i)*(ind_mat(S 0)*v stat) $w!0)" using n_def unfolding matrix_vector_mult_def diag_def stat_def ind_vec_def ind_mat_def card by (simp add:sum.If_cases if_distrib if_distribR sum_divide_distrib) also have "... = (∑w∈?V. (∏i<lp. (xt ! i ** A) $ w!(i+1) $ w!i) * (xh *v stat) $ w ! 0)" unfolding xh_eq by simp also have "... = foldl (λx M. M *v x) (xh *v stat) (map (λx. x ** A) xt) ∙ 1" using True unfolding foldl_matrix_mult_expand_2 by (simp add:len_xt lp_def) also have "... = foldl (λx M. M *v (A *v x)) (xh *v stat) xt ∙ 1" by (simp add: matrix_vector_mul_assoc foldl_map) also have "... = foldl (λx M. M *v x) stat (intersperse A (xh#xt)) ∙ 1" by (subst foldl_intersperse_2, simp) also have "... = ?R" unfolding xh_xt xs_def by simp finally show ?thesis by simp next case False hence "l = 0" by simp thus ?thesis unfolding stat_def by (simp add: inner_1_1) qed lemma hitting_property: assumes "S ⊆ verts G" assumes "I ⊆ {..<l}" defines "μ ≡ real (card S) / card (verts G)" shows "measure (pmf_of_multiset (walks G l)) {w. set (nths w I) ⊆ S} ≤ (μ+Λ⇩_{a}*(1-μ))^card I" (is "?L ≤ ?R") proof - define T where "T = (λi. if i ∈ I then S else UNIV)" have 0: "ind_mat UNIV = mat 1" unfolding ind_mat_def diag_def ind_vec_def Finite_Cartesian_Product.mat_def by vector have Λ_range: "Λ⇩_{a}∈ {0..1}" using Λ_ge_0 Λ_le_1 by simp have "S ⊆ range enum_verts" using assms(1) enum_verts unfolding bij_betw_def by simp moreover have "inj enum_verts" using bij_betw_imp_inj_on[OF enum_verts] by simp ultimately have μ_alt: "μ = real (card (enum_verts -` S)) / CARD ('n)" unfolding μ_def card by (subst card_vimage_inj) auto have "?L = measure (pmf_of_multiset (walks G l)) {w. ∀i<l. w ! i ∈ T i}" using walks_nonempty set_walks_3 unfolding T_def set_nths by (intro measure_eq_AE AE_pmfI) auto also have "... = foldl (λx M. M *v x) stat (intersperse A (map (λi. (if i ∈ I then ind_mat S else mat 1)) [0..<l])) ∙ 1" unfolding walk_distr T_def by (simp add:if_distrib if_distribR 0 cong:if_cong) also have "... ≤ ?R" unfolding μ_alt ind_mat_def by (intro hitting_property_alg_2[OF Λ_range assms(2) spec_bound markov]) finally show ?thesis by simp qed lemma uniform_property: assumes "i < l" "x ∈ verts G" shows "measure (pmf_of_multiset (walks G l)) {w. w ! i = x} = 1/real (card (verts G))" (is "?L = ?R") proof - obtain xi where xi_def: "enum_verts xi = x" using assms(2) bij_betw_imp_surj_on[OF enum_verts] by force define T where "T = (λj. if j = i then {x} else UNIV)" have "diag (ind_vec UNIV) = mat 1" unfolding diag_def ind_vec_def Finite_Cartesian_Product.mat_def by vector moreover have "enum_verts -` {x} = {xi}" using bij_betw_imp_inj_on[OF enum_verts] unfolding vimage_def xi_def[symmetric] by (auto simp add:inj_on_def) ultimately have 0: "ind_mat (T j) = (if j = i then diag (ind_vec {xi}) else mat 1)" for j unfolding T_def ind_mat_def by (cases "j = i", auto) have "?L = measure (pmf_of_multiset (walks G l)) {w. ∀j < l. w ! j ∈ T j}" unfolding T_def using assms(1) by simp also have "... = foldl (λx M. M *v x) stat (intersperse A (map (λj. ind_mat (T j)) [0..<l])) ∙ 1" unfolding walk_distr by simp also have "... = 1/CARD('n)" unfolding 0 uniform_property_alg[OF assms(1) markov] by simp also have "... = ?R" unfolding card by simp finally show ?thesis by simp qed end context regular_graph begin lemmas expansionD3 = regular_graph_tts.expansionD3[OF eg_tts_1, internalize_sort "'n :: finite", OF _ regular_graph_axioms, unfolded remove_finite_premise, cancel_type_definition, OF verts_non_empty] lemmas g_step_remains_orth = regular_graph_tts.g_step_remains_orth[OF eg_tts_1, internalize_sort "'n :: finite", OF _ regular_graph_axioms, unfolded remove_finite_premise, cancel_type_definition, OF verts_non_empty] lemmas hitting_property = regular_graph_tts.hitting_property[OF eg_tts_1, internalize_sort "'n :: finite", OF _ regular_graph_axioms, unfolded remove_finite_premise, cancel_type_definition, OF verts_non_empty] lemmas uniform_property_2 = regular_graph_tts.uniform_property[OF eg_tts_1, internalize_sort "'n :: finite", OF _ regular_graph_axioms, unfolded remove_finite_premise, cancel_type_definition, OF verts_non_empty] theorem uniform_property: assumes "i < l" shows "map_pmf (λw. w ! i) (pmf_of_multiset (walks G l)) = pmf_of_set (verts G)" (is "?L = ?R") proof (rule pmf_eqI) fix x :: "'a" have a:"measure (pmf_of_multiset (walks G l)) {w. w ! i = x} = 0" (is "?L1 = ?R1") if "x ∉ verts G" proof - have "?L1 ≤ measure (pmf_of_multiset (walks G l)) {w. set w ⊆ verts G ∧ x ∈ set w}" using walks_nonempty set_walks_3 assms(1) by (intro pmf_mono) auto also have "... ≤ measure (pmf_of_multiset (walks G l)) {}" using that by (intro pmf_mono) auto also have "... = 0" by simp finally have "?L1 ≤ 0" by simp thus ?thesis using measure_le_0_iff by blast qed have "pmf ?L x = measure (pmf_of_multiset (walks G l)) {w. w ! i = x}" unfolding pmf_map by (simp add:vimage_def) also have "... = indicator (verts G) x/real (card (verts G))" using uniform_property_2[OF assms(1)] a by (cases "x ∈ verts G", auto) also have "... = pmf ?R x" using verts_non_empty by (intro pmf_of_set[symmetric]) auto finally show "pmf ?L x = pmf ?R x" by simp qed lemma uniform_property_gen: fixes S :: "'a set" assumes "S ⊆ verts G" "i < l" defines "μ ≡ real (card S) / card (verts G)" shows "measure (pmf_of_multiset (walks G l)) {w. w ! i ∈ S} = μ" (is "?L = ?R") proof - have "?L = measure (map_pmf (λw. w ! i) (pmf_of_multiset (walks G l))) S" unfolding measure_map_pmf by (simp add:vimage_def) also have "... = measure (pmf_of_set (verts G)) S" unfolding uniform_property[OF assms(2)] by simp also have "... = ?R" using verts_non_empty Int_absorb1[OF assms(1)] unfolding μ_def by (subst measure_pmf_of_set) auto finally show ?thesis by simp qed theorem kl_chernoff_property: assumes "l > 0" assumes "S ⊆ verts G" defines "μ ≡ real (card S) / card (verts G)" assumes "γ ≤ 1" "μ + Λ⇩_{a}* (1-μ) ∈ {0<..γ}" shows "measure (pmf_of_multiset (walks G l)) {w. real (card {i ∈ {..<l}. w ! i ∈ S}) ≥ γ*l} ≤ exp (- real l * KL_div γ (μ+Λ⇩_{a}*(1-μ)))" (is "?L ≤ ?R") proof - let ?δ = "(∑i<l. μ+Λ⇩_{a}*(1-μ))/l" have a: "measure (pmf_of_multiset (walks G l)) {w. ∀i∈T. w ! i ∈ S} ≤ (μ + Λ⇩_{a}*(1-μ)) ^ card T" (is "?L1 ≤ ?R1") if "T ⊆ {..<l}" for T proof - have "?L1 = measure (pmf_of_multiset (walks G l)) {w. set (nths w T) ⊆ S}" unfolding set_nths setcompr_eq_image using that set_walks_3 walks_nonempty by (intro measure_eq_AE AE_pmfI) (auto simp add:image_subset_iff) also have "... ≤ ?R1" unfolding μ_def by (intro hitting_property[OF assms(2) that]) finally show ?thesis by simp qed have "?L ≤ exp ( - real l * KL_div γ ?δ)" using assms(1,4,5) a by (intro impagliazzo_kabanets_pmf) simp_all also have "... = ?R" by simp finally show ?thesis by simp qed end unbundle no_intro_cong_syntax end