Theory Expander_Graphs.Pseudorandom_Objects_Expander_Walks

section ‹Expander Walks as Pseudorandom Objects›

theory Pseudorandom_Objects_Expander_Walks
  imports
    Universal_Hash_Families.Pseudorandom_Objects
    Expander_Graphs.Expander_Graphs_Strongly_Explicit
begin

unbundle intro_cong_syntax
hide_const (open) Quantum.T
hide_fact (open) SN_Orders.of_nat_mono
hide_fact Missing_Ring.mult_pos_pos

definition expander_pro ::
  "nat ⇒ real ⇒ ('a,'b) pseudorandom_object_scheme ⇒ (nat ⇒ 'a) pseudorandom_object"
  where "expander_pro l Λ S = (
    let e = see_standard (pro_size S) Λ in
      ⦇ pro_last = see_size e * see_degree e^(l-1) - 1,
        pro_select = (λi j. pro_select S (see_sample_walk e (l-1) i ! j mod pro_size S)) ⦈
    )"

context
  fixes l :: nat
  fixes Λ :: real
  fixes S :: "('a,'b) pseudorandom_object_scheme"
  assumes l_gt_0: "l > 0"
  assumes Λ_gt_0: "Λ > 0"
begin

private definition e where "e = see_standard (pro_size S) Λ"

private lemma expander_pro_alt: "expander_pro l Λ S = ⦇ pro_last = see_size e * see_degree e^(l-1) - 1,
        pro_select = (λi j. pro_select S (see_sample_walk e (l-1) i ! j mod pro_size S)) ⦈"
  unfolding expander_pro_def e_def[symmetric] by (auto simp:Let_def)

private lemmas see_standard = see_standard [OF pro_size_gt_0[where S="S"] Λ_gt_0]

interpretation E: regular_graph "graph_of e"
  using see_standard(1) unfolding is_expander_def e_def by auto

private lemma e_deg_gt_0: "see_degree e > 0"
  unfolding e_def see_standard by simp

private lemma e_size_gt_0: "see_size e > 0"
  unfolding e_def using see_standard pro_size_gt_0 by simp

private lemma expander_sample_size: "pro_size (expander_pro l Λ S) =  see_size e * see_degree e^(l-1)"
  using e_deg_gt_0 e_size_gt_0 unfolding expander_pro_alt pro_size_def by simp

private lemma sample_pro_expander_walks:
  defines "R ≡ map_pmf (λxs i. pro_select S (xs ! i mod pro_size S))
    (pmf_of_multiset (walks (graph_of e) l))"
  shows "sample_pro (expander_pro l Λ S) = R"
proof -
  let ?S = "{..<see_size e * see_degree e ^ (l-1)}"
  let ?T = "(map_pmf (see_sample_walk e (l-1)) (pmf_of_set ?S))"

  have "0 ∈ ?S"
    using e_size_gt_0 e_deg_gt_0  by auto
  hence "?S ≠ {}"
    by blast
  hence "?T = pmf_of_multiset {#see_sample_walk e (l-1) i. i ∈# mset_set ?S#}"
    by (subst map_pmf_of_set) simp_all
  also have "... = pmf_of_multiset (walks' (graph_of e) (l-1))"
    by (subst see_sample_walk) auto
  also have "... = pmf_of_multiset (walks (graph_of e) l)"
    unfolding walks_def using l_gt_0 by (cases l, simp_all)
  finally have 0:"?T = pmf_of_multiset (walks (graph_of e) l)"
    by simp

  have "sample_pro (expander_pro l Λ S) = map_pmf (λxs j. pro_select S (xs ! j mod pro_size S)) ?T"
    unfolding expander_sample_size sample_pro_alt unfolding map_pmf_comp expander_pro_alt by simp
  also have "... = R" unfolding 0 R_def by simp
  finally show ?thesis by simp
qed

lemma expander_pro_range: "pro_select (expander_pro l Λ S) i j ∈ pro_set S"
  unfolding expander_pro_alt by (simp add:pro_select_in_set)

lemma expander_uniform_property:
  assumes "i < l"
  shows "map_pmf (λw. w i) (sample_pro (expander_pro l Λ S)) = sample_pro S" (is "?L = ?R")
proof -
  have "?L = map_pmf (λx. pro_select S (x mod pro_size S)) (map_pmf (λxs. (xs ! i)) (pmf_of_multiset (walks (graph_of e) l)))"
    unfolding sample_pro_expander_walks by (simp add: map_pmf_comp)
  also have "... = map_pmf (λx. pro_select S (x mod pro_size S)) (pmf_of_set (verts (graph_of e)))"
    unfolding E.uniform_property[OF assms] by simp
  also have "... = ?R"
    using pro_size_gt_0 unfolding sample_pro_alt
    by (intro map_pmf_cong) (simp_all add:e_def graph_of_def see_standard select_def)
  finally show ?thesis
    by simp
