# HG changeset patch # User hoelzl # Date 1291833131 -3600 # Node ID a1abfa4e2b44b17abc703743244a8980244b91e2 # Parent 843c40bbc37903bfce15fbc5534655e2c19d840e use SUPR_ and INFI_apply instead of SUPR_, INFI_fun_expand diff -r 843c40bbc379 -r a1abfa4e2b44 src/HOL/Probability/Borel_Space.thy --- 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\countable \ 'a \ pextreal" assumes "\i. i \ A \ f i \ borel_measurable M" - shows "(SUP i : A. f i) \ borel_measurable M" (is "?sup \ borel_measurable M") + shows "(\x. SUP i : A. f i x) \ borel_measurable M" (is "?sup \ 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 \ 'a \ pextreal" assumes "\i. i \ A \ f i \ borel_measurable M" - shows "(INF i : A. f i) \ borel_measurable M" (is "?inf \ borel_measurable M") + shows "(\x. INF i : A. f i x) \ borel_measurable M" (is "?inf \ 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) = (\x. (INF y:A. f y x))" - by (simp add: fun_eq_iff INFI_apply) - -lemma SUPR_fun_expand: - "(SUP y:A. f y) = (\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 "\i. f i \ borel_measurable M" shows "(\x. (\\<^isub>\ i. f i x)) \ 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 *: "\x. real (Real (u' x)) - real (Real (- u' x)) = u' x" by auto - have "(SUP n. INF m. (\x. Real (u (n + m) x))) \ borel_measurable M" - "(SUP n. INF m. (\x. Real (- u (n + m) x))) \ borel_measurable M" - using u by (auto intro: borel_measurable_SUP borel_measurable_INF borel_measurable_Real) + have "(\x. SUP n. INF m. Real (u (n + m) x)) \ borel_measurable M" + "(\x. SUP n. INF m. Real (- u (n + m) x)) \ borel_measurable M" + using u by auto with eq[THEN measurable_cong, of M "\x. x" borel] have "(\x. Real (u' x)) \ borel_measurable M" - "(\x. Real (- u' x)) \ borel_measurable M" - unfolding SUPR_fun_expand INFI_fun_expand by auto + "(\x. Real (- u' x)) \ borel_measurable M" by auto note this[THEN borel_measurable_real] from borel_measurable_diff[OF this] show ?thesis unfolding * . diff -r 843c40bbc379 -r a1abfa4e2b44 src/HOL/Probability/Complete_Measure.thy --- 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: "\i. f i x = f' i x" - have "g x = (SUP i. f i x)" - using `f \ 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 \ g` unfolding isoton_def by simp + ultimately show "g x = ?f x" by (simp add: SUPR_apply) qed show "?f \ 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 diff -r 843c40bbc379 -r a1abfa4e2b44 src/HOL/Probability/Lebesgue_Integration.thy --- 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 \ u` unfolding isoton_def le_fun_def by auto next - have "u \ 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 \ 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 (\x. SUP i. f i x)" (is "_ = positive_integral ?u") proof - - have "?u \ 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)) \ positive_integral ?u" @@ -1209,9 +1205,9 @@ have "\i. rf i \ borel_measurable M" unfolding rf_def using assms by (simp cong: measurable_cong) moreover have iso: "rf \ 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 \ (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 \ 'a \ pextreal" assumes "\i. u i \ borel_measurable M" - shows "positive_integral (SUP n. INF m. u (m + n)) \ + shows "positive_integral (\x. SUP n. INF m. u (m + n) x) \ (SUP n. INF m. positive_integral (u (m + n)))" proof - - have "(SUP n. INF m. u (m + n)) \ borel_measurable M" - by (auto intro!: borel_measurable_SUP borel_measurable_INF assms) - - have "(\n. INF m. u (m + n)) \ (SUP n. INF m. u (m + n))" - proof (unfold isoton_def, safe intro!: INF_mono bexI) - fix i m show "u (Suc m + i) \ 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 (\x. SUP n. INF m. u (m + n) x) + = (SUP n. positive_integral (\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 "\ \ (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: "\i. (\x. Real (f i x)) \ borel_measurable M" using i unfolding integrable_def by auto - hence "(SUP i. (\x. Real (f i x))) \ borel_measurable M" + hence "(\x. SUP i. Real (f i x)) \ borel_measurable M" by auto hence borel_u: "u \ 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: "\n. positive_integral (\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 (\x. Real (2 * w x)) \ 0" - have "positive_integral (\x. Real (2 * w x)) = positive_integral (SUP n. INF m. (\x. Real (?diff (m + n) x)))" - proof (rule positive_integral_cong, unfold SUPR_fun_expand INFI_fun_expand, subst add_commute) + have "positive_integral (\x. Real (2 * w x)) = positive_integral (\x. SUP n. INF m. Real (?diff (m + n) x))" + proof (rule positive_integral_cong, subst add_commute) fix x assume x: "x \ space M" show "Real (2 * w x) = (SUP n. INF m. Real (?diff (n + m) x))" proof (rule LIMSEQ_imp_lim_INF[symmetric]) diff -r 843c40bbc379 -r a1abfa4e2b44 src/HOL/Probability/Lebesgue_Measure.thy --- 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) \ borel_measurable M" - using i by (rule borel_measurable_SUP) + have "\x. (SUP i. f i x) = u x" using mono lim SUP_Lim_pextreal + unfolding fun_eq_iff mono_def by auto + moreover have "(\x. SUP i. f i x) \ borel_measurable M" + using i by auto ultimately show "u \ borel_measurable M" by simp qed diff -r 843c40bbc379 -r a1abfa4e2b44 src/HOL/Probability/Probability_Space.thy --- 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 "\g\borel_measurable M'. \x\space M. Z x = g (Y x)" proof (intro ballI bexI) - show "(SUP i. g i) \ borel_measurable M'" + show "(\x. SUP i. g i x) \ borel_measurable M'" using g by (auto intro: M'.borel_measurable_simple_function) fix x assume "x \ space M" have "Z x = (SUP i. f i) x" using `f \ Z` unfolding isoton_def by simp - also have "\ = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand + also have "\ = (SUP i. g i (Y x))" unfolding SUPR_apply using g `x \ 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 diff -r 843c40bbc379 -r a1abfa4e2b44 src/HOL/Probability/Product_Measure.thy --- 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: "\i. F i \ borel_measurable P" and F_mono: "\i x. F i x \ F (Suc i) x" and F_SUPR: "\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)) \ borel_measurable M1" - using F(1) by (auto intro!: M1.borel_measurable_SUP) + then have "(\x. SUP i. ?C (F i) x) \ borel_measurable M1" + using F(1) by auto moreover { fix x assume "x \ space M1" have isotone: "(\ i y. F i (x, y)) \ (\y. f (x, y))" @@ -783,7 +783,7 @@ by (simp add: isoton_def) } note SUPR_C = this ultimately show "?C f \ borel_measurable M1" - unfolding SUPR_fun_expand by (simp cong: measurable_cong) + by (simp cong: measurable_cong) have "positive_integral (\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]) diff -r 843c40bbc379 -r a1abfa4e2b44 src/HOL/Probability/Radon_Nikodym.thy --- 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 \ g" and f: "\i. f i \ G" have "g \ G" unfolding G_def proof safe - from `f \ g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp + from `f \ g` have [simp]: "g = (\x. SUP i. f i x)" + unfolding isoton_def fun_eq_iff SUPR_apply by simp have f_borel: "\i. f i \ borel_measurable M" using f unfolding G_def by simp - thus "g \ borel_measurable M" by (auto intro!: borel_measurable_SUP) + thus "g \ borel_measurable M" by auto fix A assume "A \ sets M" hence "\i. (\x. f i x * indicator A x) \ borel_measurable M" using f_borel by (auto intro!: borel_measurable_indicator)