# HG changeset patch
# User hoelzl
# Date 1402580856 -7200
# Node ID b0b9a10e4bf42c88150cf58dcf883cea4f8abf71
# Parent  596a499318ab81afc1ca79da4f8cd97d2e533029
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)

diff -r 596a499318ab -r b0b9a10e4bf4 CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Jun 11 13:39:38 2014 +0200
+++ b/CONTRIBUTORS	Thu Jun 12 15:47:36 2014 +0200
@@ -6,10 +6,14 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+
 * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
   Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT,
   Waldmeister, etc.).
 
+* June 2014: Sudeep Kanav, TUM, and Johannes Hölzl, TUM
+  Various properties of Erlang and exponentially distributed random variables.
+
 * May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM
   SML-based engines for MaSh.
 
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -557,6 +557,11 @@
   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)"
   unfolding nn_integral_snd[OF assms] M2.nn_integral_fst[OF assms] ..
 
+lemma (in pair_sigma_finite) Fubini':
+  assumes f: "split f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
+  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)"
+  using Fubini[OF f] by simp
+
 subsection {* Products on counting spaces, densities and distributions *}
 
 lemma sigma_sets_pair_measure_generator_finite:
@@ -737,4 +742,109 @@
     by (subst (1 2 3) emeasure_count_space) (auto simp: finite_cartesian_product_iff)
 qed
 
+subsection {* Product of Borel spaces *}
+
+lemma borel_Times:
+  fixes A :: "'a::topological_space set" and B :: "'b::topological_space set"
+  assumes A: "A \<in> sets borel" and B: "B \<in> sets borel"
+  shows "A \<times> B \<in> sets borel"
+proof -
+  have "A \<times> B = (A\<times>UNIV) \<inter> (UNIV \<times> B)"
+    by auto
+  moreover
+  { have "A \<in> sigma_sets UNIV {S. open S}" using A by (simp add: sets_borel)
+    then have "A\<times>UNIV \<in> sets borel"
+    proof (induct A)
+      case (Basic S) then show ?case
+        by (auto intro!: borel_open open_Times)
+    next
+      case (Compl A)
+      moreover have *: "(UNIV - A) \<times> UNIV = UNIV - (A \<times> UNIV)"
+        by auto
+      ultimately show ?case
+        unfolding * by auto
+    next
+      case (Union A)
+      moreover have *: "(UNION UNIV A) \<times> UNIV = UNION UNIV (\<lambda>i. A i \<times> UNIV)"
+        by auto
+      ultimately show ?case
+        unfolding * by auto
+    qed simp }
+  moreover
+  { have "B \<in> sigma_sets UNIV {S. open S}" using B by (simp add: sets_borel)
+    then have "UNIV\<times>B \<in> sets borel"
+    proof (induct B)
+      case (Basic S) then show ?case
+        by (auto intro!: borel_open open_Times)
+    next
+      case (Compl B)
+      moreover have *: "UNIV \<times> (UNIV - B) = UNIV - (UNIV \<times> B)"
+        by auto
+      ultimately show ?case
+        unfolding * by auto
+    next
+      case (Union B)
+      moreover have *: "UNIV \<times> (UNION UNIV B) = UNION UNIV (\<lambda>i. UNIV \<times> B i)"
+        by auto
+      ultimately show ?case
+        unfolding * by auto
+    qed simp }
+  ultimately show ?thesis
+    by auto
+qed
+
+lemma borel_prod: "sets (borel \<Otimes>\<^sub>M borel) =
+    (sets borel :: ('a::second_countable_topology \<times> 'b::second_countable_topology) set set)"
+  (is "?l = ?r")
+proof -
+  obtain A :: "'a set set" where A: "countable A" "topological_basis A"
+    by (metis ex_countable_basis)
+  moreover obtain B :: "'b set set" where B: "countable B" "topological_basis B"
+    by (metis ex_countable_basis)
+  ultimately have AB: "countable ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
+    by (auto intro!: topological_basis_prod)
+  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}"
+    by (simp add: sets_pair_measure
+       borel_eq_countable_basis[OF A] borel_eq_countable_basis[OF B])
+  also have "\<dots> \<supseteq> sigma_sets UNIV ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))" (is "... \<supseteq> ?A")
+    by (auto intro!: sigma_sets_mono)
+  also (xtrans) have "?A = sets borel"
+    by (simp add: borel_eq_countable_basis[OF AB])
+  finally have "?r \<subseteq> ?l" .
+  moreover have "?l \<subseteq> ?r"
+  proof (simp add: sets_pair_measure, safe intro!: sigma_sets_mono)
+    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}"
+    then show "A \<in> sets borel"
+      by (induct A) (auto intro!: borel_Times)
+  qed
+  ultimately show ?thesis by auto
+qed
+
+lemma borel_prod':
+  "borel \<Otimes>\<^sub>M borel = (borel :: 
+      ('a::second_countable_topology \<times> 'b::second_countable_topology) measure)"
+proof (rule measure_eqI[OF borel_prod])
+  interpret sigma_finite_measure "borel :: 'b measure"
+      by (default) (auto simp: borel_def emeasure_sigma intro!: exI[of _ "\<lambda>_. UNIV"])
+  fix X :: "('a \<times> 'b) set" assume asm: "X \<in> sets (borel \<Otimes>\<^sub>M borel)"
+  have "UNIV \<times> UNIV \<in> sets (borel \<Otimes>\<^sub>M borel :: ('a \<times> 'b) measure)" 
+      by (simp add: borel_prod)
+  moreover have "emeasure (borel \<Otimes>\<^sub>M borel) (UNIV \<times> UNIV :: ('a \<times> 'b) set) = 0"
+      by (subst emeasure_pair_measure_Times, simp_all add: borel_def emeasure_sigma)
+  moreover have "X \<subseteq> UNIV \<times> UNIV" by auto
+  ultimately have "emeasure (borel \<Otimes>\<^sub>M borel) X = 0" by (rule emeasure_eq_0)
+  thus "emeasure (borel \<Otimes>\<^sub>M borel) X = emeasure borel X"
+      by (simp add: borel_def emeasure_sigma)
+qed
+
+lemma finite_measure_pair_measure:
+  assumes "finite_measure M" "finite_measure N"
+  shows "finite_measure (N  \<Otimes>\<^sub>M M)"
+proof (rule finite_measureI)
+  interpret M: finite_measure M by fact
+  interpret N: finite_measure N by fact
+  show "emeasure (N  \<Otimes>\<^sub>M M) (space (N  \<Otimes>\<^sub>M M)) \<noteq> \<infinity>"
+    by (auto simp: space_pair_measure M.emeasure_pair_measure_Times)
+qed
+
 end
\ No newline at end of file
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -1518,9 +1518,37 @@
   using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
   using integral_norm_bound_ereal[of M f] by simp
   
+lemma integrableI_nn_integral_finite:
+  assumes [measurable]: "f \<in> borel_measurable M"
+    and nonneg: "AE x in M. 0 \<le> f x"
+    and finite: "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
+  shows "integrable M f"
+proof (rule integrableI_bounded)
+  have "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
+    using nonneg by (intro nn_integral_cong_AE) auto
+  with finite show "(\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M) < \<infinity>"
+    by auto
+qed simp
+
 lemma integral_eq_nn_integral:
-  "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)"
-  by (subst nn_integral_eq_integral) auto
+  assumes [measurable]: "f \<in> borel_measurable M"
+  assumes nonneg: "AE x in M. 0 \<le> f x"
+  shows "integral\<^sup>L M f = real (\<integral>\<^sup>+ x. ereal (f x) \<partial>M)"
+proof cases
+  assume *: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) = \<infinity>"
+  also have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) = (\<integral>\<^sup>+ x. ereal (norm (f x)) \<partial>M)"
+    using nonneg by (intro nn_integral_cong_AE) auto
+  finally have "\<not> integrable M f"
+    by (auto simp: integrable_iff_bounded)
+  then show ?thesis
+    by (simp add: * not_integrable_integral_eq)
+next
+  assume "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M) \<noteq> \<infinity>"
+  then have "integrable M f"
+    by (cases "\<integral>\<^sup>+ x. ereal (f x) \<partial>M") (auto intro!: integrableI_nn_integral_finite assms)
+  from nn_integral_eq_integral[OF this nonneg] show ?thesis
+    by simp
+qed
   
 lemma integrableI_simple_bochner_integrable:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -1933,7 +1961,7 @@
 subsection {* Legacy lemmas for the real-valued Lebesgue integral *}
 
 lemma real_lebesgue_integral_def:
-  assumes f: "integrable M f"
+  assumes f[measurable]: "integrable M f"
   shows "integral\<^sup>L M f = real (\<integral>\<^sup>+x. f x \<partial>M) - real (\<integral>\<^sup>+x. - f x \<partial>M)"
 proof -
   have "integral\<^sup>L M f = integral\<^sup>L M (\<lambda>x. max 0 (f x) - max 0 (- f x))"
@@ -1941,9 +1969,9 @@
   also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
     by (intro integral_diff integrable_max integrable_minus integrable_zero f)
   also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
-    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
+    by (subst integral_eq_nn_integral[symmetric]) auto
   also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
-    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
+    by (subst integral_eq_nn_integral[symmetric]) auto
   also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
     by (auto simp: max_def)
   also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -35,6 +35,9 @@
 lemma space_in_borel[measurable]: "UNIV \<in> sets borel"
   unfolding borel_def by auto
 
+lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}"
+  unfolding borel_def by (rule sets_measure_of) simp
+
 lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
   unfolding borel_def pred_def by auto
 
@@ -801,6 +804,20 @@
   "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"
   by (simp add: min_def)
 