qed

lemma expander_kl_chernoff_bound:
  assumes "measure (sample_pro S) {w. T w} ≤ μ"
  assumes "γ ≤ 1" "μ + Λ * (1-μ) ≤ γ" "μ ≤ 1"
  shows "measure (sample_pro (expander_pro l Λ S)) {w. real (card {i ∈ {..<l}. T (w i)}) ≥ γ*l}
    ≤ exp (- real l * KL_div γ (μ + Λ*(1-μ)))" (is "?L ≤ ?R")
proof (cases "measure (sample_pro S) {w. T w} > 0")
  case True
  let ?w = "pmf_of_multiset (walks (graph_of e) l)"
  define V where "V = {v∈ verts (graph_of e). T (pro_select S v)} "
  define ν where "ν = measure (sample_pro S) {w. T w}"

  have ν_gt_0: "ν > 0" unfolding ν_def using True by simp
  have ν_le_1: "ν ≤ 1" unfolding ν_def by simp
  have ν_le_μ: "ν ≤ μ" unfolding ν_def using assms(1) by simp

  have 0: "card {i ∈ {..<l}. T (pro_select S (w ! i mod pro_size S))} = card {i ∈ {..<l}. w ! i ∈ V}"
    if "w  ∈ set_pmf (pmf_of_multiset (walks (graph_of e) l))" for w
  proof -
    have a0: "w ∈# walks (graph_of e) l" using that E.walks_nonempty by simp
    have a1:"w ! i ∈ verts (graph_of e)" if "i < l" for i
      using that E.set_walks_3[OF a0] by auto
    moreover have "w ! i mod pro_size S = w ! i" if "i < l" for i
      using a1[OF that] see_standard(2) e_def by (simp add:graph_of_def)
    ultimately show ?thesis
      unfolding V_def
      by (intro arg_cong[where f="card"] restr_Collect_cong) auto
  qed

  have 1:"E.Λ⇩a ≤ Λ"
    using see_standard(1) unfolding is_expander_def e_def by simp

  have 2: "V ⊆ verts (graph_of e)"
    unfolding V_def by simp

  have "ν = measure (pmf_of_set {..<pro_size S}) ({v. T (pro_select S v)})"
    unfolding ν_def sample_pro_alt by simp
  also have "... = real (card ({v∈{..<pro_size S}. T (pro_select S v)})) / real (pro_size S)"
    using pro_size_gt_0 by (subst measure_pmf_of_set) (auto simp add:Int_def)
  also have "... = real (card V) / card (verts (graph_of e))"
    unfolding V_def graph_of_def e_def using see_standard by (simp add:Int_commute)
  finally have ν_eq: "ν = real (card V) / card (verts (graph_of e))"
    by simp

  have 3: "0 < ν + E.Λ⇩a * (1 - ν)"
    using ν_le_1 by (intro add_pos_nonneg ν_gt_0 mult_nonneg_nonneg E.Λ_ge_0) auto

  have "ν + E.Λ⇩a * (1 - ν) = ν * (1 - E.Λ⇩a) + E.Λ⇩a" by (simp add:algebra_simps)
  also have "... ≤ μ * (1- E.Λ⇩a) + E.Λ⇩a" using E.Λ_le_1
    by (intro add_mono mult_right_mono ν_le_μ) auto
  also have "... = μ + E.Λ⇩a * (1 - μ)" by (simp add:algebra_simps)
  also have "... ≤ μ + Λ * (1 - μ)" using assms(4) by (intro add_mono mult_right_mono 1) auto
  finally have 4: "ν + E.Λ⇩a * (1 - ν) ≤ μ + Λ * (1 - μ)" by simp

  have 5: "ν + E.Λ⇩a*(1-ν) ≤ γ" using 4 assms(3) by simp

  have "?L = measure ?w {y. γ * real l ≤ real (card {i ∈ {..<l}. T (pro_select S (y ! i mod pro_size S))})}"
    unfolding sample_pro_expander_walks by simp
  also have "... = measure ?w {y. γ * real l ≤ real (card {i ∈ {..<l}. y ! i ∈ V})}"
    using 0 by (intro measure_pmf_cong) (simp)
  also have "... ≤ exp (- real l * KL_div γ (ν + E.Λ⇩a*(1-ν)) )"
    using assms(2) 3 5 unfolding ν_eq by (intro E.kl_chernoff_property l_gt_0 2) auto
  also have "... ≤ exp (- real l * KL_div γ (μ + Λ*(1-μ)))"
    using l_gt_0 by (intro iffD2[OF exp_le_cancel_iff] iffD2[OF mult_le_cancel_left_neg]
      KL_div_mono_right[OF disjI2] conjI 3 4 assms(2,3)) auto
  finally show ?thesis by simp
