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
bundle expander_pseudorandom_object_notation
begin
notation expander_pro ("ℰ")
end
bundle no_expander_pseudorandom_object_notation
begin
no_notation expander_pro ("ℰ")
end
unbundle expander_pseudorandom_object_notation
unbundle no_intro_cong_syntax
end