src/HOL/Probability/Measure_Space.thy
 changeset 56994 8d5e5ec1cac3 parent 56212 3253aaf73a01 child 57025 e7fd64f82876
```     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Mon May 19 12:04:45 2014 +0200
1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Mon May 19 13:44:13 2014 +0200
1.3 @@ -73,7 +73,7 @@
1.4    represent sigma algebras (with an arbitrary emeasure).
1.5  *}
1.6
1.7 -section "Extend binary sets"
1.8 +subsection "Extend binary sets"
1.9
1.10  lemma LIMSEQ_binaryset:
1.11    assumes f: "f {} = 0"
1.12 @@ -105,7 +105,7 @@
1.13    shows "f {} = 0 \<Longrightarrow> (\<Sum>n. f (binaryset A B n)) = f A + f B"
1.14    by (metis binaryset_sums sums_unique)
1.15
1.16 -section {* Properties of a premeasure @{term \<mu>} *}
1.17 +subsection {* Properties of a premeasure @{term \<mu>} *}
1.18
1.19  text {*
1.20    The definitions for @{const positive} and @{const countably_additive} should be here, by they are
1.21 @@ -429,7 +429,7 @@
1.22    using empty_continuous_imp_continuous_from_below[OF f fin] cont
1.23    by blast
1.24
1.25 -section {* Properties of @{const emeasure} *}
1.26 +subsection {* Properties of @{const emeasure} *}
1.27
1.28  lemma emeasure_positive: "positive (sets M) (emeasure M)"
1.29    by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
1.30 @@ -761,7 +761,7 @@
1.32  qed simp_all
1.33
1.34 -section "@{text \<mu>}-null sets"
1.35 +subsection {* @{text \<mu>}-null sets *}
1.36
1.37  definition null_sets :: "'a measure \<Rightarrow> 'a set set" where
1.38    "null_sets M = {N\<in>sets M. emeasure M N = 0}"
1.39 @@ -853,7 +853,7 @@
1.40      by (subst plus_emeasure[symmetric]) auto
1.41  qed
1.42
1.43 -section "Formalize almost everywhere"
1.44 +subsection {* The almost everywhere filter (i.e.\ quantifier) *}
1.45
1.46  definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
1.47    "ae_filter M = Abs_filter (\<lambda>P. \<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N)"
1.48 @@ -1053,7 +1053,7 @@
1.49    shows "emeasure M A = emeasure M B"
1.50    using assms by (safe intro!: antisym emeasure_mono_AE) auto
1.51
1.52 -section {* @{text \<sigma>}-finite Measures *}
1.53 +subsection {* @{text \<sigma>}-finite Measures *}
1.54
1.55  locale sigma_finite_measure =
1.56    fixes M :: "'a measure"
1.57 @@ -1103,7 +1103,7 @@
1.58    qed (force simp: incseq_def)+
1.59  qed
1.60
1.61 -section {* Measure space induced by distribution of @{const measurable}-functions *}
1.62 +subsection {* Measure space induced by distribution of @{const measurable}-functions *}
1.63
1.64  definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
1.65    "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
1.66 @@ -1187,7 +1187,7 @@
1.67    by (auto simp add: emeasure_distr measurable_space
1.68             intro!: arg_cong[where f="emeasure M"] measure_eqI)
1.69
1.70 -section {* Real measure values *}
1.71 +subsection {* Real measure values *}
1.72
1.73  lemma measure_nonneg: "0 \<le> measure M A"
1.74    using emeasure_nonneg[of M A] unfolding measure_def by (auto intro: real_of_ereal_pos)
1.75 @@ -1324,7 +1324,7 @@
1.76      by (intro lim_real_of_ereal) simp
1.77  qed
1.78
1.79 -section {* Measure spaces with @{term "emeasure M (space M) < \<infinity>"} *}
1.80 +subsection {* Measure spaces with @{term "emeasure M (space M) < \<infinity>"} *}
1.81
1.82  locale finite_measure = sigma_finite_measure M for M +
1.83    assumes finite_emeasure_space: "emeasure M (space M) \<noteq> \<infinity>"
1.84 @@ -1527,7 +1527,7 @@
1.85    shows "measure M B = 0"
1.86    using measure_space_inter[of B A] assms by (auto simp: ac_simps)
1.87
1.88 -section {* Counting space *}
1.89 +subsection {* Counting space *}
1.90
1.91  lemma strict_monoI_Suc:
1.92    assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
1.93 @@ -1653,7 +1653,7 @@
1.94    show "sigma_finite_measure (count_space A)" ..
1.95  qed
1.96
1.97 -section {* Measure restricted to space *}
1.98 +subsection {* Measure restricted to space *}
1.99
1.100  lemma emeasure_restrict_space:
1.101    assumes "\<Omega> \<in> sets M" "A \<subseteq> \<Omega>"
```