Theory 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

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)) ⦈
    )"

open_bundle expander_pseudorandom_object_syntax
begin
notation expander_pro (‹ℰ›)
end

unbundle expander_pseudorandom_object_syntax

context
  fixes l :: nat
  fixes Λ :: real
  fixes P :: "'a pseudorandom_object"
  assumes l_gt_0: "l > 0"
  assumes Λ_gt_0: "Λ > 0"
begin

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

private lemma expander_pro_alt:
  "expander_pro l Λ P =
    ⦇ pro_last = see_size e * see_degree e^(l-1) - 1,
      pro_select = (λi j. pro_select P (see_sample_walk e (l-1) i ! j mod pro_size P)) ⦈"
  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="P"] Λ_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 (ℰ l Λ P) =  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 P (xs ! i mod pro_size P))
    (pmf_of_multiset (walks (graph_of e) l))"
  shows "sample_pro (expander_pro l Λ P) = 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 Λ P) = map_pmf (λxs j. pro_select P (xs ! j mod pro_size P)) ?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 Λ P) i j ∈ pro_set P"
  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 Λ P)) = sample_pro P" (is "?L = ?R")
proof -
  have "?L = map_pmf (λx. pro_select P (x mod pro_size P)) (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 P (x mod pro_size P)) (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 P) {w. T w} ≤ μ"
  assumes "c ≤ 1" "μ + Λ * (1-μ) ≤ c" "μ ≤ 1"
  shows "measure (sample_pro (expander_pro l Λ P)) {w. real (card {i ∈ {..<l}. T (w i)}) ≥ c*l}
    ≤ exp (- real l * KL_div c (μ + Λ*(1-μ)))" (is "?L ≤ ?R")
proof (cases "measure (sample_pro P) {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 P v)} "
  define ν where "ν = measure (sample_pro P) {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 P (w ! i mod pro_size P))} = 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 P = 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 P}) ({v. T (pro_select P v)})"
    unfolding ν_def sample_pro_alt by simp
  also have "… = real (card ({v∈{..<pro_size P}. T (pro_select P v)})) / real (pro_size P)"
    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-ν) ≤ c" using 4 assms(3) by simp

  have "?L = measure ?w {y. c * real l ≤ real (card {i ∈ {..<l}. T (pro_select P (y ! i mod pro_size P))})}"
    unfolding sample_pro_expander_walks by simp
  also have "… = measure ?w {y. c * real l ≤ real (card {i ∈ {..<l}. y ! i ∈ V})}"
    using 0 by (intro measure_pmf_cong) (simp)
  also have "… ≤ exp (- real l * KL_div c (ν + 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 c (μ + Λ*(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 P) {w. T w} = 0" using zero_less_measure_iff by blast
  hence 1:"T w = False" if "w ∈ pro_set P" 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 "c > 0" using assms(3) by auto
  hence 2:"c*real l > 0" using l_gt_0 by simp

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

  have "?L = measure ?w {y. c*real l≤ card {i ∈ {..<l}. T (pro_select P (y ! i mod pro_size P))}}"
    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_pro_size:
  "pro_size (expander_pro l Λ P) = pro_size P * (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 P * (16 ^ nat ⌈ln Λ / ln (19 / 20)⌉) ^ (l - 1)"
    using see_standard unfolding e_def by simp
  also have "… = pro_size P * (16 ^ ((l-1) * nat ⌈ln Λ / ln (19 / 20)⌉))"
    unfolding power_mult[symmetric] by (simp add:ac_simps)
  finally show ?thesis
    by simp
qed

context
  fixes γ :: real
  assumes γ_ge_0: "γ ≥ 0"
begin

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

  have 1: "indicator {w. T w} x = f x" if "x ∈ pro_set P" 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 P {w. T w} = (∫x. indicator {w. T w} x ∂P)" by simp
  also have "… = (∫x. f x ∂P)" using 1 by (intro integral_cong_AE AE_pmfI) auto
  also have "… ≤ μ" using assms(2) by simp
  finally have 0: "measure P {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 γ_ge_0 by argo

  have "?L = measure ?w {w. (γ+Λ+μ)*l ≤ (∑i<l. f (w i))}"
    using l_gt_0 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 Λ P)"
    hence "ω x ∈ pro_set P" 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 γ_ge_0 Λ_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 γ_ge_0 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 γ_ge_0 μ_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 l_gt_0 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_1:
  assumes "AE x in sample_pro P. f x ∈ {0,1::real}"
  defines "μ ≡ (∫x. f x ∂sample_pro P)"
  shows "measure (ℰ l Λ P) {w. ¦(∑i<l. f (w i))/l-μ¦≥γ+Λ} ≤ 2*exp (- 2 * real l * γ^2)"
    (is "?L ≤ ?R")
proof -
  let ?w = "sample_pro (expander_pro l Λ P)"
  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 l_gt_0 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_chernoff_bound:
  assumes "AE x in sample_pro P. f x ∈ {0,1::real}"
  defines "μ ≡ measure_pmf.expectation P f"
  shows "𝒫(ω in ℰ l Λ P. ¦(∑i<l. f (ω i))/l-μ¦≥γ+Λ) ≤ 2*exp (- 2 * real l * γ^2)"
    (is "?L ≤ ?R")
proof -
  have "?L = measure (expander_pro l Λ P) {w. ¦(∑i<l. f (w i))/l-μ¦≥γ+Λ}" by simp
  also have "… ≤ ?R" unfolding μ_def by (intro expander_chernoff_bound_1 assms(1))
  finally show ?thesis by simp
qed

lemma expander_chernoff_bound_2:
  assumes "AE x in sample_pro P. f x ∈ {0,1::real}"
  defines "μ ≡ measure_pmf.expectation P f"
  shows "𝒫(ω in sample_pro (ℰ l Λ P). ¦(∑i<l. f (ω i))-real l*μ¦≥real l*(γ+Λ)) ≤ 2*exp (- 2 * real l * γ^2)"
    (is "?L ≤ ?R")
proof -
  have "?L = measure (expander_pro l Λ P) {w. ¦(∑i<l. f (w i))/l-μ¦≥γ+Λ}"
    using l_gt_0 by (intro arg_cong2[where f="measure"] refl Collect_cong) (simp add: field_simps)
  also have "… ≤ ?R" unfolding μ_def by (intro expander_chernoff_bound_1 assms(1))
  finally show ?thesis by simp
qed

end

end

unbundle no intro_cong_syntax

end