next
  case False
  hence 0:"measure (sample_pro S) {w. T w} = 0" using zero_less_measure_iff by blast
  hence 1:"T w = False" if "w ∈ pro_set S" for w using that measure_pmf_posI by force

  have "μ + Λ * (1-μ) > 0"
  proof (cases "μ = 0")
    case True then show ?thesis using Λ_gt_0 by auto
  next
    case False
    then show ?thesis using assms(1,4) 0 Λ_gt_0
      by (intro add_pos_nonneg mult_nonneg_nonneg) simp_all
  qed
  hence "γ > 0" using assms(3) by auto
  hence 2:"γ*real l > 0" using l_gt_0 by simp

  let ?w = "pmf_of_multiset (walks (graph_of e) l)"

  have "?L = measure ?w {y. γ*real l≤ card {i ∈ {..<l}. T (pro_select S (y ! i mod pro_size S))}}"
    unfolding sample_pro_expander_walks by simp
  also have "... = 0" using pro_select_in_set 2 by (subst 1) auto
  also have "... ≤ ?R" by simp
  finally show ?thesis by simp
qed

lemma expander_chernoff_bound_one_sided:
  assumes "AE x in sample_pro S. f x ∈ {0,1::real}"
  assumes "(∫x. f x ∂sample_pro S) ≤ μ" "l > 0" "γ ≥ 0"
  shows "measure (expander_pro l Λ S) {w. (∑i<l. f (w i))/l-μ≥γ+Λ} ≤ exp (- 2 * real l * γ^2)"
    (is "?L ≤ ?R")
proof -
  let ?w = "sample_pro (expander_pro l Λ S)"
  define T where "T x = (f x=1)" for x

  have 1: "indicator {w. T w} x = f x" if "x ∈ pro_set S" for x
  proof -
    have "f x ∈ {0,1}" using assms(1) that unfolding AE_measure_pmf_iff by simp
    thus ?thesis unfolding T_def by auto
  qed

  have "measure S {w. T w} = (∫x. indicator {w. T w} x ∂S)" by simp
  also have "... = (∫x. f x ∂S)" using 1 by (intro integral_cong_AE AE_pmfI) auto
  also have "... ≤ μ" using assms(2) by simp
  finally have 0: "measure S {w. T w} ≤ μ" by simp

  hence μ_ge_0: "μ ≥ 0" using measure_nonneg order.trans by blast

  have cases: "(γ=0 ⟹ p) ⟹ (γ+Λ+μ > 1  ⟹ p) ⟹ (γ+Λ+μ ≤ 1 ∧ γ > 0 ⟹ p) ⟹ p" for p
    using assms(4) by argo

  have "?L = measure ?w {w. (γ+Λ+μ)*l ≤ (∑i<l. f (w i))}"
    using assms(3) by (intro measure_pmf_cong) (auto simp:field_simps)
  also have "... = measure ?w {w. (γ+Λ+μ)*l ≤ card {i ∈ {..<l}. T (w i)}}"
  proof (rule measure_pmf_cong)
    fix ω
    assume "ω ∈ pro_set (expander_pro l Λ S)"
    hence "ω x ∈ pro_set S" for x using expander_pro_range set_sample_pro by (metis image_iff)
    hence "(∑i<l. f (ω i)) = (∑i<l. indicator {w. T w} (ω i))" using 1 by (intro sum.cong) auto
    also have "... = card {i ∈ {..<l}. T (ω i)}" unfolding indicator_def by (auto simp:Int_def)
    finally have "(∑i<l. f (ω i)) = (card {i ∈ {..<l}. T (ω i)})" by simp
    thus "(ω ∈ {w. (γ+Λ+μ)*l ≤ (∑i<l. f (w i))})=(ω ∈ {w. (γ+Λ+μ)*l≤card {i ∈ {..<l}. T (w i)}})"
      by simp
  qed
  also have "... ≤ ?R" (is "?L1 ≤ _")
  proof (rule cases)
    assume "γ = 0" thus "?thesis" by simp
  next
    assume a:"γ + Λ + μ ≤ 1 ∧ 0 < γ"
    hence μ_lt_1: "μ < 1" using assms(4) Λ_gt_0 by simp
    hence μ_le_1: "μ ≤ 1" by simp
    have "μ + Λ * (1 - μ) ≤ μ + Λ * 1" using μ_ge_0 Λ_gt_0 by (intro add_mono mult_left_mono) auto
    also have "... < γ+Λ+μ" using assms(4) a by simp
    finally have b:"μ + Λ * (1 - μ) < γ +Λ +μ" by simp
    hence "μ + Λ * (1 - μ) < 1" using a by simp
    moreover have "μ + Λ * (1 - μ) > 0" using μ_lt_1
      by (intro add_nonneg_pos μ_ge_0 mult_pos_pos Λ_gt_0) simp
    ultimately have c: "μ + Λ * (1 - μ) ∈ {0<..<1}" by simp
    have d: " γ + Λ + μ ∈ {0..1}" using a b c by simp
    have "?L1 ≤ exp (- real l * KL_div (γ+Λ+μ) (μ + Λ*(1-μ)))"
      using a b by (intro expander_kl_chernoff_bound μ_le_1 0) auto
    also have "... ≤ exp (- real l * (2 * ((γ+Λ+μ)- (μ + Λ*(1-μ)))^2))"
      by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono_neg KL_div_lower_bound c d) simp
    also have "... ≤ exp (- real l * (2 * (γ^2)))"
      using assms(4) μ_lt_1 Λ_gt_0 μ_ge_0
      by (intro iffD2[OF exp_le_cancel_iff] mult_left_mono_neg[where c="-real l"] mult_left_mono
          power_mono) simp_all
    also have "... = ?R" by simp
    finally show "?L1 ≤ ?R" by simp
  next
    assume a:"1 < γ + Λ + μ"
    have "(γ+Λ+μ)* real l > real (card {i ∈ {..<l}. (x i)})" for x
    proof -
      have "real (card {i ∈ {..<l}. (x i)}) ≤ card {..<l}" by (intro of_nat_mono card_mono) auto
      also have "... = real l" by simp
      also have "... < (γ+Λ+μ)* real l" using assms(3) a by simp
      finally show ?thesis by simp
    qed
    hence "?L1 = 0" unfolding not_le[symmetric] by auto
    also have "... ≤ ?R" by simp
    finally show "?L1 ≤ ?R" by simp
  qed
  finally show ?thesis by simp
