1077 thus "(\<lambda>x. indicat_real {X n..b} x *\<^sub>R f x) \<in> borel_measurable M" |
1077 thus "(\<lambda>x. indicat_real {X n..b} x *\<^sub>R f x) \<in> borel_measurable M" |
1078 by (simp add: set_integrable_def) |
1078 by (simp add: set_integrable_def) |
1079 qed |
1079 qed |
1080 qed |
1080 qed |
1081 |
1081 |
|
1082 |
|
1083 |
|
1084 theorem integral_Markov_inequality': |
|
1085 fixes u :: "'a \<Rightarrow> real" |
|
1086 assumes [measurable]: "set_integrable M A u" and "A \<in> sets M" |
|
1087 assumes "AE x in M. x \<in> A \<longrightarrow> u x \<ge> 0" and "0 < (c::real)" |
|
1088 shows "emeasure M {x\<in>A. u x \<ge> c} \<le> (1/c::real) * (\<integral>x\<in>A. u x \<partial>M)" |
|
1089 proof - |
|
1090 have "(\<lambda>x. u x * indicator A x) \<in> borel_measurable M" |
|
1091 using assms by (auto simp: set_integrable_def mult_ac) |
|
1092 hence "(\<lambda>x. ennreal (u x * indicator A x)) \<in> borel_measurable M" |
|
1093 by measurable |
|
1094 also have "(\<lambda>x. ennreal (u x * indicator A x)) = (\<lambda>x. ennreal (u x) * indicator A x)" |
|
1095 by (intro ext) (auto simp: indicator_def) |
|
1096 finally have meas: "\<dots> \<in> borel_measurable M" . |
|
1097 from assms(3) have AE: "AE x in M. 0 \<le> u x * indicator A x" |
|
1098 by eventually_elim (auto simp: indicator_def) |
|
1099 have nonneg: "set_lebesgue_integral M A u \<ge> 0" |
|
1100 unfolding set_lebesgue_integral_def |
|
1101 by (intro Bochner_Integration.integral_nonneg_AE eventually_mono[OF AE]) (auto simp: mult_ac) |
|
1102 |
|
1103 have A: "A \<subseteq> space M" |
|
1104 using \<open>A \<in> sets M\<close> by (simp add: sets.sets_into_space) |
|
1105 have "{x \<in> A. u x \<ge> c} = {x \<in> A. ennreal(1/c) * u x \<ge> 1}" |
|
1106 using \<open>c>0\<close> A by (auto simp: ennreal_mult'[symmetric]) |
|
1107 then have "emeasure M {x \<in> A. u x \<ge> c} = emeasure M ({x \<in> A. ennreal(1/c) * u x \<ge> 1})" |
|
1108 by simp |
|
1109 also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator A x \<partial>M)" |
|
1110 by (intro nn_integral_Markov_inequality meas assms) |
|
1111 also have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator A x \<partial>M) = ennreal (set_lebesgue_integral M A u)" |
|
1112 unfolding set_lebesgue_integral_def nn_integral_set_ennreal using assms AE |
|
1113 by (subst nn_integral_eq_integral) (simp_all add: mult_ac set_integrable_def) |
|
1114 finally show ?thesis |
|
1115 using \<open>c > 0\<close> nonneg by (subst ennreal_mult) auto |
|
1116 qed |
|
1117 |
|
1118 theorem integral_Markov_inequality'_measure: |
|
1119 assumes [measurable]: "set_integrable M A u" and "A \<in> sets M" |
|
1120 and "AE x in M. x \<in> A \<longrightarrow> 0 \<le> u x" "0 < (c::real)" |
|
1121 shows "measure M {x\<in>A. u x \<ge> c} \<le> (\<integral>x\<in>A. u x \<partial>M) / c" |
|
1122 proof - |
|
1123 have nonneg: "set_lebesgue_integral M A u \<ge> 0" |
|
1124 unfolding set_lebesgue_integral_def |
|
1125 by (intro Bochner_Integration.integral_nonneg_AE eventually_mono[OF assms(3)]) |
|
1126 (auto simp: mult_ac) |
|
1127 have le: "emeasure M {x\<in>A. u x \<ge> c} \<le> ennreal ((1/c) * (\<integral>x\<in>A. u x \<partial>M))" |
|
1128 by (rule integral_Markov_inequality') (use assms in auto) |
|
1129 also have "\<dots> < top" |
|
1130 by auto |
|
1131 finally have "ennreal (measure M {x\<in>A. u x \<ge> c}) = emeasure M {x\<in>A. u x \<ge> c}" |
|
1132 by (intro emeasure_eq_ennreal_measure [symmetric]) auto |
|
1133 also note le |
|
1134 finally show ?thesis using nonneg |
|
1135 by (subst (asm) ennreal_le_iff) |
|
1136 (auto intro!: divide_nonneg_pos Bochner_Integration.integral_nonneg_AE assms) |
|
1137 qed |
|
1138 |
|
1139 theorem%important (in finite_measure) Chernoff_ineq_ge: |
|
1140 assumes s: "s > 0" |
|
1141 assumes integrable: "set_integrable M A (\<lambda>x. exp (s * f x))" and "A \<in> sets M" |
|
1142 shows "measure M {x\<in>A. f x \<ge> a} \<le> exp (-s * a) * (\<integral>x\<in>A. exp (s * f x) \<partial>M)" |
|
1143 proof - |
|
1144 have "{x\<in>A. f x \<ge> a} = {x\<in>A. exp (s * f x) \<ge> exp (s * a)}" |
|
1145 using s by auto |
|
1146 also have "measure M \<dots> \<le> set_lebesgue_integral M A (\<lambda>x. exp (s * f x)) / exp (s * a)" |
|
1147 by (intro integral_Markov_inequality'_measure assms) auto |
|
1148 finally show ?thesis |
|
1149 by (simp add: exp_minus field_simps) |
|
1150 qed |
|
1151 |
|
1152 theorem%important (in finite_measure) Chernoff_ineq_le: |
|
1153 assumes s: "s > 0" |
|
1154 assumes integrable: "set_integrable M A (\<lambda>x. exp (-s * f x))" and "A \<in> sets M" |
|
1155 shows "measure M {x\<in>A. f x \<le> a} \<le> exp (s * a) * (\<integral>x\<in>A. exp (-s * f x) \<partial>M)" |
|
1156 proof - |
|
1157 have "{x\<in>A. f x \<le> a} = {x\<in>A. exp (-s * f x) \<ge> exp (-s * a)}" |
|
1158 using s by auto |
|
1159 also have "measure M \<dots> \<le> set_lebesgue_integral M A (\<lambda>x. exp (-s * f x)) / exp (-s * a)" |
|
1160 by (intro integral_Markov_inequality'_measure assms) auto |
|
1161 finally show ?thesis |
|
1162 by (simp add: exp_minus field_simps) |
|
1163 qed |
|
1164 |
1082 end |
1165 end |