src/HOL/Probability/Distributions.thy
 author hoelzl Mon Apr 14 13:08:17 2014 +0200 (2014-04-14) changeset 56571 f4635657d66f parent 56536 aefb4a8da31f child 56993 e5366291d6aa permissions -rw-r--r--
 hoelzl@50419 ` 1` ```theory Distributions ``` hoelzl@50419 ` 2` ``` imports Probability_Measure ``` hoelzl@50419 ` 3` ```begin ``` hoelzl@50419 ` 4` hoelzl@50419 ` 5` ```subsection {* Exponential distribution *} ``` hoelzl@50419 ` 6` hoelzl@50419 ` 7` ```definition exponential_density :: "real \ real \ real" where ``` hoelzl@50419 ` 8` ``` "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))" ``` hoelzl@50419 ` 9` hoelzl@50419 ` 10` ```lemma borel_measurable_exponential_density[measurable]: "exponential_density l \ borel_measurable borel" ``` hoelzl@50419 ` 11` ``` by (auto simp add: exponential_density_def[abs_def]) ``` hoelzl@50419 ` 12` hoelzl@50419 ` 13` ```lemma (in prob_space) exponential_distributed_params: ``` hoelzl@50419 ` 14` ``` assumes D: "distributed M lborel X (exponential_density l)" ``` hoelzl@50419 ` 15` ``` shows "0 < l" ``` hoelzl@50419 ` 16` ```proof (cases l "0 :: real" rule: linorder_cases) ``` hoelzl@50419 ` 17` ``` assume "l < 0" ``` hoelzl@50419 ` 18` ``` have "emeasure lborel {0 <.. 1::real} \ ``` hoelzl@50419 ` 19` ``` emeasure lborel {x :: real \ space lborel. 0 < x}" ``` hoelzl@50419 ` 20` ``` by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric]) ``` hoelzl@50419 ` 21` ``` also have "emeasure lborel {x :: real \ space lborel. 0 < x} = 0" ``` hoelzl@50419 ` 22` ``` proof - ``` hoelzl@50419 ` 23` ``` have "AE x in lborel. 0 \ exponential_density l x" ``` hoelzl@50419 ` 24` ``` using assms by (auto simp: distributed_real_AE) ``` hoelzl@50419 ` 25` ``` then have "AE x in lborel. x \ (0::real)" ``` hoelzl@50419 ` 26` ``` apply eventually_elim ``` hoelzl@50419 ` 27` ``` using `l < 0` ``` hoelzl@50419 ` 28` ``` apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm) ``` hoelzl@50419 ` 29` ``` done ``` hoelzl@50419 ` 30` ``` then show "emeasure lborel {x :: real \ space lborel. 0 < x} = 0" ``` hoelzl@50419 ` 31` ``` by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric]) ``` hoelzl@50419 ` 32` ``` qed ``` hoelzl@50419 ` 33` ``` finally show "0 < l" by simp ``` hoelzl@50419 ` 34` ```next ``` hoelzl@50419 ` 35` ``` assume "l = 0" ``` hoelzl@50419 ` 36` ``` then have [simp]: "\x. ereal (exponential_density l x) = 0" ``` hoelzl@50419 ` 37` ``` by (simp add: exponential_density_def) ``` hoelzl@50419 ` 38` ``` interpret X: prob_space "distr M lborel X" ``` hoelzl@50419 ` 39` ``` using distributed_measurable[OF D] by (rule prob_space_distr) ``` hoelzl@50419 ` 40` ``` from X.emeasure_space_1 ``` hoelzl@50419 ` 41` ``` show "0 < l" ``` hoelzl@50419 ` 42` ``` by (simp add: emeasure_density distributed_distr_eq_density[OF D]) ``` hoelzl@50419 ` 43` ```qed assumption ``` hoelzl@50419 ` 44` hoelzl@50419 ` 45` ```lemma ``` hoelzl@50419 ` 46` ``` assumes [arith]: "0 < l" ``` hoelzl@50419 ` 47` ``` shows emeasure_exponential_density_le0: "0 \ a \ emeasure (density lborel (exponential_density l)) {.. a} = 1 - exp (- a * l)" ``` hoelzl@50419 ` 48` ``` and prob_space_exponential_density: "prob_space (density lborel (exponential_density l))" ``` hoelzl@50419 ` 49` ``` (is "prob_space ?D") ``` hoelzl@50419 ` 50` ```proof - ``` hoelzl@50419 ` 51` ``` let ?f = "\x. l * exp (- x * l)" ``` hoelzl@50419 ` 52` ``` let ?F = "\x. - exp (- x * l)" ``` hoelzl@50419 ` 53` hoelzl@50419 ` 54` ``` have deriv: "\x. DERIV ?F x :> ?f x" "\x. 0 \ l * exp (- x * l)" ``` hoelzl@56381 ` 55` ``` by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff) ``` hoelzl@50419 ` 56` wenzelm@53015 ` 57` ``` have "emeasure ?D (space ?D) = (\\<^sup>+ x. ereal (?f x) * indicator {0..} x \lborel)" ``` hoelzl@50419 ` 58` ``` by (auto simp: emeasure_density exponential_density_def ``` hoelzl@50419 ` 59` ``` intro!: positive_integral_cong split: split_indicator) ``` hoelzl@50419 ` 60` ``` also have "\ = ereal (0 - ?F 0)" ``` hoelzl@50419 ` 61` ``` proof (rule positive_integral_FTC_atLeast) ``` hoelzl@50419 ` 62` ``` have "((\x. exp (l * x)) ---> 0) at_bot" ``` hoelzl@50419 ` 63` ``` by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]]) ``` hoelzl@50419 ` 64` ``` (simp_all add: tendsto_const filterlim_ident) ``` hoelzl@50419 ` 65` ``` then show "((\x. - exp (- x * l)) ---> 0) at_top" ``` hoelzl@50419 ` 66` ``` unfolding filterlim_at_top_mirror ``` hoelzl@50419 ` 67` ``` by (simp add: tendsto_minus_cancel_left[symmetric] ac_simps) ``` hoelzl@50419 ` 68` ``` qed (insert deriv, auto) ``` hoelzl@50419 ` 69` ``` also have "\ = 1" by (simp add: one_ereal_def) ``` hoelzl@50419 ` 70` ``` finally have "emeasure ?D (space ?D) = 1" . ``` hoelzl@50419 ` 71` ``` then show "prob_space ?D" by rule ``` hoelzl@50419 ` 72` hoelzl@50419 ` 73` ``` assume "0 \ a" ``` wenzelm@53015 ` 74` ``` have "emeasure ?D {..a} = (\\<^sup>+x. ereal (?f x) * indicator {0..a} x \lborel)" ``` hoelzl@50419 ` 75` ``` by (auto simp add: emeasure_density intro!: positive_integral_cong split: split_indicator) ``` hoelzl@50419 ` 76` ``` (auto simp: exponential_density_def) ``` wenzelm@53015 ` 77` ``` also have "(\\<^sup>+x. ereal (?f x) * indicator {0..a} x \lborel) = ereal (?F a) - ereal (?F 0)" ``` hoelzl@50419 ` 78` ``` using `0 \ a` deriv by (intro positive_integral_FTC_atLeastAtMost) auto ``` hoelzl@50419 ` 79` ``` also have "\ = 1 - exp (- a * l)" ``` hoelzl@50419 ` 80` ``` by simp ``` hoelzl@50419 ` 81` ``` finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" . ``` hoelzl@50419 ` 82` ```qed ``` hoelzl@50419 ` 83` hoelzl@50419 ` 84` hoelzl@50419 ` 85` ```lemma (in prob_space) exponential_distributedD_le: ``` hoelzl@50419 ` 86` ``` assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" ``` hoelzl@50419 ` 87` ``` shows "\

(x in M. X x \ a) = 1 - exp (- a * l)" ``` hoelzl@50419 ` 88` ```proof - ``` hoelzl@50419 ` 89` ``` have "emeasure M {x \ space M. X x \ a } = emeasure (distr M lborel X) {.. a}" ``` hoelzl@50419 ` 90` ``` using distributed_measurable[OF D] ``` hoelzl@50419 ` 91` ``` by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) ``` hoelzl@50419 ` 92` ``` also have "\ = emeasure (density lborel (exponential_density l)) {.. a}" ``` hoelzl@50419 ` 93` ``` unfolding distributed_distr_eq_density[OF D] .. ``` hoelzl@50419 ` 94` ``` also have "\ = 1 - exp (- a * l)" ``` hoelzl@50419 ` 95` ``` using emeasure_exponential_density_le0[OF exponential_distributed_params[OF D] a] . ``` hoelzl@50419 ` 96` ``` finally show ?thesis ``` hoelzl@50419 ` 97` ``` by (auto simp: measure_def) ``` hoelzl@50419 ` 98` ```qed ``` hoelzl@50419 ` 99` hoelzl@50419 ` 100` ```lemma (in prob_space) exponential_distributedD_gt: ``` hoelzl@50419 ` 101` ``` assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a" ``` hoelzl@50419 ` 102` ``` shows "\

(x in M. a < X x ) = exp (- a * l)" ``` hoelzl@50419 ` 103` ```proof - ``` hoelzl@50419 ` 104` ``` have "exp (- a * l) = 1 - \

(x in M. X x \ a)" ``` hoelzl@50419 ` 105` ``` unfolding exponential_distributedD_le[OF D a] by simp ``` hoelzl@50419 ` 106` ``` also have "\ = prob (space M - {x \ space M. X x \ a })" ``` hoelzl@50419 ` 107` ``` using distributed_measurable[OF D] ``` hoelzl@50419 ` 108` ``` by (subst prob_compl) auto ``` hoelzl@50419 ` 109` ``` also have "\ = \

(x in M. a < X x )" ``` hoelzl@50419 ` 110` ``` by (auto intro!: arg_cong[where f=prob] simp: not_le) ``` hoelzl@50419 ` 111` ``` finally show ?thesis by simp ``` hoelzl@50419 ` 112` ```qed ``` hoelzl@50419 ` 113` hoelzl@50419 ` 114` ```lemma (in prob_space) exponential_distributed_memoryless: ``` hoelzl@50419 ` 115` ``` assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \ a"and t: "0 \ t" ``` hoelzl@50419 ` 116` ``` shows "\

(x in M. a + t < X x \ a < X x) = \

(x in M. t < X x)" ``` hoelzl@50419 ` 117` ```proof - ``` hoelzl@50419 ` 118` ``` have "\

(x in M. a + t < X x \ a < X x) = \

(x in M. a + t < X x) / \

(x in M. a < X x)" ``` hoelzl@50419 ` 119` ``` using `0 \ t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"]) ``` hoelzl@50419 ` 120` ``` also have "\ = exp (- (a + t) * l) / exp (- a * l)" ``` hoelzl@50419 ` 121` ``` using a t by (simp add: exponential_distributedD_gt[OF D]) ``` hoelzl@50419 ` 122` ``` also have "\ = exp (- t * l)" ``` hoelzl@50419 ` 123` ``` using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric]) ``` hoelzl@50419 ` 124` ``` finally show ?thesis ``` hoelzl@50419 ` 125` ``` using t by (simp add: exponential_distributedD_gt[OF D]) ``` hoelzl@50419 ` 126` ```qed ``` hoelzl@50419 ` 127` hoelzl@50419 ` 128` ```lemma exponential_distributedI: ``` hoelzl@50419 ` 129` ``` assumes X[measurable]: "X \ borel_measurable M" and [arith]: "0 < l" ``` hoelzl@50419 ` 130` ``` and X_distr: "\a. 0 \ a \ emeasure M {x\space M. X x \ a} = 1 - exp (- a * l)" ``` hoelzl@50419 ` 131` ``` shows "distributed M lborel X (exponential_density l)" ``` hoelzl@50419 ` 132` ```proof (rule distributedI_borel_atMost) ``` hoelzl@50419 ` 133` ``` fix a :: real ``` hoelzl@50419 ` 134` hoelzl@50419 ` 135` ``` { assume "a \ 0" ``` hoelzl@50419 ` 136` ``` with X have "emeasure M {x\space M. X x \ a} \ emeasure M {x\space M. X x \ 0}" ``` hoelzl@50419 ` 137` ``` by (intro emeasure_mono) auto ``` hoelzl@50419 ` 138` ``` then have "emeasure M {x\space M. X x \ a} = 0" ``` hoelzl@50419 ` 139` ``` using X_distr[of 0] by (simp add: one_ereal_def emeasure_le_0_iff) } ``` hoelzl@50419 ` 140` ``` note eq_0 = this ``` hoelzl@50419 ` 141` hoelzl@50419 ` 142` ``` have "\x. \ 0 \ a \ ereal (exponential_density l x) * indicator {..a} x = 0" ``` hoelzl@50419 ` 143` ``` by (simp add: exponential_density_def) ``` wenzelm@53015 ` 144` ``` then show "(\\<^sup>+ x. exponential_density l x * indicator {..a} x \lborel) = ereal (if 0 \ a then 1 - exp (- a * l) else 0)" ``` hoelzl@50419 ` 145` ``` using emeasure_exponential_density_le0[of l a] ``` hoelzl@50419 ` 146` ``` by (auto simp: emeasure_density times_ereal.simps[symmetric] ereal_indicator ``` hoelzl@50419 ` 147` ``` simp del: times_ereal.simps ereal_zero_times) ``` hoelzl@50419 ` 148` ``` show "emeasure M {x\space M. X x \ a} = ereal (if 0 \ a then 1 - exp (- a * l) else 0)" ``` hoelzl@50419 ` 149` ``` using X_distr[of a] eq_0 by (auto simp: one_ereal_def) ``` hoelzl@50419 ` 150` ``` show "AE x in lborel. 0 \ exponential_density l x " ``` nipkow@56536 ` 151` ``` by (auto simp: exponential_density_def) ``` hoelzl@50419 ` 152` ```qed simp_all ``` hoelzl@50419 ` 153` hoelzl@50419 ` 154` ```lemma (in prob_space) exponential_distributed_iff: ``` hoelzl@50419 ` 155` ``` "distributed M lborel X (exponential_density l) \ ``` hoelzl@50419 ` 156` ``` (X \ borel_measurable M \ 0 < l \ (\a\0. \

(x in M. X x \ a) = 1 - exp (- a * l)))" ``` hoelzl@50419 ` 157` ``` using ``` hoelzl@50419 ` 158` ``` distributed_measurable[of M lborel X "exponential_density l"] ``` hoelzl@50419 ` 159` ``` exponential_distributed_params[of X l] ``` hoelzl@50419 ` 160` ``` emeasure_exponential_density_le0[of l] ``` hoelzl@50419 ` 161` ``` exponential_distributedD_le[of X l] ``` hoelzl@50419 ` 162` ``` by (auto intro!: exponential_distributedI simp: one_ereal_def emeasure_eq_measure) ``` hoelzl@50419 ` 163` hoelzl@50419 ` 164` ```lemma borel_integral_x_exp: ``` hoelzl@50419 ` 165` ``` "(\x. x * exp (- x) * indicator {0::real ..} x \lborel) = 1" ``` hoelzl@50419 ` 166` ```proof (rule integral_monotone_convergence) ``` hoelzl@50419 ` 167` ``` let ?f = "\i x. x * exp (- x) * indicator {0::real .. i} x" ``` hoelzl@50419 ` 168` ``` have "eventually (\b::real. 0 \ b) at_top" ``` hoelzl@50419 ` 169` ``` by (rule eventually_ge_at_top) ``` wenzelm@53015 ` 170` ``` then have "eventually (\b. 1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)) at_top" ``` hoelzl@50419 ` 171` ``` proof eventually_elim ``` hoelzl@50419 ` 172` ``` fix b :: real assume [simp]: "0 \ b" ``` wenzelm@53015 ` 173` ``` have "(\x. (exp (-x)) * indicator {0 .. b} x \lborel) - (integral\<^sup>L lborel (?f b)) = ``` hoelzl@50419 ` 174` ``` (\x. (exp (-x) - x * exp (-x)) * indicator {0 .. b} x \lborel)" ``` hoelzl@50419 ` 175` ``` by (subst integral_diff(2)[symmetric]) ``` hoelzl@50419 ` 176` ``` (auto intro!: borel_integrable_atLeastAtMost integral_cong split: split_indicator) ``` hoelzl@50419 ` 177` ``` also have "\ = b * exp (-b) - 0 * exp (- 0)" ``` hoelzl@50419 ` 178` ``` proof (rule integral_FTC_atLeastAtMost) ``` hoelzl@50419 ` 179` ``` fix x assume "0 \ x" "x \ b" ``` hoelzl@50419 ` 180` ``` show "DERIV (\x. x * exp (-x)) x :> exp (-x) - x * exp (-x)" ``` hoelzl@56381 ` 181` ``` by (auto intro!: derivative_eq_intros) ``` hoelzl@50419 ` 182` ``` show "isCont (\x. exp (- x) - x * exp (- x)) x " ``` hoelzl@56371 ` 183` ``` by (intro continuous_intros) ``` hoelzl@50419 ` 184` ``` qed fact ``` hoelzl@50419 ` 185` ``` also have "(\x. (exp (-x)) * indicator {0 .. b} x \lborel) = - exp (- b) - - exp (- 0)" ``` hoelzl@56381 ` 186` ``` by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros) ``` wenzelm@53015 ` 187` ``` finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)" ``` hoelzl@50419 ` 188` ``` by (auto simp: field_simps exp_minus inverse_eq_divide) ``` hoelzl@50419 ` 189` ``` qed ``` wenzelm@53015 ` 190` ``` then have "((\i. integral\<^sup>L lborel (?f i)) ---> 1 - (0 + 0)) at_top" ``` hoelzl@50419 ` 191` ``` proof (rule Lim_transform_eventually) ``` hoelzl@50419 ` 192` ``` show "((\i. 1 - (inverse (exp i) + i / exp i)) ---> 1 - (0 + 0 :: real)) at_top" ``` hoelzl@50419 ` 193` ``` using tendsto_power_div_exp_0[of 1] ``` hoelzl@50419 ` 194` ``` by (intro tendsto_intros tendsto_inverse_0_at_top exp_at_top) simp ``` hoelzl@50419 ` 195` ``` qed ``` wenzelm@53015 ` 196` ``` then show "(\i. integral\<^sup>L lborel (?f i)) ----> 1" ``` hoelzl@50419 ` 197` ``` by (intro filterlim_compose[OF _ filterlim_real_sequentially]) simp ``` hoelzl@50419 ` 198` ``` show "AE x in lborel. mono (\n::nat. x * exp (- x) * indicator {0..real n} x)" ``` hoelzl@50419 ` 199` ``` by (auto simp: mono_def mult_le_0_iff zero_le_mult_iff split: split_indicator) ``` hoelzl@50419 ` 200` ``` show "\i::nat. integrable lborel (\x. x * exp (- x) * indicator {0..real i} x)" ``` hoelzl@50419 ` 201` ``` by (rule borel_integrable_atLeastAtMost) auto ``` hoelzl@50419 ` 202` ``` show "AE x in lborel. (\i. x * exp (- x) * indicator {0..real i} x) ----> x * exp (- x) * indicator {0..} x" ``` hoelzl@50419 ` 203` ``` apply (intro AE_I2 Lim_eventually ) ``` hoelzl@50419 ` 204` ``` apply (rule_tac c="natfloor x + 1" in eventually_sequentiallyI) ``` hoelzl@50419 ` 205` ``` apply (auto simp add: not_le dest!: ge_natfloor_plus_one_imp_gt[simplified] split: split_indicator) ``` hoelzl@50419 ` 206` ``` done ``` hoelzl@50419 ` 207` ```qed (auto intro!: borel_measurable_times borel_measurable_exp) ``` hoelzl@50419 ` 208` hoelzl@50419 ` 209` ```lemma (in prob_space) exponential_distributed_expectation: ``` hoelzl@50419 ` 210` ``` assumes D: "distributed M lborel X (exponential_density l)" ``` hoelzl@50419 ` 211` ``` shows "expectation X = 1 / l" ``` hoelzl@50419 ` 212` ```proof (subst distributed_integral[OF D, of "\x. x", symmetric]) ``` hoelzl@50419 ` 213` ``` have "0 < l" ``` hoelzl@50419 ` 214` ``` using exponential_distributed_params[OF D] . ``` hoelzl@50419 ` 215` ``` have [simp]: "\x. x * (l * (exp (- (x * l)) * indicator {0..} (x * l))) = ``` hoelzl@50419 ` 216` ``` x * exponential_density l x" ``` hoelzl@50419 ` 217` ``` using `0 < l` ``` hoelzl@50419 ` 218` ``` by (auto split: split_indicator simp: zero_le_mult_iff exponential_density_def) ``` hoelzl@50419 ` 219` ``` from borel_integral_x_exp `0 < l` ``` hoelzl@50419 ` 220` ``` show "(\ x. exponential_density l x * x \lborel) = 1 / l" ``` hoelzl@50419 ` 221` ``` by (subst (asm) lebesgue_integral_real_affine[of "l" _ 0]) ``` hoelzl@50419 ` 222` ``` (simp_all add: borel_measurable_exp nonzero_eq_divide_eq ac_simps) ``` hoelzl@50419 ` 223` ```qed simp ``` hoelzl@50419 ` 224` hoelzl@50419 ` 225` ```subsection {* Uniform distribution *} ``` hoelzl@50419 ` 226` hoelzl@50419 ` 227` ```lemma uniform_distrI: ``` hoelzl@50419 ` 228` ``` assumes X: "X \ measurable M M'" ``` hoelzl@50419 ` 229` ``` and A: "A \ sets M'" "emeasure M' A \ \" "emeasure M' A \ 0" ``` hoelzl@50419 ` 230` ``` assumes distr: "\B. B \ sets M' \ emeasure M (X -` B \ space M) = emeasure M' (A \ B) / emeasure M' A" ``` hoelzl@50419 ` 231` ``` shows "distr M M' X = uniform_measure M' A" ``` hoelzl@50419 ` 232` ``` unfolding uniform_measure_def ``` hoelzl@50419 ` 233` ```proof (intro measure_eqI) ``` hoelzl@50419 ` 234` ``` let ?f = "\x. indicator A x / emeasure M' A" ``` hoelzl@50419 ` 235` ``` fix B assume B: "B \ sets (distr M M' X)" ``` hoelzl@50419 ` 236` ``` with X have "emeasure M (X -` B \ space M) = emeasure M' (A \ B) / emeasure M' A" ``` hoelzl@50419 ` 237` ``` by (simp add: distr[of B] measurable_sets) ``` hoelzl@50419 ` 238` ``` also have "\ = (1 / emeasure M' A) * emeasure M' (A \ B)" ``` hoelzl@50419 ` 239` ``` by simp ``` wenzelm@53015 ` 240` ``` also have "\ = (\\<^sup>+ x. (1 / emeasure M' A) * indicator (A \ B) x \M')" ``` hoelzl@50419 ` 241` ``` using A B ``` hoelzl@50419 ` 242` ``` by (intro positive_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal) ``` wenzelm@53015 ` 243` ``` also have "\ = (\\<^sup>+ x. ?f x * indicator B x \M')" ``` hoelzl@50419 ` 244` ``` by (rule positive_integral_cong) (auto split: split_indicator) ``` hoelzl@50419 ` 245` ``` finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B" ``` hoelzl@50419 ` 246` ``` using A B X by (auto simp add: emeasure_distr emeasure_density) ``` hoelzl@50419 ` 247` ```qed simp ``` hoelzl@50419 ` 248` hoelzl@50419 ` 249` ```lemma uniform_distrI_borel: ``` hoelzl@50419 ` 250` ``` fixes A :: "real set" ``` hoelzl@50419 ` 251` ``` assumes X[measurable]: "X \ borel_measurable M" and A: "emeasure lborel A = ereal r" "0 < r" ``` hoelzl@50419 ` 252` ``` and [measurable]: "A \ sets borel" ``` hoelzl@50419 ` 253` ``` assumes distr: "\a. emeasure M {x\space M. X x \ a} = emeasure lborel (A \ {.. a}) / r" ``` hoelzl@50419 ` 254` ``` shows "distributed M lborel X (\x. indicator A x / measure lborel A)" ``` hoelzl@50419 ` 255` ```proof (rule distributedI_borel_atMost) ``` hoelzl@50419 ` 256` ``` let ?f = "\x. 1 / r * indicator A x" ``` hoelzl@50419 ` 257` ``` fix a ``` hoelzl@50419 ` 258` ``` have "emeasure lborel (A \ {..a}) \ emeasure lborel A" ``` hoelzl@50419 ` 259` ``` using A by (intro emeasure_mono) auto ``` hoelzl@50419 ` 260` ``` also have "\ < \" ``` hoelzl@50419 ` 261` ``` using A by simp ``` hoelzl@50419 ` 262` ``` finally have fin: "emeasure lborel (A \ {..a}) \ \" ``` hoelzl@50419 ` 263` ``` by simp ``` hoelzl@50419 ` 264` ``` from emeasure_eq_ereal_measure[OF this] ``` hoelzl@50419 ` 265` ``` have fin_eq: "emeasure lborel (A \ {..a}) / r = ereal (measure lborel (A \ {..a}) / r)" ``` hoelzl@50419 ` 266` ``` using A by simp ``` hoelzl@50419 ` 267` ``` then show "emeasure M {x\space M. X x \ a} = ereal (measure lborel (A \ {..a}) / r)" ``` hoelzl@50419 ` 268` ``` using distr by simp ``` hoelzl@50419 ` 269` ``` ``` wenzelm@53015 ` 270` ``` have "(\\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \lborel) = ``` wenzelm@53015 ` 271` ``` (\\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \ {..a}) x \lborel)" ``` hoelzl@50419 ` 272` ``` by (auto intro!: positive_integral_cong split: split_indicator) ``` hoelzl@50419 ` 273` ``` also have "\ = ereal (1 / measure lborel A) * emeasure lborel (A \ {..a})" ``` hoelzl@50419 ` 274` ``` using `A \ sets borel` ``` hoelzl@50419 ` 275` ``` by (intro positive_integral_cmult_indicator) (auto simp: measure_nonneg) ``` hoelzl@50419 ` 276` ``` also have "\ = ereal (measure lborel (A \ {..a}) / r)" ``` hoelzl@50419 ` 277` ``` unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def) ``` wenzelm@53015 ` 278` ``` finally show "(\\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \lborel) = ``` hoelzl@50419 ` 279` ``` ereal (measure lborel (A \ {..a}) / r)" . ``` hoelzl@56571 ` 280` ```qed (auto simp: measure_nonneg) ``` hoelzl@50419 ` 281` hoelzl@50419 ` 282` ```lemma (in prob_space) uniform_distrI_borel_atLeastAtMost: ``` hoelzl@50419 ` 283` ``` fixes a b :: real ``` hoelzl@50419 ` 284` ``` assumes X: "X \ borel_measurable M" and "a < b" ``` hoelzl@50419 ` 285` ``` assumes distr: "\t. a \ t \ t \ b \ \

(x in M. X x \ t) = (t - a) / (b - a)" ``` hoelzl@50419 ` 286` ``` shows "distributed M lborel X (\x. indicator {a..b} x / measure lborel {a..b})" ``` hoelzl@50419 ` 287` ```proof (rule uniform_distrI_borel) ``` hoelzl@50419 ` 288` ``` fix t ``` hoelzl@50419 ` 289` ``` have "t < a \ (a \ t \ t \ b) \ b < t" ``` hoelzl@50419 ` 290` ``` by auto ``` hoelzl@50419 ` 291` ``` then show "emeasure M {x\space M. X x \ t} = emeasure lborel ({a .. b} \ {..t}) / (b - a)" ``` hoelzl@50419 ` 292` ``` proof (elim disjE conjE) ``` hoelzl@50419 ` 293` ``` assume "t < a" ``` hoelzl@50419 ` 294` ``` then have "emeasure M {x\space M. X x \ t} \ emeasure M {x\space M. X x \ a}" ``` hoelzl@50419 ` 295` ``` using X by (auto intro!: emeasure_mono measurable_sets) ``` hoelzl@50419 ` 296` ``` also have "\ = 0" ``` hoelzl@50419 ` 297` ``` using distr[of a] `a < b` by (simp add: emeasure_eq_measure) ``` hoelzl@50419 ` 298` ``` finally have "emeasure M {x\space M. X x \ t} = 0" ``` hoelzl@50419 ` 299` ``` by (simp add: antisym measure_nonneg emeasure_le_0_iff) ``` hoelzl@50419 ` 300` ``` with `t < a` show ?thesis by simp ``` hoelzl@50419 ` 301` ``` next ``` hoelzl@50419 ` 302` ``` assume bnds: "a \ t" "t \ b" ``` hoelzl@50419 ` 303` ``` have "{a..b} \ {..t} = {a..t}" ``` hoelzl@50419 ` 304` ``` using bnds by auto ``` hoelzl@50419 ` 305` ``` then show ?thesis using `a \ t` `a < b` ``` hoelzl@50419 ` 306` ``` using distr[OF bnds] by (simp add: emeasure_eq_measure) ``` hoelzl@50419 ` 307` ``` next ``` hoelzl@50419 ` 308` ``` assume "b < t" ``` hoelzl@50419 ` 309` ``` have "1 = emeasure M {x\space M. X x \ b}" ``` hoelzl@50419 ` 310` ``` using distr[of b] `a < b` by (simp add: one_ereal_def emeasure_eq_measure) ``` hoelzl@50419 ` 311` ``` also have "\ \ emeasure M {x\space M. X x \ t}" ``` hoelzl@50419 ` 312` ``` using X `b < t` by (auto intro!: emeasure_mono measurable_sets) ``` hoelzl@50419 ` 313` ``` finally have "emeasure M {x\space M. X x \ t} = 1" ``` hoelzl@50419 ` 314` ``` by (simp add: antisym emeasure_eq_measure one_ereal_def) ``` hoelzl@50419 ` 315` ``` with `b < t` `a < b` show ?thesis by (simp add: measure_def one_ereal_def) ``` hoelzl@50419 ` 316` ``` qed ``` hoelzl@50419 ` 317` ```qed (insert X `a < b`, auto) ``` hoelzl@50419 ` 318` hoelzl@50419 ` 319` ```lemma (in prob_space) uniform_distributed_measure: ``` hoelzl@50419 ` 320` ``` fixes a b :: real ``` hoelzl@50419 ` 321` ``` assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" ``` hoelzl@50419 ` 322` ``` assumes " a \ t" "t \ b" ``` hoelzl@50419 ` 323` ``` shows "\

(x in M. X x \ t) = (t - a) / (b - a)" ``` hoelzl@50419 ` 324` ```proof - ``` hoelzl@50419 ` 325` ``` have "emeasure M {x \ space M. X x \ t} = emeasure (distr M lborel X) {.. t}" ``` hoelzl@50419 ` 326` ``` using distributed_measurable[OF D] ``` hoelzl@50419 ` 327` ``` by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure]) ``` wenzelm@53015 ` 328` ``` also have "\ = (\\<^sup>+x. ereal (1 / (b - a)) * indicator {a .. t} x \lborel)" ``` hoelzl@50419 ` 329` ``` using distributed_borel_measurable[OF D] `a \ t` `t \ b` ``` hoelzl@50419 ` 330` ``` unfolding distributed_distr_eq_density[OF D] ``` hoelzl@50419 ` 331` ``` by (subst emeasure_density) ``` hoelzl@50419 ` 332` ``` (auto intro!: positive_integral_cong simp: measure_def split: split_indicator) ``` hoelzl@50419 ` 333` ``` also have "\ = ereal (1 / (b - a)) * (t - a)" ``` hoelzl@50419 ` 334` ``` using `a \ t` `t \ b` ``` hoelzl@50419 ` 335` ``` by (subst positive_integral_cmult_indicator) auto ``` hoelzl@50419 ` 336` ``` finally show ?thesis ``` hoelzl@50419 ` 337` ``` by (simp add: measure_def) ``` hoelzl@50419 ` 338` ```qed ``` hoelzl@50419 ` 339` hoelzl@50419 ` 340` ```lemma (in prob_space) uniform_distributed_bounds: ``` hoelzl@50419 ` 341` ``` fixes a b :: real ``` hoelzl@50419 ` 342` ``` assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" ``` hoelzl@50419 ` 343` ``` shows "a < b" ``` hoelzl@50419 ` 344` ```proof (rule ccontr) ``` hoelzl@50419 ` 345` ``` assume "\ a < b" ``` hoelzl@50419 ` 346` ``` then have "{a .. b} = {} \ {a .. b} = {a .. a}" by simp ``` hoelzl@50419 ` 347` ``` with uniform_distributed_params[OF D] show False ``` hoelzl@50419 ` 348` ``` by (auto simp: measure_def) ``` hoelzl@50419 ` 349` ```qed ``` hoelzl@50419 ` 350` hoelzl@50419 ` 351` ```lemma (in prob_space) uniform_distributed_iff: ``` hoelzl@50419 ` 352` ``` fixes a b :: real ``` hoelzl@50419 ` 353` ``` shows "distributed M lborel X (\x. indicator {a..b} x / measure lborel {a..b}) \ ``` hoelzl@50419 ` 354` ``` (X \ borel_measurable M \ a < b \ (\t\{a .. b}. \

(x in M. X x \ t)= (t - a) / (b - a)))" ``` hoelzl@50419 ` 355` ``` using ``` hoelzl@50419 ` 356` ``` uniform_distributed_bounds[of X a b] ``` hoelzl@50419 ` 357` ``` uniform_distributed_measure[of X a b] ``` hoelzl@50419 ` 358` ``` distributed_measurable[of M lborel X] ``` hoelzl@50419 ` 359` ``` by (auto intro!: uniform_distrI_borel_atLeastAtMost simp: one_ereal_def emeasure_eq_measure) ``` hoelzl@50419 ` 360` hoelzl@50419 ` 361` ```lemma (in prob_space) uniform_distributed_expectation: ``` hoelzl@50419 ` 362` ``` fixes a b :: real ``` hoelzl@50419 ` 363` ``` assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" ``` hoelzl@50419 ` 364` ``` shows "expectation X = (a + b) / 2" ``` hoelzl@50419 ` 365` ```proof (subst distributed_integral[OF D, of "\x. x", symmetric]) ``` hoelzl@50419 ` 366` ``` have "a < b" ``` hoelzl@50419 ` 367` ``` using uniform_distributed_bounds[OF D] . ``` hoelzl@50419 ` 368` hoelzl@50419 ` 369` ``` have "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = ``` hoelzl@50419 ` 370` ``` (\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel)" ``` hoelzl@50419 ` 371` ``` by (intro integral_cong) auto ``` hoelzl@50419 ` 372` ``` also have "(\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel) = (a + b) / 2" ``` hoelzl@50419 ` 373` ``` proof (subst integral_FTC_atLeastAtMost) ``` hoelzl@50419 ` 374` ``` fix x ``` wenzelm@53077 ` 375` ``` show "DERIV (\x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" ``` hoelzl@50419 ` 376` ``` using uniform_distributed_params[OF D] ``` hoelzl@56381 ` 377` ``` by (auto intro!: derivative_eq_intros) ``` hoelzl@50419 ` 378` ``` show "isCont (\x. x / Sigma_Algebra.measure lborel {a..b}) x" ``` hoelzl@50419 ` 379` ``` using uniform_distributed_params[OF D] ``` hoelzl@50419 ` 380` ``` by (auto intro!: isCont_divide) ``` wenzelm@53015 ` 381` ``` have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = ``` hoelzl@50419 ` 382` ``` (b*b - a * a) / (2 * (b - a))" ``` hoelzl@50419 ` 383` ``` using `a < b` ``` hoelzl@50419 ` 384` ``` by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) ``` wenzelm@53015 ` 385` ``` show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" ``` hoelzl@50419 ` 386` ``` using `a < b` ``` hoelzl@50419 ` 387` ``` unfolding * square_diff_square_factored by (auto simp: field_simps) ``` hoelzl@50419 ` 388` ``` qed (insert `a < b`, simp) ``` hoelzl@50419 ` 389` ``` finally show "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = (a + b) / 2" . ``` hoelzl@50419 ` 390` ```qed auto ``` hoelzl@50419 ` 391` hoelzl@50419 ` 392` ```end ```