qed

lemma expander_chernoff_bound:
  assumes "AE x in sample_pro S. f x ∈ {0,1::real}" "l > 0" "γ ≥ 0"
  defines "μ ≡ (∫x. f x ∂sample_pro S)"
  shows "measure (expander_pro l Λ S) {w. ¦(∑i<l. f (w i))/l-μ¦≥γ+Λ} ≤ 2*exp (- 2 * real l * γ^2)"
    (is "?L ≤ ?R")
proof -
  let ?w = "sample_pro (expander_pro l Λ S)"
  have "?L ≤ measure ?w {w. (∑i<l. f (w i))/l-μ≥γ+Λ} + measure ?w {w. (∑i<l. f (w i))/l-μ≤-(γ+Λ)}"
    by (intro pmf_add) auto
  also have "... ≤ exp (-2*real l*γ^2) + measure ?w {w. -((∑i<l. f (w i))/l-μ)≥(γ+Λ)}"
    using assms by (intro add_mono expander_chernoff_bound_one_sided) (auto simp:algebra_simps)
  also have "... ≤ exp (-2*real l*γ^2) + measure ?w {w. ((∑i<l. 1-f (w i))/l-(1-μ))≥(γ+Λ)}"
    using assms(2) by (auto simp: sum_subtractf field_simps)
  also have "... ≤ exp (-2*real l*γ^2) + exp (-2*real l*γ^2)"
    using assms by (intro add_mono expander_chernoff_bound_one_sided) auto
  also have "... = ?R" by simp
  finally show ?thesis by simp
qed

lemma expander_pro_size:
  "pro_size (expander_pro l Λ S) = pro_size S * (16 ^ ((l-1) * nat ⌈ln Λ / ln (19 / 20)⌉))"
  (is "?L = ?R")
proof -
  have "?L = see_size e * see_degree e ^ (l - 1)"
    unfolding expander_sample_size by simp
  also have "... = pro_size S * (16 ^ nat ⌈ln Λ / ln (19 / 20)⌉) ^ (l - 1)"
    using see_standard unfolding e_def by simp
  also have "... = pro_size S * (16 ^ ((l-1) * nat ⌈ln Λ / ln (19 / 20)⌉))"
    unfolding power_mult[symmetric] by (simp add:ac_simps)
  finally show ?thesis
    by simp
qed

end

open_bundle expander_pseudorandom_object_syntax
begin
notation expander_pro (‹ℰ›)
end

unbundle no intro_cong_syntax

end