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 * .