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