src/HOL/Probability/Probability_Measure.thy
 changeset 57025 e7fd64f82876 parent 56996 891e992e510f child 57235 b0b9a10e4bf4
```     1.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue May 20 16:52:59 2014 +0200
1.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue May 20 19:24:39 2014 +0200
1.3 @@ -111,6 +111,26 @@
1.4    then show False by auto
1.5  qed
1.6
1.7 +lemma (in prob_space) integral_ge_const:
1.8 +  fixes c :: real
1.9 +  shows "integrable M f \<Longrightarrow> (AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>x. f x \<partial>M)"
1.10 +  using integral_mono_AE[of M "\<lambda>x. c" f] prob_space by simp
1.11 +
1.12 +lemma (in prob_space) integral_le_const:
1.13 +  fixes c :: real
1.14 +  shows "integrable M f \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>x. f x \<partial>M) \<le> c"
1.15 +  using integral_mono_AE[of M f "\<lambda>x. c"] prob_space by simp
1.16 +
1.17 +lemma (in prob_space) nn_integral_ge_const:
1.18 +  "(AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>\<^sup>+x. f x \<partial>M)"
1.19 +  using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1
1.20 +  by (simp add: nn_integral_const_If split: split_if_asm)
1.21 +
1.22 +lemma (in prob_space) nn_integral_le_const:
1.23 +  "0 \<le> c \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) \<le> c"
1.24 +  using nn_integral_mono_AE[of f "\<lambda>x. c" M] emeasure_space_1
1.25 +  by (simp add: nn_integral_const_If split: split_if_asm)
1.26 +
1.27  lemma (in prob_space) expectation_less:
1.28    fixes X :: "_ \<Rightarrow> real"
1.29    assumes [simp]: "integrable M X"
```