Theory Expander_Graphs_Walks

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