properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
authorhoelzl
Thu Jun 12 15:47:36 2014 +0200 (2014-06-12)
changeset 57235b0b9a10e4bf4
parent 57234 596a499318ab
child 57236 2eb14982cd29
child 57247 8191ccf6a1bd
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
CONTRIBUTORS
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Convolution.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Probability_Measure.thy
     1.1 --- a/CONTRIBUTORS	Wed Jun 11 13:39:38 2014 +0200
     1.2 +++ b/CONTRIBUTORS	Thu Jun 12 15:47:36 2014 +0200
     1.3 @@ -6,10 +6,14 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +
     1.8  * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
     1.9    Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT,
    1.10    Waldmeister, etc.).
    1.11  
    1.12 +* June 2014: Sudeep Kanav, TUM, and Johannes Hölzl, TUM
    1.13 +  Various properties of Erlang and exponentially distributed random variables.
    1.14 +
    1.15  * May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM
    1.16    SML-based engines for MaSh.
    1.17  
     2.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Jun 11 13:39:38 2014 +0200
     2.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu Jun 12 15:47:36 2014 +0200
     2.3 @@ -557,6 +557,11 @@
     2.4    shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f (x, y) \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x, y) \<partial>M2) \<partial>M1)"
     2.5    unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] ..
     2.6  
     2.7 +lemma (in pair_sigma_finite) Fubini':
     2.8 +  assumes f: "split f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
     2.9 +  shows "(\<integral>\<^sup>+ y. (\<integral>\<^sup>+ x. f x y \<partial>M1) \<partial>M2) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f x y \<partial>M2) \<partial>M1)"
    2.10 +  using Fubini[OF f] by simp
    2.11 +
    2.12  subsection {* Products on counting spaces, densities and distributions *}
    2.13  
    2.14  lemma sigma_sets_pair_measure_generator_finite:
    2.15 @@ -737,4 +742,109 @@
    2.16      by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff)
    2.17  qed
    2.18  
    2.19 +subsection {* Product of Borel spaces *}
    2.20 +
    2.21 +lemma borel_Times:
    2.22 +  fixes A :: "'a::topological_space set" and B :: "'b::topological_space set"
    2.23 +  assumes A: "A \<in> sets borel" and B: "B \<in> sets borel"
    2.24 +  shows "A \<times> B \<in> sets borel"
    2.25 +proof -
    2.26 +  have "A \<times> B = (A\<times>UNIV) \<inter> (UNIV \<times> B)"
    2.27 +    by auto
    2.28 +  moreover
    2.29 +  { have "A \<in> sigma_sets UNIV {S. open S}" using A by (simp add: sets_borel)
    2.30 +    then have "A\<times>UNIV \<in> sets borel"
    2.31 +    proof (induct A)
    2.32 +      case (Basic S) then show ?case
    2.33 +        by (auto intro!: borel_open open_Times)
    2.34 +    next
    2.35 +      case (Compl A)
    2.36 +      moreover have *: "(UNIV - A) \<times> UNIV = UNIV - (A \<times> UNIV)"
    2.37 +        by auto
    2.38 +      ultimately show ?case
    2.39 +        unfolding * by auto
    2.40 +    next
    2.41 +      case (Union A)
    2.42 +      moreover have *: "(UNION UNIV A) \<times> UNIV = UNION UNIV (\<lambda>i. A i \<times> UNIV)"
    2.43 +        by auto
    2.44 +      ultimately show ?case
    2.45 +        unfolding * by auto
    2.46 +    qed simp }
    2.47 +  moreover
    2.48 +  { have "B \<in> sigma_sets UNIV {S. open S}" using B by (simp add: sets_borel)
    2.49 +    then have "UNIV\<times>B \<in> sets borel"
    2.50 +    proof (induct B)
    2.51 +      case (Basic S) then show ?case
    2.52 +        by (auto intro!: borel_open open_Times)
    2.53 +    next
    2.54 +      case (Compl B)
    2.55 +      moreover have *: "UNIV \<times> (UNIV - B) = UNIV - (UNIV \<times> B)"
    2.56 +        by auto
    2.57 +      ultimately show ?case
    2.58 +        unfolding * by auto
    2.59 +    next
    2.60 +      case (Union B)
    2.61 +      moreover have *: "UNIV \<times> (UNION UNIV B) = UNION UNIV (\<lambda>i. UNIV \<times> B i)"
    2.62 +        by auto
    2.63 +      ultimately show ?case
    2.64 +        unfolding * by auto
    2.65 +    qed simp }
    2.66 +  ultimately show ?thesis
    2.67 +    by auto
    2.68 +qed
    2.69 +
    2.70 +lemma borel_prod: "sets (borel \<Otimes>\<^sub>M borel) =
    2.71 +    (sets borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) set set)"
    2.72 +  (is "?l = ?r")
    2.73 +proof -
    2.74 +  obtain A :: "'a set set" where A: "countable A" "topological_basis A"
    2.75 +    by (metis ex_countable_basis)
    2.76 +  moreover obtain B :: "'b set set" where B: "countable B" "topological_basis B"
    2.77 +    by (metis ex_countable_basis)
    2.78 +  ultimately have AB: "countable ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
    2.79 +    by (auto intro!: topological_basis_prod)
    2.80 +  have "sets (borel \<Otimes>\<^sub>M borel) = sigma_sets UNIV {a \<times> b |a b. a \<in> sigma_sets UNIV A \<and> b \<in> sigma_sets UNIV B}"
    2.81 +    by (simp add: sets_pair_measure
    2.82 +       borel_eq_countable_basis[OF A] borel_eq_countable_basis[OF B])
    2.83 +  also have "\<dots> \<supseteq> sigma_sets UNIV ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" (is "... \<supseteq> ?A")
    2.84 +    by (auto intro!: sigma_sets_mono)
    2.85 +  also (xtrans) have "?A = sets borel"
    2.86 +    by (simp add: borel_eq_countable_basis[OF AB])
    2.87 +  finally have "?r \<subseteq> ?l" .
    2.88 +  moreover have "?l \<subseteq> ?r"
    2.89 +  proof (simp add: sets_pair_measure, safe intro!: sigma_sets_mono)
    2.90 +    fix A::"('a \<times> 'b) set" assume "A \<in> sigma_sets UNIV {a \<times> b |a b. a \<in> sets borel \<and> b \<in> sets borel}"
    2.91 +    then show "A \<in> sets borel"
    2.92 +      by (induct A) (auto intro!: borel_Times)
    2.93 +  qed
    2.94 +  ultimately show ?thesis by auto
    2.95 +qed
    2.96 +
    2.97 +lemma borel_prod':
    2.98 +  "borel \<Otimes>\<^sub>M borel = (borel :: 
    2.99 +      ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
   2.100 +proof (rule measure_eqI[OF borel_prod])
   2.101 +  interpret sigma_finite_measure "borel :: 'b measure"
   2.102 +      by (default) (auto simp: borel_def emeasure_sigma intro!: exI[of _ "\<lambda>_. UNIV"])
   2.103 +  fix X :: "('a \<times> 'b) set" assume asm: "X \<in> sets (borel \<Otimes>\<^sub>M borel)"
   2.104 +  have "UNIV \<times> UNIV \<in> sets (borel \<Otimes>\<^sub>M borel :: ('a \<times> 'b) measure)" 
   2.105 +      by (simp add: borel_prod)
   2.106 +  moreover have "emeasure (borel \<Otimes>\<^sub>M borel) (UNIV \<times> UNIV :: ('a \<times> 'b) set) = 0"
   2.107 +      by (subst emeasure_pair_measure_Times, simp_all add: borel_def emeasure_sigma)
   2.108 +  moreover have "X \<subseteq> UNIV \<times> UNIV" by auto
   2.109 +  ultimately have "emeasure (borel \<Otimes>\<^sub>M borel) X = 0" by (rule emeasure_eq_0)
   2.110 +  thus "emeasure (borel \<Otimes>\<^sub>M borel) X = emeasure borel X"
   2.111 +      by (simp add: borel_def emeasure_sigma)
   2.112 +qed
   2.113 +
   2.114 +lemma finite_measure_pair_measure:
   2.115 +  assumes "finite_measure M" "finite_measure N"
   2.116 +  shows "finite_measure (N  \<Otimes>\<^sub>M M)"
   2.117 +proof (rule finite_measureI)
   2.118 +  interpret M: finite_measure M by fact
   2.119 +  interpret N: finite_measure N by fact
   2.120 +  show "emeasure (N  \<Otimes>\<^sub>M M) (space (N  \<Otimes>\<^sub>M M)) \<noteq> \<infinity>"
   2.121 +    by (auto simp: space_pair_measure M.emeasure_pair_measure_Times)
   2.122 +qed
   2.123 +
   2.124  end
   2.125 \ No newline at end of file
     3.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Wed Jun 11 13:39:38 2014 +0200
     3.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Jun 12 15:47:36 2014 +0200
     3.3 @@ -1518,9 +1518,37 @@
     3.4    using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
     3.5    using integral_norm_bound_ereal[of M f] by simp
     3.6    
     3.7 +lemma integrableI_nn_integral_finite:
     3.8 +  assumes [measurable]: "f \<in> borel_measurable M"
     3.9 +    and nonneg: "AE x in M. 0 \<le> f x"
    3.10 +    and finite: "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
    3.11 +  shows "integrable M f"
    3.12 +proof (rule integrableI_bounded)
    3.13 +  have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
    3.14 +    using nonneg by (intro nn_integral_cong_AE) auto
    3.15 +  with finite show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
    3.16 +    by auto
    3.17 +qed simp
    3.18 +
    3.19  lemma integral_eq_nn_integral:
    3.20 -  "integrable M f \<Longrightarrow> (\<And>x. 0 \<le> f x) \<Longrightarrow> integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
    3.21 -  by (subst nn_integral_eq_integral) auto
    3.22 +  assumes [measurable]: "f \<in> borel_measurable M"
    3.23 +  assumes nonneg: "AE x in M. 0 \<le> f x"
    3.24 +  shows "integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
    3.25 +proof cases
    3.26 +  assume *: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) = \<infinity>"
    3.27 +  also have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) = (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
    3.28 +    using nonneg by (intro nn_integral_cong_AE) auto
    3.29 +  finally have "\<not> integrable M f"
    3.30 +    by (auto simp: integrable_iff_bounded)
    3.31 +  then show ?thesis
    3.32 +    by (simp add: * not_integrable_integral_eq)
    3.33 +next
    3.34 +  assume "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
    3.35 +  then have "integrable M f"
    3.36 +    by (cases "\<integral>\<^sup>+ x. ereal (f x) \<partial>M") (auto intro!: integrableI_nn_integral_finite assms)
    3.37 +  from nn_integral_eq_integral[OF this nonneg] show ?thesis
    3.38 +    by simp
    3.39 +qed
    3.40    
    3.41  lemma integrableI_simple_bochner_integrable:
    3.42    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    3.43 @@ -1933,7 +1961,7 @@
    3.44  subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
    3.45  
    3.46  lemma real_lebesgue_integral_def:
    3.47 -  assumes f: "integrable M f"
    3.48 +  assumes f[measurable]: "integrable M f"
    3.49    shows "integral\<^sup>L M f = real (\<integral>\<^sup>+x. f x \<partial>M) - real (\<integral>\<^sup>+x. - f x \<partial>M)"
    3.50  proof -
    3.51    have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"
    3.52 @@ -1941,9 +1969,9 @@
    3.53    also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
    3.54      by (intro integral_diff integrable_max integrable_minus integrable_zero f)
    3.55    also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
    3.56 -    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
    3.57 +    by (subst integral_eq_nn_integral[symmetric]) auto
    3.58    also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
    3.59 -    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
    3.60 +    by (subst integral_eq_nn_integral[symmetric]) auto
    3.61    also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
    3.62      by (auto simp: max_def)
    3.63    also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
     4.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Jun 11 13:39:38 2014 +0200
     4.2 +++ b/src/HOL/Probability/Borel_Space.thy	Thu Jun 12 15:47:36 2014 +0200
     4.3 @@ -35,6 +35,9 @@
     4.4  lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
     4.5    unfolding borel_def by auto
     4.6  
     4.7 +lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}"
     4.8 +  unfolding borel_def by (rule sets_measure_of) simp
     4.9 +
    4.10  lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
    4.11    unfolding borel_def pred_def by auto
    4.12  
    4.13 @@ -801,6 +804,20 @@
    4.14    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
    4.15    by (simp add: min_def)
    4.16  
    4.17 +lemma borel_measurable_Min[measurable (raw)]:
    4.18 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Min ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
    4.19 +proof (induct I rule: finite_induct)
    4.20 +  case (insert i I) then show ?case
    4.21 +    by (cases "I = {}") auto
    4.22 +qed auto
    4.23 +
    4.24 +lemma borel_measurable_Max[measurable (raw)]:
    4.25 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. Max ((\<lambda>i. f i x)`I) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
    4.26 +proof (induct I rule: finite_induct)
    4.27 +  case (insert i I) then show ?case
    4.28 +    by (cases "I = {}") auto
    4.29 +qed auto
    4.30 +
    4.31  lemma borel_measurable_abs[measurable (raw)]:
    4.32    "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
    4.33    unfolding abs_real_def by simp
    4.34 @@ -874,6 +891,36 @@
    4.35    "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
    4.36    by simp
    4.37  
    4.38 +lemma borel_measurable_root [measurable]: "(root n) \<in> borel_measurable borel"
    4.39 +  by (intro borel_measurable_continuous_on1 continuous_intros)
    4.40 +
    4.41 +lemma borel_measurable_sqrt [measurable]: "sqrt \<in> borel_measurable borel"
    4.42 +  by (intro borel_measurable_continuous_on1 continuous_intros)
    4.43 +
    4.44 +lemma borel_measurable_power [measurable (raw)]:
    4.45 +   fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
    4.46 +   assumes f: "f \<in> borel_measurable M"
    4.47 +   shows "(\<lambda>x. (f x) ^ n) \<in> borel_measurable M"
    4.48 +   by (intro borel_measurable_continuous_on [OF _ f] continuous_intros)
    4.49 +
    4.50 +lemma borel_measurable_Re [measurable]: "Re \<in> borel_measurable borel"
    4.51 +  by (intro borel_measurable_continuous_on1 continuous_intros)
    4.52 +
    4.53 +lemma borel_measurable_Im [measurable]: "Im \<in> borel_measurable borel"
    4.54 +  by (intro borel_measurable_continuous_on1 continuous_intros)
    4.55 +
    4.56 +lemma borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel"
    4.57 +  by (intro borel_measurable_continuous_on1 continuous_intros)
    4.58 +
    4.59 +lemma borel_measurable_sin [measurable]: "sin \<in> borel_measurable borel"
    4.60 +  by (intro borel_measurable_continuous_on1 continuous_intros)
    4.61 +
    4.62 +lemma borel_measurable_cos [measurable]: "cos \<in> borel_measurable borel"
    4.63 +  by (intro borel_measurable_continuous_on1 continuous_intros)
    4.64 +
    4.65 +lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
    4.66 +  by (intro borel_measurable_continuous_on1 continuous_intros)
    4.67 +
    4.68  subsection "Borel space on the extended reals"
    4.69  
    4.70  lemma borel_measurable_ereal[measurable (raw)]:
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Probability/Convolution.thy	Thu Jun 12 15:47:36 2014 +0200
     5.3 @@ -0,0 +1,241 @@
     5.4 +(*  Title:      HOL/Probability/Convolution.thy
     5.5 +    Author:     Sudeep Kanav, TU München
     5.6 +    Author:     Johannes Hölzl, TU München *)
     5.7 +
     5.8 +header {* Convolution Measure *}
     5.9 +
    5.10 +theory Convolution
    5.11 +  imports Independent_Family
    5.12 +begin
    5.13 +
    5.14 +lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M"
    5.15 +  ..
    5.16 +
    5.17 +definition convolution :: "('a :: ordered_euclidean_space) measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" (infix "\<star>" 50) where
    5.18 +  "convolution M N = distr (M \<Otimes>\<^sub>M N) borel (\<lambda>(x, y). x + y)"
    5.19 +
    5.20 +lemma
    5.21 +  shows space_convolution[simp]: "space (convolution M N) = space borel"
    5.22 +    and sets_convolution[simp]: "sets (convolution M N) = sets borel"
    5.23 +    and measurable_convolution1[simp]: "measurable A (convolution M N) = measurable A borel"
    5.24 +    and measurable_convolution2[simp]: "measurable (convolution M N) B = measurable borel B"
    5.25 +  by (simp_all add: convolution_def)
    5.26 +
    5.27 +lemma nn_integral_convolution:
    5.28 +  assumes "finite_measure M" "finite_measure N"
    5.29 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
    5.30 +  assumes [measurable]: "f \<in> borel_measurable borel"
    5.31 +  shows "(\<integral>\<^sup>+x. f x \<partial>convolution M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f (x + y) \<partial>N \<partial>M)"
    5.32 +proof -
    5.33 +  interpret M: finite_measure M by fact
    5.34 +  interpret N: finite_measure N by fact
    5.35 +  interpret pair_sigma_finite M N ..
    5.36 +  show ?thesis
    5.37 +    unfolding convolution_def
    5.38 +    by (simp add: nn_integral_distr N.nn_integral_fst[symmetric])
    5.39 +qed
    5.40 +
    5.41 +lemma convolution_emeasure:
    5.42 +  assumes "A \<in> sets borel" "finite_measure M" "finite_measure N"
    5.43 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
    5.44 +  assumes [simp]: "space M = space N" "space N = space borel"
    5.45 +  shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. (emeasure N {a. a + x \<in> A}) \<partial>M "
    5.46 +  using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution 
    5.47 +    nn_integral_indicator[symmetric] ab_semigroup_add_class.add_ac split:split_indicator)
    5.48 +
    5.49 +lemma convolution_emeasure':
    5.50 +  assumes [simp]:"A \<in> sets borel"
    5.51 +  assumes [simp]: "finite_measure M" "finite_measure N"
    5.52 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
    5.53 +  shows  "emeasure (M \<star> N) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y.  (indicator  A (x + y)) \<partial>N  \<partial>M"
    5.54 +  by (auto simp del: nn_integral_indicator simp: nn_integral_convolution
    5.55 +    nn_integral_indicator[symmetric] borel_measurable_indicator)
    5.56 +
    5.57 +lemma convolution_finite:
    5.58 +  assumes [simp]: "finite_measure M" "finite_measure N"
    5.59 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
    5.60 +  shows "finite_measure (M \<star> N)"
    5.61 +  unfolding convolution_def
    5.62 +  by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto
    5.63 +
    5.64 +lemma convolution_emeasure_3:
    5.65 +  assumes [simp, measurable]: "A \<in> sets borel"
    5.66 +  assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L"
    5.67 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
    5.68 +  shows "emeasure (L \<star> (M \<star> N )) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. \<integral>\<^sup>+z. indicator A (x + y + z) \<partial>N \<partial>M \<partial>L"
    5.69 +  apply (subst nn_integral_indicator[symmetric], simp)
    5.70 +  apply (subst nn_integral_convolution, 
    5.71 +        auto intro!: borel_measurable_indicator borel_measurable_indicator' convolution_finite)+
    5.72 +  by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add_assoc)
    5.73 +
    5.74 +lemma convolution_emeasure_3':
    5.75 +  assumes [simp, measurable]:"A \<in> sets borel"
    5.76 +  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
    5.77 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
    5.78 +  shows "emeasure ((L \<star> M) \<star> N ) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. \<integral>\<^sup>+z. indicator A (x + y + z) \<partial>N \<partial>M \<partial>L"
    5.79 +  apply (subst nn_integral_indicator[symmetric], simp)+
    5.80 +  apply (subst nn_integral_convolution)
    5.81 +  apply (simp_all add: convolution_finite)
    5.82 +  apply (subst nn_integral_convolution)
    5.83 +  apply (simp_all add: finite_measure.sigma_finite_measure sigma_finite_measure.borel_measurable_nn_integral)
    5.84 +  done
    5.85 +
    5.86 +lemma convolution_commutative:
    5.87 +  assumes [simp]: "finite_measure M" "finite_measure N"
    5.88 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
    5.89 +  shows "(M \<star> N) = (N \<star> M)"
    5.90 +proof (rule measure_eqI)  
    5.91 +  interpret M: finite_measure M by fact
    5.92 +  interpret N: finite_measure N by fact
    5.93 +  interpret pair_sigma_finite M N ..
    5.94 +
    5.95 +  show "sets (M \<star> N) = sets (N \<star> M)" by simp
    5.96 +
    5.97 +  fix A assume "A \<in> sets (M \<star> N)"
    5.98 +  then have 1[measurable]:"A \<in> sets borel" by simp
    5.99 +  have "emeasure (M \<star> N) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator A (x + y) \<partial>N \<partial>M" by (auto intro!: convolution_emeasure')
   5.100 +  also have "... = \<integral>\<^sup>+x. \<integral>\<^sup>+y. (\<lambda>(x,y). indicator A (x + y)) (x, y) \<partial>N \<partial>M" by (auto intro!: nn_integral_cong)
   5.101 +  also have "... = \<integral>\<^sup>+y. \<integral>\<^sup>+x. (\<lambda>(x,y). indicator A (x + y)) (x, y) \<partial>M \<partial>N" by (rule Fubini[symmetric]) simp
   5.102 +  also have "... = emeasure (N \<star> M) A" by (auto intro!: nn_integral_cong simp: add_commute convolution_emeasure')
   5.103 +  finally show "emeasure (M \<star> N) A = emeasure (N \<star> M) A" by simp
   5.104 +qed
   5.105 +
   5.106 +lemma convolution_associative:
   5.107 +  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
   5.108 +  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
   5.109 +  shows "(L \<star> (M \<star> N)) = ((L \<star> M) \<star> N)"
   5.110 +  by (auto intro!: measure_eqI simp: convolution_emeasure_3 convolution_emeasure_3')
   5.111 +
   5.112 +lemma (in prob_space) sum_indep_random_variable:
   5.113 +  assumes ind: "indep_var borel X borel Y"
   5.114 +  assumes [simp, measurable]: "random_variable borel X"
   5.115 +  assumes [simp, measurable]: "random_variable borel Y"
   5.116 +  shows "distr M borel (\<lambda>x. X x + Y x) = convolution (distr M borel X)  (distr M borel Y)"
   5.117 +  using ind unfolding indep_var_distribution_eq convolution_def
   5.118 +  by (auto simp: distr_distr intro!:arg_cong[where f = "distr M borel"])
   5.119 +
   5.120 +lemma (in prob_space) sum_indep_random_variable_lborel:
   5.121 +  assumes ind: "indep_var borel X borel Y"
   5.122 +  assumes [simp, measurable]: "random_variable lborel X"
   5.123 +  assumes [simp, measurable]:"random_variable lborel Y" 
   5.124 +  shows "distr M lborel (\<lambda>x. X x + Y x) = convolution (distr M lborel X)  (distr M lborel Y)"
   5.125 +  using ind unfolding indep_var_distribution_eq convolution_def 
   5.126 +  by (auto simp: distr_distr o_def intro!: arg_cong[where f = "distr M borel"] cong: distr_cong)
   5.127 +
   5.128 +lemma convolution_density:
   5.129 +  fixes f g :: "real \<Rightarrow> ereal"
   5.130 +  assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
   5.131 +  assumes [simp]:"finite_measure (density lborel f)" "finite_measure (density lborel g)"
   5.132 +  assumes gt_0[simp]: "AE x in lborel. 0 \<le> f x" "AE x in lborel. 0 \<le> g x"
   5.133 +  shows "density lborel f \<star> density lborel g = density lborel (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)"
   5.134 +    (is "?l = ?r")
   5.135 +proof (intro measure_eqI)
   5.136 +  fix A assume "A \<in> sets ?l"
   5.137 +  then have [measurable]: "A \<in> sets borel"
   5.138 +    by simp
   5.139 +
   5.140 +  have "(\<integral>\<^sup>+x. f x * (\<integral>\<^sup>+y. g y * indicator A (x + y) \<partial>lborel) \<partial>lborel) =
   5.141 +    (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
   5.142 +    using gt_0
   5.143 +  proof (intro nn_integral_cong_AE, eventually_elim)
   5.144 +    fix x assume "0 \<le> f x"
   5.145 +    then have "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) =
   5.146 +      (\<integral>\<^sup>+ y. f x * (g y * indicator A (x + y)) \<partial>lborel)"
   5.147 +      by (intro nn_integral_cmult[symmetric]) auto
   5.148 +    then show "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) =
   5.149 +      (\<integral>\<^sup>+ y. g y * (f x * indicator A (x + y)) \<partial>lborel)"
   5.150 +      by (simp add: ac_simps)
   5.151 +  qed
   5.152 +  also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
   5.153 +    by (intro lborel_pair.Fubini') simp
   5.154 +  also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)"
   5.155 +    using gt_0
   5.156 +  proof (intro nn_integral_cong_AE, eventually_elim)
   5.157 +    fix y assume "0 \<le> g y"
   5.158 +    then have "(\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
   5.159 +      g y * (\<integral>\<^sup>+x. f x * indicator A (x + y) \<partial>lborel)"
   5.160 +      by (intro nn_integral_cmult) auto
   5.161 +    also have "\<dots> = g y * (\<integral>\<^sup>+x. f (x - y) * indicator A x \<partial>lborel)"
   5.162 +      using gt_0
   5.163 +      by (subst nn_integral_real_affine[where c=1 and t="-y"])
   5.164 +         (auto simp del: gt_0 simp add: one_ereal_def[symmetric])
   5.165 +    also have "\<dots> = (\<integral>\<^sup>+x. g y * (f (x - y) * indicator A x) \<partial>lborel)"
   5.166 +      using `0 \<le> g y` by (intro nn_integral_cmult[symmetric]) auto
   5.167 +    finally show "(\<integral>\<^sup>+ x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
   5.168 +      (\<integral>\<^sup>+ x. f (x - y) * g y * indicator A x \<partial>lborel)"
   5.169 +      by (simp add: ac_simps)
   5.170 +  qed
   5.171 +  also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)"
   5.172 +    by (intro lborel_pair.Fubini') simp
   5.173 +  finally show "emeasure ?l A = emeasure ?r A"
   5.174 +    by (auto simp: convolution_emeasure' nn_integral_density emeasure_density
   5.175 +      nn_integral_multc)
   5.176 +qed simp
   5.177 +
   5.178 +lemma (in prob_space) distributed_finite_measure_density:
   5.179 +  "distributed M N X f \<Longrightarrow> finite_measure (density N f)"
   5.180 +  using finite_measure_distr[of X N] distributed_distr_eq_density[of M N X f] by simp
   5.181 +  
   5.182 +
   5.183 +lemma (in prob_space) distributed_convolution:
   5.184 +  fixes f :: "real \<Rightarrow> _"
   5.185 +  fixes g :: "real \<Rightarrow> _"
   5.186 +  assumes indep: "indep_var borel X borel Y"
   5.187 +  assumes X: "distributed M lborel X f"
   5.188 +  assumes Y: "distributed M lborel Y g"
   5.189 +  shows "distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)"
   5.190 +  unfolding distributed_def
   5.191 +proof safe
   5.192 +  show "AE x in lborel. 0 \<le> \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel"
   5.193 +    by (auto simp: nn_integral_nonneg)
   5.194 +
   5.195 +  have fg[measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
   5.196 +    using distributed_borel_measurable[OF X] distributed_borel_measurable[OF Y] by simp_all
   5.197 +  
   5.198 +  show "(\<lambda>x. \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel) \<in> borel_measurable lborel" 
   5.199 +    by measurable
   5.200 +
   5.201 +  have "distr M borel (\<lambda>x. X x + Y x) = (distr M borel X \<star> distr M borel Y)"
   5.202 +    using distributed_measurable[OF X] distributed_measurable[OF Y]
   5.203 +    by (intro sum_indep_random_variable) (auto simp: indep)
   5.204 +  also have "\<dots> = (density lborel f \<star> density lborel g)"
   5.205 +    using distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
   5.206 +    by (simp cong: distr_cong)
   5.207 +  also have "\<dots> = density lborel (\<lambda>x. \<integral>\<^sup>+ y. f (x - y) * g y \<partial>lborel)"
   5.208 +  proof (rule convolution_density)
   5.209 +    show "finite_measure (density lborel f)"
   5.210 +      using X by (rule distributed_finite_measure_density)
   5.211 +    show "finite_measure (density lborel g)"
   5.212 +      using Y by (rule distributed_finite_measure_density)
   5.213 +    show "AE x in lborel. 0 \<le> f x"
   5.214 +      using X by (rule distributed_AE)
   5.215 +    show "AE x in lborel. 0 \<le> g x"
   5.216 +      using Y by (rule distributed_AE)
   5.217 +  qed fact+
   5.218 +  finally show "distr M lborel (\<lambda>x. X x + Y x) = density lborel (\<lambda>x. \<integral>\<^sup>+ y. f (x - y) * g y \<partial>lborel)"
   5.219 +    by (simp cong: distr_cong)
   5.220 +  show "random_variable lborel (\<lambda>x. X x + Y x)"
   5.221 +    using distributed_measurable[OF X] distributed_measurable[OF Y] by simp
   5.222 +qed
   5.223 +
   5.224 +lemma prob_space_convolution_density:
   5.225 +  fixes f:: "real \<Rightarrow> _"
   5.226 +  fixes g:: "real \<Rightarrow> _"
   5.227 +  assumes [measurable]: "f\<in> borel_measurable borel"
   5.228 +  assumes [measurable]: "g\<in> borel_measurable borel"
   5.229 +  assumes gt_0[simp]: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x"
   5.230 +  assumes "prob_space (density lborel f)" (is "prob_space ?F")
   5.231 +  assumes "prob_space (density lborel g)" (is "prob_space ?G")
   5.232 +  shows "prob_space (density lborel (\<lambda>x.\<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel))" (is "prob_space ?D")
   5.233 +proof (subst convolution_density[symmetric])
   5.234 +  interpret F: prob_space ?F by fact
   5.235 +  show "finite_measure ?F" by unfold_locales
   5.236 +  interpret G: prob_space ?G by fact
   5.237 +  show "finite_measure ?G" by unfold_locales
   5.238 +  interpret FG: pair_prob_space ?F ?G ..
   5.239 +
   5.240 +  show "prob_space (density lborel f \<star> density lborel g)"
   5.241 +    unfolding convolution_def by (rule FG.prob_space_distr) simp
   5.242 +qed simp_all
   5.243 +
   5.244 +end
     6.1 --- a/src/HOL/Probability/Distributions.thy	Wed Jun 11 13:39:38 2014 +0200
     6.2 +++ b/src/HOL/Probability/Distributions.thy	Thu Jun 12 15:47:36 2014 +0200
     6.3 @@ -1,14 +1,313 @@
     6.4 +(*  Title:      HOL/Probability/Distributions.thy
     6.5 +    Author:     Sudeep Kanav, TU München
     6.6 +    Author:     Johannes Hölzl, TU München *)
     6.7 +
     6.8 +header {* Properties of Various Distributions *}
     6.9 +
    6.10  theory Distributions
    6.11 -  imports Probability_Measure
    6.12 +  imports Probability_Measure Convolution
    6.13  begin
    6.14  
    6.15 +lemma measure_lebesgue_Icc: "measure lebesgue {a .. b} = (if a \<le> b then b - a else 0)"
    6.16 +  by (auto simp: measure_def)
    6.17 +
    6.18 +lemma integral_power:
    6.19 +  "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
    6.20 +proof (subst integral_FTC_atLeastAtMost)
    6.21 +  fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
    6.22 +    by (intro derivative_eq_intros) auto
    6.23 +qed (auto simp: field_simps)
    6.24 +
    6.25 +lemma has_bochner_integral_nn_integral:
    6.26 +  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
    6.27 +  assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
    6.28 +  shows "has_bochner_integral M f x"
    6.29 +  unfolding has_bochner_integral_iff
    6.30 +proof
    6.31 +  show "integrable M f"
    6.32 +    using assms by (rule integrableI_nn_integral_finite)
    6.33 +qed (auto simp: assms integral_eq_nn_integral)
    6.34 +
    6.35 +lemma (in prob_space) distributed_AE2:
    6.36 +  assumes [measurable]: "distributed M N X f" "Measurable.pred N P"
    6.37 +  shows "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)"
    6.38 +proof -
    6.39 +  have "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in distr M N X. P x)"
    6.40 +    by (simp add: AE_distr_iff)
    6.41 +  also have "\<dots> \<longleftrightarrow> (AE x in density N f. P x)"
    6.42 +    unfolding distributed_distr_eq_density[OF assms(1)] ..
    6.43 +  also have "\<dots> \<longleftrightarrow>  (AE x in N. 0 < f x \<longrightarrow> P x)"
    6.44 +    by (rule AE_density) simp
    6.45 +  finally show ?thesis .
    6.46 +qed
    6.47 +
    6.48 +subsection {* Erlang *}
    6.49 +
    6.50 +lemma nn_intergal_power_times_exp_Icc:
    6.51 +  assumes [arith]: "0 \<le> a"
    6.52 +  shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x \<partial>lborel) =
    6.53 +    (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _")
    6.54 +proof -
    6.55 +  let ?f = "\<lambda>k x. x^k * exp (-x) / fact k"
    6.56 +  let ?F = "\<lambda>k x. - (\<Sum>n\<le>k. (x^n * exp (-x)) / fact n)"
    6.57 +
    6.58 +  have "?I * (inverse (fact k)) = 
    6.59 +      (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (fact k)) \<partial>lborel)"
    6.60 +    by (intro nn_integral_multc[symmetric]) auto
    6.61 +  also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)"
    6.62 +    by (intro nn_integral_cong) (simp add: field_simps)
    6.63 +  also have "\<dots> = ereal (?F k a) - (?F k 0)"
    6.64 +  proof (rule nn_integral_FTC_atLeastAtMost)
    6.65 +    fix x assume "x \<in> {0..a}"
    6.66 +    show "DERIV (?F k) x :> ?f k x"
    6.67 +    proof(induction k)
    6.68 +      case 0 show ?case by (auto intro!: derivative_eq_intros)
    6.69 +    next
    6.70 +      case (Suc k)
    6.71 +      have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :>
    6.72 +        ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k))"
    6.73 +        by (intro DERIV_diff Suc)
    6.74 +           (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc
    6.75 +                 simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric])
    6.76 +      also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)"
    6.77 +        by simp
    6.78 +      also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k)) = ?f (Suc k) x"
    6.79 +        by (auto simp: field_simps simp del: fact_Suc)
    6.80 +           (simp_all add: real_of_nat_Suc field_simps)
    6.81 +      finally show ?case .
    6.82 +    qed
    6.83 +  qed auto
    6.84 +  also have "\<dots> = ereal (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n))"
    6.85 +    by (auto simp: power_0_left if_distrib[where f="\<lambda>x. x / a" for a] setsum_cases)
    6.86 +  finally show ?thesis
    6.87 +    by (cases "?I") (auto simp: field_simps)
    6.88 +qed
    6.89 +
    6.90 +lemma nn_intergal_power_times_exp_Ici:
    6.91 +  shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = fact k"
    6.92 +proof (rule LIMSEQ_unique)
    6.93 +  let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel"
    6.94 +  show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
    6.95 +    apply (intro nn_integral_LIMSEQ)
    6.96 +    apply (auto simp: incseq_def le_fun_def eventually_sequentially
    6.97 +                split: split_indicator intro!: Lim_eventually)
    6.98 +    apply (metis natceiling_le_eq)
    6.99 +    done
   6.100 +
   6.101 +  have "((\<lambda>x. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / real (fact n))) * fact k) ---> (1 - (\<Sum>n\<le>k. 0 / real (fact n))) * fact k) at_top"
   6.102 +    by (intro tendsto_intros tendsto_power_div_exp_0) simp
   6.103 +  then show "?X ----> fact k"
   6.104 +    by (subst nn_intergal_power_times_exp_Icc)
   6.105 +       (auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially])
   6.106 +qed
   6.107 +
   6.108 +definition erlang_density :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
   6.109 +  "erlang_density k l x = (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k)"
   6.110 +
   6.111 +definition erlang_CDF ::  "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
   6.112 +  "erlang_CDF k l x = (if x < 0 then 0 else 1 - (\<Sum>n\<le>k. ((l * x)^n * exp (- l * x) / fact n)))"
   6.113 +
   6.114 +lemma erlang_density_nonneg: "0 \<le> l \<Longrightarrow> 0 \<le> erlang_density k l x"
   6.115 +  by (simp add: erlang_density_def)
   6.116 +
   6.117 +lemma borel_measurable_erlang_density[measurable]: "erlang_density k l \<in> borel_measurable borel"
   6.118 +  by (auto simp add: erlang_density_def[abs_def])
   6.119 +
   6.120 +lemma erlang_CDF_transform: "0 < l \<Longrightarrow> erlang_CDF k l a = erlang_CDF k 1 (l * a)"
   6.121 +  by (auto simp add: erlang_CDF_def mult_less_0_iff)
   6.122 +
   6.123 +lemma nn_integral_erlang_density:
   6.124 +  assumes [arith]: "0 < l"
   6.125 +  shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a"
   6.126 +proof cases
   6.127 +  assume [arith]: "0 \<le> a"
   6.128 +  have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x"
   6.129 +    by (simp add: field_simps split: split_indicator)
   6.130 +  have "(\<integral>\<^sup>+x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) =
   6.131 +    (\<integral>\<^sup>+x. (l/fact k) * (ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x) \<partial>lborel)"
   6.132 +    by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib split: split_indicator)
   6.133 +  also have "\<dots> = (l/fact k) * (\<integral>\<^sup>+x. ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x \<partial>lborel)"
   6.134 +    by (intro nn_integral_cmult) auto
   6.135 +  also have "\<dots> = ereal (l/fact k) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^k * exp (- x)) * indicator {0 .. l * a} x \<partial>lborel))"
   6.136 +    by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq)
   6.137 +  also have "\<dots> = (1 - (\<Sum>n\<le>k. ((l * a)^n * exp (-(l * a))) / fact n))"
   6.138 +    by (subst nn_intergal_power_times_exp_Icc) auto
   6.139 +  also have "\<dots> = erlang_CDF k l a"
   6.140 +    by (auto simp: erlang_CDF_def)
   6.141 +  finally show ?thesis .
   6.142 +next
   6.143 +  assume "\<not> 0 \<le> a" 
   6.144 +  moreover then have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))"
   6.145 +    by (intro nn_integral_cong) (auto simp: erlang_density_def)
   6.146 +  ultimately show ?thesis
   6.147 +    by (simp add: erlang_CDF_def)
   6.148 +qed
   6.149 +
   6.150 +lemma emeasure_erlang_density: 
   6.151 +  "0 < l \<Longrightarrow> emeasure (density lborel (erlang_density k l)) {.. a} = erlang_CDF k l a"
   6.152 +  by (simp add: emeasure_density nn_integral_erlang_density)
   6.153 +
   6.154 +lemma nn_integral_erlang_ith_moment: 
   6.155 +  fixes k i :: nat and l :: real
   6.156 +  assumes [arith]: "0 < l" 
   6.157 +  shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x ^ i) \<partial>lborel) = fact (k + i) / (fact k * l ^ i)"
   6.158 +proof -
   6.159 +  have eq: "\<And>x. indicator {0..} (x / l) = indicator {0..} x"
   6.160 +    by (simp add: field_simps split: split_indicator)
   6.161 +  have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x^i) \<partial>lborel) =
   6.162 +    (\<integral>\<^sup>+x. (l/(fact k * l^i)) * (ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x) \<partial>lborel)"
   6.163 +    by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib power_add split: split_indicator)
   6.164 +  also have "\<dots> = (l/(fact k * l^i)) * (\<integral>\<^sup>+x. ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x \<partial>lborel)"
   6.165 +    by (intro nn_integral_cmult) auto
   6.166 +  also have "\<dots> = ereal (l/(fact k * l^i)) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^(k+i) * exp (- x)) * indicator {0 ..} x \<partial>lborel))"
   6.167 +    by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq)
   6.168 +  also have "\<dots> = fact (k + i) / (fact k * l ^ i)"
   6.169 +    by (subst nn_intergal_power_times_exp_Ici) auto
   6.170 +  finally show ?thesis .
   6.171 +qed
   6.172 +
   6.173 +lemma prob_space_erlang_density:
   6.174 +  assumes l[arith]: "0 < l"
   6.175 +  shows "prob_space (density lborel (erlang_density k l))" (is "prob_space ?D")
   6.176 +proof
   6.177 +  show "emeasure ?D (space ?D) = 1"
   6.178 +    using nn_integral_erlang_ith_moment[OF l, where k=k and i=0] by (simp add: emeasure_density)
   6.179 +qed
   6.180 +
   6.181 +lemma (in prob_space) erlang_distributed_le:
   6.182 +  assumes D: "distributed M lborel X (erlang_density k l)"
   6.183 +  assumes [simp, arith]: "0 < l" "0 \<le> a"
   6.184 +  shows "\<P>(x in M. X x \<le> a) = erlang_CDF k l a"
   6.185 +proof -
   6.186 +  have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}"
   6.187 +    using distributed_measurable[OF D]
   6.188 +    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
   6.189 +  also have "\<dots> = emeasure (density lborel (erlang_density k l)) {.. a}"
   6.190 +    unfolding distributed_distr_eq_density[OF D] ..
   6.191 +  also have "\<dots> = erlang_CDF k l a"
   6.192 +    by (auto intro!: emeasure_erlang_density)
   6.193 +  finally show ?thesis
   6.194 +    by (auto simp: measure_def)
   6.195 +qed
   6.196 +
   6.197 +lemma (in prob_space) erlang_distributed_gt:
   6.198 +  assumes D[simp]: "distributed M lborel X (erlang_density k l)"
   6.199 +  assumes [arith]: "0 < l" "0 \<le> a"
   6.200 +  shows "\<P>(x in M. a < X x ) = 1 - (erlang_CDF k l a)"
   6.201 +proof -
   6.202 +  have " 1 - (erlang_CDF k l a) = 1 - \<P>(x in M. X x \<le> a)" by (subst erlang_distributed_le) auto
   6.203 +  also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })"
   6.204 +    using distributed_measurable[OF D] by (auto simp: prob_compl)
   6.205 +  also have "\<dots> = \<P>(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le)
   6.206 +  finally show ?thesis by simp
   6.207 +qed
   6.208 +
   6.209 +lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0"
   6.210 +  by (induction k) (auto simp: erlang_CDF_def)
   6.211 +
   6.212 +lemma erlang_distributedI:
   6.213 +  assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
   6.214 +    and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = erlang_CDF k l a"
   6.215 +  shows "distributed M lborel X (erlang_density k l)"
   6.216 +proof (rule distributedI_borel_atMost)
   6.217 +  fix a :: real
   6.218 +  { assume "a \<le> 0"  
   6.219 +    with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}"
   6.220 +      by (intro emeasure_mono) auto
   6.221 +    also have "... = 0"  by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0])
   6.222 +    finally have "emeasure M {x\<in>space M. X x \<le> a} \<le> 0" by simp
   6.223 +    then have "emeasure M {x\<in>space M. X x \<le> a} = 0" by (simp add:emeasure_le_0_iff)
   6.224 +  }
   6.225 +  note eq_0 = this
   6.226 +
   6.227 +  show "(\<integral>\<^sup>+ x. erlang_density k l x * indicator {..a} x \<partial>lborel) = ereal (erlang_CDF k l a)"
   6.228 +    using nn_integral_erlang_density[of l k a]
   6.229 +    by (simp add: times_ereal.simps(1)[symmetric] ereal_indicator del: times_ereal.simps)
   6.230 +
   6.231 +  show "emeasure M {x\<in>space M. X x \<le> a} = ereal (erlang_CDF k l a)"
   6.232 +    using X_distr[of a] eq_0 by (auto simp: one_ereal_def erlang_CDF_def)
   6.233 +qed (simp_all add: erlang_density_nonneg)
   6.234 +
   6.235 +lemma (in prob_space) erlang_distributed_iff:
   6.236 +  assumes [arith]: "0<l"
   6.237 +  shows "distributed M lborel X (erlang_density k l) \<longleftrightarrow>
   6.238 +    (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 ))"
   6.239 +  using
   6.240 +    distributed_measurable[of M lborel X "erlang_density k l"]
   6.241 +    emeasure_erlang_density[of l]
   6.242 +    erlang_distributed_le[of X k l]
   6.243 +  by (auto intro!: erlang_distributedI simp: one_ereal_def emeasure_eq_measure) 
   6.244 +
   6.245 +lemma (in prob_space) erlang_distributed_mult_const:
   6.246 +  assumes erlX: "distributed M lborel X (erlang_density k l)"
   6.247 +  assumes a_pos[arith]: "0 < \<alpha>"  "0 < l"
   6.248 +  shows  "distributed M lborel (\<lambda>x. \<alpha> * X x) (erlang_density k (l / \<alpha>))"
   6.249 +proof (subst erlang_distributed_iff, safe)
   6.250 +  have [measurable]: "random_variable borel X"  and  [arith]: "0 < l " 
   6.251 +  and  [simp]: "\<And>a. 0 \<le> a \<Longrightarrow> prob {x \<in> space M. X x \<le> a} = erlang_CDF k l a"
   6.252 +    by(insert erlX, auto simp: erlang_distributed_iff)
   6.253 +
   6.254 +  show "random_variable borel (\<lambda>x. \<alpha> * X x)" "0 < l / \<alpha>"  "0 < l / \<alpha>" 
   6.255 +    by (auto simp:field_simps)
   6.256 +  
   6.257 +  fix a:: real assume [arith]: "0 \<le> a"
   6.258 +  obtain b:: real  where [simp, arith]: "b = a/ \<alpha>" by blast 
   6.259 +
   6.260 +  have [arith]: "0 \<le> b" by (auto simp: divide_nonneg_pos)
   6.261 + 
   6.262 +  have "prob {x \<in> space M. \<alpha> * X x \<le> a}  = prob {x \<in> space M.  X x \<le> b}"
   6.263 +    by (rule arg_cong[where f= prob]) (auto simp:field_simps)
   6.264 +  
   6.265 +  moreover have "prob {x \<in> space M. X x \<le> b} = erlang_CDF k l b" by auto
   6.266 +  moreover have "erlang_CDF k (l / \<alpha>) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto
   6.267 +  ultimately show "prob {x \<in> space M. \<alpha> * X x \<le> a} = erlang_CDF k (l / \<alpha>) a" by fastforce  
   6.268 +qed
   6.269 +
   6.270 +lemma (in prob_space) has_bochner_integral_erlang_ith_moment:
   6.271 +  fixes k i :: nat and l :: real
   6.272 +  assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)"
   6.273 +  shows "has_bochner_integral M (\<lambda>x. X x ^ i) (fact (k + i) / (fact k * l ^ i))"
   6.274 +proof (rule has_bochner_integral_nn_integral)
   6.275 +  show "AE x in M. 0 \<le> X x ^ i"
   6.276 +    by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def)
   6.277 +  show "(\<integral>\<^sup>+ x. ereal (X x ^ i) \<partial>M) = ereal (fact (k + i) / (fact k * l ^ i))"
   6.278 +    using nn_integral_erlang_ith_moment[of l k i]
   6.279 +    by (subst distributed_nn_integral[symmetric, OF D]) auto
   6.280 +qed (insert distributed_measurable[OF D], simp)
   6.281 +
   6.282 +lemma (in prob_space) erlang_ith_moment_integrable:
   6.283 +  "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> integrable M (\<lambda>x. X x ^ i)"
   6.284 +  by rule (rule has_bochner_integral_erlang_ith_moment)
   6.285 +
   6.286 +lemma (in prob_space) erlang_ith_moment:
   6.287 +  "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow>
   6.288 +    expectation (\<lambda>x. X x ^ i) = fact (k + i) / (fact k * l ^ i)"
   6.289 +  by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment)
   6.290 +
   6.291 +lemma (in prob_space) erlang_distributed_variance:
   6.292 +  assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)"
   6.293 +  shows "variance X = (k + 1) / l\<^sup>2"
   6.294 +proof (subst variance_eq)
   6.295 +  show "integrable M X" "integrable M (\<lambda>x. (X x)\<^sup>2)"
   6.296 +    using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2]
   6.297 +    by auto
   6.298 +
   6.299 +  show "expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2"
   6.300 +    using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2]
   6.301 +    by simp (auto simp: power2_eq_square field_simps real_of_nat_Suc)
   6.302 +qed
   6.303 +
   6.304  subsection {* Exponential distribution *}
   6.305  
   6.306 -definition exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where
   6.307 -  "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))"
   6.308 +abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where
   6.309 +  "exponential_density \<equiv> erlang_density 0"
   6.310  
   6.311 -lemma borel_measurable_exponential_density[measurable]: "exponential_density l \<in> borel_measurable borel"
   6.312 -  by (auto simp add: exponential_density_def[abs_def])
   6.313 +lemma exponential_density_def:
   6.314 +  "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))"
   6.315 +  by (simp add: fun_eq_iff erlang_density_def)
   6.316 +
   6.317 +lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \<le> a then 1 - exp (- l * a) else 0)"
   6.318 +  by (simp add: erlang_CDF_def)
   6.319  
   6.320  lemma (in prob_space) exponential_distributed_params:
   6.321    assumes D: "distributed M lborel X (exponential_density l)"
   6.322 @@ -42,74 +341,20 @@
   6.323      by (simp add: emeasure_density distributed_distr_eq_density[OF D])
   6.324  qed assumption
   6.325  
   6.326 -lemma
   6.327 -  assumes [arith]: "0 < l"
   6.328 -  shows emeasure_exponential_density_le0: "0 \<le> a \<Longrightarrow> emeasure (density lborel (exponential_density l)) {.. a} = 1 - exp (- a * l)"
   6.329 -    and prob_space_exponential_density: "prob_space (density lborel (exponential_density l))"
   6.330 -      (is "prob_space ?D")
   6.331 -proof -
   6.332 -  let ?f = "\<lambda>x. l * exp (- x * l)"
   6.333 -  let ?F = "\<lambda>x. - exp (- x * l)"
   6.334 -
   6.335 -  have deriv: "\<And>x. DERIV ?F x :> ?f x" "\<And>x. 0 \<le> l * exp (- x * l)"
   6.336 -    by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff)
   6.337 -
   6.338 -  have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)"
   6.339 -    by (auto simp: emeasure_density exponential_density_def
   6.340 -             intro!: nn_integral_cong split: split_indicator)
   6.341 -  also have "\<dots> = ereal (0 - ?F 0)"
   6.342 -  proof (rule nn_integral_FTC_atLeast)
   6.343 -    have "((\<lambda>x. exp (l * x)) ---> 0) at_bot"
   6.344 -      by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]])
   6.345 -         (simp_all add: tendsto_const filterlim_ident)
   6.346 -    then show "((\<lambda>x. - exp (- x * l)) ---> 0) at_top"
   6.347 -      unfolding filterlim_at_top_mirror
   6.348 -      by (simp add: tendsto_minus_cancel_left[symmetric] ac_simps)
   6.349 -  qed (insert deriv, auto)
   6.350 -  also have "\<dots> = 1" by (simp add: one_ereal_def)
   6.351 -  finally have "emeasure ?D (space ?D) = 1" .
   6.352 -  then show "prob_space ?D" by rule
   6.353 -
   6.354 -  assume "0 \<le> a"
   6.355 -  have "emeasure ?D {..a} = (\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)"
   6.356 -    by (auto simp add: emeasure_density intro!: nn_integral_cong split: split_indicator)
   6.357 -       (auto simp: exponential_density_def)
   6.358 -  also have "(\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)"
   6.359 -    using `0 \<le> a` deriv by (intro nn_integral_FTC_atLeastAtMost) auto
   6.360 -  also have "\<dots> = 1 - exp (- a * l)"
   6.361 -    by simp
   6.362 -  finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" .
   6.363 -qed
   6.364 -
   6.365 +lemma prob_space_exponential_density: "0 < l \<Longrightarrow> prob_space (density lborel (exponential_density l))"
   6.366 +  by (rule prob_space_erlang_density)
   6.367  
   6.368  lemma (in prob_space) exponential_distributedD_le:
   6.369    assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
   6.370    shows "\<P>(x in M. X x \<le> a) = 1 - exp (- a * l)"
   6.371 -proof -
   6.372 -  have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}"
   6.373 -    using distributed_measurable[OF D] 
   6.374 -    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
   6.375 -  also have "\<dots> = emeasure (density lborel (exponential_density l)) {.. a}"
   6.376 -    unfolding distributed_distr_eq_density[OF D] ..
   6.377 -  also have "\<dots> = 1 - exp (- a * l)"
   6.378 -    using emeasure_exponential_density_le0[OF exponential_distributed_params[OF D] a] .
   6.379 -  finally show ?thesis
   6.380 -    by (auto simp: measure_def)
   6.381 -qed
   6.382 +  using erlang_distributed_le[OF D exponential_distributed_params[OF D] a] a
   6.383 +  by (simp add: erlang_CDF_def)
   6.384  
   6.385  lemma (in prob_space) exponential_distributedD_gt:
   6.386    assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
   6.387    shows "\<P>(x in M. a < X x ) = exp (- a * l)"
   6.388 -proof -
   6.389 -  have "exp (- a * l) = 1 - \<P>(x in M. X x \<le> a)"
   6.390 -    unfolding exponential_distributedD_le[OF D a] by simp
   6.391 -  also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })"
   6.392 -    using distributed_measurable[OF D]
   6.393 -    by (subst prob_compl) auto
   6.394 -  also have "\<dots> = \<P>(x in M. a < X x )"
   6.395 -    by (auto intro!: arg_cong[where f=prob] simp: not_le)
   6.396 -  finally show ?thesis by simp
   6.397 -qed
   6.398 +  using erlang_distributed_gt[OF D exponential_distributed_params[OF D] a] a
   6.399 +  by (simp add: erlang_CDF_def)
   6.400  
   6.401  lemma (in prob_space) exponential_distributed_memoryless:
   6.402    assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t"
   6.403 @@ -129,100 +374,202 @@
   6.404    assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
   6.405      and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1 - exp (- a * l)"
   6.406    shows "distributed M lborel X (exponential_density l)"
   6.407 -proof (rule distributedI_borel_atMost)
   6.408 -  fix a :: real
   6.409 -
   6.410 -  { assume "a \<le> 0"  
   6.411 -    with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}"
   6.412 -      by (intro emeasure_mono) auto
   6.413 -    then have "emeasure M {x\<in>space M. X x \<le> a} = 0"
   6.414 -      using X_distr[of 0] by (simp add: one_ereal_def emeasure_le_0_iff) }
   6.415 -  note eq_0 = this
   6.416 -
   6.417 -  have "\<And>x. \<not> 0 \<le> a \<Longrightarrow> ereal (exponential_density l x) * indicator {..a} x = 0"
   6.418 -    by (simp add: exponential_density_def)
   6.419 -  then show "(\<integral>\<^sup>+ x. exponential_density l x * indicator {..a} x \<partial>lborel) = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)"
   6.420 -    using emeasure_exponential_density_le0[of l a]
   6.421 -    by (auto simp: emeasure_density times_ereal.simps[symmetric] ereal_indicator
   6.422 -             simp del: times_ereal.simps ereal_zero_times)
   6.423 -  show "emeasure M {x\<in>space M. X x \<le> a} = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)"
   6.424 -    using X_distr[of a] eq_0 by (auto simp: one_ereal_def)
   6.425 -  show "AE x in lborel. 0 \<le> exponential_density l x "
   6.426 -    by (auto simp: exponential_density_def)
   6.427 -qed simp_all
   6.428 +proof (rule erlang_distributedI)
   6.429 +  fix a :: real assume "0 \<le> a" then show "emeasure M {x \<in> space M. X x \<le> a} = ereal (erlang_CDF 0 l a)"
   6.430 +    using X_distr[of a] by (simp add: erlang_CDF_def one_ereal_def)
   6.431 +qed fact+
   6.432  
   6.433  lemma (in prob_space) exponential_distributed_iff:
   6.434    "distributed M lborel X (exponential_density l) \<longleftrightarrow>
   6.435      (X \<in> borel_measurable M \<and> 0 < l \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = 1 - exp (- a * l)))"
   6.436 -  using
   6.437 -    distributed_measurable[of M lborel X "exponential_density l"]
   6.438 -    exponential_distributed_params[of X l]
   6.439 -    emeasure_exponential_density_le0[of l]
   6.440 -    exponential_distributedD_le[of X l]
   6.441 -  by (auto intro!: exponential_distributedI simp: one_ereal_def emeasure_eq_measure)
   6.442 +  using exponential_distributed_params[of X l] erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0)
   6.443  
   6.444 -lemma borel_integral_x_exp:
   6.445 -  "has_bochner_integral lborel (\<lambda>x. x * exp (- x) * indicator {0::real ..} x) 1"
   6.446 -proof (rule has_bochner_integral_monotone_convergence)
   6.447 -  let ?f = "\<lambda>i x. x * exp (- x) * indicator {0::real .. i} x"
   6.448 -  have "eventually (\<lambda>b::real. 0 \<le> b) at_top"
   6.449 -    by (rule eventually_ge_at_top)
   6.450 -  then have "eventually (\<lambda>b. 1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)) at_top"
   6.451 -  proof eventually_elim
   6.452 -   fix b :: real assume [simp]: "0 \<le> b"
   6.453 -    have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) - (integral\<^sup>L lborel (?f b)) = 
   6.454 -      (\<integral>x. (exp (-x) - x * exp (-x)) * indicator {0 .. b} x \<partial>lborel)"
   6.455 -      by (subst integral_diff[symmetric])
   6.456 -         (auto intro!: borel_integrable_atLeastAtMost integral_cong split: split_indicator)
   6.457 -    also have "\<dots> = b * exp (-b) - 0 * exp (- 0)"
   6.458 -    proof (rule integral_FTC_atLeastAtMost)
   6.459 -      fix x assume "0 \<le> x" "x \<le> b"
   6.460 -      show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)"
   6.461 -        by (auto intro!: derivative_eq_intros)
   6.462 -      show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x "
   6.463 -        by (intro continuous_intros)
   6.464 -    qed fact
   6.465 -    also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)"
   6.466 -      by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros)
   6.467 -    finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)"
   6.468 -      by (auto simp: field_simps exp_minus inverse_eq_divide)
   6.469 -  qed
   6.470 -  then have "((\<lambda>i. integral\<^sup>L lborel (?f i)) ---> 1 - (0 + 0)) at_top"
   6.471 -  proof (rule Lim_transform_eventually)
   6.472 -    show "((\<lambda>i. 1 - (inverse (exp i) + i / exp i)) ---> 1 - (0 + 0 :: real)) at_top"
   6.473 -      using tendsto_power_div_exp_0[of 1]
   6.474 -      by (intro tendsto_intros tendsto_inverse_0_at_top exp_at_top) simp
   6.475 -  qed
   6.476 -  then show "(\<lambda>i. integral\<^sup>L lborel (?f i)) ----> 1"
   6.477 -    by (intro filterlim_compose[OF _ filterlim_real_sequentially]) simp
   6.478 -  show "AE x in lborel. mono (\<lambda>n::nat. x * exp (- x) * indicator {0..real n} x)"
   6.479 -    by (auto simp: mono_def mult_le_0_iff zero_le_mult_iff split: split_indicator)
   6.480 -  show "\<And>i::nat. integrable lborel (\<lambda>x. x * exp (- x) * indicator {0..real i} x)"
   6.481 -    by (rule borel_integrable_atLeastAtMost) auto
   6.482 -  show "AE x in lborel. (\<lambda>i. x * exp (- x) * indicator {0..real i} x) ----> x * exp (- x) * indicator {0..} x"
   6.483 -    apply (intro AE_I2 Lim_eventually )
   6.484 -    apply (rule_tac c="natfloor x + 1" in eventually_sequentiallyI)
   6.485 -    apply (auto simp add: not_le dest!: ge_natfloor_plus_one_imp_gt[simplified] split: split_indicator)
   6.486 -    done
   6.487 -qed (auto intro!: borel_measurable_times borel_measurable_exp)
   6.488  
   6.489  lemma (in prob_space) exponential_distributed_expectation:
   6.490 -  assumes D: "distributed M lborel X (exponential_density l)"
   6.491 -  shows "expectation X = 1 / l"
   6.492 -proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric])
   6.493 -  have "0 < l"
   6.494 -   using exponential_distributed_params[OF D] .
   6.495 -  have [simp]: "\<And>x. x * (l * (exp (- (x * l)) * indicator {0..} (x * l))) =
   6.496 -    x * exponential_density l x"
   6.497 -    using `0 < l`
   6.498 -    by (auto split: split_indicator simp: zero_le_mult_iff exponential_density_def)
   6.499 -  from borel_integral_x_exp `0 < l`
   6.500 -  have "has_bochner_integral lborel (\<lambda>x. exponential_density l x * x) (1 / l)"
   6.501 -    by (subst (asm) lborel_has_bochner_integral_real_affine_iff[of l _ _ 0])
   6.502 -       (simp_all add: field_simps)
   6.503 -  then show "(\<integral> x. exponential_density l x * x \<partial>lborel) = 1 / l"
   6.504 -    by (metis has_bochner_integral_integral_eq)
   6.505 -qed simp
   6.506 +  "distributed M lborel X (exponential_density l) \<Longrightarrow> expectation X = 1 / l"
   6.507 +  using erlang_ith_moment[OF exponential_distributed_params, of X l X 0 1] by simp
   6.508 +
   6.509 +lemma exponential_density_nonneg: "0 < l \<Longrightarrow> 0 \<le> exponential_density l x"
   6.510 +  by (auto simp: exponential_density_def)
   6.511 +
   6.512 +lemma (in prob_space) exponential_distributed_min:
   6.513 +  assumes expX: "distributed M lborel X (exponential_density l)"
   6.514 +  assumes expY: "distributed M lborel Y (exponential_density u)"
   6.515 +  assumes ind: "indep_var borel X borel Y"
   6.516 +  shows "distributed M lborel (\<lambda>x. min (X x) (Y x)) (exponential_density (l + u))"
   6.517 +proof (subst exponential_distributed_iff, safe)
   6.518 +  have randX: "random_variable borel X" using expX by (simp add: exponential_distributed_iff)
   6.519 +  moreover have randY: "random_variable borel Y" using expY by (simp add: exponential_distributed_iff)
   6.520 +  ultimately show "random_variable borel (\<lambda>x. min (X x) (Y x))" by auto
   6.521 +  
   6.522 +  have "0 < l" by (rule exponential_distributed_params) fact
   6.523 +  moreover have "0 < u" by (rule exponential_distributed_params) fact
   6.524 +  ultimately  show " 0 < l + u" by force
   6.525 +
   6.526 +  fix a::real assume a[arith]: "0 \<le> a"
   6.527 +  have gt1[simp]: "\<P>(x in M. a < X x ) = exp (- a * l)" by (rule exponential_distributedD_gt[OF expX a]) 
   6.528 +  have gt2[simp]: "\<P>(x in M. a < Y x ) = exp (- a * u)" by (rule exponential_distributedD_gt[OF expY a]) 
   6.529 +
   6.530 +  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])
   6.531 +
   6.532 +  also have " ... =  \<P>(x in M. a < (X x)) *  \<P>(x in M. a< (Y x) )"
   6.533 +    using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp
   6.534 +  also have " ... = exp (- a * (l + u))" by (auto simp:field_simps mult_exp_exp)
   6.535 +  finally have indep_prob: "\<P>(x in M. a < (min (X x) (Y x)) ) = exp (- a * (l + u))" .
   6.536 +
   6.537 +  have "{x \<in> space M. (min (X x) (Y x)) \<le>a } = (space M - {x \<in> space M. a<(min (X x) (Y x)) })"
   6.538 +    by auto
   6.539 +  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}"
   6.540 +    using randX randY by (auto simp: prob_compl) 
   6.541 +  then show "prob {x \<in> space M. (min (X x) (Y x)) \<le> a} = 1 - exp (- a * (l + u))"
   6.542 +    using indep_prob by auto
   6.543 +qed
   6.544 + 
   6.545 +lemma (in prob_space) exponential_distributed_Min:
   6.546 +  assumes finI: "finite I"
   6.547 +  assumes A: "I \<noteq> {}"
   6.548 +  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density (l i))"
   6.549 +  assumes ind: "indep_vars (\<lambda>i. borel) X I" 
   6.550 +  shows "distributed M lborel (\<lambda>x. Min ((\<lambda>i. X i x)`I)) (exponential_density (\<Sum>i\<in>I. l i))"
   6.551 +using assms
   6.552 +proof (induct rule: finite_ne_induct)
   6.553 +  case (singleton i) then show ?case by simp
   6.554 +next
   6.555 +  case (insert i I)
   6.556 +  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)))"
   6.557 +      by (intro exponential_distributed_min indep_vars_Min insert)
   6.558 +         (auto intro: indep_vars_subset) 
   6.559 +  then show ?case
   6.560 +    using insert by simp
   6.561 +qed
   6.562 +
   6.563 +lemma (in prob_space) exponential_distributed_variance:
   6.564 +  "distributed M lborel X (exponential_density l) \<Longrightarrow> variance X = 1 / l\<^sup>2"
   6.565 +  using erlang_distributed_variance[OF exponential_distributed_params, of X l X 0] by simp
   6.566 +
   6.567 +lemma nn_integral_zero': "AE x in M. f x = 0 \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) = 0"
   6.568 +  by (simp cong: nn_integral_cong_AE)
   6.569 +
   6.570 +lemma convolution_erlang_density:
   6.571 +  fixes k\<^sub>1 k\<^sub>2 :: nat
   6.572 +  assumes [simp, arith]: "0 < l"
   6.573 +  shows "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y)) * ereal (erlang_density k\<^sub>2 l y) \<partial>lborel) =
   6.574 +    (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
   6.575 +      (is "?LHS = ?RHS")
   6.576 +proof
   6.577 +  fix x :: real
   6.578 +  have "x \<le> 0 \<or> 0 < x"
   6.579 +    by arith
   6.580 +  then show "?LHS x = ?RHS x"
   6.581 +  proof
   6.582 +    assume "x \<le> 0" then show ?thesis
   6.583 +      apply (subst nn_integral_zero')
   6.584 +      apply (rule AE_I[where N="{0}"])
   6.585 +      apply (auto simp add: erlang_density_def not_less)
   6.586 +      done
   6.587 +  next
   6.588 +    note zero_le_mult_iff[simp] zero_le_divide_iff[simp]
   6.589 +  
   6.590 +    have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l) = 1"
   6.591 +      using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 0] by (simp del: fact_Suc)
   6.592 +  
   6.593 +    have 1: "(\<integral>\<^sup>+ x. ereal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l x * indicator {0<..} x) \<partial>lborel) = 1"
   6.594 +      apply (subst I_eq1[symmetric])
   6.595 +      unfolding erlang_density_def
   6.596 +      by (auto intro!: nn_integral_cong split:split_indicator)
   6.597 +  
   6.598 +    have "prob_space (density lborel ?LHS)"
   6.599 +      unfolding times_ereal.simps[symmetric]
   6.600 +      by (intro prob_space_convolution_density) 
   6.601 +         (auto intro!: prob_space_erlang_density erlang_density_nonneg)
   6.602 +    then have 2: "integral\<^sup>N lborel ?LHS = 1"
   6.603 +      by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density)
   6.604 +  
   6.605 +    let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))"
   6.606 +    let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))"
   6.607 +    let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1"
   6.608 +    let ?L = "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \<partial>lborel)"
   6.609 +
   6.610 +    { fix x :: real assume [arith]: "0 < x"
   6.611 +      have *: "\<And>x y n. (x - y * x::real)^n = x^n * (1 - y)^n"
   6.612 +        unfolding power_mult_distrib[symmetric] by (simp add: field_simps)
   6.613 +    
   6.614 +      have "?LHS x = ?L x"
   6.615 +        unfolding erlang_density_def
   6.616 +        by (auto intro!: nn_integral_cong split:split_indicator)
   6.617 +      also have "... = (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x"
   6.618 +        apply (subst nn_integral_real_affine[where c=x and t = 0])
   6.619 +        apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] erlang_density_nonneg del: fact_Suc)
   6.620 +        apply (intro nn_integral_cong)
   6.621 +        apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add *
   6.622 +                    simp del: fact_Suc split: split_indicator)
   6.623 +        done
   6.624 +      finally have "(\<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y) * erlang_density k\<^sub>2 l y) \<partial>lborel) = 
   6.625 +        (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x"
   6.626 +        by simp }
   6.627 +    note * = this
   6.628 +
   6.629 +    assume [arith]: "0 < x"
   6.630 +    have 3: "1 = integral\<^sup>N lborel (\<lambda>xa. ?LHS xa * indicator {0<..} xa)"
   6.631 +      by (subst 2[symmetric])
   6.632 +         (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"]
   6.633 +               simp: erlang_density_def  nn_integral_multc[symmetric] indicator_def split: split_if_asm)
   6.634 +    also have "... = integral\<^sup>N lborel (\<lambda>x. (ereal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))"
   6.635 +      by (auto intro!: nn_integral_cong simp: * split: split_indicator)
   6.636 +    also have "... = ereal (?C) * ?I"
   6.637 +      using 1
   6.638 +      by (auto simp: nn_integral_nonneg nn_integral_cmult)  
   6.639 +    finally have " ereal (?C) * ?I = 1" by presburger
   6.640 +  
   6.641 +    then show ?thesis
   6.642 +      using * by simp
   6.643 +  qed
   6.644 +qed
   6.645 +
   6.646 +lemma (in prob_space) sum_indep_erlang:
   6.647 +  assumes indep: "indep_var borel X borel Y"
   6.648 +  assumes [simp, arith]: "0 < l"
   6.649 +  assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)"
   6.650 +  assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)"
   6.651 +  shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
   6.652 +  using assms
   6.653 +  apply (subst convolution_erlang_density[symmetric, OF `0<l`])
   6.654 +  apply (intro distributed_convolution)
   6.655 +  apply auto
   6.656 +  done
   6.657 +
   6.658 +lemma (in prob_space) erlang_distributed_setsum:
   6.659 +  assumes finI : "finite I"
   6.660 +  assumes A: "I \<noteq> {}"
   6.661 +  assumes [simp, arith]: "0 < l"
   6.662 +  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (erlang_density (k i) l)"
   6.663 +  assumes ind: "indep_vars (\<lambda>i. borel) X I"
   6.664 +  shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((\<Sum>i\<in>I. Suc (k i)) - 1) l)"
   6.665 +using assms
   6.666 +proof (induct rule: finite_ne_induct)
   6.667 +  case (singleton i) then show ?case by auto
   6.668 +next
   6.669 +  case (insert i I)
   6.670 +    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)"
   6.671 +      by(intro sum_indep_erlang indep_vars_setsum) (auto intro!: indep_vars_subset)
   6.672 +    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)"
   6.673 +      using insert by auto
   6.674 +    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"
   6.675 +      using insert by (auto intro!: Suc_pred simp: ac_simps)    
   6.676 +    finally show ?case by fast
   6.677 +qed
   6.678 +
   6.679 +lemma (in prob_space) exponential_distributed_setsum:
   6.680 +  assumes finI: "finite I"
   6.681 +  assumes A: "I \<noteq> {}"
   6.682 +  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density l)"
   6.683 +  assumes ind: "indep_vars (\<lambda>i. borel) X I" 
   6.684 +  shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((card I) - 1) l)"
   6.685 +proof -
   6.686 +  obtain i where "i \<in> I" using assms by auto
   6.687 +  note exponential_distributed_params[OF expX[OF this]]
   6.688 +  from erlang_distributed_setsum[OF assms(1,2) this assms(3,4)] show ?thesis by simp
   6.689 +qed
   6.690  
   6.691  subsection {* Uniform distribution *}
   6.692  
   6.693 @@ -393,4 +740,19 @@
   6.694    finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" .
   6.695  qed auto
   6.696  
   6.697 +lemma (in prob_space) uniform_distributed_variance:
   6.698 +  fixes a b :: real
   6.699 +  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
   6.700 +  shows "variance X = (b - a)\<^sup>2 / 12"
   6.701 +proof (subst distributed_variance)
   6.702 +  have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
   6.703 +  let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
   6.704 +  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)"
   6.705 +    by (intro integral_cong) (auto split: split_indicator)
   6.706 +  also have "\<dots> = (b - a)\<^sup>2 / 12"
   6.707 +    by (simp add: integral_power measure_lebesgue_Icc uniform_distributed_expectation[OF D])
   6.708 +       (simp add: eval_nat_numeral field_simps )
   6.709 +  finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
   6.710 +qed fact
   6.711 +
   6.712  end
     7.1 --- a/src/HOL/Probability/Independent_Family.thy	Wed Jun 11 13:39:38 2014 +0200
     7.2 +++ b/src/HOL/Probability/Independent_Family.thy	Thu Jun 12 15:47:36 2014 +0200
     7.3 @@ -1,5 +1,6 @@
     7.4  (*  Title:      HOL/Probability/Independent_Family.thy
     7.5      Author:     Johannes Hölzl, TU München
     7.6 +    Author:     Sudeep Kanav, TU München
     7.7  *)
     7.8  
     7.9  header {* Independent families of events, event sets, and random variables *}
    7.10 @@ -478,6 +479,107 @@
    7.11      by (simp cong: indep_sets_cong)
    7.12  qed
    7.13  
    7.14 +lemma (in prob_space) indep_vars_restrict:
    7.15 +  assumes ind: "indep_vars M' X I" and K: "\<And>j. j \<in> L \<Longrightarrow> K j \<subseteq> I" and J: "disjoint_family_on K L"
    7.16 +  shows "indep_vars (\<lambda>j. PiM (K j) M') (\<lambda>j \<omega>. restrict (\<lambda>i. X i \<omega>) (K j)) L"
    7.17 +  unfolding indep_vars_def
    7.18 +proof safe
    7.19 +  fix j assume "j \<in> L" then show "random_variable (Pi\<^sub>M (K j) M') (\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>)"
    7.20 +    using K ind by (auto simp: indep_vars_def intro!: measurable_restrict)
    7.21 +next
    7.22 +  have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable M (M' i)"
    7.23 +    using ind by (auto simp: indep_vars_def)
    7.24 +  let ?proj = "\<lambda>j S. {(\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>) -` A \<inter> space M |A. A \<in> S}"
    7.25 +  let ?UN = "\<lambda>j. sigma_sets (space M) (\<Union>i\<in>K j. { X i -` A \<inter> space M| A. A \<in> sets (M' i) })"
    7.26 +  show "indep_sets (\<lambda>i. sigma_sets (space M) (?proj i (sets (Pi\<^sub>M (K i) M')))) L"
    7.27 +  proof (rule indep_sets_mono_sets)
    7.28 +    fix j assume j: "j \<in> L"
    7.29 +    have "sigma_sets (space M) (?proj j (sets (Pi\<^sub>M (K j) M'))) = 
    7.30 +      sigma_sets (space M) (sigma_sets (space M) (?proj j (prod_algebra (K j) M')))"
    7.31 +      using j K X[THEN measurable_space] unfolding sets_PiM
    7.32 +      by (subst sigma_sets_vimage_commute) (auto simp add: Pi_iff)
    7.33 +    also have "\<dots> = sigma_sets (space M) (?proj j (prod_algebra (K j) M'))"
    7.34 +      by (rule sigma_sets_sigma_sets_eq) auto
    7.35 +    also have "\<dots> \<subseteq> ?UN j"
    7.36 +    proof (rule sigma_sets_mono, safe del: disjE elim!: prod_algebraE)
    7.37 +      fix J E assume J: "finite J" "J \<noteq> {} \<or> K j = {}"  "J \<subseteq> K j" and E: "\<forall>i. i \<in> J \<longrightarrow> E i \<in> sets (M' i)"
    7.38 +      show "(\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>) -` prod_emb (K j) M' J (Pi\<^sub>E J E) \<inter> space M \<in> ?UN j"
    7.39 +      proof cases
    7.40 +        assume "K j = {}" with J show ?thesis
    7.41 +          by (auto simp add: sigma_sets_empty_eq prod_emb_def)
    7.42 +      next
    7.43 +        assume "K j \<noteq> {}" with J have "J \<noteq> {}"
    7.44 +          by auto
    7.45 +        { interpret sigma_algebra "space M" "?UN j"
    7.46 +            by (rule sigma_algebra_sigma_sets) auto 
    7.47 +          have "\<And>A. (\<And>i. i \<in> J \<Longrightarrow> A i \<in> ?UN j) \<Longrightarrow> INTER J A \<in> ?UN j"
    7.48 +            using `finite J` `J \<noteq> {}` by (rule finite_INT) blast }
    7.49 +        note INT = this
    7.50 +
    7.51 +        from `J \<noteq> {}` J K E[rule_format, THEN sets.sets_into_space] j
    7.52 +        have "(\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>) -` prod_emb (K j) M' J (Pi\<^sub>E J E) \<inter> space M
    7.53 +          = (\<Inter>i\<in>J. X i -` E i \<inter> space M)"
    7.54 +          apply (subst prod_emb_PiE[OF _ ])
    7.55 +          apply auto []
    7.56 +          apply auto []
    7.57 +          apply (auto simp add: Pi_iff intro!: X[THEN measurable_space])
    7.58 +          apply (erule_tac x=i in ballE)
    7.59 +          apply auto
    7.60 +          done
    7.61 +        also have "\<dots> \<in> ?UN j"
    7.62 +          apply (rule INT)
    7.63 +          apply (rule sigma_sets.Basic)
    7.64 +          using `J \<subseteq> K j` E
    7.65 +          apply auto
    7.66 +          done
    7.67 +        finally show ?thesis .
    7.68 +      qed
    7.69 +    qed
    7.70 +    finally show "sigma_sets (space M) (?proj j (sets (Pi\<^sub>M (K j) M'))) \<subseteq> ?UN j" .
    7.71 +  next
    7.72 +    show "indep_sets ?UN L"
    7.73 +    proof (rule indep_sets_collect_sigma)
    7.74 +      show "indep_sets (\<lambda>i. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) (\<Union>j\<in>L. K j)"
    7.75 +      proof (rule indep_sets_mono_index)
    7.76 +        show "indep_sets (\<lambda>i. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
    7.77 +          using ind unfolding indep_vars_def2 by auto
    7.78 +        show "(\<Union>l\<in>L. K l) \<subseteq> I"
    7.79 +          using K by auto
    7.80 +      qed
    7.81 +    next
    7.82 +      fix l i assume "l \<in> L" "i \<in> K l"
    7.83 +      show "Int_stable {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
    7.84 +        apply (auto simp: Int_stable_def)
    7.85 +        apply (rule_tac x="A \<inter> Aa" in exI)
    7.86 +        apply auto
    7.87 +        done
    7.88 +    qed fact
    7.89 +  qed
    7.90 +qed
    7.91 +
    7.92 +lemma (in prob_space) indep_var_restrict:
    7.93 +  assumes ind: "indep_vars M' X I" and AB: "A \<inter> B = {}" "A \<subseteq> I" "B \<subseteq> I"
    7.94 +  shows "indep_var (PiM A M') (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) A) (PiM B M') (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) B)"
    7.95 +proof -
    7.96 +  have *:
    7.97 +    "case_bool (Pi\<^sub>M A M') (Pi\<^sub>M B M') = (\<lambda>b. PiM (case_bool A B b) M')"
    7.98 +    "case_bool (\<lambda>\<omega>. \<lambda>i\<in>A. X i \<omega>) (\<lambda>\<omega>. \<lambda>i\<in>B. X i \<omega>) = (\<lambda>b \<omega>. \<lambda>i\<in>case_bool A B b. X i \<omega>)"
    7.99 +    by (simp_all add: fun_eq_iff split: bool.split)
   7.100 +  show ?thesis
   7.101 +    unfolding indep_var_def * using AB
   7.102 +    by (intro indep_vars_restrict[OF ind]) (auto simp: disjoint_family_on_def split: bool.split)
   7.103 +qed
   7.104 +
   7.105 +lemma (in prob_space) indep_vars_subset:
   7.106 +  assumes "indep_vars M' X I" "J \<subseteq> I"
   7.107 +  shows "indep_vars M' X J"
   7.108 +  using assms unfolding indep_vars_def indep_sets_def
   7.109 +  by auto
   7.110 +
   7.111 +lemma (in prob_space) indep_vars_cong:
   7.112 +  "I = J \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> X i = Y i) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> M' i = N' i) \<Longrightarrow> indep_vars M' X I \<longleftrightarrow> indep_vars N' Y J"
   7.113 +  unfolding indep_vars_def2 by (intro conj_cong indep_sets_cong) auto
   7.114 +
   7.115  definition (in prob_space) tail_events where
   7.116    "tail_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
   7.117  
   7.118 @@ -801,6 +903,69 @@
   7.119    qed
   7.120  qed
   7.121  
   7.122 +lemma (in prob_space) indep_var_compose:
   7.123 +  assumes "indep_var M1 X1 M2 X2" "Y1 \<in> measurable M1 N1" "Y2 \<in> measurable M2 N2"
   7.124 +  shows "indep_var N1 (Y1 \<circ> X1) N2 (Y2 \<circ> X2)"
   7.125 +proof -
   7.126 +  have "indep_vars (case_bool N1 N2) (\<lambda>b. case_bool Y1 Y2 b \<circ> case_bool X1 X2 b) UNIV"
   7.127 +    using assms
   7.128 +    by (intro indep_vars_compose[where M'="case_bool M1 M2"])
   7.129 +       (auto simp: indep_var_def split: bool.split)
   7.130 +  also have "(\<lambda>b. case_bool Y1 Y2 b \<circ> case_bool X1 X2 b) = case_bool (Y1 \<circ> X1) (Y2 \<circ> X2)"
   7.131 +    by (simp add: fun_eq_iff split: bool.split)
   7.132 +  finally show ?thesis
   7.133 +    unfolding indep_var_def .
   7.134 +qed
   7.135 +
   7.136 +lemma (in prob_space) indep_vars_Min:
   7.137 +  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   7.138 +  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
   7.139 +  shows "indep_var borel (X i) borel (\<lambda>\<omega>. Min ((\<lambda>i. X i \<omega>)`I))"
   7.140 +proof -
   7.141 +  have "indep_var
   7.142 +    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
   7.143 +    borel ((\<lambda>f. Min (f`I)) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
   7.144 +    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] borel_measurable_Min) auto
   7.145 +  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
   7.146 +    by auto
   7.147 +  also have "((\<lambda>f. Min (f`I)) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I)) = (\<lambda>\<omega>. Min ((\<lambda>i. X i \<omega>)`I))"
   7.148 +    by (auto cong: rev_conj_cong)
   7.149 +  finally show ?thesis
   7.150 +    unfolding indep_var_def .
   7.151 +qed
   7.152 +
   7.153 +lemma (in prob_space) indep_vars_setsum:
   7.154 +  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   7.155 +  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
   7.156 +  shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Sum>i\<in>I. X i \<omega>)"
   7.157 +proof -
   7.158 +  have "indep_var 
   7.159 +    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
   7.160 +    borel ((\<lambda>f. \<Sum>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
   7.161 +    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] ) auto
   7.162 +  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
   7.163 +    by auto
   7.164 +  also have "((\<lambda>f. \<Sum>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I)) = (\<lambda>\<omega>. \<Sum>i\<in>I. X i \<omega>)"
   7.165 +    by (auto cong: rev_conj_cong)
   7.166 +  finally show ?thesis .
   7.167 +qed
   7.168 +
   7.169 +lemma (in prob_space) indep_vars_setprod:
   7.170 +  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   7.171 +  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
   7.172 +  shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Prod>i\<in>I. X i \<omega>)"
   7.173 +proof -
   7.174 +  have "indep_var 
   7.175 +    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
   7.176 +    borel ((\<lambda>f. \<Prod>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
   7.177 +    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] ) auto
   7.178 +  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
   7.179 +    by auto
   7.180 +  also have "((\<lambda>f. \<Prod>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I)) = (\<lambda>\<omega>. \<Prod>i\<in>I. X i \<omega>)"
   7.181 +    by (auto cong: rev_conj_cong)
   7.182 +  finally show ?thesis .
   7.183 +qed
   7.184 +
   7.185  lemma (in prob_space) indep_varsD_finite:
   7.186    assumes X: "indep_vars M' X I"
   7.187    assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)"
   7.188 @@ -933,6 +1098,20 @@
   7.189    finally show ?thesis .
   7.190  qed
   7.191  
   7.192 +lemma (in prob_space) prob_indep_random_variable:
   7.193 +  assumes ind[simp]: "indep_var N X N Y"
   7.194 +  assumes [simp]: "A \<in> sets N" "B \<in> sets N"
   7.195 +  shows "\<P>(x in M. X x \<in> A \<and> Y x \<in> B) = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
   7.196 +proof-
   7.197 +  have  " \<P>(x in M. (X x)\<in>A \<and>  (Y x)\<in> B ) = prob ((\<lambda>x. (X x, Y x)) -` (A \<times> B) \<inter> space M)" 
   7.198 +    by (auto intro!: arg_cong[where f= prob])
   7.199 +  also have "...=  prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"  
   7.200 +    by (auto intro!: indep_varD[where Ma=N and Mb=N])     
   7.201 +  also have "... = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
   7.202 +    by (auto intro!: arg_cong2[where f= "op *"] arg_cong[where f= prob])
   7.203 +  finally show ?thesis .
   7.204 +qed
   7.205 +
   7.206  lemma (in prob_space)
   7.207    assumes "indep_var S X T Y"
   7.208    shows indep_var_rv1: "random_variable S X"
   7.209 @@ -1023,4 +1202,115 @@
   7.210    using indep_var_distribution_eq[of S X T Y] indep
   7.211    by (intro distributed_joint_indep'[OF S T X Y]) auto
   7.212  
   7.213 +lemma (in prob_space) indep_vars_nn_integral:
   7.214 +  assumes I: "finite I" "indep_vars (\<lambda>_. borel) X I" "\<And>i \<omega>. i \<in> I \<Longrightarrow> 0 \<le> X i \<omega>"
   7.215 +  shows "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
   7.216 +proof cases
   7.217 +  assume "I \<noteq> {}"
   7.218 +  def Y \<equiv> "\<lambda>i \<omega>. if i \<in> I then X i \<omega> else 0"
   7.219 +  { fix i have "i \<in> I \<Longrightarrow> random_variable borel (X i)"
   7.220 +    using I(2) by (cases "i\<in>I") (auto simp: indep_vars_def) }
   7.221 +  note rv_X = this
   7.222 +
   7.223 +  { fix i have "random_variable borel (Y i)"
   7.224 +    using I(2) by (cases "i\<in>I") (auto simp: Y_def rv_X) }
   7.225 +  note rv_Y = this[measurable]
   7.226 +    
   7.227 +  interpret Y: prob_space "distr M borel (Y i)" for i
   7.228 +    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def)
   7.229 +  interpret product_sigma_finite "\<lambda>i. distr M borel (Y i)"
   7.230 +    ..
   7.231 +  
   7.232 +  have indep_Y: "indep_vars (\<lambda>i. borel) Y I"
   7.233 +    by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def)
   7.234 +
   7.235 +  have "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (Y i \<omega>)) \<partial>M)"
   7.236 +    using I(3) by (auto intro!: nn_integral_cong setprod_cong simp add: Y_def max_def)
   7.237 +  also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))"
   7.238 +    by (subst nn_integral_distr) auto
   7.239 +  also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. max 0 (\<omega> i)) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
   7.240 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] ..
   7.241 +  also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^sup>+\<omega>. max 0 \<omega> \<partial>distr M borel (Y i)))"
   7.242 +    by (rule product_nn_integral_setprod) (auto intro: `finite I`)
   7.243 +  also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
   7.244 +    by (intro setprod_cong nn_integral_cong)
   7.245 +       (auto simp: nn_integral_distr nn_integral_max_0 Y_def rv_X)
   7.246 +  finally show ?thesis .
   7.247 +qed (simp add: emeasure_space_1)
   7.248 +
   7.249 +lemma (in prob_space)
   7.250 +  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{real_normed_field, banach, second_countable_topology}"
   7.251 +  assumes I: "finite I" "indep_vars (\<lambda>_. borel) X I" "\<And>i. i \<in> I \<Longrightarrow> integrable M (X i)"
   7.252 +  shows indep_vars_lebesgue_integral: "(\<integral>\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)" (is ?eq)
   7.253 +    and indep_vars_integrable: "integrable M (\<lambda>\<omega>. (\<Prod>i\<in>I. X i \<omega>))" (is ?int)
   7.254 +proof (induct rule: case_split)
   7.255 +  assume "I \<noteq> {}"
   7.256 +  def Y \<equiv> "\<lambda>i \<omega>. if i \<in> I then X i \<omega> else 0"
   7.257 +  { fix i have "i \<in> I \<Longrightarrow> random_variable borel (X i)"
   7.258 +    using I(2) by (cases "i\<in>I") (auto simp: indep_vars_def) }
   7.259 +  note rv_X = this[measurable]
   7.260 +
   7.261 +  { fix i have "random_variable borel (Y i)"
   7.262 +    using I(2) by (cases "i\<in>I") (auto simp: Y_def rv_X) }
   7.263 +  note rv_Y = this[measurable]
   7.264 +
   7.265 +  { fix i have "integrable M (Y i)"
   7.266 +    using I(3) by (cases "i\<in>I") (auto simp: Y_def) }
   7.267 +  note int_Y = this
   7.268 +    
   7.269 +  interpret Y: prob_space "distr M borel (Y i)" for i
   7.270 +    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def)
   7.271 +  interpret product_sigma_finite "\<lambda>i. distr M borel (Y i)"
   7.272 +    ..
   7.273 +  
   7.274 +  have indep_Y: "indep_vars (\<lambda>i. borel) Y I"
   7.275 +    by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def)
   7.276 +
   7.277 +  have "(\<integral>\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<omega>. (\<Prod>i\<in>I. Y i \<omega>) \<partial>M)"
   7.278 +    using I(3) by (simp add: Y_def)
   7.279 +  also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))"
   7.280 +    by (subst integral_distr) auto
   7.281 +  also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
   7.282 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] ..
   7.283 +  also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<omega>. \<omega> \<partial>distr M borel (Y i)))"
   7.284 +    by (rule product_integral_setprod) (auto intro: `finite I` simp: integrable_distr_eq int_Y)
   7.285 +  also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)"
   7.286 +    by (intro setprod_cong integral_cong)
   7.287 +       (auto simp: integral_distr Y_def rv_X)
   7.288 +  finally show ?eq .
   7.289 +
   7.290 +  have "integrable (distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x)) (\<lambda>\<omega>. (\<Prod>i\<in>I. \<omega> i))"
   7.291 +    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y]
   7.292 +    by (intro product_integrable_setprod[OF `finite I`])
   7.293 +       (simp add: integrable_distr_eq int_Y)
   7.294 +  then show ?int
   7.295 +    by (simp add: integrable_distr_eq Y_def)
   7.296 +qed (simp_all add: prob_space)
   7.297 +
   7.298 +lemma (in prob_space)
   7.299 +  fixes X1 X2 :: "'a \<Rightarrow> 'b::{real_normed_field, banach, second_countable_topology}"
   7.300 +  assumes "indep_var borel X1 borel X2" "integrable M X1" "integrable M X2"
   7.301 +  shows indep_var_lebesgue_integral: "(\<integral>\<omega>. X1 \<omega> * X2 \<omega> \<partial>M) = (\<integral>\<omega>. X1 \<omega> \<partial>M) * (\<integral>\<omega>. X2 \<omega> \<partial>M)" (is ?eq)
   7.302 +    and indep_var_integrable: "integrable M (\<lambda>\<omega>. X1 \<omega> * X2 \<omega>)" (is ?int)
   7.303 +unfolding indep_var_def
   7.304 +proof -
   7.305 +  have *: "(\<lambda>\<omega>. X1 \<omega> * X2 \<omega>) = (\<lambda>\<omega>. \<Prod>i\<in>UNIV. (case_bool X1 X2 i \<omega>))"
   7.306 +    by (simp add: UNIV_bool mult_commute)
   7.307 +  have **: "(\<lambda> _. borel) = case_bool borel borel"
   7.308 +    by (rule ext, metis (full_types) bool.simps(3) bool.simps(4))
   7.309 +  show ?eq
   7.310 +    apply (subst *)
   7.311 +    apply (subst indep_vars_lebesgue_integral)
   7.312 +    apply (auto)
   7.313 +    apply (subst **, subst indep_var_def [symmetric], rule assms)
   7.314 +    apply (simp split: bool.split add: assms)
   7.315 +    by (simp add: UNIV_bool mult_commute)
   7.316 +  show ?int
   7.317 +    apply (subst *)
   7.318 +    apply (rule indep_vars_integrable)
   7.319 +    apply auto
   7.320 +    apply (subst **, subst indep_var_def [symmetric], rule assms)
   7.321 +    by (simp split: bool.split add: assms)
   7.322 +qed
   7.323 +
   7.324  end
     8.1 --- a/src/HOL/Probability/Information.thy	Wed Jun 11 13:39:38 2014 +0200
     8.2 +++ b/src/HOL/Probability/Information.thy	Thu Jun 12 15:47:36 2014 +0200
     8.3 @@ -8,7 +8,7 @@
     8.4  theory Information
     8.5  imports
     8.6    Independent_Family
     8.7 -  Radon_Nikodym
     8.8 +  Distributions
     8.9    "~~/src/HOL/Library/Convex"
    8.10  begin
    8.11  
    8.12 @@ -400,27 +400,6 @@
    8.13      done
    8.14  qed
    8.15  
    8.16 -lemma distributed_integrable:
    8.17 -  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
    8.18 -    integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
    8.19 -  by (auto simp: distributed_real_AE
    8.20 -                    distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq)
    8.21 -  
    8.22 -lemma distributed_transform_integrable:
    8.23 -  assumes Px: "distributed M N X Px"
    8.24 -  assumes "distributed M P Y Py"
    8.25 -  assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
    8.26 -  shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
    8.27 -proof -
    8.28 -  have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))"
    8.29 -    by (rule distributed_integrable) fact+
    8.30 -  also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))"
    8.31 -    using Y by simp
    8.32 -  also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
    8.33 -    using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
    8.34 -  finally show ?thesis .
    8.35 -qed
    8.36 -
    8.37  lemma integrable_cong_AE_imp:
    8.38    "integrable M g \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (AE x in M. g x = f x) \<Longrightarrow> integrable M f"
    8.39    using integrable_cong_AE[of f M g] by (auto simp: eq_commute)
    8.40 @@ -937,6 +916,35 @@
    8.41      by (subst integral_mult_right) (auto simp: measure_def)
    8.42  qed
    8.43  
    8.44 +lemma (in information_space) entropy_exponential:
    8.45 +  assumes D: "distributed M lborel X (exponential_density l)"
    8.46 +  shows "entropy b lborel X = log b (exp 1 / l)"
    8.47 +proof -
    8.48 +  have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D])
    8.49 + 
    8.50 +  have [simp]: "integrable lborel (exponential_density l)"
    8.51 +    using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp
    8.52 +
    8.53 +  have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1"
    8.54 +    using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space)
    8.55 +    
    8.56 +  have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)"
    8.57 +    using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp
    8.58 +
    8.59 +  have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l"
    8.60 +    using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp
    8.61 +    
    8.62 +  have "entropy b lborel X = - (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)"
    8.63 +    using D by (rule entropy_distr)
    8.64 +  also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 
    8.65 +    (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
    8.66 +    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
    8.67 +  also have "\<dots> = (ln l - 1) / ln b"
    8.68 +    by simp
    8.69 +  finally show ?thesis
    8.70 +    by (simp add: log_def divide_simps ln_div)
    8.71 +qed
    8.72 +
    8.73  lemma (in information_space) entropy_simple_distributed:
    8.74    "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
    8.75    by (subst entropy_distr[OF simple_distributed])
     9.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Jun 11 13:39:38 2014 +0200
     9.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jun 12 15:47:36 2014 +0200
     9.3 @@ -516,6 +516,8 @@
     9.4      by (intro exI[of _ A]) (auto simp: subset_eq)
     9.5  qed
     9.6  
     9.7 +interpretation lborel_pair: pair_sigma_finite lborel lborel ..
     9.8 +
     9.9  lemma Int_stable_atLeastAtMost:
    9.10    fixes x::"'a::ordered_euclidean_space"
    9.11    shows "Int_stable (range (\<lambda>(a, b::'a). {a..b}))"
    9.12 @@ -1226,4 +1228,64 @@
    9.13    finally show ?thesis .
    9.14  qed
    9.15  
    9.16 +subsection {* Integration by parts *}
    9.17 +
    9.18 +lemma integral_by_parts_integrable:
    9.19 +  fixes f g F G::"real \<Rightarrow> real"
    9.20 +  assumes "a \<le> b"
    9.21 +  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
    9.22 +  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
    9.23 +  assumes [intro]: "!!x. DERIV F x :> f x"
    9.24 +  assumes [intro]: "!!x. DERIV G x :> g x"
    9.25 +  shows  "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
    9.26 +  by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)
    9.27 +
    9.28 +lemma integral_by_parts:
    9.29 +  fixes f g F G::"real \<Rightarrow> real"
    9.30 +  assumes [arith]: "a \<le> b"
    9.31 +  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
    9.32 +  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
    9.33 +  assumes [intro]: "!!x. DERIV F x :> f x"
    9.34 +  assumes [intro]: "!!x. DERIV G x :> g x"
    9.35 +  shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
    9.36 +            =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" 
    9.37 +proof-
    9.38 +  have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
    9.39 +    by (rule integral_FTC_atLeastAtMost, auto intro!: derivative_eq_intros continuous_intros) 
    9.40 +      (auto intro!: DERIV_isCont)
    9.41 +
    9.42 +  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
    9.43 +    (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
    9.44 +    apply (subst integral_add[symmetric])
    9.45 +    apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
    9.46 +    by (auto intro!: DERIV_isCont integral_cong split:split_indicator)
    9.47 +
    9.48 +  thus ?thesis using 0 by auto
    9.49 +qed
    9.50 +
    9.51 +lemma integral_by_parts':
    9.52 +  fixes f g F G::"real \<Rightarrow> real"
    9.53 +  assumes "a \<le> b"
    9.54 +  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
    9.55 +  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
    9.56 +  assumes "!!x. DERIV F x :> f x"
    9.57 +  assumes "!!x. DERIV G x :> g x"
    9.58 +  shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
    9.59 +            =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" 
    9.60 +  using integral_by_parts[OF assms] by (simp add: mult_ac)
    9.61 +
    9.62 +lemma integral_tendsto_at_top:
    9.63 +  fixes f :: "real \<Rightarrow> real"
    9.64 +  assumes [simp, intro]: "\<And>x. isCont f x"
    9.65 +  assumes [simp, arith]: "\<And>x. 0 \<le> f x"
    9.66 +  assumes [simp]: "integrable lborel f"
    9.67 +  assumes [measurable]: "f \<in> borel_measurable borel"
    9.68 +  shows "((\<lambda>x. \<integral>xa. f xa * indicator {0..x} xa \<partial>lborel) ---> \<integral>xa. f xa * indicator {0..} xa \<partial>lborel) at_top"
    9.69 +  apply (auto intro!: borel_integrable_atLeastAtMost monoI integral_mono tendsto_at_topI_sequentially  
    9.70 +    split:split_indicator)
    9.71 +  apply (rule integral_dominated_convergence[where w = " \<lambda>x. f x * indicator {0..} x"])
    9.72 +  unfolding LIMSEQ_def  
    9.73 +  apply (auto intro!: AE_I2 tendsto_mult integrable_mult_indicator split: split_indicator)
    9.74 +  by (metis ge_natfloor_plus_one_imp_gt less_imp_le)
    9.75 +
    9.76  end
    10.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Jun 11 13:39:38 2014 +0200
    10.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Jun 12 15:47:36 2014 +0200
    10.3 @@ -1187,6 +1187,7 @@
    10.4    by (auto simp add: emeasure_distr measurable_space
    10.5             intro!: arg_cong[where f="emeasure M"] measure_eqI)
    10.6  
    10.7 +
    10.8  subsection {* Real measure values *}
    10.9  
   10.10  lemma measure_nonneg: "0 \<le> measure M A"
   10.11 @@ -1526,6 +1527,14 @@
   10.12    assumes "measure M A = measure M (space M)" "A \<inter> B = {}"
   10.13    shows "measure M B = 0"
   10.14    using measure_space_inter[of B A] assms by (auto simp: ac_simps)
   10.15 +lemma (in finite_measure) finite_measure_distr:
   10.16 +  assumes f: "f \<in> measurable M M'" 
   10.17 +  shows "finite_measure (distr M M' f)"
   10.18 +proof (rule finite_measureI)
   10.19 +  have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
   10.20 +  with f show "emeasure (distr M M' f) (space (distr M M' f)) \<noteq> \<infinity>" by (auto simp: emeasure_distr)
   10.21 +qed
   10.22 +
   10.23  
   10.24  subsection {* Counting space *}
   10.25  
    11.1 --- a/src/HOL/Probability/Probability_Measure.thy	Wed Jun 11 13:39:38 2014 +0200
    11.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Thu Jun 12 15:47:36 2014 +0200
    11.3 @@ -27,6 +27,7 @@
    11.4  abbreviation (in prob_space) "prob \<equiv> measure M"
    11.5  abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"
    11.6  abbreviation (in prob_space) "expectation \<equiv> integral\<^sup>L M"
    11.7 +abbreviation (in prob_space) "variance X \<equiv> integral\<^sup>L M (\<lambda>x. (X x - expectation X)\<^sup>2)"
    11.8  
    11.9  lemma (in prob_space) prob_space_distr:
   11.10    assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)"
   11.11 @@ -333,6 +334,16 @@
   11.12      \<Longrightarrow> emeasure (distr M (MX \<Otimes>\<^sub>M MY) (\<lambda>x. (X x, Y x))) (A \<times> B) \<le> emeasure (distr M MY Y) B"
   11.13    by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
   11.14  
   11.15 +lemma (in prob_space) variance_eq:
   11.16 +  fixes X :: "'a \<Rightarrow> real"
   11.17 +  assumes [simp]: "integrable M X"
   11.18 +  assumes [simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)"
   11.19 +  shows "variance X = expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2"
   11.20 +  by (simp add: field_simps prob_space power2_diff power2_eq_square[symmetric])
   11.21 +
   11.22 +lemma (in prob_space) variance_positive: "0 \<le> variance (X::'a \<Rightarrow> real)"
   11.23 +  by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE)
   11.24 +
   11.25  locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
   11.26  
   11.27  sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>M M2"
   11.28 @@ -713,6 +724,47 @@
   11.29      done
   11.30  qed
   11.31  
   11.32 +lemma distributed_integrable:
   11.33 +  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
   11.34 +    integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
   11.35 +  by (auto simp: distributed_real_AE
   11.36 +                    distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq)
   11.37 +  
   11.38 +lemma distributed_transform_integrable:
   11.39 +  assumes Px: "distributed M N X Px"
   11.40 +  assumes "distributed M P Y Py"
   11.41 +  assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
   11.42 +  shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
   11.43 +proof -
   11.44 +  have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))"
   11.45 +    by (rule distributed_integrable) fact+
   11.46 +  also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))"
   11.47 +    using Y by simp
   11.48 +  also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
   11.49 +    using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
   11.50 +  finally show ?thesis .
   11.51 +qed
   11.52 +
   11.53 +lemma (in prob_space) distributed_variance:
   11.54 +  fixes f::"real \<Rightarrow> real"
   11.55 +  assumes D: "distributed M lborel X f"
   11.56 +  shows "variance X = (\<integral>x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)"
   11.57 +proof (subst distributed_integral[OF D, symmetric])
   11.58 +  show "(\<integral> x. f x * (x - expectation X)\<^sup>2 \<partial>lborel) = (\<integral> x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)"
   11.59 +    by (subst lborel_integral_real_affine[where c=1 and t="expectation X"])  (auto simp: ac_simps)
   11.60 +qed simp
   11.61 +
   11.62 +lemma (in prob_space) variance_affine:
   11.63 +  fixes f::"real \<Rightarrow> real"
   11.64 +  assumes [arith]: "b \<noteq> 0"
   11.65 +  assumes D[intro]: "distributed M lborel X f"
   11.66 +  assumes [simp]: "prob_space (density lborel f)"
   11.67 +  assumes I[simp]: "integrable M X"
   11.68 +  assumes I2[simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)" 
   11.69 +  shows "variance (\<lambda>x. a + b * X x) = b\<^sup>2 * variance X"
   11.70 +  by (subst variance_eq)
   11.71 +     (auto simp: power2_sum power_mult_distrib prob_space variance_eq right_diff_distrib)
   11.72 +
   11.73  definition
   11.74    "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and>
   11.75      finite (X`space M)"