fixed document generation for HOL-Probability
authorhoelzl
Mon May 19 13:44:13 2014 +0200 (2014-05-19)
changeset 569948d5e5ec1cac3
parent 56993 e5366291d6aa
child 56995 61855ade6c7e
fixed document generation for HOL-Probability
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/document/root.tex
src/HOL/Probability/ex/Dining_Cryptographers.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Mon May 19 12:04:45 2014 +0200
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Mon May 19 13:44:13 2014 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  lemma rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
     1.5    by auto
     1.6  
     1.7 -section "Binary products"
     1.8 +subsection "Binary products"
     1.9  
    1.10  definition pair_measure (infixr "\<Otimes>\<^sub>M" 80) where
    1.11    "A \<Otimes>\<^sub>M B = measure_of (space A \<times> space B)
    1.12 @@ -480,7 +480,7 @@
    1.13      done
    1.14  qed
    1.15  
    1.16 -section "Fubinis theorem"
    1.17 +subsection "Fubinis theorem"
    1.18  
    1.19  lemma measurable_compose_Pair1:
    1.20    "x \<in> space M1 \<Longrightarrow> g \<in> measurable (M1 \<Otimes>\<^sub>M M2) L \<Longrightarrow> (\<lambda>y. g (x, y)) \<in> measurable M2 L"
    1.21 @@ -557,7 +557,7 @@
    1.22    shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M2) \<partial>M1)"
    1.23    unfolding positive_integral_snd[OF assms] M2.positive_integral_fst[OF assms] ..
    1.24  
    1.25 -section {* Products on counting spaces, densities and distributions *}
    1.26 +subsection {* Products on counting spaces, densities and distributions *}
    1.27  
    1.28  lemma sigma_sets_pair_measure_generator_finite:
    1.29    assumes "finite A" and "finite B"
     2.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Mon May 19 12:04:45 2014 +0200
     2.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Mon May 19 13:44:13 2014 +0200
     2.3 @@ -1519,7 +1519,7 @@
     2.4      integral\<^sup>L M f \<le> integral\<^sup>L M g"
     2.5    by (intro integral_mono_AE) auto
     2.6  
     2.7 -section {* Measure spaces with an associated density *}
     2.8 +subsection {* Measure spaces with an associated density *}
     2.9  
    2.10  lemma integrable_density:
    2.11    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and g :: "'a \<Rightarrow> real"
    2.12 @@ -1673,7 +1673,7 @@
    2.13      has_bochner_integral M (\<lambda>x. f (g x)) x \<Longrightarrow> has_bochner_integral (distr M N g) f x"
    2.14    by (simp add: has_bochner_integral_iff integrable_distr_eq integral_distr)
    2.15  
    2.16 -section {* Lebesgue integration on @{const count_space} *}
    2.17 +subsection {* Lebesgue integration on @{const count_space} *}
    2.18  
    2.19  lemma integrable_count_space:
    2.20    fixes f :: "'a \<Rightarrow> 'b::{banach,second_countable_topology}"
    2.21 @@ -1703,7 +1703,7 @@
    2.22    by (subst lebesgue_integral_count_space_finite_support)
    2.23       (auto intro!: setsum_mono_zero_cong_left)
    2.24  
    2.25 -section {* Point measure *}
    2.26 +subsection {* Point measure *}
    2.27  
    2.28  lemma lebesgue_integral_point_measure_finite:
    2.29    fixes g :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    2.30 @@ -1720,7 +1720,7 @@
    2.31    apply (auto simp: AE_count_space integrable_count_space)
    2.32    done
    2.33  
    2.34 -subsection {* Legacy lemmas for the real-valued Lebesgue integral\<^sup>L *}
    2.35 +subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
    2.36  
    2.37  lemma real_lebesgue_integral_def:
    2.38    assumes f: "integrable M f"
    2.39 @@ -2080,7 +2080,7 @@
    2.40  qed
    2.41  
    2.42  
    2.43 -section "Lebesgue integration on countable spaces"
    2.44 +subsection {* Lebesgue integration on countable spaces *}
    2.45  
    2.46  lemma integral_on_countable:
    2.47    fixes f :: "real \<Rightarrow> real"
     3.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon May 19 12:04:45 2014 +0200
     3.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon May 19 13:44:13 2014 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4    "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
     3.5  begin
     3.6  
     3.7 -section "Generic Borel spaces"
     3.8 +subsection {* Generic Borel spaces *}
     3.9  
    3.10  definition borel :: "'a::topological_space measure" where
    3.11    "borel = sigma UNIV {S. open S}"
    3.12 @@ -213,7 +213,7 @@
    3.13      unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
    3.14  qed
    3.15  
    3.16 -section "Borel spaces on euclidean spaces"
    3.17 +subsection {* Borel spaces on euclidean spaces *}
    3.18  
    3.19  lemma borel_measurable_inner[measurable (raw)]:
    3.20    fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_inner}"
    3.21 @@ -1140,7 +1140,7 @@
    3.22    shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
    3.23    unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
    3.24  
    3.25 -section "LIMSEQ is borel measurable"
    3.26 +subsection {* LIMSEQ is borel measurable *}
    3.27  
    3.28  lemma borel_measurable_LIMSEQ:
    3.29    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"
     4.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon May 19 12:04:45 2014 +0200
     4.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon May 19 13:44:13 2014 +0200
     4.3 @@ -45,7 +45,7 @@
     4.4                       SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
     4.5  qed
     4.6  
     4.7 -subsection {* Measure Spaces *}
     4.8 +subsection {* Characterizations of Measures *}
     4.9  
    4.10  definition subadditive where "subadditive M f \<longleftrightarrow>
    4.11    (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
    4.12 @@ -54,9 +54,6 @@
    4.13    (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
    4.14      (f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))"
    4.15  
    4.16 -definition lambda_system where "lambda_system \<Omega> M f = {l \<in> M.
    4.17 -  \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
    4.18 -
    4.19  definition outer_measure_space where "outer_measure_space M f \<longleftrightarrow>
    4.20    positive M f \<and> increasing M f \<and> countably_subadditive M f"
    4.21  
    4.22 @@ -67,7 +64,10 @@
    4.23    "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
    4.24    by (auto simp add: subadditive_def)
    4.25  
    4.26 -subsection {* Lambda Systems *}
    4.27 +subsubsection {* Lambda Systems *}
    4.28 +
    4.29 +definition lambda_system where "lambda_system \<Omega> M f = {l \<in> M.
    4.30 +  \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
    4.31  
    4.32  lemma (in algebra) lambda_system_eq:
    4.33    shows "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}"
    4.34 @@ -643,6 +643,8 @@
    4.35    by (simp add: measure_space_def positive_def countably_additive_def)
    4.36       blast
    4.37  
    4.38 +subsection {* Caratheodory's theorem *}
    4.39 +
    4.40  theorem (in ring_of_sets) caratheodory':
    4.41    assumes posf: "positive M f" and ca: "countably_additive M f"
    4.42    shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
    4.43 @@ -670,8 +672,6 @@
    4.44      by (intro exI[of _ ?infm]) auto
    4.45  qed
    4.46  
    4.47 -subsubsection {*Alternative instances of caratheodory*}
    4.48 -
    4.49  lemma (in ring_of_sets) caratheodory_empty_continuous:
    4.50    assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>"
    4.51    assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
    4.52 @@ -680,7 +680,7 @@
    4.53    show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
    4.54  qed (rule cont)
    4.55  
    4.56 -section {* Volumes *}
    4.57 +subsection {* Volumes *}
    4.58  
    4.59  definition volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
    4.60    "volume M f \<longleftrightarrow>
    4.61 @@ -818,7 +818,7 @@
    4.62    qed
    4.63  qed
    4.64  
    4.65 -section {* Caratheodory on semirings *}
    4.66 +subsubsection {* Caratheodory on semirings *}
    4.67  
    4.68  theorem (in semiring_of_sets) caratheodory:
    4.69    assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
     5.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon May 19 12:04:45 2014 +0200
     5.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Mon May 19 13:44:13 2014 +0200
     5.3 @@ -11,7 +11,7 @@
     5.4  lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
     5.5    by auto
     5.6  
     5.7 -subsubsection {* Merge two extensional functions *}
     5.8 +subsubsection {* More about Function restricted by @{const extensional}  *}
     5.9  
    5.10  definition
    5.11    "merge I J = (\<lambda>(x, y) i. if i \<in> I then x i else if i \<in> J then y i else undefined)"
    5.12 @@ -105,9 +105,9 @@
    5.13    "I \<inter> J = {} \<Longrightarrow> merge I J -` Pi\<^sub>E (I \<union> J) E = Pi I E \<times> Pi J E"
    5.14    by (auto simp: restrict_Pi_cancel PiE_def)
    5.15  
    5.16 -section "Finite product spaces"
    5.17 +subsection {* Finite product spaces *}
    5.18  
    5.19 -section "Products"
    5.20 +subsubsection {* Products *}
    5.21  
    5.22  definition prod_emb where
    5.23    "prod_emb I M K X = (\<lambda>x. restrict x K) -` X \<inter> (PIE i:I. space (M i))"
     6.1 --- a/src/HOL/Probability/Information.thy	Mon May 19 12:04:45 2014 +0200
     6.2 +++ b/src/HOL/Probability/Information.thy	Mon May 19 13:44:13 2014 +0200
     6.3 @@ -26,7 +26,7 @@
     6.4    "((A, B) = X) \<longleftrightarrow> (fst X = A \<and> snd X = B)" and
     6.5    "(X = (A, B)) \<longleftrightarrow> (fst X = A \<and> snd X = B)" by auto
     6.6  
     6.7 -section "Information theory"
     6.8 +subsection "Information theory"
     6.9  
    6.10  locale information_space = prob_space +
    6.11    fixes b :: real assumes b_gt_1: "1 < b"
     7.1 --- a/src/HOL/Probability/Measure_Space.thy	Mon May 19 12:04:45 2014 +0200
     7.2 +++ b/src/HOL/Probability/Measure_Space.thy	Mon May 19 13:44:13 2014 +0200
     7.3 @@ -73,7 +73,7 @@
     7.4    represent sigma algebras (with an arbitrary emeasure).
     7.5  *}
     7.6  
     7.7 -section "Extend binary sets"
     7.8 +subsection "Extend binary sets"
     7.9  
    7.10  lemma LIMSEQ_binaryset:
    7.11    assumes f: "f {} = 0"
    7.12 @@ -105,7 +105,7 @@
    7.13    shows "f {} = 0 \<Longrightarrow> (\<Sum>n. f (binaryset A B n)) = f A + f B"
    7.14    by (metis binaryset_sums sums_unique)
    7.15  
    7.16 -section {* Properties of a premeasure @{term \<mu>} *}
    7.17 +subsection {* Properties of a premeasure @{term \<mu>} *}
    7.18  
    7.19  text {*
    7.20    The definitions for @{const positive} and @{const countably_additive} should be here, by they are
    7.21 @@ -429,7 +429,7 @@
    7.22    using empty_continuous_imp_continuous_from_below[OF f fin] cont
    7.23    by blast
    7.24  
    7.25 -section {* Properties of @{const emeasure} *}
    7.26 +subsection {* Properties of @{const emeasure} *}
    7.27  
    7.28  lemma emeasure_positive: "positive (sets M) (emeasure M)"
    7.29    by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
    7.30 @@ -761,7 +761,7 @@
    7.31      by (simp add: emeasure_countably_additive)
    7.32  qed simp_all
    7.33  
    7.34 -section "@{text \<mu>}-null sets"
    7.35 +subsection {* @{text \<mu>}-null sets *}
    7.36  
    7.37  definition null_sets :: "'a measure \<Rightarrow> 'a set set" where
    7.38    "null_sets M = {N\<in>sets M. emeasure M N = 0}"
    7.39 @@ -853,7 +853,7 @@
    7.40      by (subst plus_emeasure[symmetric]) auto
    7.41  qed
    7.42  
    7.43 -section "Formalize almost everywhere"
    7.44 +subsection {* The almost everywhere filter (i.e.\ quantifier) *}
    7.45  
    7.46  definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
    7.47    "ae_filter M = Abs_filter (\<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N)"
    7.48 @@ -1053,7 +1053,7 @@
    7.49    shows "emeasure M A = emeasure M B"
    7.50    using assms by (safe intro!: antisym emeasure_mono_AE) auto
    7.51  
    7.52 -section {* @{text \<sigma>}-finite Measures *}
    7.53 +subsection {* @{text \<sigma>}-finite Measures *}
    7.54  
    7.55  locale sigma_finite_measure =
    7.56    fixes M :: "'a measure"
    7.57 @@ -1103,7 +1103,7 @@
    7.58    qed (force simp: incseq_def)+
    7.59  qed
    7.60  
    7.61 -section {* Measure space induced by distribution of @{const measurable}-functions *}
    7.62 +subsection {* Measure space induced by distribution of @{const measurable}-functions *}
    7.63  
    7.64  definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
    7.65    "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
    7.66 @@ -1187,7 +1187,7 @@
    7.67    by (auto simp add: emeasure_distr measurable_space
    7.68             intro!: arg_cong[where f="emeasure M"] measure_eqI)
    7.69  
    7.70 -section {* Real measure values *}
    7.71 +subsection {* Real measure values *}
    7.72  
    7.73  lemma measure_nonneg: "0 \<le> measure M A"
    7.74    using emeasure_nonneg[of M A] unfolding measure_def by (auto intro: real_of_ereal_pos)
    7.75 @@ -1324,7 +1324,7 @@
    7.76      by (intro lim_real_of_ereal) simp
    7.77  qed
    7.78  
    7.79 -section {* Measure spaces with @{term "emeasure M (space M) < \<infinity>"} *}
    7.80 +subsection {* Measure spaces with @{term "emeasure M (space M) < \<infinity>"} *}
    7.81  
    7.82  locale finite_measure = sigma_finite_measure M for M +
    7.83    assumes finite_emeasure_space: "emeasure M (space M) \<noteq> \<infinity>"
    7.84 @@ -1527,7 +1527,7 @@
    7.85    shows "measure M B = 0"
    7.86    using measure_space_inter[of B A] assms by (auto simp: ac_simps)
    7.87  
    7.88 -section {* Counting space *}
    7.89 +subsection {* Counting space *}
    7.90  
    7.91  lemma strict_monoI_Suc:
    7.92    assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
    7.93 @@ -1653,7 +1653,7 @@
    7.94    show "sigma_finite_measure (count_space A)" ..
    7.95  qed
    7.96  
    7.97 -section {* Measure restricted to space *}
    7.98 +subsection {* Measure restricted to space *}
    7.99  
   7.100  lemma emeasure_restrict_space:
   7.101    assumes "\<Omega> \<in> sets M" "A \<subseteq> \<Omega>"
     8.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon May 19 12:04:45 2014 +0200
     8.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon May 19 13:44:13 2014 +0200
     8.3 @@ -13,7 +13,7 @@
     8.4    "indicator A x \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
     8.5    by (simp add: indicator_def not_le)
     8.6  
     8.7 -section "Simple function"
     8.8 +subsection "Simple function"
     8.9  
    8.10  text {*
    8.11  
    8.12 @@ -501,7 +501,7 @@
    8.13    finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
    8.14  qed
    8.15  
    8.16 -section "Simple integral"
    8.17 +subsection "Simple integral"
    8.18  
    8.19  definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>S") where
    8.20    "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))"
    8.21 @@ -734,7 +734,7 @@
    8.22    then show ?thesis by simp
    8.23  qed
    8.24  
    8.25 -section "Continuous positive integration"
    8.26 +subsection {* Integral on nonnegative functions *}
    8.27  
    8.28  definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>P") where
    8.29    "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
    8.30 @@ -1556,7 +1556,9 @@
    8.31      by (simp add: F_def)
    8.32  qed
    8.33  
    8.34 -section {* Distributions *}
    8.35 +subsection {* Integral under concrete measures *}
    8.36 +
    8.37 +subsubsection {* Distributions *}
    8.38  
    8.39  lemma positive_integral_distr':
    8.40    assumes T: "T \<in> measurable M M'"
    8.41 @@ -1587,7 +1589,7 @@
    8.42    by (subst (1 2) positive_integral_max_0[symmetric])
    8.43       (simp add: positive_integral_distr')
    8.44  
    8.45 -section {* Lebesgue integration on @{const count_space} *}
    8.46 +subsubsection {* Counting space *}
    8.47  
    8.48  lemma simple_function_count_space[simp]:
    8.49    "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)"
    8.50 @@ -1666,7 +1668,7 @@
    8.51    finally show ?thesis .
    8.52  qed
    8.53  
    8.54 -section {* Measures with Restricted Space *}
    8.55 +subsubsection {* Measures with Restricted Space *}
    8.56  
    8.57  lemma positive_integral_restrict_space:
    8.58    assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x" "\<And>x. x \<in> space M - \<Omega> \<Longrightarrow> f x = 0"
    8.59 @@ -1696,7 +1698,7 @@
    8.60      by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> positive_integral_monotone_convergence_SUP)
    8.61  qed
    8.62  
    8.63 -section {* Measure spaces with an associated density *}
    8.64 +subsubsection {* Measure spaces with an associated density *}
    8.65  
    8.66  definition density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
    8.67    "density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^sup>+ x. f x * indicator A x \<partial>M)"
    8.68 @@ -1918,7 +1920,7 @@
    8.69      using f g by (subst density_density_eq) auto
    8.70  qed
    8.71  
    8.72 -section {* Point measure *}
    8.73 +subsubsection {* Point measure *}
    8.74  
    8.75  definition point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
    8.76    "point_measure A f = density (count_space A) f"
    8.77 @@ -1991,7 +1993,7 @@
    8.78      integral\<^sup>P (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
    8.79    by (subst positive_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le)
    8.80  
    8.81 -section {* Uniform measure *}
    8.82 +subsubsection {* Uniform measure *}
    8.83  
    8.84  definition "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)"
    8.85  
    8.86 @@ -2019,7 +2021,7 @@
    8.87    using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)] B] A
    8.88    by (cases "emeasure M A" "emeasure M (A \<inter> B)" rule: ereal2_cases) (simp_all add: measure_def)
    8.89  
    8.90 -section {* Uniform count measure *}
    8.91 +subsubsection {* Uniform count measure *}
    8.92  
    8.93  definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
    8.94   
     9.1 --- a/src/HOL/Probability/Probability_Measure.thy	Mon May 19 12:04:45 2014 +0200
     9.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Mon May 19 13:44:13 2014 +0200
     9.3 @@ -349,7 +349,7 @@
     9.4    finally show ?thesis by simp
     9.5  qed
     9.6  
     9.7 -section {* Distributions *}
     9.8 +subsection {* Distributions *}
     9.9  
    9.10  definition "distributed M N X f \<longleftrightarrow> distr M N X = density N f \<and> 
    9.11    f \<in> borel_measurable N \<and> (AE x in N. 0 \<le> f x) \<and> X \<in> measurable M N"
    10.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Mon May 19 12:04:45 2014 +0200
    10.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon May 19 13:44:13 2014 +0200
    10.3 @@ -769,7 +769,7 @@
    10.4      by (auto intro!: bexI[of _ "\<lambda>x. h x * f x"] simp: density_density_eq)
    10.5  qed
    10.6  
    10.7 -section "Uniqueness of densities"
    10.8 +subsection {* Uniqueness of densities *}
    10.9  
   10.10  lemma finite_density_unique:
   10.11    assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   10.12 @@ -1060,7 +1060,7 @@
   10.13    apply (auto simp: max_def intro!: measurable_If)
   10.14    done
   10.15  
   10.16 -section "Radon-Nikodym derivative"
   10.17 +subsection {* Radon-Nikodym derivative *}
   10.18  
   10.19  definition RN_deriv :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a \<Rightarrow> ereal" where
   10.20    "RN_deriv M N =
    11.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Mon May 19 12:04:45 2014 +0200
    11.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon May 19 13:44:13 2014 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4      translated by Lawrence Paulson.
    11.5  *)
    11.6  
    11.7 -header {* Sigma Algebras *}
    11.8 +header {* Describing measurable sets *}
    11.9  
   11.10  theory Sigma_Algebra
   11.11  imports
   11.12 @@ -33,9 +33,7 @@
   11.13  lemma (in subset_class) sets_into_space: "x \<in> M \<Longrightarrow> x \<subseteq> \<Omega>"
   11.14    by (metis PowD contra_subsetD space_closed)
   11.15  
   11.16 -subsection {* Semiring of sets *}
   11.17 -
   11.18 -subsubsection {* Disjoint sets *}
   11.19 +subsubsection {* Semiring of sets *}
   11.20  
   11.21  definition "disjoint A \<longleftrightarrow> (\<forall>a\<in>A. \<forall>b\<in>A. a \<noteq> b \<longrightarrow> a \<inter> b = {})"
   11.22  
   11.23 @@ -255,7 +253,7 @@
   11.24    "X \<subseteq> S \<Longrightarrow> algebra S { {}, X, S - X, S }"
   11.25    by (auto simp: algebra_iff_Int)
   11.26  
   11.27 -subsection {* Restricted algebras *}
   11.28 +subsubsection {* Restricted algebras *}
   11.29  
   11.30  abbreviation (in algebra)
   11.31    "restricted_space A \<equiv> (op \<inter> A) ` M"
   11.32 @@ -264,7 +262,7 @@
   11.33    assumes "A \<in> M" shows "algebra A (restricted_space A)"
   11.34    using assms by (auto simp: algebra_iff_Int)
   11.35  
   11.36 -subsection {* Sigma Algebras *}
   11.37 +subsubsection {* Sigma Algebras *}
   11.38  
   11.39  locale sigma_algebra = algebra +
   11.40    assumes countable_nat_UN [intro]: "\<And>A. range A \<subseteq> M \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
   11.41 @@ -446,7 +444,7 @@
   11.42    shows "sigma_algebra S { {}, X, S - X, S }"
   11.43    using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp
   11.44  
   11.45 -subsection {* Binary Unions *}
   11.46 +subsubsection {* Binary Unions *}
   11.47  
   11.48  definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
   11.49    where "binary a b =  (\<lambda>x. b)(0 := a)"
   11.50 @@ -468,7 +466,7 @@
   11.51    by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def
   11.52           algebra_iff_Un Un_range_binary)
   11.53  
   11.54 -subsection {* Initial Sigma Algebra *}
   11.55 +subsubsection {* Initial Sigma Algebra *}
   11.56  
   11.57  text {*Sigma algebras can naturally be created as the closure of any set of
   11.58    M with regard to the properties just postulated.  *}
   11.59 @@ -775,7 +773,7 @@
   11.60    qed
   11.61  qed
   11.62  
   11.63 -subsection "Disjoint families"
   11.64 +subsubsection "Disjoint families"
   11.65  
   11.66  definition
   11.67    disjoint_family_on  where
   11.68 @@ -934,7 +932,7 @@
   11.69      by (intro disjointD[OF d]) auto
   11.70  qed
   11.71  
   11.72 -subsection {* Ring generated by a semiring *}
   11.73 +subsubsection {* Ring generated by a semiring *}
   11.74  
   11.75  definition (in semiring_of_sets)
   11.76    "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
   11.77 @@ -1064,759 +1062,7 @@
   11.78      by (blast intro!: sigma_sets_mono elim: generated_ringE)
   11.79  qed (auto intro!: generated_ringI_Basic sigma_sets_mono)
   11.80  
   11.81 -subsection {* Measure type *}
   11.82 -
   11.83 -definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
   11.84 -  "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0 \<and> (\<forall>A\<in>M. 0 \<le> \<mu> A)"
   11.85 -
   11.86 -definition countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
   11.87 -  "countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
   11.88 -    (\<Sum>i. f (A i)) = f (\<Union>i. A i))"
   11.89 -
   11.90 -definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
   11.91 -  "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
   11.92 -
   11.93 -typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
   11.94 -proof
   11.95 -  have "sigma_algebra UNIV {{}, UNIV}"
   11.96 -    by (auto simp: sigma_algebra_iff2)
   11.97 -  then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
   11.98 -    by (auto simp: measure_space_def positive_def countably_additive_def)
   11.99 -qed
  11.100 -
  11.101 -definition space :: "'a measure \<Rightarrow> 'a set" where
  11.102 -  "space M = fst (Rep_measure M)"
  11.103 -
  11.104 -definition sets :: "'a measure \<Rightarrow> 'a set set" where
  11.105 -  "sets M = fst (snd (Rep_measure M))"
  11.106 -
  11.107 -definition emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ereal" where
  11.108 -  "emeasure M = snd (snd (Rep_measure M))"
  11.109 -
  11.110 -definition measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
  11.111 -  "measure M A = real (emeasure M A)"
  11.112 -
  11.113 -declare [[coercion sets]]
  11.114 -
  11.115 -declare [[coercion measure]]
  11.116 -
  11.117 -declare [[coercion emeasure]]
  11.118 -
  11.119 -lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
  11.120 -  by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
  11.121 -
  11.122 -interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure"
  11.123 -  using measure_space[of M] by (auto simp: measure_space_def)
  11.124 -
  11.125 -definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
  11.126 -  "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
  11.127 -    \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
  11.128 -
  11.129 -abbreviation "sigma \<Omega> A \<equiv> measure_of \<Omega> A (\<lambda>x. 0)"
  11.130 -
  11.131 -lemma measure_space_0: "A \<subseteq> Pow \<Omega> \<Longrightarrow> measure_space \<Omega> (sigma_sets \<Omega> A) (\<lambda>x. 0)"
  11.132 -  unfolding measure_space_def
  11.133 -  by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def)
  11.134 -
  11.135 -lemma sigma_algebra_trivial: "sigma_algebra \<Omega> {{}, \<Omega>}"
  11.136 -by unfold_locales(fastforce intro: exI[where x="{{}}"] exI[where x="{\<Omega>}"])+
  11.137 -
  11.138 -lemma measure_space_0': "measure_space \<Omega> {{}, \<Omega>} (\<lambda>x. 0)"
  11.139 -by(simp add: measure_space_def positive_def countably_additive_def sigma_algebra_trivial)
  11.140 -
  11.141 -lemma measure_space_closed:
  11.142 -  assumes "measure_space \<Omega> M \<mu>"
  11.143 -  shows "M \<subseteq> Pow \<Omega>"
  11.144 -proof -
  11.145 -  interpret sigma_algebra \<Omega> M using assms by(simp add: measure_space_def)
  11.146 -  show ?thesis by(rule space_closed)
  11.147 -qed
  11.148 -
  11.149 -lemma (in ring_of_sets) positive_cong_eq:
  11.150 -  "(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> positive M \<mu>' = positive M \<mu>"
  11.151 -  by (auto simp add: positive_def)
  11.152 -
  11.153 -lemma (in sigma_algebra) countably_additive_eq:
  11.154 -  "(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> countably_additive M \<mu>' = countably_additive M \<mu>"
  11.155 -  unfolding countably_additive_def
  11.156 -  by (intro arg_cong[where f=All] ext) (auto simp add: countably_additive_def subset_eq)
  11.157 -
  11.158 -lemma measure_space_eq:
  11.159 -  assumes closed: "A \<subseteq> Pow \<Omega>" and eq: "\<And>a. a \<in> sigma_sets \<Omega> A \<Longrightarrow> \<mu> a = \<mu>' a"
  11.160 -  shows "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>'"
  11.161 -proof -
  11.162 -  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" using closed by (rule sigma_algebra_sigma_sets)
  11.163 -  from positive_cong_eq[OF eq, of "\<lambda>i. i"] countably_additive_eq[OF eq, of "\<lambda>i. i"] show ?thesis
  11.164 -    by (auto simp: measure_space_def)
  11.165 -qed
  11.166 -
  11.167 -lemma measure_of_eq:
  11.168 -  assumes closed: "A \<subseteq> Pow \<Omega>" and eq: "(\<And>a. a \<in> sigma_sets \<Omega> A \<Longrightarrow> \<mu> a = \<mu>' a)"
  11.169 -  shows "measure_of \<Omega> A \<mu> = measure_of \<Omega> A \<mu>'"
  11.170 -proof -
  11.171 -  have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>'"
  11.172 -    using assms by (rule measure_space_eq)
  11.173 -  with eq show ?thesis
  11.174 -    by (auto simp add: measure_of_def intro!: arg_cong[where f=Abs_measure])
  11.175 -qed
  11.176 -
  11.177 -lemma
  11.178 -  shows space_measure_of_conv: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
  11.179 -  and sets_measure_of_conv:
  11.180 -  "sets (measure_of \<Omega> A \<mu>) = (if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>})" (is ?sets)
  11.181 -  and emeasure_measure_of_conv: 
  11.182 -  "emeasure (measure_of \<Omega> A \<mu>) = 
  11.183 -  (\<lambda>B. if B \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> B else 0)" (is ?emeasure)
  11.184 -proof -
  11.185 -  have "?space \<and> ?sets \<and> ?emeasure"
  11.186 -  proof(cases "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>")
  11.187 -    case True
  11.188 -    from measure_space_closed[OF this] sigma_sets_superset_generator[of A \<Omega>]
  11.189 -    have "A \<subseteq> Pow \<Omega>" by simp
  11.190 -    hence "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A)
  11.191 -      (\<lambda>a. if a \<in> sigma_sets \<Omega> A then \<mu> a else 0)"
  11.192 -      by(rule measure_space_eq) auto
  11.193 -    with True `A \<subseteq> Pow \<Omega>` show ?thesis
  11.194 -      by(simp add: measure_of_def space_def sets_def emeasure_def Abs_measure_inverse)
  11.195 -  next
  11.196 -    case False thus ?thesis
  11.197 -      by(cases "A \<subseteq> Pow \<Omega>")(simp_all add: Abs_measure_inverse measure_of_def sets_def space_def emeasure_def measure_space_0 measure_space_0')
  11.198 -  qed
  11.199 -  thus ?space ?sets ?emeasure by simp_all
  11.200 -qed
  11.201 -
  11.202 -lemma [simp]:
  11.203 -  assumes A: "A \<subseteq> Pow \<Omega>"
  11.204 -  shows sets_measure_of: "sets (measure_of \<Omega> A \<mu>) = sigma_sets \<Omega> A"
  11.205 -    and space_measure_of: "space (measure_of \<Omega> A \<mu>) = \<Omega>"
  11.206 -using assms
  11.207 -by(simp_all add: sets_measure_of_conv space_measure_of_conv)
  11.208 -
  11.209 -lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \<Omega> M \<mu>) = M"
  11.210 -  using space_closed by (auto intro!: sigma_sets_eq)
  11.211 -
  11.212 -lemma (in sigma_algebra) space_measure_of_eq[simp]: "space (measure_of \<Omega> M \<mu>) = \<Omega>"
  11.213 -  by (rule space_measure_of_conv)
  11.214 -
  11.215 -lemma measure_of_subset: "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
  11.216 -  by (auto intro!: sigma_sets_subseteq)
  11.217 -
  11.218 -lemma sigma_sets_mono'':
  11.219 -  assumes "A \<in> sigma_sets C D"
  11.220 -  assumes "B \<subseteq> D"
  11.221 -  assumes "D \<subseteq> Pow C"
  11.222 -  shows "sigma_sets A B \<subseteq> sigma_sets C D"
  11.223 -proof
  11.224 -  fix x assume "x \<in> sigma_sets A B"
  11.225 -  thus "x \<in> sigma_sets C D"
  11.226 -  proof induct
  11.227 -    case (Basic a) with assms have "a \<in> D" by auto
  11.228 -    thus ?case ..
  11.229 -  next
  11.230 -    case Empty show ?case by (rule sigma_sets.Empty)
  11.231 -  next
  11.232 -    from assms have "A \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`])
  11.233 -    moreover case (Compl a) hence "a \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`])
  11.234 -    ultimately have "A - a \<in> sets (sigma C D)" ..
  11.235 -    thus ?case by (subst (asm) sets_measure_of[OF `D \<subseteq> Pow C`])
  11.236 -  next
  11.237 -    case (Union a)
  11.238 -    thus ?case by (intro sigma_sets.Union)
  11.239 -  qed
  11.240 -qed
  11.241 -
  11.242 -lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
  11.243 -  by auto
  11.244 -
  11.245 -subsection {* Constructing simple @{typ "'a measure"} *}
  11.246 -
  11.247 -lemma emeasure_measure_of:
  11.248 -  assumes M: "M = measure_of \<Omega> A \<mu>"
  11.249 -  assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
  11.250 -  assumes X: "X \<in> sets M"
  11.251 -  shows "emeasure M X = \<mu> X"
  11.252 -proof -
  11.253 -  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
  11.254 -  have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
  11.255 -    using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
  11.256 -  thus ?thesis using X ms
  11.257 -    by(simp add: M emeasure_measure_of_conv sets_measure_of_conv)
  11.258 -qed
  11.259 -
  11.260 -lemma emeasure_measure_of_sigma:
  11.261 -  assumes ms: "sigma_algebra \<Omega> M" "positive M \<mu>" "countably_additive M \<mu>"
  11.262 -  assumes A: "A \<in> M"
  11.263 -  shows "emeasure (measure_of \<Omega> M \<mu>) A = \<mu> A"
  11.264 -proof -
  11.265 -  interpret sigma_algebra \<Omega> M by fact
  11.266 -  have "measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
  11.267 -    using ms sigma_sets_eq by (simp add: measure_space_def)
  11.268 -  thus ?thesis by(simp add: emeasure_measure_of_conv A)
  11.269 -qed
  11.270 -
  11.271 -lemma measure_cases[cases type: measure]:
  11.272 -  obtains (measure) \<Omega> A \<mu> where "x = Abs_measure (\<Omega>, A, \<mu>)" "\<forall>a\<in>-A. \<mu> a = 0" "measure_space \<Omega> A \<mu>"
  11.273 -  by atomize_elim (cases x, auto)
  11.274 -
  11.275 -lemma sets_eq_imp_space_eq:
  11.276 -  "sets M = sets M' \<Longrightarrow> space M = space M'"
  11.277 -  using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
  11.278 -  by blast
  11.279 -
  11.280 -lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
  11.281 -  by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
  11.282 -
  11.283 -lemma emeasure_neq_0_sets: "emeasure M A \<noteq> 0 \<Longrightarrow> A \<in> sets M"
  11.284 -  using emeasure_notin_sets[of A M] by blast
  11.285 -
  11.286 -lemma measure_notin_sets: "A \<notin> sets M \<Longrightarrow> measure M A = 0"
  11.287 -  by (simp add: measure_def emeasure_notin_sets)
  11.288 -
  11.289 -lemma measure_eqI:
  11.290 -  fixes M N :: "'a measure"
  11.291 -  assumes "sets M = sets N" and eq: "\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A = emeasure N A"
  11.292 -  shows "M = N"
  11.293 -proof (cases M N rule: measure_cases[case_product measure_cases])
  11.294 -  case (measure_measure \<Omega> A \<mu> \<Omega>' A' \<mu>')
  11.295 -  interpret M: sigma_algebra \<Omega> A using measure_measure by (auto simp: measure_space_def)
  11.296 -  interpret N: sigma_algebra \<Omega>' A' using measure_measure by (auto simp: measure_space_def)
  11.297 -  have "A = sets M" "A' = sets N"
  11.298 -    using measure_measure by (simp_all add: sets_def Abs_measure_inverse)
  11.299 -  with `sets M = sets N` have AA': "A = A'" by simp
  11.300 -  moreover from M.top N.top M.space_closed N.space_closed AA' have "\<Omega> = \<Omega>'" by auto
  11.301 -  moreover { fix B have "\<mu> B = \<mu>' B"
  11.302 -    proof cases
  11.303 -      assume "B \<in> A"
  11.304 -      with eq `A = sets M` have "emeasure M B = emeasure N B" by simp
  11.305 -      with measure_measure show "\<mu> B = \<mu>' B"
  11.306 -        by (simp add: emeasure_def Abs_measure_inverse)
  11.307 -    next
  11.308 -      assume "B \<notin> A"
  11.309 -      with `A = sets M` `A' = sets N` `A = A'` have "B \<notin> sets M" "B \<notin> sets N"
  11.310 -        by auto
  11.311 -      then have "emeasure M B = 0" "emeasure N B = 0"
  11.312 -        by (simp_all add: emeasure_notin_sets)
  11.313 -      with measure_measure show "\<mu> B = \<mu>' B"
  11.314 -        by (simp add: emeasure_def Abs_measure_inverse)
  11.315 -    qed }
  11.316 -  then have "\<mu> = \<mu>'" by auto
  11.317 -  ultimately show "M = N"
  11.318 -    by (simp add: measure_measure)
  11.319 -qed
  11.320 -
  11.321 -lemma emeasure_sigma: "A \<subseteq> Pow \<Omega> \<Longrightarrow> emeasure (sigma \<Omega> A) = (\<lambda>_. 0)"
  11.322 -  using measure_space_0[of A \<Omega>]
  11.323 -  by (simp add: measure_of_def emeasure_def Abs_measure_inverse)
  11.324 -
  11.325 -lemma sigma_eqI:
  11.326 -  assumes [simp]: "M \<subseteq> Pow \<Omega>" "N \<subseteq> Pow \<Omega>" "sigma_sets \<Omega> M = sigma_sets \<Omega> N"
  11.327 -  shows "sigma \<Omega> M = sigma \<Omega> N"
  11.328 -  by (rule measure_eqI) (simp_all add: emeasure_sigma)
  11.329 -
  11.330 -subsection {* Measurable functions *}
  11.331 -
  11.332 -definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
  11.333 -  "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
  11.334 -
  11.335 -lemma measurable_space:
  11.336 -  "f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A"
  11.337 -   unfolding measurable_def by auto
  11.338 -
  11.339 -lemma measurable_sets:
  11.340 -  "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
  11.341 -   unfolding measurable_def by auto
  11.342 -
  11.343 -lemma measurable_sets_Collect:
  11.344 -  assumes f: "f \<in> measurable M N" and P: "{x\<in>space N. P x} \<in> sets N" shows "{x\<in>space M. P (f x)} \<in> sets M"
  11.345 -proof -
  11.346 -  have "f -` {x \<in> space N. P x} \<inter> space M = {x\<in>space M. P (f x)}"
  11.347 -    using measurable_space[OF f] by auto
  11.348 -  with measurable_sets[OF f P] show ?thesis
  11.349 -    by simp
  11.350 -qed
  11.351 -
  11.352 -lemma measurable_sigma_sets:
  11.353 -  assumes B: "sets N = sigma_sets \<Omega> A" "A \<subseteq> Pow \<Omega>"
  11.354 -      and f: "f \<in> space M \<rightarrow> \<Omega>"
  11.355 -      and ba: "\<And>y. y \<in> A \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
  11.356 -  shows "f \<in> measurable M N"
  11.357 -proof -
  11.358 -  interpret A: sigma_algebra \<Omega> "sigma_sets \<Omega> A" using B(2) by (rule sigma_algebra_sigma_sets)
  11.359 -  from B sets.top[of N] A.top sets.space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
  11.360 -  
  11.361 -  { fix X assume "X \<in> sigma_sets \<Omega> A"
  11.362 -    then have "f -` X \<inter> space M \<in> sets M \<and> X \<subseteq> \<Omega>"
  11.363 -      proof induct
  11.364 -        case (Basic a) then show ?case
  11.365 -          by (auto simp add: ba) (metis B(2) subsetD PowD)
  11.366 -      next
  11.367 -        case (Compl a)
  11.368 -        have [simp]: "f -` \<Omega> \<inter> space M = space M"
  11.369 -          by (auto simp add: funcset_mem [OF f])
  11.370 -        then show ?case
  11.371 -          by (auto simp add: vimage_Diff Diff_Int_distrib2 sets.compl_sets Compl)
  11.372 -      next
  11.373 -        case (Union a)
  11.374 -        then show ?case
  11.375 -          by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast
  11.376 -      qed auto }
  11.377 -  with f show ?thesis
  11.378 -    by (auto simp add: measurable_def B \<Omega>)
  11.379 -qed
  11.380 -
  11.381 -lemma measurable_measure_of:
  11.382 -  assumes B: "N \<subseteq> Pow \<Omega>"
  11.383 -      and f: "f \<in> space M \<rightarrow> \<Omega>"
  11.384 -      and ba: "\<And>y. y \<in> N \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
  11.385 -  shows "f \<in> measurable M (measure_of \<Omega> N \<mu>)"
  11.386 -proof -
  11.387 -  have "sets (measure_of \<Omega> N \<mu>) = sigma_sets \<Omega> N"
  11.388 -    using B by (rule sets_measure_of)
  11.389 -  from this assms show ?thesis by (rule measurable_sigma_sets)
  11.390 -qed
  11.391 -
  11.392 -lemma measurable_iff_measure_of:
  11.393 -  assumes "N \<subseteq> Pow \<Omega>" "f \<in> space M \<rightarrow> \<Omega>"
  11.394 -  shows "f \<in> measurable M (measure_of \<Omega> N \<mu>) \<longleftrightarrow> (\<forall>A\<in>N. f -` A \<inter> space M \<in> sets M)"
  11.395 -  by (metis assms in_measure_of measurable_measure_of assms measurable_sets)
  11.396 -
  11.397 -lemma measurable_cong_sets:
  11.398 -  assumes sets: "sets M = sets M'" "sets N = sets N'"
  11.399 -  shows "measurable M N = measurable M' N'"
  11.400 -  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
  11.401 -
  11.402 -lemma measurable_cong:
  11.403 -  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
  11.404 -  shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
  11.405 -  unfolding measurable_def using assms
  11.406 -  by (simp cong: vimage_inter_cong Pi_cong)
  11.407 -
  11.408 -lemma measurable_cong_strong:
  11.409 -  "M = N \<Longrightarrow> M' = N' \<Longrightarrow> (\<And>w. w \<in> space M \<Longrightarrow> f w = g w) \<Longrightarrow>
  11.410 -    f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'"
  11.411 -  by (metis measurable_cong)
  11.412 -
  11.413 -lemma measurable_eqI:
  11.414 -     "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
  11.415 -        sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
  11.416 -      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
  11.417 -  by (simp add: measurable_def sigma_algebra_iff2)
  11.418 -
  11.419 -lemma measurable_compose:
  11.420 -  assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L"
  11.421 -  shows "(\<lambda>x. g (f x)) \<in> measurable M L"
  11.422 -proof -
  11.423 -  have "\<And>A. (\<lambda>x. g (f x)) -` A \<inter> space M = f -` (g -` A \<inter> space N) \<inter> space M"
  11.424 -    using measurable_space[OF f] by auto
  11.425 -  with measurable_space[OF f] measurable_space[OF g] show ?thesis
  11.426 -    by (auto intro: measurable_sets[OF f] measurable_sets[OF g]
  11.427 -             simp del: vimage_Int simp add: measurable_def)
  11.428 -qed
  11.429 -
  11.430 -lemma measurable_comp:
  11.431 -  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> g \<circ> f \<in> measurable M L"
  11.432 -  using measurable_compose[of f M N g L] by (simp add: comp_def)
  11.433 -
  11.434 -lemma measurable_const:
  11.435 -  "c \<in> space M' \<Longrightarrow> (\<lambda>x. c) \<in> measurable M M'"
  11.436 -  by (auto simp add: measurable_def)
  11.437 -
  11.438 -lemma measurable_If:
  11.439 -  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
  11.440 -  assumes P: "{x\<in>space M. P x} \<in> sets M"
  11.441 -  shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'"
  11.442 -  unfolding measurable_def
  11.443 -proof safe
  11.444 -  fix x assume "x \<in> space M"
  11.445 -  thus "(if P x then f x else g x) \<in> space M'"
  11.446 -    using measure unfolding measurable_def by auto
  11.447 -next
  11.448 -  fix A assume "A \<in> sets M'"
  11.449 -  hence *: "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M =
  11.450 -    ((f -` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union>
  11.451 -    ((g -` A \<inter> space M) \<inter> (space M - {x\<in>space M. P x}))"
  11.452 -    using measure unfolding measurable_def by (auto split: split_if_asm)
  11.453 -  show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
  11.454 -    using `A \<in> sets M'` measure P unfolding * measurable_def
  11.455 -    by (auto intro!: sets.Un)
  11.456 -qed
  11.457 -
  11.458 -lemma measurable_If_set:
  11.459 -  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
  11.460 -  assumes P: "A \<inter> space M \<in> sets M"
  11.461 -  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'"
  11.462 -proof (rule measurable_If[OF measure])
  11.463 -  have "{x \<in> space M. x \<in> A} = A \<inter> space M" by auto
  11.464 -  thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<inter> space M \<in> sets M` by auto
  11.465 -qed
  11.466 -
  11.467 -lemma measurable_ident: "id \<in> measurable M M"
  11.468 -  by (auto simp add: measurable_def)
  11.469 -
  11.470 -lemma measurable_ident_sets:
  11.471 -  assumes eq: "sets M = sets M'" shows "(\<lambda>x. x) \<in> measurable M M'"
  11.472 -  using measurable_ident[of M]
  11.473 -  unfolding id_def measurable_def eq sets_eq_imp_space_eq[OF eq] .
  11.474 -
  11.475 -lemma sets_Least:
  11.476 -  assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
  11.477 -  shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
  11.478 -proof -
  11.479 -  { fix i have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M \<in> sets M"
  11.480 -    proof cases
  11.481 -      assume i: "(LEAST j. False) = i"
  11.482 -      have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
  11.483 -        {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x})) \<union> (space M - (\<Union>i. {x\<in>space M. P i x}))"
  11.484 -        by (simp add: set_eq_iff, safe)
  11.485 -           (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
  11.486 -      with meas show ?thesis
  11.487 -        by (auto intro!: sets.Int)
  11.488 -    next
  11.489 -      assume i: "(LEAST j. False) \<noteq> i"
  11.490 -      then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
  11.491 -        {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x}))"
  11.492 -      proof (simp add: set_eq_iff, safe)
  11.493 -        fix x assume neq: "(LEAST j. False) \<noteq> (LEAST j. P j x)"
  11.494 -        have "\<exists>j. P j x"
  11.495 -          by (rule ccontr) (insert neq, auto)
  11.496 -        then show "P (LEAST j. P j x) x" by (rule LeastI_ex)
  11.497 -      qed (auto dest: Least_le intro!: Least_equality)
  11.498 -      with meas show ?thesis
  11.499 -        by auto
  11.500 -    qed }
  11.501 -  then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
  11.502 -    by (intro sets.countable_UN) auto
  11.503 -  moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
  11.504 -    (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
  11.505 -  ultimately show ?thesis by auto
  11.506 -qed
  11.507 -
  11.508 -lemma measurable_strong:
  11.509 -  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
  11.510 -  assumes f: "f \<in> measurable a b" and g: "g \<in> space b \<rightarrow> space c"
  11.511 -      and t: "f ` (space a) \<subseteq> t"
  11.512 -      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
  11.513 -  shows "(g o f) \<in> measurable a c"
  11.514 -proof -
  11.515 -  have fab: "f \<in> (space a -> space b)"
  11.516 -   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
  11.517 -     by (auto simp add: measurable_def)
  11.518 -  have eq: "\<And>y. (g \<circ> f) -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
  11.519 -    by force
  11.520 -  show ?thesis
  11.521 -    apply (auto simp add: measurable_def vimage_comp)
  11.522 -    apply (metis funcset_mem fab g)
  11.523 -    apply (subst eq)
  11.524 -    apply (metis ba cb)
  11.525 -    done
  11.526 -qed
  11.527 -
  11.528 -lemma measurable_mono1:
  11.529 -  "M' \<subseteq> Pow \<Omega> \<Longrightarrow> M \<subseteq> M' \<Longrightarrow>
  11.530 -    measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
  11.531 -  using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
  11.532 -
  11.533 -subsection {* Counting space *}
  11.534 -
  11.535 -definition count_space :: "'a set \<Rightarrow> 'a measure" where
  11.536 -  "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
  11.537 -
  11.538 -lemma 
  11.539 -  shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
  11.540 -    and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
  11.541 -  using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]
  11.542 -  by (auto simp: count_space_def)
  11.543 -
  11.544 -lemma measurable_count_space_eq1[simp]:
  11.545 -  "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
  11.546 - unfolding measurable_def by simp
  11.547 -
  11.548 -lemma measurable_count_space_eq2:
  11.549 -  assumes "finite A"
  11.550 -  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
  11.551 -proof -
  11.552 -  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
  11.553 -    with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
  11.554 -      by (auto dest: finite_subset)
  11.555 -    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
  11.556 -    ultimately have "f -` X \<inter> space M \<in> sets M"
  11.557 -      using `X \<subseteq> A` by (auto intro!: sets.finite_UN simp del: UN_simps) }
  11.558 -  then show ?thesis
  11.559 -    unfolding measurable_def by auto
  11.560 -qed
  11.561 -
  11.562 -lemma measurable_count_space_eq2_countable:
  11.563 -  fixes f :: "'a => 'c::countable"
  11.564 -  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
  11.565 -proof -
  11.566 -  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
  11.567 -    assume *: "\<And>a. a\<in>A \<Longrightarrow> f -` {a} \<inter> space M \<in> sets M"
  11.568 -    have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)"
  11.569 -      by auto
  11.570 -    also have "\<dots> \<in> sets M"
  11.571 -      using * `X \<subseteq> A` by (intro sets.countable_UN) auto
  11.572 -    finally have "f -` X \<inter> space M \<in> sets M" . }
  11.573 -  then show ?thesis
  11.574 -    unfolding measurable_def by auto
  11.575 -qed
  11.576 -
  11.577 -lemma measurable_compose_countable:
  11.578 -  assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)"
  11.579 -  shows "(\<lambda>x. f (g x) x) \<in> measurable M N"
  11.580 -  unfolding measurable_def
  11.581 -proof safe
  11.582 -  fix x assume "x \<in> space M" then show "f (g x) x \<in> space N"
  11.583 -    using f[THEN measurable_space] g[THEN measurable_space] by auto
  11.584 -next
  11.585 -  fix A assume A: "A \<in> sets N"
  11.586 -  have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
  11.587 -    by auto
  11.588 -  also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
  11.589 -    by (auto intro!: sets.countable_UN measurable_sets)
  11.590 -  finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
  11.591 -qed
  11.592 -
  11.593 -lemma measurable_count_space_const:
  11.594 -  "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
  11.595 -  by (simp add: measurable_const)
  11.596 -
  11.597 -lemma measurable_count_space:
  11.598 -  "f \<in> measurable (count_space A) (count_space UNIV)"
  11.599 -  by simp
  11.600 -
  11.601 -lemma measurable_compose_rev:
  11.602 -  assumes f: "f \<in> measurable L N" and g: "g \<in> measurable M L"
  11.603 -  shows "(\<lambda>x. f (g x)) \<in> measurable M N"
  11.604 -  using measurable_compose[OF g f] .
  11.605 -
  11.606 -lemma measurable_count_space_eq_countable:
  11.607 -  assumes "countable A"
  11.608 -  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
  11.609 -proof -
  11.610 -  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
  11.611 -    with `countable A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "countable X"
  11.612 -      by (auto dest: countable_subset)
  11.613 -    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
  11.614 -    ultimately have "f -` X \<inter> space M \<in> sets M"
  11.615 -      using `X \<subseteq> A` by (auto intro!: sets.countable_UN' simp del: UN_simps) }
  11.616 -  then show ?thesis
  11.617 -    unfolding measurable_def by auto
  11.618 -qed
  11.619 -
  11.620 -subsection {* Extend measure *}
  11.621 -
  11.622 -definition "extend_measure \<Omega> I G \<mu> =
  11.623 -  (if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)
  11.624 -      then measure_of \<Omega> (G`I) (SOME \<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>')
  11.625 -      else measure_of \<Omega> (G`I) (\<lambda>_. 0))"
  11.626 -
  11.627 -lemma space_extend_measure: "G ` I \<subseteq> Pow \<Omega> \<Longrightarrow> space (extend_measure \<Omega> I G \<mu>) = \<Omega>"
  11.628 -  unfolding extend_measure_def by simp
  11.629 -
  11.630 -lemma sets_extend_measure: "G ` I \<subseteq> Pow \<Omega> \<Longrightarrow> sets (extend_measure \<Omega> I G \<mu>) = sigma_sets \<Omega> (G`I)"
  11.631 -  unfolding extend_measure_def by simp
  11.632 -
  11.633 -lemma emeasure_extend_measure:
  11.634 -  assumes M: "M = extend_measure \<Omega> I G \<mu>"
  11.635 -    and eq: "\<And>i. i \<in> I \<Longrightarrow> \<mu>' (G i) = \<mu> i"
  11.636 -    and ms: "G ` I \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'"
  11.637 -    and "i \<in> I"
  11.638 -  shows "emeasure M (G i) = \<mu> i"
  11.639 -proof cases
  11.640 -  assume *: "(\<forall>i\<in>I. \<mu> i = 0)"
  11.641 -  with M have M_eq: "M = measure_of \<Omega> (G`I) (\<lambda>_. 0)"
  11.642 -   by (simp add: extend_measure_def)
  11.643 -  from measure_space_0[OF ms(1)] ms `i\<in>I`
  11.644 -  have "emeasure M (G i) = 0"
  11.645 -    by (intro emeasure_measure_of[OF M_eq]) (auto simp add: M measure_space_def sets_extend_measure)
  11.646 -  with `i\<in>I` * show ?thesis
  11.647 -    by simp
  11.648 -next
  11.649 -  def P \<equiv> "\<lambda>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>'"
  11.650 -  assume "\<not> (\<forall>i\<in>I. \<mu> i = 0)"
  11.651 -  moreover
  11.652 -  have "measure_space (space M) (sets M) \<mu>'"
  11.653 -    using ms unfolding measure_space_def by auto default
  11.654 -  with ms eq have "\<exists>\<mu>'. P \<mu>'"
  11.655 -    unfolding P_def
  11.656 -    by (intro exI[of _ \<mu>']) (auto simp add: M space_extend_measure sets_extend_measure)
  11.657 -  ultimately have M_eq: "M = measure_of \<Omega> (G`I) (Eps P)"
  11.658 -    by (simp add: M extend_measure_def P_def[symmetric])
  11.659 -
  11.660 -  from `\<exists>\<mu>'. P \<mu>'` have P: "P (Eps P)" by (rule someI_ex)
  11.661 -  show "emeasure M (G i) = \<mu> i"
  11.662 -  proof (subst emeasure_measure_of[OF M_eq])
  11.663 -    have sets_M: "sets M = sigma_sets \<Omega> (G`I)"
  11.664 -      using M_eq ms by (auto simp: sets_extend_measure)
  11.665 -    then show "G i \<in> sets M" using `i \<in> I` by auto
  11.666 -    show "positive (sets M) (Eps P)" "countably_additive (sets M) (Eps P)" "Eps P (G i) = \<mu> i"
  11.667 -      using P `i\<in>I` by (auto simp add: sets_M measure_space_def P_def)
  11.668 -  qed fact
  11.669 -qed
  11.670 -
  11.671 -lemma emeasure_extend_measure_Pair:
  11.672 -  assumes M: "M = extend_measure \<Omega> {(i, j). I i j} (\<lambda>(i, j). G i j) (\<lambda>(i, j). \<mu> i j)"
  11.673 -    and eq: "\<And>i j. I i j \<Longrightarrow> \<mu>' (G i j) = \<mu> i j"
  11.674 -    and ms: "\<And>i j. I i j \<Longrightarrow> G i j \<in> Pow \<Omega>" "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'"
  11.675 -    and "I i j"
  11.676 -  shows "emeasure M (G i j) = \<mu> i j"
  11.677 -  using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) `I i j`
  11.678 -  by (auto simp: subset_eq)
  11.679 -
  11.680 -subsection {* Sigma algebra generated by function preimages *}
  11.681 -
  11.682 -definition
  11.683 -  "vimage_algebra M S X = sigma S ((\<lambda>A. X -` A \<inter> S) ` sets M)"
  11.684 -
  11.685 -lemma sigma_algebra_preimages:
  11.686 -  fixes f :: "'x \<Rightarrow> 'a"
  11.687 -  assumes "f \<in> S \<rightarrow> space M"
  11.688 -  shows "sigma_algebra S ((\<lambda>A. f -` A \<inter> S) ` sets M)"
  11.689 -    (is "sigma_algebra _ (?F ` sets M)")
  11.690 -proof (simp add: sigma_algebra_iff2, safe)
  11.691 -  show "{} \<in> ?F ` sets M" by blast
  11.692 -next
  11.693 -  fix A assume "A \<in> sets M"
  11.694 -  moreover have "S - ?F A = ?F (space M - A)"
  11.695 -    using assms by auto
  11.696 -  ultimately show "S - ?F A \<in> ?F ` sets M"
  11.697 -    by blast
  11.698 -next
  11.699 -  fix A :: "nat \<Rightarrow> 'x set" assume *: "range A \<subseteq> ?F ` M"
  11.700 -  have "\<forall>i. \<exists>b. b \<in> M \<and> A i = ?F b"
  11.701 -  proof safe
  11.702 -    fix i
  11.703 -    have "A i \<in> ?F ` M" using * by auto
  11.704 -    then show "\<exists>b. b \<in> M \<and> A i = ?F b" by auto
  11.705 -  qed
  11.706 -  from choice[OF this] obtain b where b: "range b \<subseteq> M" "\<And>i. A i = ?F (b i)"
  11.707 -    by auto
  11.708 -  then have "(\<Union>i. A i) = ?F (\<Union>i. b i)" by auto
  11.709 -  then show "(\<Union>i. A i) \<in> ?F ` M" using b(1) by blast
  11.710 -qed
  11.711 -
  11.712 -lemma sets_vimage_algebra[simp]:
  11.713 -  "f \<in> S \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra M S f) = (\<lambda>A. f -` A \<inter> S) ` sets M"
  11.714 -  using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_preimages, of f S M]
  11.715 -  by (simp add: vimage_algebra_def)
  11.716 -
  11.717 -lemma space_vimage_algebra[simp]:
  11.718 -  "f \<in> S \<rightarrow> space M \<Longrightarrow> space (vimage_algebra M S f) = S"
  11.719 -  using sigma_algebra.space_measure_of_eq[OF sigma_algebra_preimages, of f S M]
  11.720 -  by (simp add: vimage_algebra_def)
  11.721 -
  11.722 -lemma in_vimage_algebra[simp]:
  11.723 -  "f \<in> S \<rightarrow> space M \<Longrightarrow> A \<in> sets (vimage_algebra M S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
  11.724 -  by (simp add: image_iff)
  11.725 -
  11.726 -lemma measurable_vimage_algebra:
  11.727 -  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
  11.728 -  shows "f \<in> measurable (vimage_algebra M S f) M"
  11.729 -  unfolding measurable_def using assms by force
  11.730 -
  11.731 -lemma measurable_vimage:
  11.732 -  fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a"
  11.733 -  assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M"
  11.734 -  shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra M S f) M2"
  11.735 -proof -
  11.736 -  note measurable_vimage_algebra[OF assms(2)]
  11.737 -  from measurable_comp[OF this assms(1)]
  11.738 -  show ?thesis by (simp add: comp_def)
  11.739 -qed
  11.740 -
  11.741 -lemma sigma_sets_vimage:
  11.742 -  assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
  11.743 -  shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
  11.744 -proof (intro set_eqI iffI)
  11.745 -  let ?F = "\<lambda>X. f -` X \<inter> S'"
  11.746 -  fix X assume "X \<in> sigma_sets S' (?F ` A)"
  11.747 -  then show "X \<in> ?F ` sigma_sets S A"
  11.748 -  proof induct
  11.749 -    case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A"
  11.750 -      by auto
  11.751 -    then show ?case by auto
  11.752 -  next
  11.753 -    case Empty then show ?case
  11.754 -      by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty)
  11.755 -  next
  11.756 -    case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A"
  11.757 -      by auto
  11.758 -    then have "S - X' \<in> sigma_sets S A"
  11.759 -      by (auto intro!: sigma_sets.Compl)
  11.760 -    then show ?case
  11.761 -      using X assms by (auto intro!: image_eqI[where x="S - X'"])
  11.762 -  next
  11.763 -    case (Union F)
  11.764 -    then have "\<forall>i. \<exists>F'.  F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'"
  11.765 -      by (auto simp: image_iff Bex_def)
  11.766 -    from choice[OF this] obtain F' where
  11.767 -      "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'"
  11.768 -      by auto
  11.769 -    then show ?case
  11.770 -      by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"])
  11.771 -  qed
  11.772 -next
  11.773 -  let ?F = "\<lambda>X. f -` X \<inter> S'"
  11.774 -  fix X assume "X \<in> ?F ` sigma_sets S A"
  11.775 -  then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto
  11.776 -  then show "X \<in> sigma_sets S' (?F ` A)"
  11.777 -  proof (induct arbitrary: X)
  11.778 -    case Empty then show ?case by (auto intro: sigma_sets.Empty)
  11.779 -  next
  11.780 -    case (Compl X')
  11.781 -    have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)"
  11.782 -      apply (rule sigma_sets.Compl)
  11.783 -      using assms by (auto intro!: Compl.hyps simp: Compl.prems)
  11.784 -    also have "S' - (S' - X) = X"
  11.785 -      using assms Compl by auto
  11.786 -    finally show ?case .
  11.787 -  next
  11.788 -    case (Union F)
  11.789 -    have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)"
  11.790 -      by (intro sigma_sets.Union Union.hyps) simp
  11.791 -    also have "(\<Union>i. f -` F i \<inter> S') = X"
  11.792 -      using assms Union by auto
  11.793 -    finally show ?case .
  11.794 -  qed auto
  11.795 -qed
  11.796 -
  11.797 -subsection {* Restricted Space Sigma Algebra *}
  11.798 -
  11.799 -definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
  11.800 -
  11.801 -lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega>"
  11.802 -  unfolding restrict_space_def by (subst space_measure_of) auto
  11.803 -
  11.804 -lemma sets_restrict_space: "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
  11.805 -  using sigma_sets_vimage[of "\<lambda>x. x" \<Omega> "space M" "sets M"]
  11.806 -  unfolding restrict_space_def
  11.807 -  by (subst sets_measure_of) (auto simp: sets.sigma_sets_eq Int_commute[of _ \<Omega>] sets.space_closed)
  11.808 -
  11.809 -lemma sets_restrict_space_iff:
  11.810 -  "\<Omega> \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
  11.811 -  by (subst sets_restrict_space) (auto dest: sets.sets_into_space)
  11.812 -
  11.813 -lemma measurable_restrict_space1:
  11.814 -  assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> measurable M N" shows "f \<in> measurable (restrict_space M \<Omega>) N"
  11.815 -  unfolding measurable_def
  11.816 -proof (intro CollectI conjI ballI)
  11.817 -  show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N"
  11.818 -    using measurable_space[OF f] sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
  11.819 -
  11.820 -  fix A assume "A \<in> sets N"
  11.821 -  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> \<Omega>"
  11.822 -    using sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
  11.823 -  also have "\<dots> \<in> sets (restrict_space M \<Omega>)"
  11.824 -    unfolding sets_restrict_space_iff[OF \<Omega>]
  11.825 -    using measurable_sets[OF f `A \<in> sets N`] \<Omega> by blast
  11.826 -  finally show "f -` A \<inter> space (restrict_space M \<Omega>) \<in> sets (restrict_space M \<Omega>)" .
  11.827 -qed
  11.828 -
  11.829 -lemma measurable_restrict_space2:
  11.830 -  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> f \<in> measurable M (restrict_space N \<Omega>)"
  11.831 -  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
  11.832 -
  11.833 -subsection {* A Two-Element Series *}
  11.834 +subsubsection {* A Two-Element Series *}
  11.835  
  11.836  definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
  11.837    where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)"
  11.838 @@ -1830,7 +1076,7 @@
  11.839  lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
  11.840    by (simp add: SUP_def range_binaryset_eq)
  11.841  
  11.842 -section {* Closed CDI *}
  11.843 +subsubsection {* Closed CDI *}
  11.844  
  11.845  definition closed_cdi where
  11.846    "closed_cdi \<Omega> M \<longleftrightarrow>
  11.847 @@ -2064,7 +1310,7 @@
  11.848      by blast
  11.849  qed
  11.850  
  11.851 -subsection {* Dynkin systems *}
  11.852 +subsubsection {* Dynkin systems *}
  11.853  
  11.854  locale dynkin_system = subset_class +
  11.855    assumes space: "\<Omega> \<in> M"
  11.856 @@ -2126,7 +1372,7 @@
  11.857    show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI)
  11.858  qed
  11.859  
  11.860 -subsection "Intersection stable algebras"
  11.861 +subsubsection "Intersection sets systems"
  11.862  
  11.863  definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
  11.864  
  11.865 @@ -2162,7 +1408,7 @@
  11.866    qed auto
  11.867  qed
  11.868  
  11.869 -subsection "Smallest Dynkin systems"
  11.870 +subsubsection "Smallest Dynkin systems"
  11.871  
  11.872  definition dynkin where
  11.873    "dynkin \<Omega> M =  (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})"
  11.874 @@ -2309,6 +1555,11 @@
  11.875      using assms by (auto simp: dynkin_def)
  11.876  qed
  11.877  
  11.878 +subsubsection {* Induction rule for intersection-stable generators *}
  11.879 +
  11.880 +text {* The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
  11.881 +generated by a generator closed under intersection. *}
  11.882 +
  11.883  lemma sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
  11.884    assumes "Int_stable G"
  11.885      and closed: "G \<subseteq> Pow \<Omega>"
  11.886 @@ -2330,4 +1581,756 @@
  11.887    with A show ?thesis by auto
  11.888  qed
  11.889  
  11.890 +subsection {* Measure type *}
  11.891 +
  11.892 +definition positive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
  11.893 +  "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0 \<and> (\<forall>A\<in>M. 0 \<le> \<mu> A)"
  11.894 +
  11.895 +definition countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
  11.896 +  "countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
  11.897 +    (\<Sum>i. f (A i)) = f (\<Union>i. A i))"
  11.898 +
  11.899 +definition measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
  11.900 +  "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
  11.901 +
  11.902 +typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
  11.903 +proof
  11.904 +  have "sigma_algebra UNIV {{}, UNIV}"
  11.905 +    by (auto simp: sigma_algebra_iff2)
  11.906 +  then show "(UNIV, {{}, UNIV}, \<lambda>A. 0) \<in> {(\<Omega>, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu>} "
  11.907 +    by (auto simp: measure_space_def positive_def countably_additive_def)
  11.908 +qed
  11.909 +
  11.910 +definition space :: "'a measure \<Rightarrow> 'a set" where
  11.911 +  "space M = fst (Rep_measure M)"
  11.912 +
  11.913 +definition sets :: "'a measure \<Rightarrow> 'a set set" where
  11.914 +  "sets M = fst (snd (Rep_measure M))"
  11.915 +
  11.916 +definition emeasure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ereal" where
  11.917 +  "emeasure M = snd (snd (Rep_measure M))"
  11.918 +
  11.919 +definition measure :: "'a measure \<Rightarrow> 'a set \<Rightarrow> real" where
  11.920 +  "measure M A = real (emeasure M A)"
  11.921 +
  11.922 +declare [[coercion sets]]
  11.923 +
  11.924 +declare [[coercion measure]]
  11.925 +
  11.926 +declare [[coercion emeasure]]
  11.927 +
  11.928 +lemma measure_space: "measure_space (space M) (sets M) (emeasure M)"
  11.929 +  by (cases M) (auto simp: space_def sets_def emeasure_def Abs_measure_inverse)
  11.930 +
  11.931 +interpretation sets!: sigma_algebra "space M" "sets M" for M :: "'a measure"
  11.932 +  using measure_space[of M] by (auto simp: measure_space_def)
  11.933 +
  11.934 +definition measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
  11.935 +  "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
  11.936 +    \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
  11.937 +
  11.938 +abbreviation "sigma \<Omega> A \<equiv> measure_of \<Omega> A (\<lambda>x. 0)"
  11.939 +
  11.940 +lemma measure_space_0: "A \<subseteq> Pow \<Omega> \<Longrightarrow> measure_space \<Omega> (sigma_sets \<Omega> A) (\<lambda>x. 0)"
  11.941 +  unfolding measure_space_def
  11.942 +  by (auto intro!: sigma_algebra_sigma_sets simp: positive_def countably_additive_def)
  11.943 +
  11.944 +lemma sigma_algebra_trivial: "sigma_algebra \<Omega> {{}, \<Omega>}"
  11.945 +by unfold_locales(fastforce intro: exI[where x="{{}}"] exI[where x="{\<Omega>}"])+
  11.946 +
  11.947 +lemma measure_space_0': "measure_space \<Omega> {{}, \<Omega>} (\<lambda>x. 0)"
  11.948 +by(simp add: measure_space_def positive_def countably_additive_def sigma_algebra_trivial)
  11.949 +
  11.950 +lemma measure_space_closed:
  11.951 +  assumes "measure_space \<Omega> M \<mu>"
  11.952 +  shows "M \<subseteq> Pow \<Omega>"
  11.953 +proof -
  11.954 +  interpret sigma_algebra \<Omega> M using assms by(simp add: measure_space_def)
  11.955 +  show ?thesis by(rule space_closed)
  11.956 +qed
  11.957 +
  11.958 +lemma (in ring_of_sets) positive_cong_eq:
  11.959 +  "(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> positive M \<mu>' = positive M \<mu>"
  11.960 +  by (auto simp add: positive_def)
  11.961 +
  11.962 +lemma (in sigma_algebra) countably_additive_eq:
  11.963 +  "(\<And>a. a \<in> M \<Longrightarrow> \<mu>' a = \<mu> a) \<Longrightarrow> countably_additive M \<mu>' = countably_additive M \<mu>"
  11.964 +  unfolding countably_additive_def
  11.965 +  by (intro arg_cong[where f=All] ext) (auto simp add: countably_additive_def subset_eq)
  11.966 +
  11.967 +lemma measure_space_eq:
  11.968 +  assumes closed: "A \<subseteq> Pow \<Omega>" and eq: "\<And>a. a \<in> sigma_sets \<Omega> A \<Longrightarrow> \<mu> a = \<mu>' a"
  11.969 +  shows "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>'"
  11.970 +proof -
  11.971 +  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" using closed by (rule sigma_algebra_sigma_sets)
  11.972 +  from positive_cong_eq[OF eq, of "\<lambda>i. i"] countably_additive_eq[OF eq, of "\<lambda>i. i"] show ?thesis
  11.973 +    by (auto simp: measure_space_def)
  11.974 +qed
  11.975 +
  11.976 +lemma measure_of_eq:
  11.977 +  assumes closed: "A \<subseteq> Pow \<Omega>" and eq: "(\<And>a. a \<in> sigma_sets \<Omega> A \<Longrightarrow> \<mu> a = \<mu>' a)"
  11.978 +  shows "measure_of \<Omega> A \<mu> = measure_of \<Omega> A \<mu>'"
  11.979 +proof -
  11.980 +  have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>'"
  11.981 +    using assms by (rule measure_space_eq)
  11.982 +  with eq show ?thesis
  11.983 +    by (auto simp add: measure_of_def intro!: arg_cong[where f=Abs_measure])
  11.984 +qed
  11.985 +
  11.986 +lemma
  11.987 +  shows space_measure_of_conv: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
  11.988 +  and sets_measure_of_conv:
  11.989 +  "sets (measure_of \<Omega> A \<mu>) = (if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>})" (is ?sets)
  11.990 +  and emeasure_measure_of_conv: 
  11.991 +  "emeasure (measure_of \<Omega> A \<mu>) = 
  11.992 +  (\<lambda>B. if B \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> B else 0)" (is ?emeasure)
  11.993 +proof -
  11.994 +  have "?space \<and> ?sets \<and> ?emeasure"
  11.995 +  proof(cases "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>")
  11.996 +    case True
  11.997 +    from measure_space_closed[OF this] sigma_sets_superset_generator[of A \<Omega>]
  11.998 +    have "A \<subseteq> Pow \<Omega>" by simp
  11.999 +    hence "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> = measure_space \<Omega> (sigma_sets \<Omega> A)
 11.1000 +      (\<lambda>a. if a \<in> sigma_sets \<Omega> A then \<mu> a else 0)"
 11.1001 +      by(rule measure_space_eq) auto
 11.1002 +    with True `A \<subseteq> Pow \<Omega>` show ?thesis
 11.1003 +      by(simp add: measure_of_def space_def sets_def emeasure_def Abs_measure_inverse)
 11.1004 +  next
 11.1005 +    case False thus ?thesis
 11.1006 +      by(cases "A \<subseteq> Pow \<Omega>")(simp_all add: Abs_measure_inverse measure_of_def sets_def space_def emeasure_def measure_space_0 measure_space_0')
 11.1007 +  qed
 11.1008 +  thus ?space ?sets ?emeasure by simp_all
 11.1009 +qed
 11.1010 +
 11.1011 +lemma [simp]:
 11.1012 +  assumes A: "A \<subseteq> Pow \<Omega>"
 11.1013 +  shows sets_measure_of: "sets (measure_of \<Omega> A \<mu>) = sigma_sets \<Omega> A"
 11.1014 +    and space_measure_of: "space (measure_of \<Omega> A \<mu>) = \<Omega>"
 11.1015 +using assms
 11.1016 +by(simp_all add: sets_measure_of_conv space_measure_of_conv)
 11.1017 +
 11.1018 +lemma (in sigma_algebra) sets_measure_of_eq[simp]: "sets (measure_of \<Omega> M \<mu>) = M"
 11.1019 +  using space_closed by (auto intro!: sigma_sets_eq)
 11.1020 +
 11.1021 +lemma (in sigma_algebra) space_measure_of_eq[simp]: "space (measure_of \<Omega> M \<mu>) = \<Omega>"
 11.1022 +  by (rule space_measure_of_conv)
 11.1023 +
 11.1024 +lemma measure_of_subset: "M \<subseteq> Pow \<Omega> \<Longrightarrow> M' \<subseteq> M \<Longrightarrow> sets (measure_of \<Omega> M' \<mu>) \<subseteq> sets (measure_of \<Omega> M \<mu>')"
 11.1025 +  by (auto intro!: sigma_sets_subseteq)
 11.1026 +
 11.1027 +lemma sigma_sets_mono'':
 11.1028 +  assumes "A \<in> sigma_sets C D"
 11.1029 +  assumes "B \<subseteq> D"
 11.1030 +  assumes "D \<subseteq> Pow C"
 11.1031 +  shows "sigma_sets A B \<subseteq> sigma_sets C D"
 11.1032 +proof
 11.1033 +  fix x assume "x \<in> sigma_sets A B"
 11.1034 +  thus "x \<in> sigma_sets C D"
 11.1035 +  proof induct
 11.1036 +    case (Basic a) with assms have "a \<in> D" by auto
 11.1037 +    thus ?case ..
 11.1038 +  next
 11.1039 +    case Empty show ?case by (rule sigma_sets.Empty)
 11.1040 +  next
 11.1041 +    from assms have "A \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`])
 11.1042 +    moreover case (Compl a) hence "a \<in> sets (sigma C D)" by (subst sets_measure_of[OF `D \<subseteq> Pow C`])
 11.1043 +    ultimately have "A - a \<in> sets (sigma C D)" ..
 11.1044 +    thus ?case by (subst (asm) sets_measure_of[OF `D \<subseteq> Pow C`])
 11.1045 +  next
 11.1046 +    case (Union a)
 11.1047 +    thus ?case by (intro sigma_sets.Union)
 11.1048 +  qed
 11.1049 +qed
 11.1050 +
 11.1051 +lemma in_measure_of[intro, simp]: "M \<subseteq> Pow \<Omega> \<Longrightarrow> A \<in> M \<Longrightarrow> A \<in> sets (measure_of \<Omega> M \<mu>)"
 11.1052 +  by auto
 11.1053 +
 11.1054 +subsubsection {* Constructing simple @{typ "'a measure"} *}
 11.1055 +
 11.1056 +lemma emeasure_measure_of:
 11.1057 +  assumes M: "M = measure_of \<Omega> A \<mu>"
 11.1058 +  assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
 11.1059 +  assumes X: "X \<in> sets M"
 11.1060 +  shows "emeasure M X = \<mu> X"
 11.1061 +proof -
 11.1062 +  interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
 11.1063 +  have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
 11.1064 +    using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)
 11.1065 +  thus ?thesis using X ms
 11.1066 +    by(simp add: M emeasure_measure_of_conv sets_measure_of_conv)
 11.1067 +qed
 11.1068 +
 11.1069 +lemma emeasure_measure_of_sigma:
 11.1070 +  assumes ms: "sigma_algebra \<Omega> M" "positive M \<mu>" "countably_additive M \<mu>"
 11.1071 +  assumes A: "A \<in> M"
 11.1072 +  shows "emeasure (measure_of \<Omega> M \<mu>) A = \<mu> A"
 11.1073 +proof -
 11.1074 +  interpret sigma_algebra \<Omega> M by fact
 11.1075 +  have "measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
 11.1076 +    using ms sigma_sets_eq by (simp add: measure_space_def)
 11.1077 +  thus ?thesis by(simp add: emeasure_measure_of_conv A)
 11.1078 +qed
 11.1079 +
 11.1080 +lemma measure_cases[cases type: measure]:
 11.1081 +  obtains (measure) \<Omega> A \<mu> where "x = Abs_measure (\<Omega>, A, \<mu>)" "\<forall>a\<in>-A. \<mu> a = 0" "measure_space \<Omega> A \<mu>"
 11.1082 +  by atomize_elim (cases x, auto)
 11.1083 +
 11.1084 +lemma sets_eq_imp_space_eq:
 11.1085 +  "sets M = sets M' \<Longrightarrow> space M = space M'"
 11.1086 +  using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
 11.1087 +  by blast
 11.1088 +
 11.1089 +lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
 11.1090 +  by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
 11.1091 +
 11.1092 +lemma emeasure_neq_0_sets: "emeasure M A \<noteq> 0 \<Longrightarrow> A \<in> sets M"
 11.1093 +  using emeasure_notin_sets[of A M] by blast
 11.1094 +
 11.1095 +lemma measure_notin_sets: "A \<notin> sets M \<Longrightarrow> measure M A = 0"
 11.1096 +  by (simp add: measure_def emeasure_notin_sets)
 11.1097 +
 11.1098 +lemma measure_eqI:
 11.1099 +  fixes M N :: "'a measure"
 11.1100 +  assumes "sets M = sets N" and eq: "\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A = emeasure N A"
 11.1101 +  shows "M = N"
 11.1102 +proof (cases M N rule: measure_cases[case_product measure_cases])
 11.1103 +  case (measure_measure \<Omega> A \<mu> \<Omega>' A' \<mu>')
 11.1104 +  interpret M: sigma_algebra \<Omega> A using measure_measure by (auto simp: measure_space_def)
 11.1105 +  interpret N: sigma_algebra \<Omega>' A' using measure_measure by (auto simp: measure_space_def)
 11.1106 +  have "A = sets M" "A' = sets N"
 11.1107 +    using measure_measure by (simp_all add: sets_def Abs_measure_inverse)
 11.1108 +  with `sets M = sets N` have AA': "A = A'" by simp
 11.1109 +  moreover from M.top N.top M.space_closed N.space_closed AA' have "\<Omega> = \<Omega>'" by auto
 11.1110 +  moreover { fix B have "\<mu> B = \<mu>' B"
 11.1111 +    proof cases
 11.1112 +      assume "B \<in> A"
 11.1113 +      with eq `A = sets M` have "emeasure M B = emeasure N B" by simp
 11.1114 +      with measure_measure show "\<mu> B = \<mu>' B"
 11.1115 +        by (simp add: emeasure_def Abs_measure_inverse)
 11.1116 +    next
 11.1117 +      assume "B \<notin> A"
 11.1118 +      with `A = sets M` `A' = sets N` `A = A'` have "B \<notin> sets M" "B \<notin> sets N"
 11.1119 +        by auto
 11.1120 +      then have "emeasure M B = 0" "emeasure N B = 0"
 11.1121 +        by (simp_all add: emeasure_notin_sets)
 11.1122 +      with measure_measure show "\<mu> B = \<mu>' B"
 11.1123 +        by (simp add: emeasure_def Abs_measure_inverse)
 11.1124 +    qed }
 11.1125 +  then have "\<mu> = \<mu>'" by auto
 11.1126 +  ultimately show "M = N"
 11.1127 +    by (simp add: measure_measure)
 11.1128 +qed
 11.1129 +
 11.1130 +lemma emeasure_sigma: "A \<subseteq> Pow \<Omega> \<Longrightarrow> emeasure (sigma \<Omega> A) = (\<lambda>_. 0)"
 11.1131 +  using measure_space_0[of A \<Omega>]
 11.1132 +  by (simp add: measure_of_def emeasure_def Abs_measure_inverse)
 11.1133 +
 11.1134 +lemma sigma_eqI:
 11.1135 +  assumes [simp]: "M \<subseteq> Pow \<Omega>" "N \<subseteq> Pow \<Omega>" "sigma_sets \<Omega> M = sigma_sets \<Omega> N"
 11.1136 +  shows "sigma \<Omega> M = sigma \<Omega> N"
 11.1137 +  by (rule measure_eqI) (simp_all add: emeasure_sigma)
 11.1138 +
 11.1139 +subsubsection {* Measurable functions *}
 11.1140 +
 11.1141 +definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
 11.1142 +  "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
 11.1143 +
 11.1144 +lemma measurable_space:
 11.1145 +  "f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A"
 11.1146 +   unfolding measurable_def by auto
 11.1147 +
 11.1148 +lemma measurable_sets:
 11.1149 +  "f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f -` S \<inter> space M \<in> sets M"
 11.1150 +   unfolding measurable_def by auto
 11.1151 +
 11.1152 +lemma measurable_sets_Collect:
 11.1153 +  assumes f: "f \<in> measurable M N" and P: "{x\<in>space N. P x} \<in> sets N" shows "{x\<in>space M. P (f x)} \<in> sets M"
 11.1154 +proof -
 11.1155 +  have "f -` {x \<in> space N. P x} \<inter> space M = {x\<in>space M. P (f x)}"
 11.1156 +    using measurable_space[OF f] by auto
 11.1157 +  with measurable_sets[OF f P] show ?thesis
 11.1158 +    by simp
 11.1159 +qed
 11.1160 +
 11.1161 +lemma measurable_sigma_sets:
 11.1162 +  assumes B: "sets N = sigma_sets \<Omega> A" "A \<subseteq> Pow \<Omega>"
 11.1163 +      and f: "f \<in> space M \<rightarrow> \<Omega>"
 11.1164 +      and ba: "\<And>y. y \<in> A \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
 11.1165 +  shows "f \<in> measurable M N"
 11.1166 +proof -
 11.1167 +  interpret A: sigma_algebra \<Omega> "sigma_sets \<Omega> A" using B(2) by (rule sigma_algebra_sigma_sets)
 11.1168 +  from B sets.top[of N] A.top sets.space_closed[of N] A.space_closed have \<Omega>: "\<Omega> = space N" by force
 11.1169 +  
 11.1170 +  { fix X assume "X \<in> sigma_sets \<Omega> A"
 11.1171 +    then have "f -` X \<inter> space M \<in> sets M \<and> X \<subseteq> \<Omega>"
 11.1172 +      proof induct
 11.1173 +        case (Basic a) then show ?case
 11.1174 +          by (auto simp add: ba) (metis B(2) subsetD PowD)
 11.1175 +      next
 11.1176 +        case (Compl a)
 11.1177 +        have [simp]: "f -` \<Omega> \<inter> space M = space M"
 11.1178 +          by (auto simp add: funcset_mem [OF f])
 11.1179 +        then show ?case
 11.1180 +          by (auto simp add: vimage_Diff Diff_Int_distrib2 sets.compl_sets Compl)
 11.1181 +      next
 11.1182 +        case (Union a)
 11.1183 +        then show ?case
 11.1184 +          by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast
 11.1185 +      qed auto }
 11.1186 +  with f show ?thesis
 11.1187 +    by (auto simp add: measurable_def B \<Omega>)
 11.1188 +qed
 11.1189 +
 11.1190 +lemma measurable_measure_of:
 11.1191 +  assumes B: "N \<subseteq> Pow \<Omega>"
 11.1192 +      and f: "f \<in> space M \<rightarrow> \<Omega>"
 11.1193 +      and ba: "\<And>y. y \<in> N \<Longrightarrow> (f -` y) \<inter> space M \<in> sets M"
 11.1194 +  shows "f \<in> measurable M (measure_of \<Omega> N \<mu>)"
 11.1195 +proof -
 11.1196 +  have "sets (measure_of \<Omega> N \<mu>) = sigma_sets \<Omega> N"
 11.1197 +    using B by (rule sets_measure_of)
 11.1198 +  from this assms show ?thesis by (rule measurable_sigma_sets)
 11.1199 +qed
 11.1200 +
 11.1201 +lemma measurable_iff_measure_of:
 11.1202 +  assumes "N \<subseteq> Pow \<Omega>" "f \<in> space M \<rightarrow> \<Omega>"
 11.1203 +  shows "f \<in> measurable M (measure_of \<Omega> N \<mu>) \<longleftrightarrow> (\<forall>A\<in>N. f -` A \<inter> space M \<in> sets M)"
 11.1204 +  by (metis assms in_measure_of measurable_measure_of assms measurable_sets)
 11.1205 +
 11.1206 +lemma measurable_cong_sets:
 11.1207 +  assumes sets: "sets M = sets M'" "sets N = sets N'"
 11.1208 +  shows "measurable M N = measurable M' N'"
 11.1209 +  using sets[THEN sets_eq_imp_space_eq] sets by (simp add: measurable_def)
 11.1210 +
 11.1211 +lemma measurable_cong:
 11.1212 +  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
 11.1213 +  shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'"
 11.1214 +  unfolding measurable_def using assms
 11.1215 +  by (simp cong: vimage_inter_cong Pi_cong)
 11.1216 +
 11.1217 +lemma measurable_cong_strong:
 11.1218 +  "M = N \<Longrightarrow> M' = N' \<Longrightarrow> (\<And>w. w \<in> space M \<Longrightarrow> f w = g w) \<Longrightarrow>
 11.1219 +    f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'"
 11.1220 +  by (metis measurable_cong)
 11.1221 +
 11.1222 +lemma measurable_eqI:
 11.1223 +     "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
 11.1224 +        sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
 11.1225 +      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
 11.1226 +  by (simp add: measurable_def sigma_algebra_iff2)
 11.1227 +
 11.1228 +lemma measurable_compose:
 11.1229 +  assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L"
 11.1230 +  shows "(\<lambda>x. g (f x)) \<in> measurable M L"
 11.1231 +proof -
 11.1232 +  have "\<And>A. (\<lambda>x. g (f x)) -` A \<inter> space M = f -` (g -` A \<inter> space N) \<inter> space M"
 11.1233 +    using measurable_space[OF f] by auto
 11.1234 +  with measurable_space[OF f] measurable_space[OF g] show ?thesis
 11.1235 +    by (auto intro: measurable_sets[OF f] measurable_sets[OF g]
 11.1236 +             simp del: vimage_Int simp add: measurable_def)
 11.1237 +qed
 11.1238 +
 11.1239 +lemma measurable_comp:
 11.1240 +  "f \<in> measurable M N \<Longrightarrow> g \<in> measurable N L \<Longrightarrow> g \<circ> f \<in> measurable M L"
 11.1241 +  using measurable_compose[of f M N g L] by (simp add: comp_def)
 11.1242 +
 11.1243 +lemma measurable_const:
 11.1244 +  "c \<in> space M' \<Longrightarrow> (\<lambda>x. c) \<in> measurable M M'"
 11.1245 +  by (auto simp add: measurable_def)
 11.1246 +
 11.1247 +lemma measurable_If:
 11.1248 +  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
 11.1249 +  assumes P: "{x\<in>space M. P x} \<in> sets M"
 11.1250 +  shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'"
 11.1251 +  unfolding measurable_def
 11.1252 +proof safe
 11.1253 +  fix x assume "x \<in> space M"
 11.1254 +  thus "(if P x then f x else g x) \<in> space M'"
 11.1255 +    using measure unfolding measurable_def by auto
 11.1256 +next
 11.1257 +  fix A assume "A \<in> sets M'"
 11.1258 +  hence *: "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M =
 11.1259 +    ((f -` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union>
 11.1260 +    ((g -` A \<inter> space M) \<inter> (space M - {x\<in>space M. P x}))"
 11.1261 +    using measure unfolding measurable_def by (auto split: split_if_asm)
 11.1262 +  show "(\<lambda>x. if P x then f x else g x) -` A \<inter> space M \<in> sets M"
 11.1263 +    using `A \<in> sets M'` measure P unfolding * measurable_def
 11.1264 +    by (auto intro!: sets.Un)
 11.1265 +qed
 11.1266 +
 11.1267 +lemma measurable_If_set:
 11.1268 +  assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'"
 11.1269 +  assumes P: "A \<inter> space M \<in> sets M"
 11.1270 +  shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'"
 11.1271 +proof (rule measurable_If[OF measure])
 11.1272 +  have "{x \<in> space M. x \<in> A} = A \<inter> space M" by auto
 11.1273 +  thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<inter> space M \<in> sets M` by auto
 11.1274 +qed
 11.1275 +
 11.1276 +lemma measurable_ident: "id \<in> measurable M M"
 11.1277 +  by (auto simp add: measurable_def)
 11.1278 +
 11.1279 +lemma measurable_ident_sets:
 11.1280 +  assumes eq: "sets M = sets M'" shows "(\<lambda>x. x) \<in> measurable M M'"
 11.1281 +  using measurable_ident[of M]
 11.1282 +  unfolding id_def measurable_def eq sets_eq_imp_space_eq[OF eq] .
 11.1283 +
 11.1284 +lemma sets_Least:
 11.1285 +  assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
 11.1286 +  shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
 11.1287 +proof -
 11.1288 +  { fix i have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M \<in> sets M"
 11.1289 +    proof cases
 11.1290 +      assume i: "(LEAST j. False) = i"
 11.1291 +      have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
 11.1292 +        {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x})) \<union> (space M - (\<Union>i. {x\<in>space M. P i x}))"
 11.1293 +        by (simp add: set_eq_iff, safe)
 11.1294 +           (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
 11.1295 +      with meas show ?thesis
 11.1296 +        by (auto intro!: sets.Int)
 11.1297 +    next
 11.1298 +      assume i: "(LEAST j. False) \<noteq> i"
 11.1299 +      then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
 11.1300 +        {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x}))"
 11.1301 +      proof (simp add: set_eq_iff, safe)
 11.1302 +        fix x assume neq: "(LEAST j. False) \<noteq> (LEAST j. P j x)"
 11.1303 +        have "\<exists>j. P j x"
 11.1304 +          by (rule ccontr) (insert neq, auto)
 11.1305 +        then show "P (LEAST j. P j x) x" by (rule LeastI_ex)
 11.1306 +      qed (auto dest: Least_le intro!: Least_equality)
 11.1307 +      with meas show ?thesis
 11.1308 +        by auto
 11.1309 +    qed }
 11.1310 +  then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
 11.1311 +    by (intro sets.countable_UN) auto
 11.1312 +  moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
 11.1313 +    (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
 11.1314 +  ultimately show ?thesis by auto
 11.1315 +qed
 11.1316 +
 11.1317 +lemma measurable_strong:
 11.1318 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
 11.1319 +  assumes f: "f \<in> measurable a b" and g: "g \<in> space b \<rightarrow> space c"
 11.1320 +      and t: "f ` (space a) \<subseteq> t"
 11.1321 +      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
 11.1322 +  shows "(g o f) \<in> measurable a c"
 11.1323 +proof -
 11.1324 +  have fab: "f \<in> (space a -> space b)"
 11.1325 +   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
 11.1326 +     by (auto simp add: measurable_def)
 11.1327 +  have eq: "\<And>y. (g \<circ> f) -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
 11.1328 +    by force
 11.1329 +  show ?thesis
 11.1330 +    apply (auto simp add: measurable_def vimage_comp)
 11.1331 +    apply (metis funcset_mem fab g)
 11.1332 +    apply (subst eq)
 11.1333 +    apply (metis ba cb)
 11.1334 +    done
 11.1335 +qed
 11.1336 +
 11.1337 +lemma measurable_mono1:
 11.1338 +  "M' \<subseteq> Pow \<Omega> \<Longrightarrow> M \<subseteq> M' \<Longrightarrow>
 11.1339 +    measurable (measure_of \<Omega> M \<mu>) N \<subseteq> measurable (measure_of \<Omega> M' \<mu>') N"
 11.1340 +  using measure_of_subset[of M' \<Omega> M] by (auto simp add: measurable_def)
 11.1341 +
 11.1342 +subsubsection {* Counting space *}
 11.1343 +
 11.1344 +definition count_space :: "'a set \<Rightarrow> 'a measure" where
 11.1345 +  "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then ereal (card A) else \<infinity>)"
 11.1346 +
 11.1347 +lemma 
 11.1348 +  shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
 11.1349 +    and sets_count_space[simp]: "sets (count_space \<Omega>) = Pow \<Omega>"
 11.1350 +  using sigma_sets_into_sp[of "Pow \<Omega>" \<Omega>]
 11.1351 +  by (auto simp: count_space_def)
 11.1352 +
 11.1353 +lemma measurable_count_space_eq1[simp]:
 11.1354 +  "f \<in> measurable (count_space A) M \<longleftrightarrow> f \<in> A \<rightarrow> space M"
 11.1355 + unfolding measurable_def by simp
 11.1356 +
 11.1357 +lemma measurable_count_space_eq2:
 11.1358 +  assumes "finite A"
 11.1359 +  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
 11.1360 +proof -
 11.1361 +  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
 11.1362 +    with `finite A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "finite X"
 11.1363 +      by (auto dest: finite_subset)
 11.1364 +    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
 11.1365 +    ultimately have "f -` X \<inter> space M \<in> sets M"
 11.1366 +      using `X \<subseteq> A` by (auto intro!: sets.finite_UN simp del: UN_simps) }
 11.1367 +  then show ?thesis
 11.1368 +    unfolding measurable_def by auto
 11.1369 +qed
 11.1370 +
 11.1371 +lemma measurable_count_space_eq2_countable:
 11.1372 +  fixes f :: "'a => 'c::countable"
 11.1373 +  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
 11.1374 +proof -
 11.1375 +  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
 11.1376 +    assume *: "\<And>a. a\<in>A \<Longrightarrow> f -` {a} \<inter> space M \<in> sets M"
 11.1377 +    have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)"
 11.1378 +      by auto
 11.1379 +    also have "\<dots> \<in> sets M"
 11.1380 +      using * `X \<subseteq> A` by (intro sets.countable_UN) auto
 11.1381 +    finally have "f -` X \<inter> space M \<in> sets M" . }
 11.1382 +  then show ?thesis
 11.1383 +    unfolding measurable_def by auto
 11.1384 +qed
 11.1385 +
 11.1386 +lemma measurable_compose_countable:
 11.1387 +  assumes f: "\<And>i::'i::countable. (\<lambda>x. f i x) \<in> measurable M N" and g: "g \<in> measurable M (count_space UNIV)"
 11.1388 +  shows "(\<lambda>x. f (g x) x) \<in> measurable M N"
 11.1389 +  unfolding measurable_def
 11.1390 +proof safe
 11.1391 +  fix x assume "x \<in> space M" then show "f (g x) x \<in> space N"
 11.1392 +    using f[THEN measurable_space] g[THEN measurable_space] by auto
 11.1393 +next
 11.1394 +  fix A assume A: "A \<in> sets N"
 11.1395 +  have "(\<lambda>x. f (g x) x) -` A \<inter> space M = (\<Union>i. (g -` {i} \<inter> space M) \<inter> (f i -` A \<inter> space M))"
 11.1396 +    by auto
 11.1397 +  also have "\<dots> \<in> sets M" using f[THEN measurable_sets, OF A] g[THEN measurable_sets]
 11.1398 +    by (auto intro!: sets.countable_UN measurable_sets)
 11.1399 +  finally show "(\<lambda>x. f (g x) x) -` A \<inter> space M \<in> sets M" .
 11.1400 +qed
 11.1401 +
 11.1402 +lemma measurable_count_space_const:
 11.1403 +  "(\<lambda>x. c) \<in> measurable M (count_space UNIV)"
 11.1404 +  by (simp add: measurable_const)
 11.1405 +
 11.1406 +lemma measurable_count_space:
 11.1407 +  "f \<in> measurable (count_space A) (count_space UNIV)"
 11.1408 +  by simp
 11.1409 +
 11.1410 +lemma measurable_compose_rev:
 11.1411 +  assumes f: "f \<in> measurable L N" and g: "g \<in> measurable M L"
 11.1412 +  shows "(\<lambda>x. f (g x)) \<in> measurable M N"
 11.1413 +  using measurable_compose[OF g f] .
 11.1414 +
 11.1415 +lemma measurable_count_space_eq_countable:
 11.1416 +  assumes "countable A"
 11.1417 +  shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))"
 11.1418 +proof -
 11.1419 +  { fix X assume "X \<subseteq> A" "f \<in> space M \<rightarrow> A"
 11.1420 +    with `countable A` have "f -` X \<inter> space M = (\<Union>a\<in>X. f -` {a} \<inter> space M)" "countable X"
 11.1421 +      by (auto dest: countable_subset)
 11.1422 +    moreover assume "\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M"
 11.1423 +    ultimately have "f -` X \<inter> space M \<in> sets M"
 11.1424 +      using `X \<subseteq> A` by (auto intro!: sets.countable_UN' simp del: UN_simps) }
 11.1425 +  then show ?thesis
 11.1426 +    unfolding measurable_def by auto
 11.1427 +qed
 11.1428 +
 11.1429 +subsubsection {* Extend measure *}
 11.1430 +
 11.1431 +definition "extend_measure \<Omega> I G \<mu> =
 11.1432 +  (if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)
 11.1433 +      then measure_of \<Omega> (G`I) (SOME \<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>')
 11.1434 +      else measure_of \<Omega> (G`I) (\<lambda>_. 0))"
 11.1435 +
 11.1436 +lemma space_extend_measure: "G ` I \<subseteq> Pow \<Omega> \<Longrightarrow> space (extend_measure \<Omega> I G \<mu>) = \<Omega>"
 11.1437 +  unfolding extend_measure_def by simp
 11.1438 +
 11.1439 +lemma sets_extend_measure: "G ` I \<subseteq> Pow \<Omega> \<Longrightarrow> sets (extend_measure \<Omega> I G \<mu>) = sigma_sets \<Omega> (G`I)"
 11.1440 +  unfolding extend_measure_def by simp
 11.1441 +
 11.1442 +lemma emeasure_extend_measure:
 11.1443 +  assumes M: "M = extend_measure \<Omega> I G \<mu>"
 11.1444 +    and eq: "\<And>i. i \<in> I \<Longrightarrow> \<mu>' (G i) = \<mu> i"
 11.1445 +    and ms: "G ` I \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'"
 11.1446 +    and "i \<in> I"
 11.1447 +  shows "emeasure M (G i) = \<mu> i"
 11.1448 +proof cases
 11.1449 +  assume *: "(\<forall>i\<in>I. \<mu> i = 0)"
 11.1450 +  with M have M_eq: "M = measure_of \<Omega> (G`I) (\<lambda>_. 0)"
 11.1451 +   by (simp add: extend_measure_def)
 11.1452 +  from measure_space_0[OF ms(1)] ms `i\<in>I`
 11.1453 +  have "emeasure M (G i) = 0"
 11.1454 +    by (intro emeasure_measure_of[OF M_eq]) (auto simp add: M measure_space_def sets_extend_measure)
 11.1455 +  with `i\<in>I` * show ?thesis
 11.1456 +    by simp
 11.1457 +next
 11.1458 +  def P \<equiv> "\<lambda>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>'"
 11.1459 +  assume "\<not> (\<forall>i\<in>I. \<mu> i = 0)"
 11.1460 +  moreover
 11.1461 +  have "measure_space (space M) (sets M) \<mu>'"
 11.1462 +    using ms unfolding measure_space_def by auto default
 11.1463 +  with ms eq have "\<exists>\<mu>'. P \<mu>'"
 11.1464 +    unfolding P_def
 11.1465 +    by (intro exI[of _ \<mu>']) (auto simp add: M space_extend_measure sets_extend_measure)
 11.1466 +  ultimately have M_eq: "M = measure_of \<Omega> (G`I) (Eps P)"
 11.1467 +    by (simp add: M extend_measure_def P_def[symmetric])
 11.1468 +
 11.1469 +  from `\<exists>\<mu>'. P \<mu>'` have P: "P (Eps P)" by (rule someI_ex)
 11.1470 +  show "emeasure M (G i) = \<mu> i"
 11.1471 +  proof (subst emeasure_measure_of[OF M_eq])
 11.1472 +    have sets_M: "sets M = sigma_sets \<Omega> (G`I)"
 11.1473 +      using M_eq ms by (auto simp: sets_extend_measure)
 11.1474 +    then show "G i \<in> sets M" using `i \<in> I` by auto
 11.1475 +    show "positive (sets M) (Eps P)" "countably_additive (sets M) (Eps P)" "Eps P (G i) = \<mu> i"
 11.1476 +      using P `i\<in>I` by (auto simp add: sets_M measure_space_def P_def)
 11.1477 +  qed fact
 11.1478 +qed
 11.1479 +
 11.1480 +lemma emeasure_extend_measure_Pair:
 11.1481 +  assumes M: "M = extend_measure \<Omega> {(i, j). I i j} (\<lambda>(i, j). G i j) (\<lambda>(i, j). \<mu> i j)"
 11.1482 +    and eq: "\<And>i j. I i j \<Longrightarrow> \<mu>' (G i j) = \<mu> i j"
 11.1483 +    and ms: "\<And>i j. I i j \<Longrightarrow> G i j \<in> Pow \<Omega>" "positive (sets M) \<mu>'" "countably_additive (sets M) \<mu>'"
 11.1484 +    and "I i j"
 11.1485 +  shows "emeasure M (G i j) = \<mu> i j"
 11.1486 +  using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) `I i j`
 11.1487 +  by (auto simp: subset_eq)
 11.1488 +
 11.1489 +subsubsection {* Sigma algebra generated by function preimages *}
 11.1490 +
 11.1491 +definition
 11.1492 +  "vimage_algebra M S X = sigma S ((\<lambda>A. X -` A \<inter> S) ` sets M)"
 11.1493 +
 11.1494 +lemma sigma_algebra_preimages:
 11.1495 +  fixes f :: "'x \<Rightarrow> 'a"
 11.1496 +  assumes "f \<in> S \<rightarrow> space M"
 11.1497 +  shows "sigma_algebra S ((\<lambda>A. f -` A \<inter> S) ` sets M)"
 11.1498 +    (is "sigma_algebra _ (?F ` sets M)")
 11.1499 +proof (simp add: sigma_algebra_iff2, safe)
 11.1500 +  show "{} \<in> ?F ` sets M" by blast
 11.1501 +next
 11.1502 +  fix A assume "A \<in> sets M"
 11.1503 +  moreover have "S - ?F A = ?F (space M - A)"
 11.1504 +    using assms by auto
 11.1505 +  ultimately show "S - ?F A \<in> ?F ` sets M"
 11.1506 +    by blast
 11.1507 +next
 11.1508 +  fix A :: "nat \<Rightarrow> 'x set" assume *: "range A \<subseteq> ?F ` M"
 11.1509 +  have "\<forall>i. \<exists>b. b \<in> M \<and> A i = ?F b"
 11.1510 +  proof safe
 11.1511 +    fix i
 11.1512 +    have "A i \<in> ?F ` M" using * by auto
 11.1513 +    then show "\<exists>b. b \<in> M \<and> A i = ?F b" by auto
 11.1514 +  qed
 11.1515 +  from choice[OF this] obtain b where b: "range b \<subseteq> M" "\<And>i. A i = ?F (b i)"
 11.1516 +    by auto
 11.1517 +  then have "(\<Union>i. A i) = ?F (\<Union>i. b i)" by auto
 11.1518 +  then show "(\<Union>i. A i) \<in> ?F ` M" using b(1) by blast
 11.1519 +qed
 11.1520 +
 11.1521 +lemma sets_vimage_algebra[simp]:
 11.1522 +  "f \<in> S \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra M S f) = (\<lambda>A. f -` A \<inter> S) ` sets M"
 11.1523 +  using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_preimages, of f S M]
 11.1524 +  by (simp add: vimage_algebra_def)
 11.1525 +
 11.1526 +lemma space_vimage_algebra[simp]:
 11.1527 +  "f \<in> S \<rightarrow> space M \<Longrightarrow> space (vimage_algebra M S f) = S"
 11.1528 +  using sigma_algebra.space_measure_of_eq[OF sigma_algebra_preimages, of f S M]
 11.1529 +  by (simp add: vimage_algebra_def)
 11.1530 +
 11.1531 +lemma in_vimage_algebra[simp]:
 11.1532 +  "f \<in> S \<rightarrow> space M \<Longrightarrow> A \<in> sets (vimage_algebra M S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
 11.1533 +  by (simp add: image_iff)
 11.1534 +
 11.1535 +lemma measurable_vimage_algebra:
 11.1536 +  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
 11.1537 +  shows "f \<in> measurable (vimage_algebra M S f) M"
 11.1538 +  unfolding measurable_def using assms by force
 11.1539 +
 11.1540 +lemma measurable_vimage:
 11.1541 +  fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a"
 11.1542 +  assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M"
 11.1543 +  shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra M S f) M2"
 11.1544 +proof -
 11.1545 +  note measurable_vimage_algebra[OF assms(2)]
 11.1546 +  from measurable_comp[OF this assms(1)]
 11.1547 +  show ?thesis by (simp add: comp_def)
 11.1548 +qed
 11.1549 +
 11.1550 +lemma sigma_sets_vimage:
 11.1551 +  assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
 11.1552 +  shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
 11.1553 +proof (intro set_eqI iffI)
 11.1554 +  let ?F = "\<lambda>X. f -` X \<inter> S'"
 11.1555 +  fix X assume "X \<in> sigma_sets S' (?F ` A)"
 11.1556 +  then show "X \<in> ?F ` sigma_sets S A"
 11.1557 +  proof induct
 11.1558 +    case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A"
 11.1559 +      by auto
 11.1560 +    then show ?case by auto
 11.1561 +  next
 11.1562 +    case Empty then show ?case
 11.1563 +      by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty)
 11.1564 +  next
 11.1565 +    case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A"
 11.1566 +      by auto
 11.1567 +    then have "S - X' \<in> sigma_sets S A"
 11.1568 +      by (auto intro!: sigma_sets.Compl)
 11.1569 +    then show ?case
 11.1570 +      using X assms by (auto intro!: image_eqI[where x="S - X'"])
 11.1571 +  next
 11.1572 +    case (Union F)
 11.1573 +    then have "\<forall>i. \<exists>F'.  F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'"
 11.1574 +      by (auto simp: image_iff Bex_def)
 11.1575 +    from choice[OF this] obtain F' where
 11.1576 +      "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'"
 11.1577 +      by auto
 11.1578 +    then show ?case
 11.1579 +      by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"])
 11.1580 +  qed
 11.1581 +next
 11.1582 +  let ?F = "\<lambda>X. f -` X \<inter> S'"
 11.1583 +  fix X assume "X \<in> ?F ` sigma_sets S A"
 11.1584 +  then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto
 11.1585 +  then show "X \<in> sigma_sets S' (?F ` A)"
 11.1586 +  proof (induct arbitrary: X)
 11.1587 +    case Empty then show ?case by (auto intro: sigma_sets.Empty)
 11.1588 +  next
 11.1589 +    case (Compl X')
 11.1590 +    have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)"
 11.1591 +      apply (rule sigma_sets.Compl)
 11.1592 +      using assms by (auto intro!: Compl.hyps simp: Compl.prems)
 11.1593 +    also have "S' - (S' - X) = X"
 11.1594 +      using assms Compl by auto
 11.1595 +    finally show ?case .
 11.1596 +  next
 11.1597 +    case (Union F)
 11.1598 +    have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)"
 11.1599 +      by (intro sigma_sets.Union Union.hyps) simp
 11.1600 +    also have "(\<Union>i. f -` F i \<inter> S') = X"
 11.1601 +      using assms Union by auto
 11.1602 +    finally show ?case .
 11.1603 +  qed auto
 11.1604 +qed
 11.1605 +
 11.1606 +subsubsection {* Restricted Space Sigma Algebra *}
 11.1607 +
 11.1608 +definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"
 11.1609 +
 11.1610 +lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega>"
 11.1611 +  unfolding restrict_space_def by (subst space_measure_of) auto
 11.1612 +
 11.1613 +lemma sets_restrict_space: "\<Omega> \<subseteq> space M \<Longrightarrow> sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
 11.1614 +  using sigma_sets_vimage[of "\<lambda>x. x" \<Omega> "space M" "sets M"]
 11.1615 +  unfolding restrict_space_def
 11.1616 +  by (subst sets_measure_of) (auto simp: sets.sigma_sets_eq Int_commute[of _ \<Omega>] sets.space_closed)
 11.1617 +
 11.1618 +lemma sets_restrict_space_iff:
 11.1619 +  "\<Omega> \<in> sets M \<Longrightarrow> A \<in> sets (restrict_space M \<Omega>) \<longleftrightarrow> (A \<subseteq> \<Omega> \<and> A \<in> sets M)"
 11.1620 +  by (subst sets_restrict_space) (auto dest: sets.sets_into_space)
 11.1621 +
 11.1622 +lemma measurable_restrict_space1:
 11.1623 +  assumes \<Omega>: "\<Omega> \<in> sets M" and f: "f \<in> measurable M N" shows "f \<in> measurable (restrict_space M \<Omega>) N"
 11.1624 +  unfolding measurable_def
 11.1625 +proof (intro CollectI conjI ballI)
 11.1626 +  show sp: "f \<in> space (restrict_space M \<Omega>) \<rightarrow> space N"
 11.1627 +    using measurable_space[OF f] sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
 11.1628 +
 11.1629 +  fix A assume "A \<in> sets N"
 11.1630 +  have "f -` A \<inter> space (restrict_space M \<Omega>) = (f -` A \<inter> space M) \<inter> \<Omega>"
 11.1631 +    using sets.sets_into_space[OF \<Omega>] by (auto simp: space_restrict_space)
 11.1632 +  also have "\<dots> \<in> sets (restrict_space M \<Omega>)"
 11.1633 +    unfolding sets_restrict_space_iff[OF \<Omega>]
 11.1634 +    using measurable_sets[OF f `A \<in> sets N`] \<Omega> by blast
 11.1635 +  finally show "f -` A \<inter> space (restrict_space M \<Omega>) \<in> sets (restrict_space M \<Omega>)" .
 11.1636 +qed
 11.1637 +
 11.1638 +lemma measurable_restrict_space2:
 11.1639 +  "\<Omega> \<in> sets N \<Longrightarrow> f \<in> space M \<rightarrow> \<Omega> \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> f \<in> measurable M (restrict_space N \<Omega>)"
 11.1640 +  by (simp add: measurable_def space_restrict_space sets_restrict_space_iff)
 11.1641 +
 11.1642  end
    12.1 --- a/src/HOL/Probability/document/root.tex	Mon May 19 12:04:45 2014 +0200
    12.2 +++ b/src/HOL/Probability/document/root.tex	Mon May 19 13:44:13 2014 +0200
    12.3 @@ -13,7 +13,7 @@
    12.4  
    12.5  \begin{document}
    12.6  
    12.7 -\title{Multivariate Analysis}
    12.8 +\title{Measure and Probability Theory}
    12.9  \maketitle
   12.10  
   12.11  \tableofcontents
    13.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Mon May 19 12:04:45 2014 +0200
    13.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Mon May 19 13:44:13 2014 +0200
    13.3 @@ -8,7 +8,7 @@
    13.4  lemma Ex1_eq: "\<exists>!x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
    13.5    by auto
    13.6  
    13.7 -section "Define the state space"
    13.8 +subsection {* Define the state space *}
    13.9  
   13.10  text {*
   13.11  
    14.1 --- a/src/HOL/ROOT	Mon May 19 12:04:45 2014 +0200
    14.2 +++ b/src/HOL/ROOT	Mon May 19 13:44:13 2014 +0200
    14.3 @@ -685,8 +685,9 @@
    14.4    options [document_graph]
    14.5    theories [document = false]
    14.6      "~~/src/HOL/Library/Countable"
    14.7 -    "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
    14.8      "~~/src/HOL/Library/Permutation"
    14.9 +    "~~/src/HOL/Library/Order_Continuity"
   14.10 +    "~~/src/HOL/Library/Diagonal_Subsequence"
   14.11    theories
   14.12      Probability
   14.13      "ex/Dining_Cryptographers"