diff --git a/thys/Gauss_Sums/Polya_Vinogradov.thy b/thys/Gauss_Sums/Polya_Vinogradov.thy --- a/thys/Gauss_Sums/Polya_Vinogradov.thy +++ b/thys/Gauss_Sums/Polya_Vinogradov.thy @@ -1,873 +1,849 @@ (* File: Polya_Vinogradov.thy Authors: Rodrigo Raya, EPFL; Manuel Eberl, TUM The Pólya--Vinogradov inequality, both the general case and the stronger variant for primitive characters. *) section \The Pólya--Vinogradov Inequality\ theory Polya_Vinogradov imports Gauss_Sums "Dirichlet_Series.Divisor_Count" begin unbundle no_vec_lambda_notation subsection \The case of primitive characters\ text \ We first prove a stronger variant of the Pólya--Vinogradov inequality for primitive characters. The fully general variant will then simply be a corollary of this. First, we need some bounds on logarithms, exponentials, and the harmonic numbers: \ -(* TODO: Move? *) -lemma ln_add_one_self_less_self: - fixes x :: real - assumes "x > 0" - shows "ln (1 + x) < x" +lemma exp_1_less_powr: + assumes "x > (0::real)" + shows "exp 1 < (1 + 1 / x) powr (x+1)" proof - - have "0 \ x" "0 < x" "exp x > 0" "1+x > 0" using assms by simp+ - have "1 + x < 1 + x + x\<^sup>2 / 2" - using \0 < x\ by auto - also have "\ \ exp x" - using exp_lower_Taylor_quadratic[OF \0 \ x\] by blast - finally have "1 + x < exp (x)" by blast - then have "ln (1 + x) < ln (exp (x))" - using ln_less_cancel_iff[OF \1+x > 0\ \exp(x) > 0\] by auto - also have "\ = x" using ln_exp by blast - finally show ?thesis by auto -qed - -lemma exp_1_bounds: - assumes "x > (0::real)" - shows "exp 1 > (1 + 1 / x) powr x" and "exp 1 < (1 + 1 / x) powr (x+1)" -proof - - have "ln (1 + 1 / x) < 1 / x" - using ln_add_one_self_less_self assms by simp - thus "exp 1 > (1 + 1 / x) powr x" using assms - by (simp add: field_simps powr_def) -next have "1 < (x + 1) * ln ((x + 1) / x)" (is "_ < ?f x") proof (rule DERIV_neg_imp_decreasing_at_top[where ?f = ?f]) fix t assume t: "x \ t" have "(?f has_field_derivative (ln (1 + 1 / t) - 1 / t)) (at t)" using t assms by (auto intro!: derivative_eq_intros simp:divide_simps) moreover have "ln (1 + 1 / t) - 1 / t < 0" using ln_add_one_self_less_self[of "1 / t"] t assms by auto ultimately show "\y. ((\t. (t + 1) * ln ((t + 1) / t)) has_real_derivative y) (at t) \ y < 0" by blast qed real_asymp thus "exp 1 < (1 + 1 / x) powr (x + 1)" using assms by (simp add: powr_def field_simps) qed lemma harm_aux_ineq_1: fixes k :: real assumes "k > 1" shows "1 / k < ln (1 + 1 / (k - 1))" proof - have "k-1 > 0" \k > 0\ using assms by simp+ - from exp_1_bounds(2)[OF \k-1 > 0\] - have "exp 1 < (1 + 1 / (k - 1)) powr k" by simp + from exp_1_less_powr[OF \k-1 > 0\] + have eless: "exp 1 < (1 + 1 / (k - 1)) powr k" by simp then have n_z: "(1 + 1 / (k - 1)) powr k > 0" using assms not_exp_less_zero by auto have "(1::real) = ln (exp(1))" using ln_exp by auto also have "\ < ln ((1 + 1 / (k - 1)) powr k)" - using ln_less_cancel_iff[of "exp(1)",simplified,OF \(1 + 1 / (k - 1)) powr k > 0\] - exp_1_bounds[OF \k - 1 > 0\] by simp + by (meson eless dual_order.strict_trans exp_gt_zero ln_less_cancel_iff) also have "\ = k * ln (1 + 1 / (k - 1))" using ln_powr n_z by simp finally have "1 < k * ln (1 + 1 / (k - 1))" by blast then show ?thesis using assms by (simp add: field_simps) qed lemma harm_aux_ineq_2_lemma: assumes "x \ (0::real)" shows "1 < (x + 1) * ln (1 + 2 / (2 * x + 1))" proof - have "0 < ln (1+2/(2*x+1)) - 1 / (x + 1)" (is "_ < ?f x") proof (rule DERIV_neg_imp_decreasing_at_top[where ?f = ?f]) fix t assume t: "x \ t" from assms t have "3 + 8 * t + 4 * t^2 > 0" by (intro add_pos_nonneg) auto hence *: "3 + 8 * t + 4 * t^2 \ 0" by auto have "(?f has_field_derivative (-1 / ((1 + t)^2 * (3 + 8 * t + 4 * t ^ 2)))) (at t)" apply (insert assms t *, (rule derivative_eq_intros refl | simp add: add_pos_pos)+) apply (auto simp: divide_simps) apply (auto simp: algebra_simps power2_eq_square) done moreover have "-1 / ((1 + t)^2 * (3 + 8 * t + 4 * t^2)) < 0" using t assms by (intro divide_neg_pos mult_pos_pos add_pos_nonneg) auto ultimately show "\y. (?f has_real_derivative y) (at t) \ y < 0" by blast qed real_asymp thus "1 < (x + 1) * ln (1+2/(2*x+1))" using assms by (simp add: field_simps) qed lemma harm_aux_ineq_2: fixes k :: real assumes "k \ 1" shows "1 / (k + 1) < ln (1 + 2 / (2 * k + 1))" proof - have "k > 0" using assms by auto have "1 < (k + 1) * ln (1 + 2 / (2 * k + 1))" using harm_aux_ineq_2_lemma assms by simp then show ?thesis by (simp add: \0 < k\ add_pos_pos mult.commute mult_imp_div_pos_less) qed lemma nat_0_1_induct [case_names 0 1 step]: assumes "P 0" "P 1" "\n. n \ 1 \ P n \ P (Suc n)" shows "P n" proof (induction n rule: less_induct) case (less n) show ?case using assms(3)[OF _ less.IH[of "n - 1"]] by (cases "n \ 1") (insert assms(1-2),auto simp: eval_nat_numeral le_Suc_eq) qed lemma harm_less_ln: fixes m :: nat assumes "m > 0" shows "harm m < ln (2 * m + 1)" using assms proof (induct m rule: nat_0_1_induct) case 0 then show ?case by blast next case 1 have "harm 1 = (1::real)" unfolding harm_def by simp have "harm 1 < ln (3::real)" by (subst \harm 1 = 1\,subst ln3_gt_1,simp) then show ?case by simp next case (step n) have "harm (n+1) = harm n + 1/(n+1)" by ((subst Suc_eq_plus1[symmetric])+,subst harm_Suc,subst inverse_eq_divide,blast) also have "\ < ln (real (2 * n + 1)) + 1/(n+1)" using step(1-2) by auto also have "\ < ln (real (2 * n + 1)) + ln (1+2/(2*n+1))" proof - from step(1) have "real n \ 1" by simp have "1 / real (n + 1) < ln (1 + 2 / real (2 * n + 1))" using harm_aux_ineq_2[OF \1 \ (real n)\] by (simp add: add.commute) then show ?thesis by auto qed also have "\ = ln ((2 * n + 1) * (1+2/(2*n+1)))" by (rule ln_mult[symmetric],simp,simp add: field_simps) also have "\ = ln (2*(n+1)+1)" proof - have "(2 * n + 1) * (1+2/(2*n+1)) = 2*(n+1)+1" by (simp add: field_simps) then show ?thesis by presburger qed finally show ?case by simp qed (* END TODO *) text\Theorem 8.21\ theorem (in primitive_dchar) polya_vinogradov_inequality_primitive: fixes x :: nat shows "norm (\m=1..x. \ m) < sqrt n * ln n" proof - define \ :: complex where "\ = gauss_sum 1 div sqrt n" have \_mod: "norm \ = 1" using fourier_primitive(2) by (simp add: \_def) { fix m have "\ m = (\ div sqrt n) * (\k = 1..n. (cnj (\ k)) * unity_root n (-m*k))" using fourier_primitive(1)[of m] \_def by blast} note chi_expr = this have "(\m = 1..x. \(m)) = (\m = 1..x. (\ div sqrt n) * (\k = 1..n. (cnj (\ k)) * unity_root n (-m*k)))" by(rule sum.cong[OF refl]) (use chi_expr in blast) also have "\ = (\m = 1..x. (\k = 1..n. (\ div sqrt n) * ((cnj (\ k)) * unity_root n (-m*k))))" by (rule sum.cong,simp,simp add: sum_distrib_left) also have "\ = (\k = 1..n. (\m = 1..x. (\ div sqrt n) * ((cnj (\ k)) * unity_root n (-m*k))))" by (rule sum.swap) also have "\ = (\k = 1..n. (\ div sqrt n) * (cnj (\ k) * (\m = 1..x. unity_root n (-m*k))))" by (rule sum.cong,simp,simp add: sum_distrib_left) also have "\ = (\k = 1.. div sqrt n) * (cnj (\ k) * (\m = 1..x. unity_root n (-m*k))))" using n by (intro sum.mono_neutral_right) (auto intro: eq_zero) also have "\ = (\ div sqrt n) * (\k = 1.. k) * (\m = 1..x. unity_root n (-m*k))))" by (simp add: sum_distrib_left) finally have "(\m = 1..x. \(m)) = (\ div sqrt n) * (\k = 1.. k) * (\m = 1..x. unity_root n (-m*k))))" by blast hence eq: "sqrt n * (\m=1..x. \(m)) = \ * (\k=1.. k) * (\m=1..x. unity_root n (-m*k))))" by auto define f where "f = (\k. (\m = 1..x. unity_root n (-m*k)))" hence "(sqrt n) * norm(\m = 1..x. \(m)) = norm(\ * (\k=1.. k) * (\m = 1..x. unity_root n (-m*k)))))" proof - have "norm(sqrt n * (\m=1..x. \(m))) = norm (sqrt n) * norm((\m = 1..x. \(m)))" by (simp add: norm_mult) also have "\ = (sqrt n) * norm((\m = 1..x. \(m)))" by simp finally have 1: "norm((sqrt n) * (\m = 1..x. \(m))) = (sqrt n) * norm((\m = 1..x. \(m)))" by blast then show ?thesis using eq by algebra qed also have "\ = norm (\k = 1.. k) * (\m = 1..x. unity_root n (-m*k))))" by (simp add: norm_mult \_mod) also have "\ \ (\k = 1.. k) * (\ m = 1..x. unity_root n (-m*k))))" using norm_sum by blast also have "\ = (\k = 1.. k)) * norm((\ m = 1..x. unity_root n (-m*k))))" by (rule sum.cong,simp, simp add: norm_mult) also have "\ \ (\k = 1..m = 1..x. unity_root n (-m*k))))" proof - show ?thesis proof (rule sum_mono) fix k assume "k \ {1..m=1..x. unity_root n (- int m * int k))" have "sum_aux \ 0" unfolding sum_aux_def by auto have "norm (cnj (\ k)) \ 1" using norm_le_1[of k] by simp then have "norm (cnj (\ k)) * sum_aux \ 1 * sum_aux" using \sum_aux \ 0\ by (simp add: mult_left_le_one_le) then show " norm (cnj (\ k)) * norm (\m = 1..x. unity_root n (- int m * int k)) \ norm (\m = 1..x. unity_root n (- int m * int k))" unfolding sum_aux_def by argo qed qed also have "\ = (\k = 1..m = 1..x. \(m)) \ (\k = 1..m = 1..x. unity_root n (-m*(n-k)))" unfolding f_def by blast also have "\ = (\m = 1..x. unity_root n (m*k))" proof (rule sum.cong,simp) fix xa assume "xa \ {1..x}" have "(k * int xa - int n * int xa) mod int n = (k * int xa - 0) mod int n" by (intro mod_diff_cong) auto thus "unity_root n (-int xa * (int n - k)) = unity_root n (int xa * k)" unfolding ring_distribs by (intro unity_root_cong) (auto simp: cong_def algebra_simps) qed also have "\ = cnj(f(k))" proof - have "cnj(f(k)) = cnj (\m = 1..x. unity_root n (- int m * k))" unfolding f_def by blast also have "cnj (\m = 1..x. unity_root n (- int m * k)) = (\m = 1..x. cnj(unity_root n (- int m * k)))" by (rule cnj_sum) also have "\ = (\m = 1..x. unity_root n (int m * k))" by (intro sum.cong) (auto simp: unity_root_uminus) finally show ?thesis by auto qed finally show "f(n-k) = cnj(f(k))" by blast qed hence "norm(f(n-k)) = norm(cnj(f(k)))" by simp hence "norm(f(n-k)) = norm(f(k))" by auto } note eq = this have 25: "odd n \ (\k = 1..n - 1. norm (f (int k))) \ 2 * (\k = 1..(n-1) div 2. norm (f (int k)))" "even n \ (\k = 1..n - 1. norm (f (int k))) \ 2 * (\k = 1..(n-2) div 2. norm (f (int k))) + norm(f(n div 2))" proof - assume "odd n" define g where "g = (\k. norm (f k))" have "(n-1) div 2 = n div 2" using \odd n\ n using div_mult_self1_is_m[OF pos2,of "n-1"] odd_two_times_div_two_nat[OF \odd n\] by linarith have "(\i=1..n-1. g i) = (\i\{1..n div 2}\{n div 2<..n-1}. g i)" using n by (intro sum.cong,auto) also have "\ = (\i\{1..n div 2}. g i) + (\i\{n div 2<..n-1}. g i)" by (subst sum.union_disjoint,auto) also have "(\i\{n div 2<..n-1}. g i) = (\i\{1..n - (n div 2 + 1)}. g (n - i))" by (rule sum.reindex_bij_witness[of _ "\i. n - i" "\i. n - i"],auto) also have "\ \ (\i\{1..n div 2}. g (n - i))" by (intro sum_mono2,simp,auto simp add: g_def) finally have 1: "(\i=1..n-1. g i) \ (\i=1..n div 2. g i + g (n - i))" by (simp add: sum.distrib) have "(\i=1..n div 2. g i + g (n - i)) = (\i=1..n div 2. 2 * g i)" unfolding g_def apply(rule sum.cong,simp) using eq int_ops(6) by force also have "\ = 2 * (\i=1..n div 2. g i)" by (rule sum_distrib_left[symmetric]) finally have 2: "(\i=1..n div 2. g i + g (n - i)) = 2 * (\i=1..n div 2. g i)" by blast from 1 2 have "(\i=1..n-1. g i) \ 2 * (\i=1..n div 2. g i)" by algebra then show "(\n = 1..n - 1. norm (f (int n))) \ 2 * (\n = 1..(n-1) div 2. norm (f (int n)))" unfolding g_def \(n-1) div 2 = n div 2\ by blast next assume "even n" define g where "g = (\n. norm (f (n)))" have "(n-2) div 2 = n div 2 - 1" using \even n\ n by simp have "(\i=1..n-1. g i) = (\i\{1.. {n div 2} \ {n div 2<..n-1}. g i)" using n by (intro sum.cong,auto) also have "\ = (\i\{1..i\{n div 2<..n-1}. g i) + g(n div 2)" by (subst sum.union_disjoint,auto) also have "(\i\{n div 2<..n-1}. g i) = (\i\{1..n - (n div 2+1)}. g (n - i))" by (rule sum.reindex_bij_witness[of _ "\i. n - i" "\i. n - i"],auto) also have "\ \ (\i\{1..even n\ n by auto then have "n - (n div 2 + 1) < n div 2" using n by (simp add: divide_simps) then show "{1..n - (n div 2 + 1)} \ {1..i=1..n-1. g i) \ (\i=1..i=1..i=1.. = 2 * (\i=1..i=1..i=1..i=1..n-1. g i) \ 2 * (\i=1..i=1..n-1. g i) \ 2 * (\i=1..(n-2) div 2. g i) + g(n div 2)" proof - have "{1..i=1..i=1..(n-2) div 2. g i)" by (rule sum.cong,simp) then show ?thesis using 3 by presburger qed then show "(\k = 1..n - 1. norm (f (int k))) \ 2 * (\n = 1..(n-2) div 2. norm (f (int n))) + g(n div 2)" unfolding g_def by blast qed (* expression for each f(n) *) {fix k :: int assume "1 \ k" "k \ n div 2" have "k \ n - 1" using \k \ n div 2\ n by linarith define y where "y = unity_root n (-k)" define z where "z = exp (-(pi*k/n)* \)" have "z^2 = exp (2*(-(pi*k/n)* \))" unfolding z_def using exp_double[symmetric] by blast also have "\ = y" unfolding y_def unity_root_conv_exp by (simp add: algebra_simps) finally have z_eq: "y = z^2" by blast have z_not_0: "z \ 0" using z_eq by (simp add: z_def) then have "y \ 1" using unity_root_eq_1_iff_int \1 \ k\ \k \ n - 1\ not_less unity_root_eq_1_iff_int y_def zdvd_not_zless by auto have "f(k) = (\m = 1..x . y^m)" unfolding f_def y_def by (subst unity_root_pow,rule sum.cong,simp,simp add: algebra_simps) also have sum: "\ = (\m = 1.. = (\m = 0.. = (y^(x+1) - 1) div (y - 1) - 1" using geometric_sum[OF \y \ 1\, of "x+1"] by (simp add: atLeast0LessThan) also have "\ = (y^(x+1) - 1 - (y-1)) div (y - 1)" proof - have "y - 1 \ 0" using \y \ 1\ by simp show ?thesis using divide_diff_eq_iff[OF \y - 1 \ 0\, of "(y^(x+1) - 1)" 1] by auto qed also have "\ = (y^(x+1) - y) div (y - 1)" by (simp add: algebra_simps) also have "\ = y * (y^x - 1) div (y - 1)" by (simp add: algebra_simps) also have "\ = z^2 * ((z^2)^x - 1) div (z^2 - 1)" unfolding z_eq by blast also have "\ = z^2 * (z^(2*x) - 1) div (z^2 - 1)" by (subst power_mult[symmetric, of z 2 x],blast) also have "\ = z^(x+1)*((z ^x -inverse(z^x))) / (z - inverse(z))" proof - have "z^x \ 0" using z_not_0 by auto have 1: "z ^ (2 * x) - 1 = z^x*(z ^x -inverse(z^x))" by (simp add: semiring_normalization_rules(36) right_inverse[OF \z^x \ 0\] right_diff_distrib') have 2: "z\<^sup>2 - 1 = z*(z - inverse(z))" by (simp add: right_diff_distrib' semiring_normalization_rules(29) right_inverse[OF \z \ 0\]) have 3: "z\<^sup>2 * (z^x / z) = z^(x+1)" proof - have "z\<^sup>2 * (z^x / z) = z\<^sup>2 * (z^x * inverse z)" by (simp add: inverse_eq_divide) also have "\ = z^(x+1)" by (simp add: algebra_simps power2_eq_square right_inverse[OF \z \ 0\]) finally show ?thesis by blast qed have "z\<^sup>2 * (z ^ (2 * x) - 1) / (z\<^sup>2 - 1) = z\<^sup>2 * (z^x*(z ^x -inverse(z^x))) / (z*(z - inverse(z)))" by (subst 1, subst 2,blast) also have "\ = (z\<^sup>2 * (z^x / z)) * ((z ^x -inverse(z^x))) / (z - inverse(z))" by simp also have "\ = z^(x+1) *((z ^x -inverse(z^x))) / (z - inverse(z))" by (subst 3,simp) finally show ?thesis by simp qed finally have "f(k) = z^(x+1) *((z ^x -inverse(z^x))) / (z - inverse(z))" by blast (* inequality for each f(k) *) then have "norm(f(k)) = norm(z^(x+1) * (((z ^x -inverse(z^x))) / (z - inverse(z))))" by auto also have "\ = norm(z^(x+1)) * norm(((z ^x -inverse(z^x))) / (z - inverse(z)))" using norm_mult by blast also have "\ = norm(((z ^x -inverse(z^x))) / (z - inverse(z)))" proof - have "norm(z) = 1" unfolding z_def by auto have "norm(z^(x+1)) = 1" by (subst norm_power,simp add: \norm(z) = 1\) then show ?thesis by simp qed also have "\ = norm((exp (-(x*pi*k/n)* \) - exp ((x*pi*k/n)* \)) div (exp (-(pi*k/n)* \) - exp ((pi*k/n)* \)))" proof - have 1: "z ^ x = exp (-(x*pi*k/n)* \)" unfolding z_def by (subst exp_of_nat_mult[symmetric],simp add: algebra_simps) have "inverse (z ^ x) = inverse (exp (-(x*pi*k/n)* \))" using \z ^ x = exp (-(x*pi*k/n)* \)\ by auto also have "\ = (exp ((x*pi*k/n)* \))" by (simp add: exp_minus) finally have 2: "inverse(z^x) = exp ((x*pi*k/n)* \)" by simp have 3: "inverse z = exp ((pi*k/n)* \)" by (simp add: exp_minus z_def) show ?thesis using 1 2 3 z_def by simp qed also have "\ = norm((sin (x*pi*k/n)) div (sin (pi*k/n)))" proof - have num: "(exp (-(x*pi*k/n)* \) - exp ((x*pi*k/n)* \)) = (-2*\* sin((x*pi*k/n)))" proof - have 1: "exp (-(x*pi*k/n)* \) = cos(-(x*pi*k/n)) + \ * sin(-(x*pi*k/n))" "exp ((x*pi*k/n)* \) = cos((x*pi*k/n)) + \ * sin((x*pi*k/n))" using Euler Im_complex_of_real Im_divide_of_nat Im_i_times Re_complex_of_real complex_Re_of_int complex_i_mult_minus exp_zero mult.assoc mult.commute by force+ have "(exp (-(x*pi*k/n)* \) - exp ((x*pi*k/n)* \)) = (cos(-(x*pi*k/n)) + \ * sin(-(x*pi*k/n))) - (cos((x*pi*k/n)) + \ * sin((x*pi*k/n)))" using 1 by argo also have "\ = -2*\* sin((x*pi*k/n))" by simp finally show ?thesis by blast qed have den: "(exp (-(pi*k/n)* \) - exp ((pi*k/n)* \)) = -2*\* sin((pi*k/n))" proof - have 1: "exp (-(pi*k/n)* \) = cos(-(pi*k/n)) + \ * sin(-(pi*k/n))" "exp ((pi*k/n)* \) = cos((pi*k/n)) + \ * sin((pi*k/n))" using Euler Im_complex_of_real Im_divide_of_nat Im_i_times Re_complex_of_real complex_Re_of_int complex_i_mult_minus exp_zero mult.assoc mult.commute by force+ have "(exp (-(pi*k/n)* \) - exp ((pi*k/n)* \)) = (cos(-(pi*k/n)) + \ * sin(-(pi*k/n))) - (cos((pi*k/n)) + \ * sin((pi*k/n)))" using 1 by argo also have "\ = -2*\* sin((pi*k/n))" by simp finally show ?thesis by blast qed have "norm((exp (-(x*pi*k/n)* \) - exp ((x*pi*k/n)* \)) div (exp (-(pi*k/n)* \) - exp ((pi*k/n)* \))) = norm((-2*\* sin((x*pi*k/n))) div (-2*\* sin((pi*k/n))))" using num den by presburger also have "\ = norm(sin((x*pi*k/n)) div sin((pi*k/n)))" by (simp add: norm_divide) finally show ?thesis by blast qed also have "\ = norm((sin (x*pi*k/n))) div norm((sin (pi*k/n)))" by (simp add: norm_divide) also have "\ \ 1 div norm((sin (pi*k/n)))" proof - have "norm((sin (pi*k/n))) \ 0" by simp have "norm (sin (x*pi*k/n)) \ 1" by simp then show ?thesis using divide_right_mono[OF \norm (sin (x*pi*k/n)) \ 1\ \norm((sin (pi*k/n))) \ 0\] by blast qed finally have 26: "norm(f(k)) \ 1 div norm((sin (pi*k/n)))" by blast (* inequality with sin *) { fix t assume "t \ 0" "t \ pi div 2" then have "t \ {0..pi div 2}" by auto have "convex_on {0..pi/2} (\x. -sin x)" by (rule convex_on_realI[where f' = "\x. - cos x"]) (auto intro!: derivative_eq_intros simp: cos_monotone_0_pi_le) from convex_onD_Icc'[OF this \t \ {0..pi div 2}\] have "sin(t) \ (2 div pi)*t" by simp } note sin_ineq = this have sin_ineq_inst: "sin ((pi*k) / n) \ (2 * k) / n" proof - have "pi / n \ 0" by simp have 1: "(pi*k) / n \ 0" using \1 \ k\ by auto have "(pi*k)/n = (pi / n) * k" by simp also have "\ \ (pi / n) * (n / 2)" using mult_left_mono[of "k" "n / 2" "pi / n"] \k \ n div 2\ \0 \ pi / real n\ by linarith also have "\ \ pi / 2" by (simp add: divide_simps) finally have 2: "(pi*k)/n \ pi / 2" by auto have "(2 / pi) * (pi * k / n) \ sin((pi * k) / n)" using sin_ineq[OF 1 2] by blast then show "sin((pi * k) / n) \ (2*k) / n" by auto qed from 26 have "norm(f(k)) \ 1 div abs((sin (pi*k/n)))" by simp also have "\ \ 1 / abs((2*k) / n)" proof - have "sin (pi*k/n) \ (2*k) / n" using sin_ineq_inst by simp moreover have "(2*k) / n > 0" using n \1 \ k\ by auto ultimately have "abs((sin (pi*k/n))) \ abs((2*k)/n)" by auto have "abs((2*k)/n) > 0" using \(2*k)/n > 0\ by linarith then show "1 div abs((sin (pi*k/n))) \ 1 / abs(((2*k)/n))" using \abs((2*k)/n) > 0\ \abs((sin (pi*k/n))) \ abs(((2*k)/n))\ by (intro frac_le) auto qed also have "\ = n / (2*k)" using \k \ 1\ by simp finally have "norm(f(k)) \ n / (2*k)" by blast } note ineq = this (* inequality for the odd and even case*) have "sqrt n * norm (sum \ {1..x}) < n * ln n" proof (cases "even n") case True have "norm (f(n div 2)) \ 1" proof - have "int (n div 2) \ 1" using n \even n\ by auto show ?thesis using ineq[OF \int (n div 2) \ 1\] True n by force qed from 24 have "sqrt n * norm (sum \ {1..x}) \ (\k = 1.. = (\k = 1..n-1. norm (f (int k)))" by (intro sum.cong) auto also have "\ \ 2 * (\k = 1..(n - 2) div 2. norm (f (int k))) + norm(f(n div 2))" using 25(2)[OF True] by blast also have "\ \ real n * (\k = 1..(n - 2) div 2. 1 / k) + norm(f(n div 2))" proof - have "(\k = 1..(n - 2) div 2. norm (f (int k))) \ (\k = 1..(n - 2) div 2. real n div (2*k))" proof (rule sum_mono) fix k assume "k \ {1..(n - 2) div 2}" then have "1 \ int k" "int k \ n div 2" by auto show "norm (f (int k)) \ real n / (2*k)" using ineq[OF \1 \ int k\ \int k \ n div 2\] by auto qed also have "\ = (\k = 1..(n - 2) div 2. (real n div 2) * (1 / k))" by (rule sum.cong,auto) also have "\ = (real n div 2) * (\k = 1..(n - 2) div 2. 1 / k)" using sum_distrib_left[symmetric] by fast finally have "(\k = 1..(n - 2) div 2. norm (f (int k))) \ (real n div 2) * (\k = 1..(n - 2) div 2. 1 / k)" by blast then show ?thesis by argo qed also have "\ = real n * harm ((n - 2) div 2) + norm(f(n div 2))" unfolding harm_def inverse_eq_divide by simp also have "\ < n * ln n" proof (cases "n = 2") case True have "real n * harm ((n - 2) div 2) + norm (f (int (n div 2))) \ 1" using \n = 2\ \norm (f (int (n div 2))) \ 1\ unfolding harm_def by simp moreover have "real n * ln (real n) \ 4 / 3" using \n = 2\ ln2_ge_two_thirds by auto ultimately show ?thesis by argo next case False have "n > 3" using n \n \ 2\ \even n\ by auto then have "(n-2) div 2 > 0" by simp then have "harm ((n - 2) div 2) < ln (real (2 * ((n - 2) div 2) + 1))" using harm_less_ln by blast also have "\ = ln (real (n - 1))" using \even n\ \n > 3\ by simp finally have 1: "harm ((n - 2) div 2) < ln (real (n - 1))" by blast then have "real n * harm ((n - 2) div 2) < real n * ln (real (n - 1))" using n by simp then have "real n * harm ((n - 2) div 2) + norm (f (int (n div 2))) < real n * ln (real (n - 1)) + 1" using \norm (f (int (n div 2))) \ 1\ by argo also have "\ = real n * ln (real (n - 1)) + real n * 1 / real n" using n by auto also have "\ < real n * ln (real (n - 1)) + real n * ln (1 + 1 / (real n - 1))" proof - have "real n > 1" "real n > 0" using n by simp+ then have "real n * (1 / real n) < real n * ln (1 + 1 / (real n - 1))" by (intro mult_strict_left_mono harm_aux_ineq_1) auto then show ?thesis by auto qed also have "\ = real n * ( ln (real (n - 1)) + ln (1 + 1 / (real n - 1)))" by argo also have "\ = real n * ( ln (real (n - 1) * (1 + 1 / (real n - 1))))" proof - have "real (n - 1) > 0" "1 + 1 / (real n - 1) > 0" using n by (auto simp add: add_pos_nonneg) show ?thesis by (subst ln_mult [OF \real (n - 1) > 0\ \1 + 1 / (real n - 1) > 0\,symmetric],blast) qed also have "\ = real n * ln n" using n by (auto simp add: divide_simps) finally show ?thesis by blast qed finally show ?thesis by blast next case False from 24 have "sqrt n * norm (sum \ {1..x}) \ (\k= 1.. = (\k= 1..n-1. norm (f (int k)))" by (intro sum.cong) auto also have "\ \ 2 * (\k = 1..(n - 1) div 2. norm (f (int k)))" using 25(1)[OF False] by blast also have "\ \ real n * (\k = 1..(n - 1) div 2. 1 / k)" proof - have "(\k = 1..(n - 1) div 2. norm (f (int k))) \ (\k = 1..(n - 1) div 2. real n div (2*k))" proof (rule sum_mono) fix k assume "k \ {1..(n - 1) div 2}" then have "1 \ int k" "int k \ n div 2" by auto show "norm (f (int k)) \ real n / (2*k)" using ineq[OF \1 \ int k\ \int k \ n div 2\] by auto qed also have "\ = (\k = 1..(n - 1) div 2. (n / 2) * (1 / k))" by (rule sum.cong,auto) also have "\ = (n / 2) * (\k = 1..(n - 1) div 2. 1 / k)" using sum_distrib_left[symmetric] by fast finally have "(\k = 1..(n - 1) div 2. norm (f (int k))) \ (real n div 2) * (\k = 1..(n - 1) div 2. 1 / k)" by blast then show ?thesis by argo qed also have "\ = real n * harm ((n - 1) div 2)" unfolding harm_def inverse_eq_divide by simp also have "\ < n * ln n" proof - have "n > 2" using n \odd n\ by presburger then have "(n-1) div 2 > 0" by auto then have "harm ((n - 1) div 2) < ln (real (2 * ((n - 1) div 2) + 1))" using harm_less_ln by blast also have "\ = ln (real n)" using \odd n\ by simp finally show ?thesis using n by simp qed finally show ?thesis by blast qed then have 1: "sqrt n * norm (sum \ {1..x}) < n * ln n" by blast show "norm (sum \ {1..x}) < sqrt n * ln n" proof - have 2: "norm (sum \ {1..x}) * sqrt n < n * ln n" using 1 by argo have "sqrt n > 0" using n by simp have 3: "(n * ln n) / sqrt n = sqrt n * ln n" using n by (simp add: field_simps) show "norm (sum \ {1..x}) < sqrt n * ln n" using mult_imp_less_div_pos[OF \sqrt n > 0\ 2] 3 by argo qed qed subsection \General case\ text \ We now first prove the inequality for the general case in terms of the divisor function: \ theorem (in dcharacter) polya_vinogradov_inequality_explicit: assumes nonprincipal: "\ \ principal_dchar n" shows "norm (sum \ {1..x}) < sqrt conductor * ln conductor * divisor_count (n div conductor)" proof - write primitive_extension ("\") write conductor ("c") interpret \: primitive_dchar c "residue_mult_group c" primitive_extension using primitive_primitive_extension nonprincipal by metis have *: "k \ x div b \ b * k \ x" if "b > 0" for b k by (metis that antisym_conv div_le_mono div_mult_self1_is_m less_imp_le not_less times_div_less_eq_dividend) have **: "a > 0" if "a dvd n" for a using n that by (auto intro!: Nat.gr0I) from nonprincipal have "(\m=1..x. \ m) = (\m | m \ {1..x} \ coprime m n. \ m)" by (intro sum.mono_neutral_cong_right) (auto simp: eq_zero_iff principal_decomposition) also have "\ = (\m=1..x. \ m * (\d | d dvd gcd m n. moebius_mu d))" by (subst sum_moebius_mu_divisors', intro sum.mono_neutral_cong_left) (auto simp: coprime_iff_gcd_eq_1 simp del: coprime_imp_gcd_eq_1) also have "\ = (\m=1..x. \d | d dvd gcd m n. \ m * moebius_mu d)" by (simp add: sum_distrib_left) also have "\ = (\m=1..x. \d | d dvd m \ d dvd n. \ m * moebius_mu d)" by (intro sum.cong) auto also have "\ = (\(m, d)\(SIGMA m:{1..x}. {d. d dvd m \ d dvd n}). \ m * moebius_mu d)" using n by (subst sum.Sigma) auto also have "\ = (\(d, q)\(SIGMA d:{d. d dvd n}. {1..x div d}). moebius_mu d * \ (d * q))" by (intro sum.reindex_bij_witness[of _ "\(d,q). (d * q, d)" "\(m,d). (d, m div d)"]) (auto simp: * ** Suc_le_eq) also have "\ = (\d | d dvd n. moebius_mu d * \ d * (\q=1..x div d. \ q))" using n by (subst sum.Sigma [symmetric]) (auto simp: sum_distrib_left mult.assoc) finally have eq: "(\m=1..x. \ m) = \" . have "norm (\m=1..x. \ m) \ (\d | d dvd n. norm (moebius_mu d * \ d) * norm (\q=1..x div d. \ q))" unfolding eq by (intro sum_norm_le) (simp add: norm_mult) also have "\ < (\d | d dvd n. norm (moebius_mu d * \ d) * (sqrt c * ln c))" (is "sum ?lhs _ < sum ?rhs _") proof (rule sum_strict_mono_ex1) show "\d\{d. d dvd n}. ?lhs d \ ?rhs d" by (intro ballI mult_left_mono less_imp_le[OF \.polya_vinogradov_inequality_primitive]) auto show "\d\{d. d dvd n}. ?lhs d < ?rhs d" by (intro bexI[of _ 1] mult_strict_left_mono \.polya_vinogradov_inequality_primitive) auto qed (use n in auto) also have "\ = sqrt c * ln c * (\d | d dvd n. norm (moebius_mu d * \ d))" by (simp add: sum_distrib_left sum_distrib_right mult_ac) also have "(\d | d dvd n. norm (moebius_mu d * \ d)) = (\d | d dvd n \ squarefree d \ coprime d c. 1)" using n by (intro sum.mono_neutral_cong_right) (auto simp: moebius_mu_def \.eq_zero_iff norm_mult norm_power \.norm) also have "\ = card {d. d dvd n \ squarefree d \ coprime d c}" by simp also have "card {d. d dvd n \ squarefree d \ coprime d c} \ card {d. d dvd (n div c)}" proof (intro card_mono; safe?) show "finite {d. d dvd (n div c)}" using dvd_div_eq_0_iff[of c n] n conductor_dvd by (intro finite_divisors_nat) auto next fix d assume d: "d dvd n" "squarefree d" "coprime d c" hence "d > 0" by (intro Nat.gr0I) auto show "d dvd (n div c)" proof (rule multiplicity_le_imp_dvd) fix p :: nat assume p: "prime p" show "multiplicity p d \ multiplicity p (n div c)" proof (cases "p dvd d") assume "p dvd d" with d \d > 0\ p have "multiplicity p d = 1" by (auto simp: squarefree_factorial_semiring' in_prime_factors_iff) moreover have "p dvd (n div c)" proof - have "p dvd c * (n div c)" using \p dvd d\ \d dvd n\ conductor_dvd by auto moreover have "\(p dvd c)" using d p \p dvd d\ coprime_common_divisor not_prime_unit by blast ultimately show "p dvd (n div c)" using p prime_dvd_mult_iff by blast qed hence "multiplicity p (n div c) \ 1" using n p conductor_dvd dvd_div_eq_0_iff[of c n] by (intro multiplicity_geI) (auto intro: Nat.gr0I) ultimately show ?thesis by simp qed (auto simp: not_dvd_imp_multiplicity_0) qed (use \d > 0\ in simp_all) qed also have "card {d. d dvd (n div c)} = divisor_count (n div c)" by (simp add: divisor_count_def) finally show "norm (sum \ {1..x}) < sqrt c * ln c * divisor_count (n div c)" using conductor_gr_0 by (simp add: mult_left_mono) qed (* TODO: Move? *) text \ Next, we obtain a suitable upper bound on the number of divisors of \n\: \ lemma divisor_count_upper_bound_aux: fixes n :: nat shows "divisor_count n \ 2 * card {d. d dvd n \ d \ sqrt n}" proof (cases "n = 0") case False hence n: "n > 0" by simp have *: "x > 0" if "x dvd n" for x using that n by (auto intro!: Nat.gr0I) have **: "real n = sqrt (real n) * sqrt (real n)" by simp have ***: "n < x * sqrt n \ sqrt n < x" "x * sqrt n < n \ x < sqrt n" for x by (metis ** n of_nat_0_less_iff mult_less_iff1 real_sqrt_gt_0_iff)+ have "divisor_count n = card {d. d dvd n}" by (simp add: divisor_count_def) also have "{d. d dvd n} = {d. d dvd n \ d \ sqrt n} \ {d. d dvd n \ d > sqrt n}" by auto also have "card \ = card {d. d dvd n \ d \ sqrt n} + card {d. d dvd n \ d > sqrt n}" using n by (subst card_Un_disjoint) auto also have "bij_betw (\d. n div d) {d. d dvd n \ d > sqrt n} {d. d dvd n \ d < sqrt n}" using n by (intro bij_betwI[of _ _ _ "\d. n div d"]) (auto simp: Real.real_of_nat_div real_sqrt_divide field_simps * ***) hence "card {d. d dvd n \ d > sqrt n} = card {d. d dvd n \ d < sqrt n}" by (rule bij_betw_same_card) also have "\ \ card {d. d dvd n \ d \ sqrt n}" using n by (intro card_mono) auto finally show "divisor_count n \ 2 * \" by simp qed auto lemma divisor_count_upper_bound: fixes n :: nat shows "divisor_count n \ 2 * nat \sqrt n\" proof (cases "n = 0") case False have "divisor_count n \ 2 * card {d. d dvd n \ d \ sqrt n}" by (rule divisor_count_upper_bound_aux) also have "card {d. d dvd n \ d \ sqrt n} \ card {1..nat \sqrt n\}" using False by (intro card_mono) (auto simp: le_nat_iff le_floor_iff Suc_le_eq intro!: Nat.gr0I) also have "\ = nat \sqrt n\" by simp finally show ?thesis by simp qed auto lemma divisor_count_upper_bound': fixes n :: nat shows "real (divisor_count n) \ 2 * sqrt n" proof - have "real (divisor_count n) \ 2 * real (nat \sqrt n\)" using divisor_count_upper_bound[of n] by linarith also have "\ \ 2 * sqrt n" by simp finally show ?thesis . qed (* END TODO *) text \ We are now ready to prove the `regular' Pólya--Vinogradov inequality. Apostol formulates it in the following way (Theorem 13.15, notation adapted): `If \\\ is any nonprincipal character mod \n\, then for all \x \ 2\ we have $\sum_{m\leq x} \chi(m) = O(\sqrt{n}\log n)$.' The precondition \x \ 2\ here is completely unnecessary. The `Big-O' notation is somewhat problematic since it does not make explicit in what way the variables are quantified (in particular the \x\ and the \\\). The statement of the theorem in this way (for a fixed character \\\) seems to suggest that \n\ is fixed here, which would make the use of `Big-O' completely vacuous, since it is an asymptotic statement about \n\. We therefore decided to formulate the inequality in the following more explicit way, even giving an explicit constant factor: \ theorem (in dcharacter) polya_vinogradov_inequality: assumes nonprincipal: "\ \ principal_dchar n" shows "norm (\m=1..x. \ m) < 2 * sqrt n * ln n" proof - have "n div conductor > 0" using n conductor_dvd dvd_div_eq_0_iff[of conductor n] by auto have "norm (\m=1..x. \ m) < sqrt conductor * ln conductor * divisor_count (n div conductor)" using nonprincipal by (rule polya_vinogradov_inequality_explicit) also have "\ \ sqrt conductor * ln conductor * (2 * sqrt (n div conductor))" using conductor_gr_0 \n div conductor > 0\ by (intro mult_left_mono divisor_count_upper_bound') (auto simp: Suc_le_eq) also have "sqrt (n div conductor) = sqrt n / sqrt conductor" using conductor_dvd by (simp add: Real.real_of_nat_div real_sqrt_divide) also have "sqrt conductor * ln conductor * (2 * (sqrt n / sqrt conductor)) = 2 * sqrt n * ln conductor" using conductor_gr_0 n by (simp add: algebra_simps) also have "\ \ 2 * sqrt n * ln n" using conductor_le_modulus conductor_gr_0 by (intro mult_left_mono) auto finally show ?thesis . qed unbundle vec_lambda_notation end \ No newline at end of file diff --git a/thys/Lovasz_Local/Lovasz_Local_Lemma.thy b/thys/Lovasz_Local/Lovasz_Local_Lemma.thy --- a/thys/Lovasz_Local/Lovasz_Local_Lemma.thy +++ b/thys/Lovasz_Local/Lovasz_Local_Lemma.thy @@ -1,765 +1,706 @@ (* Theory: Lovasz_Local_Lemma Author: Chelsea Edmonds *) section \Lovasz Local Lemma \ theory Lovasz_Local_Lemma imports Basic_Method "HOL-Real_Asymp.Real_Asymp" Indep_Events Digraph_Extensions begin -(* The following two lemmas were taken from Gauss_Sums.Polya_Vinogradov AFP entry. - Adding in entire dependency caused a significant slow down, could these be moved to the Analysis - library at some point? *) -lemma ln_add_one_self_less_self: - fixes x :: real - assumes "x > 0" - shows "ln (1 + x) < x" -proof - - have "0 \ x" "0 < x" "exp x > 0" "1+x > 0" using assms by simp+ - have "1 + x < 1 + x + x\<^sup>2 / 2" - using \0 < x\ by auto - also have "\ \ exp x" - using exp_lower_Taylor_quadratic[OF \0 \ x\] by blast - finally have "1 + x < exp (x)" by blast - then have "ln (1 + x) < ln (exp (x))" - using ln_less_cancel_iff[OF \1+x > 0\ \exp(x) > 0\] by auto - also have "\ = x" using ln_exp by blast - finally show ?thesis by auto -qed - -lemma exp_1_bounds: - assumes "x > (0::real)" - shows "exp 1 > (1 + 1 / x) powr x" and "exp 1 < (1 + 1 / x) powr (x+1)" -proof - - have "ln (1 + 1 / x) < 1 / x" - using ln_add_one_self_less_self assms by simp - thus "exp 1 > (1 + 1 / x) powr x" using assms - by (simp add: field_simps powr_def) -next - have "1 < (x + 1) * ln ((x + 1) / x)" (is "_ < ?f x") - proof (rule DERIV_neg_imp_decreasing_at_top[where ?f = ?f]) - fix t assume t: "x \ t" - have "(?f has_field_derivative (ln (1 + 1 / t) - 1 / t)) (at t)" - using t assms by (auto intro!: derivative_eq_intros simp:divide_simps) - moreover have "ln (1 + 1 / t) - 1 / t < 0" - using ln_add_one_self_less_self[of "1 / t"] t assms by auto - ultimately show "\y. ((\t. (t + 1) * ln ((t + 1) / t)) has_real_derivative y) (at t) \ y < 0" - by blast - qed real_asymp - thus "exp 1 < (1 + 1 / x) powr (x + 1)" - using assms by (simp add: powr_def field_simps) -qed - - subsection \Random Lemmas on Product Operator \ lemma prod_constant_ge: fixes y :: "'b :: {comm_monoid_mult, linordered_semidom}" assumes "card A \ k" assumes "y \ 0" and "y < 1" - shows "(\x\ A. y) \ y ^ k" -using assms(1) proof (induct A rule: infinite_finite_induct) - case (infinite A) - then show ?case using assms(2) assms(3) by (simp add: power_le_one) -next - case empty - then show ?case using assms(2) assms(3) by (simp add: power_le_one) -next - case (insert x F) - then show ?case using assms(2) assms(3) - by (metis nless_le power_decreasing prod_constant) -qed + shows "(\x\A. y) \ y ^ k" + using assms power_decreasing by fastforce lemma (in linordered_idom) prod_mono3: assumes "finite J" "I \ J" "\i. i \ J \ 0 \ f i" "(\i. i \ J \ f i \ 1)" shows "prod f J \ prod f I" proof - have "prod f J \ (\i\J. if i \ I then f i else 1)" using assms by (intro prod_mono) auto also have "\ = prod f I" using \finite J\ \I \ J\ by (simp add: prod.If_cases Int_absorb1) finally show ?thesis . qed lemma bij_on_ss_image: assumes "A \ B" assumes "bij_betw g B B'" shows "g ` A \ B'" using assms by (auto simp add: bij_betw_apply subsetD) lemma bij_on_ss_proper_image: assumes "A \ B" assumes "bij_betw g B B'" shows "g ` A \ B'" -proof (intro psubsetI subsetI) - fix x assume "x \ g ` A" - then show "x \ B'" using assms bij_betw_apply subsetD by fastforce -next - show "g ` A \ B'" using assms by (auto) (smt (verit, best) bij_betw_iff_bijections imageE subset_eq) -qed + by (smt (verit, ccfv_SIG) assms bij_betw_iff_bijections bij_betw_subset leD psubsetD psubsetI subsetI) subsection \Dependency Graph Concept \ text \Uses directed graphs. The pair\_digraph locale was sufficient as multi-edges are irrelevant \ locale dependency_digraph = pair_digraph "G :: nat pair_pre_digraph" + prob_space "M :: 'a measure" for G M + fixes F :: "nat \ 'a set" assumes vss: "F ` (pverts G) \ events" assumes mis: "\ i. i \ (pverts G) \ mutual_indep_events (F i) F ((pverts G) - ({i} \ neighborhood i))" begin lemma dep_graph_indiv_nh_indep: assumes "A \ pverts G" "B \ pverts G" assumes "B \ neighborhood A" assumes "A \ B" assumes "prob (F B) \ 0" shows "\

((F A) | (F B)) = prob (F A)" proof- have "B \ {A} \ neighborhood A" using assms(3) assms(4) by auto then have "B \ (pverts G - ({A} \ neighborhood A))" using assms(2) by auto moreover have "mutual_indep_events (F A) F (pverts G - ({A} \ neighborhood A))" using mis assms by auto ultimately show ?thesis using assms(5) assms(1) assms(2) vss mutual_indep_ev_cond_single by auto qed lemma mis_subset: assumes "i \ pverts G" assumes "A \ pverts G" shows "mutual_indep_events (F i) F (A - ({i} \ neighborhood i))" proof (cases "A \ ({i} \ neighborhood i)") case True then have "A - ({i} \ neighborhood i) = {}" by auto then show ?thesis using mutual_indep_ev_empty vss assms(1) by blast next case False then have "A - ({i} \ neighborhood i) \ pverts G - ({i} \ neighborhood i)" using assms(2) by auto then show ?thesis using mutual_indep_ev_subset mis assms(1) by blast qed lemma dep_graph_indep_events: assumes "A \ pverts G" assumes "\ Ai. Ai \ A \ out_degree G Ai = 0" shows "indep_events F A" proof - have "\ Ai. Ai \ A \ (mutual_indep_events (F Ai) F (A - {Ai}))" proof - fix Ai assume ain: "Ai \ A" then have "(neighborhood Ai) = {}" using assms(2) neighborhood_empty_iff by simp moreover have "mutual_indep_events (F Ai) F (A - ({Ai} \ neighborhood Ai))" using mis_subset[of Ai A] ain assms(1) by auto ultimately show "mutual_indep_events (F Ai) F (A - {Ai})" by simp qed then show ?thesis using mutual_indep_ev_set_all[of F A] vss by auto qed end subsection \Lovasz Local General Lemma \ context prob_space begin lemma compl_sets_index: assumes "F ` A \ events" shows "(\ i. space M - F i) ` A \ events" proof (intro subsetI) fix x assume "x \ (\i. space M - F i) ` A" then obtain i where xeq: "x = space M - F i" and "i \ A" by blast then have "F i \ events" using assms by auto thus "x \ events" using sets.compl_sets xeq by simp qed lemma lovasz_inductive_base: assumes "dependency_digraph G M F" assumes "\ Ai . Ai \ A \ g Ai \ 0 \ g Ai < 1" assumes "\ Ai. Ai \ A \ (prob (F Ai) \ (g Ai) * (\ Aj \ pre_digraph.neighborhood G Ai. (1 - (g Aj))))" assumes "Ai \ A" assumes "pverts G = A" shows "prob (F Ai) \ g Ai" proof - have genprod: "\ S. S \ A \ (\Aj \ S . (1 - (g Aj))) \ 1" using assms(2) by (smt (verit) prod_le_1 subsetD) interpret dg: dependency_digraph G M F using assms(1) by simp have "dg.neighborhood Ai \ A" using assms(3) dg.neighborhood_wf assms(5) by simp then show ?thesis using genprod assms mult_left_le by (smt (verit)) qed lemma lovasz_inductive_base_set: assumes "N \ A" assumes "\ Ai . Ai \ A \ g Ai \ 0 \ g Ai < 1" assumes "\ Ai. Ai \ A \ (prob (F Ai) \ (g Ai) * (\ Aj \ N. (1 - (g Aj))))" assumes "Ai \ A" shows "prob (F Ai) \ g Ai" proof - have genprod: "\ S. S \ A \ (\Aj \ S . (1 - (g Aj))) \ 1" using assms(2) by (smt (verit) prod_le_1 subsetD) then show ?thesis using genprod assms mult_left_le by (smt (verit)) qed lemma split_prob_lt_helper: assumes dep_graph: "dependency_digraph G M F" assumes dep_graph_verts: "pverts G = A" assumes fbounds: "\ i . i \ A \ f i \ 0 \ f i < 1" assumes prob_Ai: "\ Ai. Ai \ A \ prob (F Ai) \ (f Ai) * (\ Aj \ pre_digraph.neighborhood G Ai . (1 - (f Aj)))" assumes aiin: "Ai \ A" assumes "N \ pre_digraph.neighborhood G Ai" assumes "\ P1 P2. \

(F Ai | \Aj\S. space M - F Aj) = P1/P2 \ P1 \ prob (F Ai)\ P2 \ (\ Aj \ N . (1 - (f Aj)))" shows "\

(F Ai | \Aj\S. space M - F Aj) \ f Ai" proof - interpret dg: dependency_digraph G M F using assms(1) by simp have lt1: "\ Aj. Aj \ A \ (1 - (f Aj)) \ 1" using assms(3) by auto have gt0: "\ Aj. Aj \ A \ (1 - (f Aj)) > 0" using assms(3) by auto then have prodgt0: "\ S'. S' \ A \ (\ Aj \ S' . (1 - f Aj)) > 0" using prod_pos by (metis subsetD) obtain P1 P2 where peq: "\

(F Ai | \Aj\S. space M - F Aj) = P1/P2" and "P1 \ prob (F Ai)" and p2gt: "P2 \ (\ Aj \ N . (1 - (f Aj)))" using assms(7) by auto then have "P1 \ (f Ai) * (\ Aj \ pre_digraph.neighborhood G Ai . (1 - (f Aj)))" using prob_Ai aiin by fastforce moreover have "P2 \ (\ Aj \ dg.neighborhood Ai . (1 - (f Aj)))" using assms(6) gt0 dg.neighborhood_wf dep_graph_verts subset_iff lt1 dg.neighborhood_finite p2gt by (smt (verit, ccfv_threshold) prod_mono3) ultimately have "P1/P2 \ ((f Ai) * (\ Aj \ dg.neighborhood Ai . (1 - (f Aj)))/(\ Aj \ dg.neighborhood Ai . (1 - (f Aj))))" using frac_le[of "(f Ai) * (\ Aj \ dg.neighborhood Ai . (1 - (f Aj)))" "P1" "(\ Aj \ dg.neighborhood Ai . (1 - (f Aj)))"] prodgt0[of "dg.neighborhood Ai"] assms(3) dg.neighborhood_wf[of Ai] by (simp add: assms(2) bounded_measure finite_measure_compl assms(5)) then show ?thesis using prodgt0[of "dg.neighborhood Ai"] dg.neighborhood_wf[of Ai] assms(2) peq by (metis divide_eq_imp rel_simps(70)) qed lemma lovasz_inequality: assumes finS: "finite S" assumes sevents: "F ` S \ events" assumes S_subset: "S \ A - {Ai}" assumes prob2: "prob (\ Aj \ S . (space M - (F Aj))) > 0" assumes irange: "i \ {0.. N)" assumes s2_def: "S2 = S - S1" assumes ne_cond: "i > 0 \ S2 \ {}" assumes hyps: "\ B. B \ S \ g i \ A \ B \ A - {g i} \ B \ {} \ 0 < prob (\Aj\B. space M - F Aj) \ \

(F (g i) | \Aj\B. space M - F Aj) \ f (g i)" shows "\

((space M - F (g i)) | (\ ((\ i. space M - F i) ` g ` {0.. ((\ i. space M - F i) ` S2)))) \ (1 - f (g i))" proof - let ?c = "(\ i. space M - F i)" define S1ss where "S1ss = g ` {0.. {0.. {0.. S1ss" using bb S1ss_def irange by (smt (verit, best) bij_betw_iff_bijections image_iff subset_eq) have ginotin2: "g i \ S2" unfolding s2_def using irange bb by (simp add: bij_betwE) have giS: "g i \ S" using irange bij_betw_imp_surj_on imageI Int_iff s1_def bb by blast have "{0.. {0.. S1" unfolding S1ss_def using irange bb bij_on_ss_proper_image by meson then have sss: "S1ss \ S2 \ S" using s1_def s2_def by blast moreover have xsiin: "g i \ A"using irange using giS S_subset by (metis DiffE in_mono) moreover have ne: "S1ss \ S2 \ {}" using ne_cond S1ss_def by auto moreover have "S1ss \ S2 \ A - {g i}" using S_subset sss ginotin1 ginotin2 by auto moreover have gt02: "0 < prob (\ (?c ` (S1ss \ S2)))" using finS prob2 sevents prob_inter_ss_lt_index[of S ?c "S1ss \ S2"] ne sss compl_sets_index[of F S] by fastforce ultimately have ltfAi: "\

(F (g i) | \ (?c ` (S1ss \ S2))) \ f (g i)" using hyps[of "S1ss \ S2"] by blast have "?c ` (S1ss \ S2) \ events" using sss \S1ss \ S1\ compl_subset_in_events sevents s1_def s2_def by fastforce then have "\ (?c ` (S1ss \ S2)) \ events" using Inter_event_ss sss by (meson \S1ss \ S2 \ {}\ finite_imageI finite_subset image_is_empty finS subset_iff_psubset_eq) moreover have "F (g i) \ events" using xsiin giS sevents by auto ultimately have "\

(?c (g i) | \ (?c ` (S1ss \ S2))) \ 1 - f (g i)" using cond_prob_neg[of "\ (?c ` (S1ss \ S2))" "F (g i)"] gt02 xsiin ltfAi by simp then show "\

(?c (g i) | (\ (?c ` g ` {0.. (?c ` S2)))) \ (1 - f (g i))" by (simp add: S1ss_def image_Un) qed text \The main helper lemma \ lemma lovasz_inductive: assumes finA: "finite A" assumes Aevents: "F ` A \ events" assumes fbounds: "\ i . i \ A \ f i \ 0 \ f i < 1" assumes dep_graph: "dependency_digraph G M F" assumes dep_graph_verts: "pverts G = A" assumes prob_Ai: "\ Ai. Ai \ A \ prob (F Ai) \ (f Ai) * (\ Aj \ pre_digraph.neighborhood G Ai . (1 - (f Aj)))" assumes Ai_in: "Ai \ A" assumes S_subset: "S \ A - {Ai}" assumes S_nempty: "S \ {}" assumes prob2: "prob (\ Aj \ S . (space M - (F Aj))) > 0" shows "\

((F Ai) | (\ Aj \ S . (space M - (F Aj)))) \ f Ai" proof - let ?c = "\ i. space M - F i" have ceq: "\ A. ?c ` A = ((-) (space M)) ` (F ` A)" by auto interpret dg: dependency_digraph G M F using assms(4) by simp have finS: "finite S" using assms finite_subset by (metis finite_Diff) show "\

(( F Ai) | (\ Aj \ S . (space M - (F Aj)))) \ f Ai" using finS Ai_in S_subset S_nempty prob2 proof (induct S arbitrary: Ai rule: finite_psubset_induct ) case (psubset S) define S1 where "S1 = (S \ dg.neighborhood Ai)" define S2 where "S2 = S - S1" have "\ s . s \ S2 \ s \ A - ({Ai} \ dg.neighborhood Ai)" using S1_def S2_def psubset.prems(2) by blast then have s2ssmis: "S2 \ A - ({Ai} \ dg.neighborhood Ai)" by auto have sevents: "F ` S \ events" using assms(2) psubset.prems(2) by auto then have s1events: "F ` S1 \ events" using S1_def by auto have finS2: "finite S2" and finS1: "finite S1" using S2_def S1_def by (simp_all add: psubset(1)) have "mutual_indep_set (F Ai) (F ` S2)" using dg.mis[of Ai] mutual_indep_ev_subset s2ssmis psubset.prems(1) dep_graph_verts mutual_indep_iff by auto then have mis2: "mutual_indep_set (F Ai) (?c ` S2)" using mutual_indep_events_compl[of "F ` S2" "F Ai"] finS2 ceq[of S2] by simp have scompl_ev: "?c ` S \ events" using compl_sets_index sevents by simp then have s2cev: "?c ` S2 \ events" using S2_def scompl_ev by blast have "(\ Aj \ S . space M - (F Aj)) \ (\ Aj \ S2 . space M - (F Aj))" unfolding S2_def using Diff_subset image_mono Inter_anti_mono by blast then have "S2 \ {} \ prob (\ Aj \ S2 . space M - (F Aj)) \ 0" using psubset.prems(4) s2cev finS2 Inter_event_ss[of "?c ` S2"] finite_measure_mono[of "\ (?c ` S)" "\(?c ` S2)"] by simp then have s2prob_eq: "S2 \ {} \ \

((F Ai) | (\ (?c ` S2))) = prob (F Ai)" using assms(2) mutual_indep_cond_full[of " F Ai" "?c ` S2"] psubset.prems(1) s2cev finS2 mis2 by simp show ?case proof (cases "S1 = {}") case True then show ?thesis using lovasz_inductive_base[of G F A f Ai] psubset.prems(3) S2_def assms(3) assms(4) psubset.prems(1) prob_Ai s2prob_eq dep_graph_verts by (simp) next case s1F: False then have csgt0: "card S1 > 0" using s1F finS1 card_gt_0_iff by blast obtain g where bb: "bij_betw g {0..i. i \ {0.. 1 - f (g i) \ 0" using S1_def psubset.prems(2) bb bij_betw_apply assms(3) by fastforce have s1ss: "S1 \ dg.neighborhood Ai" using S1_def by auto moreover have "\ P1 P2. \

(F Ai | \Aj\S. space M - F Aj) = P1/P2 \ P1 \ prob (F Ai) \ P2 \ (\ Aj \ S1 . (1 - (f Aj)))" proof (cases "S2 = {}") case True then have Seq: "S1 = S" using S1_def S2_def by auto have inter_eventsS: "(\ Aj \ S . (space M - (F Aj))) \ events" using psubset.prems assms by (meson measure_notin_sets zero_less_measure_iff) then have peq: "\

((F Ai) | (\ Aj \ S1 . ?c Aj)) = prob ((\ Aj \ S1 . ?c Aj) \ (F Ai))/prob ((\ (?c ` S1)))" (is "\

((F Ai) | (\ Aj \ S1 . ?c Aj)) = ?Num/?Den") using cond_prob_ev_def[of "(\ Aj \ S1 . (space M - (F Aj)))" "F Ai"] using Seq psubset.prems(1) assms(2) by blast have "?Num \ prob (F Ai)" using finite_measure_mono assms(2) psubset.prems(1) by simp moreover have "?Den \ (\ Aj \ S1 . (1 - (f Aj)))" proof - have pcond: "prob (\(?c ` S1)) = prob (?c (g 0)) * (\i \ {1..(?c (g i) | (\(?c ` g ` {0.. i. i \ {1.. \

(?c (g i) | (\(?c ` g ` {0.. (1 - (f (g i)))" using lovasz_inequality[of S1 F A Ai _ S1 g S1 "{}" f] sevents finS psubset.prems(2) psubset.prems(4) bb psubset.hyps(2)[of _ "g _"] Seq by fastforce have "(\i. i \ {1.. 1 - f (g i) \ 0)" using igt0 by simp then have "(\i \ {1..<(card S1)} . \

(?c (g i) | (\(?c ` g ` {0.. (\i \ {1..<(card S1)} . (1 - (f (g i))))" using ineq prod_mono by (smt(verit, ccfv_threshold)) moreover have "prob (?c (g 0)) \ (1 - f (g 0))" proof - have g0in: "g 0 \ A" using bb csgt0 using psubset.prems(2) bij_betwE Seq by fastforce then have "prob (?c (g 0)) = 1 - prob (F (g 0))" using Aevents by (simp add: prob_compl) then show ?thesis using lovasz_inductive_base[of G F A f "g 0"] prob_Ai assms(4) dep_graph_verts fbounds g0in by auto qed moreover have "0 \ (\i = 1..(?c ` S1)) \ (1 - (f (g 0))) * (\i \ {1..<(card S1)} . (1 - (f (g i))))" using pcond igt0 mult_mono'[of "(1 - (f (g 0)))" ] by fastforce moreover have "{0.. {1..(?c ` S1)) \ (\i \ {0..<(card S1)} . (1 - (f (g i))))" by auto moreover have "(\i \ {0..<(card S1)} . (1 - (f (g i)))) = (\i \ S1 . (1 - (f (i))))" using prod.reindex_bij_betw bb by simp ultimately show ?thesis by simp qed ultimately show ?thesis using peq Seq by blast next case s2F: False have s2inter: "\ (?c ` S2) \ events" using s2F finS2 s2cev Inter_event_ss[of "?c ` S2"] by auto have split: "(\ Aj \ S . (?c Aj)) = (\ (?c `S1)) \ (\ (?c ` S2))" using S1_def S2_def by auto then have "\

(F Ai | (\ Aj \ S . (?c Aj))) = \

(F Ai | (\ (?c `S1)) \ (\ (?c ` S2)))" by simp moreover have s2n0: "prob (\ (?c ` S2)) \ 0" using psubset.prems(4) S2_def by (metis Int_lower2 split finite_measure_mono measure_le_0_iff s2inter semiring_norm(137)) moreover have "\ (?c ` S1) \ events" using finS1 S1_def scompl_ev s1F Inter_event_ss[of "(?c ` S1)"] by auto ultimately have peq: "\

(F Ai | (\ Aj \ S . (?c Aj))) = \

(F Ai \ (\ (?c `S1)) | \ (?c ` S2))/ \

(\ (?c `S1) | \ (?c `S2))" (is "\

(F Ai | (\ Aj \ S . (?c Aj))) = ?Num/?Den") using cond_prob_dual_intersect[of "F Ai" "\ (?c `S1)" "\ (?c `S2)"] assms(2) psubset.prems(1) s2inter by fastforce have "?Num \ \

(F Ai | \ (?c `S2))" using cond_prob_inter_set_lt[of "F Ai" "\ (?c `S2)" "?c ` S1"] using s1events finS1 psubset.prems(1) assms(2) s2inter finite_imageI[of S1 F] by blast then have "?Num \ prob (F Ai)" using s2F s2prob_eq by auto moreover have "?Den \ (\ Aj \ S1 . (1 - (f Aj)))" using psubset.hyps proof - have "prob (\(?c ` S2)) > 0" using s2n0 by (meson zero_less_measure_iff) then have pcond: "\

(\ (?c `S1) | \ (?c `S2)) = (\i = 0..(?c (g i) | (\ (?c ` g ` {0.. (?c ` S2)))))" using prob_cond_Inter_index_cond_compl_fn[of S1 "?c ` S2" F] s1F finS1 s2cev finS2 s2F s1events bb by auto have "\ i. i \ {0.. \

(?c (g i) | (\ (?c ` g ` {0.. (?c ` S2)))) \ (1 - f (g i))" using lovasz_inequality[of S F A Ai _ S1 g "dg.neighborhood Ai" S2 f] S1_def S2_def sevents finS psubset.prems(2) psubset.prems(4) bb psubset.hyps(2)[of _ "g _"] psubset(1) s2F by meson then have c1: "\

(\ (?c `S1) | \ (?c `S2)) \ (\i = 0..(\ (?c `S1) | \ (?c `S2)) \ (\i \ {0..i \ {0..x \ S1 . (1 - f x))" using bb using prod.reindex_bij_betw by fastforce ultimately show ?thesis by simp qed ultimately show ?thesis using peq by blast qed ultimately show ?thesis by (intro split_prob_lt_helper[of G F A]) (simp_all add: dep_graph dep_graph_verts fbounds psubset.prems(1) prob_Ai) qed qed qed text \The main lemma \ theorem lovasz_local_general: assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "\ Ai . Ai \ A \ f Ai \ 0 \ f Ai < 1" assumes "dependency_digraph G M F" assumes "\ Ai. Ai \ A \ (prob (F Ai) \ (f Ai) * (\ Aj \ pre_digraph.neighborhood G Ai. (1 - (f Aj))))" assumes "pverts G = A" shows "prob (\ Ai \ A . (space M - (F Ai))) \ (\ Ai \ A . (1 - f Ai))" "(\ Ai \ A . (1 - f Ai)) > 0" proof - show gt0: "(\ Ai \ A . (1 - f Ai)) > 0" using assms(4) by (simp add: prod_pos) let ?c = "\ i. space M - F i" interpret dg: dependency_digraph G M F using assms(5) by simp have general: "\Ai S. Ai \ A \ S \ A - {Ai} \ S \ {} \ prob (\ Aj \ S . (?c Aj)) > 0 \ \

(F Ai | (\ Aj \ S . (?c Aj))) \ f Ai" using assms lovasz_inductive[of A F f G] by simp have base: "\ Ai. Ai \ A \ prob (F Ai) \ f Ai" using lovasz_inductive_base assms(4) assms(6) assms(5) assms(7) by blast show "prob (\ Ai \ A . (?c Ai)) \ (\ Ai \ A . (1 - f Ai))" using assms(3) assms(1) assms(2) assms(4) general base proof (induct A rule: finite_ne_induct) case (singleton x) then show ?case using singleton.prems singleton prob_compl by auto next case (insert x X) define Ax where "Ax = ?c ` (insert x X)" have xie: "F x \ events" using insert.prems by simp have A'ie: "\(?c ` X) \ events" using insert.prems insert.hyps by auto have "(\Ai S. Ai \ insert x X \ S \ insert x X - {Ai} \ S \ {} \ prob (\ Aj \ S . (?c Aj)) > 0 \ \

(F Ai | \ (?c ` S)) \ f Ai)" using insert.prems by simp then have "(\Ai S. Ai \ X \ S \ X - {Ai} \ S \ {} \ prob (\ Aj \ S . (?c Aj)) > 0 \ \

(F Ai | \ (?c ` S)) \ f Ai)" by auto then have A'gt: "(\Ai\X. 1 - f Ai) \ prob (\ (?c ` X))" using insert.hyps(4) insert.prems(2) insert.prems(1) insert.prems(4) by auto then have "prob (\(?c ` X)) > 0" using insert.hyps insert.prems prod_pos basic_trans_rules(22) diff_gt_0_iff_gt by (metis (no_types, lifting) insert_Diff insert_subset subset_insertI) then have "\

((?c x) | (\(?c ` X))) = 1 - \

(F x | (\(?c ` X)))" using cond_prob_neg[of "\(?c ` X)" "F x"] xie A'ie by simp moreover have "\

(F x | (\(?c ` X))) \ f x" using insert.prems(3)[of x X] insert.hyps(2) insert(3) A'gt \0 < prob (\ (?c ` X))\ by fastforce ultimately have pnxgt: "\

((?c x) | (\(?c ` X))) \ 1 - f x" by simp have xgt0: "1 - f x \ 0" using insert.prems(2)[of x] by auto have "prob (\ Ax) = prob ((?c x) \ \(?c ` X))" using Ax_def by simp also have "... = prob (\(?c ` X)) * \

((?c x) | (\(?c ` X)))" using prob_intersect_B xie A'ie by simp also have "... \ (\Ai\X. 1 - f Ai) * (1 - f x)" using A'gt pnxgt mult_left_le \0 < prob (\(?c ` X))\ xgt0 mult_mono by (smt(verit)) finally have "prob (\ Ax) \ (\Ai\insert x X. 1 - f Ai)" by (simp add: local.insert(1) local.insert(3) mult.commute) then show ?case using Ax_def by auto qed qed subsection \Lovasz Corollaries and Variations \ corollary lovasz_local_general_positive: assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "\ Ai . Ai \ A \ f Ai \ 0 \ f Ai < 1" assumes "dependency_digraph G M F" assumes "\ Ai. Ai \ A \ (prob (F Ai) \ (f Ai) * (\ Aj \ pre_digraph.neighborhood G Ai. (1 - (f Aj))))" assumes "pverts G = A" shows "prob (\ Ai \ A . (space M - (F Ai))) > 0" using assms lovasz_local_general(1)[of A F f G] lovasz_local_general(2)[of A F f G] by simp theorem lovasz_local_symmetric_dep_graph: fixes e :: real fixes d :: nat assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "dependency_digraph G M F" assumes "\ Ai. Ai \ A \ out_degree G Ai \ d" assumes "\ Ai. Ai \ A \ prob (F Ai) \ p" assumes "exp(1)* p * (d + 1) \ 1" (* e should be euler's number \ using exponential function? *) assumes "pverts G = A" shows "prob (\ Ai \ A . (space M - (F Ai))) > 0" proof (cases "d = 0") case True interpret g: dependency_digraph G M F using assms(4) by simp (* Because all have mutual independence \ complete independence *) have "indep_events F A" using g.dep_graph_indep_events[of A] assms(8) assms(5) True by simp moreover have "p < 1" proof - have "exp (1) * p \ 1" using assms(7) True by simp then show ?thesis using exp_gt_one less_1_mult linorder_neqE_linordered_idom rel_simps(68) verit_prod_simplify(2) by (smt (verit) mult_le_cancel_left1) qed ultimately show ?thesis using complete_indep_bound3[of A F] assms(2) assms(1) assms(3) assms(6) by force next case False define f :: "nat \ real" where "f \ (\ Ai . 1 /(d + 1))" then have fbounds: "\ Ai. f Ai \ 0 \ f Ai < 1" using f_def False by simp interpret dg: dependency_digraph G M F using assms(4) by auto (* Showing bound is the most work *) have "\ Ai. Ai \ A \ prob (F Ai) \ (f Ai) * (\ Aj \ dg.neighborhood Ai . (1 - (f Aj)))" proof - fix Ai assume ain: "Ai \ A" have d_boundslt1: "(1/(d + 1)) < 1" and d_boundsgt0: "(1/(d + 1))> 0" using False by fastforce+ have d_bounds2: "(1 - (1 /(d + 1)))^d < 1" using False by(simp add: field_simps) (smt (verit) of_nat_0_le_iff power_mono_iff) have d_bounds0: "(1 - (1 /(d + 1)))^d > 0" using False by (simp) - have "exp(1) > (1 + 1/d) powr d" using exp_1_bounds(1) False by simp + have "exp(1) > (1 + 1/d) powr d" using exp_1_gt_powr False by simp then have "exp(1) > (1 + 1/d)^d" using False by (simp add: powr_realpow zero_compare_simps(2)) moreover have "1/(1+ 1/d)^d = (1 - (1/(d+1)))^d" proof - have "1/(1+ 1/d)^d = 1/((d/d) + 1/d)^d" by (simp add: field_simps) then show ?thesis by (simp add: field_simps) qed ultimately have exp_lt: "1/exp(1) < (1 - (1 /(d + 1)))^d" by (metis d_bounds0 frac_less2 less_eq_real_def of_nat_zero_less_power_iff power_eq_if zero_less_divide_1_iff) then have "(1 /(d + 1))* (1 - (1 /(d + 1)))^d > (1 /(d + 1))*(1/exp(1))" using exp_lt mult_strict_left_mono[of "1/exp(1)" "(1 - (1 /(d + 1)))^d" "(1/(d+1))"] d_boundslt1 by simp then have "(1 /(d + 1))* (1 - (1 /(d + 1)))^d > (1/((d+1)*exp(1)))" by auto then have gtp: "(1 /(d + 1))* (1 - (1 /(d + 1)))^d > p" by (smt (verit, ccfv_SIG) d_boundslt1 d_boundsgt0 assms(7) divide_divide_eq_left divide_less_cancel divide_less_eq divide_nonneg_nonpos nonzero_mult_div_cancel_left not_exp_le_zero) have "card (dg.neighborhood Ai) \ d" using assms(5) dg.out_degree_neighborhood ain by auto then have "(\ Aj \ dg.neighborhood Ai . (1 - (1 /(d + 1)))) \ (1 - (1 /(d + 1)))^d" using prod_constant_ge[of "dg.neighborhood Ai" "d" "1 - (1/d+1)"] using d_boundslt1 by auto then have "(1 /(d + 1)) * (\ Aj \ dg.neighborhood Ai . (1 - (1 /(d + 1)))) \ (1 /(d + 1))* (1 - (1 /(d + 1)))^d" by (simp add: divide_right_mono) then have "(1 /(d + 1)) * (\ Aj \ dg.neighborhood Ai . (1 - (1 /(d + 1)))) > p" using gtp by simp then show "prob (F Ai) \ f Ai * (\ Aj \ dg.neighborhood Ai . (1 - f Aj))" using assms(6) \Ai \ A\ f_def by force qed then show ?thesis using lovasz_local_general_positive[of A F f G] assms(4) assms(1) assms(2) assms(3) assms(8) fbounds by auto qed corollary lovasz_local_symmetric4gt: fixes e :: real fixes d :: nat assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "dependency_digraph G M F" assumes "\ Ai. Ai \ A \ out_degree G Ai \ d" assumes "\ Ai. Ai \ A \ prob (F Ai) \ p" assumes "4 * p * d \ 1" (* only works if d \ge 3 *) assumes "d \ 3" assumes "pverts G = A" shows "prob (\ Ai \ A . (space M - F Ai)) > 0" proof - have "exp(1)* p * (d + 1) \ 1" proof (cases "p = 0") case True then show ?thesis by simp next case False then have pgt: "p > 0" using assms(1) assms(6) assms(3) ex_min_if_finite less_eq_real_def by (meson basic_trans_rules(23) basic_trans_rules(24) linorder_neqE_linordered_idom measure_nonneg) have "3 * (d + 1) \ 4 * d" by (simp add: field_simps assms(8)) then have "exp(1) * (d + 1) \ 4 *d" using exp_le exp_gt_one[of 1] assms(8) by (smt (verit, del_insts) Num.of_nat_simps(2) Num.of_nat_simps(5) le_add2 le_eq_less_or_eq mult_right_mono nat_less_real_le numeral.simps(3) numerals(1) of_nat_numeral) then have "exp(1) * (d + 1) * p \ 4 *d *p" using pgt by simp then show ?thesis using assms(7) by (simp add: field_simps) qed then show ?thesis using assms lovasz_local_symmetric_dep_graph[of A F G d p] by auto qed lemma lovasz_local_symmetric4: fixes e :: real fixes d :: nat assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "dependency_digraph G M F" assumes "\ Ai. Ai \ A \ out_degree G Ai \ d" assumes "\ Ai. Ai \ A \ prob (F Ai) \ p" assumes "4 * p * d \ 1" assumes "d \ 1" assumes "pverts G = A" shows "prob (\ Ai \ A . (space M - F Ai)) > 0" proof (cases "d \ 3") case True then show ?thesis using lovasz_local_symmetric4gt assms by presburger next case d3: False define f :: "nat \ real" where "f \ (\ Ai . 1 /(d + 1))" then have fbounds: "\ Ai. f Ai \ 0 \ f Ai < 1" using f_def assms(8) by simp interpret dg: dependency_digraph G M F using assms(4) by auto have "\ Ai. Ai \ A \ prob (F Ai) \ (f Ai) * (\ Aj \ dg.neighborhood Ai . (1 - (f Aj)))" proof - fix Ai assume ain: "Ai \ A" have d_boundslt1: "(1/(d + 1)) < 1" and d_boundsgt0: "(1/(d + 1))> 0" using assms by fastforce+ have plt: "1/(4*d) \ p" using assms(7) assms(8) by (metis (mono_tags, opaque_lifting) Num.of_nat_simps(5) bot_nat_0.not_eq_extremum le_numeral_extra(2) more_arith_simps(11) mult_of_nat_commute nat_0_less_mult_iff of_nat_0_less_iff of_nat_numeral pos_divide_less_eq rel_simps(51) verit_comp_simplify(3)) then have gtp: "(1 /(d + 1))* (1 - (1 /(d + 1)))^d \ p" proof (cases "d = 1") case False then have "d = 2" using d3 assms(8) by auto then show ?thesis using plt by (simp add: field_simps) qed (simp) have "card (dg.neighborhood Ai) \ d" using assms(5) dg.out_degree_neighborhood ain by auto then have "(\ Aj \ dg.neighborhood Ai . (1 - (1 /(d + 1)))) \ (1 - (1 /(d + 1)))^d" using prod_constant_ge[of "dg.neighborhood Ai" "d" "1 - (1/d+1)"] using d_boundslt1 by auto then have "(1 /(d + 1)) * (\ Aj \ dg.neighborhood Ai . (1 - (1 /(d + 1)))) \ (1 /(d + 1))* (1 - (1 /(d + 1)))^d" by (simp add: divide_right_mono) then have "(1 /(d + 1)) * (\ Aj \ dg.neighborhood Ai . (1 - (1 /(d + 1)))) \ p" using gtp by simp then show "prob (F Ai) \ f Ai * (\ Aj \ dg.neighborhood Ai . (1 - f Aj))" using assms(6) \Ai \ A\ f_def by force qed then show ?thesis using lovasz_local_general_positive[of A F f G] assms(4) assms(1) assms(2) assms(3) assms(9) fbounds by auto qed text \Converting between dependency graph and indexed set representation of mutual independence \ lemma (in pair_digraph) g_Ai_simplification: assumes "Ai \ A" assumes "g Ai \ A - {Ai}" assumes "pverts G = A" assumes "parcs G = {e \ A \ A . snd e \ (A - ({fst e} \ (g (fst e))))}" shows "g Ai = A - ({Ai} \ neighborhood Ai)" proof - have "g Ai = A - ({Ai} \ {v \ A . v \ (A - ({Ai} \ (g (Ai))))})" using assms(2) by auto then have "g Ai = A - ({Ai} \ {v \ A . (Ai, v) \ parcs G})" using Collect_cong assms(1) mem_Collect_eq assms(3) assms(4) by auto then show "g Ai = A - ({Ai} \ neighborhood Ai)" unfolding neighborhood_def using assms(3) by simp qed lemma define_dep_graph_set: assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "\ Ai. Ai \ A \ g Ai \ A - {Ai} \ mutual_indep_events (F Ai) F (g Ai)" shows "dependency_digraph \ pverts = A, parcs = {e \ A \ A . snd e \ (A - ({fst e} \ (g (fst e))))} \ M F" (is "dependency_digraph ?G M F") proof - interpret pd: pair_digraph ?G using assms(3)by (unfold_locales) auto have "\ Ai. Ai \ A \ g Ai \ A - {Ai}" using assms(4) by simp then have "\ i. i \ A \ g i = A - ({i} \ pd.neighborhood i)" using pd.g_Ai_simplification[of _ A g] pd.pair_digraph by auto then have "dependency_digraph ?G M F" using assms(2) assms(4) by (unfold_locales) auto then show ?thesis by simp qed lemma define_dep_graph_deg_bound: assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "\ Ai. Ai \ A \ g Ai \ A - {Ai} \ card (g Ai) \ card A - d - 1 \ mutual_indep_events (F Ai) F (g Ai)" shows "\ Ai. Ai \ A \ out_degree \ pverts = A, parcs = {e \ A \ A . snd e \ (A - ({fst e} \ (g (fst e))))} \ Ai \ d" (is "\ Ai. Ai \ A \ out_degree (with_proj ?G) Ai \ d") proof - interpret pd: dependency_digraph ?G M F using assms define_dep_graph_set by simp show "\ Ai. Ai \ A \ out_degree ?G Ai \ d" proof - fix Ai assume a: "Ai \ A" then have geq: "g Ai = A - ({Ai} \ pd.neighborhood Ai)" using assms(4)[of Ai] pd.pair_digraph pd.g_Ai_simplification[of Ai A g ] by simp then have pss: "g Ai \ A" using a by auto then have "card (g Ai) = card (A - ({Ai} \ pd.neighborhood Ai))" using assms(4) geq by argo moreover have ss: "({Ai} \ pd.neighborhood Ai) \ A" using pd.neighborhood_wf a by simp moreover have "finite ({Ai} \ pd.neighborhood Ai)" using calculation(2) assms(3) finite_subset by auto moreover have "Ai \ pd.neighborhood Ai" using pd.neighborhood_self_not by simp moreover have "card {Ai} = 1" using is_singleton_altdef by auto moreover have cardss: "card ({Ai} \ pd.neighborhood Ai) = 1 + card (pd.neighborhood Ai)" using calculation(5) calculation(4) card_Un_disjoint pd.neighborhood_finite by auto ultimately have eq: "card (g Ai) = card A - 1 - card (pd.neighborhood Ai)" using card_Diff_subset[of "({Ai} \ pd.neighborhood Ai)" A] assms(3) by presburger have ggt: "\ Ai. Ai \ A \ card (g Ai) \ int (card A) - int d - 1" using assms(4) by fastforce have "card (pd.neighborhood Ai) = card A - 1 - card (g Ai)" using cardss assms(3) card_mono diff_add_inverse diff_diff_cancel diff_le_mono ss eq by (metis (no_types, lifting)) moreover have "card A \ (1 + card (g Ai))" using pss assms(3) card_seteq not_less_eq_eq by auto ultimately have "card (pd.neighborhood Ai) = int (card A) - 1 - int (card (g Ai))" by auto moreover have "int (card (g Ai)) \ (card A) - (int d) - 1" using ggt a by simp ultimately show "out_degree ?G Ai \ d" using pd.out_degree_neighborhood by simp qed qed lemma obtain_dependency_graph: assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "\ Ai. Ai \ A \ (\ S . S \ A - {Ai} \ card S \ card A - d - 1 \ mutual_indep_events (F Ai) F S)" obtains G where "dependency_digraph G M F" "pverts G = A" "\ Ai. Ai \ A \ out_degree G Ai \ d" proof - obtain g where gdef: "\ Ai. Ai \ A \ g Ai \ A - {Ai} \ card (g Ai) \ card A - d - 1 \ mutual_indep_events (F Ai) F (g Ai)" using assms(4) by metis then show ?thesis using define_dep_graph_set[of A F g] define_dep_graph_deg_bound[of A F g d]that assms by auto qed text \This is the variation of the symmetric version most commonly in use \ theorem lovasz_local_symmetric: fixes d :: nat assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "\ Ai. Ai \ A \ (\ S . S \ A - {Ai} \ card S \ card A - d - 1 \ mutual_indep_events (F Ai) F S)" assumes "\ Ai. Ai \ A \ prob (F Ai) \ p" assumes "exp(1)* p * (d + 1) \ 1" shows "prob (\ Ai \ A . (space M - (F Ai))) > 0" proof - obtain G where odg: "dependency_digraph G M F" "pverts G = A" "\ Ai. Ai \ A \ out_degree G Ai \ d" using assms obtain_dependency_graph by metis then show ?thesis using odg assms lovasz_local_symmetric_dep_graph[of A F G d p] by auto qed lemma lovasz_local_symmetric4_set: fixes d :: nat assumes "A \ {}" assumes "F ` A \ events" assumes "finite A" assumes "\ Ai. Ai \ A \ (\ S . S \ A - {Ai} \ card S \ card A - d - 1 \ mutual_indep_events (F Ai) F S)" assumes "\ Ai. Ai \ A \ prob (F Ai) \ p" assumes "4 * p * d \ 1" assumes "d \ 1" shows "prob (\ Ai \ A . (space M - F Ai)) > 0" proof - obtain G where odg: "dependency_digraph G M F" "pverts G = A" "\ Ai. Ai \ A \ out_degree G Ai \ d" using assms obtain_dependency_graph by metis then show ?thesis using odg assms lovasz_local_symmetric4[of A F G d p] by auto qed end end \ No newline at end of file