# HG changeset patch # User desharna # Date 1614071589 -3600 # Node ID 8b6fa865bac490a5b816c59dd83a65cb0b220c14 # Parent f84a93f1de2fdd1a3d3d6c4b2db5a22d2b93da26# Parent 04c9a2cd7686e2eccce4dca1f8206b4bc5dbc5ba merged diff -r f84a93f1de2f -r 8b6fa865bac4 .hgtags --- a/.hgtags Fri Feb 19 11:52:34 2021 +0100 +++ b/.hgtags Tue Feb 23 10:13:09 2021 +0100 @@ -37,10 +37,4 @@ 91162dd89571fb9ddfa36844fdb1a16aea13adcf Isabelle2018 83774d669b5181fb28d19d7a0219fbf6c6d38aab Isabelle2019 abf3e80bd815c2c062b02c78b256f7ba27481380 Isabelle2020 -21ff9c1a464494b3a61c3538650664cc1b42c0cb Isabelle2021-RC0 -d4b67dc6f4ebd5f0fbd4ed1cccd0cc32c344d122 Isabelle2021-RC1 -802647edfe7be4478ca47a6e54e4d73733347e02 Isabelle2021-RC2 -02422c9add5e1c608290e48f3f0815c93ab00c1d Isabelle2021-RC3 -2ab14dbc6feb5e64c9c0c93ff2dff28f34a23f28 Isabelle2021-RC4 -a88dbf2a020fbd4ebee247f56fcc56e851e1f928 Isabelle2021-RC5 -ed36e33a2e4b01751c93c8ad28c07f8b00e11722 Isabelle2021-RC6 +7e2a9a8c2b85f10d81f3be433878fe51fa13eb6f Isabelle2021 diff -r f84a93f1de2f -r 8b6fa865bac4 Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST Fri Feb 19 11:52:34 2021 +0100 +++ b/Admin/Release/CHECKLIST Tue Feb 23 10:13:09 2021 +0100 @@ -80,6 +80,10 @@ isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2021 Isabelle2021_linux.tar.gz + docker login + + docker push makarius/isabelle:Isabelle2021 + https://hub.docker.com/r/makarius/isabelle https://docs.docker.com/engine/reference/commandline/push diff -r f84a93f1de2f -r 8b6fa865bac4 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Feb 19 11:52:34 2021 +0100 +++ b/Admin/components/components.sha1 Tue Feb 23 10:13:09 2021 +0100 @@ -222,7 +222,9 @@ edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300 naproche-20210129.tar.gz 810ee0f35adada9bf970c33fd80b986ab2255bf3 naproche-20210201.tar.gz +4a4e56fd03b7ba4edd38046f853873a90cf55d1a naproche-4ad61140062f.tar.gz 77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz +9c02ecf93863c3289002c5e5ac45a83e2505984c naproche-755224402e36.tar.gz e1b34e8f54e7e5844873612635444fed434718a1 naproche-7d0947a91dd5.tar.gz 26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz diff -r f84a93f1de2f -r 8b6fa865bac4 CONTRIBUTORS --- a/CONTRIBUTORS Fri Feb 19 11:52:34 2021 +0100 +++ b/CONTRIBUTORS Tue Feb 23 10:13:09 2021 +0100 @@ -6,6 +6,10 @@ Contributions to this Isabelle version -------------------------------------- +* February 2021: Manuel Eberl + New material in HOL-Analysis/HOL-Probability, most notably Hoeffding's + inequality and the negative binomial distribution + * January 2021: Jakub Kądziołka Some lemmas for HOL-Computational_Algebra. diff -r f84a93f1de2f -r 8b6fa865bac4 NEWS --- a/NEWS Fri Feb 19 11:52:34 2021 +0100 +++ b/NEWS Tue Feb 23 10:13:09 2021 +0100 @@ -4,6 +4,60 @@ (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) +New in this Isabelle version +---------------------------- + +*** HOL *** + +* Theory Multiset: dedicated predicate "multiset" is gone, use +explict expression instead. Minor INCOMPATIBILITY. + +* HOL-Analysis/HOL-Probability: indexed products of discrete +distributions, negative binomial distribution, Hoeffding's inequality, +Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some +more small lemmas. Some theorems that were stated awkwardly before were +corrected. Minor INCOMPATIBILITY. + + +*** ML *** + +* External bash processes are always managed by Isabelle/Scala, in +contrast to Isabelle2021 where this was only done for macOS on Apple +Silicon. + +The main Isabelle/ML interface is Isabelle_System.bash_process with +result type Process_Result.T (resembling class Process_Result in Scala); +derived operations Isabelle_System.bash and Isabelle_System.bash_output +provide similar functionality as before. Rare INCOMPATIBILITY due to +subtle semantic differences: + + - Processes invoked from Isabelle/ML actually run in the context of + the Java VM of Isabelle/Scala. The settings environment and current + working directory are usually the same on both sides, but there can be + subtle corner cases (e.g. unexpected uses of "cd" or "putenv" in ML). + + - Output via stdout and stderr is line-oriented: Unix vs. Windows + line-endings are normalized towards Unix; presence or absence of a + final newline is irrelevant. The original lines are available as + Process_Result.out_lines/err_lines; the concatenated versions + Process_Result.out/err *omit* a trailing newline (using + Library.trim_line, which was occasional seen in applications before, + but is no longer necessary). + + - Output needs to be plain text encoded in UTF-8: Isabelle/Scala + recodes it temporarily as UTF-16. This works for well-formed Unicode + text, but not for arbitrary byte strings. In such cases, the bash + script should write tempory files, managed by Isabelle/ML operations + like Isabelle_System.with_tmp_file to create a file name and + File.read to retrieve its content. + +New Process_Result.timing works as in Isabelle/Scala, based on direct +measurements of the bash_process wrapper in C: elapsed time is always +available, CPU time is only available on Linux and macOS, GC time is +unavailable. + + + New in Isabelle2021 (February 2021) ----------------------------------- diff -r f84a93f1de2f -r 8b6fa865bac4 etc/components --- a/etc/components Fri Feb 19 11:52:34 2021 +0100 +++ b/etc/components Tue Feb 23 10:13:09 2021 +0100 @@ -1,4 +1,4 @@ -#hard-wired components +#built-in components src/Tools/jEdit src/Tools/Graphview src/Tools/VSCode diff -r f84a93f1de2f -r 8b6fa865bac4 etc/settings --- a/etc/settings Fri Feb 19 11:52:34 2021 +0100 +++ b/etc/settings Tue Feb 23 10:13:09 2021 +0100 @@ -16,7 +16,7 @@ ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" -ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -J-Xms512m -J-Xmx4g -J-Xss16m" +ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:11 -J-Xms512m -J-Xmx4g -J-Xss16m" classpath "$ISABELLE_HOME/lib/classes/Pure.jar" diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Algebra/Polynomial_Divisibility.thy --- a/src/HOL/Algebra/Polynomial_Divisibility.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1507,7 +1507,7 @@ assumes "p \ carrier (poly_ring R)" shows "alg_mult p = count (roots p)" using finite_number_of_roots[OF assms] unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] - by (simp add: multiset_def roots_def) + by (simp add: roots_def) lemma (in domain) roots_mem_iff_is_root: assumes "p \ carrier (poly_ring R)" shows "x \# roots p \ is_root p x" diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Analysis/Bochner_Integration.thy --- a/src/HOL/Analysis/Bochner_Integration.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Analysis/Bochner_Integration.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1315,6 +1315,27 @@ using integrableI_bounded[of f M] has_bochner_integral_implies_finite_norm[of M f] unfolding integrable.simps has_bochner_integral.simps[abs_def] by auto +lemma (in finite_measure) square_integrable_imp_integrable: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, real_normed_div_algebra}" + assumes [measurable]: "f \ borel_measurable M" + assumes "integrable M (\x. f x ^ 2)" + shows "integrable M f" +proof - + have less_top: "emeasure M (space M) < top" + using finite_emeasure_space by (meson top.not_eq_extremum) + have "nn_integral M (\x. norm (f x)) ^ 2 \ + nn_integral M (\x. norm (f x) ^ 2) * emeasure M (space M)" + using Cauchy_Schwarz_nn_integral[of "\x. norm (f x)" M "\_. 1"] + by (simp add: ennreal_power) + also have "\ < \" + using assms(2) less_top + by (subst (asm) integrable_iff_bounded) (auto simp: norm_power ennreal_mult_less_top) + finally have "nn_integral M (\x. norm (f x)) < \" + by (simp add: power_less_top_ennreal) + thus ?thesis + by (simp add: integrable_iff_bounded) +qed + lemma integrable_bound: fixes f :: "'a \ 'b::{banach, second_countable_topology}" and g :: "'a \ 'c::{banach, second_countable_topology}" @@ -2065,16 +2086,50 @@ have "{x \ space M. u x \ c} = {x \ space M. ennreal(1/c) * u x \ 1} \ (space M)" using \c>0\ by (auto simp: ennreal_mult'[symmetric]) - then have "emeasure M {x \ space M. u x \ c} = emeasure M ({x \ space M. ennreal(1/c) * u x \ 1} \ (space M))" + then have "emeasure M {x \ space M. u x \ c} = emeasure M ({x \ space M. ennreal(1/c) * u x \ 1})" by simp also have "... \ ennreal(1/c) * (\\<^sup>+ x. ennreal(u x) * indicator (space M) x \M)" by (rule nn_integral_Markov_inequality) (auto simp add: assms) also have "... \ ennreal(1/c) * (\x. u x \M)" - apply (rule mult_left_mono) using * \c>0\ by auto + by (rule mult_left_mono) (use * \c > 0\ in auto) finally show ?thesis using \0 by (simp add: ennreal_mult'[symmetric]) qed +theorem integral_Markov_inequality_measure: + assumes [measurable]: "integrable M u" and "A \ sets M" and "AE x in M. 0 \ u x" "0 < (c::real)" + shows "measure M {x\space M. u x \ c} \ (\x. u x \M) / c" +proof - + have le: "emeasure M {x\space M. u x \ c} \ ennreal ((1/c) * (\x. u x \M))" + by (rule integral_Markov_inequality) (use assms in auto) + also have "\ < top" + by auto + finally have "ennreal (measure M {x\space M. u x \ c}) = emeasure M {x\space M. u x \ c}" + by (intro emeasure_eq_ennreal_measure [symmetric]) auto + also note le + finally show ?thesis + by (subst (asm) ennreal_le_iff) + (auto intro!: divide_nonneg_pos Bochner_Integration.integral_nonneg_AE assms) +qed + +theorem%important (in finite_measure) second_moment_method: + assumes [measurable]: "f \ M \\<^sub>M borel" + assumes "integrable M (\x. f x ^ 2)" + defines "\ \ lebesgue_integral M f" + assumes "a > 0" + shows "measure M {x\space M. \f x\ \ a} \ lebesgue_integral M (\x. f x ^ 2) / a\<^sup>2" +proof - + have integrable: "integrable M f" + using assms by (blast dest: square_integrable_imp_integrable) + have "{x\space M. \f x\ \ a} = {x\space M. f x ^ 2 \ a\<^sup>2}" + using \a > 0\ by (simp flip: abs_le_square_iff) + hence "measure M {x\space M. \f x\ \ a} = measure M {x\space M. f x ^ 2 \ a\<^sup>2}" + by simp + also have "\ \ lebesgue_integral M (\x. f x ^ 2) / a\<^sup>2" + using assms by (intro integral_Markov_inequality_measure) auto + finally show ?thesis . +qed + lemma integral_ineq_eq_0_then_AE: fixes f::"_ \ real" assumes "AE x in M. f x \ g x" "integrable M f" "integrable M g" diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Analysis/Borel_Space.thy --- a/src/HOL/Analysis/Borel_Space.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Analysis/Borel_Space.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1640,6 +1640,12 @@ shows "f \ M \\<^sub>M borel \ g \ M \\<^sub>M borel \ (\x. f x - g x) \ M \\<^sub>M borel" unfolding is_borel_def[symmetric] by transfer simp +lemma borel_measurable_power_ennreal [measurable (raw)]: + fixes f :: "_ \ ennreal" + assumes f: "f \ borel_measurable M" + shows "(\x. (f x) ^ n) \ borel_measurable M" + by (induction n) (use f in auto) + lemma borel_measurable_prod_ennreal[measurable (raw)]: fixes f :: "'c \ 'a \ ennreal" assumes "\i. i \ S \ f i \ borel_measurable M" diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1174,13 +1174,18 @@ qed theorem nn_integral_Markov_inequality: - assumes u: "u \ borel_measurable M" and "A \ sets M" - shows "(emeasure M) ({x\space M. 1 \ c * u x} \ A) \ c * (\\<^sup>+ x. u x * indicator A x \M)" + assumes u: "(\x. u x * indicator A x) \ borel_measurable M" and "A \ sets M" + shows "(emeasure M) ({x\A. 1 \ c * u x}) \ c * (\\<^sup>+ x. u x * indicator A x \M)" (is "(emeasure M) ?A \ _ * ?PI") proof - - have "?A \ sets M" - using \A \ sets M\ u by auto - hence "(emeasure M) ?A = (\\<^sup>+ x. indicator ?A x \M)" + define u' where "u' = (\x. u x * indicator A x)" + have [measurable]: "u' \ borel_measurable M" + using u unfolding u'_def . + have "{x\space M. c * u' x \ 1} \ sets M" + by measurable + also have "{x\space M. c * u' x \ 1} = ?A" + using sets.sets_into_space[OF \A \ sets M\] by (auto simp: u'_def indicator_def) + finally have "(emeasure M) ?A = (\\<^sup>+ x. indicator ?A x \M)" using nn_integral_indicator by simp also have "\ \ (\\<^sup>+ x. c * (u x * indicator A x) \M)" using u by (auto intro!: nn_integral_mono_AE simp: indicator_def) @@ -1189,6 +1194,37 @@ finally show ?thesis . qed +lemma Chernoff_ineq_nn_integral_ge: + assumes s: "s > 0" and [measurable]: "A \ sets M" + assumes [measurable]: "(\x. f x * indicator A x) \ borel_measurable M" + shows "emeasure M {x\A. f x \ a} \ + ennreal (exp (-s * a)) * nn_integral M (\x. ennreal (exp (s * f x)) * indicator A x)" +proof - + define f' where "f' = (\x. f x * indicator A x)" + have [measurable]: "f' \ borel_measurable M" + using assms(3) unfolding f'_def by assumption + have "(\x. ennreal (exp (s * f' x)) * indicator A x) \ borel_measurable M" + by simp + also have "(\x. ennreal (exp (s * f' x)) * indicator A x) = + (\x. ennreal (exp (s * f x)) * indicator A x)" + by (auto simp: f'_def indicator_def fun_eq_iff) + finally have meas: "\ \ borel_measurable M" . + + have "{x\A. f x \ a} = {x\A. ennreal (exp (-s * a)) * ennreal (exp (s * f x)) \ 1}" + using s by (auto simp: exp_minus field_simps simp flip: ennreal_mult) + also have "emeasure M \ \ ennreal (exp (-s * a)) * + (\\<^sup>+x. ennreal (exp (s * f x)) * indicator A x \M)" + by (intro order.trans[OF nn_integral_Markov_inequality] meas) auto + finally show ?thesis . +qed + +lemma Chernoff_ineq_nn_integral_le: + assumes s: "s > 0" and [measurable]: "A \ sets M" + assumes [measurable]: "f \ borel_measurable M" + shows "emeasure M {x\A. f x \ a} \ + ennreal (exp (s * a)) * nn_integral M (\x. ennreal (exp (-s * f x)) * indicator A x)" + using Chernoff_ineq_nn_integral_ge[of s A M "\x. -f x" "-a"] assms by simp + lemma nn_integral_noteq_infinite: assumes g: "g \ borel_measurable M" and "integral\<^sup>N M g \ \" shows "AE x in M. g x \ \" @@ -1432,7 +1468,7 @@ qed lemma nn_integral_0_iff: - assumes u: "u \ borel_measurable M" + assumes u [measurable]: "u \ borel_measurable M" shows "integral\<^sup>N M u = 0 \ emeasure M {x\space M. u x \ 0} = 0" (is "_ \ (emeasure M) ?A = 0") proof - @@ -1449,9 +1485,13 @@ have "0 = (SUP n. (emeasure M) (?M n \ ?A))" proof - { fix n :: nat - from nn_integral_Markov_inequality[OF u, of ?A "of_nat n"] u - have "(emeasure M) (?M n \ ?A) \ 0" - by (simp add: ennreal_of_nat_eq_real_of_nat u_eq *) + have "emeasure M {x \ ?A. 1 \ of_nat n * u x} \ + of_nat n * \\<^sup>+ x. u x * indicator ?A x \M" + by (intro nn_integral_Markov_inequality) auto + also have "{x \ ?A. 1 \ of_nat n * u x} = (?M n \ ?A)" + by (auto simp: ennreal_of_nat_eq_real_of_nat u_eq * ) + finally have "emeasure M (?M n \ ?A) \ 0" + by (simp add: ennreal_of_nat_eq_real_of_nat u_eq * ) moreover have "0 \ (emeasure M) (?M n \ ?A)" using u by auto ultimately have "(emeasure M) (?M n \ ?A) = 0" by auto } thus ?thesis by simp @@ -1617,6 +1657,93 @@ by (subst step) auto qed (insert bound, auto simp add: le_fun_def INF_apply[abs_def] top_fun_def intro!: meas f g) + +text \Cauchy--Schwarz inequality for \<^const>\nn_integral\\ + +lemma sum_of_squares_ge_ennreal: + fixes a b :: ennreal + shows "2 * a * b \ a\<^sup>2 + b\<^sup>2" +proof (cases a; cases b) + fix x y + assume xy: "x \ 0" "y \ 0" and [simp]: "a = ennreal x" "b = ennreal y" + have "0 \ (x - y)\<^sup>2" + by simp + also have "\ = x\<^sup>2 + y\<^sup>2 - 2 * x * y" + by (simp add: algebra_simps power2_eq_square) + finally have "2 * x * y \ x\<^sup>2 + y\<^sup>2" + by simp + hence "ennreal (2 * x * y) \ ennreal (x\<^sup>2 + y\<^sup>2)" + by (intro ennreal_leI) + thus ?thesis using xy + by (simp add: ennreal_mult ennreal_power) +qed auto + +lemma Cauchy_Schwarz_nn_integral: + assumes [measurable]: "f \ borel_measurable M" "g \ borel_measurable M" + shows "(\\<^sup>+x. f x * g x \M)\<^sup>2 \ (\\<^sup>+x. f x ^ 2 \M) * (\\<^sup>+x. g x ^ 2 \M)" +proof (cases "(\\<^sup>+x. f x * g x \M) = 0") + case False + define F where "F = nn_integral M (\x. f x ^ 2)" + define G where "G = nn_integral M (\x. g x ^ 2)" + from False have "\(AE x in M. f x = 0 \ g x = 0)" + by (auto simp: nn_integral_0_iff_AE) + hence "\(AE x in M. f x = 0)" and "\(AE x in M. g x = 0)" + by (auto intro: AE_disjI1 AE_disjI2) + hence nz: "F \ 0" "G \ 0" + by (auto simp: nn_integral_0_iff_AE F_def G_def) + + show ?thesis + proof (cases "F = \ \ G = \") + case True + thus ?thesis using nz + by (auto simp: F_def G_def) + next + case False + define F' where "F' = ennreal (sqrt (enn2real F))" + define G' where "G' = ennreal (sqrt (enn2real G))" + from False have fin: "F < top" "G < top" + by (simp_all add: top.not_eq_extremum) + have F'_sqr: "F'\<^sup>2 = F" + using False by (cases F) (auto simp: F'_def ennreal_power) + have G'_sqr: "G'\<^sup>2 = G" + using False by (cases G) (auto simp: G'_def ennreal_power) + have nz': "F' \ 0" "G' \ 0" and fin': "F' \ \" "G' \ \" + using F'_sqr G'_sqr nz fin by auto + from fin' have fin'': "F' < top" "G' < top" + by (auto simp: top.not_eq_extremum) + + have "2 * (F' / F') * (G' / G') * (\\<^sup>+x. f x * g x \M) = + F' * G' * (\\<^sup>+x. 2 * (f x / F') * (g x / G') \M)" + using nz' fin'' + by (simp add: divide_ennreal_def algebra_simps ennreal_inverse_mult flip: nn_integral_cmult) + also have "F'/ F' = 1" + using nz' fin'' by simp + also have "G'/ G' = 1" + using nz' fin'' by simp + also have "2 * 1 * 1 = (2 :: ennreal)" by simp + also have "F' * G' * (\\<^sup>+ x. 2 * (f x / F') * (g x / G') \M) \ + F' * G' * (\\<^sup>+x. (f x / F')\<^sup>2 + (g x / G')\<^sup>2 \M)" + by (intro mult_left_mono nn_integral_mono sum_of_squares_ge_ennreal) auto + also have "\ = F' * G' * (F / F'\<^sup>2 + G / G'\<^sup>2)" using nz + by (auto simp: nn_integral_add algebra_simps nn_integral_divide F_def G_def) + also have "F / F'\<^sup>2 = 1" + using nz F'_sqr fin by simp + also have "G / G'\<^sup>2 = 1" + using nz G'_sqr fin by simp + also have "F' * G' * (1 + 1) = 2 * (F' * G')" + by (simp add: mult_ac) + finally have "(\\<^sup>+x. f x * g x \M) \ F' * G'" + by (subst (asm) ennreal_mult_le_mult_iff) auto + hence "(\\<^sup>+x. f x * g x \M)\<^sup>2 \ (F' * G')\<^sup>2" + by (intro power_mono_ennreal) + also have "\ = F * G" + by (simp add: algebra_simps F'_sqr G'_sqr) + finally show ?thesis + by (simp add: F_def G_def) + qed +qed auto + + (* TODO: rename? *) subsection \Integral under concrete measures\ diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Analysis/Set_Integral.thy --- a/src/HOL/Analysis/Set_Integral.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Analysis/Set_Integral.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1079,4 +1079,87 @@ qed qed + + +theorem integral_Markov_inequality': + fixes u :: "'a \ real" + assumes [measurable]: "set_integrable M A u" and "A \ sets M" + assumes "AE x in M. x \ A \ u x \ 0" and "0 < (c::real)" + shows "emeasure M {x\A. u x \ c} \ (1/c::real) * (\x\A. u x \M)" +proof - + have "(\x. u x * indicator A x) \ borel_measurable M" + using assms by (auto simp: set_integrable_def mult_ac) + hence "(\x. ennreal (u x * indicator A x)) \ borel_measurable M" + by measurable + also have "(\x. ennreal (u x * indicator A x)) = (\x. ennreal (u x) * indicator A x)" + by (intro ext) (auto simp: indicator_def) + finally have meas: "\ \ borel_measurable M" . + from assms(3) have AE: "AE x in M. 0 \ u x * indicator A x" + by eventually_elim (auto simp: indicator_def) + have nonneg: "set_lebesgue_integral M A u \ 0" + unfolding set_lebesgue_integral_def + by (intro Bochner_Integration.integral_nonneg_AE eventually_mono[OF AE]) (auto simp: mult_ac) + + have A: "A \ space M" + using \A \ sets M\ by (simp add: sets.sets_into_space) + have "{x \ A. u x \ c} = {x \ A. ennreal(1/c) * u x \ 1}" + using \c>0\ A by (auto simp: ennreal_mult'[symmetric]) + then have "emeasure M {x \ A. u x \ c} = emeasure M ({x \ A. ennreal(1/c) * u x \ 1})" + by simp + also have "... \ ennreal(1/c) * (\\<^sup>+ x. ennreal(u x) * indicator A x \M)" + by (intro nn_integral_Markov_inequality meas assms) + also have "(\\<^sup>+ x. ennreal(u x) * indicator A x \M) = ennreal (set_lebesgue_integral M A u)" + unfolding set_lebesgue_integral_def nn_integral_set_ennreal using assms AE + by (subst nn_integral_eq_integral) (simp_all add: mult_ac set_integrable_def) + finally show ?thesis + using \c > 0\ nonneg by (subst ennreal_mult) auto +qed + +theorem integral_Markov_inequality'_measure: + assumes [measurable]: "set_integrable M A u" and "A \ sets M" + and "AE x in M. x \ A \ 0 \ u x" "0 < (c::real)" + shows "measure M {x\A. u x \ c} \ (\x\A. u x \M) / c" +proof - + have nonneg: "set_lebesgue_integral M A u \ 0" + unfolding set_lebesgue_integral_def + by (intro Bochner_Integration.integral_nonneg_AE eventually_mono[OF assms(3)]) + (auto simp: mult_ac) + have le: "emeasure M {x\A. u x \ c} \ ennreal ((1/c) * (\x\A. u x \M))" + by (rule integral_Markov_inequality') (use assms in auto) + also have "\ < top" + by auto + finally have "ennreal (measure M {x\A. u x \ c}) = emeasure M {x\A. u x \ c}" + by (intro emeasure_eq_ennreal_measure [symmetric]) auto + also note le + finally show ?thesis using nonneg + by (subst (asm) ennreal_le_iff) + (auto intro!: divide_nonneg_pos Bochner_Integration.integral_nonneg_AE assms) +qed + +theorem%important (in finite_measure) Chernoff_ineq_ge: + assumes s: "s > 0" + assumes integrable: "set_integrable M A (\x. exp (s * f x))" and "A \ sets M" + shows "measure M {x\A. f x \ a} \ exp (-s * a) * (\x\A. exp (s * f x) \M)" +proof - + have "{x\A. f x \ a} = {x\A. exp (s * f x) \ exp (s * a)}" + using s by auto + also have "measure M \ \ set_lebesgue_integral M A (\x. exp (s * f x)) / exp (s * a)" + by (intro integral_Markov_inequality'_measure assms) auto + finally show ?thesis + by (simp add: exp_minus field_simps) +qed + +theorem%important (in finite_measure) Chernoff_ineq_le: + assumes s: "s > 0" + assumes integrable: "set_integrable M A (\x. exp (-s * f x))" and "A \ sets M" + shows "measure M {x\A. f x \ a} \ exp (s * a) * (\x\A. exp (-s * f x) \M)" +proof - + have "{x\A. f x \ a} = {x\A. exp (-s * f x) \ exp (-s * a)}" + using s by auto + also have "measure M \ \ set_lebesgue_integral M A (\x. exp (-s * f x)) / exp (-s * a)" + by (intro integral_Markov_inequality'_measure assms) auto + finally show ?thesis + by (simp add: exp_minus field_simps) +qed + end diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Complete_Partial_Order.thy --- a/src/HOL/Complete_Partial_Order.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Complete_Partial_Order.thy Tue Feb 23 10:13:09 2021 +0100 @@ -123,11 +123,7 @@ proof (cases "\z\M. f x \ z") case True then have "f x \ Sup M" - apply rule - apply (erule order_trans) - apply (rule ccpo_Sup_upper[OF chM]) - apply assumption - done + by (blast intro: ccpo_Sup_upper[OF chM] order_trans) then show ?thesis .. next case False @@ -141,11 +137,7 @@ proof (cases "\x\M. y \ x") case True then have "y \ Sup M" - apply rule - apply (erule order_trans) - apply (rule ccpo_Sup_upper[OF Sup(1)]) - apply assumption - done + by (blast intro: ccpo_Sup_upper[OF Sup(1)] order_trans) then show ?thesis .. next case False with Sup @@ -328,20 +320,17 @@ qed qed moreover - have "Sup A = Sup {x \ A. P x}" if "\x\A. \y\A. x \ y \ P y" for P + have "Sup A = Sup {x \ A. P x}" if "\x. x\A \ \y\A. x \ y \ P y" for P proof (rule antisym) have chain_P: "chain (\) {x \ A. P x}" by (rule chain_compr [OF chain]) show "Sup A \ Sup {x \ A. P x}" - apply (rule ccpo_Sup_least [OF chain]) - apply (drule that [rule_format]) - apply clarify - apply (erule order_trans) - apply (simp add: ccpo_Sup_upper [OF chain_P]) - done + proof (rule ccpo_Sup_least [OF chain]) + show "\x. x \ A \ x \ \ {x \ A. P x}" + by (blast intro: ccpo_Sup_upper[OF chain_P] order_trans dest: that) + qed show "Sup {x \ A. P x} \ Sup A" apply (rule ccpo_Sup_least [OF chain_P]) - apply clarify apply (simp add: ccpo_Sup_upper [OF chain]) done qed @@ -350,13 +339,15 @@ | "\x. x \ A \ Q x" "Sup A = Sup {x \ A. Q x}" by blast then show "P (Sup A) \ Q (Sup A)" - apply cases - apply simp_all - apply (rule disjI1) - apply (rule ccpo.admissibleD [OF P chain_compr [OF chain]]; simp) - apply (rule disjI2) - apply (rule ccpo.admissibleD [OF Q chain_compr [OF chain]]; simp) - done + proof cases + case 1 + then show ?thesis + using ccpo.admissibleD [OF P chain_compr [OF chain]] by force + next + case 2 + then show ?thesis + using ccpo.admissibleD [OF Q chain_compr [OF chain]] by force + qed qed end diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Computational_Algebra/Factorial_Ring.thy --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1208,8 +1208,7 @@ lift_definition prime_factorization :: "'a \ 'a multiset" is "\x p. if prime p then multiplicity p x else 0" - unfolding multiset_def -proof clarify +proof - fix x :: 'a show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A") proof (cases "x = 0") @@ -2097,7 +2096,7 @@ from \finite S\ S(1) have "(\p\S. p ^ f p) \ 0" by auto with S(2) have nz: "n \ 0" by auto from S_eq \finite S\ have count_A: "count A = f" - unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def) + unfolding A_def by (subst multiset.Abs_multiset_inverse) simp_all from S_eq count_A have set_mset_A: "set_mset A = S" by (simp only: set_mset_def) from S(2) have "normalize n = (\p\S. p ^ f p)" . diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Computational_Algebra/Primes.thy --- a/src/HOL/Computational_Algebra/Primes.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Computational_Algebra/Primes.thy Tue Feb 23 10:13:09 2021 +0100 @@ -728,8 +728,8 @@ define g where "g = (\x. if x \ S then f x else 0)" define A where "A = Abs_multiset g" have "{x. g x > 0} \ S" by (auto simp: g_def) - from finite_subset[OF this assms(1)] have [simp]: "g \ multiset" - by (simp add: multiset_def) + from finite_subset[OF this assms(1)] have [simp]: "finite {x. 0 < g x}" + by simp from assms have count_A: "count A x = g x" for x unfolding A_def by simp have set_mset_A: "set_mset A = {x\S. f x > 0}" diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Feb 23 10:13:09 2021 +0100 @@ -10,47 +10,93 @@ imports Finite_Set Lattices_Big Set_Interval begin +locale preordering_bdd = preordering +begin + +definition bdd :: \'a set \ bool\ + where unfold: \bdd A \ (\M. \x \ A. x \<^bold>\ M)\ + +lemma empty [simp, intro]: + \bdd {}\ + by (simp add: unfold) + +lemma I [intro]: + \bdd A\ if \\x. x \ A \ x \<^bold>\ M\ + using that by (auto simp add: unfold) + +lemma E: + assumes \bdd A\ + obtains M where \\x. x \ A \ x \<^bold>\ M\ + using assms that by (auto simp add: unfold) + +lemma I2: + \bdd (f ` A)\ if \\x. x \ A \ f x \<^bold>\ M\ + using that by (auto simp add: unfold) + +lemma mono: + \bdd A\ if \bdd B\ \A \ B\ + using that by (auto simp add: unfold) + +lemma Int1 [simp]: + \bdd (A \ B)\ if \bdd A\ + using mono that by auto + +lemma Int2 [simp]: + \bdd (A \ B)\ if \bdd B\ + using mono that by auto + +end + context preorder begin -definition "bdd_above A \ (\M. \x \ A. x \ M)" -definition "bdd_below A \ (\m. \x \ A. m \ x)" +sublocale bdd_above: preordering_bdd \(\)\ \(<)\ + defines bdd_above_primitive_def: bdd_above = bdd_above.bdd .. + +sublocale bdd_below: preordering_bdd \(\)\ \(>)\ + defines bdd_below_primitive_def: bdd_below = bdd_below.bdd .. + +lemma bdd_above_def: \bdd_above A \ (\M. \x \ A. x \ M)\ + by (fact bdd_above.unfold) -lemma bdd_aboveI[intro]: "(\x. x \ A \ x \ M) \ bdd_above A" - by (auto simp: bdd_above_def) +lemma bdd_below_def: \bdd_below A \ (\M. \x \ A. M \ x)\ + by (fact bdd_below.unfold) -lemma bdd_belowI[intro]: "(\x. x \ A \ m \ x) \ bdd_below A" - by (auto simp: bdd_below_def) +lemma bdd_aboveI: "(\x. x \ A \ x \ M) \ bdd_above A" + by (fact bdd_above.I) + +lemma bdd_belowI: "(\x. x \ A \ m \ x) \ bdd_below A" + by (fact bdd_below.I) lemma bdd_aboveI2: "(\x. x \ A \ f x \ M) \ bdd_above (f`A)" - by force + by (fact bdd_above.I2) lemma bdd_belowI2: "(\x. x \ A \ m \ f x) \ bdd_below (f`A)" - by force + by (fact bdd_below.I2) -lemma bdd_above_empty [simp, intro]: "bdd_above {}" - unfolding bdd_above_def by auto +lemma bdd_above_empty: "bdd_above {}" + by (fact bdd_above.empty) -lemma bdd_below_empty [simp, intro]: "bdd_below {}" - unfolding bdd_below_def by auto +lemma bdd_below_empty: "bdd_below {}" + by (fact bdd_below.empty) lemma bdd_above_mono: "bdd_above B \ A \ B \ bdd_above A" - by (metis (full_types) bdd_above_def order_class.le_neq_trans psubsetD) + by (fact bdd_above.mono) lemma bdd_below_mono: "bdd_below B \ A \ B \ bdd_below A" - by (metis bdd_below_def order_class.le_neq_trans psubsetD) + by (fact bdd_below.mono) -lemma bdd_above_Int1 [simp]: "bdd_above A \ bdd_above (A \ B)" - using bdd_above_mono by auto +lemma bdd_above_Int1: "bdd_above A \ bdd_above (A \ B)" + by (fact bdd_above.Int1) -lemma bdd_above_Int2 [simp]: "bdd_above B \ bdd_above (A \ B)" - using bdd_above_mono by auto +lemma bdd_above_Int2: "bdd_above B \ bdd_above (A \ B)" + by (fact bdd_above.Int2) -lemma bdd_below_Int1 [simp]: "bdd_below A \ bdd_below (A \ B)" - using bdd_below_mono by auto +lemma bdd_below_Int1: "bdd_below A \ bdd_below (A \ B)" + by (fact bdd_below.Int1) -lemma bdd_below_Int2 [simp]: "bdd_below B \ bdd_below (A \ B)" - using bdd_below_mono by auto +lemma bdd_below_Int2: "bdd_below B \ bdd_below (A \ B)" + by (fact bdd_below.Int2) lemma bdd_above_Ioo [simp, intro]: "bdd_above {a <..< b}" by (auto simp add: bdd_above_def intro!: exI[of _ b] less_imp_le) @@ -90,11 +136,21 @@ end -lemma (in order_top) bdd_above_top[simp, intro!]: "bdd_above A" - by (rule bdd_aboveI[of _ top]) simp +context order_top +begin + +lemma bdd_above_top [simp, intro!]: "bdd_above A" + by (rule bdd_aboveI [of _ top]) simp + +end -lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A" - by (rule bdd_belowI[of _ bot]) simp +context order_bot +begin + +lemma bdd_below_bot [simp, intro!]: "bdd_below A" + by (rule bdd_belowI [of _ bot]) simp + +end lemma bdd_above_image_mono: "mono f \ bdd_above A \ bdd_above (f`A)" by (auto simp: bdd_above_def mono_def) diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Library/DAList_Multiset.thy --- a/src/HOL/Library/DAList_Multiset.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Library/DAList_Multiset.thy Tue Feb 23 10:13:09 2021 +0100 @@ -100,7 +100,7 @@ definition count_of :: "('a \ nat) list \ 'a \ nat" where "count_of xs x = (case map_of xs x of None \ 0 | Some n \ n)" -lemma count_of_multiset: "count_of xs \ multiset" +lemma count_of_multiset: "finite {x. 0 < count_of xs x}" proof - let ?A = "{x::'a. 0 < (case map_of xs x of None \ 0::nat | Some n \ n)}" have "?A \ dom (map_of xs)" @@ -117,7 +117,7 @@ with finite_dom_map_of [of xs] have "finite ?A" by (auto intro: finite_subset) then show ?thesis - by (simp add: count_of_def fun_eq_iff multiset_def) + by (simp add: count_of_def fun_eq_iff) qed lemma count_simps [simp]: @@ -291,7 +291,7 @@ let ?inv = "{xs :: ('a \ nat) list. (distinct \ map fst) xs}" note cs[simp del] = count_simps have count[simp]: "\x. count (Abs_multiset (count_of x)) = count_of x" - by (rule Abs_multiset_inverse[OF count_of_multiset]) + by (rule Abs_multiset_inverse) (simp add: count_of_multiset) assume ys: "ys \ ?inv" then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))" unfolding Bag_def unfolding Alist_inverse[OF ys] diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Library/Extended_Nonnegative_Real.thy --- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Feb 23 10:13:09 2021 +0100 @@ -555,6 +555,32 @@ lemma ennreal_add_bot[simp]: "bot + x = (x::ennreal)" by transfer simp +lemma add_top_right_ennreal [simp]: "x + top = (top :: ennreal)" + by (cases x) auto + +lemma add_top_left_ennreal [simp]: "top + x = (top :: ennreal)" + by (cases x) auto + +lemma ennreal_top_mult_left [simp]: "x \ 0 \ x * top = (top :: ennreal)" + by (subst ennreal_mult_eq_top_iff) auto + +lemma ennreal_top_mult_right [simp]: "x \ 0 \ top * x = (top :: ennreal)" + by (subst ennreal_mult_eq_top_iff) auto + + +lemma power_top_ennreal [simp]: "n > 0 \ top ^ n = (top :: ennreal)" + by (induction n) auto + +lemma power_eq_top_ennreal_iff: "x ^ n = top \ x = (top :: ennreal) \ n > 0" + by (induction n) (auto simp: ennreal_mult_eq_top_iff) + +lemma ennreal_mult_le_mult_iff: "c \ 0 \ c \ top \ c * a \ c * b \ a \ (b :: ennreal)" + including ennreal.lifting + by (transfer, subst ereal_mult_le_mult_iff) (auto simp: top_ereal_def) + +lemma power_mono_ennreal: "x \ y \ x ^ n \ (y ^ n :: ennreal)" + by (induction n) (auto intro!: mult_mono) + instance ennreal :: semiring_char_0 proof (standard, safe intro!: linorder_injI) have *: "1 + of_nat k \ (0::ennreal)" for k @@ -683,6 +709,9 @@ unfolding divide_ennreal_def by transfer (auto simp: ereal_zero_less_0_iff top_ereal_def ereal_0_gt_inverse) +lemma add_divide_distrib_ennreal: "(a + b) / c = a / c + b / (c :: ennreal)" + by (simp add: divide_ennreal_def ring_distribs) + lemma divide_right_mono_ennreal: fixes a b c :: ennreal shows "a \ b \ a / c \ b / c" @@ -976,6 +1005,10 @@ qed qed +lemma power_divide_distrib_ennreal [algebra_simps]: + "(x / y) ^ n = x ^ n / (y ^ n :: ennreal)" + by (simp add: divide_ennreal_def algebra_simps ennreal_inverse_power) + lemma ennreal_divide_numeral: "0 \ x \ ennreal x / numeral b = ennreal (x / numeral b)" by (subst divide_ennreal[symmetric]) auto @@ -983,6 +1016,11 @@ by (induction A rule: infinite_finite_induct) (auto simp: ennreal_mult prod_nonneg) +lemma prod_mono_ennreal: + assumes "\x. x \ A \ f x \ (g x :: ennreal)" + shows "prod f A \ prod g A" + using assms by (induction A rule: infinite_finite_induct) (auto intro!: mult_mono) + lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \ (a = b \ c \ 0)" proof (cases "0 \ c") case True diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Feb 23 10:13:09 2021 +0100 @@ -14,17 +14,19 @@ subsection \The type of multisets\ -definition "multiset = {f :: 'a \ nat. finite {x. f x > 0}}" - -typedef 'a multiset = "multiset :: ('a \ nat) set" +typedef 'a multiset = \{f :: 'a \ nat. finite {x. f x > 0}}\ morphisms count Abs_multiset - unfolding multiset_def proof - show "(\x. 0::nat) \ {f. finite {x. f x > 0}}" by simp + show \(\x. 0::nat) \ {f. finite {x. f x > 0}}\ + by simp qed setup_lifting type_definition_multiset +lemma count_Abs_multiset: + \count (Abs_multiset f) = f\ if \finite {x. f x > 0}\ + by (rule Abs_multiset_inverse) (simp add: that) + lemma multiset_eq_iff: "M = N \ (\a. count M a = count N a)" by (simp only: count_inject [symmetric] fun_eq_iff) @@ -33,37 +35,15 @@ text \Preservation of the representing set \<^term>\multiset\.\ -lemma const0_in_multiset: "(\a. 0) \ multiset" - by (simp add: multiset_def) - -lemma only1_in_multiset: "(\b. if b = a then n else 0) \ multiset" - by (simp add: multiset_def) - -lemma union_preserves_multiset: "M \ multiset \ N \ multiset \ (\a. M a + N a) \ multiset" - by (simp add: multiset_def) - lemma diff_preserves_multiset: - assumes "M \ multiset" - shows "(\a. M a - N a) \ multiset" -proof - - have "{x. N x < M x} \ {x. 0 < M x}" - by auto - with assms show ?thesis - by (auto simp add: multiset_def intro: finite_subset) -qed + \finite {x. 0 < M x - N x}\ if \finite {x. 0 < M x}\ for M N :: \'a \ nat\ + using that by (rule rev_finite_subset) auto lemma filter_preserves_multiset: - assumes "M \ multiset" - shows "(\x. if P x then M x else 0) \ multiset" -proof - - have "{x. (P x \ 0 < M x) \ P x} \ {x. 0 < M x}" - by auto - with assms show ?thesis - by (auto simp add: multiset_def intro: finite_subset) -qed - -lemmas in_multiset = const0_in_multiset only1_in_multiset - union_preserves_multiset diff_preserves_multiset filter_preserves_multiset + \finite {x. 0 < (if P x then M x else 0)}\ if \finite {x. 0 < M x}\ for M N :: \'a \ nat\ + using that by (rule rev_finite_subset) auto + +lemmas in_multiset = diff_preserves_multiset filter_preserves_multiset subsection \Representing multisets\ @@ -74,19 +54,19 @@ begin lift_definition zero_multiset :: "'a multiset" is "\a. 0" -by (rule const0_in_multiset) + by simp abbreviation Mempty :: "'a multiset" ("{#}") where "Mempty \ 0" lift_definition plus_multiset :: "'a multiset \ 'a multiset \ 'a multiset" is "\M N. (\a. M a + N a)" -by (rule union_preserves_multiset) + by simp lift_definition minus_multiset :: "'a multiset \ 'a multiset \ 'a multiset" is "\ M N. \a. M a - N a" -by (rule diff_preserves_multiset) + by (rule diff_preserves_multiset) instance - by (standard; transfer; simp add: fun_eq_iff) + by (standard; transfer) (simp_all add: fun_eq_iff) end @@ -99,9 +79,9 @@ end lemma add_mset_in_multiset: - assumes M: \M \ multiset\ - shows \(\b. if b = a then Suc (M b) else M b) \ multiset\ - using assms by (simp add: multiset_def flip: insert_Collect) + \finite {x. 0 < (if x = a then Suc (M x) else M x)}\ + if \finite {x. 0 < M x}\ + using that by (simp add: flip: insert_Collect) lift_definition add_mset :: "'a \ 'a multiset \ 'a multiset" is "\a M b. if b = a then Suc (M b) else M b" @@ -246,7 +226,7 @@ lemma finite_set_mset [iff]: "finite (set_mset M)" - using count [of M] by (simp add: multiset_def) + using count [of M] by simp lemma set_mset_add_mset_insert [simp]: \set_mset (add_mset a A) = insert a (set_mset A)\ by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits) @@ -1029,18 +1009,18 @@ lift_definition Inf_multiset :: "'a multiset set \ 'a multiset" is "\A i. if A = {} then 0 else Inf ((\f. f i) ` A)" proof - - fix A :: "('a \ nat) set" assume *: "\x. x \ A \ x \ multiset" - have "finite {i. (if A = {} then 0 else Inf ((\f. f i) ` A)) > 0}" unfolding multiset_def + fix A :: "('a \ nat) set" + assume *: "\f. f \ A \ finite {x. 0 < f x}" + show \finite {i. 0 < (if A = {} then 0 else INF f\A. f i)}\ proof (cases "A = {}") case False then obtain f where "f \ A" by blast hence "{i. Inf ((\f. f i) ` A) > 0} \ {i. f i > 0}" by (auto intro: less_le_trans[OF _ cInf_lower]) - moreover from \f \ A\ * have "finite \" by (simp add: multiset_def) + moreover from \f \ A\ * have "finite \" by simp ultimately have "finite {i. Inf ((\f. f i) ` A) > 0}" by (rule finite_subset) with False show ?thesis by simp qed simp_all - thus "(\i. if A = {} then 0 else INF f\A. f i) \ multiset" by (simp add: multiset_def) qed instance .. @@ -1098,10 +1078,9 @@ qed lemma Sup_multiset_in_multiset: - assumes "A \ {}" "subset_mset.bdd_above A" - shows "(\i. SUP X\A. count X i) \ multiset" - unfolding multiset_def -proof + \finite {i. 0 < (SUP M\A. count M i)}\ + if \A \ {}\ \subset_mset.bdd_above A\ +proof - have "{i. Sup ((\X. count X i) ` A) > 0} \ (\X\A. {i. 0 < count X i})" proof safe fix i assume pos: "(SUP X\A. count X i) > 0" @@ -1109,20 +1088,21 @@ proof (rule ccontr) assume "i \ (\X\A. {i. 0 < count X i})" hence "\X\A. count X i \ 0" by (auto simp: count_eq_zero_iff) - with assms have "(SUP X\A. count X i) \ 0" + with that have "(SUP X\A. count X i) \ 0" by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto with pos show False by simp qed qed - moreover from assms have "finite \" by (rule bdd_above_multiset_imp_finite_support) - ultimately show "finite {i. Sup ((\X. count X i) ` A) > 0}" by (rule finite_subset) + moreover from that have "finite \" + by (rule bdd_above_multiset_imp_finite_support) + ultimately show "finite {i. Sup ((\X. count X i) ` A) > 0}" + by (rule finite_subset) qed lemma count_Sup_multiset_nonempty: - assumes "A \ {}" "subset_mset.bdd_above A" - shows "count (Sup A) x = (SUP X\A. count X x)" - using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset) - + \count (Sup A) x = (SUP X\A. count X x)\ + if \A \ {}\ \subset_mset.bdd_above A\ + using that by (simp add: Sup_multiset_def Sup_multiset_in_multiset count_Abs_multiset) interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\#)" "(\#)" "(\#)" "(\#)" proof @@ -3700,7 +3680,7 @@ by (rule natLeq_cinfinite) show "ordLeq3 (card_of (set_mset X)) natLeq" for X by transfer - (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def) + (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric]) show "rel_mset R OO rel_mset S \ rel_mset (R OO S)" for R S unfolding rel_mset_def[abs_def] OO_def apply clarify @@ -3749,9 +3729,8 @@ unfolding rel_mset_def Grp_def by auto declare multiset.count[simp] -declare Abs_multiset_inverse[simp] +declare count_Abs_multiset[simp] declare multiset.count_inverse[simp] -declare union_preserves_multiset[simp] lemma rel_mset_Plus: assumes ab: "R a b" diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Orderings.thy Tue Feb 23 10:13:09 2021 +0100 @@ -13,114 +13,160 @@ subsection \Abstract ordering\ -locale ordering = - fixes less_eq :: "'a \ 'a \ bool" (infix "\<^bold>\" 50) - and less :: "'a \ 'a \ bool" (infix "\<^bold><" 50) - assumes strict_iff_order: "a \<^bold>< b \ a \<^bold>\ b \ a \ b" - assumes refl: "a \<^bold>\ a" \ \not \iff\: makes problems due to multiple (dual) interpretations\ - and antisym: "a \<^bold>\ b \ b \<^bold>\ a \ a = b" - and trans: "a \<^bold>\ b \ b \<^bold>\ c \ a \<^bold>\ c" +locale partial_preordering = + fixes less_eq :: \'a \ 'a \ bool\ (infix \\<^bold>\\ 50) + assumes refl: \a \<^bold>\ a\ \ \not \iff\: makes problems due to multiple (dual) interpretations\ + and trans: \a \<^bold>\ b \ b \<^bold>\ c \ a \<^bold>\ c\ + +locale preordering = partial_preordering + + fixes less :: \'a \ 'a \ bool\ (infix \\<^bold><\ 50) + assumes strict_iff_not: \a \<^bold>< b \ a \<^bold>\ b \ \ b \<^bold>\ a\ begin lemma strict_implies_order: - "a \<^bold>< b \ a \<^bold>\ b" - by (simp add: strict_iff_order) + \a \<^bold>< b \ a \<^bold>\ b\ + by (simp add: strict_iff_not) + +lemma irrefl: \ \not \iff\: makes problems due to multiple (dual) interpretations\ + \\ a \<^bold>< a\ + by (simp add: strict_iff_not) + +lemma asym: + \a \<^bold>< b \ b \<^bold>< a \ False\ + by (auto simp add: strict_iff_not) + +lemma strict_trans1: + \a \<^bold>\ b \ b \<^bold>< c \ a \<^bold>< c\ + by (auto simp add: strict_iff_not intro: trans) + +lemma strict_trans2: + \a \<^bold>< b \ b \<^bold>\ c \ a \<^bold>< c\ + by (auto simp add: strict_iff_not intro: trans) + +lemma strict_trans: + \a \<^bold>< b \ b \<^bold>< c \ a \<^bold>< c\ + by (auto intro: strict_trans1 strict_implies_order) + +end + +lemma preordering_strictI: \ \Alternative introduction rule with bias towards strict order\ + fixes less_eq (infix \\<^bold>\\ 50) + and less (infix \\<^bold><\ 50) + assumes less_eq_less: \\a b. a \<^bold>\ b \ a \<^bold>< b \ a = b\ + assumes asym: \\a b. a \<^bold>< b \ \ b \<^bold>< a\ + assumes irrefl: \\a. \ a \<^bold>< a\ + assumes trans: \\a b c. a \<^bold>< b \ b \<^bold>< c \ a \<^bold>< c\ + shows \preordering (\<^bold>\) (\<^bold><)\ +proof + fix a b + show \a \<^bold>< b \ a \<^bold>\ b \ \ b \<^bold>\ a\ + by (auto simp add: less_eq_less asym irrefl) +next + fix a + show \a \<^bold>\ a\ + by (auto simp add: less_eq_less) +next + fix a b c + assume \a \<^bold>\ b\ and \b \<^bold>\ c\ then show \a \<^bold>\ c\ + by (auto simp add: less_eq_less intro: trans) +qed + +lemma preordering_dualI: + fixes less_eq (infix \\<^bold>\\ 50) + and less (infix \\<^bold><\ 50) + assumes \preordering (\a b. b \<^bold>\ a) (\a b. b \<^bold>< a)\ + shows \preordering (\<^bold>\) (\<^bold><)\ +proof - + from assms interpret preordering \\a b. b \<^bold>\ a\ \\a b. b \<^bold>< a\ . + show ?thesis + by standard (auto simp: strict_iff_not refl intro: trans) +qed + +locale ordering = partial_preordering + + fixes less :: \'a \ 'a \ bool\ (infix \\<^bold><\ 50) + assumes strict_iff_order: \a \<^bold>< b \ a \<^bold>\ b \ a \ b\ + assumes antisym: \a \<^bold>\ b \ b \<^bold>\ a \ a = b\ +begin + +sublocale preordering \(\<^bold>\)\ \(\<^bold><)\ +proof + show \a \<^bold>< b \ a \<^bold>\ b \ \ b \<^bold>\ a\ for a b + by (auto simp add: strict_iff_order intro: antisym) +qed lemma strict_implies_not_eq: - "a \<^bold>< b \ a \ b" + \a \<^bold>< b \ a \ b\ by (simp add: strict_iff_order) lemma not_eq_order_implies_strict: - "a \ b \ a \<^bold>\ b \ a \<^bold>< b" + \a \ b \ a \<^bold>\ b \ a \<^bold>< b\ by (simp add: strict_iff_order) lemma order_iff_strict: - "a \<^bold>\ b \ a \<^bold>< b \ a = b" + \a \<^bold>\ b \ a \<^bold>< b \ a = b\ by (auto simp add: strict_iff_order refl) -lemma irrefl: \ \not \iff\: makes problems due to multiple (dual) interpretations\ - "\ a \<^bold>< a" - by (simp add: strict_iff_order) - -lemma asym: - "a \<^bold>< b \ b \<^bold>< a \ False" - by (auto simp add: strict_iff_order intro: antisym) - -lemma strict_trans1: - "a \<^bold>\ b \ b \<^bold>< c \ a \<^bold>< c" - by (auto simp add: strict_iff_order intro: trans antisym) - -lemma strict_trans2: - "a \<^bold>< b \ b \<^bold>\ c \ a \<^bold>< c" - by (auto simp add: strict_iff_order intro: trans antisym) - -lemma strict_trans: - "a \<^bold>< b \ b \<^bold>< c \ a \<^bold>< c" - by (auto intro: strict_trans1 strict_implies_order) - -lemma eq_iff: "a = b \ a \<^bold>\ b \ b \<^bold>\ a" +lemma eq_iff: \a = b \ a \<^bold>\ b \ b \<^bold>\ a\ by (auto simp add: refl intro: antisym) end -text \Alternative introduction rule with bias towards strict order\ - -lemma ordering_strictI: - fixes less_eq (infix "\<^bold>\" 50) - and less (infix "\<^bold><" 50) - assumes less_eq_less: "\a b. a \<^bold>\ b \ a \<^bold>< b \ a = b" - assumes asym: "\a b. a \<^bold>< b \ \ b \<^bold>< a" - assumes irrefl: "\a. \ a \<^bold>< a" - assumes trans: "\a b c. a \<^bold>< b \ b \<^bold>< c \ a \<^bold>< c" - shows "ordering less_eq less" +lemma ordering_strictI: \ \Alternative introduction rule with bias towards strict order\ + fixes less_eq (infix \\<^bold>\\ 50) + and less (infix \\<^bold><\ 50) + assumes less_eq_less: \\a b. a \<^bold>\ b \ a \<^bold>< b \ a = b\ + assumes asym: \\a b. a \<^bold>< b \ \ b \<^bold>< a\ + assumes irrefl: \\a. \ a \<^bold>< a\ + assumes trans: \\a b c. a \<^bold>< b \ b \<^bold>< c \ a \<^bold>< c\ + shows \ordering (\<^bold>\) (\<^bold><)\ proof fix a b - show "a \<^bold>< b \ a \<^bold>\ b \ a \ b" + show \a \<^bold>< b \ a \<^bold>\ b \ a \ b\ by (auto simp add: less_eq_less asym irrefl) next fix a - show "a \<^bold>\ a" + show \a \<^bold>\ a\ by (auto simp add: less_eq_less) next fix a b c - assume "a \<^bold>\ b" and "b \<^bold>\ c" then show "a \<^bold>\ c" + assume \a \<^bold>\ b\ and \b \<^bold>\ c\ then show \a \<^bold>\ c\ by (auto simp add: less_eq_less intro: trans) next fix a b - assume "a \<^bold>\ b" and "b \<^bold>\ a" then show "a = b" + assume \a \<^bold>\ b\ and \b \<^bold>\ a\ then show \a = b\ by (auto simp add: less_eq_less asym) qed lemma ordering_dualI: - fixes less_eq (infix "\<^bold>\" 50) - and less (infix "\<^bold><" 50) - assumes "ordering (\a b. b \<^bold>\ a) (\a b. b \<^bold>< a)" - shows "ordering less_eq less" + fixes less_eq (infix \\<^bold>\\ 50) + and less (infix \\<^bold><\ 50) + assumes \ordering (\a b. b \<^bold>\ a) (\a b. b \<^bold>< a)\ + shows \ordering (\<^bold>\) (\<^bold><)\ proof - - from assms interpret ordering "\a b. b \<^bold>\ a" "\a b. b \<^bold>< a" . + from assms interpret ordering \\a b. b \<^bold>\ a\ \\a b. b \<^bold>< a\ . show ?thesis by standard (auto simp: strict_iff_order refl intro: antisym trans) qed locale ordering_top = ordering + - fixes top :: "'a" ("\<^bold>\") - assumes extremum [simp]: "a \<^bold>\ \<^bold>\" + fixes top :: \'a\ (\\<^bold>\\) + assumes extremum [simp]: \a \<^bold>\ \<^bold>\\ begin lemma extremum_uniqueI: - "\<^bold>\ \<^bold>\ a \ a = \<^bold>\" + \\<^bold>\ \<^bold>\ a \ a = \<^bold>\\ by (rule antisym) auto lemma extremum_unique: - "\<^bold>\ \<^bold>\ a \ a = \<^bold>\" + \\<^bold>\ \<^bold>\ a \ a = \<^bold>\\ by (auto intro: antisym) lemma extremum_strict [simp]: - "\ (\<^bold>\ \<^bold>< a)" + \\ (\<^bold>\ \<^bold>< a)\ using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl) lemma not_eq_extremum: - "a \ \<^bold>\ \ a \<^bold>< \<^bold>\" + \a \ \<^bold>\ \ a \<^bold>< \<^bold>\\ by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum) end @@ -165,6 +211,16 @@ and order_trans: "x \ y \ y \ z \ x \ z" begin +sublocale order: preordering less_eq less + dual_order: preordering greater_eq greater +proof - + interpret preordering less_eq less + by standard (auto intro: order_trans simp add: less_le_not_le) + show \preordering less_eq less\ + by (fact preordering_axioms) + then show \preordering greater_eq greater\ + by (rule preordering_dualI) +qed + text \Reflexivity.\ lemma eq_refl: "x = y \ x \ y" @@ -217,7 +273,7 @@ text \Dual order\ lemma dual_preorder: - "class.preorder (\) (>)" + \class.preorder (\) (>)\ by standard (auto simp add: less_le_not_le intro: order_trans) end diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Central_Limit_Theorem.thy --- a/src/HOL/Probability/Central_Limit_Theorem.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Probability/Central_Limit_Theorem.thy Tue Feb 23 10:13:09 2021 +0100 @@ -14,7 +14,6 @@ and \ :: real and S :: "nat \ 'a \ real" assumes X_indep: "indep_vars (\i. borel) X UNIV" - and X_integrable: "\n. integrable M (X n)" and X_mean_0: "\n. expectation (X n) = 0" and \_pos: "\ > 0" and X_square_integrable: "\n. integrable M (\x. (X n x)\<^sup>2)" @@ -27,8 +26,10 @@ define \ where "\ n = char (distr M borel (?S' n))" for n define \ where "\ n t = char \ (t / sqrt (\\<^sup>2 * n))" for n t - have X_rv [simp, measurable]: "\n. random_variable borel (X n)" + have X_rv [simp, measurable]: "random_variable borel (X n)" for n using X_indep unfolding indep_vars_def2 by simp + have X_integrable [simp, intro]: "integrable M (X n)" for n + by (rule square_integrable_imp_integrable[OF _ X_square_integrable]) simp_all interpret \: real_distribution \ by (subst X_distrib [symmetric, of 0], rule real_distribution_distr, simp) @@ -120,7 +121,6 @@ and \ :: real and S :: "nat \ 'a \ real" assumes X_indep: "indep_vars (\i. borel) X UNIV" - and X_integrable: "\n. integrable M (X n)" and X_mean: "\n. expectation (X n) = m" and \_pos: "\ > 0" and X_square_integrable: "\n. integrable M (\x. (X n x)\<^sup>2)" @@ -131,8 +131,12 @@ proof (intro central_limit_theorem_zero_mean) show "indep_vars (\i. borel) X' UNIV" unfolding X'_def[abs_def] using X_indep by (rule indep_vars_compose2) auto - show "integrable M (X' n)" "expectation (X' n) = 0" for n - using X_integrable X_mean by (auto simp: X'_def[abs_def] prob_space) + have X_rv [simp, measurable]: "random_variable borel (X n)" for n + using X_indep unfolding indep_vars_def2 by simp + have X_integrable [simp, intro]: "integrable M (X n)" for n + by (rule square_integrable_imp_integrable[OF _ X_square_integrable]) simp_all + show "expectation (X' n) = 0" for n + using X_mean by (auto simp: X'_def[abs_def] prob_space) show "\ > 0" "integrable M (\x. (X' n x)\<^sup>2)" "variance (X' n) = \\<^sup>2" for n using \0 < \\ X_integrable X_mean X_square_integrable X_variance unfolding X'_def by (auto simp: prob_space power2_diff) diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Conditional_Expectation.thy --- a/src/HOL/Probability/Conditional_Expectation.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Probability/Conditional_Expectation.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1291,7 +1291,7 @@ finally have "\q y\ > \q 0\ - e" by auto then show ?thesis unfolding e_def by simp qed - have "emeasure M {x \ space M. \X x\ < d} \ emeasure M ({x \ space M. 1 \ ennreal(1/e) * \q(X x)\} \ space M)" + have "emeasure M {x \ space M. \X x\ < d} \ emeasure M ({x \ space M. 1 \ ennreal(1/e) * \q(X x)\})" by (rule emeasure_mono, auto simp add: * \e>0\ less_imp_le ennreal_mult''[symmetric]) also have "... \ (1/e) * (\\<^sup>+x. ennreal(\q(X x)\) * indicator (space M) x \M)" by (rule nn_integral_Markov_inequality, auto) @@ -1304,7 +1304,7 @@ have "{x \ space M. \X x\ \ d} = {x \ space M. 1 \ ennreal(1/d) * \X x\} \ space M" by (auto simp add: \d>0\ ennreal_mult''[symmetric]) - then have "emeasure M {x \ space M. \X x\ \ d} = emeasure M ({x \ space M. 1 \ ennreal(1/d) * \X x\} \ space M)" + then have "emeasure M {x \ space M. \X x\ \ d} = emeasure M ({x \ space M. 1 \ ennreal(1/d) * \X x\})" by auto also have "... \ (1/d) * (\\<^sup>+x. ennreal(\X x\) * indicator (space M) x \M)" by (rule nn_integral_Markov_inequality, auto) diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Giry_Monad.thy --- a/src/HOL/Probability/Giry_Monad.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Probability/Giry_Monad.thy Tue Feb 23 10:13:09 2021 +0100 @@ -2,15 +2,17 @@ Author: Johannes Hölzl, TU München Author: Manuel Eberl, TU München -Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability +Defines subprobability spaces, the subprobability functor and the Giry monad on subprobability spaces. *) +section \The Giry monad\ + theory Giry_Monad imports Probability_Measure "HOL-Library.Monad_Syntax" begin -section \Sub-probability spaces\ +subsection \Sub-probability spaces\ locale subprob_space = finite_measure + assumes emeasure_space_le_1: "emeasure M (space M) \ 1" @@ -521,7 +523,7 @@ qed qed -section \Properties of return\ +subsection \Properties of ``return''\ definition return :: "'a measure \ 'a \ 'a measure" where "return R x = measure_of (space R) (sets R) (\A. indicator A x)" @@ -757,7 +759,7 @@ "sets M = sets (subprob_algebra N) \ space (select_sets M) = space N" by (intro sets_eq_imp_space_eq sets_select_sets) -section \Join\ +subsection \Join\ definition join :: "'a measure measure \ 'a measure" where "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\B. \\<^sup>+ M'. emeasure M' B \M)" @@ -1784,4 +1786,28 @@ by (subst bind_distr[OF _ measurable_compose[OF _ return_measurable]]) (auto intro!: bind_return_distr') +lemma (in prob_space) AE_eq_constD: + assumes "AE x in M. x = y" + shows "M = return M y" "y \ space M" +proof - + have "AE x in M. x \ space M" + by auto + with assms have "AE x in M. y \ space M" + by eventually_elim auto + thus "y \ space M" + by simp + + show "M = return M y" + proof (rule measure_eqI) + fix X assume X: "X \ sets M" + have "AE x in M. (x \ X) = (x \ (if y \ X then space M else {}))" + using assms by eventually_elim (use X \y \ space M\ in auto) + hence "emeasure M X = emeasure M (if y \ X then space M else {})" + using X by (intro emeasure_eq_AE) auto + also have "\ = emeasure (return M y) X" + using X by (auto simp: emeasure_space_1) + finally show "emeasure M X = \" . + qed auto +qed + end diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Hoeffding.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Hoeffding.thy Tue Feb 23 10:13:09 2021 +0100 @@ -0,0 +1,923 @@ +(* + File: Hoeffding.thy + Author: Manuel Eberl, TU München +*) +section \Hoeffding's Lemma and Hoeffding's Inequality\ +theory Hoeffding + imports Product_PMF Independent_Family +begin + +text \ + Hoeffding's inequality shows that a sum of bounded independent random variables is concentrated + around its mean, with an exponential decay of the tail probabilities. +\ + +subsection \Hoeffding's Lemma\ + +lemma convex_on_exp: + fixes l :: real + assumes "l \ 0" + shows "convex_on UNIV (\x. exp(l*x))" + using assms + by (intro convex_on_realI[where f' = "\x. l * exp (l * x)"]) + (auto intro!: derivative_eq_intros mult_left_mono) + +lemma mult_const_minus_self_real_le: + fixes x :: real + shows "x * (c - x) \ c\<^sup>2 / 4" +proof - + have "x * (c - x) = -(x - c / 2)\<^sup>2 + c\<^sup>2 / 4" + by (simp add: field_simps power2_eq_square) + also have "\ \ 0 + c\<^sup>2 / 4" + by (intro add_mono) auto + finally show ?thesis by simp +qed + +lemma Hoeffdings_lemma_aux: + fixes h p :: real + assumes "h \ 0" and "p \ 0" + defines "L \ (\h. -h * p + ln (1 + p * (exp h - 1)))" + shows "L h \ h\<^sup>2 / 8" +proof (cases "h = 0") + case False + hence h: "h > 0" + using \h \ 0\ by simp + define L' where "L' = (\h. -p + p * exp h / (1 + p * (exp h - 1)))" + define L'' where "L'' = (\h. -(p\<^sup>2) * exp h * exp h / (1 + p * (exp h - 1))\<^sup>2 + + p * exp h / (1 + p * (exp h - 1)))" + define Ls where "Ls = (\n. [L, L', L''] ! n)" + + have [simp]: "L 0 = 0" "L' 0 = 0" + by (auto simp: L_def L'_def) + + have L': "(L has_real_derivative L' x) (at x)" if "x \ {0..h}" for x + proof - + have "1 + p * (exp x - 1) > 0" + using \p \ 0\ that by (intro add_pos_nonneg mult_nonneg_nonneg) auto + thus ?thesis + unfolding L_def L'_def by (auto intro!: derivative_eq_intros) + qed + + have L'': "(L' has_real_derivative L'' x) (at x)" if "x \ {0..h}" for x + proof - + have *: "1 + p * (exp x - 1) > 0" + using \p \ 0\ that by (intro add_pos_nonneg mult_nonneg_nonneg) auto + show ?thesis + unfolding L'_def L''_def + by (insert *, (rule derivative_eq_intros refl | simp)+) (auto simp: divide_simps; algebra) + qed + + have diff: "\m t. m < 2 \ 0 \ t \ t \ h \ (Ls m has_real_derivative Ls (Suc m) t) (at t)" + using L' L'' by (auto simp: Ls_def nth_Cons split: nat.splits) + from Taylor[of 2 Ls L 0 h 0 h, OF _ _ diff] + obtain t where t: "t \ {0<..2 / 2" + using \h > 0\ by (auto simp: Ls_def lessThan_nat_numeral) + define u where "u = p * exp t / (1 + p * (exp t - 1))" + + have "L'' t = u * (1 - u)" + by (simp add: L''_def u_def divide_simps; algebra) + also have "\ \ 1 / 4" + using mult_const_minus_self_real_le[of u 1] by simp + finally have "L'' t \ 1 / 4" . + + note t(2) + also have "L'' t * h\<^sup>2 / 2 \ (1 / 4) * h\<^sup>2 / 2" + using \L'' t \ 1 / 4\ by (intro mult_right_mono divide_right_mono) auto + finally show "L h \ h\<^sup>2 / 8" by simp +qed (auto simp: L_def) + + +locale interval_bounded_random_variable = prob_space + + fixes f :: "'a \ real" and a b :: real + assumes random_variable [measurable]: "random_variable borel f" + assumes AE_in_interval: "AE x in M. f x \ {a..b}" +begin + +lemma integrable [intro]: "integrable M f" +proof (rule integrable_const_bound) + show "AE x in M. norm (f x) \ max \a\ \b\" + by (intro eventually_mono[OF AE_in_interval]) auto +qed (fact random_variable) + +text \ + We first show Hoeffding's lemma for distributions whose expectation is 0. The general + case will easily follow from this later. +\ +lemma Hoeffdings_lemma_nn_integral_0: + assumes "l > 0" and E0: "expectation f = 0" + shows "nn_integral M (\x. exp (l * f x)) \ ennreal (exp (l\<^sup>2 * (b - a)\<^sup>2 / 8))" +proof (cases "AE x in M. f x = 0") + case True + hence "nn_integral M (\x. exp (l * f x)) = nn_integral M (\x. ennreal 1)" + by (intro nn_integral_cong_AE) auto + also have "\ = ennreal (expectation (\_. 1))" + by (intro nn_integral_eq_integral) auto + finally show ?thesis by (simp add: prob_space) +next + case False + have "a < 0" + proof (rule ccontr) + assume a: "\(a < 0)" + have "AE x in M. f x = 0" + proof (subst integral_nonneg_eq_0_iff_AE [symmetric]) + show "AE x in M. f x \ 0" + using AE_in_interval by eventually_elim (use a in auto) + qed (use E0 in \auto simp: id_def integrable\) + with False show False by contradiction + qed + + have "b > 0" + proof (rule ccontr) + assume b: "\(b > 0)" + have "AE x in M. -f x = 0" + proof (subst integral_nonneg_eq_0_iff_AE [symmetric]) + show "AE x in M. -f x \ 0" + using AE_in_interval by eventually_elim (use b in auto) + qed (use E0 in \auto simp: id_def integrable\) + with False show False by simp + qed + + have "a < b" + using \a < 0\ \b > 0\ by linarith + + define p where "p = -a / (b - a)" + define L where "L = (\t. -t* p + ln (1 - p + p * exp t))" + define z where "z = l * (b - a)" + have "z > 0" + unfolding z_def using \a < b\ \l > 0\ by auto + have "p > 0" + using \a < 0\ \a < b\ unfolding p_def by (intro divide_pos_pos) auto + + have "(\\<^sup>+x. exp (l * f x) \M) \ + (\\<^sup>+x. (b - f x) / (b - a) * exp (l * a) + (f x - a) / (b - a) * exp (l * b) \M)" + proof (intro nn_integral_mono_AE eventually_mono[OF AE_in_interval] ennreal_leI) + fix x assume x: "f x \ {a..b}" + define y where "y = (b - f x) / (b-a)" + have y: "y \ {0..1}" + using x \a < b\ by (auto simp: y_def) + have conv: "convex_on UNIV (\x. exp(l*x))" + using \l > 0\ by (intro convex_on_exp) auto + have "exp (l * ((1 - y) *\<^sub>R b + y *\<^sub>R a)) \ (1 - y) * exp (l * b) + y * exp (l * a)" + using y \l > 0\ by (intro convex_onD[OF convex_on_exp]) auto + also have "(1 - y) *\<^sub>R b + y *\<^sub>R a = f x" + using \a < b\ by (simp add: y_def divide_simps) (simp add: algebra_simps)? + also have "1 - y = (f x - a) / (b - a)" + using \a < b\ by (simp add: field_simps y_def) + finally show "exp (l * f x) \ (b - f x) / (b - a) * exp (l*a) + (f x - a)/(b-a) * exp (l*b)" + by (simp add: y_def) + qed + also have "\ = (\\<^sup>+x. ennreal (b - f x) * exp (l * a) / (b - a) + + ennreal (f x - a) * exp (l * b) / (b - a) \M)" + using \a < 0\ \b > 0\ + by (intro nn_integral_cong_AE eventually_mono[OF AE_in_interval]) + (simp add: ennreal_plus ennreal_mult flip: divide_ennreal) + also have "\ = ((\\<^sup>+ x. ennreal (b - f x) \M) * ennreal (exp (l * a)) + + (\\<^sup>+ x. ennreal (f x - a) \M) * ennreal (exp (l * b))) / ennreal (b - a)" + by (simp add: nn_integral_add nn_integral_divide nn_integral_multc add_divide_distrib_ennreal) + also have "(\\<^sup>+ x. ennreal (b - f x) \M) = ennreal (expectation (\x. b - f x))" + by (intro nn_integral_eq_integral Bochner_Integration.integrable_diff + eventually_mono[OF AE_in_interval] integrable_const integrable) auto + also have "expectation (\x. b - f x) = b" + using assms by (subst Bochner_Integration.integral_diff) (auto simp: prob_space) + also have "(\\<^sup>+ x. ennreal (f x - a) \M) = ennreal (expectation (\x. f x - a))" + by (intro nn_integral_eq_integral Bochner_Integration.integrable_diff + eventually_mono[OF AE_in_interval] integrable_const integrable) auto + also have "expectation (\x. f x - a) = (-a)" + using assms by (subst Bochner_Integration.integral_diff) (auto simp: prob_space) + also have "(ennreal b * (exp (l * a)) + ennreal (-a) * (exp (l * b))) / (b - a) = + ennreal (b * exp (l * a) - a * exp (l * b)) / ennreal (b - a)" + using \a < 0\ \b > 0\ + by (simp flip: ennreal_mult ennreal_plus add: mult_nonpos_nonneg divide_ennreal mult_mono) + also have "b * exp (l * a) - a * exp (l * b) = exp (L z) * (b - a)" + proof - + have pos: "1 - p + p * exp z > 0" + proof - + have "exp z > 1" using \l > 0\ and \a < b\ + by (subst one_less_exp_iff) (auto simp: z_def intro!: mult_pos_pos) + hence "(exp z - 1) * p \ 0" + unfolding p_def using \a < 0\ and \a < b\ + by (intro mult_nonneg_nonneg divide_nonneg_pos) auto + thus ?thesis + by (simp add: algebra_simps) + qed + + have "exp (L z) * (b - a) = exp (-z * p) * (1 - p + p * exp z) * (b - a)" + using pos by (simp add: exp_add L_def exp_diff exp_minus divide_simps) + also have "\ = b * exp (l * a) - a * exp (l * b)" using \a < b\ + by (simp add: p_def z_def divide_simps) (simp add: exp_diff algebra_simps)? + finally show ?thesis by simp + qed + also have "ennreal (exp (L z) * (b - a)) / ennreal (b - a) = ennreal (exp (L z))" + using \a < b\ by (simp add: divide_ennreal) + also have "L z = -z * p + ln (1 + p * (exp z - 1))" + by (simp add: L_def algebra_simps) + also have "\ \ z\<^sup>2 / 8" + unfolding L_def by (rule Hoeffdings_lemma_aux[where p = p]) (use \z > 0\ \p > 0\ in simp_all) + hence "ennreal (exp (-z * p + ln (1 + p * (exp z - 1)))) \ ennreal (exp (z\<^sup>2 / 8))" + by (intro ennreal_leI) auto + finally show ?thesis + by (simp add: z_def power_mult_distrib) +qed + +context +begin + +interpretation shift: interval_bounded_random_variable M "\x. f x - \" "a - \" "b - \" + rewrites "b - \ - (a - \) \ b - a" + by unfold_locales (auto intro!: eventually_mono[OF AE_in_interval]) + +lemma expectation_shift: "expectation (\x. f x - expectation f) = 0" + by (subst Bochner_Integration.integral_diff) (auto simp: integrable prob_space) + +lemmas Hoeffdings_lemma_nn_integral = shift.Hoeffdings_lemma_nn_integral_0[OF _ expectation_shift] + +end + +end + + + +subsection \Hoeffding's Inequality\ + +text \ + Consider \n\ independent real random variables $X_1, \ldots, X_n$ that each almost surely lie + in a compact interval $[a_i, b_i]$. Hoeffding's inequality states that the distribution of the + sum of the $X_i$ is tightly concentrated around the sum of the expected values: the probability + of it being above or below the sum of the expected values by more than some \\\ decreases + exponentially with \\\. +\ + +locale indep_interval_bounded_random_variables = prob_space + + fixes I :: "'b set" and X :: "'b \ 'a \ real" + fixes a b :: "'b \ real" + assumes fin: "finite I" + assumes indep: "indep_vars (\_. borel) X I" + assumes AE_in_interval: "\i. i \ I \ AE x in M. X i x \ {a i..b i}" +begin + +lemma random_variable [measurable]: + assumes i: "i \ I" + shows "random_variable borel (X i)" + using i indep unfolding indep_vars_def by blast + +lemma bounded_random_variable [intro]: + assumes i: "i \ I" + shows "interval_bounded_random_variable M (X i) (a i) (b i)" + by unfold_locales (use AE_in_interval[OF i] i in auto) + +end + + +locale Hoeffding_ineq = indep_interval_bounded_random_variables + + fixes \ :: real + defines "\ \ (\i\I. expectation (X i))" +begin + +theorem%important Hoeffding_ineq_ge: + assumes "\ \ 0" + assumes "(\i\I. (b i - a i)\<^sup>2) > 0" + shows "prob {x\space M. (\i\I. X i x) \ \ + \} \ exp (-2 * \\<^sup>2 / (\i\I. (b i - a i)\<^sup>2))" +proof (cases "\ = 0") + case [simp]: True + have "prob {x\space M. (\i\I. X i x) \ \ + \} \ 1" + by simp + thus ?thesis by simp +next + case False + with \\ \ 0\ have \: "\ > 0" + by auto + + define d where "d = (\i\I. (b i - a i)\<^sup>2)" + define l :: real where "l = 4 * \ / d" + have d: "d > 0" + using assms by (simp add: d_def) + have l: "l > 0" + using \ d by (simp add: l_def) + define \' where "\' = (\i. expectation (X i))" + + have "{x\space M. (\i\I. X i x) \ \ + \} = {x\space M. (\i\I. X i x) - \ \ \}" + by (simp add: algebra_simps) + hence "ennreal (prob {x\space M. (\i\I. X i x) \ \ + \}) = emeasure M \" + by (simp add: emeasure_eq_measure) + also have "\ \ ennreal (exp (-l*\)) * (\\<^sup>+x\space M. exp (l * ((\i\I. X i x) - \)) \M)" + by (intro Chernoff_ineq_nn_integral_ge l) auto + also have "(\x. (\i\I. X i x) - \) = (\x. (\i\I. X i x - \' i))" + by (simp add: \_def sum_subtractf \'_def) + also have "(\\<^sup>+x\space M. exp (l * ((\i\I. X i x - \' i))) \M) = + (\\<^sup>+x. (\i\I. ennreal (exp (l * (X i x - \' i)))) \M)" + by (intro nn_integral_cong) + (simp_all add: sum_distrib_left ring_distribs exp_diff exp_sum fin prod_ennreal) + also have "\ = (\i\I. \\<^sup>+x. ennreal (exp (l * (X i x - \' i))) \M)" + by (intro indep_vars_nn_integral fin indep_vars_compose2[OF indep]) auto + also have "ennreal (exp (-l * \)) * \ \ + ennreal (exp (-l * \)) * (\i\I. ennreal (exp (l\<^sup>2 * (b i - a i)\<^sup>2 / 8)))" + proof (intro mult_left_mono prod_mono_ennreal) + fix i assume i: "i \ I" + from i interpret interval_bounded_random_variable M "X i" "a i" "b i" .. + show "(\\<^sup>+x. ennreal (exp (l * (X i x - \' i))) \M) \ ennreal (exp (l\<^sup>2 * (b i - a i)\<^sup>2 / 8))" + unfolding \'_def by (rule Hoeffdings_lemma_nn_integral) fact+ + qed auto + also have "\ = ennreal (exp (-l*\) * (\i\I. exp (l\<^sup>2 * (b i - a i)\<^sup>2 / 8)))" + by (simp add: prod_ennreal prod_nonneg flip: ennreal_mult) + also have "exp (-l*\) * (\i\I. exp (l\<^sup>2 * (b i - a i)\<^sup>2 / 8)) = exp (d * l\<^sup>2 / 8 - l * \)" + by (simp add: exp_diff exp_minus sum_divide_distrib sum_distrib_left + sum_distrib_right exp_sum fin divide_simps mult_ac d_def) + also have "d * l\<^sup>2 / 8 - l * \ = -2 * \\<^sup>2 / d" + using d by (simp add: l_def field_simps power2_eq_square) + finally show ?thesis + by (subst (asm) ennreal_le_iff) (simp_all add: d_def) +qed + +corollary Hoeffding_ineq_le: + assumes \: "\ \ 0" + assumes "(\i\I. (b i - a i)\<^sup>2) > 0" + shows "prob {x\space M. (\i\I. X i x) \ \ - \} \ exp (-2 * \\<^sup>2 / (\i\I. (b i - a i)\<^sup>2))" +proof - + interpret flip: Hoeffding_ineq M I "\i x. -X i x" "\i. -b i" "\i. -a i" "-\" + proof unfold_locales + fix i assume "i \ I" + then interpret interval_bounded_random_variable M "X i" "a i" "b i" .. + show "AE x in M. - X i x \ {- b i..- a i}" + by (intro eventually_mono[OF AE_in_interval]) auto + qed (auto simp: fin \_def sum_negf intro: indep_vars_compose2[OF indep]) + + have "prob {x\space M. (\i\I. X i x) \ \ - \} = prob {x\space M. (\i\I. -X i x) \ -\ + \}" + by (simp add: sum_negf algebra_simps) + also have "\ \ exp (- 2 * \\<^sup>2 / (\i\I. (b i - a i)\<^sup>2))" + using flip.Hoeffding_ineq_ge[OF \] assms(2) by simp + finally show ?thesis . +qed + +corollary Hoeffding_ineq_abs_ge: + assumes \: "\ \ 0" + assumes "(\i\I. (b i - a i)\<^sup>2) > 0" + shows "prob {x\space M. \(\i\I. X i x) - \\ \ \} \ 2 * exp (-2 * \\<^sup>2 / (\i\I. (b i - a i)\<^sup>2))" +proof - + have "{x\space M. \(\i\I. X i x) - \\ \ \} = + {x\space M. (\i\I. X i x) \ \ + \} \ {x\space M. (\i\I. X i x) \ \ - \}" + by auto + also have "prob \ \ prob {x\space M. (\i\I. X i x) \ \ + \} + + prob {x\space M. (\i\I. X i x) \ \ - \}" + by (intro measure_Un_le) auto + also have "\ \ exp (-2 * \\<^sup>2 / (\i\I. (b i - a i)\<^sup>2)) + exp (-2 * \\<^sup>2 / (\i\I. (b i - a i)\<^sup>2))" + by (intro add_mono Hoeffding_ineq_ge Hoeffding_ineq_le assms) + finally show ?thesis by simp +qed + +end + + +subsection \Hoeffding's inequality for i.i.d. bounded random variables\ + +text \ + If we have \n\ even identically-distributed random variables, the statement of Hoeffding's + lemma simplifies a bit more: it shows that the probability that the average of the $X_i$ + is more than \\\ above the expected value is no greater than $e^{\frac{-2ny^2}{(b-a)^2}}$. + + This essentially gives us a more concrete version of the weak law of large numbers: the law + states that the probability vanishes for \n \ \\ for any \\ > 0\. Unlike Hoeffding's inequality, + it does not assume the variables to have bounded support, but it does not provide concrete bounds. +\ + +locale iid_interval_bounded_random_variables = prob_space + + fixes I :: "'b set" and X :: "'b \ 'a \ real" and Y :: "'a \ real" + fixes a b :: real + assumes fin: "finite I" + assumes indep: "indep_vars (\_. borel) X I" + assumes distr_X: "i \ I \ distr M borel (X i) = distr M borel Y" + assumes rv_Y [measurable]: "random_variable borel Y" + assumes AE_in_interval: "AE x in M. Y x \ {a..b}" +begin + +lemma random_variable [measurable]: + assumes i: "i \ I" + shows "random_variable borel (X i)" + using i indep unfolding indep_vars_def by blast + +sublocale X: indep_interval_bounded_random_variables M I X "\_. a" "\_. b" +proof + fix i assume i: "i \ I" + have "AE x in M. Y x \ {a..b}" + by (fact AE_in_interval) + also have "?this \ (AE x in distr M borel Y. x \ {a..b})" + by (subst AE_distr_iff) auto + also have "distr M borel Y = distr M borel (X i)" + using i by (simp add: distr_X) + also have "(AE x in \. x \ {a..b}) \ (AE x in M. X i x \ {a..b})" + using i by (subst AE_distr_iff) auto + finally show "AE x in M. X i x \ {a..b}" . +qed (simp_all add: fin indep) + +lemma expectation_X [simp]: + assumes i: "i \ I" + shows "expectation (X i) = expectation Y" +proof - + have "expectation (X i) = lebesgue_integral (distr M borel (X i)) (\x. x)" + using i by (intro integral_distr [symmetric]) auto + also have "distr M borel (X i) = distr M borel Y" + using i by (rule distr_X) + also have "lebesgue_integral \ (\x. x) = expectation Y" + by (rule integral_distr) auto + finally show "expectation (X i) = expectation Y" . +qed + +end + + +locale Hoeffding_ineq_iid = iid_interval_bounded_random_variables + + fixes \ :: real + defines "\ \ expectation Y" +begin + +sublocale X: Hoeffding_ineq M I X "\_. a" "\_. b" "real (card I) * \" + by unfold_locales (simp_all add: \_def) + +corollary + assumes \: "\ \ 0" + assumes "a < b" "I \ {}" + defines "n \ card I" + shows Hoeffding_ineq_ge: + "prob {x\space M. (\i\I. X i x) \ n * \ + \} \ + exp (-2 * \\<^sup>2 / (n * (b - a)\<^sup>2))" (is ?le) + and Hoeffding_ineq_le: + "prob {x\space M. (\i\I. X i x) \ n * \ - \} \ + exp (-2 * \\<^sup>2 / (n * (b - a)\<^sup>2))" (is ?ge) + and Hoeffding_ineq_abs_ge: + "prob {x\space M. \(\i\I. X i x) - n * \\ \ \} \ + 2 * exp (-2 * \\<^sup>2 / (n * (b - a)\<^sup>2))" (is ?abs_ge) +proof - + have pos: "(\i\I. (b - a)\<^sup>2) > 0" + using \a < b\ \I \ {}\ fin by (intro sum_pos) auto + show ?le + using X.Hoeffding_ineq_ge[OF \ pos] by (simp add: n_def) + show ?ge + using X.Hoeffding_ineq_le[OF \ pos] by (simp add: n_def) + show ?abs_ge + using X.Hoeffding_ineq_abs_ge[OF \ pos] by (simp add: n_def) +qed + +lemma + assumes \: "\ \ 0" + assumes "a < b" "I \ {}" + defines "n \ card I" + shows Hoeffding_ineq_ge': + "prob {x\space M. (\i\I. X i x) / n \ \ + \} \ + exp (-2 * n * \\<^sup>2 / (b - a)\<^sup>2)" (is ?ge) + and Hoeffding_ineq_le': + "prob {x\space M. (\i\I. X i x) / n \ \ - \} \ + exp (-2 * n * \\<^sup>2 / (b - a)\<^sup>2)" (is ?le) + and Hoeffding_ineq_abs_ge': + "prob {x\space M. \(\i\I. X i x) / n - \\ \ \} \ + 2 * exp (-2 * n * \\<^sup>2 / (b - a)\<^sup>2)" (is ?abs_ge) +proof - + have "n > 0" + using assms fin by (auto simp: field_simps) + have \': "\ * n \ 0" + using \n > 0\ \\ \ 0\ by auto + have eq: "- (2 * (\ * real n)\<^sup>2 / (real (card I) * (b - a)\<^sup>2)) = + - (2 * real n * \\<^sup>2 / (b - a)\<^sup>2)" + using \n > 0\ by (simp add: power2_eq_square divide_simps n_def) + + have "{x\space M. (\i\I. X i x) / n \ \ + \} = + {x\space M. (\i\I. X i x) \ \ * n + \ * n}" + using \n > 0\ by (intro Collect_cong conj_cong refl) (auto simp: field_simps) + with Hoeffding_ineq_ge[OF \' \a < b\ \I \ {}\] \n > 0\ eq show ?ge + by (simp add: n_def mult_ac) + + have "{x\space M. (\i\I. X i x) / n \ \ - \} = + {x\space M. (\i\I. X i x) \ \ * n - \ * n}" + using \n > 0\ by (intro Collect_cong conj_cong refl) (auto simp: field_simps) + with Hoeffding_ineq_le[OF \' \a < b\ \I \ {}\] \n > 0\ eq show ?le + by (simp add: n_def mult_ac) + + have "{x\space M. \(\i\I. X i x) / n - \\ \ \} = + {x\space M. \(\i\I. X i x) - \ * n\ \ \ * n}" + using \n > 0\ by (intro Collect_cong conj_cong refl) (auto simp: field_simps) + with Hoeffding_ineq_abs_ge[OF \' \a < b\ \I \ {}\] \n > 0\ eq show ?abs_ge + by (simp add: n_def mult_ac) +qed + +end + + +subsection \Hoeffding's Inequality for the Binomial distribution\ + +text \ + We can now apply Hoeffding's inequality to the Binomial distribution, which can be seen + as the sum of \n\ i.i.d. coin flips (the support of each of which is contained in $[0,1]$). +\ + +locale binomial_distribution = + fixes n :: nat and p :: real + assumes p: "p \ {0..1}" +begin + +context + fixes coins :: "(nat \ bool) pmf" and \ + assumes n: "n > 0" + defines "coins \ Pi_pmf {.._. bernoulli_pmf p)" +begin + +lemma coins_component: + assumes i: "i < n" + shows "distr (measure_pmf coins) borel (\f. if f i then 1 else 0) = + distr (measure_pmf (bernoulli_pmf p)) borel (\b. if b then 1 else 0)" +proof - + have "distr (measure_pmf coins) borel (\f. if f i then 1 else 0) = + distr (measure_pmf (map_pmf (\f. f i) coins)) borel (\b. if b then 1 else 0)" + unfolding map_pmf_rep_eq by (subst distr_distr) (auto simp: o_def) + also have "map_pmf (\f. f i) coins = bernoulli_pmf p" + unfolding coins_def using i by (subst Pi_pmf_component) auto + finally show ?thesis + unfolding map_pmf_rep_eq . +qed + +lemma prob_binomial_pmf_conv_coins: + "measure_pmf.prob (binomial_pmf n p) {x. P (real x)} = + measure_pmf.prob coins {x. P (\ii{..ii\{i\{..v. card {i\{..i f. if f i then 1 else 0" "\f. if f 0 then 1 else 0" 0 1 p +proof unfold_locales + show "prob_space.indep_vars (measure_pmf coins) (\_. borel) (\i f. if f i then 1 else 0) {..f. if f 0 then 1 else 0 :: real) = + measure_pmf.expectation (map_pmf (\f. f 0) coins) (\b. if b then 1 else 0 :: real)" + by (simp add: coins_def) + also have "map_pmf (\f. f 0) coins = bernoulli_pmf p" + using n by (simp add: coins_def Pi_pmf_component) + also have "measure_pmf.expectation \ (\b. if b then 1 else 0) = p" + using p by simp + finally show "p \ measure_pmf.expectation coins (\f. if f 0 then 1 else 0)" by simp +qed (auto simp: coins_component) + +corollary + fixes \ :: real + assumes \: "\ \ 0" + shows prob_ge: "measure_pmf.prob (binomial_pmf n p) {x. x \ n * p + \} \ exp (-2 * \\<^sup>2 / n)" + and prob_le: "measure_pmf.prob (binomial_pmf n p) {x. x \ n * p - \} \ exp (-2 * \\<^sup>2 / n)" + and prob_abs_ge: + "measure_pmf.prob (binomial_pmf n p) {x. \x - n * p\ \ \} \ 2 * exp (-2 * \\<^sup>2 / n)" +proof - + have [simp]: "{.. {}" + using n by auto + show "measure_pmf.prob (binomial_pmf n p) {x. x \ n * p + \} \ exp (-2 * \\<^sup>2 / n)" + using Hoeffding_ineq_ge[of \] by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all) + show "measure_pmf.prob (binomial_pmf n p) {x. x \ n * p - \} \ exp (-2 * \\<^sup>2 / n)" + using Hoeffding_ineq_le[of \] by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all) + show "measure_pmf.prob (binomial_pmf n p) {x. \x - n * p\ \ \} \ 2 * exp (-2 * \\<^sup>2 / n)" + using Hoeffding_ineq_abs_ge[of \] + by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all) +qed + +corollary + fixes \ :: real + assumes \: "\ \ 0" + shows prob_ge': "measure_pmf.prob (binomial_pmf n p) {x. x / n \ p + \} \ exp (-2 * n * \\<^sup>2)" + and prob_le': "measure_pmf.prob (binomial_pmf n p) {x. x / n \ p - \} \ exp (-2 * n * \\<^sup>2)" + and prob_abs_ge': + "measure_pmf.prob (binomial_pmf n p) {x. \x / n - p\ \ \} \ 2 * exp (-2 * n * \\<^sup>2)" +proof - + have [simp]: "{.. {}" + using n by auto + show "measure_pmf.prob (binomial_pmf n p) {x. x / n \ p + \} \ exp (-2 * n * \\<^sup>2)" + using Hoeffding_ineq_ge'[of \] by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all) + show "measure_pmf.prob (binomial_pmf n p) {x. x / n \ p - \} \ exp (-2 * n * \\<^sup>2)" + using Hoeffding_ineq_le'[of \] by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all) + show "measure_pmf.prob (binomial_pmf n p) {x. \x / n - p\ \ \} \ 2 * exp (-2 * n * \\<^sup>2)" + using Hoeffding_ineq_abs_ge'[of \] + by (subst prob_binomial_pmf_conv_coins) (use assms in simp_all) +qed + +end + +end + + +subsection \Tail bounds for the negative binomial distribution\ + +text \ + Since the tail probabilities of a negative Binomial distribution are equal to the + tail probabilities of some Binomial distribution, we can obtain tail bounds for the + negative Binomial distribution through the Hoeffding tail bounds for the Binomial + distribution. +\ + +context + fixes p q :: real + assumes p: "p \ {0<..<1}" + defines "q \ 1 - p" +begin + +lemma prob_neg_binomial_pmf_ge_bound: + fixes n :: nat and k :: real + defines "\ \ real n * q / p" + assumes k: "k \ 0" + shows "measure_pmf.prob (neg_binomial_pmf n p) {x. real x \ \ + k} + \ exp (- 2 * p ^ 3 * k\<^sup>2 / (n + p * k))" +proof - + consider "n = 0" | "p = 1" | "n > 0" "p \ 1" + by blast + thus ?thesis + proof cases + assume [simp]: "n = 0" + show ?thesis using k + by (simp add: indicator_def \_def) + next + assume [simp]: "p = 1" + show ?thesis using k + by (auto simp add: indicator_def \_def q_def) + next + assume n: "n > 0" and "p \ 1" + from \p \ 1\ and p have p: "p \ {0<..<1}" + by auto + from p have q: "q \ {0<..<1}" + by (auto simp: q_def) + + define k1 where "k1 = \ + k" + have k1: "k1 \ \" + using k by (simp add: k1_def) + have "k1 > 0" + by (rule less_le_trans[OF _ k1]) (use p n in \auto simp: q_def \_def\) + + define k1' where "k1' = nat (ceiling k1)" + have "\ \ 0" using p + by (auto simp: \_def q_def) + have "\(x < k1') \ real x \ k1" for x + unfolding k1'_def by linarith + hence eq: "UNIV - {.. k1}" + by auto + hence "measure_pmf.prob (neg_binomial_pmf n p) {n. n \ k1} = + 1 - measure_pmf.prob (neg_binomial_pmf n p) {.. = measure_pmf.prob (binomial_pmf (n + k1' - 1) q) {n. n \ k1}" + using measure_pmf.prob_compl[of "{.. k1} = {x. x \ real (n + k1' - 1) * q + (k1 - real (n + k1' - 1) * q)}" + by simp + also have "measure_pmf.prob (binomial_pmf (n + k1' - 1) q) \ \ + exp (-2 * (k1 - real (n + k1' - 1) * q)\<^sup>2 / real (n + k1' - 1))" + proof (rule binomial_distribution.prob_ge) + show "binomial_distribution q" + by unfold_locales (use q in auto) + next + show "n + k1' - 1 > 0" + using \k1 > 0\ n unfolding k1'_def by linarith + next + have "real (n + nat \k1\ - 1) \ real n + k1" + using \k1 > 0\ by linarith + hence "real (n + k1' - 1) * q \ (real n + k1) * q" + unfolding k1'_def by (intro mult_right_mono) (use p in \simp_all add: q_def\) + also have "\ \ k1" + using k1 p by (simp add: q_def field_simps \_def) + finally show "0 \ k1 - real (n + k1' - 1) * q" + by simp + qed + also have "{x. real (n + k1' - 1) * q + (k1 - real (n + k1' - 1) * q) \ real x} = {x. real x \ k1}" + by simp + also have "exp (-2 * (k1 - real (n + k1' - 1) * q)\<^sup>2 / real (n + k1' - 1)) \ + exp (-2 * (k1 - (n + k1) * q)\<^sup>2 / (n + k1))" + proof - + have "real (n + k1' - Suc 0) \ real n + k1" + unfolding k1'_def using \k1 > 0\ by linarith + moreover have "(real n + k1) * q \ k1" + using k1 p by (auto simp: q_def field_simps \_def) + moreover have "1 < n + k1'" + using n \k1 > 0\ unfolding k1'_def by linarith + ultimately have "2 * (k1 - real (n + k1' - 1) * q)\<^sup>2 / real (n + k1' - 1) \ + 2 * (k1 - (n + k1) * q)\<^sup>2 / (n + k1)" + by (intro frac_le mult_left_mono power_mono mult_nonneg_nonneg mult_right_mono diff_mono) + (use q in simp_all) + thus ?thesis + by simp + qed + also have "\ = exp (-2 * (p * k1 - q * n)\<^sup>2 / (k1 + n))" + by (simp add: q_def algebra_simps) + also have "-2 * (p * k1 - q * n)\<^sup>2 = -2 * p\<^sup>2 * (k1 - \)\<^sup>2" + using p by (auto simp: field_simps \_def) + also have "k1 - \ = k" + by (simp add: k1_def \_def) + also note k1_def + also have "\ + k + real n = real n / p + k" + using p by (simp add: \_def q_def field_simps) + also have "- 2 * p\<^sup>2 * k\<^sup>2 / (real n / p + k) = - 2 * p ^ 3 * k\<^sup>2 / (p * k + n)" + using p by (simp add: field_simps power3_eq_cube power2_eq_square) + finally show ?thesis by (simp add: add_ac) + qed +qed + +lemma prob_neg_binomial_pmf_le_bound: + fixes n :: nat and k :: real + defines "\ \ real n * q / p" + assumes k: "k \ 0" + shows "measure_pmf.prob (neg_binomial_pmf n p) {x. real x \ \ - k} + \ exp (-2 * p ^ 3 * k\<^sup>2 / (n - p * k))" +proof - + consider "n = 0" | "p = 1" | "k > \" | "n > 0" "p \ 1" "k \ \" + by force + thus ?thesis + proof cases + assume [simp]: "n = 0" + show ?thesis using k + by (simp add: indicator_def \_def) + next + assume [simp]: "p = 1" + show ?thesis using k + by (auto simp add: indicator_def \_def q_def) + next + assume "k > \" + hence "{x. real x \ \ - k} = {}" + by auto + thus ?thesis by simp + next + assume n: "n > 0" and "p \ 1" and "k \ \" + from \p \ 1\ and p have p: "p \ {0<..<1}" + by auto + from p have q: "q \ {0<..<1}" + by (auto simp: q_def) + + define f :: "real \ real" where "f = (\x. (p * x - q * n)\<^sup>2 / (x + n))" + have f_mono: "f x \ f y" if "x \ 0" "y \ n * q / p" "x \ y" for x y :: real + using that(3) + proof (rule DERIV_nonpos_imp_nonincreasing) + fix t assume t: "t \ x" "t \ y" + have "x > -n" + using n \x \ 0\ by linarith + hence "(f has_field_derivative ((p * t - q * n) * (n * (1 + p) + p * t) / (n + t) ^ 2)) (at t)" + unfolding f_def using t + by (auto intro!: derivative_eq_intros simp: algebra_simps q_def power2_eq_square) + moreover { + have "p * t \ p * y" + using p by (intro mult_left_mono t) auto + also have "p * y \ q * n" + using \y \ n * q / p\ p by (simp add: field_simps) + finally have "p * t \ q * n" . + } + hence "(p * t - q * n) * (n * (1 + p) + p * t) / (n + t) ^ 2 \ 0" + using p \x \ 0\ t + by (intro mult_nonpos_nonneg divide_nonpos_nonneg add_nonneg_nonneg mult_nonneg_nonneg) auto + ultimately show "\y. (f has_real_derivative y) (at t) \ y \ 0" + by blast + qed + + define k1 where "k1 = \ - k" + have k1: "k1 \ real n * q / p" + using assms by (simp add: \_def k1_def) + have "k1 \ 0" + using k \k \ \\ by (simp add: \_def k1_def) + + define k1' where "k1' = nat (floor k1)" + have "\ \ 0" using p + by (auto simp: \_def q_def) + have "(x \ k1') \ real x \ k1" for x + unfolding k1'_def not_less using \k1 \ 0\ by linarith + hence eq: "{n. n \ k1} = {..k1'}" + by auto + hence "measure_pmf.prob (neg_binomial_pmf n p) {n. n \ k1} = + measure_pmf.prob (neg_binomial_pmf n p) {..k1'}" + by simp + also have "measure_pmf.prob (neg_binomial_pmf n p) {..k1'} = + measure_pmf.prob (binomial_pmf (n + k1') q) {..k1'}" + unfolding q_def using p by (intro prob_neg_binomial_pmf_atMost) auto + also note eq [symmetric] + also have "{x. real x \ k1} = {x. x \ real (n + k1') * q - (real (n + k1') * q - real k1')}" + using eq by auto + also have "measure_pmf.prob (binomial_pmf (n + k1') q) \ \ + exp (-2 * (real (n + k1') * q - real k1')\<^sup>2 / real (n + k1'))" + proof (rule binomial_distribution.prob_le) + show "binomial_distribution q" + by unfold_locales (use q in auto) + next + show "n + k1' > 0" + using \k1 \ 0\ n unfolding k1'_def by linarith + next + have "p * k1' \ p * k1" + using p \k1 \ 0\ by (intro mult_left_mono) (auto simp: k1'_def) + also have "\ \ q * n" + using k1 p by (simp add: field_simps) + finally show "0 \ real (n + k1') * q - real k1'" + by (simp add: algebra_simps q_def) + qed + also have "{x. real x \ real (n + k1') * q - (real (n + k1') * q - k1')} = {..k1'}" + by auto + also have "real (n + k1') * q - k1' = -(p * k1' - q * n)" + by (simp add: q_def algebra_simps) + also have "\ ^ 2 = (p * k1' - q * n) ^ 2" + by algebra + also have "- 2 * (p * real k1' - q * real n)\<^sup>2 / real (n + k1') = -2 * f (real k1')" + by (simp add: f_def) + also have "f (real k1') \ f k1" + by (rule f_mono) (use \k1 \ 0\ k1 in \auto simp: k1'_def\) + hence "exp (-2 * f (real k1')) \ exp (-2 * f k1)" + by simp + also have "\ = exp (-2 * (p * k1 - q * n)\<^sup>2 / (k1 + n))" + by (simp add: f_def) + + also have "-2 * (p * k1 - q * n)\<^sup>2 = -2 * p\<^sup>2 * (k1 - \)\<^sup>2" + using p by (auto simp: field_simps \_def) + also have "(k1 - \) ^ 2 = k ^ 2" + by (simp add: k1_def \_def) + also note k1_def + also have "\ - k + real n = real n / p - k" + using p by (simp add: \_def q_def field_simps) + also have "- 2 * p\<^sup>2 * k\<^sup>2 / (real n / p - k) = - 2 * p ^ 3 * k\<^sup>2 / (n - p * k)" + using p by (simp add: field_simps power3_eq_cube power2_eq_square) + also have "{..k1'} = {x. real x \ \ - k}" + using eq by (simp add: k1_def) + finally show ?thesis . + qed +qed + +text \ + Due to the function $exp(-l/x)$ being concave for $x \geq \frac{l}{2}$, the above two + bounds can be combined into the following one for moderate values of \k\. + (cf. \<^url>\https://math.stackexchange.com/questions/1565559\) +\ +lemma prob_neg_binomial_pmf_abs_ge_bound: + fixes n :: nat and k :: real + defines "\ \ real n * q / p" + assumes "k \ 0" and n_ge: "n \ p * k * (p\<^sup>2 * k + 1)" + shows "measure_pmf.prob (neg_binomial_pmf n p) {x. \real x - \\ \ k} \ + 2 * exp (-2 * p ^ 3 * k ^ 2 / n)" +proof (cases "k = 0") + case False + with \k \ 0\ have k: "k > 0" + by auto + define l :: real where "l = 2 * p ^ 3 * k ^ 2" + have l: "l > 0" + using p k by (auto simp: l_def) + define f :: "real \ real" where "f = (\x. exp (-l / x))" + define f' where "f' = (\x. -l * exp (-l / x) / x ^ 2)" + + have f'_mono: "f' x \ f' y" if "x \ l / 2" "x \ y" for x y :: real + using that(2) + proof (rule DERIV_nonneg_imp_nondecreasing) + fix t assume t: "x \ t" "t \ y" + have "t > 0" + using that l t by auto + have "(f' has_field_derivative (l * (2 * t - l) / (exp (l / t) * t ^ 4))) (at t)" + unfolding f'_def using t that \t > 0\ + by (auto intro!: derivative_eq_intros simp: field_simps exp_minus simp flip: power_Suc) + moreover have "l * (2 * t - l) / (exp (l / t) * t ^ 4) \ 0" + using that t l by (intro divide_nonneg_pos mult_nonneg_nonneg) auto + ultimately show "\y. (f' has_real_derivative y) (at t) \ 0 \ y" by blast + qed + + have convex: "convex_on {l/2..} (\x. -f x)" unfolding f_def + proof (intro convex_on_realI[where f' = f']) + show "((\x. - exp (- l / x)) has_real_derivative f' x) (at x)" if "x \ {l/2..}" for x + using that l + by (auto intro!: derivative_eq_intros simp: f'_def power2_eq_square algebra_simps) + qed (use l in \auto intro!: f'_mono\) + + have eq: "{x. \real x - \\ \ k} = {x. real x \ \ - k} \ {x. real x \ \ + k}" + by auto + have "measure_pmf.prob (neg_binomial_pmf n p) {x. \real x - \\ \ k} \ + measure_pmf.prob (neg_binomial_pmf n p) {x. real x \ \ - k} + + measure_pmf.prob (neg_binomial_pmf n p) {x. real x \ \ + k}" + by (subst eq, rule measure_Un_le) auto + also have "\ \ exp (-2 * p ^ 3 * k\<^sup>2 / (n - p * k)) + exp (-2 * p ^ 3 * k\<^sup>2 / (n + p * k))" + unfolding \_def + by (intro prob_neg_binomial_pmf_le_bound prob_neg_binomial_pmf_ge_bound add_mono \k \ 0\) + also have "\ = 2 * (1/2 * f (n - p * k) + 1/2 * f (n + p * k))" + by (simp add: f_def l_def) + also have "1/2 * f (n - p * k) + 1/2 * f (n + p * k) \ f (1/2 * (n - p * k) + 1/2 * (n + p * k))" + proof - + let ?x = "n - p * k" and ?y = "n + p * k" + have le1: "l / 2 \ ?x" using n_ge + by (simp add: l_def power2_eq_square power3_eq_cube algebra_simps) + also have "\ \ ?y" + using p k by simp + finally have le2: "l / 2 \ ?y" . + have "-f ((1 - 1 / 2) *\<^sub>R ?x + (1 / 2) *\<^sub>R ?y) \ (1 - 1 / 2) * - f ?x + 1 / 2 * - f ?y" + using le1 le2 by (intro convex_onD[OF convex]) auto + thus ?thesis by simp + qed + also have "1/2 * (n - p * k) + 1/2 * (n + p * k) = n" + by (simp add: algebra_simps) + also have "2 * f n = 2 * exp (-l / n)" + by (simp add: f_def) + finally show ?thesis + by (simp add: l_def) +qed auto + +end + +end diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Independent_Family.thy --- a/src/HOL/Probability/Independent_Family.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Probability/Independent_Family.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1138,6 +1138,33 @@ qed qed +lemma (in prob_space) indep_vars_iff_distr_eq_PiM': + fixes I :: "'i set" and X :: "'i \ 'a \ 'b" + assumes "I \ {}" + 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 - + from assms obtain j where j: "j \ I" + by auto + define N' where "N' = (\i. if i \ I then M' i else M' j)" + define Y where "Y = (\i. if i \ I then X i else X j)" + have rv: "random_variable (N' i) (Y i)" for i + using j by (auto simp: N'_def Y_def intro: assms) + + have "indep_vars M' X I = indep_vars N' Y I" + by (intro indep_vars_cong) (auto simp: N'_def Y_def) + also have "\ \ distr M (\\<^sub>M i\I. N' i) (\x. \i\I. Y i x) = (\\<^sub>M i\I. distr M (N' i) (Y i))" + by (intro indep_vars_iff_distr_eq_PiM rv assms) + also have "(\\<^sub>M i\I. N' i) = (\\<^sub>M i\I. M' i)" + by (intro PiM_cong) (simp_all add: N'_def) + also have "(\x. \i\I. Y i x) = (\x. \i\I. X i x)" + by (simp_all add: Y_def fun_eq_iff) + also have "(\\<^sub>M i\I. distr M (N' i) (Y i)) = (\\<^sub>M i\I. distr M (M' i) (X i))" + by (intro PiM_cong distr_cong) (simp_all add: N'_def Y_def) + finally show ?thesis . +qed + lemma (in prob_space) indep_varD: assumes indep: "indep_var Ma A Mb B" assumes sets: "Xa \ sets Ma" "Xb \ sets Mb" diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Feb 23 10:13:09 2021 +0100 @@ -392,4 +392,51 @@ end +lemma PiM_return: + assumes "finite I" + assumes [measurable]: "\i. i \ I \ {a i} \ sets (M i)" + shows "PiM I (\i. return (M i) (a i)) = return (PiM I M) (restrict a I)" +proof - + have [simp]: "a i \ space (M i)" if "i \ I" for i + using assms(2)[OF that] by (meson insert_subset sets.sets_into_space) + interpret prob_space "PiM I (\i. return (M i) (a i))" + by (intro prob_space_PiM prob_space_return) auto + have "AE x in PiM I (\i. return (M i) (a i)). \i\I. x i = restrict a I i" + by (intro eventually_ball_finite ballI AE_PiM_component prob_space_return assms) + (auto simp: AE_return) + moreover have "AE x in PiM I (\i. return (M i) (a i)). x \ space (PiM I (\i. return (M i) (a i)))" + by simp + ultimately have "AE x in PiM I (\i. return (M i) (a i)). x = restrict a I" + by eventually_elim (auto simp: fun_eq_iff space_PiM) + hence "Pi\<^sub>M I (\i. return (M i) (a i)) = return (Pi\<^sub>M I (\i. return (M i) (a i))) (restrict a I)" + by (rule AE_eq_constD) + also have "\ = return (PiM I M) (restrict a I)" + by (intro return_cong sets_PiM_cong) auto + finally show ?thesis . +qed + +lemma distr_PiM_finite_prob_space': + assumes fin: "finite I" + assumes "\i. i \ I \ prob_space (M i)" + assumes "\i. i \ I \ prob_space (M' i)" + assumes [measurable]: "\i. i \ I \ f \ measurable (M i) (M' i)" + shows "distr (PiM I M) (PiM I M') (compose I f) = PiM I (\i. distr (M i) (M' i) f)" +proof - + define N where "N = (\i. if i \ I then M i else return (count_space UNIV) undefined)" + define N' where "N' = (\i. if i \ I then M' i else return (count_space UNIV) undefined)" + have [simp]: "PiM I N = PiM I M" "PiM I N' = PiM I M'" + by (intro PiM_cong; simp add: N_def N'_def)+ + + have "distr (PiM I N) (PiM I N') (compose I f) = PiM I (\i. distr (N i) (N' i) f)" + proof (rule distr_PiM_finite_prob_space) + show "product_prob_space N" + by (rule product_prob_spaceI) (auto simp: N_def intro!: prob_space_return assms) + show "product_prob_space N'" + by (rule product_prob_spaceI) (auto simp: N'_def intro!: prob_space_return assms) + qed (auto simp: N_def N'_def fin) + also have "Pi\<^sub>M I (\i. distr (N i) (N' i) f) = Pi\<^sub>M I (\i. distr (M i) (M' i) f)" + by (intro PiM_cong) (simp_all add: N_def N'_def) + finally show ?thesis by simp +qed + end diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Probability.thy --- a/src/HOL/Probability/Probability.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Probability/Probability.thy Tue Feb 23 10:13:09 2021 +0100 @@ -10,6 +10,8 @@ Projective_Limit Random_Permutations SPMF + Product_PMF + Hoeffding Stream_Space Tree_Space Conditional_Expectation diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Feb 23 10:13:09 2021 +0100 @@ -1,6 +1,7 @@ (* Title: HOL/Probability/Probability_Mass_Function.thy Author: Johannes Hölzl, TU München Author: Andreas Lochbihler, ETH Zurich + Author: Manuel Eberl, TU München *) section \ Probability mass function \ @@ -529,6 +530,16 @@ shows "integral\<^sup>L (map_pmf g p) f = integral\<^sup>L p (\x. f (g x))" by (simp add: integral_distr map_pmf_rep_eq) +lemma integrable_map_pmf_eq [simp]: + fixes g :: "'a \ 'b::{banach, second_countable_topology}" + shows "integrable (map_pmf f p) g \ integrable (measure_pmf p) (\x. g (f x))" + by (subst map_pmf_rep_eq, subst integrable_distr_eq) auto + +lemma integrable_map_pmf [intro]: + fixes g :: "'a \ 'b::{banach, second_countable_topology}" + shows "integrable (measure_pmf p) (\x. g (f x)) \ integrable (map_pmf f p) g" + by (subst integrable_map_pmf_eq) + lemma pmf_abs_summable [intro]: "pmf p abs_summable_on A" by (rule abs_summable_on_subset[OF _ subset_UNIV]) (auto simp: abs_summable_on_def integrable_iff_bounded nn_integral_pmf) @@ -669,6 +680,9 @@ by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD intro!: measure_pmf.finite_measure_eq_AE) +lemma pair_return_pmf [simp]: "pair_pmf (return_pmf x) (return_pmf y) = return_pmf (x, y)" + by (auto simp: pair_pmf_def bind_return_pmf) + lemma pmf_map_inj': "inj f \ pmf (map_pmf f M) (f x) = pmf M x" apply(cases "x \ set_pmf M") apply(simp add: pmf_map_inj[OF subset_inj_on]) @@ -676,6 +690,28 @@ apply(auto simp add: pmf_eq_0_set_pmf dest: injD) done +lemma expectation_pair_pmf_fst [simp]: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + shows "measure_pmf.expectation (pair_pmf p q) (\x. f (fst x)) = measure_pmf.expectation p f" +proof - + have "measure_pmf.expectation (pair_pmf p q) (\x. f (fst x)) = + measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f" by simp + also have "map_pmf fst (pair_pmf p q) = p" + by (simp add: map_fst_pair_pmf) + finally show ?thesis . +qed + +lemma expectation_pair_pmf_snd [simp]: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + shows "measure_pmf.expectation (pair_pmf p q) (\x. f (snd x)) = measure_pmf.expectation q f" +proof - + have "measure_pmf.expectation (pair_pmf p q) (\x. f (snd x)) = + measure_pmf.expectation (map_pmf snd (pair_pmf p q)) f" by simp + also have "map_pmf snd (pair_pmf p q) = q" + by (simp add: map_snd_pair_pmf) + finally show ?thesis . +qed + lemma pmf_map_outside: "x \ f ` set_pmf M \ pmf (map_pmf f M) x = 0" unfolding pmf_eq_0_set_pmf by simp @@ -1711,9 +1747,108 @@ end +lemma geometric_pmf_1 [simp]: "geometric_pmf 1 = return_pmf 0" + by (intro pmf_eqI) (auto simp: indicator_def) + lemma set_pmf_geometric: "0 < p \ p < 1 \ set_pmf (geometric_pmf p) = UNIV" by (auto simp: set_pmf_iff) +lemma geometric_sums_times_n: + fixes c::"'a::{banach,real_normed_field}" + assumes "norm c < 1" + shows "(\n. c^n * of_nat n) sums (c / (1 - c)\<^sup>2)" +proof - + have "(\n. c * z ^ n) sums (c / (1 - z))" if "norm z < 1" for z + using geometric_sums sums_mult that by fastforce + moreover have "((\z. c / (1 - z)) has_field_derivative (c / (1 - c)\<^sup>2)) (at c)" + using assms by (auto intro!: derivative_eq_intros simp add: semiring_normalization_rules) + ultimately have "(\n. diffs (\n. c) n * c ^ n) sums (c / (1 - c)\<^sup>2)" + using assms by (intro termdiffs_sums_strong) + then have "(\n. of_nat (Suc n) * c ^ (Suc n)) sums (c / (1 - c)\<^sup>2)" + unfolding diffs_def by (simp add: power_eq_if mult.assoc) + then show ?thesis + by (subst (asm) sums_Suc_iff) (auto simp add: mult.commute) +qed + +lemma geometric_sums_times_norm: + fixes c::"'a::{banach,real_normed_field}" + assumes "norm c < 1" + shows "(\n. norm (c^n * of_nat n)) sums (norm c / (1 - norm c)\<^sup>2)" +proof - + have "norm (c^n * of_nat n) = (norm c) ^ n * of_nat n" for n::nat + by (simp add: norm_power norm_mult) + then show ?thesis + using geometric_sums_times_n[of "norm c"] assms + by force +qed + +lemma integrable_real_geometric_pmf: + assumes "p \ {0<..1}" + shows "integrable (geometric_pmf p) real" +proof - + have "summable (\x. p * ((1 - p) ^ x * real x))" + using geometric_sums_times_norm[of "1 - p"] assms + by (intro summable_mult) (auto simp: sums_iff) + hence "summable (\x. (1 - p) ^ x * real x)" + by (rule summable_mult_D) (use assms in auto) + thus ?thesis + unfolding measure_pmf_eq_density using assms + by (subst integrable_density) + (auto simp: integrable_count_space_nat_iff mult_ac) +qed + +lemma expectation_geometric_pmf: + assumes "p \ {0<..1}" + shows "measure_pmf.expectation (geometric_pmf p) real = (1 - p) / p" +proof - + have "(\n. p * ((1 - p) ^ n * n)) sums (p * ((1 - p) / p^2))" + using assms geometric_sums_times_n[of "1-p"] by (intro sums_mult) auto + moreover have "(\n. p * ((1 - p) ^ n * n)) = (\n. (1 - p) ^ n * p * real n)" + by auto + ultimately have *: "(\n. (1 - p) ^ n * p * real n) sums ((1 - p) / p)" + using assms sums_subst by (auto simp add: power2_eq_square) + have "measure_pmf.expectation (geometric_pmf p) real = + (\n. pmf (geometric_pmf p) n * real n \count_space UNIV)" + unfolding measure_pmf_eq_density by (subst integral_density) auto + also have "integrable (count_space UNIV) (\n. pmf (geometric_pmf p) n * real n)" + using * assms unfolding integrable_count_space_nat_iff by (simp add: sums_iff) + hence "(\n. pmf (geometric_pmf p) n * real n \count_space UNIV) = (1 - p) / p" + using * assms by (subst integral_count_space_nat) (simp_all add: sums_iff) + finally show ?thesis by auto +qed + +lemma geometric_bind_pmf_unfold: + assumes "p \ {0<..1}" + shows "geometric_pmf p = + do {b \ bernoulli_pmf p; + if b then return_pmf 0 else map_pmf Suc (geometric_pmf p)}" +proof - + have *: "(Suc -` {i}) = (if i = 0 then {} else {i - 1})" for i + by force + have "pmf (geometric_pmf p) i = + pmf (bernoulli_pmf p \ + (\b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p))) + i" for i + proof - + have "pmf (geometric_pmf p) i = + (if i = 0 then p else (1 - p) * pmf (geometric_pmf p) (i - 1))" + using assms by (simp add: power_eq_if) + also have "\ = (if i = 0 then p else (1 - p) * pmf (map_pmf Suc (geometric_pmf p)) i)" + by (simp add: pmf_map indicator_def measure_pmf_single *) + also have "\ = measure_pmf.expectation (bernoulli_pmf p) + (\x. pmf (if x then return_pmf 0 else map_pmf Suc (geometric_pmf p)) i)" + using assms by (auto simp add: pmf_map *) + also have "\ = pmf (bernoulli_pmf p \ + (\b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p))) + i" + by (auto simp add: pmf_bind) + finally show ?thesis . + qed + then show ?thesis + using pmf_eqI by blast +qed + + subsubsection \ Uniform Multiset Distribution \ context @@ -1945,6 +2080,23 @@ lemma set_pmf_binomial[simp]: "0 < p \ p < 1 \ set_pmf (binomial_pmf n p) = {..n}" by (simp add: set_pmf_binomial_eq) +lemma finite_set_pmf_binomial_pmf [intro]: "p \ {0..1} \ finite (set_pmf (binomial_pmf n p))" + by (subst set_pmf_binomial_eq) auto + +lemma expectation_binomial_pmf': + fixes f :: "nat \ 'a :: {banach, second_countable_topology}" + assumes p: "p \ {0..1}" + shows "measure_pmf.expectation (binomial_pmf n p) f = + (\k\n. (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) *\<^sub>R f k)" + using p by (subst integral_measure_pmf[where A = "{..n}"]) + (auto simp: set_pmf_binomial_eq split: if_splits) + +lemma integrable_binomial_pmf [simp, intro]: + fixes f :: "nat \ 'a :: {banach, second_countable_topology}" + assumes p: "p \ {0..1}" + shows "integrable (binomial_pmf n p) f" + by (rule integrable_measure_pmf_finite) (use assms in auto) + context includes lifting_syntax begin @@ -2010,6 +2162,222 @@ bind_return_pmf' binomial_pmf_0 intro!: bind_pmf_cong) +subsection \Negative Binomial distribution\ + +text \ + The negative binomial distribution counts the number of times a weighted coin comes up + tails before having come up heads \n\ times. In other words: how many failures do we see before + seeing the \n\-th success? + + An alternative view is that the negative binomial distribution is the sum of \n\ i.i.d. + geometric variables (this is the definition that we use). + + Note that there are sometimes different conventions for this distributions in the literature; + for instance, sometimes the number of \<^emph>\attempts\ is counted instead of the number of failures. + This only shifts the entire distribution by a constant number and is thus not a big difference. + I think that the convention we use is the most natural one since the support of the distribution + starts at 0, whereas for the other convention it starts at \n\. +\ +primrec neg_binomial_pmf :: "nat \ real \ nat pmf" where + "neg_binomial_pmf 0 p = return_pmf 0" +| "neg_binomial_pmf (Suc n) p = + map_pmf (\(x,y). (x + y)) (pair_pmf (geometric_pmf p) (neg_binomial_pmf n p))" + +lemma neg_binomial_pmf_Suc_0 [simp]: "neg_binomial_pmf (Suc 0) p = geometric_pmf p" + by (auto simp: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf bind_return_pmf') + +lemmas neg_binomial_pmf_Suc [simp del] = neg_binomial_pmf.simps(2) + +lemma neg_binomial_prob_1 [simp]: "neg_binomial_pmf n 1 = return_pmf 0" + by (induction n) (simp_all add: neg_binomial_pmf_Suc) + +text \ + We can now show the aforementioned intuition about counting the failures before the + \n\-th success with the following recurrence: +\ +lemma neg_binomial_pmf_unfold: + assumes p: "p \ {0<..1}" + shows "neg_binomial_pmf (Suc n) p = + do {b \ bernoulli_pmf p; + if b then neg_binomial_pmf n p else map_pmf Suc (neg_binomial_pmf (Suc n) p)}" + (is "_ = ?rhs") + unfolding neg_binomial_pmf_Suc + by (subst geometric_bind_pmf_unfold[OF p]) + (auto simp: map_pmf_def pair_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf' + intro!: bind_pmf_cong) + +text \ + Next, we show an explicit formula for the probability mass function of the negative + binomial distribution: +\ +lemma pmf_neg_binomial: + assumes p: "p \ {0<..1}" + shows "pmf (neg_binomial_pmf n p) k = real ((k + n - 1) choose k) * p ^ n * (1 - p) ^ k" +proof (induction n arbitrary: k) + case 0 + thus ?case using assms by (auto simp: indicator_def) +next + case (Suc n) + show ?case + proof (cases "n = 0") + case True + thus ?thesis using assms by auto + next + case False + let ?f = "pmf (neg_binomial_pmf n p)" + have "pmf (neg_binomial_pmf (Suc n) p) k = + pmf (geometric_pmf p \ (\x. map_pmf ((+) x) (neg_binomial_pmf n p))) k" + by (auto simp: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf neg_binomial_pmf_Suc) + also have "\ = measure_pmf.expectation (geometric_pmf p) + (\x. measure_pmf.prob (neg_binomial_pmf n p) ((+) x -` {k}))" + by (simp add: pmf_bind pmf_map) + also have "(\x. (+) x -` {k}) = (\x. if x \ k then {k - x} else {})" + by (auto simp: fun_eq_iff) + also have "(\x. measure_pmf.prob (neg_binomial_pmf n p) (\ x)) = + (\x. if x \ k then ?f(k - x) else 0)" + by (auto simp: fun_eq_iff measure_pmf_single) + also have "measure_pmf.expectation (geometric_pmf p) \ = + (\i\k. pmf (neg_binomial_pmf n p) (k - i) * pmf (geometric_pmf p) i)" + by (subst integral_measure_pmf_real[where A = "{..k}"]) (auto split: if_splits) + also have "\ = p^(n+1) * (1-p)^k * real (\i\k. (k - i + n - 1) choose (k - i))" + unfolding sum_distrib_left of_nat_sum + proof (intro sum.cong refl, goal_cases) + case (1 i) + have "pmf (neg_binomial_pmf n p) (k - i) * pmf (geometric_pmf p) i = + real ((k - i + n - 1) choose (k - i)) * p^(n+1) * ((1-p)^(k-i) * (1-p)^i)" + using assms Suc.IH by (simp add: mult_ac) + also have "(1-p)^(k-i) * (1-p)^i = (1-p)^k" + using 1 by (subst power_add [symmetric]) auto + finally show ?case by simp + qed + also have "(\i\k. (k - i + n - 1) choose (k - i)) = (\i\k. (n - 1 + i) choose i)" + by (intro sum.reindex_bij_witness[of _ "\i. k - i" "\i. k - i"]) + (use \n \ 0\ in \auto simp: algebra_simps\) + also have "\ = (n + k) choose k" + by (subst sum_choose_lower) (use \n \ 0\ in auto) + finally show ?thesis + by (simp add: add_ac) + qed +qed + +(* TODO: Move? *) +lemma gbinomial_0_left: "0 gchoose k = (if k = 0 then 1 else 0)" + by (cases k) auto + +text \ + The following alternative formula highlights why it is called `negative binomial distribution': +\ +lemma pmf_neg_binomial': + assumes p: "p \ {0<..1}" + shows "pmf (neg_binomial_pmf n p) k = (-1) ^ k * ((-real n) gchoose k) * p ^ n * (1 - p) ^ k" +proof (cases "n > 0") + case n: True + have "pmf (neg_binomial_pmf n p) k = real ((k + n - 1) choose k) * p ^ n * (1 - p) ^ k" + by (rule pmf_neg_binomial) fact+ + also have "real ((k + n - 1) choose k) = ((real k + real n - 1) gchoose k)" + using n by (subst binomial_gbinomial) (auto simp: of_nat_diff) + also have "\ = (-1) ^ k * ((-real n) gchoose k)" + by (subst gbinomial_negated_upper) auto + finally show ?thesis by simp +qed (auto simp: indicator_def gbinomial_0_left) + +text \ + The cumulative distribution function of the negative binomial distribution can be + expressed in terms of that of the `normal' binomial distribution. +\ +lemma prob_neg_binomial_pmf_atMost: + assumes p: "p \ {0<..1}" + shows "measure_pmf.prob (neg_binomial_pmf n p) {..k} = + measure_pmf.prob (binomial_pmf (n + k) (1 - p)) {..k}" +proof (cases "n = 0") + case [simp]: True + have "set_pmf (binomial_pmf (n + k) (1 - p)) \ {..n+k}" + using p by (subst set_pmf_binomial_eq) auto + hence "measure_pmf.prob (binomial_pmf (n + k) (1 - p)) {..k} = 1" + by (subst measure_pmf.prob_eq_1) (auto intro!: AE_pmfI) + thus ?thesis by simp +next + case False + hence n: "n > 0" by auto + have "measure_pmf.prob (binomial_pmf (n + k) (1 - p)) {..k} = (\i\k. pmf (binomial_pmf (n + k) (1 - p)) i)" + by (intro measure_measure_pmf_finite) auto + also have "\ = (\i\k. real ((n + k) choose i) * p ^ (n + k - i) * (1 - p) ^ i)" + using p by (simp add: mult_ac) + also have "\ = p ^ n * (\i\k. real ((n + k) choose i) * (1 - p) ^ i * p ^ (k - i))" + unfolding sum_distrib_left by (intro sum.cong) (auto simp: algebra_simps simp flip: power_add) + also have "(\i\k. real ((n + k) choose i) * (1 - p) ^ i * p ^ (k - i)) = + (\i\k. ((n + i - 1) choose i) * (1 - p) ^ i)" + using gbinomial_partial_sum_poly_xpos[of k "real n" "1 - p" p] n + by (simp add: binomial_gbinomial add_ac of_nat_diff) + also have "p ^ n * \ = (\i\k. pmf (neg_binomial_pmf n p) i)" + using p unfolding sum_distrib_left by (simp add: pmf_neg_binomial algebra_simps) + also have "\ = measure_pmf.prob (neg_binomial_pmf n p) {..k}" + by (intro measure_measure_pmf_finite [symmetric]) auto + finally show ?thesis .. +qed + +lemma prob_neg_binomial_pmf_lessThan: + assumes p: "p \ {0<..1}" + shows "measure_pmf.prob (neg_binomial_pmf n p) {.. + The expected value of the negative binomial distribution is $n(1-p)/p$: +\ +lemma nn_integral_neg_binomial_pmf_real: + assumes p: "p \ {0<..1}" + shows "nn_integral (measure_pmf (neg_binomial_pmf n p)) of_nat = ennreal (n * (1 - p) / p)" +proof (induction n) + case 0 + thus ?case by auto +next + case (Suc n) + have "nn_integral (measure_pmf (neg_binomial_pmf (Suc n) p)) of_nat = + nn_integral (measure_pmf (geometric_pmf p)) of_nat + + nn_integral (measure_pmf (neg_binomial_pmf n p)) of_nat" + by (simp add: neg_binomial_pmf_Suc case_prod_unfold nn_integral_add nn_integral_pair_pmf') + also have "nn_integral (measure_pmf (geometric_pmf p)) of_nat = ennreal ((1-p) / p)" + unfolding ennreal_of_nat_eq_real_of_nat + using expectation_geometric_pmf[OF p] integrable_real_geometric_pmf[OF p] + by (subst nn_integral_eq_integral) auto + also have "nn_integral (measure_pmf (neg_binomial_pmf n p)) of_nat = n * (1 - p) / p" using p + by (subst Suc.IH) + (auto simp: ennreal_of_nat_eq_real_of_nat ennreal_mult simp flip: divide_ennreal ennreal_minus) + also have "ennreal ((1 - p) / p) + ennreal (real n * (1 - p) / p) = + ennreal ((1-p) / p + real n * (1 - p) / p)" + by (intro ennreal_plus [symmetric] divide_nonneg_pos mult_nonneg_nonneg) (use p in auto) + also have "(1-p) / p + real n * (1 - p) / p = real (Suc n) * (1 - p) / p" + using p by (auto simp: field_simps) + finally show ?case + by (simp add: ennreal_of_nat_eq_real_of_nat) +qed + +lemma integrable_neg_binomial_pmf_real: + assumes p: "p \ {0<..1}" + shows "integrable (measure_pmf (neg_binomial_pmf n p)) real" + using nn_integral_neg_binomial_pmf_real[OF p, of n] + by (subst integrable_iff_bounded) (auto simp flip: ennreal_of_nat_eq_real_of_nat) + +lemma expectation_neg_binomial_pmf: + assumes p: "p \ {0<..1}" + shows "measure_pmf.expectation (neg_binomial_pmf n p) real = n * (1 - p) / p" +proof - + have "nn_integral (measure_pmf (neg_binomial_pmf n p)) of_nat = ennreal (n * (1 - p) / p)" + by (intro nn_integral_neg_binomial_pmf_real p) + also have "of_nat = (\x. ennreal (real x))" + by (simp add: ennreal_of_nat_eq_real_of_nat fun_eq_iff) + finally show ?thesis + using p by (subst (asm) nn_integral_eq_integrable) auto +qed + + subsection \PMFs from association lists\ definition pmf_of_list ::" ('a \ real) list \ 'a pmf" where diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Tue Feb 23 10:13:09 2021 +0100 @@ -465,6 +465,21 @@ "expectation X = 0 \ variance X = expectation (\x. (X x)^2)" by simp +theorem%important (in prob_space) Chebyshev_inequality: + assumes [measurable]: "random_variable borel f" + assumes "integrable M (\x. f x ^ 2)" + defines "\ \ expectation f" + assumes "a > 0" + shows "prob {x\space M. \f x - \\ \ a} \ variance f / a\<^sup>2" + unfolding \_def +proof (rule second_moment_method) + have integrable: "integrable M f" + using assms by (blast dest: square_integrable_imp_integrable) + show "integrable M (\x. (f x - expectation f)\<^sup>2)" + using assms integrable unfolding power2_eq_square ring_distribs + by (intro Bochner_Integration.integrable_diff) auto +qed (use assms in auto) + locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2 sublocale pair_prob_space \ P?: prob_space "M1 \\<^sub>M M2" @@ -501,6 +516,18 @@ finally show ?thesis by (simp add: measure_nonneg prod_nonneg) qed +lemma product_prob_spaceI: + assumes "\i. prob_space (M i)" + shows "product_prob_space M" + unfolding product_prob_space_def product_prob_space_axioms_def product_sigma_finite_def +proof safe + fix i + interpret prob_space "M i" + by (rule assms) + show "sigma_finite_measure (M i)" "prob_space (M i)" + by unfold_locales +qed + subsection \Distributions\ definition distributed :: "'a measure \ 'b measure \ ('a \ 'b) \ ('b \ ennreal) \ bool" @@ -1226,4 +1253,53 @@ lemma (in prob_space) prob_space_completion: "prob_space (completion M)" by (rule prob_spaceI) (simp add: emeasure_space_1) +lemma distr_PiM_finite_prob_space: + assumes fin: "finite I" + assumes "product_prob_space M" + assumes "product_prob_space M'" + assumes [measurable]: "\i. i \ I \ f \ measurable (M i) (M' i)" + shows "distr (PiM I M) (PiM I M') (compose I f) = PiM I (\i. distr (M i) (M' i) f)" +proof - + interpret M: product_prob_space M by fact + interpret M': product_prob_space M' by fact + define N where "N = (\i. if i \ I then distr (M i) (M' i) f else M' i)" + have [intro]: "prob_space (N i)" for i + by (auto simp: N_def intro!: M.M.prob_space_distr M'.prob_space) + + interpret N: product_prob_space N + by (intro product_prob_spaceI) (auto simp: N_def M'.prob_space intro: M.M.prob_space_distr) + + have "distr (PiM I M) (PiM I M') (compose I f) = PiM I N" + proof (rule N.PiM_eqI) + have N_events_eq: "sets (Pi\<^sub>M I N) = sets (Pi\<^sub>M I M')" + unfolding N_def by (intro sets_PiM_cong) auto + also have "\ = sets (distr (Pi\<^sub>M I M) (Pi\<^sub>M I M') (compose I f))" + by simp + finally show "sets (distr (Pi\<^sub>M I M) (Pi\<^sub>M I M') (compose I f)) = sets (Pi\<^sub>M I N)" .. + + fix A assume A: "\i. i \ I \ A i \ N.M.events i" + have "emeasure (distr (Pi\<^sub>M I M) (Pi\<^sub>M I M') (compose I f)) (Pi\<^sub>E I A) = + emeasure (Pi\<^sub>M I M) (compose I f -` Pi\<^sub>E I A \ space (Pi\<^sub>M I M))" + proof (intro emeasure_distr) + show "compose I f \ Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M I M'" + unfolding compose_def by measurable + show "Pi\<^sub>E I A \ sets (Pi\<^sub>M I M')" + unfolding N_events_eq [symmetric] by (intro sets_PiM_I_finite fin A) + qed + also have "compose I f -` Pi\<^sub>E I A \ space (Pi\<^sub>M I M) = Pi\<^sub>E I (\i. f -` A i \ space (M i))" + using A by (auto simp: space_PiM PiE_def Pi_def extensional_def N_def compose_def) + also have "emeasure (Pi\<^sub>M I M) (Pi\<^sub>E I (\i. f -` A i \ space (M i))) = + (\i\I. emeasure (M i) (f -` A i \ space (M i)))" + using A by (intro M.emeasure_PiM fin) (auto simp: N_def) + also have "\ = (\i\I. emeasure (distr (M i) (M' i) f) (A i))" + using A by (intro prod.cong emeasure_distr [symmetric]) (auto simp: N_def) + also have "\ = (\i\I. emeasure (N i) (A i))" + unfolding N_def by (intro prod.cong) (auto simp: N_def) + finally show "emeasure (distr (Pi\<^sub>M I M) (Pi\<^sub>M I M') (compose I f)) (Pi\<^sub>E I A) = \" . + qed fact+ + also have "PiM I N = PiM I (\i. distr (M i) (M' i) f)" + by (intro PiM_cong) (auto simp: N_def) + finally show ?thesis . +qed + end diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Probability/Product_PMF.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Product_PMF.thy Tue Feb 23 10:13:09 2021 +0100 @@ -0,0 +1,910 @@ +(* + File: Product_PMF.thy + Authors: Manuel Eberl, Max W. Haslbeck +*) +section \Indexed products of PMFs\ +theory Product_PMF + imports Probability_Mass_Function Independent_Family +begin + +subsection \Preliminaries\ + +lemma pmf_expectation_eq_infsetsum: "measure_pmf.expectation p f = infsetsum (\x. pmf p x * f x) UNIV" + unfolding infsetsum_def measure_pmf_eq_density by (subst integral_density) simp_all + +lemma measure_pmf_prob_product: + assumes "countable A" "countable B" + shows "measure_pmf.prob (pair_pmf M N) (A \ B) = measure_pmf.prob M A * measure_pmf.prob N B" +proof - + have "measure_pmf.prob (pair_pmf M N) (A \ B) = (\\<^sub>a(a, b)\A \ B. pmf M a * pmf N b)" + by (auto intro!: infsetsum_cong simp add: measure_pmf_conv_infsetsum pmf_pair) + also have "\ = measure_pmf.prob M A * measure_pmf.prob N B" + using assms by (subst infsetsum_product) (auto simp add: measure_pmf_conv_infsetsum) + finally show ?thesis + by simp +qed + + +subsection \Definition\ + +text \ + In analogy to @{const PiM}, we define an indexed product of PMFs. In the literature, this + is typically called taking a vector of independent random variables. Note that the components + do not have to be identically distributed. + + The operation takes an explicit index set \<^term>\A :: 'a set\ and a function \<^term>\f :: 'a \ 'b pmf\ + that maps each element from \<^term>\A\ to a PMF and defines the product measure + $\bigotimes_{i\in A} f(i)$ , which is represented as a \<^typ>\('a \ 'b) pmf\. + + Note that unlike @{const PiM}, this only works for \<^emph>\finite\ index sets. It could + be extended to countable sets and beyond, but the construction becomes somewhat more involved. +\ +definition Pi_pmf :: "'a set \ 'b \ ('a \ 'b pmf) \ ('a \ 'b) pmf" where + "Pi_pmf A dflt p = + embed_pmf (\f. if (\x. x \ A \ f x = dflt) then \x\A. pmf (p x) (f x) else 0)" + +text \ + A technical subtlety that needs to be addressed is this: Intuitively, the functions in the + support of a product distribution have domain \A\. However, since HOL is a total logic, these + functions must still return \<^emph>\some\ value for inputs outside \A\. The product measure + @{const PiM} simply lets these functions return @{const undefined} in these cases. We chose a + different solution here, which is to supply a default value \<^term>\dflt :: 'b\ that is returned + in these cases. + + As one possible application, one could model the result of \n\ different independent coin + tosses as @{term "Pi_pmf {0.._. bernoulli_pmf (1 / 2))"}. This returns a function + of type \<^typ>\nat \ bool\ that maps every natural number below \n\ to the result of the + corresponding coin toss, and every other natural number to \<^term>\False\. +\ + +lemma pmf_Pi: + assumes A: "finite A" + shows "pmf (Pi_pmf A dflt p) f = + (if (\x. x \ A \ f x = dflt) then \x\A. pmf (p x) (f x) else 0)" + unfolding Pi_pmf_def +proof (rule pmf_embed_pmf, goal_cases) + case 2 + define S where "S = {f. \x. x \ A \ f x = dflt}" + define B where "B = (\x. set_pmf (p x))" + + have neutral_left: "(\xa\A. pmf (p xa) (f xa)) = 0" + if "f \ PiE A B - (\f. restrict f A) ` S" for f + proof - + have "restrict (\x. if x \ A then f x else dflt) A \ (\f. restrict f A) ` S" + by (intro imageI) (auto simp: S_def) + also have "restrict (\x. if x \ A then f x else dflt) A = f" + using that by (auto simp: PiE_def Pi_def extensional_def fun_eq_iff) + finally show ?thesis using that by blast + qed + have neutral_right: "(\xa\A. pmf (p xa) (f xa)) = 0" + if "f \ (\f. restrict f A) ` S - PiE A B" for f + proof - + from that obtain f' where f': "f = restrict f' A" "f' \ S" by auto + moreover from this and that have "restrict f' A \ PiE A B" by simp + then obtain x where "x \ A" "pmf (p x) (f' x) = 0" by (auto simp: B_def set_pmf_eq) + with f' and A show ?thesis by auto + qed + + have "(\f. \x\A. pmf (p x) (f x)) abs_summable_on PiE A B" + by (intro abs_summable_on_prod_PiE A) (auto simp: B_def) + also have "?this \ (\f. \x\A. pmf (p x) (f x)) abs_summable_on (\f. restrict f A) ` S" + by (intro abs_summable_on_cong_neutral neutral_left neutral_right) auto + also have "\ \ (\f. \x\A. pmf (p x) (restrict f A x)) abs_summable_on S" + by (rule abs_summable_on_reindex_iff [symmetric]) (force simp: inj_on_def fun_eq_iff S_def) + also have "\ \ (\f. if \x. x \ A \ f x = dflt then \x\A. pmf (p x) (f x) else 0) + abs_summable_on UNIV" + by (intro abs_summable_on_cong_neutral) (auto simp: S_def) + finally have summable: \ . + + have "1 = (\x\A. 1::real)" by simp + also have "(\x\A. 1) = (\x\A. \\<^sub>ay\B x. pmf (p x) y)" + unfolding B_def by (subst infsetsum_pmf_eq_1) auto + also have "(\x\A. \\<^sub>ay\B x. pmf (p x) y) = (\\<^sub>af\Pi\<^sub>E A B. \x\A. pmf (p x) (f x))" + by (intro infsetsum_prod_PiE [symmetric] A) (auto simp: B_def) + also have "\ = (\\<^sub>af\(\f. restrict f A) ` S. \x\A. pmf (p x) (f x))" using A + by (intro infsetsum_cong_neutral neutral_left neutral_right refl) + also have "\ = (\\<^sub>af\S. \x\A. pmf (p x) (restrict f A x))" + by (rule infsetsum_reindex) (force simp: inj_on_def fun_eq_iff S_def) + also have "\ = (\\<^sub>af\S. \x\A. pmf (p x) (f x))" + by (intro infsetsum_cong) (auto simp: S_def) + also have "\ = (\\<^sub>af. if \x. x \ A \ f x = dflt then \x\A. pmf (p x) (f x) else 0)" + by (intro infsetsum_cong_neutral) (auto simp: S_def) + also have "ennreal \ = (\\<^sup>+f. ennreal (if \x. x \ A \ f x = dflt + then \x\A. pmf (p x) (f x) else 0) \count_space UNIV)" + by (intro nn_integral_conv_infsetsum [symmetric] summable) (auto simp: prod_nonneg) + finally show ?case by simp +qed (auto simp: prod_nonneg) + +lemma Pi_pmf_cong: + assumes "A = A'" "dflt = dflt'" "\x. x \ A \ f x = f' x" + shows "Pi_pmf A dflt f = Pi_pmf A' dflt' f'" +proof - + have "(\fa. if \x. x \ A \ fa x = dflt then \x\A. pmf (f x) (fa x) else 0) = + (\f. if \x. x \ A' \ f x = dflt' then \x\A'. pmf (f' x) (f x) else 0)" + using assms by (intro ext) (auto intro!: prod.cong) + thus ?thesis + by (simp only: Pi_pmf_def) +qed + +lemma pmf_Pi': + assumes "finite A" "\x. x \ A \ f x = dflt" + shows "pmf (Pi_pmf A dflt p) f = (\x\A. pmf (p x) (f x))" + using assms by (subst pmf_Pi) auto + +lemma pmf_Pi_outside: + assumes "finite A" "\x. x \ A \ f x \ dflt" + shows "pmf (Pi_pmf A dflt p) f = 0" + using assms by (subst pmf_Pi) auto + +lemma pmf_Pi_empty [simp]: "Pi_pmf {} dflt p = return_pmf (\_. dflt)" + by (intro pmf_eqI, subst pmf_Pi) (auto simp: indicator_def) + +lemma set_Pi_pmf_subset: "finite A \ set_pmf (Pi_pmf A dflt p) \ {f. \x. x \ A \ f x = dflt}" + by (auto simp: set_pmf_eq pmf_Pi) + + +subsection \Dependent product sets with a default\ + +text \ + The following describes a dependent product of sets where the functions are required to return + the default value \<^term>\dflt\ outside their domain, in analogy to @{const PiE}, which uses + @{const undefined}. +\ +definition PiE_dflt + where "PiE_dflt A dflt B = {f. \x. (x \ A \ f x \ B x) \ (x \ A \ f x = dflt)}" + +lemma restrict_PiE_dflt: "(\h. restrict h A) ` PiE_dflt A dflt B = PiE A B" +proof (intro equalityI subsetI) + fix h assume "h \ (\h. restrict h A) ` PiE_dflt A dflt B" + thus "h \ PiE A B" + by (auto simp: PiE_dflt_def) +next + fix h assume h: "h \ PiE A B" + hence "restrict (\x. if x \ A then h x else dflt) A \ (\h. restrict h A) ` PiE_dflt A dflt B" + by (intro imageI) (auto simp: PiE_def extensional_def PiE_dflt_def) + also have "restrict (\x. if x \ A then h x else dflt) A = h" + using h by (auto simp: fun_eq_iff) + finally show "h \ (\h. restrict h A) ` PiE_dflt A dflt B" . +qed + +lemma dflt_image_PiE: "(\h x. if x \ A then h x else dflt) ` PiE A B = PiE_dflt A dflt B" + (is "?f ` ?X = ?Y") +proof (intro equalityI subsetI) + fix h assume "h \ ?f ` ?X" + thus "h \ ?Y" + by (auto simp: PiE_dflt_def PiE_def) +next + fix h assume h: "h \ ?Y" + hence "?f (restrict h A) \ ?f ` ?X" + by (intro imageI) (auto simp: PiE_def extensional_def PiE_dflt_def) + also have "?f (restrict h A) = h" + using h by (auto simp: fun_eq_iff PiE_dflt_def) + finally show "h \ ?f ` ?X" . +qed + +lemma finite_PiE_dflt [intro]: + assumes "finite A" "\x. x \ A \ finite (B x)" + shows "finite (PiE_dflt A d B)" +proof - + have "PiE_dflt A d B = (\f x. if x \ A then f x else d) ` PiE A B" + by (rule dflt_image_PiE [symmetric]) + also have "finite \" + by (intro finite_imageI finite_PiE assms) + finally show ?thesis . +qed + +lemma card_PiE_dflt: + assumes "finite A" "\x. x \ A \ finite (B x)" + shows "card (PiE_dflt A d B) = (\x\A. card (B x))" +proof - + from assms have "(\x\A. card (B x)) = card (PiE A B)" + by (intro card_PiE [symmetric]) auto + also have "PiE A B = (\f. restrict f A) ` PiE_dflt A d B" + by (rule restrict_PiE_dflt [symmetric]) + also have "card \ = card (PiE_dflt A d B)" + by (intro card_image) (force simp: inj_on_def restrict_def fun_eq_iff PiE_dflt_def) + finally show ?thesis .. +qed + +lemma PiE_dflt_empty_iff [simp]: "PiE_dflt A dflt B = {} \ (\x\A. B x = {})" + by (simp add: dflt_image_PiE [symmetric] PiE_eq_empty_iff) + +lemma set_Pi_pmf_subset': + assumes "finite A" + shows "set_pmf (Pi_pmf A dflt p) \ PiE_dflt A dflt (set_pmf \ p)" + using assms by (auto simp: set_pmf_eq pmf_Pi PiE_dflt_def) + +lemma set_Pi_pmf: + assumes "finite A" + shows "set_pmf (Pi_pmf A dflt p) = PiE_dflt A dflt (set_pmf \ p)" +proof (rule equalityI) + show "PiE_dflt A dflt (set_pmf \ p) \ set_pmf (Pi_pmf A dflt p)" + proof safe + fix f assume f: "f \ PiE_dflt A dflt (set_pmf \ p)" + hence "pmf (Pi_pmf A dflt p) f = (\x\A. pmf (p x) (f x))" + using assms by (auto simp: pmf_Pi PiE_dflt_def) + also have "\ > 0" + using f by (intro prod_pos) (auto simp: PiE_dflt_def set_pmf_eq) + finally show "f \ set_pmf (Pi_pmf A dflt p)" + by (auto simp: set_pmf_eq) + qed +qed (use set_Pi_pmf_subset'[OF assms, of dflt p] in auto) + +text \ + The probability of an independent combination of events is precisely the product + of the probabilities of each individual event. +\ +lemma measure_Pi_pmf_PiE_dflt: + assumes [simp]: "finite A" + shows "measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B) = + (\x\A. measure_pmf.prob (p x) (B x))" +proof - + define B' where "B' = (\x. B x \ set_pmf (p x))" + have "measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B) = + (\\<^sub>ah\PiE_dflt A dflt B. pmf (Pi_pmf A dflt p) h)" + by (rule measure_pmf_conv_infsetsum) + also have "\ = (\\<^sub>ah\PiE_dflt A dflt B. \x\A. pmf (p x) (h x))" + by (intro infsetsum_cong, subst pmf_Pi') (auto simp: PiE_dflt_def) + also have "\ = (\\<^sub>ah\(\h. restrict h A) ` PiE_dflt A dflt B. \x\A. pmf (p x) (h x))" + by (subst infsetsum_reindex) (force simp: inj_on_def PiE_dflt_def fun_eq_iff)+ + also have "(\h. restrict h A) ` PiE_dflt A dflt B = PiE A B" + by (rule restrict_PiE_dflt) + also have "(\\<^sub>ah\PiE A B. \x\A. pmf (p x) (h x)) = (\\<^sub>ah\PiE A B'. \x\A. pmf (p x) (h x))" + by (intro infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq) + also have "(\\<^sub>ah\PiE A B'. \x\A. pmf (p x) (h x)) = (\x\A. infsetsum (pmf (p x)) (B' x))" + by (intro infsetsum_prod_PiE) (auto simp: B'_def) + also have "\ = (\x\A. infsetsum (pmf (p x)) (B x))" + by (intro prod.cong infsetsum_cong_neutral) (auto simp: B'_def set_pmf_eq) + also have "\ = (\x\A. measure_pmf.prob (p x) (B x))" + by (subst measure_pmf_conv_infsetsum) (rule refl) + finally show ?thesis . +qed + +lemma measure_Pi_pmf_Pi: + fixes t::nat + assumes [simp]: "finite A" + shows "measure_pmf.prob (Pi_pmf A dflt p) (Pi A B) = + (\x\A. measure_pmf.prob (p x) (B x))" (is "?lhs = ?rhs") +proof - + have "?lhs = measure_pmf.prob (Pi_pmf A dflt p) (PiE_dflt A dflt B)" + by (intro measure_prob_cong_0) + (auto simp: PiE_dflt_def PiE_def intro!: pmf_Pi_outside)+ + also have "\ = ?rhs" + using assms by (simp add: measure_Pi_pmf_PiE_dflt) + finally show ?thesis + by simp +qed + + +subsection \Common PMF operations on products\ + +text \ + @{const Pi_pmf} distributes over the `bind' operation in the Giry monad: +\ +lemma Pi_pmf_bind: + assumes "finite A" + shows "Pi_pmf A d (\x. bind_pmf (p x) (q x)) = + do {f \ Pi_pmf A d' p; Pi_pmf A d (\x. q x (f x))}" (is "?lhs = ?rhs") +proof (rule pmf_eqI, goal_cases) + case (1 f) + show ?case + proof (cases "\x\-A. f x \ d") + case False + define B where "B = (\x. set_pmf (p x))" + have [simp]: "countable (B x)" for x by (auto simp: B_def) + + { + fix x :: 'a + have "(\a. pmf (p x) a * 1) abs_summable_on B x" + by (simp add: pmf_abs_summable) + moreover have "norm (pmf (p x) a * 1) \ norm (pmf (p x) a * pmf (q x a) (f x))" for a + unfolding norm_mult by (intro mult_left_mono) (auto simp: pmf_le_1) + ultimately have "(\a. pmf (p x) a * pmf (q x a) (f x)) abs_summable_on B x" + by (rule abs_summable_on_comparison_test) + } note summable = this + + have "pmf ?rhs f = (\\<^sub>ag. pmf (Pi_pmf A d' p) g * (\x\A. pmf (q x (g x)) (f x)))" + by (subst pmf_bind, subst pmf_Pi') + (insert assms False, simp_all add: pmf_expectation_eq_infsetsum) + also have "\ = (\\<^sub>ag\PiE_dflt A d' B. + pmf (Pi_pmf A d' p) g * (\x\A. pmf (q x (g x)) (f x)))" unfolding B_def + using assms by (intro infsetsum_cong_neutral) (auto simp: pmf_Pi PiE_dflt_def set_pmf_eq) + also have "\ = (\\<^sub>ag\PiE_dflt A d' B. + (\x\A. pmf (p x) (g x) * pmf (q x (g x)) (f x)))" + using assms by (intro infsetsum_cong) (auto simp: pmf_Pi PiE_dflt_def prod.distrib) + also have "\ = (\\<^sub>ag\(\g. restrict g A) ` PiE_dflt A d' B. + (\x\A. pmf (p x) (g x) * pmf (q x (g x)) (f x)))" + by (subst infsetsum_reindex) (force simp: PiE_dflt_def inj_on_def fun_eq_iff)+ + also have "(\g. restrict g A) ` PiE_dflt A d' B = PiE A B" + by (rule restrict_PiE_dflt) + also have "(\\<^sub>ag\\. (\x\A. pmf (p x) (g x) * pmf (q x (g x)) (f x))) = + (\x\A. \\<^sub>aa\B x. pmf (p x) a * pmf (q x a) (f x))" + using assms summable by (subst infsetsum_prod_PiE) simp_all + also have "\ = (\x\A. \\<^sub>aa. pmf (p x) a * pmf (q x a) (f x))" + by (intro prod.cong infsetsum_cong_neutral) (auto simp: B_def set_pmf_eq) + also have "\ = pmf ?lhs f" + using False assms by (subst pmf_Pi') (simp_all add: pmf_bind pmf_expectation_eq_infsetsum) + finally show ?thesis .. + next + case True + have "pmf ?rhs f = + measure_pmf.expectation (Pi_pmf A d' p) (\x. pmf (Pi_pmf A d (\xa. q xa (x xa))) f)" + using assms by (simp add: pmf_bind) + also have "\ = measure_pmf.expectation (Pi_pmf A d' p) (\x. 0)" + using assms True by (intro Bochner_Integration.integral_cong pmf_Pi_outside) auto + also have "\ = pmf ?lhs f" + using assms True by (subst pmf_Pi_outside) auto + finally show ?thesis .. + qed +qed + +lemma Pi_pmf_return_pmf [simp]: + assumes "finite A" + shows "Pi_pmf A dflt (\x. return_pmf (f x)) = return_pmf (\x. if x \ A then f x else dflt)" + using assms by (intro pmf_eqI) (auto simp: pmf_Pi simp: indicator_def) + +text \ + Analogously any componentwise mapping can be pulled outside the product: +\ +lemma Pi_pmf_map: + assumes [simp]: "finite A" and "f dflt = dflt'" + shows "Pi_pmf A dflt' (\x. map_pmf f (g x)) = map_pmf (\h. f \ h) (Pi_pmf A dflt g)" +proof - + have "Pi_pmf A dflt' (\x. map_pmf f (g x)) = + Pi_pmf A dflt' (\x. g x \ (\x. return_pmf (f x)))" + using assms by (simp add: map_pmf_def Pi_pmf_bind) + also have "\ = Pi_pmf A dflt g \ (\h. return_pmf (\x. if x \ A then f (h x) else dflt'))" + by (subst Pi_pmf_bind[where d' = dflt]) (auto simp: ) + also have "\ = map_pmf (\h. f \ h) (Pi_pmf A dflt g)" + unfolding map_pmf_def using set_Pi_pmf_subset'[of A dflt g] + by (intro bind_pmf_cong refl arg_cong[of _ _ return_pmf]) + (auto dest: simp: fun_eq_iff PiE_dflt_def assms(2)) + finally show ?thesis . +qed + +text \ + We can exchange the default value in a product of PMFs like this: +\ +lemma Pi_pmf_default_swap: + assumes "finite A" + shows "map_pmf (\f x. if x \ A then f x else dflt') (Pi_pmf A dflt p) = + Pi_pmf A dflt' p" (is "?lhs = ?rhs") +proof (rule pmf_eqI, goal_cases) + case (1 f) + let ?B = "(\f x. if x \ A then f x else dflt') -` {f} \ PiE_dflt A dflt (\_. UNIV)" + show ?case + proof (cases "\x\-A. f x \ dflt'") + case False + let ?f' = "\x. if x \ A then f x else dflt" + from False have "pmf ?lhs f = measure_pmf.prob (Pi_pmf A dflt p) ?B" + using assms unfolding pmf_map + by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) + also from False have "?B = {?f'}" + by (auto simp: fun_eq_iff PiE_dflt_def) + also have "measure_pmf.prob (Pi_pmf A dflt p) {?f'} = pmf (Pi_pmf A dflt p) ?f'" + by (simp add: measure_pmf_single) + also have "\ = pmf ?rhs f" + using False assms by (subst (1 2) pmf_Pi) auto + finally show ?thesis . + next + case True + have "pmf ?lhs f = measure_pmf.prob (Pi_pmf A dflt p) ?B" + using assms unfolding pmf_map + by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) + also from True have "?B = {}" by auto + also have "measure_pmf.prob (Pi_pmf A dflt p) \ = 0" + by simp + also have "0 = pmf ?rhs f" + using True assms by (intro pmf_Pi_outside [symmetric]) auto + finally show ?thesis . + qed +qed + +text \ + The following rule allows reindexing the product: +\ +lemma Pi_pmf_bij_betw: + assumes "finite A" "bij_betw h A B" "\x. x \ A \ h x \ B" + shows "Pi_pmf A dflt (\_. f) = map_pmf (\g. g \ h) (Pi_pmf B dflt (\_. f))" + (is "?lhs = ?rhs") +proof - + have B: "finite B" + using assms bij_betw_finite by auto + have "pmf ?lhs g = pmf ?rhs g" for g + proof (cases "\a. a \ A \ g a = dflt") + case True + define h' where "h' = the_inv_into A h" + have h': "h' (h x) = x" if "x \ A" for x + unfolding h'_def using that assms by (auto simp add: bij_betw_def the_inv_into_f_f) + have h: "h (h' x) = x" if "x \ B" for x + unfolding h'_def using that assms f_the_inv_into_f_bij_betw by fastforce + have "pmf ?rhs g = measure_pmf.prob (Pi_pmf B dflt (\_. f)) ((\g. g \ h) -` {g})" + unfolding pmf_map by simp + also have "\ = measure_pmf.prob (Pi_pmf B dflt (\_. f)) + (((\g. g \ h) -` {g}) \ PiE_dflt B dflt (\_. UNIV))" + using B by (intro measure_prob_cong_0) (auto simp: PiE_dflt_def pmf_Pi_outside) + also have "\ = pmf (Pi_pmf B dflt (\_. f)) (\x. if x \ B then g (h' x) else dflt)" + proof - + have "(if h x \ B then g (h' (h x)) else dflt) = g x" for x + using h' assms True by (cases "x \ A") (auto simp add: bij_betwE) + then have "(\g. g \ h) -` {g} \ PiE_dflt B dflt (\_. UNIV) = + {(\x. if x \ B then g (h' x) else dflt)}" + using assms h' h True unfolding PiE_dflt_def by auto + then show ?thesis + by (simp add: measure_pmf_single) + qed + also have "\ = pmf (Pi_pmf A dflt (\_. f)) g" + using B assms True h'_def + by (auto simp add: pmf_Pi intro!: prod.reindex_bij_betw bij_betw_the_inv_into) + finally show ?thesis + by simp + next + case False + have "pmf ?rhs g = infsetsum (pmf (Pi_pmf B dflt (\_. f))) ((\g. g \ h) -` {g})" + using assms by (auto simp add: measure_pmf_conv_infsetsum pmf_map) + also have "\ = infsetsum (\_. 0) ((\g x. g (h x)) -` {g})" + using B False assms by (intro infsetsum_cong pmf_Pi_outside) fastforce+ + also have "\ = 0" + by simp + finally show ?thesis + using assms False by (auto simp add: pmf_Pi pmf_map) + qed + then show ?thesis + by (rule pmf_eqI) +qed + +text \ + A product of uniform random choices is again a uniform distribution. +\ +lemma Pi_pmf_of_set: + assumes "finite A" "\x. x \ A \ finite (B x)" "\x. x \ A \ B x \ {}" + shows "Pi_pmf A d (\x. pmf_of_set (B x)) = pmf_of_set (PiE_dflt A d B)" (is "?lhs = ?rhs") +proof (rule pmf_eqI, goal_cases) + case (1 f) + show ?case + proof (cases "\x. x \ A \ f x \ d") + case True + hence "pmf ?lhs f = 0" + using assms by (intro pmf_Pi_outside) (auto simp: PiE_dflt_def) + also from True have "f \ PiE_dflt A d B" + by (auto simp: PiE_dflt_def) + hence "0 = pmf ?rhs f" + using assms by (subst pmf_of_set) auto + finally show ?thesis . + next + case False + hence "pmf ?lhs f = (\x\A. pmf (pmf_of_set (B x)) (f x))" + using assms by (subst pmf_Pi') auto + also have "\ = (\x\A. indicator (B x) (f x) / real (card (B x)))" + by (intro prod.cong refl, subst pmf_of_set) (use assms False in auto) + also have "\ = (\x\A. indicator (B x) (f x)) / real (\x\A. card (B x))" + by (subst prod_dividef) simp_all + also have "(\x\A. indicator (B x) (f x) :: real) = indicator (PiE_dflt A d B) f" + using assms False by (auto simp: indicator_def PiE_dflt_def) + also have "(\x\A. card (B x)) = card (PiE_dflt A d B)" + using assms by (intro card_PiE_dflt [symmetric]) auto + also have "indicator (PiE_dflt A d B) f / \ = pmf ?rhs f" + using assms by (intro pmf_of_set [symmetric]) auto + finally show ?thesis . + qed +qed + + +subsection \Merging and splitting PMF products\ + +text \ + The following lemma shows that we can add a single PMF to a product: +\ +lemma Pi_pmf_insert: + assumes "finite A" "x \ A" + shows "Pi_pmf (insert x A) dflt p = map_pmf (\(y,f). f(x:=y)) (pair_pmf (p x) (Pi_pmf A dflt p))" +proof (intro pmf_eqI) + fix f + let ?M = "pair_pmf (p x) (Pi_pmf A dflt p)" + have "pmf (map_pmf (\(y, f). f(x := y)) ?M) f = + measure_pmf.prob ?M ((\(y, f). f(x := y)) -` {f})" + by (subst pmf_map) auto + also have "((\(y, f). f(x := y)) -` {f}) = (\y'. {(f x, f(x := y'))})" + by (auto simp: fun_upd_def fun_eq_iff) + also have "measure_pmf.prob ?M \ = measure_pmf.prob ?M {(f x, f(x := dflt))}" + using assms by (intro measure_prob_cong_0) (auto simp: pmf_pair pmf_Pi split: if_splits) + also have "\ = pmf (p x) (f x) * pmf (Pi_pmf A dflt p) (f(x := dflt))" + by (simp add: measure_pmf_single pmf_pair pmf_Pi) + also have "\ = pmf (Pi_pmf (insert x A) dflt p) f" + proof (cases "\y. y \ insert x A \ f y = dflt") + case True + with assms have "pmf (p x) (f x) * pmf (Pi_pmf A dflt p) (f(x := dflt)) = + pmf (p x) (f x) * (\xa\A. pmf (p xa) ((f(x := dflt)) xa))" + by (subst pmf_Pi') auto + also have "(\xa\A. pmf (p xa) ((f(x := dflt)) xa)) = (\xa\A. pmf (p xa) (f xa))" + using assms by (intro prod.cong) auto + also have "pmf (p x) (f x) * \ = pmf (Pi_pmf (insert x A) dflt p) f" + using assms True by (subst pmf_Pi') auto + finally show ?thesis . + qed (insert assms, auto simp: pmf_Pi) + finally show "\ = pmf (map_pmf (\(y, f). f(x := y)) ?M) f" .. +qed + +lemma Pi_pmf_insert': + assumes "finite A" "x \ A" + shows "Pi_pmf (insert x A) dflt p = + do {y \ p x; f \ Pi_pmf A dflt p; return_pmf (f(x := y))}" + using assms + by (subst Pi_pmf_insert) + (auto simp add: map_pmf_def pair_pmf_def case_prod_beta' bind_return_pmf bind_assoc_pmf) + +lemma Pi_pmf_singleton: + "Pi_pmf {x} dflt p = map_pmf (\a b. if b = x then a else dflt) (p x)" +proof - + have "Pi_pmf {x} dflt p = map_pmf (fun_upd (\_. dflt) x) (p x)" + by (subst Pi_pmf_insert) (simp_all add: pair_return_pmf2 pmf.map_comp o_def) + also have "fun_upd (\_. dflt) x = (\z y. if y = x then z else dflt)" + by (simp add: fun_upd_def fun_eq_iff) + finally show ?thesis . +qed + +text \ + Projecting a product of PMFs onto a component yields the expected result: +\ +lemma Pi_pmf_component: + assumes "finite A" + shows "map_pmf (\f. f x) (Pi_pmf A dflt p) = (if x \ A then p x else return_pmf dflt)" +proof (cases "x \ A") + case True + define A' where "A' = A - {x}" + from assms and True have A': "A = insert x A'" + by (auto simp: A'_def) + from assms have "map_pmf (\f. f x) (Pi_pmf A dflt p) = p x" unfolding A' + by (subst Pi_pmf_insert) + (auto simp: A'_def pmf.map_comp o_def case_prod_unfold map_fst_pair_pmf) + with True show ?thesis by simp +next + case False + have "map_pmf (\f. f x) (Pi_pmf A dflt p) = map_pmf (\_. dflt) (Pi_pmf A dflt p)" + using assms False set_Pi_pmf_subset[of A dflt p] + by (intro pmf.map_cong refl) (auto simp: set_pmf_eq pmf_Pi_outside) + with False show ?thesis by simp +qed + +text \ + We can take merge two PMF products on disjoint sets like this: +\ +lemma Pi_pmf_union: + assumes "finite A" "finite B" "A \ B = {}" + shows "Pi_pmf (A \ B) dflt p = + map_pmf (\(f,g) x. if x \ A then f x else g x) + (pair_pmf (Pi_pmf A dflt p) (Pi_pmf B dflt p))" (is "_ = map_pmf (?h A) (?q A)") + using assms(1,3) +proof (induction rule: finite_induct) + case (insert x A) + have "map_pmf (?h (insert x A)) (?q (insert x A)) = + do {v \ p x; (f, g) \ pair_pmf (Pi_pmf A dflt p) (Pi_pmf B dflt p); + return_pmf (\y. if y \ insert x A then (f(x := v)) y else g y)}" + by (subst Pi_pmf_insert) + (insert insert.hyps insert.prems, + simp_all add: pair_pmf_def map_bind_pmf bind_map_pmf bind_assoc_pmf bind_return_pmf) + also have "\ = do {v \ p x; (f, g) \ ?q A; return_pmf ((?h A (f,g))(x := v))}" + by (intro bind_pmf_cong refl) (auto simp: fun_eq_iff) + also have "\ = do {v \ p x; f \ map_pmf (?h A) (?q A); return_pmf (f(x := v))}" + by (simp add: bind_map_pmf map_bind_pmf case_prod_unfold cong: if_cong) + also have "\ = do {v \ p x; f \ Pi_pmf (A \ B) dflt p; return_pmf (f(x := v))}" + using insert.hyps and insert.prems by (intro bind_pmf_cong insert.IH [symmetric] refl) auto + also have "\ = Pi_pmf (insert x (A \ B)) dflt p" + by (subst Pi_pmf_insert) + (insert assms insert.hyps insert.prems, auto simp: pair_pmf_def map_bind_pmf) + also have "insert x (A \ B) = insert x A \ B" + by simp + finally show ?case .. +qed (simp_all add: case_prod_unfold map_snd_pair_pmf) + +text \ + We can also project a product to a subset of the indices by mapping all the other + indices to the default value: +\ +lemma Pi_pmf_subset: + assumes "finite A" "A' \ A" + shows "Pi_pmf A' dflt p = map_pmf (\f x. if x \ A' then f x else dflt) (Pi_pmf A dflt p)" +proof - + let ?P = "pair_pmf (Pi_pmf A' dflt p) (Pi_pmf (A - A') dflt p)" + from assms have [simp]: "finite A'" + by (blast dest: finite_subset) + from assms have "A = A' \ (A - A')" + by blast + also have "Pi_pmf \ dflt p = map_pmf (\(f,g) x. if x \ A' then f x else g x) ?P" + using assms by (intro Pi_pmf_union) auto + also have "map_pmf (\f x. if x \ A' then f x else dflt) \ = map_pmf fst ?P" + unfolding map_pmf_comp o_def case_prod_unfold + using set_Pi_pmf_subset[of A' dflt p] by (intro map_pmf_cong refl) (auto simp: fun_eq_iff) + also have "\ = Pi_pmf A' dflt p" + by (simp add: map_fst_pair_pmf) + finally show ?thesis .. +qed + +lemma Pi_pmf_subset': + fixes f :: "'a \ 'b pmf" + assumes "finite A" "B \ A" "\x. x \ A - B \ f x = return_pmf dflt" + shows "Pi_pmf A dflt f = Pi_pmf B dflt f" +proof - + have "Pi_pmf (B \ (A - B)) dflt f = + map_pmf (\(f, g) x. if x \ B then f x else g x) + (pair_pmf (Pi_pmf B dflt f) (Pi_pmf (A - B) dflt f))" + using assms by (intro Pi_pmf_union) (auto dest: finite_subset) + also have "Pi_pmf (A - B) dflt f = Pi_pmf (A - B) dflt (\_. return_pmf dflt)" + using assms by (intro Pi_pmf_cong) auto + also have "\ = return_pmf (\_. dflt)" + using assms by simp + also have "map_pmf (\(f, g) x. if x \ B then f x else g x) + (pair_pmf (Pi_pmf B dflt f) (return_pmf (\_. dflt))) = + map_pmf (\f x. if x \ B then f x else dflt) (Pi_pmf B dflt f)" + by (simp add: map_pmf_def pair_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') + also have "\ = Pi_pmf B dflt f" + using assms by (intro Pi_pmf_default_swap) (auto dest: finite_subset) + also have "B \ (A - B) = A" + using assms by auto + finally show ?thesis . +qed + +lemma Pi_pmf_if_set: + assumes "finite A" + shows "Pi_pmf A dflt (\x. if b x then f x else return_pmf dflt) = + Pi_pmf {x\A. b x} dflt f" +proof - + have "Pi_pmf A dflt (\x. if b x then f x else return_pmf dflt) = + Pi_pmf {x\A. b x} dflt (\x. if b x then f x else return_pmf dflt)" + using assms by (intro Pi_pmf_subset') auto + also have "\ = Pi_pmf {x\A. b x} dflt f" + by (intro Pi_pmf_cong) auto + finally show ?thesis . +qed + +lemma Pi_pmf_if_set': + assumes "finite A" + shows "Pi_pmf A dflt (\x. if b x then return_pmf dflt else f x) = + Pi_pmf {x\A. \b x} dflt f" +proof - + have "Pi_pmf A dflt (\x. if b x then return_pmf dflt else f x) = + Pi_pmf {x\A. \b x} dflt (\x. if b x then return_pmf dflt else f x)" + using assms by (intro Pi_pmf_subset') auto + also have "\ = Pi_pmf {x\A. \b x} dflt f" + by (intro Pi_pmf_cong) auto + finally show ?thesis . +qed + +text \ + Lastly, we can delete a single component from a product: +\ +lemma Pi_pmf_remove: + assumes "finite A" + shows "Pi_pmf (A - {x}) dflt p = map_pmf (\f. f(x := dflt)) (Pi_pmf A dflt p)" +proof - + have "Pi_pmf (A - {x}) dflt p = + map_pmf (\f xa. if xa \ A - {x} then f xa else dflt) (Pi_pmf A dflt p)" + using assms by (intro Pi_pmf_subset) auto + also have "\ = map_pmf (\f. f(x := dflt)) (Pi_pmf A dflt p)" + using set_Pi_pmf_subset[of A dflt p] assms + by (intro map_pmf_cong refl) (auto simp: fun_eq_iff) + finally show ?thesis . +qed + + +subsection \Additional properties\ + +lemma nn_integral_prod_Pi_pmf: + assumes "finite A" + shows "nn_integral (Pi_pmf A dflt p) (\y. \x\A. f x (y x)) = (\x\A. nn_integral (p x) (f x))" + using assms +proof (induction rule: finite_induct) + case (insert x A) + have "nn_integral (Pi_pmf (insert x A) dflt p) (\y. \z\insert x A. f z (y z)) = + (\\<^sup>+a. \\<^sup>+b. f x a * (\z\A. f z (if z = x then a else b z)) \Pi_pmf A dflt p \p x)" + using insert by (auto simp: Pi_pmf_insert case_prod_unfold nn_integral_pair_pmf' cong: if_cong) + also have "(\a b. \z\A. f z (if z = x then a else b z)) = (\a b. \z\A. f z (b z))" + by (intro ext prod.cong) (use insert.hyps in auto) + also have "(\\<^sup>+a. \\<^sup>+b. f x a * (\z\A. f z (b z)) \Pi_pmf A dflt p \p x) = + (\\<^sup>+y. f x y \(p x)) * (\\<^sup>+y. (\z\A. f z (y z)) \(Pi_pmf A dflt p))" + by (simp add: nn_integral_multc nn_integral_cmult) + also have "(\\<^sup>+y. (\z\A. f z (y z)) \(Pi_pmf A dflt p)) = (\x\A. nn_integral (p x) (f x))" + by (rule insert.IH) + also have "(\\<^sup>+y. f x y \(p x)) * \ = (\x\insert x A. nn_integral (p x) (f x))" + using insert.hyps by simp + finally show ?case . +qed auto + +lemma integrable_prod_Pi_pmf: + fixes f :: "'a \ 'b \ 'c :: {real_normed_field, second_countable_topology, banach}" + assumes "finite A" and "\x. x \ A \ integrable (measure_pmf (p x)) (f x)" + shows "integrable (measure_pmf (Pi_pmf A dflt p)) (\h. \x\A. f x (h x))" +proof (intro integrableI_bounded) + have "(\\<^sup>+ x. ennreal (norm (\xa\A. f xa (x xa))) \measure_pmf (Pi_pmf A dflt p)) = + (\\<^sup>+ x. (\y\A. ennreal (norm (f y (x y)))) \measure_pmf (Pi_pmf A dflt p))" + by (simp flip: prod_norm prod_ennreal) + also have "\ = (\x\A. \\<^sup>+ a. ennreal (norm (f x a)) \measure_pmf (p x))" + by (intro nn_integral_prod_Pi_pmf) fact + also have "(\\<^sup>+a. ennreal (norm (f i a)) \measure_pmf (p i)) \ top" if i: "i \ A" for i + using assms(2)[OF i] by (simp add: integrable_iff_bounded) + hence "(\x\A. \\<^sup>+ a. ennreal (norm (f x a)) \measure_pmf (p x)) \ top" + by (subst ennreal_prod_eq_top) auto + finally show "(\\<^sup>+ x. ennreal (norm (\xa\A. f xa (x xa))) \measure_pmf (Pi_pmf A dflt p)) < \" + by (simp add: top.not_eq_extremum) +qed auto + +lemma expectation_prod_Pi_pmf: + fixes f :: "_ \ _ \ real" + assumes "finite A" + assumes "\x. x \ A \ integrable (measure_pmf (p x)) (f x)" + assumes "\x y. x \ A \ y \ set_pmf (p x) \ f x y \ 0" + shows "measure_pmf.expectation (Pi_pmf A dflt p) (\y. \x\A. f x (y x)) = + (\x\A. measure_pmf.expectation (p x) (\v. f x v))" +proof - + have nonneg: "measure_pmf.expectation (p x) (f x) \ 0" if "x \ A" for x + using that by (intro Bochner_Integration.integral_nonneg_AE AE_pmfI assms) + have nonneg': "0 \ measure_pmf.expectation (Pi_pmf A dflt p) (\y. \x\A. f x (y x))" + by (intro Bochner_Integration.integral_nonneg_AE AE_pmfI assms prod_nonneg) + (use assms in \auto simp: set_Pi_pmf PiE_dflt_def\) + + have "ennreal (measure_pmf.expectation (Pi_pmf A dflt p) (\y. \x\A. f x (y x))) = + nn_integral (Pi_pmf A dflt p) (\y. ennreal (\x\A. f x (y x)))" using assms + by (intro nn_integral_eq_integral [symmetric] assms integrable_prod_Pi_pmf) + (auto simp: AE_measure_pmf_iff set_Pi_pmf PiE_dflt_def prod_nonneg) + also have "\ = nn_integral (Pi_pmf A dflt p) (\y. (\x\A. ennreal (f x (y x))))" + by (intro nn_integral_cong_AE AE_pmfI prod_ennreal [symmetric]) + (use assms(1) in \auto simp: set_Pi_pmf PiE_dflt_def intro!: assms(3)\) + also have "\ = (\x\A. \\<^sup>+ a. ennreal (f x a) \measure_pmf (p x))" + by (rule nn_integral_prod_Pi_pmf) fact+ + also have "\ = (\x\A. ennreal (measure_pmf.expectation (p x) (f x)))" + by (intro prod.cong nn_integral_eq_integral assms AE_pmfI) auto + also have "\ = ennreal (\x\A. measure_pmf.expectation (p x) (f x))" + by (intro prod_ennreal nonneg) + finally show ?thesis + using nonneg nonneg' by (subst (asm) ennreal_inj) (auto intro!: prod_nonneg) +qed + +lemma indep_vars_Pi_pmf: + assumes fin: "finite I" + shows "prob_space.indep_vars (measure_pmf (Pi_pmf I dflt p)) + (\_. count_space UNIV) (\x f. f x) I" +proof (cases "I = {}") + case True + show ?thesis + by (subst prob_space.indep_vars_def [OF measure_pmf.prob_space_axioms], + subst prob_space.indep_sets_def [OF measure_pmf.prob_space_axioms]) (simp_all add: True) +next + case [simp]: False + show ?thesis + proof (subst prob_space.indep_vars_iff_distr_eq_PiM') + show "distr (measure_pmf (Pi_pmf I dflt p)) (Pi\<^sub>M I (\i. count_space UNIV)) (\x. restrict x I) = + Pi\<^sub>M I (\i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\f. f i))" + proof (rule product_sigma_finite.PiM_eqI, goal_cases) + case 1 + interpret product_prob_space "\i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\f. f i)" + by (intro product_prob_spaceI prob_space.prob_space_distr measure_pmf.prob_space_axioms) + simp_all + show ?case by unfold_locales + next + case 3 + have "sets (Pi\<^sub>M I (\i. distr (measure_pmf (Pi_pmf I dflt p)) (count_space UNIV) (\f. f i))) = + sets (Pi\<^sub>M I (\_. count_space UNIV))" + by (intro sets_PiM_cong) simp_all + thus ?case by simp + next + case (4 A) + have "Pi\<^sub>E I A \ sets (Pi\<^sub>M I (\i. count_space UNIV))" + using 4 by (intro sets_PiM_I_finite fin) auto + hence "emeasure (distr (measure_pmf (Pi_pmf I dflt p)) (Pi\<^sub>M I (\i. count_space UNIV)) + (\x. restrict x I)) (Pi\<^sub>E I A) = + emeasure (measure_pmf (Pi_pmf I dflt p)) ((\x. restrict x I) -` Pi\<^sub>E I A)" + using 4 by (subst emeasure_distr) (auto simp: space_PiM) + also have "\ = emeasure (measure_pmf (Pi_pmf I dflt p)) (PiE_dflt I dflt A)" + by (intro emeasure_eq_AE AE_pmfI) (auto simp: PiE_dflt_def set_Pi_pmf fin) + also have "\ = (\i\I. emeasure (measure_pmf (p i)) (A i))" + by (simp add: measure_pmf.emeasure_eq_measure measure_Pi_pmf_PiE_dflt fin prod_ennreal) + also have "\ = (\i\I. emeasure (measure_pmf (map_pmf (\f. f i) (Pi_pmf I dflt p))) (A i))" + by (intro prod.cong refl, subst Pi_pmf_component) (auto simp: fin) + finally show ?case + by (simp add: map_pmf_rep_eq) + qed fact+ + qed (simp_all add: measure_pmf.prob_space_axioms) +qed + +lemma + fixes h :: "'a :: comm_monoid_add \ 'b::{banach, second_countable_topology}" + assumes fin: "finite I" + assumes integrable: "\i. i \ I \ integrable (measure_pmf (D i)) h" + shows integrable_sum_Pi_pmf: "integrable (Pi_pmf I dflt D) (\g. \i\I. h (g i))" + and expectation_sum_Pi_pmf: + "measure_pmf.expectation (Pi_pmf I dflt D) (\g. \i\I. h (g i)) = + (\i\I. measure_pmf.expectation (D i) h)" +proof - + have integrable': "integrable (Pi_pmf I dflt D) (\g. h (g i))" if i: "i \ I" for i + proof - + have "integrable (D i) h" + using i by (rule assms) + also have "D i = map_pmf (\g. g i) (Pi_pmf I dflt D)" + by (subst Pi_pmf_component) (use fin i in auto) + finally show "integrable (measure_pmf (Pi_pmf I dflt D)) (\x. h (x i))" + by simp + qed + thus "integrable (Pi_pmf I dflt D) (\g. \i\I. h (g i))" + by (intro Bochner_Integration.integrable_sum) + + have "measure_pmf.expectation (Pi_pmf I dflt D) (\x. \i\I. h (x i)) = + (\i\I. measure_pmf.expectation (map_pmf (\x. x i) (Pi_pmf I dflt D)) h)" + using integrable' by (subst Bochner_Integration.integral_sum) auto + also have "\ = (\i\I. measure_pmf.expectation (D i) h)" + by (intro sum.cong refl, subst Pi_pmf_component) (use fin in auto) + finally show "measure_pmf.expectation (Pi_pmf I dflt D) (\g. \i\I. h (g i)) = + (\i\I. measure_pmf.expectation (D i) h)" . +qed + + +subsection \Applications\ + +text \ + Choosing a subset of a set uniformly at random is equivalent to tossing a fair coin + independently for each element and collecting all the elements that came up heads. +\ +lemma pmf_of_set_Pow_conv_bernoulli: + assumes "finite (A :: 'a set)" + shows "map_pmf (\b. {x\A. b x}) (Pi_pmf A P (\_. bernoulli_pmf (1/2))) = pmf_of_set (Pow A)" +proof - + have "Pi_pmf A P (\_. bernoulli_pmf (1/2)) = pmf_of_set (PiE_dflt A P (\x. UNIV))" + using assms by (simp add: bernoulli_pmf_half_conv_pmf_of_set Pi_pmf_of_set) + also have "map_pmf (\b. {x\A. b x}) \ = pmf_of_set (Pow A)" + proof - + have "bij_betw (\b. {x \ A. b x}) (PiE_dflt A P (\_. UNIV)) (Pow A)" + by (rule bij_betwI[of _ _ _ "\B b. if b \ A then b \ B else P"]) (auto simp add: PiE_dflt_def) + then show ?thesis + using assms by (intro map_pmf_of_set_bij_betw) auto + qed + finally show ?thesis + by simp +qed + +text \ + A binomial distribution can be seen as the number of successes in \n\ independent coin tosses. +\ +lemma binomial_pmf_altdef': + fixes A :: "'a set" + assumes "finite A" and "card A = n" and p: "p \ {0..1}" + shows "binomial_pmf n p = + map_pmf (\f. card {x\A. f x}) (Pi_pmf A dflt (\_. bernoulli_pmf p))" (is "?lhs = ?rhs") +proof - + from assms have "?lhs = binomial_pmf (card A) p" + by simp + also have "\ = ?rhs" + using assms(1) + proof (induction rule: finite_induct) + case empty + with p show ?case by (simp add: binomial_pmf_0) + next + case (insert x A) + from insert.hyps have "card (insert x A) = Suc (card A)" + by simp + also have "binomial_pmf \ p = do { + b \ bernoulli_pmf p; + f \ Pi_pmf A dflt (\_. bernoulli_pmf p); + return_pmf ((if b then 1 else 0) + card {y \ A. f y}) + }" + using p by (simp add: binomial_pmf_Suc insert.IH bind_map_pmf) + also have "\ = do { + b \ bernoulli_pmf p; + f \ Pi_pmf A dflt (\_. bernoulli_pmf p); + return_pmf (card {y \ insert x A. (f(x := b)) y}) + }" + proof (intro bind_pmf_cong refl, goal_cases) + case (1 b f) + have "(if b then 1 else 0) + card {y\A. f y} = card ((if b then {x} else {}) \ {y\A. f y})" + using insert.hyps by auto + also have "(if b then {x} else {}) \ {y\A. f y} = {y\insert x A. (f(x := b)) y}" + using insert.hyps by auto + finally show ?case by simp + qed + also have "\ = map_pmf (\f. card {y\insert x A. f y}) + (Pi_pmf (insert x A) dflt (\_. bernoulli_pmf p))" + using insert.hyps by (subst Pi_pmf_insert) (simp_all add: pair_pmf_def map_bind_pmf) + finally show ?case . + qed + finally show ?thesis . +qed + +end diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Tools/Nunchaku/nunchaku_tool.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Tue Feb 23 10:13:09 2021 +0100 @@ -74,11 +74,6 @@ | CVC4_Not_Found | Unknown_Error of int * string; -fun bash_output_error s = - let val {out, err, rc, ...} = Bash.process s in - ((out, err), rc) - end; - val nunchaku_home_env_var = "NUNCHAKU_HOME"; val unknown_solver = "unknown"; @@ -108,30 +103,33 @@ [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()]; val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem; val _ = File.write prob_path prob_str; - val ((output, error), code) = bash_output_error bash_cmd; + val res = Isabelle_System.bash_process bash_cmd; + val rc = Process_Result.rc res; + val out = Process_Result.out res; + val err = Process_Result.err res; val backend = - (case map_filter (try (unprefix "{backend:")) (split_lines output) of + (case map_filter (try (unprefix "{backend:")) (split_lines out) of [s] => hd (space_explode "," s) | _ => unknown_solver); in - if String.isPrefix "SAT" output then - (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []}) - else if String.isPrefix "UNSAT" output then + if String.isPrefix "SAT" out then + (if sound then Sat else Unknown o SOME) (backend, out, {tys = [], tms = []}) + else if String.isPrefix "UNSAT" out then if complete then Unsat backend else Unknown NONE - else if String.isSubstring "TIMEOUT" output + else if String.isSubstring "TIMEOUT" out (* FIXME: temporary *) - orelse String.isSubstring "kodkod failed (errcode 152)" error then + orelse String.isSubstring "kodkod failed (errcode 152)" err then Timeout - else if String.isPrefix "UNKNOWN" output then + else if String.isPrefix "UNKNOWN" out then Unknown NONE - else if code = 126 then + else if rc = 126 then Nunchaku_Cannot_Execute - else if code = 127 then + else if rc = 127 then Nunchaku_Not_Found else - Unknown_Error (code, - simplify_spaces (elide_string 1000 (if error <> "" then error else output))) + Unknown_Error (rc, + simplify_spaces (elide_string 1000 (if err <> "" then err else out))) end); fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem = diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Feb 23 10:13:09 2021 +0100 @@ -818,11 +818,12 @@ if getenv env_var = "" then (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "") else - (case Isabelle_System.bash_output (cmd ^ File.bash_path file) of - (out, 0) => out - | (_, rc) => - error ("Error caused by prolog system " ^ env_var ^ - ": return code " ^ string_of_int rc)) + let val res = Isabelle_System.bash_process (cmd ^ File.bash_path file) in + res |> Process_Result.check |> Process_Result.out + handle ERROR msg => + cat_error ("Error caused by prolog system " ^ env_var ^ + ": return code " ^ string_of_int (Process_Result.rc res)) msg + end end @@ -865,7 +866,7 @@ (l :: r :: []) => parse_term (unprefix " " r) | _ => raise Fail "unexpected equation in prolog output") fun parse_solution s = map dest_eq (space_explode ";" s) - in map parse_solution (Library.trim_split_lines sol) end + in map parse_solution (split_lines sol) end (* calling external interpreter and getting results *) diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Tue Feb 23 10:13:09 2021 +0100 @@ -214,10 +214,6 @@ |> Exn.capture f |> Exn.release -fun elapsed_time description e = - let val ({elapsed, ...}, result) = Timing.timing e () - in (result, (description, Time.toMilliseconds elapsed)) end - fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) = let @@ -265,25 +261,31 @@ (map File.bash_platform_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ " -o " ^ File.bash_platform_path executable ^ ";" - val (_, compilation_time) = - elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) - val _ = Quickcheck.add_timing compilation_time current_result + val compilation_time = + Isabelle_System.bash_process cmd + |> Process_Result.check + |> Process_Result.timing_elapsed |> Time.toMilliseconds + handle ERROR msg => cat_error "Compilation with GHC failed" msg + val _ = Quickcheck.add_timing ("Haskell compilation", compilation_time) current_result fun haskell_string_of_bool v = if v then "True" else "False" - val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else () fun with_size genuine_only k = if k > size then (NONE, !current_result) else let val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k) val _ = current_size := k - val ((response, _), timing) = - elapsed_time ("execution of size " ^ string_of_int k) - (fn () => Isabelle_System.bash_output - (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ - string_of_int k)) - val _ = Quickcheck.add_timing timing current_result + val res = + Isabelle_System.bash_process + (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ + string_of_int k) + |> Process_Result.check + val response = Process_Result.out res + val timing = res |> Process_Result.timing_elapsed |> Time.toMilliseconds; + val _ = + Quickcheck.add_timing + ("execution of size " ^ string_of_int k, timing) current_result in - if response = "NONE\n" then with_size genuine_only (k + 1) + if response = "NONE" then with_size genuine_only (k + 1) else let val output_value = the_default "NONE" diff -r f84a93f1de2f -r 8b6fa865bac4 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Tue Feb 23 10:13:09 2021 +0100 @@ -574,7 +574,7 @@ (warning (case extract_known_atp_failure known_perl_failures output of SOME failure => string_of_atp_failure failure - | NONE => trim_line output); []))) () + | NONE => output); []))) () handle Timeout.TIMEOUT _ => [] fun find_remote_system name [] systems = diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/Admin/components.scala --- a/src/Pure/Admin/components.scala Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/Admin/components.scala Tue Feb 23 10:13:09 2021 +0100 @@ -279,9 +279,8 @@ } yield { progress.echo("Digesting remote " + entry.name) - Library.trim_line( - ssh.execute("cd " + ssh.bash_path(components_dir) + - "; sha1sum " + Bash.string(entry.name)).check.out) + ssh.execute("cd " + ssh.bash_path(components_dir) + + "; sha1sum " + Bash.string(entry.name)).check.out } write_components_sha1(read_components_sha1(lines)) } diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/General/exn.ML --- a/src/Pure/General/exn.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/General/exn.ML Tue Feb 23 10:13:09 2021 +0100 @@ -105,7 +105,7 @@ (* POSIX return code *) fun return_code exn rc = - if is_interrupt exn then (130: int) else rc; + if is_interrupt exn then 130 else rc; fun capture_exit rc f x = f x handle exn => exit (return_code exn rc); diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/General/file.ML Tue Feb 23 10:13:09 2021 +0100 @@ -48,10 +48,10 @@ val standard_path = Path.implode o Path.expand; val platform_path = ML_System.platform_path o standard_path; -val bash_path = Bash_Syntax.string o standard_path; -val bash_paths = Bash_Syntax.strings o map standard_path; +val bash_path = Bash.string o standard_path; +val bash_paths = Bash.strings o map standard_path; -val bash_platform_path = Bash_Syntax.string o platform_path; +val bash_platform_path = Bash.string o platform_path; (* full_path *) diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/ML/ml_system.ML --- a/src/Pure/ML/ml_system.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/ML/ml_system.ML Tue Feb 23 10:13:09 2021 +0100 @@ -11,7 +11,6 @@ val platform_is_windows: bool val platform_is_64: bool val platform_is_arm: bool - val platform_is_rosetta: unit -> bool val platform_path: string -> string val standard_path: string -> string end; @@ -25,12 +24,6 @@ val platform_is_64 = String.isPrefix "x86_64-" platform; val platform_is_arm = String.isPrefix "arm64-" platform; -fun platform_is_rosetta () = - (case OS.Process.getEnv "ISABELLE_APPLE_PLATFORM64" of - NONE => false - | SOME "" => false - | SOME apple_platform => apple_platform <> platform); - val platform_path = if platform_is_windows then fn path => diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/ROOT.ML Tue Feb 23 10:13:09 2021 +0100 @@ -79,7 +79,7 @@ ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; -ML_file "System/bash_syntax.ML"; +ML_file "System/bash.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; @@ -294,8 +294,7 @@ (*Isabelle system*) ML_file "PIDE/protocol_command.ML"; ML_file "System/scala.ML"; -ML_file "System/kill.ML"; -ML_file "System/bash.ML"; +ML_file "System/process_result.ML"; ML_file "System/isabelle_system.ML"; @@ -356,3 +355,4 @@ ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" + diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/ROOT.scala --- a/src/Pure/ROOT.scala Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/ROOT.scala Tue Feb 23 10:13:09 2021 +0100 @@ -21,4 +21,3 @@ val proper_string = Library.proper_string _ def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list) } - diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/System/bash.ML Tue Feb 23 10:13:09 2021 +0100 @@ -1,207 +1,35 @@ (* Title: Pure/System/bash.ML Author: Makarius -GNU bash processes, with propagation of interrupts -- POSIX version. +Syntax for GNU bash. *) signature BASH = sig val string: string -> string val strings: string list -> string - val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} end; -structure Bash: sig val terminate: int option -> unit end = -struct - -fun terminate NONE = () - | terminate (SOME pid) = - let - val kill = Kill.kill_group pid; - - fun multi_kill count s = - count = 0 orelse - (kill s; kill Kill.SIGNONE) andalso - (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); - val _ = - multi_kill 7 Kill.SIGINT andalso - multi_kill 3 Kill.SIGTERM andalso - multi_kill 1 Kill.SIGKILL; - in () end; - -end; - -if ML_System.platform_is_windows then ML -\ structure Bash: BASH = struct -open Bash; - -val string = Bash_Syntax.string; -val strings = Bash_Syntax.strings; - -val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => - let - datatype result = Wait | Signal | Result of int; - val result = Synchronized.var "bash_result" Wait; - - val id = serial_string (); - val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); - val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); - val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); - val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); - - fun cleanup_files () = - (try File.rm script_path; - try File.rm out_path; - try File.rm err_path; - try File.rm pid_path); - val _ = cleanup_files (); +fun string "" = "\"\"" + | string str = + str |> translate_string (fn ch => + let val c = ord ch in + (case ch of + "\t" => "$'\\t'" + | "\n" => "$'\\n'" + | "\f" => "$'\\f'" + | "\r" => "$'\\r'" + | _ => + if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse + exists_string (fn c => c = ch) "+,-./:_" then ch + else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'" + else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'" + else "\\" ^ ch) + end); - val system_thread = - Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => - Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => - let - val _ = File.write script_path script; - val bash_script = - "bash " ^ File.bash_path script_path ^ - " > " ^ File.bash_path out_path ^ - " 2> " ^ File.bash_path err_path; - val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; - val rc = - Windows.simpleExecute ("", - quote (ML_System.platform_path bash_process) ^ " " ^ - quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) - |> Windows.fromStatus |> SysWord.toInt; - val res = if rc = 130 orelse rc = 512 then Signal else Result rc; - in Synchronized.change result (K res) end - handle exn => - (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); - - fun read_pid 0 = NONE - | read_pid count = - (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of - NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) - | some => some); - - fun cleanup () = - (Isabelle_Thread.interrupt_unsynchronized system_thread; - cleanup_files ()); - in - let - val _ = - restore_attributes (fn () => - Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); - - val out = the_default "" (try File.read out_path); - val err = the_default "" (try File.read err_path); - val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); - val pid = read_pid 1; - val _ = cleanup (); - in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end - handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) - end); +val strings = space_implode " " o map string; end; -\ -else ML -\ -structure Bash: BASH = -struct - -open Bash; - -val string = Bash_Syntax.string; -val strings = Bash_Syntax.strings; - -val process_ml = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => - let - datatype result = Wait | Signal | Result of int; - val result = Synchronized.var "bash_result" Wait; - - val id = serial_string (); - val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); - val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); - val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); - val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); - - fun cleanup_files () = - (try File.rm script_path; - try File.rm out_path; - try File.rm err_path; - try File.rm pid_path); - val _ = cleanup_files (); - - val system_thread = - Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => - Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => - let - val _ = File.write script_path script; - val _ = getenv_strict "ISABELLE_BASH_PROCESS"; - val status = - OS.Process.system - ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^ - " bash " ^ File.bash_path script_path ^ - " > " ^ File.bash_path out_path ^ - " 2> " ^ File.bash_path err_path); - val res = - (case Posix.Process.fromStatus status of - Posix.Process.W_EXITED => Result 0 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) - | Posix.Process.W_SIGNALED s => - if s = Posix.Signal.int then Signal - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) - | Posix.Process.W_STOPPED s => - Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); - in Synchronized.change result (K res) end - handle exn => - (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); - - fun read_pid 0 = NONE - | read_pid count = - (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of - NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) - | some => some); - - fun cleanup () = - (Isabelle_Thread.interrupt_unsynchronized system_thread; - cleanup_files ()); - in - let - val _ = - restore_attributes (fn () => - Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); - - val out = the_default "" (try File.read out_path); - val err = the_default "" (try File.read err_path); - val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); - val pid = read_pid 1; - val _ = cleanup (); - in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end - handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) - end); - -fun process_scala script = - Scala.function_thread "bash_process" - ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script) - |> YXML.parse_body - |> - let open XML.Decode in - variant - [fn ([], []) => raise Exn.Interrupt, - fn ([], a) => error (YXML.string_of_body a), - fn ([a, b], c) => - let - val rc = int_atom a; - val pid = int_atom b; - val (out, err) = pair I I c |> apply2 YXML.string_of_body; - in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end] - end; - -fun process script = - if ML_System.platform_is_rosetta () then process_scala script else process_ml script; - -end; -\ \ No newline at end of file diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/System/bash.scala Tue Feb 23 10:13:09 2021 +0100 @@ -211,32 +211,24 @@ val here = Scala_Project.here def apply(script: String): String = { - val result = - Exn.capture { - val proc = process(script) - val res = proc.result() - (res, proc.pid) - } + val result = Exn.capture { Isabelle_System.bash(script) } val is_interrupt = result match { - case Exn.Res((res, _)) => res.rc == Exn.Interrupt.return_code + case Exn.Res(res) => res.rc == Exn.Interrupt.return_code case Exn.Exn(exn) => Exn.is_interrupt(exn) } - val encode: XML.Encode.T[Exn.Result[(Process_Result, String)]] = - { - import XML.Encode._ - val string = XML.Encode.string - variant(List( - { case _ if is_interrupt => (Nil, Nil) }, - { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) }, - { case Exn.Res((res, pid)) => - val out = Library.terminate_lines(res.out_lines) - val err = Library.terminate_lines(res.err_lines) - (List(int_atom(res.rc), pid), pair(string, string)(out, err)) })) + result match { + case _ if is_interrupt => "" + case Exn.Exn(exn) => Exn.message(exn) + case Exn.Res(res) => + (res.rc.toString :: + res.timing.elapsed.ms.toString :: + res.timing.cpu.ms.toString :: + res.out_lines.length.toString :: + res.out_lines ::: res.err_lines).mkString("\u0000") } - YXML.string_of_body(encode(result)) } } } diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/System/bash_syntax.ML --- a/src/Pure/System/bash_syntax.ML Fri Feb 19 11:52:34 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: Pure/System/bash_syntax.ML - Author: Makarius - -Syntax for GNU bash (see also Pure/System/bash.ML). -*) - -signature BASH_SYNTAX = -sig - val string: string -> string - val strings: string list -> string -end; - -structure Bash_Syntax: BASH_SYNTAX = -struct - -fun string "" = "\"\"" - | string str = - str |> translate_string (fn ch => - let val c = ord ch in - (case ch of - "\t" => "$'\\t'" - | "\n" => "$'\\n'" - | "\f" => "$'\\f'" - | "\r" => "$'\\r'" - | _ => - if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse - exists_string (fn c => c = ch) "+,-./:_" then ch - else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'" - else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'" - else "\\" ^ ch) - end); - -val strings = space_implode " " o map string; - -end; diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/System/isabelle_system.ML Tue Feb 23 10:13:09 2021 +0100 @@ -6,7 +6,7 @@ signature ISABELLE_SYSTEM = sig - val bash_output_check: string -> string + val bash_process: string -> Process_Result.T val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list @@ -28,29 +28,42 @@ (* bash *) -fun bash_output_check s = - (case Bash.process s of - {rc = 0, out, ...} => trim_line out - | {err, ...} => error (trim_line err)); +fun bash_process script = + Scala.function_thread "bash_process" + ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) + |> space_explode "\000" + |> (fn [] => raise Exn.Interrupt + | [err] => error err + | a :: b :: c :: d :: lines => + let + val rc = Value.parse_int a; + val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); + val (out_lines, err_lines) = chop (Value.parse_int d) lines; + in + Process_Result.make + {rc = rc, + out_lines = out_lines, + err_lines = err_lines, + timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} + end + | _ => raise Fail "Malformed Isabelle/Scala result"); + +val bash = bash_process #> Process_Result.print #> Process_Result.rc; fun bash_output s = let - val {out, err, rc, ...} = Bash.process s; - val _ = warning (trim_line err); - in (out, rc) end; - -fun bash s = - let - val (out, rc) = bash_output s; - val _ = writeln (trim_line out); - in rc end; + val res = bash_process s; + val _ = warning (Process_Result.err res); + in (Process_Result.out res, Process_Result.rc res) end; (* bash functions *) fun bash_functions () = - bash_output_check "declare -Fx" - |> split_lines |> map_filter (space_explode " " #> try List.last); + bash_process "declare -Fx" + |> Process_Result.check + |> Process_Result.out_lines + |> map_filter (space_explode " " #> try List.last); fun check_bash_function ctxt arg = Completion.check_entity Markup.bash_functionN @@ -126,9 +139,12 @@ fun download url = with_tmp_file "download" "" (fn path => - ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path) - |> Bash.process - |> (fn {rc = 0, ...} => File.read path - | {err, ...} => cat_error ("Failed to download " ^ quote url) err)); + let + val s = "curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path; + val res = bash_process s; + in + if Process_Result.ok res then File.read path + else cat_error ("Failed to download " ^ quote url) (Process_Result.err res) + end); end; diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/System/kill.ML --- a/src/Pure/System/kill.ML Fri Feb 19 11:52:34 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -(* Title: Pure/System/kill.ML - Author: Makarius - -Kill external process group. -*) - -signature KILL = -sig - type signal - val SIGNONE: signal - val SIGINT: signal - val SIGTERM: signal - val SIGKILL: signal - val kill_group: int -> signal -> bool -end; - -if ML_System.platform_is_windows then ML -\ -structure Kill: KILL = -struct - -type signal = string; - -val SIGNONE = "0"; -val SIGINT = "INT"; -val SIGTERM = "TERM"; -val SIGKILL = "KILL"; - -fun kill_group pid s = - let - val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"; - val arg = "kill -" ^ s ^ " -" ^ string_of_int pid; - in - OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg)) - handle OS.SysErr _ => false - end; - -end; -\ -else ML -\ -structure Kill: KILL = -struct - -type signal = Posix.Signal.signal; - -val SIGNONE = Posix.Signal.fromWord 0w0; -val SIGINT = Posix.Signal.int; -val SIGTERM = Posix.Signal.term; -val SIGKILL = Posix.Signal.kill; - -fun kill_group pid s = - let - val arg = Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)); - val _ = Posix.Process.kill (arg, s); - in true end handle OS.SysErr _ => false; - -end; -\ diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/System/message_channel.ML --- a/src/Pure/System/message_channel.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/System/message_channel.ML Tue Feb 23 10:13:09 2021 +0100 @@ -19,7 +19,7 @@ (* message *) -datatype message = Message of XML.body; +datatype message = Message of {body: XML.body, flush: bool}; fun body_size body = fold (YXML.traverse (Integer.add o size)) body 0; @@ -29,10 +29,7 @@ let val robust_props = map (apply2 YXML.embed_controls) raw_props; val header = XML.Elem ((name, robust_props), []); - in Message (chunk [header] @ chunk body) end; - -fun output_message stream (Message body) = - fold (YXML.traverse (fn s => fn () => File.output stream s)) body (); + in Message {body = chunk [header] @ chunk body, flush = name = Markup.protocolN} end; (* channel *) @@ -51,7 +48,11 @@ [] => (Byte_Message.flush stream; continue NONE) | msgs => received timeout msgs) and received _ (NONE :: _) = Byte_Message.flush stream - | received _ (SOME msg :: rest) = (output_message stream msg; received flush_timeout rest) + | received _ (SOME (Message {body, flush}) :: rest) = + let + val _ = fold (YXML.traverse (fn s => fn () => File.output stream s)) body (); + val timeout = if flush then (Byte_Message.flush stream; NONE) else flush_timeout; + in received timeout rest end | received timeout [] = continue timeout; in fn () => continue NONE end; diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/System/process_result.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/process_result.ML Tue Feb 23 10:13:09 2021 +0100 @@ -0,0 +1,62 @@ +(* Title: Pure/System/process_result.scala + Author: Makarius + +Result of system process. +*) + +signature PROCESS_RESULT = +sig + type T + val make: + {rc: int, + out_lines: string list, + err_lines: string list, + timing: Timing.timing} -> T + val rc: T -> int + val out_lines: T -> string list + val err_lines: T -> string list + val timing: T -> Timing.timing + val timing_elapsed: T -> Time.time + val out: T -> string + val err: T -> string + val ok: T -> bool + val check: T -> T + val print: T -> T +end; + +structure Process_Result: PROCESS_RESULT = +struct + +abstype T = + Process_Result of + {rc: int, + out_lines: string list, + err_lines: string list, + timing: Timing.timing} +with + +val make = Process_Result; +fun rep (Process_Result args) = args; + +val rc = #rc o rep; +val out_lines = #out_lines o rep; +val err_lines = #err_lines o rep; + +val timing = #timing o rep; +val timing_elapsed = #elapsed o timing; + +end; + +val out = trim_line o cat_lines o out_lines; +val err = trim_line o cat_lines o err_lines; + +fun ok result = rc result = 0; + +fun check result = if ok result then result else error (err result); + +fun print result = + (warning (err result); + writeln (out result); + make {rc = rc result, out_lines = [], err_lines = [], timing = timing result}); + +end; diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/System/process_result.scala Tue Feb 23 10:13:09 2021 +0100 @@ -38,8 +38,8 @@ err_lines: List[String] = Nil, timing: Timing = Timing.zero) { - def out: String = cat_lines(out_lines) - def err: String = cat_lines(err_lines) + def out: String = Library.trim_line(cat_lines(out_lines)) + def err: String = Library.trim_line(cat_lines(err_lines)) def output(outs: List[String]): Process_Result = copy(out_lines = out_lines ::: outs.flatMap(split_lines)) diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/Thy/presentation.scala Tue Feb 23 10:13:09 2021 +0100 @@ -680,7 +680,7 @@ if (!result.ok) { val message = Exn.cat_message( - Library.trim_line(result.err), + result.err, cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)), "Failed to build document " + quote(doc.name)) throw new Build_Error(log_lines, message) diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/Tools/doc.scala --- a/src/Pure/Tools/doc.scala Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/Tools/doc.scala Tue Feb 23 10:13:09 2021 +0100 @@ -22,7 +22,7 @@ dir <- dirs() catalog = dir + Path.basic("Contents") if catalog.is_file - line <- split_lines(Library.trim_line(File.read(catalog))) + line <- Library.trim_split_lines(File.read(catalog)) } yield (dir, line) sealed abstract class Entry diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/Tools/generated_files.ML Tue Feb 23 10:13:09 2021 +0100 @@ -332,7 +332,9 @@ (* execute compiler -- auxiliary *) fun execute dir title compile = - Isabelle_System.bash_output_check ("cd " ^ File.bash_path dir ^ " && " ^ compile) + Isabelle_System.bash_process ("cd " ^ File.bash_path dir ^ " && " ^ compile) + |> Process_Result.check + |> Process_Result.out handle ERROR msg => let val (s, pos) = Input.source_content title in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end; diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/Tools/ghc.ML --- a/src/Pure/Tools/ghc.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/Tools/ghc.ML Tue Feb 23 10:13:09 2021 +0100 @@ -83,9 +83,11 @@ let val template_path = dir + (Path.basic name |> Path.ext "hsfiles"); val _ = File.write template_path (project_template {depends = depends, modules = modules}); - val {rc, err, ...} = - Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ - " --bare " ^ File.bash_platform_path template_path); - in if rc = 0 then () else error err end; + val _ = + Isabelle_System.bash_process + ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ + " --bare " ^ File.bash_platform_path template_path) + |> Process_Result.check; + in () end; end; diff -r f84a93f1de2f -r 8b6fa865bac4 src/Pure/Tools/jedit.ML --- a/src/Pure/Tools/jedit.ML Fri Feb 19 11:52:34 2021 +0100 +++ b/src/Pure/Tools/jedit.ML Tue Feb 23 10:13:09 2021 +0100 @@ -35,10 +35,13 @@ val xml_file = XML.parse o File.read; fun xml_resource name = - let val script = "unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name in - (case Isabelle_System.bash_output script of - (txt, 0) => XML.parse txt - | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)) + let + val res = + Isabelle_System.bash_process ("unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name); + val rc = Process_Result.rc res; + in + res |> Process_Result.check |> Process_Result.out |> XML.parse + handle ERROR _ => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc) end;