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.27      from positive_integral_add[OF this]
    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.95    proof (intro countably_additiveI)
    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)"