108 shows False |
108 shows False |
109 proof - |
109 proof - |
110 from ae have "AE \<omega> in M. False" by eventually_elim auto |
110 from ae have "AE \<omega> in M. False" by eventually_elim auto |
111 then show False by auto |
111 then show False by auto |
112 qed |
112 qed |
|
113 |
|
114 lemma (in prob_space) integral_ge_const: |
|
115 fixes c :: real |
|
116 shows "integrable M f \<Longrightarrow> (AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>x. f x \<partial>M)" |
|
117 using integral_mono_AE[of M "\<lambda>x. c" f] prob_space by simp |
|
118 |
|
119 lemma (in prob_space) integral_le_const: |
|
120 fixes c :: real |
|
121 shows "integrable M f \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>x. f x \<partial>M) \<le> c" |
|
122 using integral_mono_AE[of M f "\<lambda>x. c"] prob_space by simp |
|
123 |
|
124 lemma (in prob_space) nn_integral_ge_const: |
|
125 "(AE x in M. c \<le> f x) \<Longrightarrow> c \<le> (\<integral>\<^sup>+x. f x \<partial>M)" |
|
126 using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1 |
|
127 by (simp add: nn_integral_const_If split: split_if_asm) |
|
128 |
|
129 lemma (in prob_space) nn_integral_le_const: |
|
130 "0 \<le> c \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) \<le> c" |
|
131 using nn_integral_mono_AE[of f "\<lambda>x. c" M] emeasure_space_1 |
|
132 by (simp add: nn_integral_const_If split: split_if_asm) |
113 |
133 |
114 lemma (in prob_space) expectation_less: |
134 lemma (in prob_space) expectation_less: |
115 fixes X :: "_ \<Rightarrow> real" |
135 fixes X :: "_ \<Rightarrow> real" |
116 assumes [simp]: "integrable M X" |
136 assumes [simp]: "integrable M X" |
117 assumes gt: "AE x in M. X x < b" |
137 assumes gt: "AE x in M. X x < b" |