src/HOL/Probability/Lebesgue_Integration.thy
 changeset 50002 ce0d316b5b44 parent 50001 382bd3173584 child 50003 8c213922ed49
```     1.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:00:39 2012 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 02 14:23:40 2012 +0100
1.3 @@ -70,7 +70,7 @@
1.4    have "g -` X \<inter> space M = g -` (X \<inter> g`space M) \<inter> space M" by auto
1.5    also have "\<dots> = (\<Union>x\<in>X \<inter> g`space M. g-`{x} \<inter> space M)" by auto
1.6    finally show "g -` X \<inter> space M \<in> sets M" using assms
1.7 -    by (auto intro!: finite_UN simp del: UN_simps simp: simple_function_def)
1.8 +    by (auto simp del: UN_simps simp: simple_function_def)
1.9  qed
1.10
1.11  lemma simple_function_measurable2[intro]:
1.12 @@ -167,7 +167,7 @@
1.13      (\<Union>x\<in>?G. f -` {x} \<inter> space M)" by auto
1.14    show "(g \<circ> f) -` {(g \<circ> f) x} \<inter> space M \<in> sets M"
1.15      using assms unfolding simple_function_def *
1.16 -    by (rule_tac finite_UN) (auto intro!: finite_UN)
1.17 +    by (rule_tac finite_UN) auto
1.18  qed
1.19
1.20  lemma simple_function_indicator[intro, simp]:
1.21 @@ -1210,7 +1210,7 @@
1.22      case (insert i P)
1.23      then have "f i \<in> borel_measurable M" "AE x in M. 0 \<le> f i x"
1.24        "(\<lambda>x. \<Sum>i\<in>P. f i x) \<in> borel_measurable M" "AE x in M. 0 \<le> (\<Sum>i\<in>P. f i x)"
1.25 -      by (auto intro!: borel_measurable_ereal_setsum setsum_nonneg)
1.26 +      by (auto intro!: setsum_nonneg)
1.28      show ?case using insert by auto
1.29    qed simp
1.30 @@ -1230,7 +1230,7 @@
1.31        simp: indicator_def ereal_zero_le_0_iff)
1.32    also have "\<dots> = c * (\<integral>\<^isup>+ x. u x * indicator A x \<partial>M)"
1.33      using assms
1.34 -    by (auto intro!: positive_integral_cmult borel_measurable_indicator simp: ereal_zero_le_0_iff)
1.35 +    by (auto intro!: positive_integral_cmult simp: ereal_zero_le_0_iff)
1.36    finally show ?thesis .
1.37  qed
1.38
1.39 @@ -1633,7 +1633,7 @@
1.40  lemma integral_zero[simp, intro]:
1.41    shows "integrable M (\<lambda>x. 0)" "(\<integral> x.0 \<partial>M) = 0"
1.42    unfolding integrable_def lebesgue_integral_def
1.43 -  by (auto simp add: borel_measurable_const)
1.44 +  by auto
1.45
1.46  lemma integral_cmult[simp, intro]:
1.47    assumes "integrable M f"
1.48 @@ -1644,7 +1644,7 @@
1.49    proof (cases rule: le_cases)
1.50      assume "0 \<le> a" show ?thesis
1.51        using integral_linear[OF assms integral_zero(1) `0 \<le> a`]
1.52 -      by (simp add: integral_zero)
1.53 +      by simp
1.54    next
1.55      assume "a \<le> 0" hence "0 \<le> - a" by auto
1.56      have *: "\<And>t. - a * t + 0 = (-a) * t" by simp
1.57 @@ -1718,7 +1718,7 @@
1.58      by (auto split: split_indicator simp: positive_integral_0_iff_AE one_ereal_def)
1.59    show ?int ?able
1.60      using assms unfolding lebesgue_integral_def integrable_def
1.61 -    by (auto simp: * positive_integral_indicator borel_measurable_indicator)
1.62 +    by (auto simp: *)
1.63  qed
1.64
1.65  lemma integral_cmul_indicator:
1.66 @@ -1850,7 +1850,7 @@
1.67    assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
1.68    shows "0 \<le> integral\<^isup>L M f"
1.69  proof -
1.70 -  have "0 = (\<integral>x. 0 \<partial>M)" by (auto simp: integral_zero)
1.71 +  have "0 = (\<integral>x. 0 \<partial>M)" by auto
1.72    also have "\<dots> \<le> integral\<^isup>L M f"
1.73      using assms by (rule integral_mono[OF integral_zero(1)])
1.74    finally show ?thesis .
1.75 @@ -2206,7 +2206,7 @@
1.76      let ?F = "\<lambda>n y. (\<Sum>i = 0..<n. \<bar>f i y\<bar>)"
1.77      let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
1.78      have "\<And>n. integrable M (?F n)"
1.79 -      using borel by (auto intro!: integral_setsum integrable_abs)
1.80 +      using borel by (auto intro!: integrable_abs)
1.81      thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
1.82      show "AE x in M. mono (\<lambda>n. ?w' n x)"
1.83        by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
1.84 @@ -2436,7 +2436,7 @@
1.85    by (subst density_max_0) (auto intro!: arg_cong[where f="density M"] split: split_max)
1.86
1.87  lemma emeasure_density:
1.88 -  assumes f: "f \<in> borel_measurable M" and A: "A \<in> sets M"
1.89 +  assumes f[measurable]: "f \<in> borel_measurable M" and A[measurable]: "A \<in> sets M"
1.90    shows "emeasure (density M f) A = (\<integral>\<^isup>+ x. f x * indicator A x \<partial>M)"
1.91      (is "_ = ?\<mu> A")
1.92    unfolding density_def
1.93 @@ -2453,8 +2453,9 @@
1.94      unfolding \<mu>_eq
1.96      fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M"
1.97 +    then have "\<And>i. A i \<in> sets M" by auto
1.98      then have *: "\<And>i. (\<lambda>x. max 0 (f x) * indicator (A i) x) \<in> borel_measurable M"
1.99 -      using f by (auto intro!: borel_measurable_ereal_times)
1.100 +      by (auto simp: set_eq_iff)
1.101      assume disj: "disjoint_family A"
1.102      have "(\<Sum>n. ?\<mu>' (A n)) = (\<integral>\<^isup>+ x. (\<Sum>n. max 0 (f x) * indicator (A n) x) \<partial>M)"
1.103        using f * by (simp add: positive_integral_suminf)
1.104 @@ -2483,8 +2484,7 @@
1.105        by (intro positive_integral_0_iff) auto
1.106      also have "\<dots> \<longleftrightarrow> (AE x in M. max 0 (f x) * indicator A x = 0)"
1.107        using f `A \<in> sets M`
1.108 -      by (intro AE_iff_measurable[OF _ refl, symmetric])
1.109 -         (auto intro!: sets_Collect borel_measurable_ereal_eq)
1.110 +      by (intro AE_iff_measurable[OF _ refl, symmetric]) auto
1.111      also have "(AE x in M. max 0 (f x) * indicator A x = 0) \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)"
1.112        by (auto simp add: indicator_def max_def split: split_if_asm)
1.113      finally have "(\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = 0 \<longleftrightarrow> (AE x in M. x \<in> A \<longrightarrow> f x \<le> 0)" . }
1.114 @@ -2649,7 +2649,7 @@
1.115    "finite A \<Longrightarrow>
1.116     g \<in> measurable M (point_measure A f) \<longleftrightarrow>
1.117      (g \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. g -` {a} \<inter> space M \<in> sets M))"
1.118 -  unfolding point_measure_def by simp
1.119 +  unfolding point_measure_def by (simp add: measurable_count_space_eq2)
1.120
1.121  lemma simple_function_point_measure[simp]:
1.122    "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)"
```