+lemma borel_measurable_Min[measurable (raw)]:
+  "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"
+proof (induct I rule: finite_induct)
+  case (insert i I) then show ?case
+    by (cases "I = {}") auto
+qed auto
+
+lemma borel_measurable_Max[measurable (raw)]:
+  "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"
+proof (induct I rule: finite_induct)
+  case (insert i I) then show ?case
+    by (cases "I = {}") auto
+qed auto
+
 lemma borel_measurable_abs[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
   unfolding abs_real_def by simp
@@ -874,6 +891,36 @@
   "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
   by simp
 
+lemma borel_measurable_root [measurable]: "(root n) \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_sqrt [measurable]: "sqrt \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_power [measurable (raw)]:
+   fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
+   assumes f: "f \<in> borel_measurable M"
+   shows "(\<lambda>x. (f x) ^ n) \<in> borel_measurable M"
+   by (intro borel_measurable_continuous_on [OF _ f] continuous_intros)
+
+lemma borel_measurable_Re [measurable]: "Re \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_Im [measurable]: "Im \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_sin [measurable]: "sin \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_cos [measurable]: "cos \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_intros)
+
+lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_intros)
+
 subsection "Borel space on the extended reals"
 
 lemma borel_measurable_ereal[measurable (raw)]:
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Convolution.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Convolution.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -0,0 +1,241 @@
+(*  Title:      HOL/Probability/Convolution.thy
+    Author:     Sudeep Kanav, TU München
+    Author:     Johannes Hölzl, TU München *)
+
+header {* Convolution Measure *}
+
+theory Convolution
+  imports Independent_Family
+begin
+
+lemma (in finite_measure) sigma_finite_measure: "sigma_finite_measure M"
+  ..
+
+definition convolution :: "('a :: ordered_euclidean_space) measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" (infix "\<star>" 50) where
+  "convolution M N = distr (M \<Otimes>\<^sub>M N) borel (\<lambda>(x, y). x + y)"
+
+lemma
+  shows space_convolution[simp]: "space (convolution M N) = space borel"
+    and sets_convolution[simp]: "sets (convolution M N) = sets borel"
+    and measurable_convolution1[simp]: "measurable A (convolution M N) = measurable A borel"
+    and measurable_convolution2[simp]: "measurable (convolution M N) B = measurable borel B"
+  by (simp_all add: convolution_def)
+
+lemma nn_integral_convolution:
+  assumes "finite_measure M" "finite_measure N"
+  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
+  assumes [measurable]: "f \<in> borel_measurable borel"
+  shows "(\<integral>\<^sup>+x. f x \<partial>convolution M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f (x + y) \<partial>N \<partial>M)"
+proof -
+  interpret M: finite_measure M by fact
+  interpret N: finite_measure N by fact
+  interpret pair_sigma_finite M N ..
+  show ?thesis
+    unfolding convolution_def
+    by (simp add: nn_integral_distr N.nn_integral_fst[symmetric])
+qed
+
+lemma convolution_emeasure:
+  assumes "A \<in> sets borel" "finite_measure M" "finite_measure N"
+  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
+  assumes [simp]: "space M = space N" "space N = space borel"
+  shows "emeasure (M \<star> N) A = \<integral>\<^sup>+x. (emeasure N {a. a + x \<in> A}) \<partial>M "
+  using assms by (auto intro!: nn_integral_cong simp del: nn_integral_indicator simp: nn_integral_convolution 
+    nn_integral_indicator[symmetric] ab_semigroup_add_class.add_ac split:split_indicator)
+
+lemma convolution_emeasure':
+  assumes [simp]:"A \<in> sets borel"
+  assumes [simp]: "finite_measure M" "finite_measure N"
+  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
+  shows  "emeasure (M \<star> N) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y.  (indicator  A (x + y)) \<partial>N  \<partial>M"
+  by (auto simp del: nn_integral_indicator simp: nn_integral_convolution
+    nn_integral_indicator[symmetric] borel_measurable_indicator)
+
+lemma convolution_finite:
+  assumes [simp]: "finite_measure M" "finite_measure N"
+  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
+  shows "finite_measure (M \<star> N)"
+  unfolding convolution_def
+  by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto
+
+lemma convolution_emeasure_3:
+  assumes [simp, measurable]: "A \<in> sets borel"
+  assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L"
+  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
+  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"
+  apply (subst nn_integral_indicator[symmetric], simp)
+  apply (subst nn_integral_convolution, 
+        auto intro!: borel_measurable_indicator borel_measurable_indicator' convolution_finite)+
+  by (rule nn_integral_cong)+ (auto simp: semigroup_add_class.add_assoc)
+
+lemma convolution_emeasure_3':
+  assumes [simp, measurable]:"A \<in> sets borel"
+  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
+  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
+  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"
+  apply (subst nn_integral_indicator[symmetric], simp)+
+  apply (subst nn_integral_convolution)
+  apply (simp_all add: convolution_finite)
+  apply (subst nn_integral_convolution)
+  apply (simp_all add: finite_measure.sigma_finite_measure sigma_finite_measure.borel_measurable_nn_integral)
+  done
+
+lemma convolution_commutative:
+  assumes [simp]: "finite_measure M" "finite_measure N"
+  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
+  shows "(M \<star> N) = (N \<star> M)"
+proof (rule measure_eqI)  
+  interpret M: finite_measure M by fact
+  interpret N: finite_measure N by fact
+  interpret pair_sigma_finite M N ..
+
+  show "sets (M \<star> N) = sets (N \<star> M)" by simp
+
+  fix A assume "A \<in> sets (M \<star> N)"
+  then have 1[measurable]:"A \<in> sets borel" by simp
+  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')
+  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)
+  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
+  also have "... = emeasure (N \<star> M) A" by (auto intro!: nn_integral_cong simp: add_commute convolution_emeasure')
+  finally show "emeasure (M \<star> N) A = emeasure (N \<star> M) A" by simp
+qed
+
+lemma convolution_associative:
+  assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
+  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
+  shows "(L \<star> (M \<star> N)) = ((L \<star> M) \<star> N)"
+  by (auto intro!: measure_eqI simp: convolution_emeasure_3 convolution_emeasure_3')
+
+lemma (in prob_space) sum_indep_random_variable:
+  assumes ind: "indep_var borel X borel Y"
+  assumes [simp, measurable]: "random_variable borel X"
+  assumes [simp, measurable]: "random_variable borel Y"
+  shows "distr M borel (\<lambda>x. X x + Y x) = convolution (distr M borel X)  (distr M borel Y)"
+  using ind unfolding indep_var_distribution_eq convolution_def
+  by (auto simp: distr_distr intro!:arg_cong[where f = "distr M borel"])
+
+lemma (in prob_space) sum_indep_random_variable_lborel:
+  assumes ind: "indep_var borel X borel Y"
+  assumes [simp, measurable]: "random_variable lborel X"
+  assumes [simp, measurable]:"random_variable lborel Y" 
+  shows "distr M lborel (\<lambda>x. X x + Y x) = convolution (distr M lborel X)  (distr M lborel Y)"
+  using ind unfolding indep_var_distribution_eq convolution_def 
+  by (auto simp: distr_distr o_def intro!: arg_cong[where f = "distr M borel"] cong: distr_cong)
+
+lemma convolution_density:
+  fixes f g :: "real \<Rightarrow> ereal"
+  assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
+  assumes [simp]:"finite_measure (density lborel f)" "finite_measure (density lborel g)"
+  assumes gt_0[simp]: "AE x in lborel. 0 \<le> f x" "AE x in lborel. 0 \<le> g x"
+  shows "density lborel f \<star> density lborel g = density lborel (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)"
+    (is "?l = ?r")
+proof (intro measure_eqI)
+  fix A assume "A \<in> sets ?l"
+  then have [measurable]: "A \<in> sets borel"
+    by simp
+
+  have "(\<integral>\<^sup>+x. f x * (\<integral>\<^sup>+y. g y * indicator A (x + y) \<partial>lborel) \<partial>lborel) =
+    (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
+    using gt_0
+  proof (intro nn_integral_cong_AE, eventually_elim)
+    fix x assume "0 \<le> f x"
+    then have "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) =
+      (\<integral>\<^sup>+ y. f x * (g y * indicator A (x + y)) \<partial>lborel)"
+      by (intro nn_integral_cmult[symmetric]) auto
+    then show "f x * (\<integral>\<^sup>+ y. g y * indicator A (x + y) \<partial>lborel) =
+      (\<integral>\<^sup>+ y. g y * (f x * indicator A (x + y)) \<partial>lborel)"
+      by (simp add: ac_simps)
+  qed
+  also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) \<partial>lborel)"
+    by (intro lborel_pair.Fubini') simp
+  also have "\<dots> = (\<integral>\<^sup>+y. (\<integral>\<^sup>+x. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)"
+    using gt_0
+  proof (intro nn_integral_cong_AE, eventually_elim)
+    fix y assume "0 \<le> g y"
+    then have "(\<integral>\<^sup>+x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
+      g y * (\<integral>\<^sup>+x. f x * indicator A (x + y) \<partial>lborel)"
+      by (intro nn_integral_cmult) auto
+    also have "\<dots> = g y * (\<integral>\<^sup>+x. f (x - y) * indicator A x \<partial>lborel)"
+      using gt_0
+      by (subst nn_integral_real_affine[where c=1 and t="-y"])
+         (auto simp del: gt_0 simp add: one_ereal_def[symmetric])
+    also have "\<dots> = (\<integral>\<^sup>+x. g y * (f (x - y) * indicator A x) \<partial>lborel)"
+      using `0 \<le> g y` by (intro nn_integral_cmult[symmetric]) auto
+    finally show "(\<integral>\<^sup>+ x. g y * (f x * indicator A (x + y)) \<partial>lborel) =
+      (\<integral>\<^sup>+ x. f (x - y) * g y * indicator A x \<partial>lborel)"
+      by (simp add: ac_simps)
+  qed
+  also have "\<dots> = (\<integral>\<^sup>+x. (\<integral>\<^sup>+y. f (x - y) * g y * indicator A x \<partial>lborel) \<partial>lborel)"
+    by (intro lborel_pair.Fubini') simp
+  finally show "emeasure ?l A = emeasure ?r A"
+    by (auto simp: convolution_emeasure' nn_integral_density emeasure_density
+      nn_integral_multc)
+qed simp
+
+lemma (in prob_space) distributed_finite_measure_density:
+  "distributed M N X f \<Longrightarrow> finite_measure (density N f)"
+  using finite_measure_distr[of X N] distributed_distr_eq_density[of M N X f] by simp
+  
+
+lemma (in prob_space) distributed_convolution:
+  fixes f :: "real \<Rightarrow> _"
+  fixes g :: "real \<Rightarrow> _"
+  assumes indep: "indep_var borel X borel Y"
+  assumes X: "distributed M lborel X f"
+  assumes Y: "distributed M lborel Y g"
+  shows "distributed M lborel (\<lambda>x. X x + Y x) (\<lambda>x. \<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel)"
+  unfolding distributed_def
+proof safe
+  show "AE x in lborel. 0 \<le> \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel"
+    by (auto simp: nn_integral_nonneg)
+
+  have fg[measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
+    using distributed_borel_measurable[OF X] distributed_borel_measurable[OF Y] by simp_all
+  
+  show "(\<lambda>x. \<integral>\<^sup>+ xa. f (x - xa) * g xa \<partial>lborel) \<in> borel_measurable lborel" 
+    by measurable
+
+  have "distr M borel (\<lambda>x. X x + Y x) = (distr M borel X \<star> distr M borel Y)"
+    using distributed_measurable[OF X] distributed_measurable[OF Y]
+    by (intro sum_indep_random_variable) (auto simp: indep)
+  also have "\<dots> = (density lborel f \<star> density lborel g)"
+    using distributed_distr_eq_density[OF X] distributed_distr_eq_density[OF Y]
+    by (simp cong: distr_cong)
+  also have "\<dots> = density lborel (\<lambda>x. \<integral>\<^sup>+ y. f (x - y) * g y \<partial>lborel)"
+  proof (rule convolution_density)
+    show "finite_measure (density lborel f)"
+      using X by (rule distributed_finite_measure_density)
+    show "finite_measure (density lborel g)"
+      using Y by (rule distributed_finite_measure_density)
+    show "AE x in lborel. 0 \<le> f x"
+      using X by (rule distributed_AE)
+    show "AE x in lborel. 0 \<le> g x"
+      using Y by (rule distributed_AE)
+  qed fact+
+  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)"
+    by (simp cong: distr_cong)
+  show "random_variable lborel (\<lambda>x. X x + Y x)"
+    using distributed_measurable[OF X] distributed_measurable[OF Y] by simp
+qed
+
+lemma prob_space_convolution_density:
+  fixes f:: "real \<Rightarrow> _"
+  fixes g:: "real \<Rightarrow> _"
+  assumes [measurable]: "f\<in> borel_measurable borel"
+  assumes [measurable]: "g\<in> borel_measurable borel"
+  assumes gt_0[simp]: "\<And>x. 0 \<le> f x" "\<And>x. 0 \<le> g x"
+  assumes "prob_space (density lborel f)" (is "prob_space ?F")
+  assumes "prob_space (density lborel g)" (is "prob_space ?G")
+  shows "prob_space (density lborel (\<lambda>x.\<integral>\<^sup>+y. f (x - y) * g y \<partial>lborel))" (is "prob_space ?D")
+proof (subst convolution_density[symmetric])
+  interpret F: prob_space ?F by fact
+  show "finite_measure ?F" by unfold_locales
+  interpret G: prob_space ?G by fact
+  show "finite_measure ?G" by unfold_locales
+  interpret FG: pair_prob_space ?F ?G ..
+
+  show "prob_space (density lborel f \<star> density lborel g)"
+    unfolding convolution_def by (rule FG.prob_space_distr) simp
+qed simp_all
+
+end
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -1,14 +1,313 @@
+(*  Title:      HOL/Probability/Distributions.thy
+    Author:     Sudeep Kanav, TU München
+    Author:     Johannes Hölzl, TU München *)
+
+header {* Properties of Various Distributions *}
+
 theory Distributions
-  imports Probability_Measure
+  imports Probability_Measure Convolution
 begin
 
+lemma measure_lebesgue_Icc: "measure lebesgue {a .. b} = (if a \<le> b then b - a else 0)"
+  by (auto simp: measure_def)
+
+lemma integral_power:
+  "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
+proof (subst integral_FTC_atLeastAtMost)
+  fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
+    by (intro derivative_eq_intros) auto
+qed (auto simp: field_simps)
+
+lemma has_bochner_integral_nn_integral:
+  assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
+  assumes "(\<integral>\<^sup>+x. f x \<partial>M) = ereal x"
+  shows "has_bochner_integral M f x"
+  unfolding has_bochner_integral_iff
+proof
+  show "integrable M f"
+    using assms by (rule integrableI_nn_integral_finite)
+qed (auto simp: assms integral_eq_nn_integral)
+
+lemma (in prob_space) distributed_AE2:
+  assumes [measurable]: "distributed M N X f" "Measurable.pred N P"
+  shows "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)"
+proof -
+  have "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in distr M N X. P x)"
+    by (simp add: AE_distr_iff)
+  also have "\<dots> \<longleftrightarrow> (AE x in density N f. P x)"
+    unfolding distributed_distr_eq_density[OF assms(1)] ..
+  also have "\<dots> \<longleftrightarrow>  (AE x in N. 0 < f x \<longrightarrow> P x)"
+    by (rule AE_density) simp
+  finally show ?thesis .
+qed
+
+subsection {* Erlang *}
+
+lemma nn_intergal_power_times_exp_Icc:
+  assumes [arith]: "0 \<le> a"
+  shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x \<partial>lborel) =
+    (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _")
+proof -
+  let ?f = "\<lambda>k x. x^k * exp (-x) / fact k"
+  let ?F = "\<lambda>k x. - (\<Sum>n\<le>k. (x^n * exp (-x)) / fact n)"
+
+  have "?I * (inverse (fact k)) = 
+      (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (fact k)) \<partial>lborel)"
+    by (intro nn_integral_multc[symmetric]) auto
+  also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)"
+    by (intro nn_integral_cong) (simp add: field_simps)
+  also have "\<dots> = ereal (?F k a) - (?F k 0)"
+  proof (rule nn_integral_FTC_atLeastAtMost)
+    fix x assume "x \<in> {0..a}"
+    show "DERIV (?F k) x :> ?f k x"
+    proof(induction k)
+      case 0 show ?case by (auto intro!: derivative_eq_intros)
+    next
+      case (Suc k)
+      have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :>
+        ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k))"
+        by (intro DERIV_diff Suc)
+           (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc
+                 simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric])
+      also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)"
+        by simp
+      also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k)) = ?f (Suc k) x"
+        by (auto simp: field_simps simp del: fact_Suc)
+           (simp_all add: real_of_nat_Suc field_simps)
+      finally show ?case .
+    qed
+  qed auto
+  also have "\<dots> = ereal (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n))"
+    by (auto simp: power_0_left if_distrib[where f="\<lambda>x. x / a" for a] setsum_cases)
+  finally show ?thesis
+    by (cases "?I") (auto simp: field_simps)
+qed
+
+lemma nn_intergal_power_times_exp_Ici:
+  shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = fact k"
+proof (rule LIMSEQ_unique)
+  let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel"
+  show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
+    apply (intro nn_integral_LIMSEQ)
+    apply (auto simp: incseq_def le_fun_def eventually_sequentially
+                split: split_indicator intro!: Lim_eventually)
+    apply (metis natceiling_le_eq)
+    done
+
+  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"
+    by (intro tendsto_intros tendsto_power_div_exp_0) simp
+  then show "?X ----> fact k"
+    by (subst nn_intergal_power_times_exp_Icc)
+       (auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially])
+qed
+
+definition erlang_density :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
+  "erlang_density k l x = (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k)"
+
+definition erlang_CDF ::  "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
+  "erlang_CDF k l x = (if x < 0 then 0 else 1 - (\<Sum>n\<le>k. ((l * x)^n * exp (- l * x) / fact n)))"
+
+lemma erlang_density_nonneg: "0 \<le> l \<Longrightarrow> 0 \<le> erlang_density k l x"
+  by (simp add: erlang_density_def)
+
+lemma borel_measurable_erlang_density[measurable]: "erlang_density k l \<in> borel_measurable borel"
+  by (auto simp add: erlang_density_def[abs_def])
+
+lemma erlang_CDF_transform: "0 < l \<Longrightarrow> erlang_CDF k l a = erlang_CDF k 1 (l * a)"
+  by (auto simp add: erlang_CDF_def mult_less_0_iff)
+
+lemma nn_integral_erlang_density:
+  assumes [arith]: "0 < l"
+  shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a"
+proof cases
+  assume [arith]: "0 \<le> a"
+  have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x"
+    by (simp add: field_simps split: split_indicator)
+  have "(\<integral>\<^sup>+x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) =
+    (\<integral>\<^sup>+x. (l/fact k) * (ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x) \<partial>lborel)"
+    by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib split: split_indicator)
+  also have "\<dots> = (l/fact k) * (\<integral>\<^sup>+x. ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x \<partial>lborel)"
+    by (intro nn_integral_cmult) auto
+  also have "\<dots> = ereal (l/fact k) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^k * exp (- x)) * indicator {0 .. l * a} x \<partial>lborel))"
+    by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq)
+  also have "\<dots> = (1 - (\<Sum>n\<le>k. ((l * a)^n * exp (-(l * a))) / fact n))"
+    by (subst nn_intergal_power_times_exp_Icc) auto
+  also have "\<dots> = erlang_CDF k l a"
+    by (auto simp: erlang_CDF_def)
+  finally show ?thesis .
+next
+  assume "\<not> 0 \<le> a" 
+  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))"
+    by (intro nn_integral_cong) (auto simp: erlang_density_def)
+  ultimately show ?thesis
+    by (simp add: erlang_CDF_def)
+qed
+
+lemma emeasure_erlang_density: 
+  "0 < l \<Longrightarrow> emeasure (density lborel (erlang_density k l)) {.. a} = erlang_CDF k l a"
+  by (simp add: emeasure_density nn_integral_erlang_density)
+
+lemma nn_integral_erlang_ith_moment: 
+  fixes k i :: nat and l :: real
+  assumes [arith]: "0 < l" 
+  shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x ^ i) \<partial>lborel) = fact (k + i) / (fact k * l ^ i)"
+proof -
+  have eq: "\<And>x. indicator {0..} (x / l) = indicator {0..} x"
+    by (simp add: field_simps split: split_indicator)
+  have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x^i) \<partial>lborel) =
+    (\<integral>\<^sup>+x. (l/(fact k * l^i)) * (ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x) \<partial>lborel)"
+    by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib power_add split: split_indicator)
+  also have "\<dots> = (l/(fact k * l^i)) * (\<integral>\<^sup>+x. ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x \<partial>lborel)"
+    by (intro nn_integral_cmult) auto
+  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))"
+    by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq)
+  also have "\<dots> = fact (k + i) / (fact k * l ^ i)"
+    by (subst nn_intergal_power_times_exp_Ici) auto
+  finally show ?thesis .
+qed
+
+lemma prob_space_erlang_density:
+  assumes l[arith]: "0 < l"
+  shows "prob_space (density lborel (erlang_density k l))" (is "prob_space ?D")
+proof
+  show "emeasure ?D (space ?D) = 1"
+    using nn_integral_erlang_ith_moment[OF l, where k=k and i=0] by (simp add: emeasure_density)
+qed
+
+lemma (in prob_space) erlang_distributed_le:
+  assumes D: "distributed M lborel X (erlang_density k l)"
+  assumes [simp, arith]: "0 < l" "0 \<le> a"
+  shows "\<P>(x in M. X x \<le> a) = erlang_CDF k l a"
+proof -
+  have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}"
+    using distributed_measurable[OF D]
+    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
+  also have "\<dots> = emeasure (density lborel (erlang_density k l)) {.. a}"
+    unfolding distributed_distr_eq_density[OF D] ..
+  also have "\<dots> = erlang_CDF k l a"
+    by (auto intro!: emeasure_erlang_density)
+  finally show ?thesis
+    by (auto simp: measure_def)
+qed
+
+lemma (in prob_space) erlang_distributed_gt:
+  assumes D[simp]: "distributed M lborel X (erlang_density k l)"
+  assumes [arith]: "0 < l" "0 \<le> a"
+  shows "\<P>(x in M. a < X x ) = 1 - (erlang_CDF k l a)"
+proof -
+  have " 1 - (erlang_CDF k l a) = 1 - \<P>(x in M. X x \<le> a)" by (subst erlang_distributed_le) auto
+  also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })"
+    using distributed_measurable[OF D] by (auto simp: prob_compl)
+  also have "\<dots> = \<P>(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le)
+  finally show ?thesis by simp
+qed
+
+lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0"
+  by (induction k) (auto simp: erlang_CDF_def)
+
+lemma erlang_distributedI:
+  assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
+    and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = erlang_CDF k l a"
+  shows "distributed M lborel X (erlang_density k l)"
+proof (rule distributedI_borel_atMost)
+  fix a :: real
+  { assume "a \<le> 0"  
+    with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}"
+      by (intro emeasure_mono) auto
+    also have "... = 0"  by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0])
+    finally have "emeasure M {x\<in>space M. X x \<le> a} \<le> 0" by simp
+    then have "emeasure M {x\<in>space M. X x \<le> a} = 0" by (simp add:emeasure_le_0_iff)
+  }
+  note eq_0 = this
+
+  show "(\<integral>\<^sup>+ x. erlang_density k l x * indicator {..a} x \<partial>lborel) = ereal (erlang_CDF k l a)"
+    using nn_integral_erlang_density[of l k a]
+    by (simp add: times_ereal.simps(1)[symmetric] ereal_indicator del: times_ereal.simps)
+
+  show "emeasure M {x\<in>space M. X x \<le> a} = ereal (erlang_CDF k l a)"
+    using X_distr[of a] eq_0 by (auto simp: one_ereal_def erlang_CDF_def)
+qed (simp_all add: erlang_density_nonneg)
+
+lemma (in prob_space) erlang_distributed_iff:
+  assumes [arith]: "0<l"
+  shows "distributed M lborel X (erlang_density k l) \<longleftrightarrow>
+    (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 ))"
+  using
+    distributed_measurable[of M lborel X "erlang_density k l"]
+    emeasure_erlang_density[of l]
+    erlang_distributed_le[of X k l]
+  by (auto intro!: erlang_distributedI simp: one_ereal_def emeasure_eq_measure) 
+
+lemma (in prob_space) erlang_distributed_mult_const:
+  assumes erlX: "distributed M lborel X (erlang_density k l)"
+  assumes a_pos[arith]: "0 < \<alpha>"  "0 < l"
+  shows  "distributed M lborel (\<lambda>x. \<alpha> * X x) (erlang_density k (l / \<alpha>))"
+proof (subst erlang_distributed_iff, safe)
+  have [measurable]: "random_variable borel X"  and  [arith]: "0 < l " 
+  and  [simp]: "\<And>a. 0 \<le> a \<Longrightarrow> prob {x \<in> space M. X x \<le> a} = erlang_CDF k l a"
+    by(insert erlX, auto simp: erlang_distributed_iff)
+
+  show "random_variable borel (\<lambda>x. \<alpha> * X x)" "0 < l / \<alpha>"  "0 < l / \<alpha>" 
+    by (auto simp:field_simps)
+  
+  fix a:: real assume [arith]: "0 \<le> a"
+  obtain b:: real  where [simp, arith]: "b = a/ \<alpha>" by blast 
+
+  have [arith]: "0 \<le> b" by (auto simp: divide_nonneg_pos)
+ 
+  have "prob {x \<in> space M. \<alpha> * X x \<le> a}  = prob {x \<in> space M.  X x \<le> b}"
+    by (rule arg_cong[where f= prob]) (auto simp:field_simps)
+  
+  moreover have "prob {x \<in> space M. X x \<le> b} = erlang_CDF k l b" by auto
+  moreover have "erlang_CDF k (l / \<alpha>) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto
+  ultimately show "prob {x \<in> space M. \<alpha> * X x \<le> a} = erlang_CDF k (l / \<alpha>) a" by fastforce  
+qed
+
+lemma (in prob_space) has_bochner_integral_erlang_ith_moment:
+  fixes k i :: nat and l :: real
+  assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)"
+  shows "has_bochner_integral M (\<lambda>x. X x ^ i) (fact (k + i) / (fact k * l ^ i))"
+proof (rule has_bochner_integral_nn_integral)
+  show "AE x in M. 0 \<le> X x ^ i"
+    by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def)
+  show "(\<integral>\<^sup>+ x. ereal (X x ^ i) \<partial>M) = ereal (fact (k + i) / (fact k * l ^ i))"
+    using nn_integral_erlang_ith_moment[of l k i]
+    by (subst distributed_nn_integral[symmetric, OF D]) auto
+qed (insert distributed_measurable[OF D], simp)
+
+lemma (in prob_space) erlang_ith_moment_integrable:
+  "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> integrable M (\<lambda>x. X x ^ i)"
+  by rule (rule has_bochner_integral_erlang_ith_moment)
+
+lemma (in prob_space) erlang_ith_moment:
+  "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow>
+    expectation (\<lambda>x. X x ^ i) = fact (k + i) / (fact k * l ^ i)"
+  by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment)
+
+lemma (in prob_space) erlang_distributed_variance:
+  assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)"
+  shows "variance X = (k + 1) / l\<^sup>2"
+proof (subst variance_eq)
+  show "integrable M X" "integrable M (\<lambda>x. (X x)\<^sup>2)"
+    using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2]
+    by auto
+
+  show "expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2"
+    using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2]
+    by simp (auto simp: power2_eq_square field_simps real_of_nat_Suc)
+qed
+
 subsection {* Exponential distribution *}
 
