use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
authorhoelzl
Wed Dec 08 19:32:11 2010 +0100 (2010-12-08)
changeset 41097a1abfa4e2b44
parent 41096 843c40bbc379
child 41098 ababba14c965
use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Complete_Measure.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Probability_Space.thy
src/HOL/Probability/Product_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
     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 * .
     2.1 --- a/src/HOL/Probability/Complete_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
     2.2 +++ b/src/HOL/Probability/Complete_Measure.thy	Wed Dec 08 19:32:11 2010 +0100
     2.3 @@ -257,17 +257,14 @@
     2.4    show ?thesis
     2.5    proof (intro bexI)
     2.6      from AE[unfolded all_AE_countable]
     2.7 -    show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
     2.8 +    show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
     2.9      proof (rule AE_mp, safe intro!: AE_cong)
    2.10        fix x assume eq: "\<forall>i. f i x = f' i x"
    2.11 -      have "g x = (SUP i. f i x)"
    2.12 -        using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
    2.13 -      then show "g x = ?f x"
    2.14 -        using eq unfolding SUPR_fun_expand by auto
    2.15 +      moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
    2.16 +      ultimately show "g x = ?f x" by (simp add: SUPR_apply)
    2.17      qed
    2.18      show "?f \<in> borel_measurable M"
    2.19 -      using sf by (auto intro!: borel_measurable_SUP
    2.20 -        intro: borel_measurable_simple_function)
    2.21 +      using sf by (auto intro: borel_measurable_simple_function)
    2.22    qed
    2.23  qed
    2.24  
     3.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 08 16:15:14 2010 +0100
     3.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Dec 08 19:32:11 2010 +0100
     3.3 @@ -1176,8 +1176,6 @@
     3.4      apply (rule positive_integral_mono)
     3.5      using `f \<up> u` unfolding isoton_def le_fun_def by auto
     3.6  next
     3.7 -  have "u \<in> borel_measurable M"
     3.8 -    using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def)
     3.9    have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto
    3.10  
    3.11    show "(SUP i. positive_integral (f i)) = positive_integral u"
    3.12 @@ -1198,8 +1196,6 @@
    3.13    shows "(SUP i. positive_integral (f i)) = positive_integral (\<lambda>x. SUP i. f i x)"
    3.14      (is "_ = positive_integral ?u")
    3.15  proof -
    3.16 -  have "?u \<in> borel_measurable M"
    3.17 -    using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand)
    3.18    show ?thesis
    3.19    proof (rule antisym)
    3.20      show "(SUP j. positive_integral (f j)) \<le> positive_integral ?u"
    3.21 @@ -1209,9 +1205,9 @@
    3.22      have "\<And>i. rf i \<in> borel_measurable M" unfolding rf_def
    3.23        using assms by (simp cong: measurable_cong)
    3.24      moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def
    3.25 -      unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff
    3.26 +      unfolding isoton_def le_fun_def fun_eq_iff SUPR_apply
    3.27        using SUP_const[OF UNIV_not_empty]
    3.28 -      by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff)
    3.29 +      by (auto simp: restrict_def le_fun_def fun_eq_iff)
    3.30      ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))"
    3.31        unfolding positive_integral_alt[of ru]
    3.32        by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx)
    3.33 @@ -1354,24 +1350,16 @@
    3.34  lemma (in measure_space) positive_integral_lim_INF:
    3.35    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pextreal"
    3.36    assumes "\<And>i. u i \<in> borel_measurable M"
    3.37 -  shows "positive_integral (SUP n. INF m. u (m + n)) \<le>
    3.38 +  shows "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x) \<le>
    3.39      (SUP n. INF m. positive_integral (u (m + n)))"
    3.40  proof -
    3.41 -  have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M"
    3.42 -    by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
    3.43 -
    3.44 -  have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
    3.45 -  proof (unfold isoton_def, safe intro!: INF_mono bexI)
    3.46 -    fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
    3.47 -  qed simp
    3.48 -  from positive_integral_isoton[OF this] assms
    3.49 -  have "positive_integral (SUP n. INF m. u (m + n)) =
    3.50 -    (SUP n. positive_integral (INF m. u (m + n)))"
    3.51 -    unfolding isoton_def by (simp add: borel_measurable_INF)
    3.52 +  have "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x)
    3.53 +      = (SUP n. positive_integral (\<lambda>x. INF m. u (m + n) x))"
    3.54 +    using assms
    3.55 +    by (intro positive_integral_monotone_convergence_SUP[symmetric] INF_mono)
    3.56 +       (auto simp del: add_Suc simp add: add_Suc[symmetric])
    3.57    also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
    3.58 -    apply (rule SUP_mono)
    3.59 -    apply (rule_tac x=n in bexI)
    3.60 -    by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
    3.61 +    by (auto intro!: SUP_mono bexI le_INFI positive_integral_mono INF_leI)
    3.62    finally show ?thesis .
    3.63  qed
    3.64  
    3.65 @@ -1960,10 +1948,10 @@
    3.66  
    3.67    have borel_f: "\<And>i. (\<lambda>x. Real (f i x)) \<in> borel_measurable M"
    3.68      using i unfolding integrable_def by auto
    3.69 -  hence "(SUP i. (\<lambda>x. Real (f i x))) \<in> borel_measurable M"
    3.70 +  hence "(\<lambda>x. SUP i. Real (f i x)) \<in> borel_measurable M"
    3.71      by auto
    3.72    hence borel_u: "u \<in> borel_measurable M"
    3.73 -    using pos_u by (auto simp: borel_measurable_Real_eq SUPR_fun_expand SUP_F)
    3.74 +    using pos_u by (auto simp: borel_measurable_Real_eq SUP_F)
    3.75  
    3.76    have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))"
    3.77      using i unfolding integral_def integrable_def by (auto simp: Real_real)
    3.78 @@ -2144,8 +2132,8 @@
    3.79      thus ?thesis by simp
    3.80    next
    3.81      assume neq_0: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> 0"
    3.82 -    have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (SUP n. INF m. (\<lambda>x. Real (?diff (m + n) x)))"
    3.83 -    proof (rule positive_integral_cong, unfold SUPR_fun_expand INFI_fun_expand, subst add_commute)
    3.84 +    have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (\<lambda>x. SUP n. INF m. Real (?diff (m + n) x))"
    3.85 +    proof (rule positive_integral_cong, subst add_commute)
    3.86        fix x assume x: "x \<in> space M"
    3.87        show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))"
    3.88        proof (rule LIMSEQ_imp_lim_INF[symmetric])
     4.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
     4.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 08 19:32:11 2010 +0100
     4.3 @@ -552,10 +552,10 @@
     4.4  proof -
     4.5    from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
     4.6    show ?ilim using mono lim i by auto
     4.7 -  have "(SUP i. f i) = u" using mono lim SUP_Lim_pextreal
     4.8 -    unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
     4.9 -  moreover have "(SUP i. f i) \<in> borel_measurable M"
    4.10 -    using i by (rule borel_measurable_SUP)
    4.11 +  have "\<And>x. (SUP i. f i x) = u x" using mono lim SUP_Lim_pextreal
    4.12 +    unfolding fun_eq_iff mono_def by auto
    4.13 +  moreover have "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
    4.14 +    using i by auto
    4.15    ultimately show "u \<in> borel_measurable M" by simp
    4.16  qed
    4.17  
     5.1 --- a/src/HOL/Probability/Probability_Space.thy	Wed Dec 08 16:15:14 2010 +0100
     5.2 +++ b/src/HOL/Probability/Probability_Space.thy	Wed Dec 08 19:32:11 2010 +0100
     5.3 @@ -1069,13 +1069,13 @@
     5.4  
     5.5    show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
     5.6    proof (intro ballI bexI)
     5.7 -    show "(SUP i. g i) \<in> borel_measurable M'"
     5.8 +    show "(\<lambda>x. SUP i. g i x) \<in> borel_measurable M'"
     5.9        using g by (auto intro: M'.borel_measurable_simple_function)
    5.10      fix x assume "x \<in> space M"
    5.11      have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
    5.12 -    also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
    5.13 +    also have "\<dots> = (SUP i. g i (Y x))" unfolding SUPR_apply
    5.14        using g `x \<in> space M` by simp
    5.15 -    finally show "Z x = (SUP i. g i) (Y x)" .
    5.16 +    finally show "Z x = (SUP i. g i (Y x))" .
    5.17    qed
    5.18  qed
    5.19  
     6.1 --- a/src/HOL/Probability/Product_Measure.thy	Wed Dec 08 16:15:14 2010 +0100
     6.2 +++ b/src/HOL/Probability/Product_Measure.thy	Wed Dec 08 19:32:11 2010 +0100
     6.3 @@ -767,11 +767,11 @@
     6.4    then have F_borel: "\<And>i. F i \<in> borel_measurable P"
     6.5      and F_mono: "\<And>i x. F i x \<le> F (Suc i) x"
     6.6      and F_SUPR: "\<And>x. (SUP i. F i x) = f x"
     6.7 -    unfolding isoton_def le_fun_def SUPR_fun_expand
     6.8 +    unfolding isoton_fun_expand unfolding isoton_def le_fun_def
     6.9      by (auto intro: borel_measurable_simple_function)
    6.10    note sf = simple_function_cut[OF F(1)]
    6.11 -  then have "(SUP i. ?C (F i)) \<in> borel_measurable M1"
    6.12 -    using F(1) by (auto intro!: M1.borel_measurable_SUP)
    6.13 +  then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1"
    6.14 +    using F(1) by auto
    6.15    moreover
    6.16    { fix x assume "x \<in> space M1"
    6.17      have isotone: "(\<lambda> i y. F i (x, y)) \<up> (\<lambda>y. f (x, y))"
    6.18 @@ -783,7 +783,7 @@
    6.19        by (simp add: isoton_def) }
    6.20    note SUPR_C = this
    6.21    ultimately show "?C f \<in> borel_measurable M1"
    6.22 -    unfolding SUPR_fun_expand by (simp cong: measurable_cong)
    6.23 +    by (simp cong: measurable_cong)
    6.24    have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))"
    6.25      using F_borel F_mono
    6.26      by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])
     7.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 08 16:15:14 2010 +0100
     7.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Dec 08 19:32:11 2010 +0100
     7.3 @@ -323,9 +323,10 @@
     7.4    { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
     7.5      have "g \<in> G" unfolding G_def
     7.6      proof safe
     7.7 -      from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
     7.8 +      from `f \<up> g` have [simp]: "g = (\<lambda>x. SUP i. f i x)"
     7.9 +        unfolding isoton_def fun_eq_iff SUPR_apply by simp
    7.10        have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
    7.11 -      thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
    7.12 +      thus "g \<in> borel_measurable M" by auto
    7.13        fix A assume "A \<in> sets M"
    7.14        hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
    7.15          using f_borel by (auto intro!: borel_measurable_indicator)