# HG changeset patch # User hoelzl # Date 1475244518 -7200 # Node ID 17a20ca86d62037d2b31bd8f49d1673ba07a1680 # Parent 041cda506fb22860dd10263f930e204ea0188509 HOL-Probability: more about probability, prepare for Markov processes in the AFP diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Binary_Product_Measure.thy --- a/src/HOL/Analysis/Binary_Product_Measure.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy Fri Sep 30 16:08:38 2016 +0200 @@ -686,6 +686,53 @@ show "a \ A" and "b \ B" by auto qed +lemma sets_pair_eq: + assumes Ea: "Ea \ Pow (space A)" "sets A = sigma_sets (space A) Ea" + and Ca: "countable Ca" "Ca \ Ea" "\Ca = space A" + and Eb: "Eb \ Pow (space B)" "sets B = sigma_sets (space B) Eb" + and Cb: "countable Cb" "Cb \ Eb" "\Cb = space B" + shows "sets (A \\<^sub>M B) = sets (sigma (space A \ space B) { a \ b | a b. a \ Ea \ b \ Eb })" + (is "_ = sets (sigma ?\ ?E)") +proof + show "sets (sigma ?\ ?E) \ sets (A \\<^sub>M B)" + using Ea(1) Eb(1) by (subst sigma_le_sets) (auto simp: Ea(2) Eb(2)) + have "?E \ Pow ?\" + using Ea(1) Eb(1) by auto + then have E: "a \ Ea \ b \ Eb \ a \ b \ sets (sigma ?\ ?E)" for a b + by auto + have "sets (A \\<^sub>M B) \ sets (Sup {vimage_algebra ?\ fst A, vimage_algebra ?\ snd B})" + unfolding sets_pair_eq_sets_fst_snd .. + also have "vimage_algebra ?\ fst A = vimage_algebra ?\ fst (sigma (space A) Ea)" + by (intro vimage_algebra_cong[OF refl refl]) (simp add: Ea) + also have "\ = sigma ?\ {fst -` A \ ?\ |A. A \ Ea}" + by (intro Ea vimage_algebra_sigma) auto + also have "vimage_algebra ?\ snd B = vimage_algebra ?\ snd (sigma (space B) Eb)" + by (intro vimage_algebra_cong[OF refl refl]) (simp add: Eb) + also have "\ = sigma ?\ {snd -` A \ ?\ |A. A \ Eb}" + by (intro Eb vimage_algebra_sigma) auto + also have "{sigma ?\ {fst -` Aa \ ?\ |Aa. Aa \ Ea}, sigma ?\ {snd -` Aa \ ?\ |Aa. Aa \ Eb}} = + sigma ?\ ` {{fst -` Aa \ ?\ |Aa. Aa \ Ea}, {snd -` Aa \ ?\ |Aa. Aa \ Eb}}" + by auto + also have "sets (SUP S:{{fst -` Aa \ ?\ |Aa. Aa \ Ea}, {snd -` Aa \ ?\ |Aa. Aa \ Eb}}. sigma ?\ S) = + sets (sigma ?\ (\{{fst -` Aa \ ?\ |Aa. Aa \ Ea}, {snd -` Aa \ ?\ |Aa. Aa \ Eb}}))" + using Ea(1) Eb(1) by (intro sets_Sup_sigma) auto + also have "\ \ sets (sigma ?\ ?E)" + proof (subst sigma_le_sets, safe intro!: space_in_measure_of) + fix a assume "a \ Ea" + then have "fst -` a \ ?\ = (\b\Cb. a \ b)" + using Cb(3)[symmetric] Ea(1) by auto + then show "fst -` a \ ?\ \ sets (sigma ?\ ?E)" + using Cb \a \ Ea\ by (auto intro!: sets.countable_UN' E) + next + fix b assume "b \ Eb" + then have "snd -` b \ ?\ = (\a\Ca. a \ b)" + using Ca(3)[symmetric] Eb(1) by auto + then show "snd -` b \ ?\ \ sets (sigma ?\ ?E)" + using Ca \b \ Eb\ by (auto intro!: sets.countable_UN' E) + qed + finally show "sets (A \\<^sub>M B) \ sets (sigma ?\ ?E)" . +qed + lemma borel_prod: "(borel \\<^sub>M borel) = (borel :: ('a::second_countable_topology \ 'b::second_countable_topology) measure)" (is "?P = ?B") diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Bochner_Integration.thy --- a/src/HOL/Analysis/Bochner_Integration.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Bochner_Integration.thy Fri Sep 30 16:08:38 2016 +0200 @@ -951,6 +951,10 @@ unfolding integrable.simps by (intro has_bochner_integral_cong_AE arg_cong[where f=Ex] ext) +lemma integrable_cong_AE_imp: + "integrable M g \ f \ borel_measurable M \ (AE x in M. g x = f x) \ integrable M f" + using integrable_cong_AE[of f M g] by (auto simp: eq_commute) + lemma integral_cong: "M = N \ (\x. x \ space N \ f x = g x) \ integral\<^sup>L M f = integral\<^sup>L N g" by (simp cong: has_bochner_integral_cong cong del: if_weak_cong add: lebesgue_integral_def) @@ -1682,6 +1686,16 @@ finally show ?thesis . qed +lemma nn_integral_eq_integrable: + assumes f: "f \ M \\<^sub>M borel" "AE x in M. 0 \ f x" and "0 \ x" + shows "(\\<^sup>+x. f x \M) = ennreal x \ (integrable M f \ integral\<^sup>L M f = x)" +proof (safe intro!: nn_integral_eq_integral assms) + assume *: "(\\<^sup>+x. f x \M) = ennreal x" + with integrableI_nn_integral_finite[OF f this] nn_integral_eq_integral[of M f, OF _ f(2)] + show "integrable M f" "integral\<^sup>L M f = x" + by (simp_all add: * assms integral_nonneg_AE) +qed + lemma fixes f :: "_ \ _ \ 'a :: {banach, second_countable_topology}" assumes integrable[measurable]: "\i. integrable M (f i)" @@ -2227,6 +2241,27 @@ shows "integrable (count_space UNIV) f \ integral\<^sup>L (count_space UNIV) f = (\x. f x)" using sums_integral_count_space_nat by (rule sums_unique) +lemma integrable_bij_count_space: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + assumes g: "bij_betw g A B" + shows "integrable (count_space A) (\x. f (g x)) \ integrable (count_space B) f" + unfolding integrable_iff_bounded by (subst nn_integral_bij_count_space[OF g]) auto + +lemma integral_bij_count_space: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + assumes g: "bij_betw g A B" + shows "integral\<^sup>L (count_space A) (\x. f (g x)) = integral\<^sup>L (count_space B) f" + using g[THEN bij_betw_imp_funcset] + apply (subst distr_bij_count_space[OF g, symmetric]) + apply (intro integral_distr[symmetric]) + apply auto + done + +lemma has_bochner_integral_count_space_nat: + fixes f :: "nat \ _::{banach,second_countable_topology}" + shows "has_bochner_integral (count_space UNIV) f x \ f sums x" + unfolding has_bochner_integral_iff by (auto intro!: sums_integral_count_space_nat) + subsection \Point measure\ lemma lebesgue_integral_point_measure_finite: diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Borel_Space.thy --- a/src/HOL/Analysis/Borel_Space.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Borel_Space.thy Fri Sep 30 16:08:38 2016 +0200 @@ -1500,6 +1500,9 @@ apply auto done +lemma measurable_of_bool[measurable]: "of_bool \ count_space UNIV \\<^sub>M borel" + by simp + subsection "Borel space on the extended reals" lemma borel_measurable_ereal[measurable (raw)]: @@ -1909,6 +1912,56 @@ shows "mono f \ f \ borel_measurable borel" using borel_measurable_mono_on_fnc[of f UNIV] by (simp add: mono_def mono_on_def) +lemma measurable_bdd_below_real[measurable (raw)]: + fixes F :: "'a \ 'i \ real" + assumes [simp]: "countable I" and [measurable]: "\i. i \ I \ F i \ M \\<^sub>M borel" + shows "Measurable.pred M (\x. bdd_below ((\i. F i x)`I))" +proof (subst measurable_cong) + show "bdd_below ((\i. F i x)`I) \ (\q\\. \i\I. q \ F i x)" for x + by (auto simp: bdd_below_def intro!: bexI[of _ "of_int (floor _)"] intro: order_trans of_int_floor_le) + show "Measurable.pred M (\w. \q\\. \i\I. q \ F i w)" + using countable_int by measurable +qed + +lemma borel_measurable_cINF_real[measurable (raw)]: + fixes F :: "_ \ _ \ real" + assumes [simp]: "countable I" + assumes F[measurable]: "\i. i \ I \ F i \ borel_measurable M" + shows "(\x. INF i:I. F i x) \ borel_measurable M" +proof (rule measurable_piecewise_restrict) + let ?\ = "{x\space M. bdd_below ((\i. F i x)`I)}" + show "countable {?\, - ?\}" "space M \ \{?\, - ?\}" "\X. X \ {?\, - ?\} \ X \ space M \ sets M" + by auto + fix X assume "X \ {?\, - ?\}" then show "(\x. INF i:I. F i x) \ borel_measurable (restrict_space M X)" + proof safe + show "(\x. INF i:I. F i x) \ borel_measurable (restrict_space M ?\)" + by (intro borel_measurable_cINF measurable_restrict_space1 F) + (auto simp: space_restrict_space) + show "(\x. INF i:I. F i x) \ borel_measurable (restrict_space M (-?\))" + proof (subst measurable_cong) + fix x assume "x \ space (restrict_space M (-?\))" + then have "\ (\i\I. - F i x \ y)" for y + by (auto simp: space_restrict_space bdd_above_def bdd_above_uminus[symmetric]) + then show "(INF i:I. F i x) = - (THE x. False)" + by (auto simp: space_restrict_space Inf_real_def Sup_real_def Least_def simp del: Set.ball_simps(10)) + qed simp + qed +qed + +lemma borel_Ici: "borel = sigma UNIV (range (\x::real. {x ..}))" +proof (safe intro!: borel_eq_sigmaI1[OF borel_Iio]) + fix x :: real + have eq: "{.. sets (sigma UNIV (range atLeast))" + unfolding eq by (intro sets.compl_sets) auto +qed auto + +lemma borel_measurable_pred_less[measurable (raw)]: + fixes f :: "'a \ 'b::{second_countable_topology, linorder_topology}" + shows "f \ borel_measurable M \ g \ borel_measurable M \ Measurable.pred M (\w. f w < g w)" + unfolding Measurable.pred_def by (rule borel_measurable_less) + no_notation eucl_less (infix "c. (f has_real_derivative c) F) = (\D. (f has_derivative D) F)" by (metis has_field_derivative_def has_real_derivative) +lemma has_vector_derivative_cong_ev: + assumes *: "eventually (\x. x \ s \ f x = g x) (nhds x)" "f x = g x" + shows "(f has_vector_derivative f') (at x within s) = (g has_vector_derivative f') (at x within s)" + unfolding has_vector_derivative_def has_derivative_def + using * + apply (cases "at x within s \ bot") + apply (intro refl conj_cong filterlim_cong) + apply (auto simp: netlimit_within eventually_at_filter elim: eventually_mono) + done + definition deriv :: "('a \ 'a::real_normed_field) \ 'a \ 'a" where "deriv f x \ SOME D. DERIV f x :> D" diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Finite_Product_Measure.thy --- a/src/HOL/Analysis/Finite_Product_Measure.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy Fri Sep 30 16:08:38 2016 +0200 @@ -1196,4 +1196,14 @@ by (subst emeasure_distr) (auto simp: measurable_pair_iff) qed simp +lemma infprod_in_sets[intro]: + fixes E :: "nat \ 'a set" assumes E: "\i. E i \ sets (M i)" + shows "Pi UNIV E \ sets (\\<^sub>M i\UNIV::nat set. M i)" +proof - + have "Pi UNIV E = (\i. prod_emb UNIV M {..i} (\\<^sub>E j\{..i}. E j))" + using E E[THEN sets.sets_into_space] + by (auto simp: prod_emb_def Pi_iff extensional_def) + with E show ?thesis by auto +qed + end diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Lebesgue_Measure.thy --- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy Fri Sep 30 16:08:38 2016 +0200 @@ -11,6 +11,24 @@ imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests Regularity begin +lemma measure_eqI_lessThan: + fixes M N :: "real measure" + assumes sets: "sets M = sets borel" "sets N = sets borel" + assumes fin: "\x. emeasure M {x <..} < \" + assumes "\x. emeasure M {x <..} = emeasure N {x <..}" + shows "M = N" +proof (rule measure_eqI_generator_eq_countable) + let ?LT = "\a::real. {a <..}" let ?E = "range ?LT" + show "Int_stable ?E" + by (auto simp: Int_stable_def lessThan_Int_lessThan) + + show "?E \ Pow UNIV" "sets M = sigma_sets UNIV ?E" "sets N = sigma_sets UNIV ?E" + unfolding sets borel_Ioi by auto + + show "?LT`Rats \ ?E" "(\i\Rats. ?LT i) = UNIV" "\a. a \ ?LT`Rats \ emeasure M a \ \" + using fin by (auto intro: Rats_no_bot_less simp: less_top) +qed (auto intro: assms countable_rat) + subsection \Every right continuous and nondecreasing function gives rise to a measure\ definition interval_measure :: "(real \ real) \ real measure" where diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Measurable.thy --- a/src/HOL/Analysis/Measurable.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Measurable.thy Fri Sep 30 16:08:38 2016 +0200 @@ -618,6 +618,24 @@ shows "Measurable.pred M ((R ^^ n) T)" by (induct n) (auto intro: assms) +lemma measurable_compose_countable_restrict: + assumes P: "countable {i. P i}" + and f: "f \ M \\<^sub>M count_space UNIV" + and Q: "\i. P i \ pred M (Q i)" + shows "pred M (\x. P (f x) \ Q (f x) x)" +proof - + have P_f: "{x \ space M. P (f x)} \ sets M" + unfolding pred_def[symmetric] by (rule measurable_compose[OF f]) simp + have "pred (restrict_space M {x\space M. P (f x)}) (\x. Q (f x) x)" + proof (rule measurable_compose_countable'[where g=f, OF _ _ P]) + show "f \ restrict_space M {x\space M. P (f x)} \\<^sub>M count_space {i. P i}" + by (rule measurable_count_space_extend[OF subset_UNIV]) + (auto simp: space_restrict_space intro!: measurable_restrict_space1 f) + qed (auto intro!: measurable_restrict_space1 Q) + then show ?thesis + unfolding pred_restrict_space[OF P_f] by (simp cong: measurable_cong) +qed + hide_const (open) pred end diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Measure_Space.thy --- a/src/HOL/Analysis/Measure_Space.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Measure_Space.thy Fri Sep 30 16:08:38 2016 +0200 @@ -838,6 +838,38 @@ qed qed +lemma space_empty: "space M = {} \ M = count_space {}" + by (rule measure_eqI) (simp_all add: space_empty_iff) + +lemma measure_eqI_generator_eq_countable: + fixes M N :: "'a measure" and E :: "'a set set" and A :: "'a set set" + assumes E: "Int_stable E" "E \ Pow \" "\X. X \ E \ emeasure M X = emeasure N X" + and sets: "sets M = sigma_sets \ E" "sets N = sigma_sets \ E" + and A: "A \ E" "(\A) = \" "countable A" "\a. a \ A \ emeasure M a \ \" + shows "M = N" +proof cases + assume "\ = {}" + have *: "sigma_sets \ E = sets (sigma \ E)" + using E(2) by simp + have "space M = \" "space N = \" + using sets E(2) unfolding * by (auto dest: sets_eq_imp_space_eq simp del: sets_measure_of) + then show "M = N" + unfolding \\ = {}\ by (auto dest: space_empty) +next + assume "\ \ {}" with \\A = \\ have "A \ {}" by auto + from this \countable A\ have rng: "range (from_nat_into A) = A" + by (rule range_from_nat_into) + show "M = N" + proof (rule measure_eqI_generator_eq[OF E sets]) + show "range (from_nat_into A) \ E" + unfolding rng using \A \ E\ . + show "(\i. from_nat_into A i) = \" + unfolding rng using \\A = \\ . + show "emeasure M (from_nat_into A i) \ \" for i + using rng by (intro A) auto + qed +qed + lemma measure_of_of_measure: "measure_of (space M) (sets M) (emeasure M) = M" proof (intro measure_eqI emeasure_measure_of_sigma) show "sigma_algebra (space M) (sets M)" .. @@ -1097,6 +1129,9 @@ "(\x. x \ space M \ P x \ Q x) \ (AE x in M. P x) \ (AE x in M. Q x)" by auto +lemma AE_cong_strong: "M = N \ (\x. x \ space N =simp=> P x = Q x) \ (AE x in M. P x) \ (AE x in N. Q x)" + by (auto simp: simp_implies_def) + lemma AE_all_countable: "(AE x in M. \i. P i x) \ (\i::'i::countable. AE x in M. P i x)" proof @@ -2135,9 +2170,6 @@ qed simp qed (simp add: emeasure_notin_sets) -lemma space_empty: "space M = {} \ M = count_space {}" - by (rule measure_eqI) (simp_all add: space_empty_iff) - lemma null_sets_count_space: "null_sets (count_space A) = { {} }" unfolding null_sets_def by (auto simp add: emeasure_count_space_eq_0) diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Fri Sep 30 16:08:38 2016 +0200 @@ -1692,6 +1692,16 @@ by (simp add: ** nn_integral_suminf from_nat_into) qed +lemma of_bool_Bex_eq_nn_integral: + assumes unique: "\x y. x \ X \ y \ X \ P x \ P y \ x = y" + shows "of_bool (\y\X. P y) = (\\<^sup>+y. of_bool (P y) \count_space X)" +proof cases + assume "\y\X. P y" + then obtain y where "P y" "y \ X" by auto + then show ?thesis + by (subst nn_integral_count_space'[where A="{y}"]) (auto dest: unique) +qed (auto cong: nn_integral_cong_simp) + lemma emeasure_UN_countable: assumes sets[measurable]: "\i. i \ I \ X i \ sets M" and I[simp]: "countable I" assumes disj: "disjoint_family_on X I" diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Analysis/Sigma_Algebra.thy --- a/src/HOL/Analysis/Sigma_Algebra.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Analysis/Sigma_Algebra.thy Fri Sep 30 16:08:38 2016 +0200 @@ -1244,6 +1244,10 @@ lemma (in algebra) Int_stable: "Int_stable M" unfolding Int_stable_def by auto +lemma Int_stableI_image: + "(\i j. i \ I \ j \ I \ \k\I. A i \ A j = A k) \ Int_stable (A ` I)" + by (auto simp: Int_stable_def image_def) + lemma Int_stableI: "(\a b. a \ A \ b \ A \ a \ b \ A) \ Int_stable A" unfolding Int_stable_def by auto @@ -1574,6 +1578,9 @@ using assms by(simp_all add: sets_measure_of_conv space_measure_of_conv) +lemma space_in_measure_of[simp]: "\ \ sets (measure_of \ M \)" + by (subst sets_measure_of_conv) (auto simp: sigma_sets_top) + lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \ M \) = M" using space_closed by (auto intro!: sigma_sets_eq) @@ -2259,4 +2266,7 @@ by (rule measurable_restrict_countable[OF X]) (auto simp: eq[symmetric] space_restrict_space cong: measurable_cong' intro: f measurable_restrict_space1) +lemma measurable_count_space_extend: "A \ B \ f \ space M \ A \ f \ M \\<^sub>M count_space B \ f \ M \\<^sub>M count_space A" + by (auto simp: measurable_def) + end diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Library/Countable_Set.thy --- a/src/HOL/Library/Countable_Set.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Library/Countable_Set.thy Fri Sep 30 16:08:38 2016 +0200 @@ -284,6 +284,9 @@ lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\bool))" by (simp add: Collect_finite_eq_lists) +lemma countable_int: "countable \" + unfolding Ints_def by auto + lemma countable_rat: "countable \" unfolding Rats_def by auto diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Library/Extended_Nonnegative_Real.thy --- a/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Sep 30 16:08:38 2016 +0200 @@ -220,6 +220,11 @@ shows "summable f \ finite I \ \m\- I. 0 \ f m \ setsum f I \ suminf f" by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto +lemma suminf_eq_SUP_real: + assumes X: "summable X" "\i. 0 \ X i" shows "suminf X = (SUP i. \nDefining the extended non-negative reals\ text \Basic definitions and type class setup\ diff -r 041cda506fb2 -r 17a20ca86d62 src/HOL/Probability/Giry_Monad.thy --- a/src/HOL/Probability/Giry_Monad.thy Mon Oct 03 14:09:26 2016 +0100 +++ b/src/HOL/Probability/Giry_Monad.thy Fri Sep 30 16:08:38 2016 +0200 @@ -28,6 +28,9 @@ show "subprob_space M" by standard fact+ qed +lemma (in subprob_space) emeasure_subprob_space_less_top: "emeasure M A \ top" + using emeasure_finite[of A] . + lemma prob_space_imp_subprob_space: "prob_space M \ subprob_space M" by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty) @@ -245,6 +248,43 @@ by (auto dest: subprob_space_kernel sets_kernel) qed +lemma measurable_subprob_algebra_generated: + assumes eq: "sets N = sigma_sets \ G" and "Int_stable G" "G \ Pow \