-definition exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where
-  "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))"
+abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where
+  "exponential_density \<equiv> erlang_density 0"
 
-lemma borel_measurable_exponential_density[measurable]: "exponential_density l \<in> borel_measurable borel"
-  by (auto simp add: exponential_density_def[abs_def])
+lemma exponential_density_def:
+  "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))"
+  by (simp add: fun_eq_iff erlang_density_def)
+
+lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \<le> a then 1 - exp (- l * a) else 0)"
+  by (simp add: erlang_CDF_def)
 
 lemma (in prob_space) exponential_distributed_params:
   assumes D: "distributed M lborel X (exponential_density l)"
@@ -42,74 +341,20 @@
     by (simp add: emeasure_density distributed_distr_eq_density[OF D])
 qed assumption
 
-lemma
-  assumes [arith]: "0 < l"
-  shows emeasure_exponential_density_le0: "0 \<le> a \<Longrightarrow> emeasure (density lborel (exponential_density l)) {.. a} = 1 - exp (- a * l)"
-    and prob_space_exponential_density: "prob_space (density lborel (exponential_density l))"
-      (is "prob_space ?D")
-proof -
-  let ?f = "\<lambda>x. l * exp (- x * l)"
-  let ?F = "\<lambda>x. - exp (- x * l)"
-
-  have deriv: "\<And>x. DERIV ?F x :> ?f x" "\<And>x. 0 \<le> l * exp (- x * l)"
-    by (auto intro!: derivative_eq_intros simp: zero_le_mult_iff)
-
-  have "emeasure ?D (space ?D) = (\<integral>\<^sup>+ x. ereal (?f x) * indicator {0..} x \<partial>lborel)"
-    by (auto simp: emeasure_density exponential_density_def
-             intro!: nn_integral_cong split: split_indicator)
-  also have "\<dots> = ereal (0 - ?F 0)"
-  proof (rule nn_integral_FTC_atLeast)
-    have "((\<lambda>x. exp (l * x)) ---> 0) at_bot"
-      by (rule filterlim_compose[OF exp_at_bot filterlim_tendsto_pos_mult_at_bot[of _ l]])
-         (simp_all add: tendsto_const filterlim_ident)
-    then show "((\<lambda>x. - exp (- x * l)) ---> 0) at_top"
-      unfolding filterlim_at_top_mirror
-      by (simp add: tendsto_minus_cancel_left[symmetric] ac_simps)
-  qed (insert deriv, auto)
-  also have "\<dots> = 1" by (simp add: one_ereal_def)
-  finally have "emeasure ?D (space ?D) = 1" .
-  then show "prob_space ?D" by rule
-
-  assume "0 \<le> a"
-  have "emeasure ?D {..a} = (\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel)"
-    by (auto simp add: emeasure_density intro!: nn_integral_cong split: split_indicator)
-       (auto simp: exponential_density_def)
-  also have "(\<integral>\<^sup>+x. ereal (?f x) * indicator {0..a} x \<partial>lborel) = ereal (?F a) - ereal (?F 0)"
-    using `0 \<le> a` deriv by (intro nn_integral_FTC_atLeastAtMost) auto
-  also have "\<dots> = 1 - exp (- a * l)"
-    by simp
-  finally show "emeasure ?D {.. a} = 1 - exp (- a * l)" .
-qed
-
+lemma prob_space_exponential_density: "0 < l \<Longrightarrow> prob_space (density lborel (exponential_density l))"
+  by (rule prob_space_erlang_density)
 
 lemma (in prob_space) exponential_distributedD_le:
   assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
   shows "\<P>(x in M. X x \<le> a) = 1 - exp (- a * l)"
