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

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

(x in M. a < X x ) = exp (- a * l)" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 103` ```proof - ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 104` ``` have "exp (- a * l) = 1 - \

(x in M. X x \ a)" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 105` ``` unfolding exponential_distributedD_le[OF D a] by simp ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 106` ``` also have "\ = prob (space M - {x \ space M. X x \ a })" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 107` ``` using distributed_measurable[OF D] ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 108` ``` by (subst prob_compl) auto ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 109` ``` also have "\ = \

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

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

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

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

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

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

(x in M. X x \ t)= (t - a) / (b - a)))" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 357` ``` using ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 358` ``` uniform_distributed_bounds[of X a b] ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 359` ``` uniform_distributed_measure[of X a b] ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 360` ``` distributed_measurable[of M lborel X] ``` 56993 e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces hoelzl parents: 56571 diff changeset ` 361` ``` by (auto intro!: uniform_distrI_borel_atLeastAtMost ``` e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces hoelzl parents: 56571 diff changeset ` 362` ``` simp: one_ereal_def emeasure_eq_measure ``` e5366291d6aa introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces hoelzl parents: 56571 diff changeset ` 363` ``` simp del: measure_lborel) ``` 50419 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 364` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 365` ```lemma (in prob_space) uniform_distributed_expectation: ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 366` ``` fixes a b :: real ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 367` ``` assumes D: "distributed M lborel X (\x. indicator {a .. b} x / measure lborel {a .. b})" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 368` ``` shows "expectation X = (a + b) / 2" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 369` ```proof (subst distributed_integral[OF D, of "\x. x", symmetric]) ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 370` ``` have "a < b" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 371` ``` using uniform_distributed_bounds[OF D] . ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 372` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 373` ``` have "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 374` ``` (\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel)" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 375` ``` by (intro integral_cong) auto ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 376` ``` also have "(\ x. (x / measure lborel {a .. b}) * indicator {a .. b} x \lborel) = (a + b) / 2" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 377` ``` proof (subst integral_FTC_atLeastAtMost) ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 378` ``` fix x ``` 53077 a1b3784f8129 more symbols; wenzelm parents: 53015 diff changeset ` 379` ``` show "DERIV (\x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}" ``` 50419 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 380` ``` using uniform_distributed_params[OF D] ``` 56381 0556204bc230 merged DERIV_intros, has_derivative_intros into derivative_intros hoelzl parents: 56371 diff changeset ` 381` ``` by (auto intro!: derivative_eq_intros) ``` 50419 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 382` ``` show "isCont (\x. x / Sigma_Algebra.measure lborel {a..b}) x" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 383` ``` using uniform_distributed_params[OF D] ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 384` ``` by (auto intro!: isCont_divide) ``` 53015 a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find; wenzelm parents: 50419 diff changeset ` 385` ``` have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = ``` 50419 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 386` ``` (b*b - a * a) / (2 * (b - a))" ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 387` ``` using `a < b` ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 388` ``` by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric]) ``` 53015 a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find; wenzelm parents: 50419 diff changeset ` 389` ``` show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2" ``` 50419 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 390` ``` using `a < b` ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 391` ``` unfolding * square_diff_square_factored by (auto simp: field_simps) ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 392` ``` qed (insert `a < b`, simp) ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 393` ``` finally show "(\ x. indicator {a .. b} x / measure lborel {a .. b} * x \lborel) = (a + b) / 2" . ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 394` ```qed auto ``` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 395` 3177d0374701 add exponential and uniform distributions hoelzl parents: diff changeset ` 396` ```end ```