--- a/src/HOL/Library/Extended_Reals.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Library/Extended_Reals.thy Mon May 23 19:21:05 2011 +0200
@@ -189,6 +189,9 @@
qed
end
+lemma real_of_extreal_0[simp]: "real (0::extreal) = 0"
+ unfolding real_of_extreal_def zero_extreal_def by simp
+
lemma abs_extreal_zero[simp]: "\<bar>0\<bar> = (0::extreal)"
unfolding zero_extreal_def abs_extreal.simps by simp
@@ -300,6 +303,10 @@
by (cases rule: extreal3_cases[of a b c]) auto
qed
+lemma real_of_extreal_positive_mono:
+ "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
+ by (cases rule: extreal2_cases[of x y]) auto
+
lemma extreal_MInfty_lessI[intro, simp]:
"a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
by (cases a) auto
@@ -351,17 +358,38 @@
"real y < x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < extreal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x))"
by (cases y) auto
-lemma real_of_extreal_positive_mono:
- assumes "x \<noteq> \<infinity>" "y \<noteq> \<infinity>" "0 \<le> x" "x \<le> y"
- shows "real x \<le> real y"
- using assms by (cases rule: extreal2_cases[of x y]) auto
-
lemma real_of_extreal_pos:
fixes x :: extreal shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto
lemmas real_of_extreal_ord_simps =
extreal_le_real_iff real_le_extreal_iff extreal_less_real_iff real_less_extreal_iff
+lemma abs_extreal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: extreal\<bar> = x"
+ by (cases x) auto
+
+lemma abs_extreal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: extreal\<bar> = -x"
+ by (cases x) auto
+
+lemma abs_extreal_pos[simp]: "0 \<le> \<bar>x :: extreal\<bar>"
+ by (cases x) auto
+
+lemma real_of_extreal_le_0[simp]: "real (X :: extreal) \<le> 0 \<longleftrightarrow> (X \<le> 0 \<or> X = \<infinity>)"
+ by (cases X) auto
+
+lemma abs_real_of_extreal[simp]: "\<bar>real (X :: extreal)\<bar> = real \<bar>X\<bar>"
+ by (cases X) auto
+
+lemma zero_less_real_of_extreal: "0 < real X \<longleftrightarrow> (0 < X \<and> X \<noteq> \<infinity>)"
+ by (cases X) auto
+
+lemma extreal_0_le_uminus_iff[simp]:
+ fixes a :: extreal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"
+ by (cases rule: extreal2_cases[of a]) auto
+
+lemma extreal_uminus_le_0_iff[simp]:
+ fixes a :: extreal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
+ by (cases rule: extreal2_cases[of a]) auto
+
lemma extreal_dense:
fixes x y :: extreal assumes "x < y"
shows "EX z. x < z & z < y"
@@ -444,6 +472,9 @@
and decseq_uminus[simp]: "decseq (\<lambda>x. - f x) \<longleftrightarrow> incseq f"
unfolding decseq_def incseq_def by auto
+lemma incseq_extreal: "incseq f \<Longrightarrow> incseq (\<lambda>x. extreal (f x))"
+ unfolding incseq_def by auto
+
lemma extreal_add_nonneg_nonneg:
fixes a b :: extreal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
using add_mono[of 0 a 0 b] by simp
@@ -511,6 +542,10 @@
qed
end
+lemma real_of_extreal_le_1:
+ fixes a :: extreal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
+ by (cases a) (auto simp: one_extreal_def)
+
lemma abs_extreal_one[simp]: "\<bar>1\<bar> = (1::extreal)"
unfolding one_extreal_def by simp
@@ -702,6 +737,44 @@
shows "x >= y"
by (metis assms extreal_dense leD linorder_le_less_linear)
+lemma setprod_extreal_0:
+ fixes f :: "'a \<Rightarrow> extreal"
+ shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
+proof cases
+ assume "finite A"
+ then show ?thesis by (induct A) auto
+qed auto
+
+lemma setprod_extreal_pos:
+ fixes f :: "'a \<Rightarrow> extreal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
+proof cases
+ assume "finite I" from this pos show ?thesis by induct auto
+qed simp
+
+lemma setprod_PInf:
+ assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
+ shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
+proof cases
+ assume "finite I" from this assms show ?thesis
+ proof (induct I)
+ case (insert i I)
+ then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_extreal_pos)
+ from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
+ also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
+ using setprod_extreal_pos[of I f] pos
+ by (cases rule: extreal2_cases[of "f i" "setprod f I"]) auto
+ also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
+ using insert by (auto simp: setprod_extreal_0)
+ finally show ?case .
+ qed simp
+qed simp
+
+lemma setprod_extreal: "(\<Prod>i\<in>A. extreal (f i)) = extreal (setprod f A)"
+proof cases
+ assume "finite A" then show ?thesis
+ by induct (auto simp: one_extreal_def)
+qed (simp add: one_extreal_def)
+
subsubsection {* Power *}
instantiation extreal :: power
@@ -890,6 +963,11 @@
instance proof qed
end
+lemma real_of_extreal_inverse[simp]:
+ fixes a :: extreal
+ shows "real (inverse a) = 1 / real a"
+ by (cases a) (auto simp: inverse_eq_divide)
+
lemma extreal_inverse[simp]:
"inverse 0 = \<infinity>"
"inverse (1::extreal) = 1"
@@ -1620,6 +1698,28 @@
unfolding SUPR_def INFI_def image_image
by auto
+lemma uminus_extreal_add_uminus_uminus:
+ fixes a b :: extreal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
+ by (cases rule: extreal2_cases[of a b]) auto
+
+lemma INFI_extreal_add:
+ assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
+ shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
+proof -
+ have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
+ using assms unfolding INF_less_iff by auto
+ { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
+ by (rule uminus_extreal_add_uminus_uminus) }
+ then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
+ by simp
+ also have "\<dots> = INFI UNIV f + INFI UNIV g"
+ unfolding extreal_INFI_uminus
+ using assms INF_less
+ by (subst SUPR_extreal_add)
+ (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus)
+ finally show ?thesis .
+qed
+
subsection "Limits on @{typ extreal}"
subsubsection "Topological space"
@@ -1936,9 +2036,6 @@
} ultimately show ?thesis by blast
qed
-lemma real_of_extreal_0[simp]: "real (0::extreal) = 0"
- unfolding real_of_extreal_def zero_extreal_def by simp
-
lemma real_of_extreal_mult[simp]:
fixes a b :: extreal shows "real (a * b) = real a * real b"
by (cases rule: extreal2_cases[of a b]) auto
@@ -2406,7 +2503,6 @@
from this show ?thesis using ext by blast
qed
-
lemma open_image_extreal: "open(UNIV-{\<infinity>,(-\<infinity>)})"
by (metis range_extreal open_extreal open_UNIV)
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon May 23 19:21:05 2011 +0200
@@ -805,6 +805,21 @@
} ultimately show ?thesis by auto
qed
+lemma liminf_extreal_cminus:
+ fixes f :: "nat \<Rightarrow> extreal" assumes "c \<noteq> -\<infinity>"
+ shows "liminf (\<lambda>x. c - f x) = c - limsup f"
+proof (cases c)
+ case PInf then show ?thesis by (simp add: Liminf_const)
+next
+ case (real r) then show ?thesis
+ unfolding liminf_SUPR_INFI limsup_INFI_SUPR
+ apply (subst INFI_extreal_cminus)
+ apply auto
+ apply (subst SUPR_extreal_cminus)
+ apply auto
+ done
+qed (insert `c \<noteq> -\<infinity>`, simp)
+
subsubsection {* Continuity *}
lemma continuous_imp_tendsto:
@@ -1259,4 +1274,20 @@
finally show "\<exists>r. (\<lambda>i. real (f i)) sums r" by (auto simp: sums_extreal)
qed
+lemma suminf_SUP_eq:
+ fixes f :: "nat \<Rightarrow> nat \<Rightarrow> extreal"
+ assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i"
+ shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
+proof -
+ { fix n :: nat
+ have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
+ using assms by (auto intro!: SUPR_extreal_setsum[symmetric]) }
+ note * = this
+ show ?thesis using assms
+ apply (subst (1 2) suminf_extreal_eq_SUPR)
+ unfolding *
+ apply (auto intro!: le_SUPI2)
+ apply (subst SUP_commute) ..
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Probability/Binary_Product_Measure.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Mon May 23 19:21:05 2011 +0200
@@ -8,6 +8,9 @@
imports Lebesgue_Integration
begin
+lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
+ by auto
+
lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
by auto
@@ -318,9 +321,6 @@
sublocale pair_sigma_finite \<subseteq> pair_sigma_algebra M1 M2
by default
-lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
- by auto
-
lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B"
proof
fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B"
--- a/src/HOL/Probability/Borel_Space.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Mon May 23 19:21:05 2011 +0200
@@ -1346,15 +1346,6 @@
by induct auto
qed (simp add: borel_measurable_const)
-lemma abs_extreal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: extreal\<bar> = x"
- by (cases x) auto
-
-lemma abs_extreal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: extreal\<bar> = -x"
- by (cases x) auto
-
-lemma abs_extreal_pos[simp]: "0 \<le> \<bar>x :: extreal\<bar>"
- by (cases x) auto
-
lemma (in sigma_algebra) borel_measurable_extreal_abs[intro, simp]:
fixes f :: "'a \<Rightarrow> extreal" assumes "f \<in> borel_measurable M"
shows "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
--- a/src/HOL/Probability/Caratheodory.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Mon May 23 19:21:05 2011 +0200
@@ -9,6 +9,12 @@
imports Sigma_Algebra Extended_Real_Limits
begin
+lemma sums_def2:
+ "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
+ unfolding sums_def
+ apply (subst LIMSEQ_Suc_iff[symmetric])
+ unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
+
text {*
Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
*}
@@ -853,12 +859,6 @@
subsubsection {*Alternative instances of caratheodory*}
-lemma sums_def2:
- "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
- unfolding sums_def
- apply (subst LIMSEQ_Suc_iff[symmetric])
- unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
-
lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
assumes f: "positive M f" "additive M f"
shows "countably_additive M f \<longleftrightarrow>
@@ -900,28 +900,6 @@
show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
qed
-lemma uminus_extreal_add_uminus_uminus:
- fixes a b :: extreal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
- by (cases rule: extreal2_cases[of a b]) auto
-
-lemma INFI_extreal_add:
- assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
- shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
-proof -
- have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
- using assms unfolding INF_less_iff by auto
- { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
- by (rule uminus_extreal_add_uminus_uminus) }
- then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
- by simp
- also have "\<dots> = INFI UNIV f + INFI UNIV g"
- unfolding extreal_INFI_uminus
- using assms INF_less
- by (subst SUPR_extreal_add)
- (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus)
- finally show ?thesis .
-qed
-
lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
assumes f: "positive M f" "additive M f"
shows "(\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> sets M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))
--- a/src/HOL/Probability/Finite_Product_Measure.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Mon May 23 19:21:05 2011 +0200
@@ -495,44 +495,6 @@
sublocale finite_product_sigma_finite \<subseteq> finite_product_sigma_algebra
by default (fact finite_index')
-lemma setprod_extreal_0:
- fixes f :: "'a \<Rightarrow> extreal"
- shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
-proof cases
- assume "finite A"
- then show ?thesis by (induct A) auto
-qed auto
-
-lemma setprod_extreal_pos:
- fixes f :: "'a \<Rightarrow> extreal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
-proof cases
- assume "finite I" from this pos show ?thesis by induct auto
-qed simp
-
-lemma setprod_PInf:
- assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
- shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
-proof cases
- assume "finite I" from this assms show ?thesis
- proof (induct I)
- case (insert i I)
- then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_extreal_pos)
- from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
- also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
- using setprod_extreal_pos[of I f] pos
- by (cases rule: extreal2_cases[of "f i" "setprod f I"]) auto
- also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
- using insert by (auto simp: setprod_extreal_0)
- finally show ?case .
- qed simp
-qed simp
-
-lemma setprod_extreal: "(\<Prod>i\<in>A. extreal (f i)) = extreal (setprod f A)"
-proof cases
- assume "finite A" then show ?thesis
- by induct (auto simp: one_extreal_def)
-qed (simp add: one_extreal_def)
-
lemma (in finite_product_sigma_finite) product_algebra_generator_measure:
assumes "Pi\<^isub>E I F \<in> sets G"
shows "measure G (Pi\<^isub>E I F) = (\<Prod>i\<in>I. M.\<mu> i (F i))"
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Mon May 23 19:21:05 2011 +0200
@@ -223,11 +223,6 @@
done
qed
-lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"
- unfolding measure_space_1[symmetric]
- using sets_into_space
- by (intro measure_mono) auto
-
definition (in product_prob_space)
"\<mu>G A =
(THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = measure (Pi\<^isub>M J M) X))"
--- a/src/HOL/Probability/Lebesgue_Integration.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Mon May 23 19:21:05 2011 +0200
@@ -45,9 +45,6 @@
then show ?thesis using assms by (auto intro: measurable_sets)
qed
-lemma incseq_extreal: "incseq f \<Longrightarrow> incseq (\<lambda>x. extreal (f x))"
- unfolding incseq_def by auto
-
lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
proof
assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
@@ -2184,21 +2181,6 @@
using assms unfolding lebesgue_integral_def
by (subst (1 2) positive_integral_cong_AE) (auto simp add: extreal_real)
-lemma liminf_extreal_cminus:
- fixes f :: "nat \<Rightarrow> extreal" assumes "c \<noteq> -\<infinity>"
- shows "liminf (\<lambda>x. c - f x) = c - limsup f"
-proof (cases c)
- case PInf then show ?thesis by (simp add: Liminf_const)
-next
- case (real r) then show ?thesis
- unfolding liminf_SUPR_INFI limsup_INFI_SUPR
- apply (subst INFI_extreal_cminus)
- apply auto
- apply (subst SUPR_extreal_cminus)
- apply auto
- done
-qed (insert `c \<noteq> -\<infinity>`, simp)
-
lemma (in measure_space) integral_dominated_convergence:
assumes u: "\<And>i. integrable M (u i)" and bound: "\<And>x j. x\<in>space M \<Longrightarrow> \<bar>u j x\<bar> \<le> w x"
and w: "integrable M w"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon May 23 19:21:05 2011 +0200
@@ -116,22 +116,6 @@
qed (auto intro: LIMSEQ_indicator_UN simp: cube_def)
qed simp
-lemma suminf_SUP_eq:
- fixes f :: "nat \<Rightarrow> nat \<Rightarrow> extreal"
- assumes "\<And>i. incseq (\<lambda>n. f n i)" "\<And>n i. 0 \<le> f n i"
- shows "(\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
-proof -
- { fix n :: nat
- have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
- using assms by (auto intro!: SUPR_extreal_setsum[symmetric]) }
- note * = this
- show ?thesis using assms
- apply (subst (1 2) suminf_extreal_eq_SUPR)
- unfolding *
- apply (auto intro!: le_SUPI2)
- apply (subst SUP_commute) ..
-qed
-
interpretation lebesgue: measure_space lebesgue
proof
have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff)
@@ -558,10 +542,6 @@
subsection {* Lebesgue integrable implies Gauge integrable *}
-lemma positive_not_Inf:
- "0 \<le> x \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> \<bar>x\<bar> \<noteq> \<infinity>"
- by (cases x) auto
-
lemma has_integral_cmult_real:
fixes c :: real
assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
@@ -648,10 +628,6 @@
qed
qed
-lemma real_of_extreal_positive_mono:
- "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
- by (cases rule: extreal2_cases[of x y]) auto
-
lemma positive_integral_has_integral:
fixes f :: "'a::ordered_euclidean_space \<Rightarrow> extreal"
assumes f: "f \<in> borel_measurable lebesgue" "range f \<subseteq> {0..<\<infinity>}" "integral\<^isup>P lebesgue f \<noteq> \<infinity>"
--- a/src/HOL/Probability/Measure.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Measure.thy Mon May 23 19:21:05 2011 +0200
@@ -1162,16 +1162,11 @@
using finite_measure_of_space by auto
qed
-lemma (in finite_measure) measure_not_inf:
- assumes A: "A \<in> sets M"
- shows "\<bar>\<mu> A\<bar> \<noteq> \<infinity>"
- using finite_measure[OF A] positive_measure[OF A] by auto
-
definition (in finite_measure)
"\<mu>' A = (if A \<in> sets M then real (\<mu> A) else 0)"
lemma (in finite_measure) finite_measure_eq: "A \<in> sets M \<Longrightarrow> \<mu> A = extreal (\<mu>' A)"
- using measure_not_inf[of A] by (auto simp: \<mu>'_def)
+ by (auto simp: \<mu>'_def extreal_real)
lemma (in finite_measure) positive_measure': "0 \<le> \<mu>' A"
unfolding \<mu>'_def by (auto simp: real_of_extreal_pos)
@@ -1182,8 +1177,7 @@
moreover then have "\<mu> A \<le> \<mu> (space M)"
using sets_into_space by (auto intro!: measure_mono)
ultimately show ?thesis
- using measure_not_inf[of A] measure_not_inf[of "space M"]
- by (auto simp: \<mu>'_def)
+ by (auto simp: \<mu>'_def intro!: real_of_extreal_positive_mono)
qed (simp add: \<mu>'_def real_of_extreal_pos)
lemma (in finite_measure) restricted_finite_measure:
--- a/src/HOL/Probability/Probability_Measure.thy Mon May 23 10:58:21 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Mon May 23 19:21:05 2011 +0200
@@ -9,23 +9,6 @@
imports Lebesgue_Integration Radon_Nikodym Finite_Product_Measure Lebesgue_Measure
begin
-lemma real_of_extreal_inverse[simp]:
- fixes X :: extreal
- shows "real (inverse X) = 1 / real X"
- by (cases X) (auto simp: inverse_eq_divide)
-
-lemma real_of_extreal_le_0[simp]: "real (X :: extreal) \<le> 0 \<longleftrightarrow> (X \<le> 0 \<or> X = \<infinity>)"
- by (cases X) auto
-
-lemma abs_real_of_extreal[simp]: "\<bar>real (X :: extreal)\<bar> = real \<bar>X\<bar>"
- by (cases X) auto
-
-lemma zero_less_real_of_extreal: "0 < real X \<longleftrightarrow> (0 < X \<and> X \<noteq> \<infinity>)"
- by (cases X) auto
-
-lemma real_of_extreal_le_1: fixes X :: extreal shows "X \<le> 1 \<Longrightarrow> real X \<le> 1"
- by (cases X) (auto simp: one_extreal_def)
-
locale prob_space = measure_space +
assumes measure_space_1: "measure M (space M) = 1"
@@ -83,6 +66,11 @@
"joint_distribution X X {(x, x)} = distribution X {x}"
unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
+lemma (in prob_space) measure_le_1: "X \<in> sets M \<Longrightarrow> \<mu> X \<le> 1"
+ unfolding measure_space_1[symmetric]
+ using sets_into_space
+ by (intro measure_mono) auto
+
lemma (in prob_space) distribution_1:
"distribution X A \<le> 1"
unfolding distribution_def by simp
@@ -1017,10 +1005,6 @@
qed
qed
-lemma extreal_0_le_iff_le_0[simp]:
- fixes a :: extreal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"
- by (cases rule: extreal2_cases[of a]) auto
-
lemma (in sigma_algebra) factorize_measurable_function:
fixes Z :: "'a \<Rightarrow> extreal" and Y :: "'a \<Rightarrow> 'c"
assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M"