-proof -
-  have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}"
-    using distributed_measurable[OF D] 
-    by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
-  also have "\<dots> = emeasure (density lborel (exponential_density l)) {.. a}"
-    unfolding distributed_distr_eq_density[OF D] ..
-  also have "\<dots> = 1 - exp (- a * l)"
-    using emeasure_exponential_density_le0[OF exponential_distributed_params[OF D] a] .
-  finally show ?thesis
-    by (auto simp: measure_def)
-qed
+  using erlang_distributed_le[OF D exponential_distributed_params[OF D] a] a
+  by (simp add: erlang_CDF_def)
 
 lemma (in prob_space) exponential_distributedD_gt:
   assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
   shows "\<P>(x in M. a < X x ) = exp (- a * l)"
-proof -
-  have "exp (- a * l) = 1 - \<P>(x in M. X x \<le> a)"
-    unfolding exponential_distributedD_le[OF D a] by simp
-  also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })"
-    using distributed_measurable[OF D]
-    by (subst prob_compl) auto
-  also have "\<dots> = \<P>(x in M. a < X x )"
-    by (auto intro!: arg_cong[where f=prob] simp: not_le)
-  finally show ?thesis by simp
-qed
+  using erlang_distributed_gt[OF D exponential_distributed_params[OF D] a] a
+  by (simp add: erlang_CDF_def)
 
 lemma (in prob_space) exponential_distributed_memoryless:
   assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t"
