1(* Title: HOL/Probability/Distributions.thy 2 Author: Sudeep Kanav, TU M��nchen 3 Author: Johannes H��lzl, TU M��nchen 4 Author: Jeremy Avigad, CMU *) 5 6section \<open>Properties of Various Distributions\<close> 7 8theory Distributions 9 imports Convolution Information 10begin 11 12lemma (in prob_space) distributed_affine: 13 fixes f :: "real \<Rightarrow> ennreal" 14 assumes f: "distributed M lborel X f" 15 assumes c: "c \<noteq> 0" 16 shows "distributed M lborel (\<lambda>x. t + c * X x) (\<lambda>x. f ((x - t) / c) / \<bar>c\<bar>)" 17 unfolding distributed_def 18proof safe 19 have [measurable]: "f \<in> borel_measurable borel" 20 using f by (simp add: distributed_def) 21 have [measurable]: "X \<in> borel_measurable M" 22 using f by (simp add: distributed_def) 23 24 show "(\<lambda>x. f ((x - t) / c) / \<bar>c\<bar>) \<in> borel_measurable lborel" 25 by simp 26 show "random_variable lborel (\<lambda>x. t + c * X x)" 27 by simp 28 29 have eq: "ennreal \<bar>c\<bar> * (f x / ennreal \<bar>c\<bar>) = f x" for x 30 using c 31 by (cases "f x") 32 (auto simp: divide_ennreal ennreal_mult[symmetric] ennreal_top_divide ennreal_mult_top) 33 34 have "density lborel f = distr M lborel X" 35 using f by (simp add: distributed_def) 36 with c show "distr M lborel (\<lambda>x. t + c * X x) = density lborel (\<lambda>x. f ((x - t) / c) / ennreal \<bar>c\<bar>)" 37 by (subst (2) lborel_real_affine[where c="c" and t="t"]) 38 (simp_all add: density_density_eq density_distr distr_distr field_simps eq cong: distr_cong) 39qed 40 41lemma (in prob_space) distributed_affineI: 42 fixes f :: "real \<Rightarrow> ennreal" and c :: real 43 assumes f: "distributed M lborel (\<lambda>x. (X x - t) / c) (\<lambda>x. \<bar>c\<bar> * f (x * c + t))" 44 assumes c: "c \<noteq> 0" 45 shows "distributed M lborel X f" 46proof - 47 have eq: "f x * ennreal \<bar>c\<bar> / ennreal \<bar>c\<bar> = f x" for x 48 using c by (simp add: ennreal_times_divide[symmetric]) 49 50 show ?thesis 51 using distributed_affine[OF f c, where t=t] c 52 by (simp add: field_simps eq) 53qed 54 55lemma (in prob_space) distributed_AE2: 56 assumes [measurable]: "distributed M N X f" "Measurable.pred N P" 57 shows "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)" 58proof - 59 have "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in distr M N X. P x)" 60 by (simp add: AE_distr_iff) 61 also have "\<dots> \<longleftrightarrow> (AE x in density N f. P x)" 62 unfolding distributed_distr_eq_density[OF assms(1)] .. 63 also have "\<dots> \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)" 64 by (rule AE_density) simp 65 finally show ?thesis . 66qed 67 68subsection \<open>Erlang\<close> 69 70lemma nn_intergal_power_times_exp_Icc: 71 assumes [arith]: "0 \<le> a" 72 shows "(\<integral>\<^sup>+x. ennreal (x^k * exp (-x)) * indicator {0 .. a} x \<partial>lborel) = 73 (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _") 74proof - 75 let ?f = "\<lambda>k x. x^k * exp (-x) / fact k" 76 let ?F = "\<lambda>k x. - (\<Sum>n\<le>k. (x^n * exp (-x)) / fact n)" 77 have "?I * (inverse (real_of_nat (fact k))) = 78 (\<integral>\<^sup>+x. ennreal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (real_of_nat (fact k))) \<partial>lborel)" 79 by (intro nn_integral_multc[symmetric]) auto 80 also have "\<dots> = (\<integral>\<^sup>+x. ennreal (?f k x) * indicator {0 .. a} x \<partial>lborel)" 81 by (intro nn_integral_cong) 82 (simp add: field_simps ennreal_mult'[symmetric] indicator_mult_ennreal) 83 also have "\<dots> = ennreal (?F k a - ?F k 0)" 84 proof (rule nn_integral_FTC_Icc) 85 fix x assume "x \<in> {0..a}" 86 show "DERIV (?F k) x :> ?f k x" 87 proof(induction k) 88 case 0 show ?case by (auto intro!: derivative_eq_intros) 89 next 90 case (Suc k) 91 have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :> 92 ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k))" 93 by (intro DERIV_diff Suc) 94 (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc 95 simp add: field_simps power_Suc[symmetric]) 96 also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)" 97 by simp 98 also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k)) = ?f (Suc k) x" 99 by (auto simp: field_simps simp del: fact_Suc) 100 (simp_all add: of_nat_Suc field_simps) 101 finally show ?case . 102 qed 103 qed auto 104 also have "\<dots> = ennreal (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n))" 105 by (auto simp: power_0_left if_distrib[where f="\<lambda>x. x / a" for a] sum.If_cases) 106 also have "\<dots> = ennreal ((1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k) * ennreal (inverse (fact k))" 107 by (subst ennreal_mult''[symmetric]) (auto intro!: arg_cong[where f=ennreal]) 108 finally show ?thesis 109 by (auto simp add: mult_right_ennreal_cancel le_less) 110qed 111 112lemma nn_intergal_power_times_exp_Ici: 113 shows "(\<integral>\<^sup>+x. ennreal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = real_of_nat (fact k)" 114proof (rule LIMSEQ_unique) 115 let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ennreal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel" 116 show "?X \<longlonglongrightarrow> (\<integral>\<^sup>+x. ennreal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)" 117 apply (intro nn_integral_LIMSEQ) 118 apply (auto simp: incseq_def le_fun_def eventually_sequentially 119 split: split_indicator intro!: tendsto_eventually) 120 apply (metis nat_ceiling_le_eq) 121 done 122 123 have "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) \<longlongrightarrow> 124 (1 - (\<Sum>n\<le>k. 0 / (fact n))) * fact k) at_top" 125 by (intro tendsto_intros tendsto_power_div_exp_0) simp 126 then show "?X \<longlonglongrightarrow> real_of_nat (fact k)" 127 by (subst nn_intergal_power_times_exp_Icc) 128 (auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially]) 129qed 130 131definition erlang_density :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where 132 "erlang_density k l x = (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k)" 133 134definition erlang_CDF :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where 135 "erlang_CDF k l x = (if x < 0 then 0 else 1 - (\<Sum>n\<le>k. ((l * x)^n * exp (- l * x) / fact n)))" 136 137lemma erlang_density_nonneg[simp]: "0 \<le> l \<Longrightarrow> 0 \<le> erlang_density k l x" 138 by (simp add: erlang_density_def) 139 140lemma borel_measurable_erlang_density[measurable]: "erlang_density k l \<in> borel_measurable borel" 141 by (auto simp add: erlang_density_def[abs_def]) 142 143lemma erlang_CDF_transform: "0 < l \<Longrightarrow> erlang_CDF k l a = erlang_CDF k 1 (l * a)" 144 by (auto simp add: erlang_CDF_def mult_less_0_iff) 145 146lemma erlang_CDF_nonneg[simp]: assumes "0 < l" shows "0 \<le> erlang_CDF k l x" 147 unfolding erlang_CDF_def 148proof (clarsimp simp: not_less) 149 assume "0 \<le> x" 150 have "(\<Sum>n\<le>k. (l * x) ^ n * exp (- (l * x)) / fact n) = 151 exp (- (l * x)) * (\<Sum>n\<le>k. (l * x) ^ n / fact n)" 152 unfolding sum_distrib_left by (intro sum.cong) (auto simp: field_simps) 153 also have "\<dots> = (\<Sum>n\<le>k. (l * x) ^ n / fact n) / exp (l * x)" 154 by (simp add: exp_minus field_simps) 155 also have "\<dots> \<le> 1" 156 proof (subst divide_le_eq_1_pos) 157 show "(\<Sum>n\<le>k. (l * x) ^ n / fact n) \<le> exp (l * x)" 158 using \<open>0 < l\<close> \<open>0 \<le> x\<close> summable_exp_generic[of "l * x"] 159 by (auto simp: exp_def divide_inverse ac_simps intro!: sum_le_suminf) 160 qed simp 161 finally show "(\<Sum>n\<le>k. (l * x) ^ n * exp (- (l * x)) / fact n) \<le> 1" . 162qed 163 164lemma nn_integral_erlang_density: 165 assumes [arith]: "0 < l" 166 shows "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a" 167proof (cases "0 \<le> a") 168 case [arith]: True 169 have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x" 170 by (simp add: field_simps split: split_indicator) 171 have "(\<integral>\<^sup>+x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = 172 (\<integral>\<^sup>+x. (l/fact k) * (ennreal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x) \<partial>lborel)" 173 by (intro nn_integral_cong) 174 (auto simp: erlang_density_def power_mult_distrib ennreal_mult[symmetric] split: split_indicator) 175 also have "\<dots> = (l/fact k) * (\<integral>\<^sup>+x. ennreal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x \<partial>lborel)" 176 by (intro nn_integral_cmult) auto 177 also have "\<dots> = ennreal (l/fact k) * ((1/l) * (\<integral>\<^sup>+x. ennreal (x^k * exp (- x)) * indicator {0 .. l * a} x \<partial>lborel))" 178 by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq) 179 also have "\<dots> = (1 - (\<Sum>n\<le>k. ((l * a)^n * exp (-(l * a))) / fact n))" 180 by (subst nn_intergal_power_times_exp_Icc) (auto simp: ennreal_mult'[symmetric]) 181 also have "\<dots> = erlang_CDF k l a" 182 by (auto simp: erlang_CDF_def) 183 finally show ?thesis . 184next 185 case False 186 then have "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))" 187 by (intro nn_integral_cong) (auto simp: erlang_density_def) 188 with False show ?thesis 189 by (simp add: erlang_CDF_def) 190qed 191 192lemma emeasure_erlang_density: 193 "0 < l \<Longrightarrow> emeasure (density lborel (erlang_density k l)) {.. a} = erlang_CDF k l a" 194 by (simp add: emeasure_density nn_integral_erlang_density) 195 196lemma nn_integral_erlang_ith_moment: 197 fixes k i :: nat and l :: real 198 assumes [arith]: "0 < l" 199 shows "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x * x ^ i) \<partial>lborel) = fact (k + i) / (fact k * l ^ i)" 200proof - 201 have eq: "\<And>x. indicator {0..} (x / l) = indicator {0..} x" 202 by (simp add: field_simps split: split_indicator) 203 have "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x * x^i) \<partial>lborel) = 204 (\<integral>\<^sup>+x. (l/(fact k * l^i)) * (ennreal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x) \<partial>lborel)" 205 by (intro nn_integral_cong) 206 (auto simp: erlang_density_def power_mult_distrib power_add ennreal_mult'[symmetric] split: split_indicator) 207 also have "\<dots> = (l/(fact k * l^i)) * (\<integral>\<^sup>+x. ennreal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x \<partial>lborel)" 208 by (intro nn_integral_cmult) auto 209 also have "\<dots> = ennreal (l/(fact k * l^i)) * ((1/l) * (\<integral>\<^sup>+x. ennreal (x^(k+i) * exp (- x)) * indicator {0 ..} x \<partial>lborel))" 210 by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq) 211 also have "\<dots> = fact (k + i) / (fact k * l ^ i)" 212 by (subst nn_intergal_power_times_exp_Ici) (auto simp: ennreal_mult'[symmetric]) 213 finally show ?thesis . 214qed 215 216lemma prob_space_erlang_density: 217 assumes l[arith]: "0 < l" 218 shows "prob_space (density lborel (erlang_density k l))" (is "prob_space ?D") 219proof 220 show "emeasure ?D (space ?D) = 1" 221 using nn_integral_erlang_ith_moment[OF l, where k=k and i=0] by (simp add: emeasure_density) 222qed 223 224lemma (in prob_space) erlang_distributed_le: 225 assumes D: "distributed M lborel X (erlang_density k l)" 226 assumes [simp, arith]: "0 < l" "0 \<le> a" 227 shows "\<P>(x in M. X x \<le> a) = erlang_CDF k l a" 228proof - 229 have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}" 230 using distributed_measurable[OF D] 231 by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) 232 also have "\<dots> = emeasure (density lborel (erlang_density k l)) {.. a}" 233 unfolding distributed_distr_eq_density[OF D] .. 234 also have "\<dots> = erlang_CDF k l a" 235 by (auto intro!: emeasure_erlang_density) 236 finally show ?thesis 237 by (auto simp: emeasure_eq_measure measure_nonneg) 238qed 239 240lemma (in prob_space) erlang_distributed_gt: 241 assumes D[simp]: "distributed M lborel X (erlang_density k l)" 242 assumes [arith]: "0 < l" "0 \<le> a" 243 shows "\<P>(x in M. a < X x ) = 1 - (erlang_CDF k l a)" 244proof - 245 have " 1 - (erlang_CDF k l a) = 1 - \<P>(x in M. X x \<le> a)" by (subst erlang_distributed_le) auto 246 also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })" 247 using distributed_measurable[OF D] by (auto simp: prob_compl) 248 also have "\<dots> = \<P>(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le) 249 finally show ?thesis by simp 250qed 251 252lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0" 253 by (induction k) (auto simp: erlang_CDF_def) 254 255lemma erlang_distributedI: 256 assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l" 257 and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = erlang_CDF k l a" 258 shows "distributed M lborel X (erlang_density k l)" 259proof (rule distributedI_borel_atMost) 260 fix a :: real 261 { assume "a \<le> 0" 262 with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}" 263 by (intro emeasure_mono) auto 264 also have "... = 0" by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0]) 265 finally have "emeasure M {x\<in>space M. X x \<le> a} \<le> 0" by simp 266 then have "emeasure M {x\<in>space M. X x \<le> a} = 0" by simp 267 } 268 note eq_0 = this 269 270 show "(\<integral>\<^sup>+ x. erlang_density k l x * indicator {..a} x \<partial>lborel) = ennreal (erlang_CDF k l a)" 271 using nn_integral_erlang_density[of l k a] 272 by (simp add: ennreal_indicator ennreal_mult) 273 274 show "emeasure M {x\<in>space M. X x \<le> a} = ennreal (erlang_CDF k l a)" 275 using X_distr[of a] eq_0 by (auto simp: one_ennreal_def erlang_CDF_def) 276qed simp_all 277 278lemma (in prob_space) erlang_distributed_iff: 279 assumes [arith]: "0<l" 280 shows "distributed M lborel X (erlang_density k l) \<longleftrightarrow> 281 (X \<in> borel_measurable M \<and> 0 < l \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = erlang_CDF k l a ))" 282 using 283 distributed_measurable[of M lborel X "erlang_density k l"] 284 emeasure_erlang_density[of l] 285 erlang_distributed_le[of X k l] 286 by (auto intro!: erlang_distributedI simp: one_ennreal_def emeasure_eq_measure) 287 288lemma (in prob_space) erlang_distributed_mult_const: 289 assumes erlX: "distributed M lborel X (erlang_density k l)" 290 assumes a_pos[arith]: "0 < \<alpha>" "0 < l" 291 shows "distributed M lborel (\<lambda>x. \<alpha> * X x) (erlang_density k (l / \<alpha>))" 292proof (subst erlang_distributed_iff, safe) 293 have [measurable]: "random_variable borel X" and [arith]: "0 < l " 294 and [simp]: "\<And>a. 0 \<le> a \<Longrightarrow> prob {x \<in> space M. X x \<le> a} = erlang_CDF k l a" 295 by(insert erlX, auto simp: erlang_distributed_iff) 296 297 show "random_variable borel (\<lambda>x. \<alpha> * X x)" "0 < l / \<alpha>" "0 < l / \<alpha>" 298 by (auto simp:field_simps) 299 300 fix a:: real assume [arith]: "0 \<le> a" 301 obtain b:: real where [simp, arith]: "b = a/ \<alpha>" by blast 302 303 have [arith]: "0 \<le> b" by (auto simp: divide_nonneg_pos) 304 305 have "prob {x \<in> space M. \<alpha> * X x \<le> a} = prob {x \<in> space M. X x \<le> b}" 306 by (rule arg_cong[where f= prob]) (auto simp:field_simps) 307 308 moreover have "prob {x \<in> space M. X x \<le> b} = erlang_CDF k l b" by auto 309 moreover have "erlang_CDF k (l / \<alpha>) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto 310 ultimately show "prob {x \<in> space M. \<alpha> * X x \<le> a} = erlang_CDF k (l / \<alpha>) a" by fastforce 311qed 312 313lemma (in prob_space) has_bochner_integral_erlang_ith_moment: 314 fixes k i :: nat and l :: real 315 assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)" 316 shows "has_bochner_integral M (\<lambda>x. X x ^ i) (fact (k + i) / (fact k * l ^ i))" 317proof (rule has_bochner_integral_nn_integral) 318 show "AE x in M. 0 \<le> X x ^ i" 319 by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def) 320 show "(\<integral>\<^sup>+ x. ennreal (X x ^ i) \<partial>M) = ennreal (fact (k + i) / (fact k * l ^ i))" 321 using nn_integral_erlang_ith_moment[of l k i] 322 by (subst distributed_nn_integral[symmetric, OF D]) (auto simp: ennreal_mult') 323qed (insert distributed_measurable[OF D], auto) 324 325lemma (in prob_space) erlang_ith_moment_integrable: 326 "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> integrable M (\<lambda>x. X x ^ i)" 327 by rule (rule has_bochner_integral_erlang_ith_moment) 328 329lemma (in prob_space) erlang_ith_moment: 330 "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> 331 expectation (\<lambda>x. X x ^ i) = fact (k + i) / (fact k * l ^ i)" 332 by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment) 333 334lemma (in prob_space) erlang_distributed_variance: 335 assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)" 336 shows "variance X = (k + 1) / l\<^sup>2" 337proof (subst variance_eq) 338 show "integrable M X" "integrable M (\<lambda>x. (X x)\<^sup>2)" 339 using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2] 340 by auto 341 342 show "expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2" 343 using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2] 344 by simp (auto simp: power2_eq_square field_simps of_nat_Suc) 345qed 346 347subsection \<open>Exponential distribution\<close> 348 349abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where 350 "exponential_density \<equiv> erlang_density 0" 351 352lemma exponential_density_def: 353 "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))" 354 by (simp add: fun_eq_iff erlang_density_def) 355 356lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \<le> a then 1 - exp (- l * a) else 0)" 357 by (simp add: erlang_CDF_def) 358 359lemma prob_space_exponential_density: "0 < l \<Longrightarrow> prob_space (density lborel (exponential_density l))" 360 by (rule prob_space_erlang_density) 361 362lemma (in prob_space) exponential_distributedD_le: 363 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" and l: "0 < l" 364 shows "\<P>(x in M. X x \<le> a) = 1 - exp (- a * l)" 365 using erlang_distributed_le[OF D l a] a by (simp add: erlang_CDF_def) 366 367lemma (in prob_space) exponential_distributedD_gt: 368 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" and l: "0 < l" 369 shows "\<P>(x in M. a < X x ) = exp (- a * l)" 370 using erlang_distributed_gt[OF D l a] a by (simp add: erlang_CDF_def) 371 372lemma (in prob_space) exponential_distributed_memoryless: 373 assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a" and l: "0 < l" and t: "0 \<le> t" 374 shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)" 375proof - 376 have "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. a + t < X x) / \<P>(x in M. a < X x)" 377 using \<open>0 \<le> t\<close> by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="(/)"]) 378 also have "\<dots> = exp (- (a + t) * l) / exp (- a * l)" 379 using a t by (simp add: exponential_distributedD_gt[OF D _ l]) 380 also have "\<dots> = exp (- t * l)" 381 using l by (auto simp: field_simps exp_add[symmetric]) 382 finally show ?thesis 383 using t by (simp add: exponential_distributedD_gt[OF D _ l]) 384qed 385 386lemma exponential_distributedI: 387 assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l" 388 and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1 - exp (- a * l)" 389 shows "distributed M lborel X (exponential_density l)" 390proof (rule erlang_distributedI) 391 fix a :: real assume "0 \<le> a" then show "emeasure M {x \<in> space M. X x \<le> a} = ennreal (erlang_CDF 0 l a)" 392 using X_distr[of a] by (simp add: erlang_CDF_def ennreal_minus ennreal_1[symmetric] del: ennreal_1) 393qed fact+ 394 395lemma (in prob_space) exponential_distributed_iff: 396 assumes "0 < l" 397 shows "distributed M lborel X (exponential_density l) \<longleftrightarrow> 398 (X \<in> borel_measurable M \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = 1 - exp (- a * l)))" 399 using assms erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0) 400 401 402lemma (in prob_space) exponential_distributed_expectation: 403 "0 < l \<Longrightarrow> distributed M lborel X (exponential_density l) \<Longrightarrow> expectation X = 1 / l" 404 using erlang_ith_moment[of l X 0 1] by simp 405 406lemma exponential_density_nonneg: "0 < l \<Longrightarrow> 0 \<le> exponential_density l x" 407 by (auto simp: exponential_density_def) 408 409lemma (in prob_space) exponential_distributed_min: 410 assumes "0 < l" "0 < u" 411 assumes expX: "distributed M lborel X (exponential_density l)" 412 assumes expY: "distributed M lborel Y (exponential_density u)" 413 assumes ind: "indep_var borel X borel Y" 414 shows "distributed M lborel (\<lambda>x. min (X x) (Y x)) (exponential_density (l + u))" 415proof (subst exponential_distributed_iff, safe) 416 have randX: "random_variable borel X" 417 using expX \<open>0 < l\<close> by (simp add: exponential_distributed_iff) 418 moreover have randY: "random_variable borel Y" 419 using expY \<open>0 < u\<close> by (simp add: exponential_distributed_iff) 420 ultimately show "random_variable borel (\<lambda>x. min (X x) (Y x))" by auto 421 422 show " 0 < l + u" 423 using \<open>0 < l\<close> \<open>0 < u\<close> by auto 424 425 fix a::real assume a[arith]: "0 \<le> a" 426 have gt1[simp]: "\<P>(x in M. a < X x ) = exp (- a * l)" 427 by (rule exponential_distributedD_gt[OF expX a]) fact 428 have gt2[simp]: "\<P>(x in M. a < Y x ) = exp (- a * u)" 429 by (rule exponential_distributedD_gt[OF expY a]) fact 430 431 have "\<P>(x in M. a < (min (X x) (Y x)) ) = \<P>(x in M. a < (X x) \<and> a < (Y x))" by (auto intro!:arg_cong[where f=prob]) 432 433 also have " ... = \<P>(x in M. a < (X x)) * \<P>(x in M. a< (Y x) )" 434 using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp 435 also have " ... = exp (- a * (l + u))" by (auto simp:field_simps mult_exp_exp) 436 finally have indep_prob: "\<P>(x in M. a < (min (X x) (Y x)) ) = exp (- a * (l + u))" . 437 438 have "{x \<in> space M. (min (X x) (Y x)) \<le>a } = (space M - {x \<in> space M. a<(min (X x) (Y x)) })" 439 by auto 440 then have "1 - prob {x \<in> space M. a < (min (X x) (Y x))} = prob {x \<in> space M. (min (X x) (Y x)) \<le> a}" 441 using randX randY by (auto simp: prob_compl) 442 then show "prob {x \<in> space M. (min (X x) (Y x)) \<le> a} = 1 - exp (- a * (l + u))" 443 using indep_prob by auto 444qed 445 446lemma (in prob_space) exponential_distributed_Min: 447 assumes finI: "finite I" 448 assumes A: "I \<noteq> {}" 449 assumes l: "\<And>i. i \<in> I \<Longrightarrow> 0 < l i" 450 assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density (l i))" 451 assumes ind: "indep_vars (\<lambda>i. borel) X I" 452 shows "distributed M lborel (\<lambda>x. Min ((\<lambda>i. X i x)`I)) (exponential_density (\<Sum>i\<in>I. l i))" 453using assms 454proof (induct rule: finite_ne_induct) 455 case (singleton i) then show ?case by simp 456next 457 case (insert i I) 458 then have "distributed M lborel (\<lambda>x. min (X i x) (Min ((\<lambda>i. X i x)`I))) (exponential_density (l i + (\<Sum>i\<in>I. l i)))" 459 by (intro exponential_distributed_min indep_vars_Min insert) 460 (auto intro: indep_vars_subset sum_pos) 461 then show ?case 462 using insert by simp 463qed 464 465lemma (in prob_space) exponential_distributed_variance: 466 "0 < l \<Longrightarrow> distributed M lborel X (exponential_density l) \<Longrightarrow> variance X = 1 / l\<^sup>2" 467 using erlang_distributed_variance[of l X 0] by simp 468 469lemma nn_integral_zero': "AE x in M. f x = 0 \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) = 0" 470 by (simp cong: nn_integral_cong_AE) 471 472lemma convolution_erlang_density: 473 fixes k\<^sub>1 k\<^sub>2 :: nat 474 assumes [simp, arith]: "0 < l" 475 shows "(\<lambda>x. \<integral>\<^sup>+y. ennreal (erlang_density k\<^sub>1 l (x - y)) * ennreal (erlang_density k\<^sub>2 l y) \<partial>lborel) = 476 (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)" 477 (is "?LHS = ?RHS") 478proof 479 fix x :: real 480 have "x \<le> 0 \<or> 0 < x" 481 by arith 482 then show "?LHS x = ?RHS x" 483 proof 484 assume "x \<le> 0" then show ?thesis 485 apply (subst nn_integral_zero') 486 apply (rule AE_I[where N="{0}"]) 487 apply (auto simp add: erlang_density_def not_less) 488 done 489 next 490 note zero_le_mult_iff[simp] zero_le_divide_iff[simp] 491 492 have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l) = 1" 493 using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 0] by (simp del: fact_Suc) 494 495 have 1: "(\<integral>\<^sup>+ x. ennreal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l x * indicator {0<..} x) \<partial>lborel) = 1" 496 apply (subst I_eq1[symmetric]) 497 unfolding erlang_density_def 498 by (auto intro!: nn_integral_cong split:split_indicator) 499 500 have "prob_space (density lborel ?LHS)" 501 by (intro prob_space_convolution_density) 502 (auto intro!: prob_space_erlang_density erlang_density_nonneg) 503 then have 2: "integral\<^sup>N lborel ?LHS = 1" 504 by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density) 505 506 let ?I = "(integral\<^sup>N lborel (\<lambda>y. ennreal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))" 507 let ?C = "(fact (Suc (k\<^sub>1 + k\<^sub>2))) / ((fact k\<^sub>1) * (fact k\<^sub>2))" 508 let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 509 let ?L = "(\<lambda>x. \<integral>\<^sup>+y. ennreal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \<partial>lborel)" 510 511 { fix x :: real assume [arith]: "0 < x" 512 have *: "\<And>x y n. (x - y * x::real)^n = x^n * (1 - y)^n" 513 unfolding power_mult_distrib[symmetric] by (simp add: field_simps) 514 515 have "?LHS x = ?L x" 516 unfolding erlang_density_def 517 by (auto intro!: nn_integral_cong simp: ennreal_mult split:split_indicator) 518 also have "... = (\<lambda>x. ennreal ?C * ?I * erlang_density ?s l x) x" 519 apply (subst nn_integral_real_affine[where c=x and t = 0]) 520 apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] del: fact_Suc) 521 apply (intro nn_integral_cong) 522 apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add * 523 ennreal_mult[symmetric] 524 simp del: fact_Suc split: split_indicator) 525 done 526 finally have "(\<integral>\<^sup>+y. ennreal (erlang_density k\<^sub>1 l (x - y) * erlang_density k\<^sub>2 l y) \<partial>lborel) = 527 (\<lambda>x. ennreal ?C * ?I * erlang_density ?s l x) x" 528 by (simp add: ennreal_mult) } 529 note * = this 530 531 assume [arith]: "0 < x" 532 have 3: "1 = integral\<^sup>N lborel (\<lambda>xa. ?LHS xa * indicator {0<..} xa)" 533 by (subst 2[symmetric]) 534 (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] 535 simp: erlang_density_def nn_integral_multc[symmetric] indicator_def split: if_split_asm) 536 also have "... = integral\<^sup>N lborel (\<lambda>x. (ennreal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))" 537 by (auto intro!: nn_integral_cong simp: ennreal_mult[symmetric] * split: split_indicator) 538 also have "... = ennreal (?C) * ?I" 539 using 1 540 by (auto simp: nn_integral_cmult) 541 finally have " ennreal (?C) * ?I = 1" by presburger 542 543 then show ?thesis 544 using * by (simp add: ennreal_mult) 545 qed 546qed 547 548lemma (in prob_space) sum_indep_erlang: 549 assumes indep: "indep_var borel X borel Y" 550 assumes [simp, arith]: "0 < l" 551 assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)" 552 assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)" 553 shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)" 554 using assms 555 apply (subst convolution_erlang_density[symmetric, OF \<open>0<l\<close>]) 556 apply (intro distributed_convolution) 557 apply auto 558 done 559 560lemma (in prob_space) erlang_distributed_sum: 561 assumes finI : "finite I" 562 assumes A: "I \<noteq> {}" 563 assumes [simp, arith]: "0 < l" 564 assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (erlang_density (k i) l)" 565 assumes ind: "indep_vars (\<lambda>i. borel) X I" 566 shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((\<Sum>i\<in>I. Suc (k i)) - 1) l)" 567using assms 568proof (induct rule: finite_ne_induct) 569 case (singleton i) then show ?case by auto 570next 571 case (insert i I) 572 then have "distributed M lborel (\<lambda>x. (X i x) + (\<Sum>i\<in> I. X i x)) (erlang_density (Suc (k i) + Suc ((\<Sum>i\<in>I. Suc (k i)) - 1) - 1) l)" 573 by(intro sum_indep_erlang indep_vars_sum) (auto intro!: indep_vars_subset) 574 also have "(\<lambda>x. (X i x) + (\<Sum>i\<in> I. X i x)) = (\<lambda>x. \<Sum>i\<in>insert i I. X i x)" 575 using insert by auto 576 also have "Suc(k i) + Suc ((\<Sum>i\<in>I. Suc (k i)) - 1) - 1 = (\<Sum>i\<in>insert i I. Suc (k i)) - 1" 577 using insert by (auto intro!: Suc_pred simp: ac_simps) 578 finally show ?case by fast 579qed 580 581lemma (in prob_space) exponential_distributed_sum: 582 assumes finI: "finite I" 583 assumes A: "I \<noteq> {}" 584 assumes l: "0 < l" 585 assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density l)" 586 assumes ind: "indep_vars (\<lambda>i. borel) X I" 587 shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((card I) - 1) l)" 588 using erlang_distributed_sum[OF assms] by simp 589 590lemma (in information_space) entropy_exponential: 591 assumes l[simp, arith]: "0 < l" 592 assumes D: "distributed M lborel X (exponential_density l)" 593 shows "entropy b lborel X = log b (exp 1 / l)" 594proof - 595 have [simp]: "integrable lborel (exponential_density l)" 596 using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp 597 598 have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1" 599 using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space) 600 601 have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)" 602 using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp 603 604 have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l" 605 using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp 606 607 have "entropy b lborel X = - (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)" 608 using D by (rule entropy_distr) simp 609 also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 610 (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)" 611 by (intro Bochner_Integration.integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps) 612 also have "\<dots> = (ln l - 1) / ln b" 613 by simp 614 finally show ?thesis 615 by (simp add: log_def ln_div) (simp add: field_split_simps) 616qed 617 618subsection \<open>Uniform distribution\<close> 619 620lemma uniform_distrI: 621 assumes X: "X \<in> measurable M M'" 622 and A: "A \<in> sets M'" "emeasure M' A \<noteq> \<infinity>" "emeasure M' A \<noteq> 0" 623 assumes distr: "\<And>B. B \<in> sets M' \<Longrightarrow> emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A" 624 shows "distr M M' X = uniform_measure M' A" 625 unfolding uniform_measure_def 626proof (intro measure_eqI) 627 let ?f = "\<lambda>x. indicator A x / emeasure M' A" 628 fix B assume B: "B \<in> sets (distr M M' X)" 629 with X have "emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A" 630 by (simp add: distr[of B] measurable_sets) 631 also have "\<dots> = (1 / emeasure M' A) * emeasure M' (A \<inter> B)" 632 by (simp add: divide_ennreal_def ac_simps) 633 also have "\<dots> = (\<integral>\<^sup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')" 634 using A B 635 by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: ) 636 also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')" 637 by (rule nn_integral_cong) (auto split: split_indicator) 638 finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B" 639 using A B X by (auto simp add: emeasure_distr emeasure_density) 640qed simp 641 642lemma uniform_distrI_borel: 643 fixes A :: "real set" 644 assumes X[measurable]: "X \<in> borel_measurable M" and A: "emeasure lborel A = ennreal r" "0 < r" 645 and [measurable]: "A \<in> sets borel" 646 assumes distr: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = emeasure lborel (A \<inter> {.. a}) / r" 647 shows "distributed M lborel X (\<lambda>x. indicator A x / measure lborel A)" 648proof (rule distributedI_borel_atMost) 649 let ?f = "\<lambda>x. 1 / r * indicator A x" 650 fix a 651 have "emeasure lborel (A \<inter> {..a}) \<le> emeasure lborel A" 652 using A by (intro emeasure_mono) auto 653 also have "\<dots> < \<infinity>" 654 using A by simp 655 finally have fin: "emeasure lborel (A \<inter> {..a}) \<noteq> top" 656 by simp 657 from emeasure_eq_ennreal_measure[OF this] 658 have fin_eq: "emeasure lborel (A \<inter> {..a}) / r = ennreal (measure lborel (A \<inter> {..a}) / r)" 659 using A by (simp add: divide_ennreal measure_nonneg) 660 then show "emeasure M {x\<in>space M. X x \<le> a} = ennreal (measure lborel (A \<inter> {..a}) / r)" 661 using distr by simp 662 663 have "(\<integral>\<^sup>+ x. ennreal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = 664 (\<integral>\<^sup>+ x. ennreal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)" 665 by (auto intro!: nn_integral_cong split: split_indicator) 666 also have "\<dots> = ennreal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})" 667 using \<open>A \<in> sets borel\<close> 668 by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg) 669 also have "\<dots> = ennreal (measure lborel (A \<inter> {..a}) / r)" 670 unfolding emeasure_eq_ennreal_measure[OF fin] using A 671 by (simp add: measure_def ennreal_mult'[symmetric]) 672 finally show "(\<integral>\<^sup>+ x. ennreal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) = 673 ennreal (measure lborel (A \<inter> {..a}) / r)" . 674qed (auto simp: measure_nonneg) 675 676lemma (in prob_space) uniform_distrI_borel_atLeastAtMost: 677 fixes a b :: real 678 assumes X: "X \<in> borel_measurable M" and "a < b" 679 assumes distr: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> \<P>(x in M. X x \<le> t) = (t - a) / (b - a)" 680 shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b})" 681proof (rule uniform_distrI_borel) 682 fix t 683 have "t < a \<or> (a \<le> t \<and> t \<le> b) \<or> b < t" 684 by auto 685 then show "emeasure M {x\<in>space M. X x \<le> t} = emeasure lborel ({a .. b} \<inter> {..t}) / (b - a)" 686 proof (elim disjE conjE) 687 assume "t < a" 688 then have "emeasure M {x\<in>space M. X x \<le> t} \<le> emeasure M {x\<in>space M. X x \<le> a}" 689 using X by (auto intro!: emeasure_mono measurable_sets) 690 also have "\<dots> = 0" 691 using distr[of a] \<open>a < b\<close> by (simp add: emeasure_eq_measure) 692 finally have "emeasure M {x\<in>space M. X x \<le> t} = 0" 693 by (simp add: antisym measure_nonneg) 694 with \<open>t < a\<close> show ?thesis by simp 695 next 696 assume bnds: "a \<le> t" "t \<le> b" 697 have "{a..b} \<inter> {..t} = {a..t}" 698 using bnds by auto 699 then show ?thesis using \<open>a \<le> t\<close> \<open>a < b\<close> 700 using distr[OF bnds] by (simp add: emeasure_eq_measure divide_ennreal) 701 next 702 assume "b < t" 703 have "1 = emeasure M {x\<in>space M. X x \<le> b}" 704 using distr[of b] \<open>a < b\<close> by (simp add: one_ennreal_def emeasure_eq_measure) 705 also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}" 706 using X \<open>b < t\<close> by (auto intro!: emeasure_mono measurable_sets) 707 finally have "emeasure M {x\<in>space M. X x \<le> t} = 1" 708 by (simp add: antisym emeasure_eq_measure) 709 with \<open>b < t\<close> \<open>a < b\<close> show ?thesis by (simp add: measure_def divide_ennreal) 710 qed 711qed (insert X \<open>a < b\<close>, auto) 712 713lemma (in prob_space) uniform_distributed_measure: 714 fixes a b :: real 715 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" 716 assumes t: "a \<le> t" "t \<le> b" 717 shows "\<P>(x in M. X x \<le> t) = (t - a) / (b - a)" 718proof - 719 have "emeasure M {x \<in> space M. X x \<le> t} = emeasure (distr M lborel X) {.. t}" 720 using distributed_measurable[OF D] 721 by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) 722 also have "\<dots> = (\<integral>\<^sup>+x. ennreal (1 / (b - a)) * indicator {a .. t} x \<partial>lborel)" 723 using distributed_borel_measurable[OF D] \<open>a \<le> t\<close> \<open>t \<le> b\<close> 724 unfolding distributed_distr_eq_density[OF D] 725 by (subst emeasure_density) 726 (auto intro!: nn_integral_cong simp: measure_def split: split_indicator) 727 also have "\<dots> = ennreal (1 / (b - a)) * (t - a)" 728 using \<open>a \<le> t\<close> \<open>t \<le> b\<close> 729 by (subst nn_integral_cmult_indicator) auto 730 finally show ?thesis 731 using t by (simp add: emeasure_eq_measure ennreal_mult''[symmetric] measure_nonneg) 732qed 733 734lemma (in prob_space) uniform_distributed_bounds: 735 fixes a b :: real 736 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" 737 shows "a < b" 738proof (rule ccontr) 739 assume "\<not> a < b" 740 then have "{a .. b} = {} \<or> {a .. b} = {a .. a}" by simp 741 with uniform_distributed_params[OF D] show False 742 by (auto simp: measure_def) 743qed 744 745lemma (in prob_space) uniform_distributed_iff: 746 fixes a b :: real 747 shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b}) \<longleftrightarrow> 748 (X \<in> borel_measurable M \<and> a < b \<and> (\<forall>t\<in>{a .. b}. \<P>(x in M. X x \<le> t)= (t - a) / (b - a)))" 749 using 750 uniform_distributed_bounds[of X a b] 751 uniform_distributed_measure[of X a b] 752 distributed_measurable[of M lborel X] 753 by (auto intro!: uniform_distrI_borel_atLeastAtMost simp del: content_real_if) 754 755lemma (in prob_space) uniform_distributed_expectation: 756 fixes a b :: real 757 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" 758 shows "expectation X = (a + b) / 2" 759proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric]) 760 have "a < b" 761 using uniform_distributed_bounds[OF D] . 762 763 have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = 764 (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)" 765 by (intro Bochner_Integration.integral_cong) auto 766 also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2" 767 proof (subst integral_FTC_Icc_real) 768 fix x 769 show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" 770 using uniform_distributed_params[OF D] 771 by (auto intro!: derivative_eq_intros simp del: content_real_if) 772 show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x" 773 using uniform_distributed_params[OF D] 774 by (auto intro!: isCont_divide) 775 have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = 776 (b*b - a * a) / (2 * (b - a))" 777 using \<open>a < b\<close> 778 by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) 779 show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" 780 using \<open>a < b\<close> 781 unfolding * square_diff_square_factored by (auto simp: field_simps) 782 qed (insert \<open>a < b\<close>, simp) 783 finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" . 784qed (auto simp: measure_nonneg) 785 786lemma (in prob_space) uniform_distributed_variance: 787 fixes a b :: real 788 assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})" 789 shows "variance X = (b - a)\<^sup>2 / 12" 790proof (subst distributed_variance) 791 have [arith]: "a < b" using uniform_distributed_bounds[OF D] . 792 let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}" 793 have "(\<integral>x. x\<^sup>2 * (?D x) \<partial>lborel) = (\<integral>x. x\<^sup>2 * (indicator {a - ?\<mu> .. b - ?\<mu>} x) / measure lborel {a .. b} \<partial>lborel)" 794 by (intro Bochner_Integration.integral_cong) (auto split: split_indicator) 795 also have "\<dots> = (b - a)\<^sup>2 / 12" 796 by (simp add: integral_power uniform_distributed_expectation[OF D]) 797 (simp add: eval_nat_numeral field_simps ) 798 finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" . 799qed (auto intro: D simp del: content_real_if) 800 801subsection \<open>Normal distribution\<close> 802 803 804definition normal_density :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where 805 "normal_density \<mu> \<sigma> x = 1 / sqrt (2 * pi * \<sigma>\<^sup>2) * exp (-(x - \<mu>)\<^sup>2/ (2 * \<sigma>\<^sup>2))" 806 807abbreviation std_normal_density :: "real \<Rightarrow> real" where 808 "std_normal_density \<equiv> normal_density 0 1" 809 810lemma std_normal_density_def: "std_normal_density x = (1 / sqrt (2 * pi)) * exp (- x\<^sup>2 / 2)" 811 unfolding normal_density_def by simp 812 813lemma normal_density_nonneg[simp]: "0 \<le> normal_density \<mu> \<sigma> x" 814 by (auto simp: normal_density_def) 815 816lemma normal_density_pos: "0 < \<sigma> \<Longrightarrow> 0 < normal_density \<mu> \<sigma> x" 817 by (auto simp: normal_density_def) 818 819lemma borel_measurable_normal_density[measurable]: "normal_density \<mu> \<sigma> \<in> borel_measurable borel" 820 by (auto simp: normal_density_def[abs_def]) 821 822lemma gaussian_moment_0: 823 "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2)) (sqrt pi / 2)" 824proof - 825 let ?pI = "\<lambda>f. (\<integral>\<^sup>+s. f (s::real) * indicator {0..} s \<partial>lborel)" 826 let ?gauss = "\<lambda>x. exp (- x\<^sup>2)" 827 828 let ?I = "indicator {0<..} :: real \<Rightarrow> real" 829 let ?ff= "\<lambda>x s. x * exp (- x\<^sup>2 * (1 + s\<^sup>2)) :: real" 830 831 have *: "?pI ?gauss = (\<integral>\<^sup>+x. ?gauss x * ?I x \<partial>lborel)" 832 by (intro nn_integral_cong_AE AE_I[where N="{0}"]) (auto split: split_indicator) 833 834 have "?pI ?gauss * ?pI ?gauss = (\<integral>\<^sup>+x. \<integral>\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \<partial>lborel \<partial>lborel)" 835 by (auto simp: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] * ennreal_mult[symmetric] 836 intro!: nn_integral_cong split: split_indicator) 837 also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+s. ?ff x s * ?I s * ?I x \<partial>lborel \<partial>lborel)" 838 proof (rule nn_integral_cong, cases) 839 fix x :: real assume "x \<noteq> 0" 840 then show "(\<integral>\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \<partial>lborel) = (\<integral>\<^sup>+s. ?ff x s * ?I s * ?I x \<partial>lborel)" 841 by (subst nn_integral_real_affine[where t="0" and c="x"]) 842 (auto simp: mult_exp_exp nn_integral_cmult[symmetric] field_simps zero_less_mult_iff ennreal_mult[symmetric] 843 intro!: nn_integral_cong split: split_indicator) 844 qed simp 845 also have "... = \<integral>\<^sup>+s. \<integral>\<^sup>+x. ?ff x s * ?I s * ?I x \<partial>lborel \<partial>lborel" 846 by (rule lborel_pair.Fubini'[symmetric]) auto 847 also have "... = ?pI (\<lambda>s. ?pI (\<lambda>x. ?ff x s))" 848 by (rule nn_integral_cong_AE) 849 (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] split: split_indicator_asm) 850 also have "\<dots> = ?pI (\<lambda>s. ennreal (1 / (2 * (1 + s\<^sup>2))))" 851 proof (intro nn_integral_cong ennreal_mult_right_cong) 852 fix s :: real show "?pI (\<lambda>x. ?ff x s) = ennreal (1 / (2 * (1 + s\<^sup>2)))" 853 proof (subst nn_integral_FTC_atLeast) 854 have "((\<lambda>a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) \<longlongrightarrow> (- (0 / (2 + 2 * s\<^sup>2)))) at_top" 855 apply (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top]) 856 apply (subst mult.commute) 857 apply (auto intro!: filterlim_tendsto_pos_mult_at_top 858 filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident] 859 simp: add_pos_nonneg power2_eq_square add_nonneg_eq_0_iff) 860 done 861 then show "((\<lambda>a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) \<longlongrightarrow> 0) at_top" 862 by (simp add: field_simps) 863 qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff) 864 qed 865 also have "... = ennreal (pi / 4)" 866 proof (subst nn_integral_FTC_atLeast) 867 show "((\<lambda>a. arctan a / 2) \<longlongrightarrow> (pi / 2) / 2 ) at_top" 868 by (intro tendsto_intros) (simp_all add: tendsto_arctan_at_top) 869 qed (auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps power2_eq_square) 870 finally have "?pI ?gauss^2 = pi / 4" 871 by (simp add: power2_eq_square) 872 then have "?pI ?gauss = sqrt (pi / 4)" 873 using power_eq_iff_eq_base[of 2 "enn2real (?pI ?gauss)" "sqrt (pi / 4)"] 874 by (cases "?pI ?gauss") (auto simp: power2_eq_square ennreal_mult[symmetric] ennreal_top_mult) 875 also have "?pI ?gauss = (\<integral>\<^sup>+x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2) \<partial>lborel)" 876 by (intro nn_integral_cong) (simp split: split_indicator) 877 also have "sqrt (pi / 4) = sqrt pi / 2" 878 by (simp add: real_sqrt_divide) 879 finally show ?thesis 880 by (rule has_bochner_integral_nn_integral[rotated 3]) 881 auto 882qed 883 884lemma gaussian_moment_1: 885 "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (- x\<^sup>2) * x)) (1 / 2)" 886proof - 887 have "(\<integral>\<^sup>+x. indicator {0..} x *\<^sub>R (exp (- x\<^sup>2) * x) \<partial>lborel) = 888 (\<integral>\<^sup>+x. ennreal (x * exp (- x\<^sup>2)) * indicator {0..} x \<partial>lborel)" 889 by (intro nn_integral_cong) 890 (auto simp: ac_simps split: split_indicator) 891 also have "\<dots> = ennreal (0 - (- exp (- 0\<^sup>2) / 2))" 892 proof (rule nn_integral_FTC_atLeast) 893 have "((\<lambda>x::real. - exp (- x\<^sup>2) / 2) \<longlongrightarrow> - 0 / 2) at_top" 894 by (intro tendsto_divide tendsto_minus filterlim_compose[OF exp_at_bot] 895 filterlim_compose[OF filterlim_uminus_at_bot_at_top] 896 filterlim_pow_at_top filterlim_ident) 897 auto 898 then show "((\<lambda>a::real. - exp (- a\<^sup>2) / 2) \<longlongrightarrow> 0) at_top" 899 by simp 900 qed (auto intro!: derivative_eq_intros) 901 also have "\<dots> = ennreal (1 / 2)" 902 by simp 903 finally show ?thesis 904 by (rule has_bochner_integral_nn_integral[rotated 3]) 905 (auto split: split_indicator) 906qed 907 908lemma 909 fixes k :: nat 910 shows gaussian_moment_even_pos: 911 "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k))) 912 ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" 913 (is "?even") 914 and gaussian_moment_odd_pos: 915 "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" 916 (is "?odd") 917proof - 918 let ?M = "\<lambda>k x. exp (- x\<^sup>2) * x^k :: real" 919 920 { fix k I assume Mk: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R ?M k x) I" 921 have "2 \<noteq> (0::real)" 922 by linarith 923 let ?f = "\<lambda>b. \<integral>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \<partial>lborel" 924 have "((\<lambda>b. (k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \<partial>lborel) - ?M (k + 1) b / 2) \<longlongrightarrow> 925 (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top" (is ?tendsto) 926 proof (intro tendsto_intros \<open>2 \<noteq> 0\<close> tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros]) 927 show "(?M (k + 1) \<longlongrightarrow> 0) at_top" 928 proof cases 929 assume "even k" 930 have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) \<longlongrightarrow> 0 * 0) at_top" 931 by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0] 932 filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident) 933 auto 934 also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)" 935 using \<open>even k\<close> by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: evenE) 936 finally show ?thesis by simp 937 next 938 assume "odd k" 939 have "((\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) \<longlongrightarrow> 0) at_top" 940 by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity 941 filterlim_ident filterlim_pow_at_top) 942 auto 943 also have "(\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)" 944 using \<open>odd k\<close> by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: oddE) 945 finally show ?thesis by simp 946 qed 947 qed 948 also have "?tendsto \<longleftrightarrow> ((?f \<longlongrightarrow> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top)" 949 proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI) 950 fix b :: real assume b: "0 \<le> b" 951 have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = (\<integral>x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \<partial>lborel)" 952 unfolding integral_mult_right_zero[symmetric] by (intro Bochner_Integration.integral_cong) auto 953 also have "\<dots> = exp (- b\<^sup>2) * b ^ (Suc k) - exp (- 0\<^sup>2) * 0 ^ (Suc k) - 954 (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel)" 955 by (rule integral_by_parts') 956 (auto intro!: derivative_eq_intros b 957 simp: diff_Suc of_nat_Suc field_simps split: nat.split) 958 also have "... = exp (- b\<^sup>2) * b ^ (Suc k) - (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)" 959 by (auto simp: intro!: Bochner_Integration.integral_cong) 960 also have "... = exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)" 961 unfolding Bochner_Integration.integral_mult_right_zero [symmetric] 962 by (simp del: real_scaleR_def) 963 finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = 964 exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)" . 965 then show "(k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\<partial>lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b" 966 by (simp add: field_simps atLeastAtMost_def indicator_inter_arith) 967 qed 968 finally have int_M_at_top: "((?f \<longlongrightarrow> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel)) at_top)" 969 by simp 970 971 have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R ?M (k + 2) x) ((k + 1) / 2 * I)" 972 proof (rule has_bochner_integral_monotone_convergence_at_top) 973 fix y :: real 974 have *: "(\<lambda>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..y} x::real) = 975 (\<lambda>x. indicator {0..y} x *\<^sub>R ?M (k + 2) x)" 976 by rule (simp split: split_indicator) 977 show "integrable lborel (\<lambda>x. indicator {0..} x *\<^sub>R (?M (k + 2) x) * indicator {..y} x::real)" 978 unfolding * by (rule borel_integrable_compact) (auto intro!: continuous_intros) 979 show "((?f \<longlongrightarrow> (k + 1) / 2 * I) at_top)" 980 using int_M_at_top has_bochner_integral_integral_eq[OF Mk] by simp 981 qed (auto split: split_indicator) } 982 note step = this 983 984 show ?even 985 proof (induct k) 986 case (Suc k) 987 note step[OF this] 988 also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * ((fact (2 * k)) / ((2::real)^(2*k) * fact k)))) = 989 sqrt pi / 2 * ((fact (2 * Suc k)) / ((2::real)^(2 * Suc k) * fact (Suc k)))" 990 apply (simp add: field_simps del: fact_Suc) 991 apply (simp add: of_nat_mult field_simps) 992 done 993 finally show ?case 994 by simp 995 qed (insert gaussian_moment_0, simp) 996 997 show ?odd 998 proof (induct k) 999 case (Suc k) 1000 note step[OF this] 1001 also have "(real (2 * k + 1 + 1) / (2::real) * ((fact k) / 2)) = (fact (Suc k)) / 2" 1002 by (simp add: field_simps of_nat_Suc field_split_simps del: fact_Suc) (simp add: field_simps) 1003 finally show ?case 1004 by simp 1005 qed (insert gaussian_moment_1, simp) 1006qed 1007 1008context 1009 fixes k :: nat and \<mu> \<sigma> :: real assumes [arith]: "0 < \<sigma>" 1010begin 1011 1012lemma normal_moment_even: 1013 "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>) ^ (2 * k)) (fact (2 * k) / ((2 / \<sigma>\<^sup>2)^k * fact k))" 1014proof - 1015 have eq: "\<And>x::real. x\<^sup>2^k = (x^k)\<^sup>2" 1016 by (simp add: power_mult[symmetric] ac_simps) 1017 1018 have "has_bochner_integral lborel (\<lambda>x. exp (-x\<^sup>2)*x^(2 * k)) 1019 (sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" 1020 using has_bochner_integral_even_function[OF gaussian_moment_even_pos[where k=k]] by simp 1021 then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*x^(2 * k)) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) 1022 ((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2)))" 1023 by (rule has_bochner_integral_mult_left) 1024 also have "(\<lambda>x. (exp (-x\<^sup>2)*x^(2 * k)) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) = 1025 (\<lambda>x. exp (- ((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2*\<sigma>\<^sup>2)) * ((sqrt 2 * \<sigma>) * x) ^ (2 * k) / sqrt (2 * pi * \<sigma>\<^sup>2))" 1026 by (auto simp: fun_eq_iff field_simps real_sqrt_power[symmetric] real_sqrt_mult 1027 real_sqrt_divide power_mult eq) 1028 also have "((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) = 1029 (inverse (sqrt 2 * \<sigma>) * ((fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * (fact k)))" 1030 by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_mult 1031 power2_eq_square) 1032 finally show ?thesis 1033 unfolding normal_density_def 1034 by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>]) simp_all 1035qed 1036 1037lemma normal_moment_abs_odd: 1038 "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^(2 * k + 1)) (2^k * \<sigma>^(2 * k + 1) * fact k * sqrt (2 / pi))" 1039proof - 1040 have "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)" 1041 by (rule has_bochner_integral_cong[THEN iffD1, OF _ _ _ gaussian_moment_odd_pos[of k]]) auto 1042 from has_bochner_integral_even_function[OF this] 1043 have "has_bochner_integral lborel (\<lambda>x::real. exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)" 1044 by simp 1045 then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) 1046 (fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))" 1047 by (rule has_bochner_integral_mult_left) 1048 also have "(\<lambda>x. (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) = 1049 (\<lambda>x. exp (- (((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * \<bar>sqrt 2 * \<sigma> * x\<bar> ^ (2 * k + 1) / sqrt (2 * pi * \<sigma>\<^sup>2))" 1050 by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult real_sqrt_mult) 1051 also have "(fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) = 1052 (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * (fact k) * sqrt (2 / pi)))" 1053 by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_divide 1054 real_sqrt_mult) 1055 finally show ?thesis 1056 unfolding normal_density_def 1057 by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>]) 1058 simp_all 1059qed 1060 1061lemma normal_moment_odd: 1062 "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^(2 * k + 1)) 0" 1063proof - 1064 have "has_bochner_integral lborel (\<lambda>x. exp (- x\<^sup>2) * x^(2 * k + 1)::real) 0" 1065 using gaussian_moment_odd_pos by (rule has_bochner_integral_odd_function) simp 1066 then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*x^(2 * k + 1)) * (2^k*\<sigma>^(2*k)/sqrt pi)) 1067 (0 * (2^k*\<sigma>^(2*k)/sqrt pi))" 1068 by (rule has_bochner_integral_mult_left) 1069 also have "(\<lambda>x. (exp (-x\<^sup>2)*x^(2 * k + 1)) * (2^k*\<sigma>^(2*k)/sqrt pi)) = 1070 (\<lambda>x. exp (- ((sqrt 2 * \<sigma> * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * 1071 (sqrt 2 * \<sigma> * x * (sqrt 2 * \<sigma> * x) ^ (2 * k)) / 1072 sqrt (2 * pi * \<sigma>\<^sup>2))" 1073 unfolding real_sqrt_mult 1074 by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult fun_eq_iff) 1075 finally show ?thesis 1076 unfolding normal_density_def 1077 by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>]) simp_all 1078qed 1079 1080lemma integral_normal_moment_even: 1081 "integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^(2 * k)) = fact (2 * k) / ((2 / \<sigma>\<^sup>2)^k * fact k)" 1082 using normal_moment_even by (rule has_bochner_integral_integral_eq) 1083 1084lemma integral_normal_moment_abs_odd: 1085 "integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^(2 * k + 1)) = 2 ^ k * \<sigma> ^ (2 * k + 1) * fact k * sqrt (2 / pi)" 1086 using normal_moment_abs_odd by (rule has_bochner_integral_integral_eq) 1087 1088lemma integral_normal_moment_odd: 1089 "integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^(2 * k + 1)) = 0" 1090 using normal_moment_odd by (rule has_bochner_integral_integral_eq) 1091 1092end 1093 1094 1095context 1096 fixes \<sigma> :: real 1097 assumes \<sigma>_pos[arith]: "0 < \<sigma>" 1098begin 1099 1100lemma normal_moment_nz_1: "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x) \<mu>" 1101proof - 1102 note normal_moment_even[OF \<sigma>_pos, of \<mu> 0] 1103 note normal_moment_odd[OF \<sigma>_pos, of \<mu> 0] has_bochner_integral_mult_left[of \<mu>, OF this] 1104 note has_bochner_integral_add[OF this] 1105 then show ?thesis 1106 by (simp add: power2_eq_square field_simps) 1107qed 1108 1109lemma integral_normal_moment_nz_1: 1110 "integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x) = \<mu>" 1111 using normal_moment_nz_1 by (rule has_bochner_integral_integral_eq) 1112 1113lemma integrable_normal_moment_nz_1: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x)" 1114 using normal_moment_nz_1 by rule 1115 1116lemma integrable_normal_moment: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^k)" 1117proof cases 1118 assume "even k" then show ?thesis 1119 using integrable.intros[OF normal_moment_even] by (auto elim: evenE) 1120next 1121 assume "odd k" then show ?thesis 1122 using integrable.intros[OF normal_moment_odd] by (auto elim: oddE) 1123qed 1124 1125lemma integrable_normal_moment_abs: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^k)" 1126proof cases 1127 assume "even k" then show ?thesis 1128 using integrable.intros[OF normal_moment_even] by (auto simp add: power_even_abs elim: evenE) 1129next 1130 assume "odd k" then show ?thesis 1131 using integrable.intros[OF normal_moment_abs_odd] by (auto elim: oddE) 1132qed 1133 1134lemma integrable_normal_density[simp, intro]: "integrable lborel (normal_density \<mu> \<sigma>)" 1135 using integrable_normal_moment[of \<mu> 0] by simp 1136 1137lemma integral_normal_density[simp]: "(\<integral>x. normal_density \<mu> \<sigma> x \<partial>lborel) = 1" 1138 using integral_normal_moment_even[of \<sigma> \<mu> 0] by simp 1139 1140lemma prob_space_normal_density: 1141 "prob_space (density lborel (normal_density \<mu> \<sigma>))" 1142 proof qed (simp add: emeasure_density nn_integral_eq_integral normal_density_nonneg) 1143 1144end 1145 1146 1147 1148context 1149 fixes k :: nat 1150begin 1151 1152lemma std_normal_moment_even: 1153 "has_bochner_integral lborel (\<lambda>x. std_normal_density x * x ^ (2 * k)) (fact (2 * k) / (2^k * fact k))" 1154 using normal_moment_even[of 1 0 k] by simp 1155 1156lemma std_normal_moment_abs_odd: 1157 "has_bochner_integral lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^(2 * k + 1)) (sqrt (2/pi) * 2^k * fact k)" 1158 using normal_moment_abs_odd[of 1 0 k] by (simp add: ac_simps) 1159 1160lemma std_normal_moment_odd: 1161 "has_bochner_integral lborel (\<lambda>x. std_normal_density x * x^(2 * k + 1)) 0" 1162 using normal_moment_odd[of 1 0 k] by simp 1163 1164lemma integral_std_normal_moment_even: 1165 "integral\<^sup>L lborel (\<lambda>x. std_normal_density x * x^(2*k)) = fact (2 * k) / (2^k * fact k)" 1166 using std_normal_moment_even by (rule has_bochner_integral_integral_eq) 1167 1168lemma integral_std_normal_moment_abs_odd: 1169 "integral\<^sup>L lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^(2 * k + 1)) = sqrt (2 / pi) * 2^k * fact k" 1170 using std_normal_moment_abs_odd by (rule has_bochner_integral_integral_eq) 1171 1172lemma integral_std_normal_moment_odd: 1173 "integral\<^sup>L lborel (\<lambda>x. std_normal_density x * x^(2 * k + 1)) = 0" 1174 using std_normal_moment_odd by (rule has_bochner_integral_integral_eq) 1175 1176lemma integrable_std_normal_moment_abs: "integrable lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^k)" 1177 using integrable_normal_moment_abs[of 1 0 k] by simp 1178 1179lemma integrable_std_normal_moment: "integrable lborel (\<lambda>x. std_normal_density x * x^k)" 1180 using integrable_normal_moment[of 1 0 k] by simp 1181 1182end 1183 1184lemma (in prob_space) normal_density_affine: 1185 assumes X: "distributed M lborel X (normal_density \<mu> \<sigma>)" 1186 assumes [simp, arith]: "0 < \<sigma>" "\<alpha> \<noteq> 0" 1187 shows "distributed M lborel (\<lambda>x. \<beta> + \<alpha> * X x) (normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>))" 1188proof - 1189 have eq: "\<And>x. \<bar>\<alpha>\<bar> * normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>) (x * \<alpha> + \<beta>) = 1190 normal_density \<mu> \<sigma> x" 1191 by (simp add: normal_density_def real_sqrt_mult field_simps) 1192 (simp add: power2_eq_square field_simps) 1193 show ?thesis 1194 by (rule distributed_affineI[OF _ \<open>\<alpha> \<noteq> 0\<close>, where t=\<beta>]) 1195 (simp_all add: eq X ennreal_mult'[symmetric]) 1196qed 1197 1198lemma (in prob_space) normal_standard_normal_convert: 1199 assumes pos_var[simp, arith]: "0 < \<sigma>" 1200 shows "distributed M lborel X (normal_density \<mu> \<sigma>) = distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) std_normal_density" 1201proof auto 1202 assume "distributed M lborel X (\<lambda>x. ennreal (normal_density \<mu> \<sigma> x))" 1203 then have "distributed M lborel (\<lambda>x. -\<mu> / \<sigma> + (1/\<sigma>) * X x) (\<lambda>x. ennreal (normal_density (-\<mu> / \<sigma> + (1/\<sigma>)* \<mu>) (\<bar>1/\<sigma>\<bar> * \<sigma>) x))" 1204 by(rule normal_density_affine) auto 1205 1206 then show "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ennreal (std_normal_density x))" 1207 by (simp add: diff_divide_distrib[symmetric] field_simps) 1208next 1209 assume *: "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ennreal (std_normal_density x))" 1210 have "distributed M lborel (\<lambda>x. \<mu> + \<sigma> * ((X x - \<mu>) / \<sigma>)) (\<lambda>x. ennreal (normal_density \<mu> \<bar>\<sigma>\<bar> x))" 1211 using normal_density_affine[OF *, of \<sigma> \<mu>] by simp 1212 then show "distributed M lborel X (\<lambda>x. ennreal (normal_density \<mu> \<sigma> x))" by simp 1213qed 1214 1215lemma conv_normal_density_zero_mean: 1216 assumes [simp, arith]: "0 < \<sigma>" "0 < \<tau>" 1217 shows "(\<lambda>x. \<integral>\<^sup>+y. ennreal (normal_density 0 \<sigma> (x - y) * normal_density 0 \<tau> y) \<partial>lborel) = 1218 normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2))" (is "?LHS = ?RHS") 1219proof - 1220 define \<sigma>' \<tau>' where "\<sigma>' = \<sigma>\<^sup>2" and "\<tau>' = \<tau>\<^sup>2" 1221 then have [simp, arith]: "0 < \<sigma>'" "0 < \<tau>'" 1222 by simp_all 1223 let ?\<sigma> = "sqrt ((\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))" 1224 have sqrt: "(sqrt (2 * pi * (\<sigma>' + \<tau>')) * sqrt (2 * pi * (\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))) = 1225 (sqrt (2 * pi * \<sigma>') * sqrt (2 * pi * \<tau>'))" 1226 by (subst power_eq_iff_eq_base[symmetric, where n=2]) 1227 (simp_all add: real_sqrt_mult[symmetric] power2_eq_square) 1228 have "?LHS = 1229 (\<lambda>x. \<integral>\<^sup>+y. ennreal((normal_density 0 (sqrt (\<sigma>' + \<tau>')) x) * normal_density (\<tau>' * x / (\<sigma>' + \<tau>')) ?\<sigma> y) \<partial>lborel)" 1230 apply (intro ext nn_integral_cong) 1231 apply (simp add: normal_density_def \<sigma>'_def[symmetric] \<tau>'_def[symmetric] sqrt mult_exp_exp) 1232 apply (simp add: divide_simps power2_eq_square) 1233 apply (simp add: algebra_simps) 1234 done 1235 1236 also have "... = 1237 (\<lambda>x. (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x) * \<integral>\<^sup>+y. ennreal( normal_density (\<tau>\<^sup>2* x / (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) ?\<sigma> y) \<partial>lborel)" 1238 by (subst nn_integral_cmult[symmetric]) 1239 (auto simp: \<sigma>'_def \<tau>'_def normal_density_def ennreal_mult'[symmetric]) 1240 1241 also have "... = (\<lambda>x. (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))" 1242 by (subst nn_integral_eq_integral) (auto simp: normal_density_nonneg) 1243 1244 finally show ?thesis by fast 1245qed 1246 1247lemma conv_std_normal_density: 1248 "(\<lambda>x. \<integral>\<^sup>+y. ennreal (std_normal_density (x - y) * std_normal_density y) \<partial>lborel) = 1249 (normal_density 0 (sqrt 2))" 1250 by (subst conv_normal_density_zero_mean) simp_all 1251 1252lemma (in prob_space) add_indep_normal: 1253 assumes indep: "indep_var borel X borel Y" 1254 assumes pos_var[arith]: "0 < \<sigma>" "0 < \<tau>" 1255 assumes normalX[simp]: "distributed M lborel X (normal_density \<mu> \<sigma>)" 1256 assumes normalY[simp]: "distributed M lborel Y (normal_density \<nu> \<tau>)" 1257 shows "distributed M lborel (\<lambda>x. X x + Y x) (normal_density (\<mu> + \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))" 1258proof - 1259 have ind[simp]: "indep_var borel (\<lambda>x. - \<mu> + X x) borel (\<lambda>x. - \<nu> + Y x)" 1260 proof - 1261 have "indep_var borel ( (\<lambda>x. -\<mu> + x) o X) borel ((\<lambda>x. - \<nu> + x) o Y)" 1262 by (auto intro!: indep_var_compose assms) 1263 then show ?thesis by (simp add: o_def) 1264 qed 1265 1266 have "distributed M lborel (\<lambda>x. -\<mu> + 1 * X x) (normal_density (- \<mu> + 1 * \<mu>) (\<bar>1\<bar> * \<sigma>))" 1267 by(rule normal_density_affine[OF normalX pos_var(1), of 1 "-\<mu>"]) simp 1268 then have 1[simp]: "distributed M lborel (\<lambda>x. - \<mu> + X x) (normal_density 0 \<sigma>)" by simp 1269 1270 have "distributed M lborel (\<lambda>x. -\<nu> + 1 * Y x) (normal_density (- \<nu> + 1 * \<nu>) (\<bar>1\<bar> * \<tau>))" 1271 by(rule normal_density_affine[OF normalY pos_var(2), of 1 "-\<nu>"]) simp 1272 then have 2[simp]: "distributed M lborel (\<lambda>x. - \<nu> + Y x) (normal_density 0 \<tau>)" by simp 1273 1274 have *: "distributed M lborel (\<lambda>x. (- \<mu> + X x) + (- \<nu> + Y x)) (\<lambda>x. ennreal (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))" 1275 using distributed_convolution[OF ind 1 2] conv_normal_density_zero_mean[OF pos_var] 1276 by (simp add: ennreal_mult'[symmetric] normal_density_nonneg) 1277 1278 have "distributed M lborel (\<lambda>x. \<mu> + \<nu> + 1 * (- \<mu> + X x + (- \<nu> + Y x))) 1279 (\<lambda>x. ennreal (normal_density (\<mu> + \<nu> + 1 * 0) (\<bar>1\<bar> * sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))" 1280 by (rule normal_density_affine[OF *, of 1 "\<mu> + \<nu>"]) (auto simp: add_pos_pos) 1281 1282 then show ?thesis by auto 1283qed 1284 1285lemma (in prob_space) diff_indep_normal: 1286 assumes indep[simp]: "indep_var borel X borel Y" 1287 assumes [simp, arith]: "0 < \<sigma>" "0 < \<tau>" 1288 assumes normalX[simp]: "distributed M lborel X (normal_density \<mu> \<sigma>)" 1289 assumes normalY[simp]: "distributed M lborel Y (normal_density \<nu> \<tau>)" 1290 shows "distributed M lborel (\<lambda>x. X x - Y x) (normal_density (\<mu> - \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))" 1291proof - 1292 have "distributed M lborel (\<lambda>x. 0 + - 1 * Y x) (\<lambda>x. ennreal (normal_density (0 + - 1 * \<nu>) (\<bar>- 1\<bar> * \<tau>) x))" 1293 by(rule normal_density_affine, auto) 1294 then have [simp]:"distributed M lborel (\<lambda>x. - Y x) (\<lambda>x. ennreal (normal_density (- \<nu>) \<tau> x))" by simp 1295 1296 have "distributed M lborel (\<lambda>x. X x + (- Y x)) (normal_density (\<mu> + - \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))" 1297 apply (rule add_indep_normal) 1298 apply (rule indep_var_compose[unfolded comp_def, of borel _ borel _ "\<lambda>x. x" _ "\<lambda>x. - x"]) 1299 apply simp_all 1300 done 1301 then show ?thesis by simp 1302qed 1303 1304lemma (in prob_space) sum_indep_normal: 1305 assumes "finite I" "I \<noteq> {}" "indep_vars (\<lambda>i. borel) X I" 1306 assumes "\<And>i. i \<in> I \<Longrightarrow> 0 < \<sigma> i" 1307 assumes normal: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (normal_density (\<mu> i) (\<sigma> i))" 1308 shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (normal_density (\<Sum>i\<in>I. \<mu> i) (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2)))" 1309 using assms 1310proof (induct I rule: finite_ne_induct) 1311 case (singleton i) then show ?case by (simp add : abs_of_pos) 1312next 1313 case (insert i I) 1314 then have 1: "distributed M lborel (\<lambda>x. (X i x) + (\<Sum>i\<in>I. X i x)) 1315 (normal_density (\<mu> i + sum \<mu> I) (sqrt ((\<sigma> i)\<^sup>2 + (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2))\<^sup>2)))" 1316 apply (intro add_indep_normal indep_vars_sum insert real_sqrt_gt_zero) 1317 apply (auto intro: indep_vars_subset intro!: sum_pos) 1318 apply fastforce 1319 done 1320 have 2: "(\<lambda>x. (X i x)+ (\<Sum>i\<in>I. X i x)) = (\<lambda>x. (\<Sum>j\<in>insert i I. X j x))" 1321 "\<mu> i + sum \<mu> I = sum \<mu> (insert i I)" 1322 using insert by auto 1323 1324 have 3: "(sqrt ((\<sigma> i)\<^sup>2 + (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2))\<^sup>2)) = (sqrt (\<Sum>i\<in>insert i I. (\<sigma> i)\<^sup>2))" 1325 using insert by (simp add: sum_nonneg) 1326 1327 show ?case using 1 2 3 by simp 1328qed 1329 1330lemma (in prob_space) standard_normal_distributed_expectation: 1331 assumes D: "distributed M lborel X std_normal_density" 1332 shows "expectation X = 0" 1333 using integral_std_normal_moment_odd[of 0] 1334 distributed_integral[OF D, of "\<lambda>x. x", symmetric] 1335 by (auto simp: ) 1336 1337lemma (in prob_space) normal_distributed_expectation: 1338 assumes \<sigma>[arith]: "0 < \<sigma>" 1339 assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)" 1340 shows "expectation X = \<mu>" 1341 using integral_normal_moment_nz_1[OF \<sigma>, of \<mu>] distributed_integral[OF D, of "\<lambda>x. x", symmetric] 1342 by (auto simp: field_simps) 1343 1344lemma (in prob_space) normal_distributed_variance: 1345 fixes a b :: real 1346 assumes [simp, arith]: "0 < \<sigma>" 1347 assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)" 1348 shows "variance X = \<sigma>\<^sup>2" 1349 using integral_normal_moment_even[of \<sigma> \<mu> 1] 1350 by (subst distributed_integral[OF D, symmetric]) 1351 (simp_all add: eval_nat_numeral normal_distributed_expectation[OF assms]) 1352 1353lemma (in prob_space) standard_normal_distributed_variance: 1354 "distributed M lborel X std_normal_density \<Longrightarrow> variance X = 1" 1355 using normal_distributed_variance[of 1 X 0] by simp 1356 1357lemma (in information_space) entropy_normal_density: 1358 assumes [arith]: "0 < \<sigma>" 1359 assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)" 1360 shows "entropy b lborel X = log b (2 * pi * exp 1 * \<sigma>\<^sup>2) / 2" 1361proof - 1362 have "entropy b lborel X = - (\<integral> x. normal_density \<mu> \<sigma> x * log b (normal_density \<mu> \<sigma> x) \<partial>lborel)" 1363 using D by (rule entropy_distr) simp 1364 also have "\<dots> = - (\<integral> x. normal_density \<mu> \<sigma> x * (- ln (2 * pi * \<sigma>\<^sup>2) - (x - \<mu>)\<^sup>2 / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)" 1365 by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) 1366 (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt) 1367 also have "\<dots> = - (\<integral>x. - (normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)" 1368 by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) (auto simp: field_split_simps field_simps) 1369 also have "\<dots> = (\<integral>x. normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2 \<partial>lborel) / (2 * ln b)" 1370 by (simp del: minus_add_distrib) 1371 also have "\<dots> = (ln (2 * pi * \<sigma>\<^sup>2) + 1) / (2 * ln b)" 1372 using integral_normal_moment_even[of \<sigma> \<mu> 1] by (simp add: integrable_normal_moment fact_numeral) 1373 also have "\<dots> = log b (2 * pi * exp 1 * \<sigma>\<^sup>2) / 2" 1374 by (simp add: log_def field_simps ln_mult) 1375 finally show ?thesis . 1376qed 1377 1378end 1379