diff --git a/thys/Concentration_Inequalities/Bennett_Inequality.thy b/thys/Concentration_Inequalities/Bennett_Inequality.thy new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/Bennett_Inequality.thy @@ -0,0 +1,550 @@ +section \Bennett's Inequality\ + +text \In this section we verify Bennett's inequality~\cite{bennett1962} and a (weak) version of +Bernstein's inequality as a corollary. Both inequalities give concentration bounds for sums of +independent random variables. The statement and proofs follow a summary paper by +Boucheron et al.~\cite{DBLP:conf/ac/BoucheronLB03}.\ + +theory Bennett_Inequality + imports Concentration_Inequalities_Preliminary +begin + +context prob_space +begin + +(* Restating Chernoff inequality for independent variables *) +lemma indep_vars_Chernoff_ineq_ge: + assumes I: "finite I" + assumes ind: "indep_vars (\ _. borel) X I" + assumes sge: "s \ 0" + assumes int: "\i. i \ I \ integrable M (\x. exp (s * X i x))" + shows "prob {x \ space M. (\i \I. X i x - expectation (X i)) \ t} \ + exp (-s*t) * + (\i\I. expectation (\x. exp(s * (X i x - expectation (X i)))))" +proof (cases "s = 0") + case [simp]: True + thus ?thesis + by (simp add: prob_space) +next + case False + then have s: "s > 0" using sge by auto + + have [measurable]: "\i. i \ I \ random_variable borel (X i)" + using ind unfolding indep_vars_def by blast + + have indep1: "indep_vars (\_. borel) + (\i \. exp (s * (X i \ - expectation (X i)))) I" + apply (intro indep_vars_compose[OF ind, unfolded o_def]) + by auto + + define S where "S = (\x. (\i \I. X i x - expectation (X i)))" + + have int1: "\i. i \ I \ + integrable M (\\. exp (s * (X i \ - expectation (X i))))" + by (auto simp add: algebra_simps exp_diff int) + + have eprod: "\x. exp (s * S x) = (\i\I. exp(s * (X i x - expectation (X i))))" + unfolding S_def + by (simp add: assms(1) exp_sum vector_space_over_itself.scale_sum_right) + + from indep_vars_integrable[OF I indep1 int1] + have intS: "integrable M (\x. exp (s * S x))" + unfolding eprod by auto + + then have si: "set_integrable M (space M) (\x. exp (s * S x))" + unfolding set_integrable_def + apply (intro integrable_mult_indicator) + by auto + + from Chernoff_ineq_ge[OF s si] + have "prob {x \ space M. S x \ t} \ exp (- s * t) * (\x\space M. exp (s * S x)\M)" + by auto + + also have "(\x\space M. exp (s * S x)\M) = expectation (\x. exp(s * S x))" + unfolding set_integral_space[OF intS] by auto + + also have "... = expectation (\x. \i\I. exp(s * (X i x - expectation (X i))))" + unfolding S_def + by (simp add: assms(1) exp_sum vector_space_over_itself.scale_sum_right) + also have "... = (\i\I. expectation (\x. exp(s * (X i x - expectation (X i)))))" + apply (intro indep_vars_lebesgue_integral[OF I indep1 int1]) . + finally show ?thesis + unfolding S_def + by auto +qed + +definition bennett_h::"real \ real" + where "bennett_h u = (1 + u) * ln (1 + u) - u" + +lemma exp_sub_two_terms_eq: + fixes x :: real + shows "exp x - x - 1 = (\n. x^(n+2) / fact (n+2))" + "summable (\n. x^(n+2) / fact (n+2))" +proof - + have "(\i<2. inverse (fact i) * x ^ i) = 1 + x" + by (simp add:numeral_eq_Suc) + thus "exp x - x - 1 = (\n. x^(n+2) / fact (n+2))" + unfolding exp_def + apply (subst suminf_split_initial_segment[where k = 2]) + by (auto simp add: summable_exp divide_inverse_commute) + have "summable (\n. x^n / fact n)" + by (simp add: divide_inverse_commute summable_exp) + then have "summable (\n. x^(Suc (Suc n)) / fact (Suc (Suc n)))" + apply (subst summable_Suc_iff) + apply (subst summable_Suc_iff) + by auto + thus "summable (\n. x^(n+2) / fact (n+2))" by auto +qed + +lemma psi_mono: + defines "f \ (\x. (exp x - x - 1) - x^2 / 2)" + assumes xy: "a \ (b::real)" + shows "f a \ f b" +proof - + have 1: "(f has_real_derivative (exp x - x - 1)) (at x)" for x + unfolding f_def + by (auto intro!: derivative_eq_intros) + + have 2: "\x. x \ {a..b} \ 0 \ exp x - x - 1" + by (smt (verit) exp_ge_add_one_self) + + from deriv_nonneg_imp_mono[OF 1 2 xy] + show ?thesis by auto +qed + +(* TODO: not sure if this holds for y < 0 too *) +lemma psi_inequality: + assumes le: "x \ (y::real)" "y \ 0" + shows "y^2 * (exp x - x - 1) \ x^2 * (exp y - y - 1)" +proof - + + have x: "exp x - x - 1 = (\n. (x^(n+2) / fact (n+2)))" + "summable (\n. x^(n+2) / fact (n+2))" + using exp_sub_two_terms_eq . + + have y: "exp y - y - 1 = (\n. (y^(n+2) / fact (n+2)))" + "summable (\n. y^(n+2) / fact (n+2))" + using exp_sub_two_terms_eq . + + (* Simplify the expressions in the inequality *) + have l:"y^2 * (exp x - x - 1) = (\n. y^2 * (x^(n+2) / fact (n+2)))" + using x + apply (subst suminf_mult) + by auto + have ls: "summable (\n. y^2 * (x^(n+2) / fact (n+2)))" + by (intro summable_mult[OF x(2)]) + + have r:"x^2 * (exp y - y - 1) = (\n. x^2 * (y^(n+2) / fact (n+2)))" + using y + apply (subst suminf_mult) + by auto + have rs: "summable (\n. x^2 * (y^(n+2) / fact (n+2)))" + by (intro summable_mult[OF y(2)]) + + have "\x\ \ \y\ \ \y\ < \x\" by auto + moreover { + assume "\x\ \ \y\" + then have "x^ n \ y ^n" for n + by (smt (verit, ccfv_threshold) bot_nat_0.not_eq_extremum le power_0 real_root_less_mono real_root_power_cancel root_abs_power) + then have "(x^2 * y^2) * x^n \ (x^2 * y^2) * y^n" for n + by (simp add: mult_left_mono) + then have "y\<^sup>2 * (x ^ (n + 2)) \ x\<^sup>2 * (y ^ (n + 2))" for n + by (metis (full_types) ab_semigroup_mult_class.mult_ac(1) mult.commute power_add) + then have "y\<^sup>2 * (x ^ (n + 2)) / fact (n+2)\ x\<^sup>2 * (y ^ (n + 2)) / fact (n+2)" for n + by (meson divide_right_mono fact_ge_zero) + then have "(\n. y^2 * (x^(n+2) / fact (n+2))) \ (\n. x^2 * (y^(n+2) / fact (n+2)))" + apply (intro suminf_le[OF _ ls rs]) + by auto + then have "y^2 * (exp x - x - 1) \ x^2 * (exp y - y - 1)" + using l r by presburger + } + moreover { + assume ineq: "\y\ < \x\" + + from psi_mono[OF assms(1)] + have "(exp x - x - 1) - x^2 /2 \ (exp y - y - 1) - y^2/2" . + + then have "y^2 * ((exp x - x - 1) - x^2 /2) \ x^2 * ((exp y - y - 1) - y^2/2)" + by (smt (verit, best) ineq diff_divide_distrib exp_lower_Taylor_quadratic le(1) le(2) mult_nonneg_nonneg one_less_exp_iff power_zero_numeral prob_space.psi_mono prob_space_completion right_diff_distrib zero_le_power2) + + then have "y^2 * (exp x - x - 1) \ x^2 * (exp y - y - 1)" + by (simp add: mult.commute right_diff_distrib) + } + ultimately show ?thesis by auto +qed + +(* Helper lemma, starting with normalized variables *) +lemma bennett_inequality_1: + assumes I: "finite I" + assumes ind: "indep_vars (\ _. borel) X I" + assumes intsq: "\i. i \ I \ integrable M (\x. (X i x)^2)" + assumes bnd: "\i. i \ I \ AE x in M. X i x \ 1" + assumes t: "t \ 0" + defines "V \ (\i \ I. expectation(\x. X i x^2))" + shows "prob {x \ space M. (\i \ I. X i x - expectation (X i)) \ t} \ + exp (-V * bennett_h (t / V))" +proof (cases "V = 0") + case True + then show ?thesis + by auto +next + case f: False + have "V \ 0" + unfolding V_def + apply (intro sum_nonneg integral_nonneg_AE) + by auto + then have Vpos: "V > 0" using f by auto + + define l :: real where "l = ln(1 + t / V)" + then have l: "l \ 0" + using t Vpos by auto + have rv[measurable]: "\i. i \ I \ random_variable borel (X i)" + using ind unfolding indep_vars_def by blast + + define \ where "\ = (\x::real. exp(x) - x - 1)" + + have rw: "exp y = 1 + y + \ y" for y + unfolding \_def by auto + + have ebnd: "\i. i \ I \ + AE x in M. exp (l * X i x) \ exp l" + apply (drule bnd) + using l by (auto simp add: mult_left_le) + + (* integrability *) + have int: "\i. i \ I \ integrable M (\x. (X i x))" + using rv intsq square_integrable_imp_integrable by blast + + have intl: "\i. i \ I \ integrable M (\x. (l * X i x))" + using int by blast + + have intexpl: "\i. i \ I \ integrable M (\x. exp (l * X i x))" + apply (intro integrable_const_bound[where B = "exp l"]) + using ebnd by auto + + have intpsi: "\i. i \ I \ integrable M (\x. \ (l * X i x))" + unfolding \_def + using intl intexpl by auto + + have **: "\i. i \ I \ + expectation (\x. \ (l * X i x)) \ \ l * expectation (\x. (X i x)^2)" + proof - + fix i assume i: "i \ I" + then have "AE x in M. l * X i x \ l" + using ebnd by auto + then have "AE x in M. l^2 * \ (l * X i x) \ (l * X i x)^2 * \ l" + using psi_inequality[OF _ l] unfolding \_def + by auto + then have "AE x in M. l^2 * \ (l * X i x) \ l^2 * (\ l * (X i x)^2)" + by (auto simp add: field_simps) + then have "AE x in M. \ (l * X i x) \ \ l * (X i x)^2 " + by (smt (verit, best) AE_cong \_def exp_eq_one_iff mult_cancel_left mult_eq_0_iff mult_left_mono zero_eq_power2 zero_le_power2) + then have "AE x in M. 0 \ \ l * (X i x)^2 - \ (l * X i x) " + by auto + then have "expectation (\x. \ l * (X i x)^2 + (- \ (l * X i x))) \ 0" + by (simp add: integral_nonneg_AE) + also have "expectation (\x. \ l * (X i x)^2 + (- \ (l * X i x))) = + \ l * expectation (\x. (X i x)^2) - expectation (\x. \ (l * X i x))" + apply (subst Bochner_Integration.integral_add) + using intpsi[OF i] intsq[OF i] by auto + finally show "expectation (\x. \ (l * X i x)) \ \ l * expectation (\x. (X i x)^2)" + by auto + qed + + (* Analyzing the expectation *) + then have *: "\i. i \ I \ + expectation (\x. exp (l * X i x)) \ + exp (l * expectation (X i)) * exp (\ l * expectation (\x. X i x^2))" + proof - + fix i + assume iI: "i \ I" + have "expectation (\x. exp (l * X i x)) = + 1 + l * expectation (\x. X i x) + + expectation (\x. \ (l * X i x))" + unfolding rw + apply (subst Bochner_Integration.integral_add) + using iI intl intpsi apply auto[2] + apply (subst Bochner_Integration.integral_add) + using intl iI prob_space by auto + also have "... = l * expectation (X i) + 1 + expectation (\x. \ (l * X i x))" + by auto + also have "... \ 1 + l * expectation (X i) + \ l * expectation (\x. X i x^2)" + using **[OF iI] by auto + also have "... \ exp (l * expectation (X i)) * exp (\ l * expectation (\x. X i x^2))" + by (simp add: is_num_normalize(1) mult_exp_exp) + finally show "expectation (\x. exp (l * X i x)) \ + exp (l * expectation (X i)) * exp (\ l * expectation (\x. X i x^2))" . + qed + + have "(\i\I. expectation (\x. exp (l * (X i x)))) \ + (\i\I. exp (l * expectation (X i)) * exp (\ l * expectation (\x. X i x^2)))" + by (auto intro!: prod_mono simp add: *) + also have "... = + (\i\I. exp (l * expectation (X i))) * (\i\I. exp (\ l * expectation (\x. X i x^2)))" + by (auto simp add: prod.distrib) + finally have **: + "(\i\I. expectation (\x. exp (l * (X i x)))) \ + (\i\I. exp (l * expectation (X i))) * exp (\ l * V)" + by (simp add: V_def I exp_sum sum_distrib_left) + + from indep_vars_Chernoff_ineq_ge[OF I ind l intexpl] + have "prob {x \ space M. (\i \ I. X i x - expectation (X i)) \ t} \ + exp (- l * t) * + (\i\I. expectation (\x. exp (l * (X i x - expectation (X i)))))" + by auto + also have "(\i\I. expectation (\x. exp (l * (X i x - expectation (X i))))) = + (\i\I. expectation (\x. exp (l * (X i x))) * exp (- l * expectation (X i)))" + by (auto intro!: prod.cong simp add: field_simps exp_diff exp_minus_inverse) + also have "... = + (\i\I. exp (- l * expectation (X i))) * (\i\I. expectation (\x. exp (l * (X i x))))" + by (auto simp add: prod.distrib) + also have "... \ + (\i\I. exp (- l * expectation (X i))) * ((\i\I. exp (l * expectation (X i))) * exp (\ l * V))" + apply (intro mult_left_mono[OF **]) + by (meson exp_ge_zero prod_nonneg) + also have "... = exp (\ l * V)" + apply (simp add: prod.distrib [symmetric]) + by (smt (verit, ccfv_threshold) exp_minus_inverse prod.not_neutral_contains_not_neutral) + finally have " + prob {x \ space M. (\i \ I. X i x - expectation (X i)) \ t} \ + exp (\ l * V - l * t)" + by (simp add:mult_exp_exp) + also have "\ l * V - l * t = -V * bennett_h (t / V)" + unfolding \_def l_def bennett_h_def + apply (subst exp_ln) + subgoal by (smt (verit) Vpos divide_nonneg_nonneg t) + by (auto simp add: algebra_simps) + finally show ?thesis . +qed + +lemma real_AE_le_sum: + assumes "\i. i \ I \ AE x in M. f i x \ (g i x::real)" + shows "AE x in M. (\i\I. f i x) \ (\i\I. g i x)" +proof (cases) + assume "finite I" + with AE_finite_allI[OF this assms] have 0:"AE x in M. (\i\I. f i x \ g i x)" by auto + show ?thesis by (intro eventually_mono[OF 0] sum_mono) auto +qed simp + +lemma real_AE_eq_sum: + assumes "\i. i \ I \ AE x in M. f i x = (g i x::real)" + shows "AE x in M. (\i\I. f i x) = (\i\I. g i x)" +proof - + have 1: "AE x in M. (\i\I. f i x) \ (\i\I. g i x)" + apply (intro real_AE_le_sum) + apply (drule assms) + by auto + have 2: "AE x in M. (\i\I. g i x) \ (\i\I. f i x)" + apply (intro real_AE_le_sum) + apply (drule assms) + by auto + show ?thesis + using 1 2 + by auto +qed + +(* B = 0 case trivial *) +theorem bennett_inequality: + assumes I: "finite I" + assumes ind: "indep_vars (\ _. borel) X I" + assumes intsq: "\i. i \ I \ integrable M (\x. (X i x)^2)" + assumes bnd: "\i. i \ I \ AE x in M. X i x \ B" + assumes t: "t \ 0" + assumes B: "B > 0" + defines "V \ (\i \ I. expectation (\x. X i x^2))" + shows "prob {x \ space M. (\i \ I. X i x - expectation (X i)) \ t} \ + exp (- V / B^2 * bennett_h (t * B / V))" +proof - + define Y where "Y = (\i x. X i x / B)" + + from indep_vars_compose[OF ind, where Y = "\i x. x/ B"] + have 1: "indep_vars (\_. borel) Y I" + unfolding Y_def by (auto simp add: o_def) + have 2: "\i. i \ I \ integrable M (\x. (Y i x)\<^sup>2)" + unfolding Y_def apply (drule intsq) + by (auto simp add: field_simps) + have 3: "\i. i \ I \ AE x in M. Y i x \ 1" + unfolding Y_def apply (drule bnd) + using B by auto + have 4:"0 \ t / B" using t B by auto + + have rw1: "(\i\I. Y i x - expectation (Y i)) = + (\i\I. X i x - expectation (X i)) / B" for x + unfolding Y_def + by (auto simp: diff_divide_distrib sum_divide_distrib) + + have rw2: "expectation (\x. (Y i x)\<^sup>2) = + expectation (\x. (X i x)\<^sup>2) / B^2" for i + unfolding Y_def + by (simp add: power_divide) + + have rw3:"- (\i\I. expectation (\x. (X i x)\<^sup>2) / B^2) = - V / B^2" + unfolding V_def + by (auto simp add: sum_divide_distrib) + + have "t / B / (\i\I. expectation (\x. (X i x)\<^sup>2) / B^2) = + t / B / (V / B^2)" + unfolding V_def + by (auto simp add: sum_divide_distrib) + then have rw4: "t / B / (\i\I. expectation (\x. (X i x)\<^sup>2) / B^2) = + t * B / V" + by (simp add: power2_eq_square) + have "prob {x \ space M. t \ (\i\I. X i x - expectation (X i))} = + prob{x \ space M. t / B \ (\i\I. X i x - expectation (X i)) / B}" + by (smt (verit, best) B Collect_cong divide_cancel_right divide_right_mono) + also have "... \ + exp (- V / B\<^sup>2 * + bennett_h (t * B / V))" + using bennett_inequality_1[OF I 1 2 3 4] + unfolding rw1 rw2 rw3 rw4 . + finally show ?thesis . +qed + +(* This proof follows https://math.stackexchange.com/a/4066844 *) +lemma bennett_h_bernstein_bound: + assumes "x \ 0" + shows "bennett_h x \ x^2 / (2 * (1 + x / 3))" +proof - + have eq:"x^2 / (2 * (1 + x / 3)) = 3/2 * x - 9/2 * (x / (x+3))" + using assms + by (sos "(() & ())") + + define g where "g = (\x. bennett_h x - (3/2 * x - 9/2 * (x / (x+3))))" + + define g' where "g' = (\x::real. + ln(1 + x) + 27 / (2 * (x+3)^2) - 3 / 2)" + define g'' where "g'' = (\x::real. + 1 / (1 + x) - 27 / (x+3)^3)" + + have "54 / ((2 * x + 6)^2) = 27 / (2 * (x + 3)\<^sup>2)" (is "?L = ?R") for x :: real + proof - + have "?L = 54 / (2^2 * (x + 3)^2)" + unfolding power_mult_distrib[symmetric] by (simp add:algebra_simps) + also have "... = ?R" by simp + finally show ?thesis by simp + qed + + hence 1: "x \ 0 \ (g has_real_derivative (g' x)) (at x)" for x + unfolding g_def g'_def bennett_h_def by (auto intro!: derivative_eq_intros simp:power2_eq_square) + have 2: "x \ 0 \ (g' has_real_derivative (g'' x)) (at x)" for x + unfolding g'_def g''_def + apply (auto intro!: derivative_eq_intros)[1] + by (sos "(() & ())") + + have gz: "g 0 = 0" + unfolding g_def bennett_h_def by auto + have g1z: "g' 0 = 0" + unfolding g'_def by auto + + have p2: "g'' x \ 0" if "x \ 0" for x + proof - + have "27 * (1+x) \ (x+3)^3" + using that unfolding power3_eq_cube by (auto simp:algebra_simps) + hence " 27 / (x + 3) ^ 3 \ 1 / (1+x)" + using that by (subst frac_le_eq) (auto intro!:divide_nonpos_pos) + thus ?thesis unfolding g''_def by simp + qed + + from deriv_nonneg_imp_mono[OF 2 p2 _] + have "x \ 0 \ g' x \ 0" for x using g1z + by (metis atLeastAtMost_iff) + + from deriv_nonneg_imp_mono[OF 1 this _] + have "x \ 0 \ g x \ 0" for x using gz + by (metis atLeastAtMost_iff) + + thus ?thesis + using assms eq g_def by force +qed + +lemma sum_sq_exp_eq_zero_imp_zero: + assumes "finite I" "i \ I" + assumes intsq: "integrable M (\x. (X i x)^2)" + assumes "(\i \ I. expectation (\x. X i x^2)) = 0" + shows "AE x in M. X i x = (0::real)" +proof - + have "(\i \I. expectation (\x. X i x^2) = 0)" + using assms + apply (subst sum_nonneg_eq_0_iff[symmetric]) + by auto + then have "expectation (\x. X i x^2) = 0" + using assms(2) by blast + thus ?thesis + using integral_nonneg_eq_0_iff_AE[OF intsq] + by auto +qed + +corollary bernstein_inequality: + assumes I: "finite I" + assumes ind: "indep_vars (\ _. borel) X I" + assumes intsq: "\i. i \ I \ integrable M (\x. (X i x)^2)" + assumes bnd: "\i. i \ I \ AE x in M. X i x \ B" + assumes t: "t \ 0" + assumes B: "B > 0" + defines "V \ (\i \ I. expectation (\x. X i x^2))" + shows "prob {x \ space M. (\i \ I. X i x - expectation (X i)) \ t} \ + exp (- (t^2 / (2 * (V + t * B / 3))))" +proof (cases "V = 0") + case True + then have 1:"\i. i \ I \ AE x in M. X i x = 0" + unfolding V_def + using sum_sq_exp_eq_zero_imp_zero + by (metis I intsq) + then have 2:"\i. i \ I \ expectation (X i) = 0" + using integral_eq_zero_AE by blast + + have "AE x in M. (\i \ I. X i x - expectation (X i)) = (\i \ I. 0)" + apply (intro real_AE_eq_sum) + using 1 2 + by auto + then have *: "AE x in M. (\i \ I. X i x - expectation (X i)) = 0" + by force + + moreover { + assume "t > 0" + then have "prob {x \ space M. (\i \ I. X i x - expectation (X i)) \ t} = 0" + apply (intro prob_eq_0_AE) + using * by auto + then have ?thesis by auto + } + ultimately show ?thesis + apply (cases "t = 0") using t by auto +next + case f: False + have "V \ 0" + unfolding V_def + apply (intro sum_nonneg integral_nonneg_AE) + by auto + then have V: "V > 0" using f by auto + + have "t * B / V \ 0" using t B V by auto + from bennett_h_bernstein_bound[OF this] + have "(t * B / V)\<^sup>2 / (2 * (1 + t * B / V / 3)) + \ bennett_h (t * B / V)" . + + then have "(- V / B^2) * bennett_h (t * B / V) \ + (- V / B^2) * ((t * B / V)\<^sup>2 / (2 * (1 + t * B / V / 3)))" + apply (subst mult_left_mono_neg) + using B V by auto + also have "... = + ((- V / B^2) * (t * B / V)\<^sup>2) / (2 * (1 + t * B / V / 3))" + by auto + also have " ((- V / B^2) * (t * B / V)\<^sup>2) = -(t^2) / V" + using V B by (auto simp add: field_simps power2_eq_square) + finally have *: "(- V / B^2) * bennett_h (t * B / V) \ + -(t^2) / (2 * (V + t * B / 3))" + using V by (auto simp add: field_simps) + + from bennett_inequality[OF assms(1-6)] + have "prob {x \ space M. (\i \ I. X i x - expectation (X i)) \ t} \ + exp (- V / B^2 * bennett_h (t * B / V))" + using V_def by auto + also have "... \ exp (- (t^2/ (2 * (V + t * B / 3))))" + using * + by auto + finally show ?thesis . +qed + +end + +end diff --git a/thys/Concentration_Inequalities/Bienaymes_Identity.thy b/thys/Concentration_Inequalities/Bienaymes_Identity.thy new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/Bienaymes_Identity.thy @@ -0,0 +1,181 @@ +section \Bienaym\'e's identity\ + +text \Bienaym\'e's identity~\cite[\S 17]{loeve1977} can be used to deduce the variance of a sum of +random variables, if their co-variance is known. A common use-case of the identity is the +computation of the variance of the mean of pair-wise independent variables.\ + +theory Bienaymes_Identity + imports Concentration_Inequalities_Preliminary +begin + +context prob_space +begin + +lemma variance_divide: + fixes f :: "'a \ real" + assumes "integrable M f" + shows "variance (\\. f \ / r) = variance f / r^2" + using assms + by (subst Bochner_Integration.integral_divide[OF assms(1)]) + (simp add:diff_divide_distrib[symmetric] power2_eq_square algebra_simps) + +definition covariance where + "covariance f g = expectation (\\. (f \ - expectation f) * (g \ - expectation g))" + +lemma covariance_eq: + fixes f :: "'a \ real" + assumes "f \ borel_measurable M" "g \ borel_measurable M" + assumes "integrable M (\\. f \^2)" "integrable M (\\. g \^2)" + shows "covariance f g = expectation (\\. f \ * g \) - expectation f * expectation g" +proof - + have "integrable M f" using square_integrable_imp_integrable assms by auto + moreover have "integrable M g" using square_integrable_imp_integrable assms by auto + ultimately show ?thesis + using assms cauchy_schwartz(1)[where M="M"] + by (simp add:covariance_def algebra_simps prob_space) +qed + +lemma covar_integrable: + fixes f g :: "'a \ real" + assumes "f \ borel_measurable M" "g \ borel_measurable M" + assumes "integrable M (\\. f \^2)" "integrable M (\\. g \^2)" + shows "integrable M (\\. (f \ - expectation f) * (g \ - expectation g))" +proof - + have "integrable M f" using square_integrable_imp_integrable assms by auto + moreover have "integrable M g" using square_integrable_imp_integrable assms by auto + ultimately show ?thesis using assms cauchy_schwartz(1)[where M="M"] by (simp add: algebra_simps) +qed + +lemma sum_square_int: + fixes f :: "'b \ 'a \ real" + assumes "finite I" + assumes "\i. i \ I \ f i \ borel_measurable M" + assumes "\i. i \ I \ integrable M (\\. f i \^2)" + shows "integrable M (\\. (\i \ I. f i \)\<^sup>2)" +proof - + have " integrable M (\\. \i\I. \j\I. f j \ * f i \)" + using assms + by (intro Bochner_Integration.integrable_sum cauchy_schwartz(1)[where M="M"], auto) + thus ?thesis + by (simp add:power2_eq_square sum_distrib_left sum_distrib_right) +qed + +theorem bienaymes_identity: + fixes f :: "'b \ 'a \ real" + assumes "finite I" + assumes "\i. i \ I \ f i \ borel_measurable M" + assumes "\i. i \ I \ integrable M (\\. f i \^2)" + shows + "variance (\\. (\i \ I. f i \)) = (\i \ I. (\j \ I. covariance (f i) (f j)))" +proof - + have a:"\i j. i \ I \ j \ I \ + integrable M (\\. (f i \ - expectation (f i)) * (f j \ - expectation (f j)))" + using assms covar_integrable by simp + have "variance (\\. (\i \ I. f i \)) = expectation (\\. (\i\I. f i \ - expectation (f i))\<^sup>2)" + using square_integrable_imp_integrable[OF assms(2,3)] + by (simp add: Bochner_Integration.integral_sum sum_subtractf) + also have "... = expectation (\\. (\i \ I. (\j \ I. + (f i \ - expectation (f i)) * (f j \ - expectation (f j)))))" + by (simp add: power2_eq_square sum_distrib_right sum_distrib_left mult.commute) + also have "... = (\i \ I. (\j \ I. covariance (f i) (f j)))" + using a by (simp add: Bochner_Integration.integral_sum covariance_def) + finally show ?thesis by simp +qed + +lemma covar_self_eq: + fixes f :: "'a \ real" + shows "covariance f f = variance f" + by (simp add:covariance_def power2_eq_square) + +lemma covar_indep_eq_zero: + fixes f g :: "'a \ real" + assumes "integrable M f" + assumes "integrable M g" + assumes "indep_var borel f borel g" + shows "covariance f g = 0" +proof - + have a:"indep_var borel ((\t. t - expectation f) \ f) borel ((\t. t - expectation g) \ g)" + by (rule indep_var_compose[OF assms(3)], auto) + + have b:"expectation (\\. (f \ - expectation f) * (g \ - expectation g)) = 0" + using a assms by (subst indep_var_lebesgue_integral, auto simp add:comp_def prob_space) + + thus ?thesis by (simp add:covariance_def) +qed + +lemma bienaymes_identity_2: + fixes f :: "'b \ 'a \ real" + assumes "finite I" + assumes "\i. i \ I \ f i \ borel_measurable M" + assumes "\i. i \ I \ integrable M (\\. f i \^2)" + shows "variance (\\. (\i \ I. f i \)) = + (\i \ I. variance (f i)) + (\i \ I. \j \ I - {i}. covariance (f i) (f j))" +proof - + have "variance (\\. (\i \ I. f i \)) = (\i\I. \j\I. covariance (f i) (f j))" + by (simp add: bienaymes_identity[OF assms(1,2,3)]) + also have "... = (\i\I. covariance (f i) (f i) + (\j\I-{i}. covariance (f i) (f j)))" + using assms by (subst sum.insert[symmetric], auto simp add:insert_absorb) + also have "... = (\i\I. variance (f i)) + (\i \ I. (\j\I-{i}. covariance (f i) (f j)))" + by (simp add: covar_self_eq[symmetric] sum.distrib) + finally show ?thesis by simp +qed + +theorem bienaymes_identity_pairwise_indep: + fixes f :: "'b \ 'a \ real" + assumes "finite I" + assumes "\i. i \ I \ f i \ borel_measurable M" + assumes "\i. i \ I \ integrable M (\\. f i \^2)" + assumes "\i j. i \ I \ j \ I \ i \ j \ indep_var borel (f i) borel (f j)" + shows "variance (\\. (\i \ I. f i \)) = (\i \ I. variance (f i))" +proof - + have "\i j. i \ I \ j \ I - {i} \ covariance (f i) (f j) = 0" + using covar_indep_eq_zero assms(4) square_integrable_imp_integrable[OF assms(2,3)] by auto + hence a:"(\i \ I. \j \ I - {i}. covariance (f i) (f j)) = 0" + by simp + thus ?thesis by (simp add: bienaymes_identity_2[OF assms(1,2,3)]) +qed + +lemma indep_var_from_indep_vars: + assumes "i \ j" + assumes "indep_vars (\_. M') f {i, j}" + shows "indep_var M' (f i) M' (f j)" +proof - + have a:"inj (case_bool i j)" using assms(1) + by (simp add: bool.case_eq_if inj_def) + have b:"range (case_bool i j) = {i,j}" + by (simp add: UNIV_bool insert_commute) + have c:"indep_vars (\_. M') f (range (case_bool i j))" using assms(2) b by simp + + have "True = indep_vars (\x. M') (\x. f (case_bool i j x)) UNIV" + using indep_vars_reindex[OF a c] + by (simp add:comp_def) + also have "... = indep_vars (\x. case_bool M' M' x) (\x. case_bool (f i) (f j) x) UNIV" + by (rule indep_vars_cong, auto simp:bool.case_distrib bool.case_eq_if) + also have "... = ?thesis" + by (simp add: indep_var_def) + finally show ?thesis by simp +qed + +lemma bienaymes_identity_pairwise_indep_2: + fixes f :: "'b \ 'a \ real" + assumes "finite I" + assumes "\i. i \ I \ f i \ borel_measurable M" + assumes "\i. i \ I \ integrable M (\\. f i \^2)" + assumes "\J. J \ I \ card J = 2 \ indep_vars (\ _. borel) f J" + shows "variance (\\. (\i \ I. f i \)) = (\i \ I. variance (f i))" + using assms(4) + by (intro bienaymes_identity_pairwise_indep[OF assms(1,2,3)] indep_var_from_indep_vars, auto) + +lemma bienaymes_identity_full_indep: + fixes f :: "'b \ 'a \ real" + assumes "finite I" + assumes "\i. i \ I \ f i \ borel_measurable M" + assumes "\i. i \ I \ integrable M (\\. f i \^2)" + assumes "indep_vars (\ _. borel) f I" + shows "variance (\\. (\i \ I. f i \)) = (\i \ I. variance (f i))" + by (intro bienaymes_identity_pairwise_indep_2[OF assms(1,2,3)] indep_vars_subset[OF assms(4)]) + auto + +end + +end diff --git a/thys/Concentration_Inequalities/Cantelli_Inequality.thy b/thys/Concentration_Inequalities/Cantelli_Inequality.thy new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/Cantelli_Inequality.thy @@ -0,0 +1,118 @@ +section \Cantelli's Inequality\ + +text \Cantelli's inequality~\cite{cantelli1929sui} is an improvement of Chebyshev's inequality for +one-sided tail bounds.\ + +theory Cantelli_Inequality + imports "HOL-Probability.Probability" +begin + +context prob_space +begin + +lemma cantelli_arith: + assumes "a > (0::real)" + shows "(V + (V / a)^2) / (a + (V / a))^2 = V / (a ^2 + V)" (is "?L = ?R") +proof - + have "?L = ((V * a^2 + V^2) / a^2) / ((a^2 + V)^2/a^2)" + using assms by (intro arg_cong2[where f="(/)"]) (simp_all add:field_simps power2_eq_square) + also have "... = (V * a\<^sup>2 + V\<^sup>2)/ (a\<^sup>2 + V)\<^sup>2" + using assms unfolding divide_divide_times_eq by simp + also have "... = V * (a^2 + V) / (a^2 + V)^2" + by (intro arg_cong2[where f="(/)"]) (simp_all add: algebra_simps power2_eq_square) + also have "... = ?R" by (simp add:power2_eq_square) + finally show ?thesis by simp +qed + +theorem cantelli_inequality: + assumes [measurable]: "random_variable borel Z" + assumes intZsq: "integrable M (\z. Z z^2)" + assumes a: "a > 0" + shows "prob {z \ space M. Z z - expectation Z \ a} \ + variance Z / (a^2 + variance Z)" +proof - + define u where "u = variance Z / a" + have u: "u \ 0" + unfolding u_def + by (simp add: a divide_nonneg_pos) + define Y where "Y = (\z. Z z + (-expectation Z))" + have "random_variable borel (\z. \Y z + u\)" + unfolding Y_def + by auto + then have ev: "{z \ space M. a + u \ \Y z + u\} \ events" + by auto + + have intZ:"integrable M Z" + apply (subst square_integrable_imp_integrable[OF _ intZsq]) + by auto + then have i1: "integrable M (\z. (Z z - expectation Z + u)\<^sup>2)" + unfolding power2_sum power2_diff using intZsq + by auto + + have intY:"integrable M Y" + unfolding Y_def using intZ by auto + have intYsq:"integrable M (\z. Y z^2)" + unfolding Y_def power2_sum using intZsq intZ by auto + + have "expectation Y = 0" + unfolding Y_def + apply (subst Bochner_Integration.integral_add[OF intZ]) + using prob_space by auto + + then have "expectation (\z. (Y z + u)^2) = + expectation (\z. (Y z)^2) + u^2" + unfolding power2_sum + apply (subst Bochner_Integration.integral_add[OF _ _]) + using intY intYsq apply auto[2] + apply (subst Bochner_Integration.integral_add[OF _ _]) + using intY intYsq apply auto[2] + using prob_space by auto + then have *: "expectation (\z. (Y z + u)^2) = variance Z + u^2" + unfolding Y_def by auto + + have " + prob {z \ space M. Z z - expectation Z \ a} = + prob {z \ space M. Y z + u \ a + u}" + apply (intro arg_cong[where f = prob]) + using Y_def by auto + also have "... \ prob {z \ space M. a + u \ \Y z + u\}" + apply (intro finite_measure_mono[OF _ ev]) + by auto + + also have "... \ expectation (\z. (Y z + u)^2) / (a + u)^2" + apply (intro second_moment_method) + unfolding Y_def using a u i1 by auto + also have "... = ((variance Z) + u^2) / (a + u)^2" + using * by auto + also have "... = variance Z / (a ^2 + variance Z)" + unfolding u_def using a by (auto intro!: cantelli_arith) + finally show ?thesis . +qed + +(* the left sided (negative) version of the inequality *) +corollary cantelli_inequality_neg: + assumes [measurable]: "random_variable borel Z" + assumes intZsq: "integrable M (\z. Z z^2)" + assumes a: "a > 0" + shows "prob {z \ space M. Z z - expectation Z \ -a} \ + variance Z / (a^2 + variance Z)" +proof - + define nZ where [simp]: "nZ = (\z. -Z z)" + have vnZ: "variance nZ = variance Z" + unfolding nZ_def + by (auto simp add: power2_commute) + + have 1: "random_variable borel nZ" by auto + have 2: "integrable M (\z. (nZ z)\<^sup>2) " + using intZsq by auto + from cantelli_inequality[OF 1 2 a] + have "prob {z \ space M. a \ nZ z - expectation nZ} \ + variance nZ / (a^2 + variance nZ)" + by auto + thus ?thesis unfolding vnZ apply auto[1] + by (smt (verit, del_insts) Collect_cong) +qed + +end + +end \ No newline at end of file diff --git a/thys/Concentration_Inequalities/Concentration_Inequalities_Preliminary.thy b/thys/Concentration_Inequalities/Concentration_Inequalities_Preliminary.thy new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/Concentration_Inequalities_Preliminary.thy @@ -0,0 +1,247 @@ +section \Preliminary results\ + +theory Concentration_Inequalities_Preliminary + imports Lp.Lp +begin + +text \Version of Cauchy-Schwartz for the Lebesgue integral:\ +lemma cauchy_schwartz: + fixes f g :: "_ \ real" + assumes "f \ borel_measurable M" "g \ borel_measurable M" + assumes "integrable M (\x. (f x) ^2)" "integrable M (\x. (g x) ^2)" + shows "integrable M (\x. f x * g x)" (is "?A") + "(\x. f x * g x \M) \ (\x. (f x)^2 \M) powr (1/2) * (\x. (g x)^ 2 \M) powr (1/2)" + (is "?L \ ?R") +proof - + show 0:"?A" + using assms by (intro Holder_inequality(1)[where p="2" and q="2"]) auto + + have "?L \ (\x. \f x * g x\ \M)" + using 0 by (intro integral_mono) auto + also have "... \ (\x. \f x\ powr 2 \M) powr (1/2) * (\x. \g x\ powr 2 \M) powr (1/2)" + using assms by (intro Holder_inequality(2)) auto + also have "... = ?R" by simp + finally show "?L \ ?R" by simp +qed + +text \Generalization of @{thm [source] prob_space.indep_vars_iff_distr_eq_PiM'}:\ + +lemma (in prob_space) indep_vars_iff_distr_eq_PiM'': + fixes I :: "'i set" and X :: "'i \ 'a \ 'b" + assumes rv: "\i. i \ I \ random_variable (M' i) (X i)" + shows "indep_vars M' X I \ + distr M (\\<^sub>M i\I. M' i) (\x. \i\I. X i x) = (\\<^sub>M i\I. distr M (M' i) (X i))" +proof (cases "I = {}") + case True + have 0: " indicator A (\_. undefined) = emeasure (count_space {\_. undefined}) A" (is "?L = ?R") + if "A \ {\_. undefined}" for A :: "('i \ 'b) set" + proof - + have 1:"A \ {} \ A = {\_. undefined}" + using that by auto + + have "?R = of_nat (card A)" + using finite_subset that by (intro emeasure_count_space_finite that) auto + also have "... = ?L" + using 1 by (cases "A = {}") auto + finally show ?thesis by simp + qed + + have "distr M (\\<^sub>M i\I. M' i) (\x. \i\I. X i x) = + distr M (count_space {\_. undefined}) (\_. (\_. undefined))" + unfolding True PiM_empty by (intro distr_cong) (auto simp:restrict_def) + also have "... = return (count_space {\_. undefined}) (\_. undefined)" + by (intro distr_const) auto + also have "... = count_space ({\_. undefined} :: ('i \ 'b) set) " + by (intro measure_eqI) (auto simp:0) + also have "... = (\\<^sub>M i\I. distr M (M' i) (X i))" + unfolding True PiM_empty by simp + finally have "distr M (\\<^sub>M i\I. M' i) (\x. \i\I. X i x)=(\\<^sub>M i\I. distr M (M' i) (X i)) \ True" + by simp + also have "... \ indep_vars M' X I" + unfolding indep_vars_def by (auto simp add: space_PiM indep_sets_def) (auto simp add:True) + finally show ?thesis by simp +next + case False + thus ?thesis + by (intro indep_vars_iff_distr_eq_PiM' assms) auto +qed + +lemma proj_indep: + assumes "\i. i \ I \ prob_space (M i)" + shows "prob_space.indep_vars (PiM I M) M (\i \. \ i) I" +proof - + interpret prob_space "(PiM I M)" + by (intro prob_space_PiM assms) + + have "distr (Pi\<^sub>M I M) (Pi\<^sub>M I M) (\x. restrict x I) = PiM I M" + by (intro distr_PiM_reindex assms) auto + also have "... = Pi\<^sub>M I (\i. distr (Pi\<^sub>M I M) (M i) (\\. \ i))" + by (intro PiM_cong refl distr_PiM_component[symmetric] assms) + finally have + "distr (Pi\<^sub>M I M) (Pi\<^sub>M I M) (\x. restrict x I) = Pi\<^sub>M I (\i. distr (Pi\<^sub>M I M) (M i) (\\. \ i))" + by simp + thus "indep_vars M (\i \. \ i) I" + by (intro iffD2[OF indep_vars_iff_distr_eq_PiM'']) simp_all +qed + +lemma forall_Pi_to_PiE: + assumes "\x. P x = P (restrict x I)" + shows "(\x \ Pi I A. P x) = (\x \ PiE I A. P x)" + using assms by (simp add:PiE_def Pi_def set_eq_iff, force) + +lemma PiE_reindex: + assumes "inj_on f I" + shows "PiE I (A \ f) = (\a. restrict (a \ f) I) ` PiE (f ` I) A" (is "?lhs = ?g ` ?rhs") +proof - + have "?lhs \ ?g` ?rhs" + proof (rule subsetI) + fix x + assume a:"x \ Pi\<^sub>E I (A \ f)" + define y where y_def: "y = (\k. if k \ f ` I then x (the_inv_into I f k) else undefined)" + have b:"y \ PiE (f ` I) A" + using a assms the_inv_into_f_eq[OF assms] + by (simp add: y_def PiE_iff extensional_def) + have c: "x = (\a. restrict (a \ f) I) y" + using a assms the_inv_into_f_eq extensional_arb + by (intro ext, simp add:y_def PiE_iff, fastforce) + show "x \ ?g ` ?rhs" using b c by blast + qed + moreover have "?g ` ?rhs \ ?lhs" + by (rule image_subsetI, simp add:Pi_def PiE_def) + ultimately show ?thesis by blast +qed + +context prob_space +begin + +lemma indep_sets_reindex: + assumes "inj_on f I" + shows "indep_sets A (f ` I) = indep_sets (\i. A (f i)) I" +proof - + have a: "\J g. J \ I \ (\j \ f ` J. g j) = (\j \ J. g (f j))" + by (metis assms prod.reindex_cong subset_inj_on) + + have b:"J \ I \ (\\<^sub>E i \ J. A (f i)) = (\a. restrict (a \ f) J) ` PiE (f ` J) A" for J + using assms inj_on_subset + by (subst PiE_reindex[symmetric]) auto + + have c:"\J. J \ I \ finite (f ` J) = finite J" + by (meson assms finite_image_iff inj_on_subset) + + show ?thesis + by (simp add:indep_sets_def all_subset_image a c) (simp_all add:forall_Pi_to_PiE b) +qed + +lemma indep_vars_reindex: + assumes "inj_on f I" + assumes "indep_vars M' X' (f ` I)" + shows "indep_vars (M' \ f) (\k \. X' (f k) \) I" + using assms by (simp add:indep_vars_def2 indep_sets_reindex) + +lemma indep_vars_cong_AE: + assumes "AE x in M. (\i \ I. X' i x = Y' i x)" + assumes "indep_vars M' X' I" + assumes "\i. i \ I \ random_variable (M' i) (Y' i)" + shows "indep_vars M' Y' I" +proof - + have a: "AE x in M. (\i\I. Y' i x) = (\i\I. X' i x)" + by (rule AE_mp[OF assms(1)], rule AE_I2, simp cong:restrict_cong) + have b: "\i. i \ I \ random_variable (M' i) (X' i)" + using assms(2) by (simp add:indep_vars_def2) + have c: "\x. x \ I \ AE xa in M. X' x xa = Y' x xa" + by (rule AE_mp[OF assms(1)], rule AE_I2, simp) + + have "distr M (Pi\<^sub>M I M') (\x. \i\I. Y' i x) = distr M (Pi\<^sub>M I M') (\x. \i\I. X' i x)" + by (intro distr_cong_AE measurable_restrict a b assms(3)) auto + also have "... = Pi\<^sub>M I (\i. distr M (M' i) (X' i))" + using assms b by (subst indep_vars_iff_distr_eq_PiM''[symmetric]) auto + also have "... = Pi\<^sub>M I (\i. distr M (M' i) (Y' i))" + by (intro PiM_cong distr_cong_AE c assms(3) b) auto + finally have "distr M (Pi\<^sub>M I M') (\x. \i\I. Y' i x) = Pi\<^sub>M I (\i. distr M (M' i) (Y' i))" + by simp + + thus ?thesis + using assms(3) + by (subst indep_vars_iff_distr_eq_PiM'') auto +qed + +end + +text \Integrability of bounded functions on finite measure spaces:\ + +lemma bounded_const: "bounded ((\x. (c::real)) ` T)" + by (intro boundedI[where B="norm c"]) auto + +lemma bounded_exp: + fixes f :: "'a \ real" + assumes "bounded ((\x. f x) ` T)" + shows "bounded ((\x. exp (f x)) ` T)" +proof - + obtain m where "norm (f x) \ m" if "x \ T" for x + using assms unfolding bounded_iff by auto + + thus ?thesis + by (intro boundedI[where B="exp m"]) fastforce +qed + +lemma bounded_mult_comp: + fixes f :: "'a \ real" + assumes "bounded (f ` T)" "bounded (g ` T)" + shows "bounded ((\x. (f x) * (g x)) ` T)" +proof - + obtain m1 where "norm (f x) \ m1" "m1 \0" if "x \ T" for x + using assms unfolding bounded_iff by fastforce + moreover obtain m2 where "norm (g x) \ m2" "m2 \0" if "x \ T" for x + using assms unfolding bounded_iff by fastforce + + ultimately show ?thesis + by (intro boundedI[where B="m1 * m2"]) (auto intro!: mult_mono simp:abs_mult) +qed + +lemma bounded_sum: + fixes f :: "'i \ 'a \ real" + assumes "finite I" + assumes "\i. i \ I \ bounded (f i ` T)" + shows "bounded ((\x. (\i \ I. f i x)) ` T)" + using assms by (induction I) (auto intro:bounded_plus_comp bounded_const) + +lemma (in finite_measure) bounded_int: + fixes f :: "'i \ 'a \ real" + assumes "bounded ((\ x. f (fst x) (snd x)) ` (T \ space M))" + shows "bounded ((\x. (\\. (f x \) \M)) ` T)" +proof - + obtain m where "\x y. x \ T \ y \ space M \ norm (f x y) \ m" + using assms unfolding bounded_iff by auto + hence m:"\x y. x \ T \ y \ space M \ norm (f x y) \ max m 0" + by fastforce + + have "norm (\\. (f x \) \M) \ max m 0 * measure M (space M)" (is "?L \ ?R") if "x \ T" for x + proof - + have "?L \ (\\. norm (f x \) \M)" by simp + also have "... \ (\\. max m 0 \M)" + using that m by (intro integral_mono') auto + also have "... = ?R" + by simp + finally show ?thesis by simp + qed + thus ?thesis + by (intro boundedI[where B="max m 0 * measure M (space M)"]) auto +qed + +lemmas bounded_intros = + bounded_minus_comp bounded_plus_comp bounded_mult_comp bounded_sum finite_measure.bounded_int + bounded_const bounded_exp + +lemma (in prob_space) integrable_bounded: + fixes f :: "_ \ ('b :: {banach,second_countable_topology})" + assumes "bounded (f ` space M)" + assumes "f \ M \\<^sub>M borel" + shows "integrable M f" +proof - + obtain m where "norm (f x) \ m" if "x \ space M" for x + using assms(1) unfolding bounded_iff by auto + thus ?thesis + by (intro integrable_const_bound[where B="m"] AE_I2 assms(2)) +qed + +end \ No newline at end of file diff --git a/thys/Concentration_Inequalities/Efron_Stein_Inequality.thy b/thys/Concentration_Inequalities/Efron_Stein_Inequality.thy new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/Efron_Stein_Inequality.thy @@ -0,0 +1,300 @@ +section \Efron-Stein Inequality\ + +text \In this section we verify the Efron-Stein inequality. The verified theorem is stated as +Efron-Stein inequality for non-symmetric functions by Steele~\cite{steele1986}. However most +textbook refer to this version as ``the Efron-Stein inequality''. The original result that was shown +by Efron and Stein is a tail bound for the variance of a symmetric functions of i.i.d. +random variables~\cite{efron1981}.\ + +theory Efron_Stein_Inequality + imports Concentration_Inequalities_Preliminary +begin + +theorem efron_stein_inequality_distr: + fixes f :: "_ \ real" + assumes "finite I" + assumes "\i. i \ I \ prob_space (M i)" + assumes "integrable (PiM I M) (\x. f x^2)" and f_meas: "f \ borel_measurable (PiM I M)" + shows "prob_space.variance (PiM I M) f \ + (\i\I. (\x. (f (\j. x (j,False)) - f (\j. x (j, j=i)))^2 \PiM (I\UNIV) (M \ fst))) / 2" + (is "?L \ ?R") +proof - + let ?M = "PiM (I\(UNIV::bool set)) (M \ fst)" + + have prob: "prob_space (PiM I M)" + using assms(2) by (intro prob_space_PiM) auto + + interpret prob_space "?M" + using assms(2) by (intro prob_space_PiM) auto + + define n where "n = card I" + + obtain q :: "_ \ nat" where q:"bij_betw q I {.. = "(\n x. f (\j. x (j, q j < n)))" + let ?\ = "(\n x. f (\j. x (j, q j = n)))" + let ?\ = "(\x. f (\j. x (j, False)))" + let ?\ = "(\x. f (\j. x (j, True)))" + + have meas_1: "(\\. f (g \)) \ borel_measurable ?M" + if "g \ Pi\<^sub>M (I \ UNIV) (M \ fst) \\<^sub>M Pi\<^sub>M I M" for g + using that by (intro measurable_compose[OF _ f_meas]) + + have meas_2: "(\x j. x (j, h j)) \ ?M \\<^sub>M Pi\<^sub>M I M" for h + proof - + have "?thesis \ (\x. (\j \ I. x (j, h j))) \ ?M \\<^sub>M Pi\<^sub>M I M" + by (intro measurable_cong) (auto simp:space_PiM PiE_def extensional_def) + also have "... \ True" + unfolding eq_True + by (intro measurable_restrict measurable_PiM_component_rev) auto + finally show ?thesis by simp + qed + + have int_1: "integrable ?M (\x. (g x - h x)^2)" + if "integrable ?M (\x. (g x)^2)" "integrable ?M (\x. (h x)^2)" + and "g \ borel_measurable ?M" "h \ borel_measurable ?M" + for g h :: "_ \ real" + proof - + have "integrable ?M (\x. (g x)^2 + (h x)^2 - 2 * (g x * h x))" + using that by (intro Bochner_Integration.integrable_add Bochner_Integration.integrable_diff + integrable_mult_right cauchy_schwartz(1)) + thus ?thesis by (simp add:algebra_simps power2_eq_square) + qed + + note meas_rules = borel_measurable_add borel_measurable_times borel_measurable_diff + borel_measurable_power meas_1 meas_2 + + have f_int: "integrable (Pi\<^sub>M I M) f" + by (intro finite_measure.square_integrable_imp_integrable[OF _ f_meas assms(3)] + prob_space.finite_measure prob) + moreover have "integrable (Pi\<^sub>M I M) (\x. f (restrict x I)) = integrable (Pi\<^sub>M I M) f" + by (intro Bochner_Integration.integrable_cong) (auto simp:space_PiM) + ultimately have f_int_2: "integrable (Pi\<^sub>M I M) (\x. f (restrict x I))" by simp + + have cong: "(\x. g (\j\I. x (j, h j)) \?M) = (\x. g (\j. x (j, h j)) \?M)" (is "?L1 = ?R1") + for g :: "_ \ real" and h + by (intro Bochner_Integration.integral_cong arg_cong[where f="g"] refl) + (auto simp add:space_PiM PiE_def extensional_def restrict_def) + + have lift: "(\x. g x \PiM I M) = (\x. g (\j. x (j, h j)) \?M)" (is "?L1 = ?R1") + if "g \ borel_measurable (Pi\<^sub>M I M)" + for g :: "_ \ real" and h + proof - + let ?J = "(\i. (i, h i)) ` I" + have "?R1 = (\x. g (\j \ I. x (j, h j)) \?M)" + by (intro cong[symmetric]) + also have "... = (\x. g x \distr ?M (PiM I (\i. (M\fst) (i, h i))) (\x. (\j \ I. x (j, h j))))" + using that + by (intro integral_distr[symmetric] measurable_restrict measurable_component_singleton) auto + also have "... = (\x. g x \PiM I (\i. (M \ fst) (i, h i)))" + using assms(2) + by (intro arg_cong2[where f="integral\<^sup>L"] refl distr_PiM_reindex inj_onI) auto + also have "... = ?L1" + by auto + finally show ?thesis + by simp + qed + + have lift_int: "integrable ?M (\x. g (\j. x (j, h j)))" if "integrable (Pi\<^sub>M I M) g" + for g :: "_ \ real" and h + proof - + have 0:"integrable (distr ?M (PiM I (\i. (M\fst) (i, h i))) (\x. (\j \ I. x (j, h j)))) g" + using that assms(2) by (subst distr_PiM_reindex) (auto intro:inj_onI) + have "integrable ?M (\x. g (\j\I. x (j, h j)))" + by (intro integrable_distr[OF _ 0] measurable_restrict measurable_component_singleton) auto + moreover have "integrable ?M (\x. g (\j\I. x (j, h j))) \ ?thesis" + by (intro Bochner_Integration.integrable_cong refl arg_cong[where f="g"] ext) + (auto simp:PiE_def space_PiM extensional_def) + ultimately show ?thesis + by simp + qed + + note int_rules = cauchy_schwartz(1) int_1 lift_int assms(3) f_int f_int_2 + + have "(\x. g x \?M) = (\x. g (\(j,v). x (j, v \ h j)) \?M)" (is "?L1 = ?R1") + if "g \ borel_measurable ?M" for g :: "_ \ real" and h + proof - + have "?L1 = (\x. g x \distr ?M (PiM (I\UNIV) (\i. (M \ fst) (fst i, snd i \ h (fst i)))) + (\x.(\i \ I\UNIV. x (fst i, snd i \ h (fst i))) ))" + by (subst distr_PiM_reindex) (auto intro:inj_onI assms(2) simp:comp_def) + also have "... = (\x. g (\i \ I\UNIV. x (fst i, snd i \ h (fst i))) \?M)" + using that by (intro integral_distr measurable_restrict measurable_component_singleton) + (auto simp:comp_def) + also have "... = ?R1" + by (intro Bochner_Integration.integral_cong refl arg_cong[where f="g"] ext) + (auto simp add:space_PiM PiE_def extensional_def restrict_def) + finally show ?thesis + by simp + qed + + hence switch: "(\x. g x \?M) = (\x. h x \?M)" + if "\x. h x = g (\(j,v). x (j, v \ u j))" "g \ borel_measurable ?M" + for g h :: "_ \ real" and u + using that by simp + + have 1: "(\x. (?\ x) * (?\ i x - ?\ (i+1) x) \?M) \ (\x. (?\ x - ?\ i x)^2 \?M) / 2" + (is "?L1 \ ?R1") + if "i < n" for i + proof - + have "?L1 = (\x. (?\ i x) * (?\ (i+1) x - ?\ i x) \?M)" + by (intro switch[of _ _ "(\j. q j = i)"] arg_cong2[where f="(*)"] + arg_cong2[where f="(-)"] arg_cong[where f="f"] ext meas_rules) (auto intro:arg_cong) + hence "?L1 = (?L1 + (\x. (?\ i x) * (?\ (i+1) x - ?\ i x) \?M)) / 2" + by simp + also have "... = (\x. (?\ x) * (?\ i x - ?\(i+1) x) + (?\ i x) * (?\(i+1) x - ?\ i x) \?M)/2" + by (intro Bochner_Integration.integral_add[symmetric] arg_cong2[where f="(/)"] refl + int_rules meas_rules) + also have "... = (\x. (?\ x - ?\ i x) * (?\ i x - ?\(i+1) x) \?M)/2" + by (intro arg_cong2[where f="(/)"] Bochner_Integration.integral_cong) + (auto simp:algebra_simps) + also have "...\((\x. (?\ x-?\ i x)^2 \?M)powr(1/2)*(\x.(?\ i x-?\(i+1)x)^2 \?M) powr (1/2))/2" + by (intro divide_right_mono cauchy_schwartz meas_rules int_rules) auto + also have "...=((\x. (?\ x-?\ i x)^2 \?M)powr(1/2)*(\x.(?\ x-?\ i x)^2 \?M) powr (1/2))/2" + by (intro arg_cong2[where f="(/)"] arg_cong2[where f="(*)"] arg_cong2[where f="(powr)"] refl + switch[of _ _ "(\j. q j < i)"] arg_cong2[where f="power"] arg_cong2[where f="(-)"] + arg_cong[where f="f"] ext meas_rules) (auto intro:arg_cong) + also have "... = (\x. (?\ x-?\ i x)^2 \?M)/2" + by (simp add:powr_add[symmetric]) + finally show ?thesis by simp + qed + + have "indep_vars (M \ fst) (\i \. \ i) (I \ UNIV)" + using assms(2) by (intro proj_indep) auto + hence 2:"indep_var (Pi\<^sub>M (I\{False}) (M\fst)) (\x. \j\I\{False}. x j) + (Pi\<^sub>M (I\{True}) (M\fst)) (\x. \j\I\{True}. x j)" + by (intro indep_var_restrict[where I="I \ UNIV"]) auto + have "indep_var + (Pi\<^sub>M I M) ((\x. (\i \ I. x (i, False))) \ (\x. (\j \ I\{False}. x j))) + (Pi\<^sub>M I M) ((\x. (\i \ I. x (i, True))) \ (\x. (\j \ I\{True}. x j)))" + by (intro indep_var_compose[OF 2] measurable_restrict measurable_PiM_component_rev) auto + hence "indep_var (Pi\<^sub>M I M) (\x. (\j\I. x (j, False))) (Pi\<^sub>M I M) (\x. (\j\I. x (j, True)))" + unfolding comp_def by (simp add:restrict_def cong:if_cong) + + hence "indep_var borel (f \ (\x. (\j\I. x (j, False)))) borel (f \ (\x. (\j \ I. x (j, True))))" + by (intro indep_var_compose[OF _ assms(4,4)]) auto + hence indep:"indep_var borel (\x. f (\j\I. x (j, False))) borel (\x. f (\j\I. x (j, True)))" + by (simp add:comp_def) + + have 3: "\ (j, q j = q i) = \ (j, j = i)" if + "\ \ PiE (I \ UNIV) (\i. space (M (fst i)))" "i \ I" for i j \ + proof (cases "j \ I") + case True + hence "(q j = q i) = (j = i)" + using that inj_onD[OF bij_betw_imp_inj_on[OF q]] by blast + thus ?thesis by simp + next + case False + hence "\ (j, a) = undefined" for a + using that unfolding PiE_def extensional_def by simp + thus ?thesis by simp + qed + + have "?L = (\x. (f x)^2 \PiM I M) - (\x. (f x) \PiM I M)^2" + by (intro prob_space.variance_eq f_int assms(3) prob) + also have "... = (\x. (f x)^2 \PiM I M) - (\x. f x \PiM I M) * (\x. f x \PiM I M)" + by (simp add:power2_eq_square) + also have "... = (\x. (?\ x)^2 \?M) - (\x. ?\ x \?M) * (\x. ?\ x \?M)" + by (intro arg_cong2[where f="(-)"] lift arg_cong2[where f="(*)"] meas_rules f_meas) + also have "... = (\x. (?\ x)^2 \?M)-(\x. f (\j\I. x (j,False)) \?M)*(\x. f(\j\I. x(j,True)) \?M)" + by (intro arg_cong2[where f="(-)"] arg_cong2[where f="(*)"] cong[symmetric] refl) + also have "... = (\x. (?\ x)^2 \?M) - (\x. f (\j\I. x (j,False))* f(\j\I. x(j,True)) \?M)" + by (intro arg_cong2[where f="(-)"] indep_var_lebesgue_integral[symmetric] refl int_rules indep) + also have "... = (\x. (?\ x) * (?\ 0 x) \?M) - (\x. (?\ x) * (?\ n x) \?M)" + using bij_betw_apply[OF q] by (intro arg_cong2[where f="(-)"] arg_cong2[where f="(*)"] ext + arg_cong[where f="f"] Bochner_Integration.integral_cong) + (auto simp:space_PiM power2_eq_square PiE_def extensional_def) + also have "... = (\i < n. (\x. (?\ x) * (?\ i x) \?M) - (\x. (?\ x) * (?\ (Suc i) x) \?M))" + unfolding power2_eq_square by (intro sum_lessThan_telescope'[symmetric]) + also have "... = (\i < n. (\x. (?\ x) * (?\ i x) - (?\ x) * (?\ (Suc i) x) \?M))" + by (intro sum.cong Bochner_Integration.integral_diff[symmetric] int_rules meas_rules) auto + also have "... = (\i < n. (\x. (?\ x) * (?\ i x - ?\ (i+1) x) \?M))" + by (simp_all add:power2_eq_square algebra_simps) + also have "... \ (\i< n. ((\x. (?\ x - ?\ i x)^2 \?M)) / 2)" + by (intro sum_mono 1) auto + also have "... = (\i \ I. ((\x. (f (\j. x (j,False)) - f (\j. x (j,q j=q i)))^2 \?M))/ 2)" + by (intro sum.reindex_bij_betw[OF q, symmetric]) + also have "... = (\i \ I. ((\x. (f (\j. x (j,False)) - f (\j. x (j,q j=q i)))^2 \?M)))/2" + unfolding sum_divide_distrib[symmetric] by simp + also have "... = ?R" + using inj_onD[OF bij_betw_imp_inj_on[OF q]] + by (intro arg_cong2[where f="(/)"] arg_cong2[where f="(-)"] arg_cong2[where f="power"] + arg_cong[where f="f"] Bochner_Integration.integral_cong sum.cong refl ext 3) + (auto simp add:space_PiM ) + finally show ?thesis + by simp +qed + +theorem (in prob_space) efron_stein_inequality_classic: + fixes f :: "_ \ real" + assumes "finite I" + assumes "indep_vars (M' \ fst) X (I \ (UNIV :: bool set))" + assumes "f \ borel_measurable (PiM I M')" + assumes "integrable M (\\. f (\i\I. X (i,False) \)^2)" + assumes "\i. i \ I \ distr M (M' i) (X (i, True)) = distr M (M' i) (X (i, False))" + shows "variance (\\. f (\i\I. X (i,False) \)) \ + (\j \ I. expectation (\\. (f (\i\I. X (i,False) \) - f (\i\I. X (i, i=j) \))^2))/2" + (is "?L \ ?R") +proof - + let ?D = "distr M (PiM I M') (\\. \i\I. X (i, False) \)" + + let ?M = "PiM I (\i. distr M (M' i) (X (i,False)))" + let ?N = "PiM (I \ (UNIV::bool set)) ((\i. distr M (M' i) (X (i,False))) \ fst)" + + have rv: "random_variable (M' i) (X (i, j))" if "i \ I" for i j + using assms(2) that unfolding indep_vars_def by auto + + have proj_meas: "(\x j. x (j, h j)) \ Pi\<^sub>M (I \ UNIV) (M' \ fst) \\<^sub>M Pi\<^sub>M I M'" + for h :: " _ \ bool" + proof - + have "?thesis \ (\x. (\j \ I. x (j, h j))) \ Pi\<^sub>M (I \ UNIV) (M' \ fst) \\<^sub>M Pi\<^sub>M I M'" + by (intro measurable_cong) (auto simp:space_PiM PiE_def extensional_def) + also have "... \ True" + unfolding eq_True + by (intro measurable_restrict measurable_PiM_component_rev) auto + finally show ?thesis by simp + qed + + note meas_rules = borel_measurable_add borel_measurable_times borel_measurable_diff proj_meas + borel_measurable_power assms(3) measurable_restrict measurable_compose[OF _ assms(3)] + + have "indep_vars ((M' \ fst) \ (\i. (i, False))) (\i. X (i, False)) I" + by (intro indep_vars_reindex indep_vars_subset[OF assms(2)] inj_onI) auto + hence "indep_vars M' (\i. X (i, False)) I" by (simp add: comp_def) + hence 0:"?D = PiM I (\i. distr M (M' i) (X (i,False)))" + by (intro iffD1[OF indep_vars_iff_distr_eq_PiM''] rv) + + have "distr M (M' (fst x)) (X (fst x, False)) = distr M (M' (fst x)) (X x)" + if "x \ I \ UNIV" for x + using that assms(5) by (cases x, cases "snd x") auto + + hence 1: "?N = PiM (I \ UNIV) (\i. distr M ((M' \ fst) i) (X i))" + using assms(3) by (intro PiM_cong refl) (simp add:comp_def) + also have "... = distr M (PiM (I \ UNIV) (M' \ fst)) (\x. \i\I \ UNIV. X i x)" + using rv by (intro iffD1[OF indep_vars_iff_distr_eq_PiM'', symmetric] assms(2)) auto + finally have 2:"?N = distr M (PiM (I \ UNIV) (M' \ fst)) (\x. \i\I \ UNIV. X i x)" + by simp + + have 3: "integrable (Pi\<^sub>M I (\i. distr M (M' i) (X (i, False)))) (\x. (f x)\<^sup>2)" + unfolding 0[symmetric] by (intro iffD2[OF integrable_distr_eq] meas_rules assms rv) + + have "?L = (\x. (f x - expectation (\\. f (\i\I. X (i,False) \)))^2 \?D)" + using rv by (intro integral_distr[symmetric] meas_rules measurable_restrict) auto + also have "... = prob_space.variance ?D f" + by (intro arg_cong[where f="integral\<^sup>L ?D"] arg_cong2[where f="(-)"] arg_cong2[where f="power"] + refl ext integral_distr[symmetric] measurable_restrict rv assms(3)) + also have "... = prob_space.variance ?M f" + unfolding 0 by simp + also have "... \ (\i\I. (\x. (f (\j. x (j, False)) - f (\j. x (j, j = i)))^2 \?N)) / 2" + using assms(3) by (intro efron_stein_inequality_distr prob_space_distr rv assms(1) 3) auto + also have "... = (\i\I. expectation (\\. (f (\j. (\i\I\UNIV. X i \) (j, False)) - + f (\j. (\i\I\UNIV. X i \) (j, j=i)))\<^sup>2)) / 2" + using rv unfolding 2 + by (intro sum.cong arg_cong2[where f="(/)"] integral_distr refl meas_rules) auto + also have "... = ?R" + by (simp add:restrict_def) + finally show ?thesis + by simp +qed + +end \ No newline at end of file diff --git a/thys/Concentration_Inequalities/McDiarmid_Inequality.thy b/thys/Concentration_Inequalities/McDiarmid_Inequality.thy new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/McDiarmid_Inequality.thy @@ -0,0 +1,777 @@ +section \McDiarmid's inequality\ + +text \In this section we verify McDiarmid's inequality \cite[Lemma 1.2]{mcdiarmid1989}. In the +source and also further sources sometimes refer to the result as the ``independent bounded +differences'' inequality.\ + +theory McDiarmid_Inequality + imports Concentration_Inequalities_Preliminary +begin + +lemma Collect_restr_cong: + assumes "A = B" + assumes "\x. x \ A \ P x = Q x" + shows "{x \ A. P x} = {x \ B. Q x}" + using assms by auto + +lemma ineq_chain: + fixes h :: "nat \ real" + assumes "\i. i < n \ h (i+1) \ h i" + shows "h n \ h 0" + using assms by (induction n) force+ + +lemma restrict_subset_eq: + assumes "A \ B" + assumes "restrict f B = restrict g B" + shows "restrict f A = restrict g A" + using assms unfolding restrict_def by (meson subsetD) + +text \Bochner Integral version of Hoeffding's Lemma using + @{thm [source] interval_bounded_random_variable.Hoeffdings_lemma_nn_integral_0}\ + +lemma (in prob_space) Hoeffdings_lemma_bochner: + assumes "l > 0" and E0: "expectation f = 0" + assumes "random_variable borel f" + assumes "AE x in M. f x \ {a..b::real}" + shows "expectation (\x. exp (l * f x)) \ exp (l\<^sup>2 * (b - a)\<^sup>2 / 8)" (is "?L \ ?R") +proof - + interpret interval_bounded_random_variable M f a b + using assms by (unfold_locales) auto + + have "integrable M (\x. exp (l * f x))" + using assms(1,3,4) by (intro integrable_const_bound[where B="exp (l * b)"]) simp_all + + hence "ennreal (?L) = (\\<^sup>+ x. exp (l * f x) \M)" + by (intro nn_integral_eq_integral[symmetric]) auto + also have "... \ ennreal (?R)" + by (intro Hoeffdings_lemma_nn_integral_0 assms) + finally have 0:"ennreal (?L) \ ennreal ?R" + by simp + show ?thesis + proof (cases "?L \ 0") + case True + thus ?thesis using 0 by simp + next + case False + hence "?L \ 0" by simp + also have "... \ ?R" by simp + finally show ?thesis by simp + qed +qed + +lemma (in prob_space) Hoeffdings_lemma_bochner_2: + assumes "l > 0" and E0: "expectation f = 0" + assumes "random_variable borel f" + assumes "\x y. {x,y} \ space M \ \f x - f y\ \ (c::real)" + shows "expectation (\x. exp (l * f x)) \ exp (l^2 * c^2 / 8)" (is "?L \ ?R") +proof - + define a :: real where "a = (INF x \ space M. f x)" + define b :: real where "b = a+c" + + obtain \ where \:"\ \ space M" using not_empty by auto + hence 0:"f ` space M \ {}" by auto + have 1: "c = b - a" unfolding b_def by simp + + have "bdd_below (f ` space M)" + using \ assms(4) unfolding abs_le_iff + by (intro bdd_belowI[where m="f \ - c"]) (auto simp add:algebra_simps) + hence "f x \ a" if "x \ space M" for x unfolding a_def by (intro cINF_lower that) + moreover have "f x \ b" if x_space: "x \ space M" for x + proof (rule ccontr) + assume "\(f x \ b)" + hence a:"f x > a + c" unfolding b_def by simp + have "f y \ f x - c" if "y \ space M" for y + using that x_space assms(4) unfolding abs_le_iff by (simp add:algebra_simps) + hence "f x - c \ a" unfolding a_def using cInf_greatest[OF 0] by auto + thus "False" using a by simp + qed + ultimately have "f x \ {a..b}" if "x \ space M" for x using that by auto + hence "AE x in M. f x \ {a..b}" by simp + thus ?thesis unfolding 1 by (intro Hoeffdings_lemma_bochner assms(1,2,3)) +qed + +lemma (in prob_space) Hoeffdings_lemma_bochner_3: + assumes "expectation f = 0" + assumes "random_variable borel f" + assumes "\x y. {x,y} \ space M \ \f x - f y\ \ (c::real)" + shows "expectation (\x. exp (l * f x)) \ exp (l^2 * c^2 / 8)" (is "?L \ ?R") +proof - + consider (a) "l > 0" | (b) "l = 0" | (c) "l < 0" + by argo + then show ?thesis + proof (cases) + case a thus ?thesis by (intro Hoeffdings_lemma_bochner_2 assms) auto + next + case b thus ?thesis by simp + next + case c + have "?L = expectation (\x. exp ((-l) * (-f x)))" by simp + also have "... \ exp ((-l)^2 * c\<^sup>2/8)" using c assms by (intro Hoeffdings_lemma_bochner_2) auto + also have "... = ?R" by simp + finally show ?thesis by simp + qed +qed + +text \Version of @{thm [source] product_sigma_finite.product_integral_singleton} without the +condition that @{term "M i"} has to be sigma finite for all @{term "i"}:\ + +lemma product_integral_singleton: + fixes f :: "_ \ _::{banach, second_countable_topology}" + assumes "sigma_finite_measure (M i)" + assumes "f \ borel_measurable (M i)" + shows "(\x. f (x i) \(PiM {i} M)) = (\x. f x \(M i))" (is "?L = ?R") +proof - + define M' where "M' j = (if j=i then M i else count_space {undefined})" for j + + interpret product_sigma_finite "M'" + using assms(1) unfolding product_sigma_finite_def M'_def + by (auto intro!:sigma_finite_measure_count_space_finite) + + have "?L = \x. f (x i) \(PiM {i} M')" + by (intro Bochner_Integration.integral_cong PiM_cong) (simp_all add:M'_def) + also have "... = (\x. f x \(M' i))" + using assms(2) by (intro product_integral_singleton) (simp add:M'_def) + also have "... = ?R" + by (intro Bochner_Integration.integral_cong PiM_cong) (simp_all add:M'_def) + finally show ?thesis by simp +qed + +text \Version of @{thm [source] product_sigma_finite.product_integral_fold} without the +condition that @{term "M i"} has to be sigma finite for all @{term "i"}:\ + +lemma product_integral_fold: + fixes f :: "_ \ _::{banach, second_countable_topology}" + assumes "\i. i \ I \ J \ sigma_finite_measure (M i)" + assumes "I \ J = {}" + assumes "finite I" + assumes "finite J" + assumes "integrable (PiM (I \ J) M) f" + shows "(\x. f x \PiM (I \ J) M) = (\x. (\y. f (merge I J(x,y)) \PiM J M) \PiM I M)" (is "?L = ?R") + and "integrable (PiM I M) (\x. (\y. f (merge I J(x,y)) \PiM J M))" (is "?I") + and "AE x in PiM I M. integrable (PiM J M) (\y. f (merge I J(x,y)))" (is "?T") +proof - + define M' where "M' i = (if i \ I \ J then M i else count_space {undefined})" for i + + interpret product_sigma_finite "M'" + using assms(1) unfolding product_sigma_finite_def M'_def + by (auto intro!:sigma_finite_measure_count_space_finite) + + interpret pair_sigma_finite "Pi\<^sub>M I M'" "Pi\<^sub>M J M'" + using assms(3,4) sigma_finite unfolding pair_sigma_finite_def by blast + + have 0: "integrable (Pi\<^sub>M (I \ J) M') f = integrable (Pi\<^sub>M (I \ J) M) f" + by (intro Bochner_Integration.integrable_cong PiM_cong) (simp_all add:M'_def) + + have "?L = (\x. f x \PiM (I \ J) M')" + by (intro Bochner_Integration.integral_cong PiM_cong) (simp_all add:M'_def) + also have "... = (\x. (\y. f (merge I J (x,y)) \PiM J M') \PiM I M')" + using assms(5) by (intro product_integral_fold assms(2,3,4)) (simp add:0) + also have "... = ?R" + by (intro Bochner_Integration.integral_cong PiM_cong) (simp_all add:M'_def) + finally show "?L = ?R" by simp + + have "integrable (Pi\<^sub>M (I \ J) M') f = integrable (PiM I M' \\<^sub>M PiM J M') (\x. f (merge I J x))" + using assms(5) apply (subst distr_merge[OF assms(2,3,4),symmetric]) + by (intro integrable_distr_eq) (simp_all add:0[symmetric]) + hence 1:"integrable (PiM I M' \\<^sub>M PiM J M') (\x. f (merge I J x))" + using assms(5) 0 by simp + + hence "integrable (PiM I M') (\x. (\y. f (merge I J(x,y)) \PiM J M'))" (is "?I'") + by (intro integrable_fst') auto + moreover have "?I' = ?I" + by (intro Bochner_Integration.integrable_cong PiM_cong ext Bochner_Integration.integral_cong) + (simp_all add:M'_def) + ultimately show "?I" + by simp + + have "AE x in Pi\<^sub>M I M'. integrable (Pi\<^sub>M J M') (\y. f (merge I J (x, y)))" (is "?T'") + by (intro AE_integrable_fst'[OF 1]) + moreover have "?T' = ?T" + by (intro arg_cong2[where f="almost_everywhere"] PiM_cong ext Bochner_Integration.integrable_cong) + (simp_all add:M'_def) + ultimately show "?T" + by simp +qed + +lemma product_integral_insert: + fixes f :: "_ \ _::{banach, second_countable_topology}" + assumes "\k. k \ {i} \ J \ sigma_finite_measure (M k)" + assumes "i \ J" + assumes "finite J" + assumes "integrable (PiM (insert i J) M) f" + shows "(\x. f x \PiM (insert i J) M) = (\x. (\y. f (y(i := x)) \PiM J M) \M i)" (is "?L = ?R") +proof - + note meas_cong = iffD1[OF measurable_cong] + + have "integrable (PiM {i} M) (\x. (\y. f (merge {i} J (x,y)) \PiM J M))" + using assms by (intro product_integral_fold) auto + hence 0:"(\x. (\y. f (merge {i} J (x,y)) \PiM J M)) \ borel_measurable (PiM {i} M)" + using borel_measurable_integrable by simp + have 1:"(\x. (\y. f (y(i := (x i))) \PiM J M)) \ borel_measurable (PiM {i} M)" + by (intro meas_cong[OF _ 0] Bochner_Integration.integral_cong arg_cong[where f="f"]) + (auto simp add:space_PiM merge_def fun_upd_def PiE_def extensional_def) + have "(\x. (\y. f (y(i := (\i\{i}. x) i)) \PiM J M)) \ borel_measurable (M i)" + by (intro measurable_compose[OF _ 1, where f="(\x. (\i\{i}. x))"] measurable_restrict) auto + hence 2:"(\x. (\y. f (y(i := x )) \PiM J M)) \ borel_measurable (M i)" by simp + + have "?L = (\x. f x \PiM ({i} \ J) M)" by simp + also have "... = (\x. (\y. f (merge {i} J (x,y)) \PiM J M) \PiM {i} M)" + using assms(2,4) by (intro product_integral_fold assms(1,3)) auto + also have "... = (\x. (\y. f (y(i := (x i))) \PiM J M) \PiM {i} M)" + by (intro Bochner_Integration.integral_cong refl arg_cong[where f="f"]) + (auto simp add:space_PiM merge_def fun_upd_def PiE_def extensional_def) + also have "... = ?R" + using assms(1,4) by (intro product_integral_singleton assms(1) 2) auto + finally show ?thesis by simp +qed + +lemma product_integral_insert_rev: + fixes f :: "_ \ _::{banach, second_countable_topology}" + assumes "\k. k \ {i} \ J \ sigma_finite_measure (M k)" + assumes "i \ J" + assumes "finite J" + assumes "integrable (PiM (insert i J) M) f" + shows "(\x. f x \PiM (insert i J) M) = (\y. (\x. f (y(i := x)) \M i) \PiM J M)" (is "?L = ?R") +proof - + have "?L = (\x. f x \PiM (J \ {i}) M)" by simp + also have "... = (\x. (\y. f (merge J {i} (x,y)) \PiM {i} M) \PiM J M)" + using assms(2,4) by (intro product_integral_fold assms(1,3)) auto + also have "... = (\x. (\y. f (x(i := (y i))) \PiM {i} M) \PiM J M)" + unfolding merge_singleton[OF assms(2)] + by (intro Bochner_Integration.integral_cong refl arg_cong[where f="f"]) + (metis PiE_restrict assms(2) restrict_upd space_PiM) + also have "... = ?R" + using assms(1,4) by (intro Bochner_Integration.integral_cong product_integral_singleton) auto + finally show ?thesis by simp +qed + +lemma merge_empty[simp]: + "merge {} I (y,x) = restrict x I" + "merge I {} (y,x) = restrict y I" + unfolding merge_def restrict_def by auto + +lemma merge_cong: + assumes "restrict x1 I = restrict x2 I" + assumes "restrict y1 J = restrict y2 J" + shows "merge I J (x1,y1) = merge I J (x2,y2)" + using assms unfolding merge_def restrict_def + by (intro ext) (smt (verit, best) case_prod_conv) + +lemma restrict_merge: + "restrict (merge I J x) K = merge (I \ K) (J \ K) x" + unfolding restrict_def merge_def by (intro ext) (auto simp:case_prod_beta) + +lemma map_prod_measurable: + assumes "f \ M \\<^sub>M M'" + assumes "g \ N \\<^sub>M N'" + shows "map_prod f g \ M \\<^sub>M N \\<^sub>M M' \\<^sub>M N'" + using assms by (subst measurable_pair_iff) simp + +lemma mc_diarmid_inequality_aux: + fixes f :: "(nat \ 'a) \ real" + fixes n :: nat + assumes "\i. i < n \ prob_space (M i)" + assumes "\i x y. i {x,y} \ space (PiM {.. (\j\{.. \f x-f y\\c i" + assumes f_meas: "f \ borel_measurable (PiM {.._gt_0: "\ >0" + shows "\

(\ in PiM {.. - (\\. f \ \PiM {.. \) \ exp (-(2*\^2)/(\i ?R") +proof - + define h where "h k = (\\. (\\. f (merge {.., \)) \PiM {k.. / (\i = h (Suc i) \ - h i \" for i \ + + obtain x0 where x0:"x0 \ space (PiM {..f x - f y\ \ c i" if "i < n" + "x \ PiE {..i. space (M i))" "y \ PiE {..i. space (M i))" + "restrict x ({.. 0" if "j < n" for j + proof - + have "0 \ \f x0 - f x0\" by simp + also have "... \ c j" using x0 unfolding space_PiM by (intro delta that) auto + finally show ?thesis by simp + qed + hence sum_c_ge_0: "(\i 0" by (meson sum_nonneg zero_le_power2) + + hence t_ge_0: "t \ 0" using \_gt_0 unfolding t_def by simp + + note borel_rules = + borel_measurable_sum measurable_compose[OF _ borel_measurable_exp] + borel_measurable_times + + note int_rules = + prob_space_PiM assms(1) borel_rules + prob_space.integrable_bounded bounded_intros + have h_n: "h n \ = f \" if "\ \ space (PiM {.. + proof - + have "h n \ = (\\. f (\i\{.. i) \PiM {} M)" + unfolding h_def using leD + by (intro Bochner_Integration.integral_cong PiM_cong arg_cong[where f="f"] restrict_cong) + auto + also have "... = f (restrict \ {.." + using that unfolding space_PiM PiE_def + by (simp add: extensional_restrict) + finally show ?thesis + by simp + qed + + have h_0: "h 0 \ = (\\. f \ \PiM {.. + unfolding h_def by (intro Bochner_Integration.integral_cong PiM_cong refl) + (simp_all add:space_PiM atLeast0LessThan) + + have h_cong: "h j \ = h j \" if "restrict \ {.. {.. \ + using that unfolding h_def + by (intro Bochner_Integration.integral_cong refl arg_cong[where f="f"] merge_cong) auto + + have h_meas: "h i \ borel_measurable (PiM I M)" if "i \ n" "{.. I" for i I + proof - + have 0: "{.. {i.. map_prod (\x. restrict x {.. Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M {i..\<^sub>M Pi\<^sub>M {..x. f (merge {.. borel_measurable (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M {i.. (\\<^sub>E i\{.. n" "fst u \ Pi {..i. space (M i))" "snd u \ Pi {j..i. space (M i))" + for u j + proof - + have "merge {.. (PiE ({.. {j..i. space (M i)))" + using that by (intro iffD2[OF PiE_cancel_merge]) auto + also have "... = (\\<^sub>E i\{.. (\\<^sub>E i\{.. n" "u \ PiE {..i. space (M i))" "v \ PiE {j..i. space (M i))" + for u v j + using that by (intro merge_space_aux) (simp_all add:PiE_def) + + have delta': "\f x - f y\ \ (\i PiE {..i. space (M i))" "y \ PiE {..i. space (M i))" for x y + proof - + define m where "m i = merge {.. Pi I (\i. space (M i))" if "z \ PiE {..i. space (M i))" + "I \ {.. ({.. ({.. ({.. ({..f x - f y\ = \f (m n) - f(m 0)\" + using that unfolding m_def by (simp add:atLeast0LessThan) + also have "... = \\i < n. f (m (Suc i)) - f (m i)\" + by (subst sum_lessThan_telescope) simp + also have "... \ (\i < n. \f (m (Suc i)) - f (m i)\)" + by simp + also have "... \ (\i < n. c i)" + using that unfolding m_def by (intro delta sum_mono merge_space_aux 0 subsetI) + (simp_all add:restrict_merge 3) + finally show ?thesis + by simp + qed + + have "norm (f x) \ norm (f x0) + sum c {.. space (Pi\<^sub>M {..f x - f x0\ \ sum c {..\. (f (merge {..)))) ` space (Pi\<^sub>M {j.. n" "u \ PiE {..i. space (M i))" for u j + proof - + have "(\\. merge {..)) ` space (Pi\<^sub>M {j.. space (Pi\<^sub>M {..\. f (merge {..))) \ borel_measurable (Pi\<^sub>M {j.. n" "u \ Pi {..i. space (M i))" for j u + proof - + + have 0: "{.. {j ..) = merge {..)" for \ + by (intro merge_cong) auto + + have "(\\. merge {..)) \ Pi\<^sub>M {j..\<^sub>M Pi\<^sub>M {..\. f (merge {..))) \ borel_measurable (Pi\<^sub>M {j.. n" "u \ PiE {..i. space (M i))" for j u + using that unfolding PiE_def by (intro f_merge_meas_aux) auto + + have h_bounded: "bounded (h i ` space (PiM I M))" + if h_bounded_assms: "i \ n" "{.. I" for i I + proof - + have "merge {.. space (Pi\<^sub>M {.. (\\<^sub>E i\I. space (M i)) \ (\\<^sub>E i\{i..x. f (merge {..\<^sub>E i\I. space (M i)) \ (\\<^sub>E i\{i.. I" for i I + using that unfolding V_def by (intro bounded_intros h_bounded) auto + + have V_upd_bounded: "bounded ((\x. V j (\(j := x))) ` space (M j))" + if V_upd_bounded_assms: "\ \ space (Pi\<^sub>M {.. + proof - + have "\(j := v) \ space (Pi\<^sub>M {.. space (M j)" for v + using V_upd_bounded_assms that unfolding space_PiM PiE_def extensional_def Pi_def by auto + thus ?thesis + using that unfolding image_image[of "V j" "(\x. (\(j := x)))",symmetric] + by (intro bounded_subset[OF V_bounded[of "j" "{.. = \\. h (j+1) (\(j := \)) \ M j" (is "?L1 = ?R1") + if "\ \ space (PiM {.. + proof - + have 0: "(\x. f (merge {.., x))) \ borel_measurable (Pi\<^sub>M {j..x.(f (merge {.., x)))) ` space (Pi\<^sub>M {j..\. f (merge {.., \)) \PiM (insert j {j+1..\.(\\. f (merge {.., (\(j := \)))) \PiM {j+1..M j)" + using that(1,2) 0 1 2 by (intro product_integral_insert prob_space_imp_sigma_finite assms(1) + int_rules f_merge_meas) (simp_all) + also have "... = ?R1" + using that(2) unfolding h_def + by (intro Bochner_Integration.integral_cong arg_cong[where f="f"] ext) (auto simp:merge_def) + finally show ?thesis + by simp + qed + + have V_meas: "V i \ borel_measurable (PiM I M)" if "i < n" "{.. I" for i I + unfolding V_def using that by (intro borel_measurable_diff h_meas) auto + + have V_upd_meas: "(\x. V j (\(j := x))) \ borel_measurable (M j)" + if "j < n" "\ \ space (Pi\<^sub>M {.. + using that by (intro measurable_compose[OF _ V_meas[where I="insert j {.. = V j \" if "restrict \ {..<(j+1)} = restrict \ {..<(j+1)}" for j \ \ + using that restrict_subset_eq[OF _ that] unfolding V_def + by (intro arg_cong2[where f="(-)"] h_cong) simp_all + + have exp_V: "(\\. V j (\(j := \)) \M j) = 0" (is "?L1 = 0") + if "j < n" "\ \ space (PiM {.. + proof - + + have "fun_upd \ j ` space (M j) \ space (Pi\<^sub>M (insert j {..x. h (Suc j) (\(j := x))) ` space (M j))" + unfolding image_image[of "h (Suc j)" "\x. \(j := x)",symmetric] using that + by (intro bounded_subset[OF h_bounded[where i="j+1" and I="{..x. h (Suc j) (\(j := x))) \ borel_measurable (M j)" + using h_meas that by (intro measurable_compose[OF _ h_meas[where I="insert j {..\. h (Suc j) (\(j := \)) - h j \ \M j)" + unfolding V_def + by (intro Bochner_Integration.integral_cong arg_cong2[where f="(-)"] refl h_cong) auto + also have "... = (\\. h (Suc j) (\(j := \)) \M j) - (\\. h j \ \M j)" + using that by (intro Bochner_Integration.integral_diff int_rules 0 1) auto + also have "... = 0" + using that(1) assms(1) prob_space.prob_space unfolding h_step[OF that(2,1)] by auto + finally show ?thesis + by simp + qed + + have var_V: "\V j x - V j y\ \ c j" (is "?L1 \ ?R1") + if var_V_assms: "j < n" "{x,y} \ space (PiM {.. PiE {..i. space (M i))" and y_ran: "y \ PiE {..i. space (M i))" + using that(2) by (simp_all add:space_PiM) + + have 0: "j+1 \ n" + using that by simp + + have "?L1 = \h (Suc j) x - h j y - (h (Suc j) y - h j y)\" + unfolding V_def by (intro arg_cong[where f="abs"] arg_cong2[where f="(-)"] refl h_cong that) + also have "... = \h (j+1) x - h (j+1) y\" + by simp + also have "... = + \(\\. f(merge {..))-f(merge {..)) \PiM {j+1.." + using that unfolding h_def by (intro arg_cong[where f="abs"] f_merge_meas[OF 0] x_ran + Bochner_Integration.integral_diff[symmetric] int_rules f_merge_bounded[OF 0] y_ran) auto + also have "... \ + (\\. \f(merge {..))-f(merge {..))\ \PiM {j+1.. (\\. c j \PiM {j+1.. assume "\ \ space (Pi\<^sub>M {j + 1.. ({..)) ({..)) ({.. - (\\. f \ \(PiM {..i < n. V i \)" if "\ \ space (PiM {.. + using that unfolding V_def by (subst sum_lessThan_telescope) (simp add: h_0 h_n) + hence "?L = \

(\ in PiM {..i < n. V i \) \ \)" + by (intro arg_cong2[where f="measure"] refl Collect_restr_cong arg_cong2[where f="(\)"]) auto + also have "... \ \

(\ in PiM {..i < n. V i \) ) \ exp (t * \))" + proof (intro finite_measure.finite_measure_mono subsetI prob_space.finite_measure int_rules) + show "{\ \ space (Pi\<^sub>M {..) \ exp (t * (\i))} \ sets (Pi\<^sub>M {.. (\\. exp(t*(\i < n. V i \)) \PiM {..)" + by (intro integral_Markov_inequality_measure[where A="{}"] int_rules V_bounded V_meas) auto + also have "... = exp(t^2 * (\i\{n..)*(\\. exp(t*(\i < n. V i \)) \PiM {.. exp(t^2 * (\i\{0..)*(\\. exp(t*(\i < 0. V i \)) \PiM {..<0} M)" + proof (rule ineq_chain) + fix j assume a:"j < n" + let ?L1 = "exp (t\<^sup>2*(\i=j+1..2)/8-t*\)" + let ?L2 = "?L1 * (\\. exp (t * (\i)) \PiM {..\. exp (t * (\i)) * exp(t * V j \) \PiM (insert j {..\. (\\. exp (t * (\i(j := \)))) * exp(t * V j (\(j := \))) \M j) \PiM {..\.(\\. exp (t*(\i))*exp(t*V j (\(j := \))) \M j) \PiM {..\. exp (t*(\i))*(\\. exp(t*V j (\(j := \))) \M j) \PiM {.. ?L1 * \\. exp (t*(\i))* exp (t^2 * c j^2/8) \PiM {.. assume c:"\ \ space (Pi\<^sub>M {.. \ PiE {..i. space (M i))" + unfolding space_PiM by simp + moreover have "\(j := v) \ PiE {..i. space (M i))" if "v \ space (M j)" for v + using b that unfolding PiE_def extensional_def Pi_def by auto + ultimately show "LINT \|M j. exp (t * V j (\(j := \))) \ exp (t\<^sup>2 * (c j)\<^sup>2 / 8)" + using V_upd_meas[OF c] + by (intro prob_space.Hoeffdings_lemma_bochner_3 exp_V var_V a int_rules) + (auto simp: space_PiM) + next + show "integrable (Pi\<^sub>M {..x. exp (t * (\i2 * (c j)\<^sup>2 / 8))" + using a by (intro int_rules V_bounded V_meas) auto + qed auto + also have "... = ?L1 * ((\\. exp (t*(\i)) \PiM {..M {..\. exp (t * (\i)))" + using a by (intro int_rules V_bounded V_meas) auto + qed auto + also have "... = + exp (t\<^sup>2*(\i\insert j {j+1..2)/8-t*\) * (\\. exp (t * (\i))\PiM {..2*(\i=j..2)/8-t*\) * (\\. exp (t * (\i))\PiM {..exp(t\<^sup>2*(\i=j..2)/8-t*\)*(\\. exp (t*(\i))\PiM {..i)" by (simp add:PiM_empty atLeast0LessThan) + also have "... = exp(t * ((t * (\i))" by (simp add:algebra_simps power2_eq_square) + also have "... = exp(t * (-\/2))" using sum_c_ge_0 by (auto simp add:divide_simps t_def) + also have "... = ?R" unfolding t_def by (simp add:field_simps power2_eq_square) + finally show ?thesis by simp +qed + +theorem mc_diarmid_inequality_distr: + fixes f :: "('i \ 'a) \ real" + assumes "finite I" + assumes "\i. i \ I \ prob_space (M i)" + assumes "\i x y. i \ I \ {x,y} \ space (PiM I M) \ (\j\I-{i}. x j=y j) \ \f x-f y\\c i" + assumes f_meas: "f \ borel_measurable (PiM I M)" and \_gt_0: "\ > 0" + shows "\

(\ in PiM I M. f \ - (\\. f \ \PiM I M) \ \) \ exp (-(2*\^2)/(\i\I. (c i)^2))" + (is "?L \ ?R") +proof - + define n where "n = card I" + let ?q = "from_nat_into I" + let ?r = "to_nat_on I" + let ?f = "(\\. f (\i\I. \ (?r i)))" + + have q: "bij_betw ?q {.. I" for x + by (intro from_nat_into_to_nat_on that countable_finite assms(1)) + + have [simp]: "?r (?q x) = x" if "x < n" for x + using bij_betw_imp_surj_on[OF r] that by (intro to_nat_on_from_nat_into) auto + + have a: "\i. i \ {.. prob_space ((M \ ?q) i)" + unfolding comp_def by (intro assms(2) bij_betw_apply[OF q]) + + have b:"PiM I M = PiM I (\i. (M \ ?q) (?r i))" by (intro PiM_cong) (simp_all add:comp_def) + also have "... = distr (PiM {.. ?q)) (PiM I (\i. (M \ ?q) (?r i))) (\\. \n\I. \ (?r n))" + using r unfolding bij_betw_def by (intro distr_PiM_reindex[symmetric] a) auto + finally have c: "PiM I M = distr (PiM{..?q)) (PiM I (\i.(M\?q)(?r i))) (\\. \n\I. \ (?r n))" + by simp + + have d: "(\n\I. x (?r n)) \ space (Pi\<^sub>M I M)" if 4:"x \ space (Pi\<^sub>M {.. ?q))" for x + proof - + have "x (?r i) \ space (M i)" if "i \ I" for i + proof - + have "?r i \ {.. space ((M \ ?q) (?r i))" using that 4 PiE_mem unfolding space_PiM by blast + thus ?thesis using that unfolding comp_def by simp + qed + thus ?thesis unfolding space_PiM PiE_def by auto + qed + + have "?L = \

(\ in PiM {.. ?q). ?f \ - (\\. f \ \PiM I M) \ \)" + proof (subst c, subst measure_distr, goal_cases) + case 1 thus ?case + by (intro measurable_restrict measurable_component_singleton bij_betw_apply[OF r]) + next + case 2 thus ?case unfolding b[symmetric] by (intro measurable_sets_Collect[OF f_meas]) auto + next + case 3 thus ?case using d by (intro arg_cong2[where f="measure"] refl) (auto simp:vimage_def) + qed + also have "... = \

(\ in PiM {.. ?q). ?f \ - (\\. ?f \ \PiM {.. ?q)) \ \)" + proof (subst c, subst integral_distr, goal_cases) + case (1 \) thus ?case + by (intro measurable_restrict measurable_component_singleton bij_betw_apply[OF r]) + next + case (2 \) thus ?case unfolding b[symmetric] by (rule f_meas) + next + case 3 thus ?case by simp + qed + also have "... \ exp (-(2*\^2)/(\i_gt_0, goal_cases) + case (1 i) thus ?case by (intro a) auto + next + case (2 i x y) + have "x (?r j) = y (?r j)" if "j \ I - {?q i}" for j + proof - + have "?r j \ {..j\I - {?q i}. (\i\I. x (?r i)) j = (\i\I. y (?r i)) j" by auto + thus ?case using 2 d by (intro assms(3) bij_betw_apply[OF q]) auto + next + case 3 + have "(\x. x (?r i)) \ Pi\<^sub>M {.. ?q) \\<^sub>M M i" if "i \ I" for i + proof - + have 0:"M i = (M \ ?q) (?r i)" using that by (simp add: comp_def) + show ?thesis unfolding 0 by (intro measurable_component_singleton bij_betw_apply[OF r] that) + qed + thus ?case by (intro measurable_compose[OF _ f_meas] measurable_restrict) + qed + also have "... = ?R" by (subst sum.reindex_bij_betw[OF q]) simp + finally show ?thesis by simp +qed + +lemma (in prob_space) mc_diarmid_inequality_classic: + fixes f :: "('i \ 'a) \ real" + assumes "finite I" + assumes "indep_vars N X I" + assumes "\i x y. i \ I \ {x,y} \ space (PiM I N) \ (\j\I-{i}. x j=y j) \ \f x-f y\\c i" + assumes f_meas: "f \ borel_measurable (PiM I N)" and \_gt_0: "\ > 0" + shows "\

(\ in M. f (\i\I. X i \) - (\\. f (\i\I. X i \) \M) \ \) \ exp (-(2*\^2)/(\i\I. (c i)^2))" + (is "?L \ ?R") +proof - + note indep_imp = iffD1[OF indep_vars_iff_distr_eq_PiM''] + let ?O = "\i. distr M (N i) (X i)" + have a:"distr M (Pi\<^sub>M I N) (\x. \i\I. X i x) = Pi\<^sub>M I ?O" + using assms(2) unfolding indep_vars_def by (intro indep_imp[OF _ assms(2)]) auto + + have b: "space (PiM I ?O) = space (PiM I N)" + by (metis (no_types, lifting) a space_distr) + + have "(\i\I. X i \) \ space (Pi\<^sub>M I N)" if "\ \ space M" for \ + using assms(2) that unfolding indep_vars_def measurable_def space_PiM by auto + + hence "?L = \

(\ in M. (\i\I. X i \)\ space (Pi\<^sub>M I N)\ f (\i\I. X i \)-(\\. f (\i\I. X i \) \M)\\)" + by (intro arg_cong2[where f="measure"] Collect_restr_cong refl) auto + also have "... = \

(\ in distr M (Pi\<^sub>M I N) (\x. \i\I. X i x). f \ - (\\. f (\i\I. X i \) \M) \ \)" + proof (subst measure_distr, goal_cases) + case 1 thus ?case using assms(2) unfolding indep_vars_def by (intro measurable_restrict) auto + next + case 2 thus ?case unfolding space_distr by (intro measurable_sets_Collect[OF f_meas]) auto + next + case 3 thus ?case by (simp_all add:Int_def conj_commute) + qed + also have "... = \

(\ in PiM I ?O. f \ - (\\. f (\i\I. X i \) \M) \ \)" + unfolding a by simp + also have "... = \

(\ in PiM I ?O. f \ - (\\. f \ \ distr M (Pi\<^sub>M I N) (\x. \i\I. X i x)) \ \)" + proof (subst integral_distr[OF _ f_meas], goal_cases) + case (1 \) thus ?case using assms(2) unfolding indep_vars_def by (intro measurable_restrict)auto + next + case 2 thus ?case by simp + qed + also have "... = \

(\ in PiM I ?O. f \ - (\\. f \ \ Pi\<^sub>M I ?O) \ \)" unfolding a by simp + also have "... \ ?R" + using f_meas assms(2) b unfolding indep_vars_def + by (intro mc_diarmid_inequality_distr prob_space_distr assms(1) \_gt_0 assms(3)) auto + finally show ?thesis by simp +qed + +end \ No newline at end of file diff --git a/thys/Concentration_Inequalities/Paley_Zygmund_Inequality.thy b/thys/Concentration_Inequalities/Paley_Zygmund_Inequality.thy new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/Paley_Zygmund_Inequality.thy @@ -0,0 +1,204 @@ +section \Paley-Zygmund Inequality\ + +text \This section proves slight improvements of the Paley-Zygmund Inequality~\cite{paley1932note}. +Unfortunately, the improvements are on Wikipedia with no citation.\ + +theory Paley_Zygmund_Inequality + imports Lp.Lp +begin + +context prob_space +begin + +theorem paley_zygmund_inequality_holder: + assumes p: "1 < (p::real)" + assumes rv: "random_variable borel Z" + assumes intZp: "integrable M (\z. \Z z\ powr p)" + assumes t: "\ \ 1" + assumes ZAEpos: "AE z in M. Z z \ 0" + shows " + (expectation (\x. \Z x - \ * expectation Z\ powr p) powr (1 / (p-1))) * + prob {z \ space M. Z z > \ * expectation Z} + \ ((1-\) powr (p / (p-1)) * expectation Z powr (p / (p-1))) " +proof - + have intZ: "integrable M Z" + apply (subst bound_L1_Lp[OF _ rv intZp]) + using p by auto + + define eZ where "eZ = expectation Z" + have "eZ \ 0" + unfolding eZ_def + using ZAEpos intZ integral_ge_const prob_Collect_eq_1 by auto + + have ezp: "expectation (\x. \Z x - \ * eZ\ powr p) \ 0" + by (meson Bochner_Integration.integral_nonneg powr_ge_pzero) + + have "expectation (\z. Z z - \ * eZ) = expectation (\z. Z z + (- \ * eZ))" + by auto + moreover have "... = expectation Z + expectation (\z. - \ * eZ)" + apply (subst Bochner_Integration.integral_add) + using intZ by auto + moreover have "... = eZ + (- \ * eZ)" + apply (subst lebesgue_integral_const) + using eZ_def prob_space by auto + ultimately have *: "expectation (\z. Z z - \ * eZ) = eZ - \ * eZ" + by linarith + + have ev: "{z \ space M. \ * eZ < Z z} \ events" + using rv unfolding borel_measurable_iff_greater + by auto + + define q where "q = p / (p-1)" + + have sqI:"(indicat_real E x) powr q = indicat_real E (x::'a)" for E x + unfolding q_def + by (metis indicator_simps(1) indicator_simps(2) powr_0 powr_one_eq_one) + + have bm1: "(\z. (Z z - \ * eZ)) \ borel_measurable M" + using borel_measurable_const borel_measurable_diff rv by blast + have bm2: "(\z. indicat_real {z \ space M. Z z > \ * eZ} z) \ borel_measurable M" + using borel_measurable_indicator ev by blast + have "integrable M (\x. \Z x + (-\ * eZ)\ powr p)" + apply (intro Minkowski_inequality[OF _ rv _ intZp]) + using p by auto + then have int1: "integrable M (\x. \Z x - \ * eZ\ powr p)" + by auto + + have "integrable M + (\x. 1 * indicat_real {z \ space M. \ * eZ < Z z} x)" + apply (intro integrable_real_mult_indicator[OF ev]) + by auto + + then have int2: " integrable M + (\x. \indicat_real {z \ space M. \ * eZ < Z z} x\ powr q)" + by (auto simp add: sqI ) + + have pq:"p > (0::real)" "q > 0" "1/p + 1/q = 1" + unfolding q_def using p by (auto simp:divide_simps) + from Holder_inequality[OF pq bm1 bm2 int1 int2] + have hi: "expectation (\x. (Z x - \ * eZ) * indicat_real {z \ space M. \ * eZ < Z z} x) + \ expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / p) * + expectation (\x. \indicat_real {z \ space M. \ * eZ < Z z} x\ powr q) powr (1 / q)" + by auto + + have "eZ - \ * eZ \ + expectation (\z. (Z z - \ * eZ) * indicat_real {z \ space M. Z z > \ * eZ} z)" + unfolding *[symmetric] + apply (intro integral_mono) + using intZ ev apply auto[1] + apply (auto intro!: integrable_real_mult_indicator simp add: intZ ev)[1] + unfolding indicator_def of_bool_def + by (auto simp add: mult_nonneg_nonpos2) + + also have "... \ + expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / p) * + expectation (\x. indicat_real {z \ space M. \ * eZ < Z z} x) powr (1 / q)" + using hi by (auto simp add: sqI) + + finally have "eZ - \ * eZ \ + expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / p) * + expectation (\x. indicat_real {z \ space M. \ * eZ < Z z} x) powr (1 / q)" + by auto + + then have "(eZ - \ * eZ) powr q \ + (expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / p) * + expectation (\x. indicat_real {z \ space M. \ * eZ < Z z} x) powr (1 / q)) powr q" + by (smt (verit, ccfv_SIG) \0 \ eZ\ mult_left_le_one_le powr_mono2 pq(2) right_diff_distrib' t zero_le_mult_iff) + + also have "... = + (expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / p)) powr q * + (expectation (\x. indicat_real {z \ space M. \ * eZ < Z z} x) powr (1 / q)) powr q" + using powr_ge_pzero powr_mult by presburger + also have "... = + (expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / p)) powr q * + (expectation (\x. indicat_real {z \ space M. \ * eZ < Z z} x))" + by (smt (verit, ccfv_SIG) Bochner_Integration.integral_nonneg divide_le_eq_1_pos indicator_pos_le nonzero_eq_divide_eq p powr_one powr_powr q_def) + also have "... = + (expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / (p-1))) * + (expectation (\x. indicat_real {z \ space M. \ * eZ < Z z} x))" + by (smt (verit, ccfv_threshold) divide_divide_eq_right divide_self_if p powr_powr q_def times_divide_eq_left) + also have "... = + (expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / (p-1))) * + prob {z \ space M. Z z > \ * eZ}" + by (simp add: ev) + + finally have 1: "(eZ - \ * eZ) powr q \ + (expectation (\x. \Z x - \ * eZ\ powr p) powr (1 / (p-1))) * + prob {z \ space M. Z z > \ * eZ}" by linarith + + have "(eZ - \ * eZ) powr q = ((1 - \) * eZ) powr q" + by (simp add: mult.commute right_diff_distrib) + also have "... = (1 - \) powr q * eZ powr q" + by (simp add: \0 \ eZ\ powr_mult t) + finally show ?thesis using 1 eZ_def q_def by force +qed + +corollary paley_zygmund_inequality: + assumes rv: "random_variable borel Z" + assumes intZsq: "integrable M (\z. (Z z)^2)" + assumes t: "\ \ 1" + assumes Zpos: "\z. z \ space M \ Z z \ 0" + shows " + (variance Z + (1-\)^2 * (expectation Z)^2) * + prob {z \ space M. Z z > \ * expectation Z} + \ (1-\)^2 * (expectation Z)^2" +proof - + have ZAEpos: "AE z in M. Z z \ 0" + by (simp add: Zpos) + + define p where "p = (2::real)" + have p1: "1 < p" using p_def by auto + have " integrable M (\z. \Z z\ powr p)" unfolding p_def + using intZsq by auto + + from paley_zygmund_inequality_holder[OF p1 rv this t ZAEpos] + have "(1 - \) powr (p / (p - 1)) * (expectation Z powr (p / (p - 1))) + \ expectation (\x. \Z x - \ * expectation Z\ powr p) powr (1 / (p - 1)) * + prob {z \ space M. \ * expectation Z < Z z}" . + + then have hi: "(1 - \)^2 * (expectation Z)^2 + \ expectation (\x. (Z x - \ * expectation Z)^2) * + prob {z \ space M. \ * expectation Z < Z z}" + unfolding p_def by (auto simp add: Zpos t) + + have intZ: "integrable M Z" + apply (subst square_integrable_imp_integrable[OF rv intZsq]) + by auto + + define eZ where "eZ = expectation Z" + have "eZ \ 0" + unfolding eZ_def + using Bochner_Integration.integral_nonneg Zpos by blast + + have ezp: "expectation (\x. \Z x - \ * eZ\ powr p) \ 0" + by (meson Bochner_Integration.integral_nonneg powr_ge_pzero) + + have "expectation (\z. Z z - \ * eZ) = expectation (\z. Z z + (- \ * eZ))" + by auto + also have "... = expectation Z + expectation (\z. - \ * eZ)" + apply (subst Bochner_Integration.integral_add) + using intZ by auto + also have "... = eZ + (- \ * eZ)" + apply (subst lebesgue_integral_const) + using eZ_def prob_space by auto + finally have *: "expectation (\z. Z z - \ * eZ) = eZ - \ * eZ" + by linarith + have "variance Z = + variance (\z. (Z z - \ * eZ))" + using "*" eZ_def by auto + also have "... = + expectation (\z. (Z z - \ * eZ)^2) + - (expectation (\x. Z x - \ * eZ))\<^sup>2" + apply (subst variance_eq) + by (auto simp add: intZ power2_diff intZsq) + also have "... = expectation (\z. (Z z - \ * eZ)^2) - ((1-\)^2 * eZ^2)" + unfolding * by (auto simp:algebra_simps power2_eq_square) + finally have veq: "expectation (\z. (Z z - \ * eZ)^2) = (variance Z + (1-\)^2 * eZ^2)" + by linarith + thus ?thesis + using hi by (simp add: eZ_def) +qed + +end + +end \ No newline at end of file diff --git a/thys/Concentration_Inequalities/ROOT b/thys/Concentration_Inequalities/ROOT new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/ROOT @@ -0,0 +1,17 @@ +chapter AFP + +session Concentration_Inequalities = "HOL-Probability" + + options [timeout = 1200] + sessions + Lp + theories + Bennett_Inequality + Bienaymes_Identity + Cantelli_Inequality + Concentration_Inequalities_Preliminary + Efron_Stein_Inequality + McDiarmid_Inequality + Paley_Zygmund_Inequality + document_files + "root.tex" + "root.bib" diff --git a/thys/Concentration_Inequalities/document/root.bib b/thys/Concentration_Inequalities/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/document/root.bib @@ -0,0 +1,98 @@ + +@inbook{mcdiarmid1989, + series={London Mathematical Society Lecture Note Series}, + chapter={On the method of bounded differences}, + DOI={10.1017/CBO9781107359949.008}, + title={Surveys in Combinatorics, 1989: Invited Papers at the Twelfth British Combinatorial Conference}, + publisher={Cambridge University Press}, + author={McDiarmid, Colin}, + year={1989}, + pages={148 -- 188}, +} + +@article{efron1981, + author = {B. Efron and C. Stein}, + title = {{The Jackknife Estimate of Variance}}, + volume = {9}, + journal = {The Annals of Statistics}, + number = {3}, + pages = {586 -- 596}, + year = {1981}, + doi = {10.1214/aos/1176345462}, +} + +@article{steele1986, + author = {J. Michael Steele}, + title = {{An Efron-Stein Inequality for Nonsymmetric Statistics}}, + volume = {14}, + journal = {The Annals of Statistics}, + number = {2}, + pages = {753 -- 758}, + year = {1986}, + doi = {10.1214/aos/1176349952}, +} + +@inbook{loeve1977, + author="Lo{\`e}ve, M.", + chapter="Sums of Independent Random Variables", + title="Probability Theory I", + year="1977", + publisher="Springer New York", + address="New York, NY", + pages="235--279", + isbn="978-1-4684-9464-8", + doi="10.1007/978-1-4684-9464-8_6", +} + +@article{bennett1962, + title={Probability inequalities for the sum of independent random variables}, + author={Bennett, George}, + journal={Journal of the American Statistical Association}, + volume={57}, + number={297}, + pages={33--45}, + year={1962}, + publisher={Taylor \& Francis} +} + +@inproceedings{DBLP:conf/ac/BoucheronLB03, + author = {St{\'{e}}phane Boucheron and + G{\'{a}}bor Lugosi and + Olivier Bousquet}, + editor = {Olivier Bousquet and + Ulrike von Luxburg and + Gunnar R{\"{a}}tsch}, + title = {Concentration Inequalities}, + booktitle = {Advanced Lectures on Machine Learning, {ML} Summer Schools 2003, Canberra, + Australia, February 2-14, 2003, T{\"{u}}bingen, Germany, August + 4-16, 2003, Revised Lectures}, + series = {Lecture Notes in Computer Science}, + volume = {3176}, + pages = {208--240}, + publisher = {Springer}, + year = {2003}, + url = {https://doi.org/10.1007/978-3-540-28650-9\_9}, + doi = {10.1007/978-3-540-28650-9\_9}, + timestamp = {Tue, 14 May 2019 10:00:49 +0200}, + biburl = {https://dblp.org/rec/conf/ac/BoucheronLB03.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{cantelli1929sui, + title={Sui confini della probabilita}, + author={Cantelli, Francesco Paolo}, + booktitle={Atti del Congresso Internazionale dei Matematici: Bologna del 3 al 10 de settembre di 1928}, + pages={47--60}, + year={1929} +} + +@inproceedings{paley1932note, + title={A note on analytic functions in the unit circle}, + author={Paley, Raymond EAC and Zygmund, Antoni}, + booktitle={Mathematical Proceedings of the Cambridge Philosophical Society}, + volume={28}, + number={3}, + pages={266--272}, + year={1932}, + organization={Cambridge University Press} +} diff --git a/thys/Concentration_Inequalities/document/root.tex b/thys/Concentration_Inequalities/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Concentration_Inequalities/document/root.tex @@ -0,0 +1,35 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\usepackage{pdfsetup} +\urlstyle{rm} +\isabellestyle{it} +\begin{document} + +\title{Concentration Inequalities} +\author{Emin Karayel and Yong Kiam Tan$^*$} +\maketitle +\def\thefootnote{*}\footnotetext{The authors contributed equally to this work.}\def\thefootnote{\arabic{footnote}} + +\abstract{Concentration inequalities provide bounds on how a random variable +(or a sum/composition of random variables) deviate from their expectation, +usually based on moments/independence of the variables. + +The most important concentration inequalities (the Markov, Chebyshev, and +Hoelder inequalities and the Chernoff bounds) are already part of +HOL-Probability. This entry collects more advanced results, such as +Bennett's/Bernstein's Inequality, Bienaym\'e's Identity, Cantelli's Inequality, +the Efron-Stein Inequality, McDiarmid's Inequality, and the Paley-Zygmund +Inequality.} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,788 +1,789 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel +Concentration_Inequalities CRDT CRYSTALS-Kyber CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cardinality_Continuum Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Catoids Cauchy Cayley_Hamilton Certification_Monads Ceva Chandy_Lamport Chebyshev_Polynomials Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots Coupledsim_Contrasim CryptHOL CryptoBasedCompositionalProperties Crypto_Standards Cubic_Quartic_Equations DCR-ExecutionEquivalence DFS_Framework DOM_Components DPRM_Theorem DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic DigitsInBase Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Directed_Sets Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation Disintegration DiskPaxos Distributed_Distinct_Elements Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Earley_Parser Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Efficient_Weighted_Path_Order Elimination_Of_Repeated_Factors Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Euler_Polyhedron_Formula Eudoxus_Reals Eval_FO Example-Submission Executable_Randomized_Algorithms Expander_Graphs Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FO_Theory_Rewriting FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Fixed_Length_Vector Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic Given_Clause_Loops GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Gray_Codes Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual Hypergraph_Basics Hypergraph_Colourings IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IO_Language_Conformance IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_Series Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lovasz_Local Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MHComputation MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines MLSS_Decision_Proc ML_Unification Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Multirelations_Heterogeneous Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Nominal_Myhill_Nerode Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect_Fields Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polygonal_Number_Theorem Polylog Polynomial_Crit_Geometry Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic Q0_Metatheory Q0_Soundness QHLProver QR_Decomposition Quantales Quantales_Converse Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Cardinality Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 S_Finite_Measure_Monad Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Standard_Borel_Spaces Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Three_Squares Timed_Automata Topological_Semantics Topology TortoiseHare TsirelsonBound Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Transport Treaps Tree-Automata Tree_Decomposition Tree_Enumeration Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeckendorf Zeta_3_Irrational Zeta_Function pGCL Labeled_Transition_Systems Pushdown_Systems