@@ -129,100 +374,202 @@
   assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
     and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1 - exp (- a * l)"
   shows "distributed M lborel X (exponential_density l)"
-proof (rule distributedI_borel_atMost)
-  fix a :: real
-
-  { assume "a \<le> 0"  
-    with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}"
-      by (intro emeasure_mono) auto
-    then have "emeasure M {x\<in>space M. X x \<le> a} = 0"
-      using X_distr[of 0] by (simp add: one_ereal_def emeasure_le_0_iff) }
-  note eq_0 = this
-
-  have "\<And>x. \<not> 0 \<le> a \<Longrightarrow> ereal (exponential_density l x) * indicator {..a} x = 0"
-    by (simp add: exponential_density_def)
-  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)"
-    using emeasure_exponential_density_le0[of l a]
-    by (auto simp: emeasure_density times_ereal.simps[symmetric] ereal_indicator
-             simp del: times_ereal.simps ereal_zero_times)
-  show "emeasure M {x\<in>space M. X x \<le> a} = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)"
-    using X_distr[of a] eq_0 by (auto simp: one_ereal_def)
-  show "AE x in lborel. 0 \<le> exponential_density l x "
-    by (auto simp: exponential_density_def)
-qed simp_all
+proof (rule erlang_distributedI)
+  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)"
+    using X_distr[of a] by (simp add: erlang_CDF_def one_ereal_def)
+qed fact+
 
 lemma (in prob_space) exponential_distributed_iff:
   "distributed M lborel X (exponential_density l) \<longleftrightarrow>
     (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)))"
-  using
-    distributed_measurable[of M lborel X "exponential_density l"]
-    exponential_distributed_params[of X l]
-    emeasure_exponential_density_le0[of l]
-    exponential_distributedD_le[of X l]
-  by (auto intro!: exponential_distributedI simp: one_ereal_def emeasure_eq_measure)
+  using exponential_distributed_params[of X l] erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0)
 
-lemma borel_integral_x_exp:
-  "has_bochner_integral lborel (\<lambda>x. x * exp (- x) * indicator {0::real ..} x) 1"
-proof (rule has_bochner_integral_monotone_convergence)
-  let ?f = "\<lambda>i x. x * exp (- x) * indicator {0::real .. i} x"
-  have "eventually (\<lambda>b::real. 0 \<le> b) at_top"
-    by (rule eventually_ge_at_top)
-  then have "eventually (\<lambda>b. 1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)) at_top"
-  proof eventually_elim
-   fix b :: real assume [simp]: "0 \<le> b"
-    have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) - (integral\<^sup>L lborel (?f b)) = 
-      (\<integral>x. (exp (-x) - x * exp (-x)) * indicator {0 .. b} x \<partial>lborel)"
-      by (subst integral_diff[symmetric])
-         (auto intro!: borel_integrable_atLeastAtMost integral_cong split: split_indicator)
-    also have "\<dots> = b * exp (-b) - 0 * exp (- 0)"
-    proof (rule integral_FTC_atLeastAtMost)
-      fix x assume "0 \<le> x" "x \<le> b"
-      show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)"
-        by (auto intro!: derivative_eq_intros)
-      show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x "
-        by (intro continuous_intros)
-    qed fact
-    also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)"
-      by (rule integral_FTC_atLeastAtMost) (auto intro!: derivative_eq_intros)
-    finally show "1 - (inverse (exp b) + b / exp b) = integral\<^sup>L lborel (?f b)"
-      by (auto simp: field_simps exp_minus inverse_eq_divide)
-  qed
-  then have "((\<lambda>i. integral\<^sup>L lborel (?f i)) ---> 1 - (0 + 0)) at_top"
-  proof (rule Lim_transform_eventually)
-    show "((\<lambda>i. 1 - (inverse (exp i) + i / exp i)) ---> 1 - (0 + 0 :: real)) at_top"
-      using tendsto_power_div_exp_0[of 1]
-      by (intro tendsto_intros tendsto_inverse_0_at_top exp_at_top) simp
-  qed
-  then show "(\<lambda>i. integral\<^sup>L lborel (?f i)) ----> 1"
-    by (intro filterlim_compose[OF _ filterlim_real_sequentially]) simp
-  show "AE x in lborel. mono (\<lambda>n::nat. x * exp (- x) * indicator {0..real n} x)"
-    by (auto simp: mono_def mult_le_0_iff zero_le_mult_iff split: split_indicator)
-  show "\<And>i::nat. integrable lborel (\<lambda>x. x * exp (- x) * indicator {0..real i} x)"
-    by (rule borel_integrable_atLeastAtMost) auto
-  show "AE x in lborel. (\<lambda>i. x * exp (- x) * indicator {0..real i} x) ----> x * exp (- x) * indicator {0..} x"
-    apply (intro AE_I2 Lim_eventually )
-    apply (rule_tac c="natfloor x + 1" in eventually_sequentiallyI)
-    apply (auto simp add: not_le dest!: ge_natfloor_plus_one_imp_gt[simplified] split: split_indicator)
-    done
-qed (auto intro!: borel_measurable_times borel_measurable_exp)
 
 lemma (in prob_space) exponential_distributed_expectation:
