--- 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"