properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
--- 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.
--- 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
--- 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)))"
--- 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)]:
--- /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
--- 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
--- 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
--- 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])
--- 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
--- 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 *}
--- 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)"