-  assumes D: "distributed M lborel X (exponential_density l)"
-  shows "expectation X = 1 / l"
-proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric])
-  have "0 < l"
-   using exponential_distributed_params[OF D] .
-  have [simp]: "\<And>x. x * (l * (exp (- (x * l)) * indicator {0..} (x * l))) =
-    x * exponential_density l x"
-    using `0 < l`
-    by (auto split: split_indicator simp: zero_le_mult_iff exponential_density_def)
-  from borel_integral_x_exp `0 < l`
-  have "has_bochner_integral lborel (\<lambda>x. exponential_density l x * x) (1 / l)"
-    by (subst (asm) lborel_has_bochner_integral_real_affine_iff[of l _ _ 0])
-       (simp_all add: field_simps)
-  then show "(\<integral> x. exponential_density l x * x \<partial>lborel) = 1 / l"
-    by (metis has_bochner_integral_integral_eq)
-qed simp
+  "distributed M lborel X (exponential_density l) \<Longrightarrow> expectation X = 1 / l"
+  using erlang_ith_moment[OF exponential_distributed_params, of X l X 0 1] by simp
+
+lemma exponential_density_nonneg: "0 < l \<Longrightarrow> 0 \<le> exponential_density l x"
+  by (auto simp: exponential_density_def)
+
+lemma (in prob_space) exponential_distributed_min:
+  assumes expX: "distributed M lborel X (exponential_density l)"
+  assumes expY: "distributed M lborel Y (exponential_density u)"
+  assumes ind: "indep_var borel X borel Y"
+  shows "distributed M lborel (\<lambda>x. min (X x) (Y x)) (exponential_density (l + u))"
+proof (subst exponential_distributed_iff, safe)
+  have randX: "random_variable borel X" using expX by (simp add: exponential_distributed_iff)
+  moreover have randY: "random_variable borel Y" using expY by (simp add: exponential_distributed_iff)
+  ultimately show "random_variable borel (\<lambda>x. min (X x) (Y x))" by auto
+  
+  have "0 < l" by (rule exponential_distributed_params) fact
+  moreover have "0 < u" by (rule exponential_distributed_params) fact
+  ultimately  show " 0 < l + u" by force
+
+  fix a::real assume a[arith]: "0 \<le> a"
+  have gt1[simp]: "\<P>(x in M. a < X x ) = exp (- a * l)" by (rule exponential_distributedD_gt[OF expX a]) 
+  have gt2[simp]: "\<P>(x in M. a < Y x ) = exp (- a * u)" by (rule exponential_distributedD_gt[OF expY a]) 
+
+  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])
+
+  also have " ... =  \<P>(x in M. a < (X x)) *  \<P>(x in M. a< (Y x) )"
+    using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp
+  also have " ... = exp (- a * (l + u))" by (auto simp:field_simps mult_exp_exp)
+  finally have indep_prob: "\<P>(x in M. a < (min (X x) (Y x)) ) = exp (- a * (l + u))" .
+
+  have "{x \<in> space M. (min (X x) (Y x)) \<le>a } = (space M - {x \<in> space M. a<(min (X x) (Y x)) })"
+    by auto
+  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}"
+    using randX randY by (auto simp: prob_compl) 
+  then show "prob {x \<in> space M. (min (X x) (Y x)) \<le> a} = 1 - exp (- a * (l + u))"
+    using indep_prob by auto
+qed
+ 
+lemma (in prob_space) exponential_distributed_Min:
+  assumes finI: "finite I"
+  assumes A: "I \<noteq> {}"
+  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density (l i))"
+  assumes ind: "indep_vars (\<lambda>i. borel) X I" 
+  shows "distributed M lborel (\<lambda>x. Min ((\<lambda>i. X i x)`I)) (exponential_density (\<Sum>i\<in>I. l i))"
+using assms
+proof (induct rule: finite_ne_induct)
+  case (singleton i) then show ?case by simp
+next
+  case (insert i I)
+  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)))"
+      by (intro exponential_distributed_min indep_vars_Min insert)
+         (auto intro: indep_vars_subset) 
+  then show ?case
+    using insert by simp
+qed
+
+lemma (in prob_space) exponential_distributed_variance:
+  "distributed M lborel X (exponential_density l) \<Longrightarrow> variance X = 1 / l\<^sup>2"
+  using erlang_distributed_variance[OF exponential_distributed_params, of X l X 0] by simp
+
+lemma nn_integral_zero': "AE x in M. f x = 0 \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) = 0"
+  by (simp cong: nn_integral_cong_AE)
+
+lemma convolution_erlang_density:
+  fixes k\<^sub>1 k\<^sub>2 :: nat
+  assumes [simp, arith]: "0 < l"
+  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) =
+    (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
+      (is "?LHS = ?RHS")
+proof
+  fix x :: real
+  have "x \<le> 0 \<or> 0 < x"
+    by arith
+  then show "?LHS x = ?RHS x"
+  proof
+    assume "x \<le> 0" then show ?thesis
+      apply (subst nn_integral_zero')
+      apply (rule AE_I[where N="{0}"])
+      apply (auto simp add: erlang_density_def not_less)
+      done
+  next
+    note zero_le_mult_iff[simp] zero_le_divide_iff[simp]
+  
+    have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l) = 1"
+      using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 0] by (simp del: fact_Suc)
+  
+    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"
+      apply (subst I_eq1[symmetric])
+      unfolding erlang_density_def
+      by (auto intro!: nn_integral_cong split:split_indicator)
+  
+    have "prob_space (density lborel ?LHS)"
+      unfolding times_ereal.simps[symmetric]
+      by (intro prob_space_convolution_density) 
+         (auto intro!: prob_space_erlang_density erlang_density_nonneg)
+    then have 2: "integral\<^sup>N lborel ?LHS = 1"
+      by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density)
+  
+    let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))"
+    let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))"
+    let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1"
+    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)"
+
+    { fix x :: real assume [arith]: "0 < x"
+      have *: "\<And>x y n. (x - y * x::real)^n = x^n * (1 - y)^n"
+        unfolding power_mult_distrib[symmetric] by (simp add: field_simps)
+    
+      have "?LHS x = ?L x"
+        unfolding erlang_density_def
+        by (auto intro!: nn_integral_cong split:split_indicator)
+      also have "... = (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x"
+        apply (subst nn_integral_real_affine[where c=x and t = 0])
+        apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] erlang_density_nonneg del: fact_Suc)
+        apply (intro nn_integral_cong)
+        apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add *
+                    simp del: fact_Suc split: split_indicator)
+        done
+      finally have "(\<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y) * erlang_density k\<^sub>2 l y) \<partial>lborel) = 
+        (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x"
+        by simp }
+    note * = this
+
+    assume [arith]: "0 < x"
+    have 3: "1 = integral\<^sup>N lborel (\<lambda>xa. ?LHS xa * indicator {0<..} xa)"
+      by (subst 2[symmetric])
+         (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"]
+               simp: erlang_density_def  nn_integral_multc[symmetric] indicator_def split: split_if_asm)
+    also have "... = integral\<^sup>N lborel (\<lambda>x. (ereal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))"
+      by (auto intro!: nn_integral_cong simp: * split: split_indicator)
+    also have "... = ereal (?C) * ?I"
+      using 1
+      by (auto simp: nn_integral_nonneg nn_integral_cmult)  
+    finally have " ereal (?C) * ?I = 1" by presburger
+  
+    then show ?thesis
+      using * by simp
+  qed
+qed
+
+lemma (in prob_space) sum_indep_erlang:
+  assumes indep: "indep_var borel X borel Y"
+  assumes [simp, arith]: "0 < l"
+  assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)"
+  assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)"
+  shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
+  using assms
+  apply (subst convolution_erlang_density[symmetric, OF `0<l`])
+  apply (intro distributed_convolution)
+  apply auto
+  done
+
+lemma (in prob_space) erlang_distributed_setsum:
+  assumes finI : "finite I"
+  assumes A: "I \<noteq> {}"
+  assumes [simp, arith]: "0 < l"
+  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (erlang_density (k i) l)"
+  assumes ind: "indep_vars (\<lambda>i. borel) X I"
+  shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((\<Sum>i\<in>I. Suc (k i)) - 1) l)"
+using assms
+proof (induct rule: finite_ne_induct)
+  case (singleton i) then show ?case by auto
+next
+  case (insert i I)
+    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)"
+      by(intro sum_indep_erlang indep_vars_setsum) (auto intro!: indep_vars_subset)
+    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)"
+      using insert by auto
+    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"
+      using insert by (auto intro!: Suc_pred simp: ac_simps)    
+    finally show ?case by fast
+qed
+
+lemma (in prob_space) exponential_distributed_setsum:
+  assumes finI: "finite I"
+  assumes A: "I \<noteq> {}"
+  assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density l)"
+  assumes ind: "indep_vars (\<lambda>i. borel) X I" 
+  shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((card I) - 1) l)"
+proof -
+  obtain i where "i \<in> I" using assms by auto
+  note exponential_distributed_params[OF expX[OF this]]
+  from erlang_distributed_setsum[OF assms(1,2) this assms(3,4)] show ?thesis by simp
+qed
 
 subsection {* Uniform distribution *}
 
@@ -393,4 +740,19 @@
   finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" .
 qed auto
 
+lemma (in prob_space) uniform_distributed_variance:
+  fixes a b :: real
+  assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
+  shows "variance X = (b - a)\<^sup>2 / 12"
+proof (subst distributed_variance)
+  have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
+  let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
+  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)"
+    by (intro integral_cong) (auto split: split_indicator)
+  also have "\<dots> = (b - a)\<^sup>2 / 12"
+    by (simp add: integral_power measure_lebesgue_Icc uniform_distributed_expectation[OF D])
+       (simp add: eval_nat_numeral field_simps )
+  finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
+qed fact
+
 end
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Probability/Independent_Family.thy
     Author:     Johannes Hölzl, TU München
+    Author:     Sudeep Kanav, TU München
 *)
 
 header {* Independent families of events, event sets, and random variables *}
@@ -478,6 +479,107 @@
     by (simp cong: indep_sets_cong)
 qed
 
