src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy

 
 lemma indicator_less_ereal[simp]:
   "indicator A x \<le> (indicator B x::ereal) \<longleftrightarrow> (x \<in> A \<longrightarrow> x \<in> B)"
   by (simp add: indicator_def not_le)
 
-section "Simple function"
+subsection "Simple function"
 
 text {*
 
 Our simple functions are not restricted to positive real numbers. Instead
 they are just functions with a finite range and are measurable when singleton

   also have "T -` (f -` {i} \<inter> space M') \<inter> space M = (\<lambda>x. f (T x)) -` {i} \<inter> space M"
     using T unfolding measurable_def by auto
   finally show "(\<lambda>x. f (T x)) -` {i} \<inter> space M \<in> sets M" .
 qed
 
-section "Simple integral"
+subsection "Simple integral"
 
 definition simple_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>S") where
   "integral\<^sup>S M f = (\<Sum>x \<in> f ` space M. x * emeasure M (f -` {x} \<inter> space M))"
 
 syntax

   have "integral\<^sup>S M (\<lambda>x. 0) \<le> integral\<^sup>S M f"
     using simple_integral_mono_AE[OF _ f ae] by auto
   then show ?thesis by simp
 qed
 
-section "Continuous positive integration"
+subsection {* Integral on nonnegative functions *}
 
 definition positive_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> ereal" ("integral\<^sup>P") where
   "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f}. integral\<^sup>S M g)"
 
 syntax

     by (simp add: positive_integral_suminf)
   finally show ?thesis
     by (simp add: F_def)
 qed
 
-section {* Distributions *}
+subsection {* Integral under concrete measures *}
+
+subsubsection {* Distributions *}
 
 lemma positive_integral_distr':
   assumes T: "T \<in> measurable M M'"
   and f: "f \<in> borel_measurable (distr M M' T)" "\<And>x. 0 \<le> f x"
   shows "integral\<^sup>P (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"

 lemma positive_integral_distr:
   "T \<in> measurable M M' \<Longrightarrow> f \<in> borel_measurable M' \<Longrightarrow> integral\<^sup>P (distr M M' T) f = (\<integral>\<^sup>+ x. f (T x) \<partial>M)"
   by (subst (1 2) positive_integral_max_0[symmetric])
      (simp add: positive_integral_distr')
 
-section {* Lebesgue integration on @{const count_space} *}
+subsubsection {* Counting space *}
 
 lemma simple_function_count_space[simp]:
   "simple_function (count_space A) f \<longleftrightarrow> finite (f ` A)"
   unfolding simple_function_def by simp
 

     finally show "(\<Sum>i. emeasure M (X x) * indicator {from_nat_into I i} x) = emeasure M (X x)" .
   qed
   finally show ?thesis .
 qed
 
-section {* Measures with Restricted Space *}
+subsubsection {* Measures with Restricted Space *}
 
 lemma positive_integral_restrict_space:
   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"
   shows "positive_integral (restrict_space M \<Omega>) f = positive_integral M f"
 using f proof (induct rule: borel_measurable_induct)

 next
   case (seq F) then show ?case
     by (auto simp add: SUP_eq_iff measurable_restrict_space1 \<Omega> positive_integral_monotone_convergence_SUP)
 qed
 
-section {* Measure spaces with an associated density *}
+subsubsection {* Measure spaces with an associated density *}
 
 definition density :: "'a measure \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
   "density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^sup>+ x. f x * indicator A x \<partial>M)"
 
 lemma 

     using f g ac by (auto intro!: density_cong measurable_If)
   then show ?thesis
     using f g by (subst density_density_eq) auto
 qed
 
-section {* Point measure *}
+subsubsection {* Point measure *}
 
 definition point_measure :: "'a set \<Rightarrow> ('a \<Rightarrow> ereal) \<Rightarrow> 'a measure" where
   "point_measure A f = density (count_space A) f"
 
 lemma

 lemma positive_integral_point_measure_finite:
   "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> f a) \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> 0 \<le> g a) \<Longrightarrow>
     integral\<^sup>P (point_measure A f) g = (\<Sum>a\<in>A. f a * g a)"
   by (subst positive_integral_point_measure) (auto intro!: setsum_mono_zero_left simp: less_le)
 
-section {* Uniform measure *}
+subsubsection {* Uniform measure *}
 
 definition "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)"
 
 lemma
   shows sets_uniform_measure[simp]: "sets (uniform_measure M A) = sets M"

   assumes A: "emeasure M A \<noteq> 0" "emeasure M A \<noteq> \<infinity>" and B: "B \<in> sets M"
   shows "measure (uniform_measure M A) B = measure M (A \<inter> B) / measure M A"
   using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)] B] A
   by (cases "emeasure M A" "emeasure M (A \<inter> B)" rule: ereal2_cases) (simp_all add: measure_def)
 
-section {* Uniform count measure *}
+subsubsection {* Uniform count measure *}
 
 definition "uniform_count_measure A = point_measure A (\<lambda>x. 1 / card A)"
  
 lemma 
   shows space_uniform_count_measure: "space (uniform_count_measure A) = A"