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.31      by (simp add: emeasure_countably_additive)
    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>"