+lemma (in prob_space) indep_vars_restrict:
+  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"
+  shows "indep_vars (\<lambda>j. PiM (K j) M') (\<lambda>j \<omega>. restrict (\<lambda>i. X i \<omega>) (K j)) L"
+  unfolding indep_vars_def
+proof safe
+  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>)"
+    using K ind by (auto simp: indep_vars_def intro!: measurable_restrict)
+next
+  have X: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> measurable M (M' i)"
+    using ind by (auto simp: indep_vars_def)
+  let ?proj = "\<lambda>j S. {(\<lambda>\<omega>. \<lambda>i\<in>K j. X i \<omega>) -` A \<inter> space M |A. A \<in> S}"
+  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) })"
+  show "indep_sets (\<lambda>i. sigma_sets (space M) (?proj i (sets (Pi\<^sub>M (K i) M')))) L"
+  proof (rule indep_sets_mono_sets)
+    fix j assume j: "j \<in> L"
+    have "sigma_sets (space M) (?proj j (sets (Pi\<^sub>M (K j) M'))) = 
+      sigma_sets (space M) (sigma_sets (space M) (?proj j (prod_algebra (K j) M')))"
+      using j K X[THEN measurable_space] unfolding sets_PiM
+      by (subst sigma_sets_vimage_commute) (auto simp add: Pi_iff)
+    also have "\<dots> = sigma_sets (space M) (?proj j (prod_algebra (K j) M'))"
+      by (rule sigma_sets_sigma_sets_eq) auto
+    also have "\<dots> \<subseteq> ?UN j"
+    proof (rule sigma_sets_mono, safe del: disjE elim!: prod_algebraE)
+      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)"
+      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"
+      proof cases
+        assume "K j = {}" with J show ?thesis
+          by (auto simp add: sigma_sets_empty_eq prod_emb_def)
+      next
+        assume "K j \<noteq> {}" with J have "J \<noteq> {}"
+          by auto
+        { interpret sigma_algebra "space M" "?UN j"
+            by (rule sigma_algebra_sigma_sets) auto 
+          have "\<And>A. (\<And>i. i \<in> J \<Longrightarrow> A i \<in> ?UN j) \<Longrightarrow> INTER J A \<in> ?UN j"
+            using `finite J` `J \<noteq> {}` by (rule finite_INT) blast }
+        note INT = this
+
+        from `J \<noteq> {}` J K E[rule_format, THEN sets.sets_into_space] j
+        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
+          = (\<Inter>i\<in>J. X i -` E i \<inter> space M)"
+          apply (subst prod_emb_PiE[OF _ ])
+          apply auto []
+          apply auto []
+          apply (auto simp add: Pi_iff intro!: X[THEN measurable_space])
+          apply (erule_tac x=i in ballE)
+          apply auto
+          done
+        also have "\<dots> \<in> ?UN j"
+          apply (rule INT)
+          apply (rule sigma_sets.Basic)
+          using `J \<subseteq> K j` E
+          apply auto
+          done
+        finally show ?thesis .
+      qed
+    qed
+    finally show "sigma_sets (space M) (?proj j (sets (Pi\<^sub>M (K j) M'))) \<subseteq> ?UN j" .
+  next
+    show "indep_sets ?UN L"
+    proof (rule indep_sets_collect_sigma)
+      show "indep_sets (\<lambda>i. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) (\<Union>j\<in>L. K j)"
+      proof (rule indep_sets_mono_index)
+        show "indep_sets (\<lambda>i. {X i -` A \<inter> space M |A. A \<in> sets (M' i)}) I"
+          using ind unfolding indep_vars_def2 by auto
+        show "(\<Union>l\<in>L. K l) \<subseteq> I"
+          using K by auto
+      qed
+    next
+      fix l i assume "l \<in> L" "i \<in> K l"
+      show "Int_stable {X i -` A \<inter> space M |A. A \<in> sets (M' i)}"
+        apply (auto simp: Int_stable_def)
+        apply (rule_tac x="A \<inter> Aa" in exI)
+        apply auto
+        done
+    qed fact
+  qed
+qed
+
+lemma (in prob_space) indep_var_restrict:
+  assumes ind: "indep_vars M' X I" and AB: "A \<inter> B = {}" "A \<subseteq> I" "B \<subseteq> I"
+  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)"
+proof -
+  have *:
+    "case_bool (Pi\<^sub>M A M') (Pi\<^sub>M B M') = (\<lambda>b. PiM (case_bool A B b) M')"
+    "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>)"
+    by (simp_all add: fun_eq_iff split: bool.split)
+  show ?thesis
+    unfolding indep_var_def * using AB
+    by (intro indep_vars_restrict[OF ind]) (auto simp: disjoint_family_on_def split: bool.split)
+qed
+
+lemma (in prob_space) indep_vars_subset:
+  assumes "indep_vars M' X I" "J \<subseteq> I"
+  shows "indep_vars M' X J"
+  using assms unfolding indep_vars_def indep_sets_def
+  by auto
+
+lemma (in prob_space) indep_vars_cong:
+  "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"
+  unfolding indep_vars_def2 by (intro conj_cong indep_sets_cong) auto
+
 definition (in prob_space) tail_events where
   "tail_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
 
@@ -801,6 +903,69 @@
   qed
 qed
 
+lemma (in prob_space) indep_var_compose:
+  assumes "indep_var M1 X1 M2 X2" "Y1 \<in> measurable M1 N1" "Y2 \<in> measurable M2 N2"
+  shows "indep_var N1 (Y1 \<circ> X1) N2 (Y2 \<circ> X2)"
+proof -
+  have "indep_vars (case_bool N1 N2) (\<lambda>b. case_bool Y1 Y2 b \<circ> case_bool X1 X2 b) UNIV"
+    using assms
+    by (intro indep_vars_compose[where M'="case_bool M1 M2"])
+       (auto simp: indep_var_def split: bool.split)
+  also have "(\<lambda>b. case_bool Y1 Y2 b \<circ> case_bool X1 X2 b) = case_bool (Y1 \<circ> X1) (Y2 \<circ> X2)"
+    by (simp add: fun_eq_iff split: bool.split)
+  finally show ?thesis
+    unfolding indep_var_def .
+qed
+
+lemma (in prob_space) indep_vars_Min:
+  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
+  shows "indep_var borel (X i) borel (\<lambda>\<omega>. Min ((\<lambda>i. X i \<omega>)`I))"
+proof -
+  have "indep_var
+    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
+    borel ((\<lambda>f. Min (f`I)) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
+    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] borel_measurable_Min) auto
+  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
+    by auto
+  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))"
+    by (auto cong: rev_conj_cong)
+  finally show ?thesis
+    unfolding indep_var_def .
+qed
+
+lemma (in prob_space) indep_vars_setsum:
+  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
+  shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Sum>i\<in>I. X i \<omega>)"
+proof -
+  have "indep_var 
+    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
+    borel ((\<lambda>f. \<Sum>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
+    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] ) auto
+  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
+    by auto
+  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>)"
+    by (auto cong: rev_conj_cong)
+  finally show ?thesis .
+qed
+
+lemma (in prob_space) indep_vars_setprod:
+  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
+  assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
+  shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Prod>i\<in>I. X i \<omega>)"
+proof -
+  have "indep_var 
+    borel ((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i}))
+    borel ((\<lambda>f. \<Prod>i\<in>I. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) I))"
+    using I by (intro indep_var_compose[OF indep_var_restrict[OF indep]] ) auto
+  also have "((\<lambda>f. f i) \<circ> (\<lambda>\<omega>. restrict (\<lambda>i. X i \<omega>) {i})) = X i"
+    by auto
+  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>)"
+    by (auto cong: rev_conj_cong)
+  finally show ?thesis .
+qed
+
 lemma (in prob_space) indep_varsD_finite:
   assumes X: "indep_vars M' X I"
   assumes I: "I \<noteq> {}" "finite I" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M' i)"
@@ -933,6 +1098,20 @@
   finally show ?thesis .
 qed
 
+lemma (in prob_space) prob_indep_random_variable:
+  assumes ind[simp]: "indep_var N X N Y"
+  assumes [simp]: "A \<in> sets N" "B \<in> sets N"
+  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)"
+proof-
+  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)" 
+    by (auto intro!: arg_cong[where f= prob])
+  also have "...=  prob (X -` A \<inter> space M) * prob (Y -` B \<inter> space M)"  
+    by (auto intro!: indep_varD[where Ma=N and Mb=N])     
+  also have "... = \<P>(x in M. X x \<in> A) * \<P>(x in M. Y x \<in> B)"
+    by (auto intro!: arg_cong2[where f= "op *"] arg_cong[where f= prob])
+  finally show ?thesis .
+qed
+
 lemma (in prob_space)
   assumes "indep_var S X T Y"
   shows indep_var_rv1: "random_variable S X"
@@ -1023,4 +1202,115 @@
   using indep_var_distribution_eq[of S X T Y] indep
   by (intro distributed_joint_indep'[OF S T X Y]) auto
 
+lemma (in prob_space) indep_vars_nn_integral:
+  assumes I: "finite I" "indep_vars (\<lambda>_. borel) X I" "\<And>i \<omega>. i \<in> I \<Longrightarrow> 0 \<le> X i \<omega>"
+  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)"
+proof cases
+  assume "I \<noteq> {}"
+  def Y \<equiv> "\<lambda>i \<omega>. if i \<in> I then X i \<omega> else 0"
+  { fix i have "i \<in> I \<Longrightarrow> random_variable borel (X i)"
+    using I(2) by (cases "i\<in>I") (auto simp: indep_vars_def) }
+  note rv_X = this
+
+  { fix i have "random_variable borel (Y i)"
+    using I(2) by (cases "i\<in>I") (auto simp: Y_def rv_X) }
+  note rv_Y = this[measurable]
+    
+  interpret Y: prob_space "distr M borel (Y i)" for i
+    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def)
+  interpret product_sigma_finite "\<lambda>i. distr M borel (Y i)"
+    ..
+  
+  have indep_Y: "indep_vars (\<lambda>i. borel) Y I"
+    by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def)
+
+  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)"
+    using I(3) by (auto intro!: nn_integral_cong setprod_cong simp add: Y_def max_def)
+  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))"
+    by (subst nn_integral_distr) auto
+  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)))"
+    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] ..
+  also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^sup>+\<omega>. max 0 \<omega> \<partial>distr M borel (Y i)))"
+    by (rule product_nn_integral_setprod) (auto intro: `finite I`)
+  also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
+    by (intro setprod_cong nn_integral_cong)
+       (auto simp: nn_integral_distr nn_integral_max_0 Y_def rv_X)
+  finally show ?thesis .
+qed (simp add: emeasure_space_1)
+
+lemma (in prob_space)
+  fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{real_normed_field, banach, second_countable_topology}"
+  assumes I: "finite I" "indep_vars (\<lambda>_. borel) X I" "\<And>i. i \<in> I \<Longrightarrow> integrable M (X i)"
+  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)
+    and indep_vars_integrable: "integrable M (\<lambda>\<omega>. (\<Prod>i\<in>I. X i \<omega>))" (is ?int)
+proof (induct rule: case_split)
+  assume "I \<noteq> {}"
+  def Y \<equiv> "\<lambda>i \<omega>. if i \<in> I then X i \<omega> else 0"
+  { fix i have "i \<in> I \<Longrightarrow> random_variable borel (X i)"
+    using I(2) by (cases "i\<in>I") (auto simp: indep_vars_def) }
+  note rv_X = this[measurable]
+
+  { fix i have "random_variable borel (Y i)"
+    using I(2) by (cases "i\<in>I") (auto simp: Y_def rv_X) }
+  note rv_Y = this[measurable]
+
+  { fix i have "integrable M (Y i)"
+    using I(3) by (cases "i\<in>I") (auto simp: Y_def) }
+  note int_Y = this
+    
+  interpret Y: prob_space "distr M borel (Y i)" for i
+    using I(2) by (cases "i \<in> I") (auto intro!: prob_space_distr simp: Y_def indep_vars_def)
+  interpret product_sigma_finite "\<lambda>i. distr M borel (Y i)"
+    ..
+  
+  have indep_Y: "indep_vars (\<lambda>i. borel) Y I"
+    by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def)
+
+  have "(\<integral>\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<omega>. (\<Prod>i\<in>I. Y i \<omega>) \<partial>M)"
+    using I(3) by (simp add: Y_def)
+  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))"
+    by (subst integral_distr) auto
+  also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
+    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y] ..
+  also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<omega>. \<omega> \<partial>distr M borel (Y i)))"
+    by (rule product_integral_setprod) (auto intro: `finite I` simp: integrable_distr_eq int_Y)
+  also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)"
+    by (intro setprod_cong integral_cong)
+       (auto simp: integral_distr Y_def rv_X)
+  finally show ?eq .
+
+  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))"
+    unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF `I \<noteq> {}` rv_Y indep_Y]
+    by (intro product_integrable_setprod[OF `finite I`])
+       (simp add: integrable_distr_eq int_Y)
+  then show ?int
+    by (simp add: integrable_distr_eq Y_def)
+qed (simp_all add: prob_space)
+
+lemma (in prob_space)
+  fixes X1 X2 :: "'a \<Rightarrow> 'b::{real_normed_field, banach, second_countable_topology}"
+  assumes "indep_var borel X1 borel X2" "integrable M X1" "integrable M X2"
+  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)
+    and indep_var_integrable: "integrable M (\<lambda>\<omega>. X1 \<omega> * X2 \<omega>)" (is ?int)
+unfolding indep_var_def
+proof -
+  have *: "(\<lambda>\<omega>. X1 \<omega> * X2 \<omega>) = (\<lambda>\<omega>. \<Prod>i\<in>UNIV. (case_bool X1 X2 i \<omega>))"
+    by (simp add: UNIV_bool mult_commute)
+  have **: "(\<lambda> _. borel) = case_bool borel borel"
+    by (rule ext, metis (full_types) bool.simps(3) bool.simps(4))
+  show ?eq
+    apply (subst *)
+    apply (subst indep_vars_lebesgue_integral)
+    apply (auto)
+    apply (subst **, subst indep_var_def [symmetric], rule assms)
+    apply (simp split: bool.split add: assms)
+    by (simp add: UNIV_bool mult_commute)
+  show ?int
+    apply (subst *)
+    apply (rule indep_vars_integrable)
+    apply auto
+    apply (subst **, subst indep_var_def [symmetric], rule assms)
+    by (simp split: bool.split add: assms)
+qed
+
 end
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -8,7 +8,7 @@
 theory Information
 imports
   Independent_Family
-  Radon_Nikodym
+  Distributions
   "~~/src/HOL/Library/Convex"
 begin
 
@@ -400,27 +400,6 @@
     done
 qed
 
-lemma distributed_integrable:
-  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
-    integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
-  by (auto simp: distributed_real_AE
-                    distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq)
-  
-lemma distributed_transform_integrable:
-  assumes Px: "distributed M N X Px"
-  assumes "distributed M P Y Py"
-  assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
-  shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
-proof -
-  have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))"
-    by (rule distributed_integrable) fact+
-  also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))"
-    using Y by simp
-  also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
-    using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
-  finally show ?thesis .
-qed
-
 lemma integrable_cong_AE_imp:
   "integrable M g \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (AE x in M. g x = f x) \<Longrightarrow> integrable M f"
   using integrable_cong_AE[of f M g] by (auto simp: eq_commute)
@@ -937,6 +916,35 @@
     by (subst integral_mult_right) (auto simp: measure_def)
 qed
 
+lemma (in information_space) entropy_exponential:
+  assumes D: "distributed M lborel X (exponential_density l)"
+  shows "entropy b lborel X = log b (exp 1 / l)"
+proof -
+  have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D])
+ 
+  have [simp]: "integrable lborel (exponential_density l)"
+    using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp
+
+  have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1"
+    using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space)
+    
+  have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)"
+    using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp
+
+  have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l"
+    using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp
+    
+  have "entropy b lborel X = - (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)"
+    using D by (rule entropy_distr)
+  also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 
+    (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
+    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
+  also have "\<dots> = (ln l - 1) / ln b"
+    by simp
+  finally show ?thesis
+    by (simp add: log_def divide_simps ln_div)
+qed
+
 lemma (in information_space) entropy_simple_distributed:
   "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
   by (subst entropy_distr[OF simple_distributed])
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -516,6 +516,8 @@
     by (intro exI[of _ A]) (auto simp: subset_eq)
 qed
 
+interpretation lborel_pair: pair_sigma_finite lborel lborel ..
+
 lemma Int_stable_atLeastAtMost:
   fixes x::"'a::ordered_euclidean_space"
   shows "Int_stable (range (\<lambda>(a, b::'a). {a..b}))"
@@ -1226,4 +1228,64 @@
   finally show ?thesis .
 qed
 
+subsection {* Integration by parts *}
+
+lemma integral_by_parts_integrable:
+  fixes f g F G::"real \<Rightarrow> real"
+  assumes "a \<le> b"
+  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+  assumes [intro]: "!!x. DERIV F x :> f x"
+  assumes [intro]: "!!x. DERIV G x :> g x"
+  shows  "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
+  by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)
+
+lemma integral_by_parts:
+  fixes f g F G::"real \<Rightarrow> real"
+  assumes [arith]: "a \<le> b"
+  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+  assumes [intro]: "!!x. DERIV F x :> f x"
+  assumes [intro]: "!!x. DERIV G x :> g x"
+  shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
+            =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" 
+proof-
+  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"
+    by (rule integral_FTC_atLeastAtMost, auto intro!: derivative_eq_intros continuous_intros) 
+      (auto intro!: DERIV_isCont)
+
+  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
+    (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
+    apply (subst integral_add[symmetric])
+    apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
+    by (auto intro!: DERIV_isCont integral_cong split:split_indicator)
+
+  thus ?thesis using 0 by auto
+qed
+
+lemma integral_by_parts':
+  fixes f g F G::"real \<Rightarrow> real"
+  assumes "a \<le> b"
+  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+  assumes "!!x. DERIV F x :> f x"
+  assumes "!!x. DERIV G x :> g x"
+  shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
+            =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" 
+  using integral_by_parts[OF assms] by (simp add: mult_ac)
+
+lemma integral_tendsto_at_top:
+  fixes f :: "real \<Rightarrow> real"
+  assumes [simp, intro]: "\<And>x. isCont f x"
+  assumes [simp, arith]: "\<And>x. 0 \<le> f x"
+  assumes [simp]: "integrable lborel f"
+  assumes [measurable]: "f \<in> borel_measurable borel"
+  shows "((\<lambda>x. \<integral>xa. f xa * indicator {0..x} xa \<partial>lborel) ---> \<integral>xa. f xa * indicator {0..} xa \<partial>lborel) at_top"
+  apply (auto intro!: borel_integrable_atLeastAtMost monoI integral_mono tendsto_at_topI_sequentially  
+    split:split_indicator)
+  apply (rule integral_dominated_convergence[where w = " \<lambda>x. f x * indicator {0..} x"])
+  unfolding LIMSEQ_def  
+  apply (auto intro!: AE_I2 tendsto_mult integrable_mult_indicator split: split_indicator)
+  by (metis ge_natfloor_plus_one_imp_gt less_imp_le)
+
 end
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -1187,6 +1187,7 @@
   by (auto simp add: emeasure_distr measurable_space
            intro!: arg_cong[where f="emeasure M"] measure_eqI)
 
+
 subsection {* Real measure values *}
 
 lemma measure_nonneg: "0 \<le> measure M A"
@@ -1526,6 +1527,14 @@
   assumes "measure M A = measure M (space M)" "A \<inter> B = {}"
   shows "measure M B = 0"
   using measure_space_inter[of B A] assms by (auto simp: ac_simps)
+lemma (in finite_measure) finite_measure_distr:
+  assumes f: "f \<in> measurable M M'" 
+  shows "finite_measure (distr M M' f)"
+proof (rule finite_measureI)
+  have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space)
+  with f show "emeasure (distr M M' f) (space (distr M M' f)) \<noteq> \<infinity>" by (auto simp: emeasure_distr)
+qed
+
 
 subsection {* Counting space *}
 
diff -r 596a499318ab -r b0b9a10e4bf4 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Wed Jun 11 13:39:38 2014 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Thu Jun 12 15:47:36 2014 +0200
@@ -27,6 +27,7 @@
 abbreviation (in prob_space) "prob \<equiv> measure M"
 abbreviation (in prob_space) "random_variable M' X \<equiv> X \<in> measurable M M'"
 abbreviation (in prob_space) "expectation \<equiv> integral\<^sup>L M"
+abbreviation (in prob_space) "variance X \<equiv> integral\<^sup>L M (\<lambda>x. (X x - expectation X)\<^sup>2)"
 
 lemma (in prob_space) prob_space_distr:
   assumes f: "f \<in> measurable M M'" shows "prob_space (distr M M' f)"
@@ -333,6 +334,16 @@
     \<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"
   by (auto simp: emeasure_distr measurable_pair_iff comp_def intro!: emeasure_mono measurable_sets)
 
+lemma (in prob_space) variance_eq:
+  fixes X :: "'a \<Rightarrow> real"
+  assumes [simp]: "integrable M X"
+  assumes [simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)"
+  shows "variance X = expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2"
+  by (simp add: field_simps prob_space power2_diff power2_eq_square[symmetric])
+
+lemma (in prob_space) variance_positive: "0 \<le> variance (X::'a \<Rightarrow> real)"
+  by (intro integral_nonneg_AE) (auto intro!: integral_nonneg_AE)
+
 locale pair_prob_space = pair_sigma_finite M1 M2 + M1: prob_space M1 + M2: prob_space M2 for M1 M2
 
 sublocale pair_prob_space \<subseteq> P: prob_space "M1 \<Otimes>\<^sub>M M2"
@@ -713,6 +724,47 @@
     done
 qed
 
+lemma distributed_integrable:
+  "distributed M N X f \<Longrightarrow> g \<in> borel_measurable N \<Longrightarrow>
+    integrable N (\<lambda>x. f x * g x) \<longleftrightarrow> integrable M (\<lambda>x. g (X x))"
+  by (auto simp: distributed_real_AE
+                    distributed_distr_eq_density[symmetric] integrable_real_density[symmetric] integrable_distr_eq)
+  
+lemma distributed_transform_integrable:
+  assumes Px: "distributed M N X Px"
+  assumes "distributed M P Y Py"
+  assumes Y: "Y = (\<lambda>x. T (X x))" and T: "T \<in> measurable N P" and f: "f \<in> borel_measurable P"
+  shows "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
+proof -
+  have "integrable P (\<lambda>x. Py x * f x) \<longleftrightarrow> integrable M (\<lambda>x. f (Y x))"
+    by (rule distributed_integrable) fact+
+  also have "\<dots> \<longleftrightarrow> integrable M (\<lambda>x. f (T (X x)))"
+    using Y by simp
+  also have "\<dots> \<longleftrightarrow> integrable N (\<lambda>x. Px x * f (T x))"
+    using measurable_comp[OF T f] Px by (intro distributed_integrable[symmetric]) (auto simp: comp_def)
+  finally show ?thesis .
+qed
+
+lemma (in prob_space) distributed_variance:
+  fixes f::"real \<Rightarrow> real"
+  assumes D: "distributed M lborel X f"
+  shows "variance X = (\<integral>x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)"
+proof (subst distributed_integral[OF D, symmetric])
+  show "(\<integral> x. f x * (x - expectation X)\<^sup>2 \<partial>lborel) = (\<integral> x. x\<^sup>2 * f (x + expectation X) \<partial>lborel)"
+    by (subst lborel_integral_real_affine[where c=1 and t="expectation X"])  (auto simp: ac_simps)
+qed simp
+
+lemma (in prob_space) variance_affine:
+  fixes f::"real \<Rightarrow> real"
+  assumes [arith]: "b \<noteq> 0"
+  assumes D[intro]: "distributed M lborel X f"
+  assumes [simp]: "prob_space (density lborel f)"
+  assumes I[simp]: "integrable M X"
+  assumes I2[simp]: "integrable M (\<lambda>x. (X x)\<^sup>2)" 
+  shows "variance (\<lambda>x. a + b * X x) = b\<^sup>2 * variance X"
+  by (subst variance_eq)
+     (auto simp: power2_sum power_mult_distrib prob_space variance_eq right_diff_distrib)
+
 definition
   "simple_distributed M X f \<longleftrightarrow> distributed M (count_space (X`space M)) X (\<lambda>x. ereal (f x)) \<and>
     finite (X`space M)"