--- a/src/HOL/Probability/Borel_Space.thy Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Wed Dec 08 19:32:11 2010 +0100
@@ -1395,7 +1395,7 @@
lemma (in sigma_algebra) borel_measurable_SUP[simp, intro]:
fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> pextreal"
assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
- shows "(SUP i : A. f i) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
+ shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
unfolding borel_measurable_pextreal_iff_greater
proof safe
fix a
@@ -1408,7 +1408,7 @@
lemma (in sigma_algebra) borel_measurable_INF[simp, intro]:
fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> pextreal"
assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
- shows "(INF i : A. f i) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
+ shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
unfolding borel_measurable_pextreal_iff_less
proof safe
fix a
@@ -1432,20 +1432,10 @@
using assms by auto
qed
-lemma INFI_fun_expand:
- "(INF y:A. f y) = (\<lambda>x. (INF y:A. f y x))"
- by (simp add: fun_eq_iff INFI_apply)
-
-lemma SUPR_fun_expand:
- "(SUP y:A. f y) = (\<lambda>x. (SUP y:A. f y x))"
- by (simp add: fun_eq_iff SUPR_apply)
-
lemma (in sigma_algebra) borel_measurable_psuminf[simp, intro]:
assumes "\<And>i. f i \<in> borel_measurable M"
shows "(\<lambda>x. (\<Sum>\<^isub>\<infinity> i. f i x)) \<in> borel_measurable M"
- using assms unfolding psuminf_def
- by (auto intro!: borel_measurable_SUP [unfolded SUPR_fun_expand])
-
+ using assms unfolding psuminf_def by auto
section "LIMSEQ is borel measurable"
@@ -1468,13 +1458,12 @@
note eq = this
have *: "\<And>x. real (Real (u' x)) - real (Real (- u' x)) = u' x"
by auto
- have "(SUP n. INF m. (\<lambda>x. Real (u (n + m) x))) \<in> borel_measurable M"
- "(SUP n. INF m. (\<lambda>x. Real (- u (n + m) x))) \<in> borel_measurable M"
- using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real)
+ have "(\<lambda>x. SUP n. INF m. Real (u (n + m) x)) \<in> borel_measurable M"
+ "(\<lambda>x. SUP n. INF m. Real (- u (n + m) x)) \<in> borel_measurable M"
+ using u by auto
with eq[THEN measurable_cong, of M "\<lambda>x. x" borel]
have "(\<lambda>x. Real (u' x)) \<in> borel_measurable M"
- "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M"
- unfolding SUPR_fun_expand INFI_fun_expand by auto
+ "(\<lambda>x. Real (- u' x)) \<in> borel_measurable M" by auto
note this[THEN borel_measurable_real]
from borel_measurable_diff[OF this]
show ?thesis unfolding * .
--- a/src/HOL/Probability/Complete_Measure.thy Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Complete_Measure.thy Wed Dec 08 19:32:11 2010 +0100
@@ -257,17 +257,14 @@
show ?thesis
proof (intro bexI)
from AE[unfolded all_AE_countable]
- show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
+ show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
proof (rule AE_mp, safe intro!: AE_cong)
fix x assume eq: "\<forall>i. f i x = f' i x"
- have "g x = (SUP i. f i x)"
- using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
- then show "g x = ?f x"
- using eq unfolding SUPR_fun_expand by auto
+ moreover have "g = SUPR UNIV f" using `f \<up> g` unfolding isoton_def by simp
+ ultimately show "g x = ?f x" by (simp add: SUPR_apply)
qed
show "?f \<in> borel_measurable M"
- using sf by (auto intro!: borel_measurable_SUP
- intro: borel_measurable_simple_function)
+ using sf by (auto intro: borel_measurable_simple_function)
qed
qed
--- a/src/HOL/Probability/Lebesgue_Integration.thy Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Wed Dec 08 19:32:11 2010 +0100
@@ -1176,8 +1176,6 @@
apply (rule positive_integral_mono)
using `f \<up> u` unfolding isoton_def le_fun_def by auto
next
- have "u \<in> borel_measurable M"
- using borel_measurable_SUP[of UNIV f] assms by (auto simp: isoton_def)
have u: "u = (SUP i. f i)" using `f \<up> u` unfolding isoton_def by auto
show "(SUP i. positive_integral (f i)) = positive_integral u"
@@ -1198,8 +1196,6 @@
shows "(SUP i. positive_integral (f i)) = positive_integral (\<lambda>x. SUP i. f i x)"
(is "_ = positive_integral ?u")
proof -
- have "?u \<in> borel_measurable M"
- using borel_measurable_SUP[of _ f] assms by (simp add: SUPR_fun_expand)
show ?thesis
proof (rule antisym)
show "(SUP j. positive_integral (f j)) \<le> positive_integral ?u"
@@ -1209,9 +1205,9 @@
have "\<And>i. rf i \<in> borel_measurable M" unfolding rf_def
using assms by (simp cong: measurable_cong)
moreover have iso: "rf \<up> ru" using assms unfolding rf_def ru_def
- unfolding isoton_def SUPR_fun_expand le_fun_def fun_eq_iff
+ unfolding isoton_def le_fun_def fun_eq_iff SUPR_apply
using SUP_const[OF UNIV_not_empty]
- by (auto simp: restrict_def le_fun_def SUPR_fun_expand fun_eq_iff)
+ by (auto simp: restrict_def le_fun_def fun_eq_iff)
ultimately have "positive_integral ru \<le> (SUP i. positive_integral (rf i))"
unfolding positive_integral_alt[of ru]
by (auto simp: le_fun_def intro!: SUP_leI positive_integral_SUP_approx)
@@ -1354,24 +1350,16 @@
lemma (in measure_space) positive_integral_lim_INF:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> pextreal"
assumes "\<And>i. u i \<in> borel_measurable M"
- shows "positive_integral (SUP n. INF m. u (m + n)) \<le>
+ shows "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x) \<le>
(SUP n. INF m. positive_integral (u (m + n)))"
proof -
- have "(SUP n. INF m. u (m + n)) \<in> borel_measurable M"
- by (auto intro!: borel_measurable_SUP borel_measurable_INF assms)
-
- have "(\<lambda>n. INF m. u (m + n)) \<up> (SUP n. INF m. u (m + n))"
- proof (unfold isoton_def, safe intro!: INF_mono bexI)
- fix i m show "u (Suc m + i) \<le> u (m + Suc i)" by simp
- qed simp
- from positive_integral_isoton[OF this] assms
- have "positive_integral (SUP n. INF m. u (m + n)) =
- (SUP n. positive_integral (INF m. u (m + n)))"
- unfolding isoton_def by (simp add: borel_measurable_INF)
+ have "positive_integral (\<lambda>x. SUP n. INF m. u (m + n) x)
+ = (SUP n. positive_integral (\<lambda>x. INF m. u (m + n) x))"
+ using assms
+ by (intro positive_integral_monotone_convergence_SUP[symmetric] INF_mono)
+ (auto simp del: add_Suc simp add: add_Suc[symmetric])
also have "\<dots> \<le> (SUP n. INF m. positive_integral (u (m + n)))"
- apply (rule SUP_mono)
- apply (rule_tac x=n in bexI)
- by (auto intro!: positive_integral_mono INFI_bound INF_leI exI simp: INFI_fun_expand)
+ by (auto intro!: SUP_mono bexI le_INFI positive_integral_mono INF_leI)
finally show ?thesis .
qed
@@ -1960,10 +1948,10 @@
have borel_f: "\<And>i. (\<lambda>x. Real (f i x)) \<in> borel_measurable M"
using i unfolding integrable_def by auto
- hence "(SUP i. (\<lambda>x. Real (f i x))) \<in> borel_measurable M"
+ hence "(\<lambda>x. SUP i. Real (f i x)) \<in> borel_measurable M"
by auto
hence borel_u: "u \<in> borel_measurable M"
- using pos_u by (auto simp: borel_measurable_Real_eq SUPR_fun_expand SUP_F)
+ using pos_u by (auto simp: borel_measurable_Real_eq SUP_F)
have integral_eq: "\<And>n. positive_integral (\<lambda>x. Real (f n x)) = Real (integral (f n))"
using i unfolding integral_def integrable_def by (auto simp: Real_real)
@@ -2144,8 +2132,8 @@
thus ?thesis by simp
next
assume neq_0: "positive_integral (\<lambda>x. Real (2 * w x)) \<noteq> 0"
- have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (SUP n. INF m. (\<lambda>x. Real (?diff (m + n) x)))"
- proof (rule positive_integral_cong, unfold SUPR_fun_expand INFI_fun_expand, subst add_commute)
+ have "positive_integral (\<lambda>x. Real (2 * w x)) = positive_integral (\<lambda>x. SUP n. INF m. Real (?diff (m + n) x))"
+ proof (rule positive_integral_cong, subst add_commute)
fix x assume x: "x \<in> space M"
show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))"
proof (rule LIMSEQ_imp_lim_INF[symmetric])
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Dec 08 19:32:11 2010 +0100
@@ -552,10 +552,10 @@
proof -
from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
show ?ilim using mono lim i by auto
- have "(SUP i. f i) = u" using mono lim SUP_Lim_pextreal
- unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
- moreover have "(SUP i. f i) \<in> borel_measurable M"
- using i by (rule borel_measurable_SUP)
+ have "\<And>x. (SUP i. f i x) = u x" using mono lim SUP_Lim_pextreal
+ unfolding fun_eq_iff mono_def by auto
+ moreover have "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
+ using i by auto
ultimately show "u \<in> borel_measurable M" by simp
qed
--- a/src/HOL/Probability/Probability_Space.thy Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Probability_Space.thy Wed Dec 08 19:32:11 2010 +0100
@@ -1069,13 +1069,13 @@
show "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x)"
proof (intro ballI bexI)
- show "(SUP i. g i) \<in> borel_measurable M'"
+ show "(\<lambda>x. SUP i. g i x) \<in> borel_measurable M'"
using g by (auto intro: M'.borel_measurable_simple_function)
fix x assume "x \<in> space M"
have "Z x = (SUP i. f i) x" using `f \<up> Z` unfolding isoton_def by simp
- also have "\<dots> = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand
+ also have "\<dots> = (SUP i. g i (Y x))" unfolding SUPR_apply
using g `x \<in> space M` by simp
- finally show "Z x = (SUP i. g i) (Y x)" .
+ finally show "Z x = (SUP i. g i (Y x))" .
qed
qed
--- a/src/HOL/Probability/Product_Measure.thy Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Product_Measure.thy Wed Dec 08 19:32:11 2010 +0100
@@ -767,11 +767,11 @@
then have F_borel: "\<And>i. F i \<in> borel_measurable P"
and F_mono: "\<And>i x. F i x \<le> F (Suc i) x"
and F_SUPR: "\<And>x. (SUP i. F i x) = f x"
- unfolding isoton_def le_fun_def SUPR_fun_expand
+ unfolding isoton_fun_expand unfolding isoton_def le_fun_def
by (auto intro: borel_measurable_simple_function)
note sf = simple_function_cut[OF F(1)]
- then have "(SUP i. ?C (F i)) \<in> borel_measurable M1"
- using F(1) by (auto intro!: M1.borel_measurable_SUP)
+ then have "(\<lambda>x. SUP i. ?C (F i) x) \<in> borel_measurable M1"
+ using F(1) by auto
moreover
{ fix x assume "x \<in> space M1"
have isotone: "(\<lambda> i y. F i (x, y)) \<up> (\<lambda>y. f (x, y))"
@@ -783,7 +783,7 @@
by (simp add: isoton_def) }
note SUPR_C = this
ultimately show "?C f \<in> borel_measurable M1"
- unfolding SUPR_fun_expand by (simp cong: measurable_cong)
+ by (simp cong: measurable_cong)
have "positive_integral (\<lambda>x. SUP i. F i x) = (SUP i. positive_integral (F i))"
using F_borel F_mono
by (auto intro!: positive_integral_monotone_convergence_SUP[symmetric])
--- a/src/HOL/Probability/Radon_Nikodym.thy Wed Dec 08 16:15:14 2010 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Dec 08 19:32:11 2010 +0100
@@ -323,9 +323,10 @@
{ fix f g assume "f \<up> g" and f: "\<And>i. f i \<in> G"
have "g \<in> G" unfolding G_def
proof safe
- from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
+ from `f \<up> g` have [simp]: "g = (\<lambda>x. SUP i. f i x)"
+ unfolding isoton_def fun_eq_iff SUPR_apply by simp
have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
- thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
+ thus "g \<in> borel_measurable M" by auto
fix A assume "A \<in> sets M"
hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
using f_borel by (auto intro!: borel_measurable_indicator)