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"