# HG changeset patch
# User Andreas Lochbihler
# Date 1422013077 -3600
# Node ID 14dd7e9acd92e8d48741463985c76cb23dbc5441
# Parent  6fca83e88417587b325ece8765405873f1f3b2e9# Parent  084330e2ec5eebf599e02ffea01be7cab18dac7a
merged

diff -r 6fca83e88417 -r 14dd7e9acd92 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Fri Jan 23 12:04:27 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Jan 23 12:37:57 2015 +0100
@@ -53,6 +53,18 @@
 lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1"
   using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure)
 
+lemma (in subprob_space) nn_integral_le_const:
+  assumes "0 \<le> c" "AE x in M. f x \<le> c"
+  shows "(\<integral>\<^sup>+x. f x \<partial>M) \<le> c"
+proof -
+  have "(\<integral>\<^sup>+ x. f x \<partial>M) \<le> (\<integral>\<^sup>+ x. c \<partial>M)"
+    by(rule nn_integral_mono_AE) fact
+  also have "\<dots> \<le> c * emeasure M (space M)"
+    using \<open>0 \<le> c\<close> by(simp add: nn_integral_const_If)
+  also have "\<dots> \<le> c * 1" using emeasure_space_le_1 \<open>0 \<le> c\<close> by(rule ereal_mult_left_mono)
+  finally show ?thesis by simp
+qed
+
 lemma emeasure_density_distr_interval:
   fixes h :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real" and g' :: "real \<Rightarrow> real"
   assumes [simp]: "a \<le> b"
diff -r 6fca83e88417 -r 14dd7e9acd92 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri Jan 23 12:04:27 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Jan 23 12:37:57 2015 +0100
@@ -145,11 +145,6 @@
   using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1
   by (simp add: nn_integral_const_If split: split_if_asm)
 
-lemma (in prob_space) nn_integral_le_const:
-  "0 \<le> c \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) \<le> c"
-  using nn_integral_mono_AE[of f "\<lambda>x. c" M] emeasure_space_1
-  by (simp add: nn_integral_const_If split: split_if_asm)
-
 lemma (in prob_space) expectation_less:
   fixes X :: "_ \<Rightarrow> real"
   assumes [simp]: "integrable M X"