src/HOL/Probability/Borel_Space.thy
 changeset 41097 a1abfa4e2b44 parent 41096 843c40bbc379 child 41545 9c869baf1c66
```     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 16:15:14 2010 +0100
1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 08 19:32:11 2010 +0100
1.3 @@ -1395,7 +1395,7 @@
1.4  lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]:
1.5    fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> pextreal"
1.6    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
1.7 -  shows "(SUP i : A. f i) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
1.8 +  shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
1.9    unfolding borel_measurable_pextreal_iff_greater
1.10  proof safe
1.11    fix a
1.12 @@ -1408,7 +1408,7 @@
1.13  lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:
1.14    fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> pextreal"
1.15    assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
1.16 -  shows "(INF i : A. f i) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
1.17 +  shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
1.18    unfolding borel_measurable_pextreal_iff_less
1.19  proof safe
1.20    fix a
1.21 @@ -1432,20 +1432,10 @@
1.22      using assms by auto
1.23  qed
1.24
1.25 -lemma INFI_fun_expand:
1.26 -  "(INF y:A. f y) = (\<lambda>x. (INF y:A. f y x))"
1.27 -  by (simp add: fun_eq_iff INFI_apply)
1.28 -
1.29 -lemma SUPR_fun_expand:
1.30 -  "(SUP y:A. f y) = (\<lambda>x. (SUP y:A. f y x))"
1.31 -  by (simp add: fun_eq_iff SUPR_apply)
1.32 -
1.33  lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
1.34    assumes "\<And>i. f i \<in> borel_measurable M"
1.35    shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
1.36 -  using assms unfolding psuminf_def
1.37 -  by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])
1.38 -
1.39 +  using assms unfolding psuminf_def by auto
1.40
1.41  section "LIMSEQ is borel measurable"
1.42
1.43 @@ -1468,13 +1458,12 @@
1.44    note eq = this
1.45    have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x"
1.46      by auto
1.47 -  have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M"
1.48 -       "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M"
1.49 -    using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)
1.50 +  have "(\<lambda>x. SUP n. INF m. Real (u (n + m) x)) \<in> borel_measurable M"
1.51 +       "(\<lambda>x. SUP n. INF m. Real (- u (n + m) x)) \<in> borel_measurable M"
1.52 +    using u by auto
1.53    with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
1.54    have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
1.55 -       "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
1.56 -    unfolding SUPR_fun_expand INFI_fun_expand by auto
1.57 +       "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M" by auto
1.58    note this[THEN borel_measurable_real]
1.59    from borel_measurable_diff[OF this]
1.60    show ?thesis unfolding * .
```