move theorems to be more generally useable
authorhoelzl
Fri Nov 16 18:45:57 2012 +0100 (2012-11-16)
changeset 50104de19856feb54
parent 50103 3d89c38408cd
child 50105 65d5b18e1626
move theorems to be more generally useable
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FuncSet.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Nov 16 18:49:46 2012 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Nov 16 18:45:57 2012 +0100
     1.3 @@ -124,7 +124,6 @@
     1.4    fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto
     1.5  qed auto
     1.6  
     1.7 -
     1.8  instantiation ereal :: abs
     1.9  begin
    1.10    function abs_ereal where
    1.11 @@ -145,6 +144,9 @@
    1.12  lemma abs_ereal_uminus[simp]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"
    1.13    by (cases x) auto
    1.14  
    1.15 +lemma ereal_infinity_cases: "(a::ereal) \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
    1.16 +  by auto
    1.17 +
    1.18  subsubsection "Addition"
    1.19  
    1.20  instantiation ereal :: comm_monoid_add
    1.21 @@ -530,6 +532,9 @@
    1.22  qed
    1.23  end
    1.24  
    1.25 +lemma real_ereal_1[simp]: "real (1::ereal) = 1"
    1.26 +  unfolding one_ereal_def by simp
    1.27 +
    1.28  lemma real_of_ereal_le_1:
    1.29    fixes a :: ereal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
    1.30    by (cases a) (auto simp: one_ereal_def)
    1.31 @@ -659,6 +664,16 @@
    1.32    shows "0 < a * b \<longleftrightarrow> (0 < a \<and> 0 < b) \<or> (a < 0 \<and> b < 0)"
    1.33    by (cases rule: ereal2_cases[of a b]) (simp_all add: zero_less_mult_iff)
    1.34  
    1.35 +lemma ereal_left_mult_cong:
    1.36 +  fixes a b c :: ereal
    1.37 +  shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> c * a = c * b"
    1.38 +  by (cases "c = 0") simp_all
    1.39 +
    1.40 +lemma ereal_right_mult_cong:
    1.41 +  fixes a b c :: ereal
    1.42 +  shows "(c \<noteq> 0 \<Longrightarrow> a = b) \<Longrightarrow> a * c = b * c"
    1.43 +  by (cases "c = 0") simp_all
    1.44 +
    1.45  lemma ereal_distrib:
    1.46    fixes a b c :: ereal
    1.47    assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>"
    1.48 @@ -941,6 +956,10 @@
    1.49  using assms apply (cases x, cases e) apply auto
    1.50  done
    1.51  
    1.52 +lemma ereal_minus_eq_PInfty_iff:
    1.53 +  fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
    1.54 +  by (cases x y rule: ereal2_cases) simp_all
    1.55 +
    1.56  subsubsection {* Division *}
    1.57  
    1.58  instantiation ereal :: inverse
     2.1 --- a/src/HOL/Library/FuncSet.thy	Fri Nov 16 18:49:46 2012 +0100
     2.2 +++ b/src/HOL/Library/FuncSet.thy	Fri Nov 16 18:45:57 2012 +0100
     2.3 @@ -81,7 +81,10 @@
     2.4    by (simp add: Pi_def)
     2.5  
     2.6  lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
     2.7 -by auto
     2.8 +  by auto
     2.9 +
    2.10 +lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
    2.11 +  by auto
    2.12  
    2.13  lemma Pi_eq_empty[simp]: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
    2.14  apply (simp add: Pi_def, auto)
     3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 16 18:49:46 2012 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Nov 16 18:45:57 2012 +0100
     3.3 @@ -5914,4 +5914,71 @@
     3.4  } ultimately show ?thesis by blast
     3.5  qed
     3.6  
     3.7 +
     3.8 +lemma convex_le_Inf_differential:
     3.9 +  fixes f :: "real \<Rightarrow> real"
    3.10 +  assumes "convex_on I f"
    3.11 +  assumes "x \<in> interior I" "y \<in> I"
    3.12 +  shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
    3.13 +    (is "_ \<ge> _ + Inf (?F x) * (y - x)")
    3.14 +proof (cases rule: linorder_cases)
    3.15 +  assume "x < y"
    3.16 +  moreover
    3.17 +  have "open (interior I)" by auto
    3.18 +  from openE[OF this `x \<in> interior I`] guess e . note e = this
    3.19 +  moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
    3.20 +  ultimately have "x < t" "t < y" "t \<in> ball x e"
    3.21 +    by (auto simp: dist_real_def field_simps split: split_min)
    3.22 +  with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
    3.23 +
    3.24 +  have "open (interior I)" by auto
    3.25 +  from openE[OF this `x \<in> interior I`] guess e .
    3.26 +  moreover def K \<equiv> "x - e / 2"
    3.27 +  with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)
    3.28 +  ultimately have "K \<in> I" "K < x" "x \<in> I"
    3.29 +    using interior_subset[of I] `x \<in> interior I` by auto
    3.30 +
    3.31 +  have "Inf (?F x) \<le> (f x - f y) / (x - y)"
    3.32 +  proof (rule Inf_lower2)
    3.33 +    show "(f x - f t) / (x - t) \<in> ?F x"
    3.34 +      using `t \<in> I` `x < t` by auto
    3.35 +    show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
    3.36 +      using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
    3.37 +  next
    3.38 +    fix y assume "y \<in> ?F x"
    3.39 +    with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
    3.40 +    show "(f K - f x) / (K - x) \<le> y" by auto
    3.41 +  qed
    3.42 +  then show ?thesis
    3.43 +    using `x < y` by (simp add: field_simps)
    3.44 +next
    3.45 +  assume "y < x"
    3.46 +  moreover
    3.47 +  have "open (interior I)" by auto
    3.48 +  from openE[OF this `x \<in> interior I`] guess e . note e = this
    3.49 +  moreover def t \<equiv> "x + e / 2"
    3.50 +  ultimately have "x < t" "t \<in> ball x e"
    3.51 +    by (auto simp: dist_real_def field_simps)
    3.52 +  with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
    3.53 +
    3.54 +  have "(f x - f y) / (x - y) \<le> Inf (?F x)"
    3.55 +  proof (rule Inf_greatest)
    3.56 +    have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
    3.57 +      using `y < x` by (auto simp: field_simps)
    3.58 +    also
    3.59 +    fix z  assume "z \<in> ?F x"
    3.60 +    with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
    3.61 +    have "(f y - f x) / (y - x) \<le> z" by auto
    3.62 +    finally show "(f x - f y) / (x - y) \<le> z" .
    3.63 +  next
    3.64 +    have "open (interior I)" by auto
    3.65 +    from openE[OF this `x \<in> interior I`] guess e . note e = this
    3.66 +    then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)
    3.67 +    with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
    3.68 +    then show "?F x \<noteq> {}" by blast
    3.69 +  qed
    3.70 +  then show ?thesis
    3.71 +    using `y < x` by (simp add: field_simps)
    3.72 +qed simp
    3.73 +
    3.74  end
     4.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Nov 16 18:49:46 2012 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Nov 16 18:45:57 2012 +0100
     4.3 @@ -423,6 +423,11 @@
     4.4    using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
     4.5       ereal_Liminf_uminus[of net f] assms by simp
     4.6  
     4.7 +lemma convergent_ereal_limsup:
     4.8 +  fixes X :: "nat \<Rightarrow> ereal"
     4.9 +  shows "convergent X \<Longrightarrow> limsup X = lim X"
    4.10 +  by (auto simp: convergent_def limI lim_imp_Limsup)
    4.11 +
    4.12  lemma Liminf_PInfty:
    4.13    fixes f :: "'a \<Rightarrow> ereal"
    4.14    assumes "\<not> trivial_limit net"
    4.15 @@ -486,6 +491,12 @@
    4.16    shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
    4.17    by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
    4.18  
    4.19 +lemma convergent_ereal:
    4.20 +  fixes X :: "nat \<Rightarrow> ereal"
    4.21 +  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
    4.22 +  using ereal_Liminf_eq_Limsup_iff[of sequentially]
    4.23 +  by (auto simp: convergent_def)
    4.24 +
    4.25  lemma limsup_INFI_SUPR:
    4.26    fixes f :: "nat \<Rightarrow> ereal"
    4.27    shows "limsup f = (INF n. SUP m:{n..}. f m)"
    4.28 @@ -1496,4 +1507,20 @@
    4.29      by induct (simp_all add: suminf_add_ereal setsum_nonneg)
    4.30  qed simp
    4.31  
    4.32 +lemma suminf_ereal_eq_0:
    4.33 +  fixes f :: "nat \<Rightarrow> ereal"
    4.34 +  assumes nneg: "\<And>i. 0 \<le> f i"
    4.35 +  shows "(\<Sum>i. f i) = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
    4.36 +proof
    4.37 +  assume "(\<Sum>i. f i) = 0"
    4.38 +  { fix i assume "f i \<noteq> 0"
    4.39 +    with nneg have "0 < f i" by (auto simp: less_le)
    4.40 +    also have "f i = (\<Sum>j. if j = i then f i else 0)"
    4.41 +      by (subst suminf_finite[where N="{i}"]) auto
    4.42 +    also have "\<dots> \<le> (\<Sum>i. f i)"
    4.43 +      using nneg by (auto intro!: suminf_le_pos)
    4.44 +    finally have False using `(\<Sum>i. f i) = 0` by auto }
    4.45 +  then show "\<forall>i. f i = 0" by auto
    4.46 +qed simp
    4.47 +
    4.48  end
     5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 16 18:49:46 2012 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Nov 16 18:45:57 2012 +0100
     5.3 @@ -483,6 +483,13 @@
     5.4    show ?thesis unfolding content_def using assms by (auto simp: *)
     5.5  qed
     5.6  
     5.7 +lemma content_singleton[simp]: "content {a} = 0"
     5.8 +proof -
     5.9 +  have "content {a .. a} = 0"
    5.10 +    by (subst content_closed_interval) auto
    5.11 +  then show ?thesis by simp
    5.12 +qed
    5.13 +
    5.14  lemma content_unit[intro]: "content{0..One::'a::ordered_euclidean_space} = 1"
    5.15  proof -
    5.16    have *: "\<forall>i<DIM('a). (0::'a)$$i \<le> (One::'a)$$i" by auto
    5.17 @@ -1665,6 +1672,16 @@
    5.18    unfolding o_def[THEN sym] apply(rule has_integral_linear,assumption)
    5.19    by(rule bounded_linear_scaleR_right)
    5.20  
    5.21 +lemma has_integral_cmult_real:
    5.22 +  fixes c :: real
    5.23 +  assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
    5.24 +  shows "((\<lambda>x. c * f x) has_integral c * x) A"
    5.25 +proof cases
    5.26 +  assume "c \<noteq> 0"
    5.27 +  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
    5.28 +    unfolding real_scaleR_def .
    5.29 +qed simp
    5.30 +
    5.31  lemma has_integral_neg:
    5.32    shows "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
    5.33    apply(drule_tac c="-1" in has_integral_cmul) by auto
    5.34 @@ -1746,6 +1763,12 @@
    5.35    shows "f integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) integrable_on s"
    5.36    unfolding integrable_on_def by(auto intro: has_integral_cmul)
    5.37  
    5.38 +lemma integrable_on_cmult_iff:
    5.39 +  fixes c :: real assumes "c \<noteq> 0"
    5.40 +  shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
    5.41 +  using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
    5.42 +  by auto
    5.43 +
    5.44  lemma integrable_neg:
    5.45    shows "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
    5.46    unfolding integrable_on_def by(auto intro: has_integral_neg)
    5.47 @@ -2669,6 +2692,11 @@
    5.48    unfolding split_def apply(subst scaleR_left.setsum[THEN sym, unfolded o_def])
    5.49    defer apply(subst additive_content_tagged_division[unfolded split_def]) apply assumption by auto
    5.50  
    5.51 +lemma integral_const[simp]:
    5.52 +  fixes a b :: "'a::ordered_euclidean_space"
    5.53 +  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
    5.54 +  by (rule integral_unique) (rule has_integral_const)
    5.55 +
    5.56  subsection {* Bounds on the norm of Riemann sums and the integral itself. *}
    5.57  
    5.58  lemma dsum_bound: assumes "p division_of {a..b}" "norm(c) \<le> e"
     6.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 16 18:49:46 2012 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 16 18:45:57 2012 +0100
     6.3 @@ -2891,6 +2891,10 @@
     6.4    by (fast intro: less_trans, fast intro: le_less_trans,
     6.5      fast intro: order_trans)
     6.6  
     6.7 +lemma atLeastAtMost_singleton_euclidean[simp]:
     6.8 +  fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}"
     6.9 +  by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a])
    6.10 +
    6.11  lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
    6.12  
    6.13  instance real::ordered_euclidean_space
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 18:49:46 2012 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 18:45:57 2012 +0100
     7.3 @@ -2044,6 +2044,10 @@
     7.4  unfolding bounded_any_center [where a=0]
     7.5  by (simp add: dist_norm)
     7.6  
     7.7 +lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
     7.8 +  unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
     7.9 +  using assms by auto
    7.10 +
    7.11  lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
    7.12  lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
    7.13    by (metis bounded_def subset_eq)
     8.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
     8.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
     8.3 @@ -8,24 +8,12 @@
     8.4  imports Lebesgue_Integration
     8.5  begin
     8.6  
     8.7 -lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
     8.8 -  by auto
     8.9 -
    8.10 -lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
    8.11 -  by auto
    8.12 -
    8.13 -lemma Pair_vimage_times[simp]: "\<And>A B x. Pair x -` (A \<times> B) = (if x \<in> A then B else {})"
    8.14 +lemma Pair_vimage_times[simp]: "Pair x -` (A \<times> B) = (if x \<in> A then B else {})"
    8.15    by auto
    8.16  
    8.17 -lemma rev_Pair_vimage_times[simp]: "\<And>A B y. (\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
    8.18 +lemma rev_Pair_vimage_times[simp]: "(\<lambda>x. (x, y)) -` (A \<times> B) = (if y \<in> B then A else {})"
    8.19    by auto
    8.20  
    8.21 -lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
    8.22 -  by (cases x) simp
    8.23 -
    8.24 -lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
    8.25 -  by (auto simp: fun_eq_iff)
    8.26 -
    8.27  section "Binary products"
    8.28  
    8.29  definition pair_measure (infixr "\<Otimes>\<^isub>M" 80) where
    8.30 @@ -787,4 +775,39 @@
    8.31               intro!: positive_integral_cong arg_cong[where f="emeasure N"])
    8.32  qed simp
    8.33  
    8.34 +lemma pair_measure_eqI:
    8.35 +  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
    8.36 +  assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M"
    8.37 +  assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)"
    8.38 +  shows "M1 \<Otimes>\<^isub>M M2 = M"
    8.39 +proof -
    8.40 +  interpret M1: sigma_finite_measure M1 by fact
    8.41 +  interpret M2: sigma_finite_measure M2 by fact
    8.42 +  interpret pair_sigma_finite M1 M2 by default
    8.43 +  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
    8.44 +  let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
    8.45 +  let ?P = "M1 \<Otimes>\<^isub>M M2"
    8.46 +  show ?thesis
    8.47 +  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
    8.48 +    show "?E \<subseteq> Pow (space ?P)"
    8.49 +      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
    8.50 +    show "sets ?P = sigma_sets (space ?P) ?E"
    8.51 +      by (simp add: sets_pair_measure space_pair_measure)
    8.52 +    then show "sets M = sigma_sets (space ?P) ?E"
    8.53 +      using sets[symmetric] by simp
    8.54 +  next
    8.55 +    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
    8.56 +      using F by (auto simp: space_pair_measure)
    8.57 +  next
    8.58 +    fix X assume "X \<in> ?E"
    8.59 +    then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
    8.60 +    then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
    8.61 +       by (simp add: M2.emeasure_pair_measure_Times)
    8.62 +    also have "\<dots> = emeasure M (A \<times> B)"
    8.63 +      using A B emeasure by auto
    8.64 +    finally show "emeasure ?P X = emeasure M X"
    8.65 +      by simp
    8.66 +  qed
    8.67 +qed
    8.68 +
    8.69  end
    8.70 \ No newline at end of file
     9.1 --- a/src/HOL/Probability/Borel_Space.thy	Fri Nov 16 18:49:46 2012 +0100
     9.2 +++ b/src/HOL/Probability/Borel_Space.thy	Fri Nov 16 18:45:57 2012 +0100
     9.3 @@ -1114,21 +1114,10 @@
     9.4      and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
     9.5    unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
     9.6  
     9.7 -lemma sets_Collect_eventually_sequientially[measurable]:
     9.8 +lemma sets_Collect_eventually_sequentially[measurable]:
     9.9    "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
    9.10    unfolding eventually_sequentially by simp
    9.11  
    9.12 -lemma convergent_ereal:
    9.13 -  fixes X :: "nat \<Rightarrow> ereal"
    9.14 -  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
    9.15 -  using ereal_Liminf_eq_Limsup_iff[of sequentially]
    9.16 -  by (auto simp: convergent_def)
    9.17 -
    9.18 -lemma convergent_ereal_limsup:
    9.19 -  fixes X :: "nat \<Rightarrow> ereal"
    9.20 -  shows "convergent X \<Longrightarrow> limsup X = lim X"
    9.21 -  by (auto simp: convergent_def limI lim_imp_Limsup)
    9.22 -
    9.23  lemma sets_Collect_ereal_convergent[measurable]: 
    9.24    fixes f :: "nat \<Rightarrow> 'a => ereal"
    9.25    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
    10.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
    10.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
    10.3 @@ -262,6 +262,47 @@
    10.4      using Pi_eq_empty_iff[of I F] Pi_eq_empty_iff[of I F'] by auto
    10.5  qed
    10.6  
    10.7 +lemma funset_eq_UN_fun_upd_I:
    10.8 +  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
    10.9 +  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
   10.10 +  and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
   10.11 +  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
   10.12 +proof safe
   10.13 +  fix f assume f: "f \<in> F (insert a A)"
   10.14 +  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
   10.15 +  proof (rule UN_I[of "f(a := d)"])
   10.16 +    show "f(a := d) \<in> F A" using *[OF f] .
   10.17 +    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
   10.18 +    proof (rule image_eqI[of _ _ "f a"])
   10.19 +      show "f a \<in> G (f(a := d))" using **[OF f] .
   10.20 +    qed simp
   10.21 +  qed
   10.22 +next
   10.23 +  fix f x assume "f \<in> F A" "x \<in> G f"
   10.24 +  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
   10.25 +qed
   10.26 +
   10.27 +lemma extensional_funcset_insert_eq[simp]:
   10.28 +  assumes "a \<notin> A"
   10.29 +  shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
   10.30 +  apply (rule funset_eq_UN_fun_upd_I)
   10.31 +  using assms
   10.32 +  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
   10.33 +
   10.34 +lemma finite_extensional_funcset[simp, intro]:
   10.35 +  assumes "finite A" "finite B"
   10.36 +  shows "finite (extensional A \<inter> (A \<rightarrow> B))"
   10.37 +  using assms by induct auto
   10.38 +
   10.39 +lemma finite_PiE[simp, intro]:
   10.40 +  assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
   10.41 +  shows "finite (Pi\<^isub>E A B)"
   10.42 +proof -
   10.43 +  have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
   10.44 +  show ?thesis
   10.45 +    using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
   10.46 +qed
   10.47 +
   10.48  section "Finite product spaces"
   10.49  
   10.50  section "Products"
   10.51 @@ -441,6 +482,31 @@
   10.52      done
   10.53  qed
   10.54  
   10.55 +lemma prod_algebra_cong:
   10.56 +  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
   10.57 +  shows "prod_algebra I M = prod_algebra J N"
   10.58 +proof -
   10.59 +  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
   10.60 +    using sets_eq_imp_space_eq[OF sets] by auto
   10.61 +  with sets show ?thesis unfolding `I = J`
   10.62 +    by (intro antisym prod_algebra_mono) auto
   10.63 +qed
   10.64 +
   10.65 +lemma space_in_prod_algebra:
   10.66 +  "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
   10.67 +proof cases
   10.68 +  assume "I = {}" then show ?thesis
   10.69 +    by (auto simp add: prod_algebra_def image_iff prod_emb_def)
   10.70 +next
   10.71 +  assume "I \<noteq> {}"
   10.72 +  then obtain i where "i \<in> I" by auto
   10.73 +  then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))"
   10.74 +    by (auto simp: prod_emb_def Pi_iff)
   10.75 +  also have "\<dots> \<in> prod_algebra I M"
   10.76 +    using `i \<in> I` by (intro prod_algebraI) auto
   10.77 +  finally show ?thesis .
   10.78 +qed
   10.79 +
   10.80  lemma space_PiM: "space (\<Pi>\<^isub>M i\<in>I. M i) = (\<Pi>\<^isub>E i\<in>I. space (M i))"
   10.81    using prod_algebra_sets_into_space unfolding PiM_def prod_algebra_def by (intro space_extend_measure) simp
   10.82  
   10.83 @@ -1007,6 +1073,23 @@
   10.84    show ?thesis
   10.85      unfolding lebesgue_integral_def *[THEN product_positive_integral_singleton] ..
   10.86  qed
   10.87 +lemma (in product_sigma_finite) distr_component:
   10.88 +  "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
   10.89 +proof (intro measure_eqI[symmetric])
   10.90 +  interpret I: finite_product_sigma_finite M "{i}" by default simp
   10.91 +
   10.92 +  have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
   10.93 +    by (auto simp: extensional_def restrict_def)
   10.94 +
   10.95 +  fix A assume A: "A \<in> sets ?P"
   10.96 +  then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)" 
   10.97 +    by simp
   10.98 +  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)" 
   10.99 +    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
  10.100 +  also have "\<dots> = emeasure ?D A"
  10.101 +    using A by (simp add: product_positive_integral_singleton emeasure_distr)
  10.102 +  finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
  10.103 +qed simp
  10.104  
  10.105  lemma (in product_sigma_finite) product_integral_fold:
  10.106    assumes IJ[simp]: "I \<inter> J = {}" and fin: "finite I" "finite J"
  10.107 @@ -1250,4 +1333,31 @@
  10.108      by (auto intro!: sigma_sets_subset sets_PiM_I_finite simp: E_generates P_def)
  10.109  qed
  10.110  
  10.111 +lemma pair_measure_eq_distr_PiM:
  10.112 +  fixes M1 :: "'a measure" and M2 :: "'a measure"
  10.113 +  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
  10.114 +  shows "(M1 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>x. (x True, x False))"
  10.115 +    (is "?P = ?D")
  10.116 +proof (rule pair_measure_eqI[OF assms])
  10.117 +  interpret B: product_sigma_finite "bool_case M1 M2"
  10.118 +    unfolding product_sigma_finite_def using assms by (auto split: bool.split)
  10.119 +  let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)"
  10.120 +
  10.121 +  have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
  10.122 +    by auto
  10.123 +  fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
  10.124 +  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
  10.125 +    by (simp add: UNIV_bool ac_simps)
  10.126 +  also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
  10.127 +    using A B by (subst B.emeasure_PiM) (auto split: bool.split)
  10.128 +  also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
  10.129 +    using A[THEN sets_into_space] B[THEN sets_into_space]
  10.130 +    by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split)
  10.131 +  finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
  10.132 +    using A B
  10.133 +      measurable_component_singleton[of True UNIV "bool_case M1 M2"]
  10.134 +      measurable_component_singleton[of False UNIV "bool_case M1 M2"]
  10.135 +    by (subst emeasure_distr) (auto simp: measurable_pair_iff)
  10.136 +qed simp
  10.137 +
  10.138  end
    11.1 --- a/src/HOL/Probability/Independent_Family.thy	Fri Nov 16 18:49:46 2012 +0100
    11.2 +++ b/src/HOL/Probability/Independent_Family.thy	Fri Nov 16 18:45:57 2012 +0100
    11.3 @@ -18,9 +18,6 @@
    11.4  definition (in prob_space)
    11.5    indep_events_def_alt: "indep_events A I \<longleftrightarrow> indep_sets (\<lambda>i. {A i}) I"
    11.6  
    11.7 -lemma image_subset_iff_funcset: "F ` A \<subseteq> B \<longleftrightarrow> F \<in> A \<rightarrow> B"
    11.8 -  by auto
    11.9 -
   11.10  lemma (in prob_space) indep_events_def:
   11.11    "indep_events A I \<longleftrightarrow> (A`I \<subseteq> events) \<and>
   11.12      (\<forall>J\<subseteq>I. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j)))"
   11.13 @@ -827,31 +824,6 @@
   11.14      using I by auto
   11.15  qed fact+
   11.16  
   11.17 -lemma prod_algebra_cong:
   11.18 -  assumes "I = J" and sets: "(\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i))"
   11.19 -  shows "prod_algebra I M = prod_algebra J N"
   11.20 -proof -
   11.21 -  have space: "\<And>i. i \<in> I \<Longrightarrow> space (M i) = space (N i)"
   11.22 -    using sets_eq_imp_space_eq[OF sets] by auto
   11.23 -  with sets show ?thesis unfolding `I = J`
   11.24 -    by (intro antisym prod_algebra_mono) auto
   11.25 -qed
   11.26 -
   11.27 -lemma space_in_prod_algebra:
   11.28 -  "(\<Pi>\<^isub>E i\<in>I. space (M i)) \<in> prod_algebra I M"
   11.29 -proof cases
   11.30 -  assume "I = {}" then show ?thesis
   11.31 -    by (auto simp add: prod_algebra_def image_iff prod_emb_def)
   11.32 -next
   11.33 -  assume "I \<noteq> {}"
   11.34 -  then obtain i where "i \<in> I" by auto
   11.35 -  then have "(\<Pi>\<^isub>E i\<in>I. space (M i)) = prod_emb I M {i} (\<Pi>\<^isub>E i\<in>{i}. space (M i))"
   11.36 -    by (auto simp: prod_emb_def Pi_iff)
   11.37 -  also have "\<dots> \<in> prod_algebra I M"
   11.38 -    using `i \<in> I` by (intro prod_algebraI) auto
   11.39 -  finally show ?thesis .
   11.40 -qed
   11.41 -
   11.42  lemma (in prob_space) indep_vars_iff_distr_eq_PiM:
   11.43    fixes I :: "'i set" and X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b"
   11.44    assumes "I \<noteq> {}"
   11.45 @@ -972,114 +944,6 @@
   11.46      unfolding UNIV_bool by auto
   11.47  qed
   11.48  
   11.49 -lemma measurable_bool_case[simp, intro]:
   11.50 -  "(\<lambda>(x, y). bool_case x y) \<in> measurable (M \<Otimes>\<^isub>M N) (Pi\<^isub>M UNIV (bool_case M N))"
   11.51 -    (is "?f \<in> measurable ?B ?P")
   11.52 -proof (rule measurable_PiM_single)
   11.53 -  show "?f \<in> space ?B \<rightarrow> (\<Pi>\<^isub>E i\<in>UNIV. space (bool_case M N i))"
   11.54 -    by (auto simp: space_pair_measure extensional_def split: bool.split)
   11.55 -  fix i A assume "A \<in> sets (case i of True \<Rightarrow> M | False \<Rightarrow> N)"
   11.56 -  moreover then have "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A}
   11.57 -    = (case i of True \<Rightarrow> A \<times> space N | False \<Rightarrow> space M \<times> A)" 
   11.58 -    by (auto simp: space_pair_measure split: bool.split dest!: sets_into_space)
   11.59 -  ultimately show "{\<omega> \<in> space (M \<Otimes>\<^isub>M N). prod_case bool_case \<omega> i \<in> A} \<in> sets ?B"
   11.60 -    by (auto split: bool.split)
   11.61 -qed
   11.62 -
   11.63 -lemma borel_measurable_indicator':
   11.64 -  "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
   11.65 -  using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
   11.66 -
   11.67 -lemma (in product_sigma_finite) distr_component:
   11.68 -  "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
   11.69 -proof (intro measure_eqI[symmetric])
   11.70 -  interpret I: finite_product_sigma_finite M "{i}" by default simp
   11.71 -
   11.72 -  have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
   11.73 -    by (auto simp: extensional_def restrict_def)
   11.74 -
   11.75 -  fix A assume A: "A \<in> sets ?P"
   11.76 -  then have "emeasure ?P A = (\<integral>\<^isup>+x. indicator A x \<partial>?P)" 
   11.77 -    by simp
   11.78 -  also have "\<dots> = (\<integral>\<^isup>+x. indicator ((\<lambda>x. \<lambda>i\<in>{i}. x) -` A \<inter> space (M i)) (x i) \<partial>PiM {i} M)" 
   11.79 -    by (intro positive_integral_cong) (auto simp: space_PiM indicator_def simp: eq)
   11.80 -  also have "\<dots> = emeasure ?D A"
   11.81 -    using A by (simp add: product_positive_integral_singleton emeasure_distr)
   11.82 -  finally show "emeasure (Pi\<^isub>M {i} M) A = emeasure ?D A" .
   11.83 -qed simp
   11.84 -
   11.85 -lemma pair_measure_eqI:
   11.86 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
   11.87 -  assumes sets: "sets (M1 \<Otimes>\<^isub>M M2) = sets M"
   11.88 -  assumes emeasure: "\<And>A B. A \<in> sets M1 \<Longrightarrow> B \<in> sets M2 \<Longrightarrow> emeasure M1 A * emeasure M2 B = emeasure M (A \<times> B)"
   11.89 -  shows "M1 \<Otimes>\<^isub>M M2 = M"
   11.90 -proof -
   11.91 -  interpret M1: sigma_finite_measure M1 by fact
   11.92 -  interpret M2: sigma_finite_measure M2 by fact
   11.93 -  interpret pair_sigma_finite M1 M2 by default
   11.94 -  from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
   11.95 -  let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
   11.96 -  let ?P = "M1 \<Otimes>\<^isub>M M2"
   11.97 -  show ?thesis
   11.98 -  proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
   11.99 -    show "?E \<subseteq> Pow (space ?P)"
  11.100 -      using space_closed[of M1] space_closed[of M2] by (auto simp: space_pair_measure)
  11.101 -    show "sets ?P = sigma_sets (space ?P) ?E"
  11.102 -      by (simp add: sets_pair_measure space_pair_measure)
  11.103 -    then show "sets M = sigma_sets (space ?P) ?E"
  11.104 -      using sets[symmetric] by simp
  11.105 -  next
  11.106 -    show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
  11.107 -      using F by (auto simp: space_pair_measure)
  11.108 -  next
  11.109 -    fix X assume "X \<in> ?E"
  11.110 -    then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
  11.111 -    then have "emeasure ?P X = emeasure M1 A * emeasure M2 B"
  11.112 -       by (simp add: M2.emeasure_pair_measure_Times)
  11.113 -    also have "\<dots> = emeasure M (A \<times> B)"
  11.114 -      using A B emeasure by auto
  11.115 -    finally show "emeasure ?P X = emeasure M X"
  11.116 -      by simp
  11.117 -  qed
  11.118 -qed
  11.119 -
  11.120 -lemma pair_measure_eq_distr_PiM:
  11.121 -  fixes M1 :: "'a measure" and M2 :: "'a measure"
  11.122 -  assumes "sigma_finite_measure M1" "sigma_finite_measure M2"
  11.123 -  shows "(M1 \<Otimes>\<^isub>M M2) = distr (Pi\<^isub>M UNIV (bool_case M1 M2)) (M1 \<Otimes>\<^isub>M M2) (\<lambda>x. (x True, x False))"
  11.124 -    (is "?P = ?D")
  11.125 -proof (rule pair_measure_eqI[OF assms])
  11.126 -  interpret B: product_sigma_finite "bool_case M1 M2"
  11.127 -    unfolding product_sigma_finite_def using assms by (auto split: bool.split)
  11.128 -  let ?B = "Pi\<^isub>M UNIV (bool_case M1 M2)"
  11.129 -
  11.130 -  have [simp]: "fst \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x True)" "snd \<circ> (\<lambda>x. (x True, x False)) = (\<lambda>x. x False)"
  11.131 -    by auto
  11.132 -  fix A B assume A: "A \<in> sets M1" and B: "B \<in> sets M2"
  11.133 -  have "emeasure M1 A * emeasure M2 B = (\<Prod> i\<in>UNIV. emeasure (bool_case M1 M2 i) (bool_case A B i))"
  11.134 -    by (simp add: UNIV_bool ac_simps)
  11.135 -  also have "\<dots> = emeasure ?B (Pi\<^isub>E UNIV (bool_case A B))"
  11.136 -    using A B by (subst B.emeasure_PiM) (auto split: bool.split)
  11.137 -  also have "Pi\<^isub>E UNIV (bool_case A B) = (\<lambda>x. (x True, x False)) -` (A \<times> B) \<inter> space ?B"
  11.138 -    using A[THEN sets_into_space] B[THEN sets_into_space]
  11.139 -    by (auto simp: Pi_iff all_bool_eq space_PiM split: bool.split)
  11.140 -  finally show "emeasure M1 A * emeasure M2 B = emeasure ?D (A \<times> B)"
  11.141 -    using A B
  11.142 -      measurable_component_singleton[of True UNIV "bool_case M1 M2"]
  11.143 -      measurable_component_singleton[of False UNIV "bool_case M1 M2"]
  11.144 -    by (subst emeasure_distr) (auto simp: measurable_pair_iff)
  11.145 -qed simp
  11.146 -
  11.147 -lemma measurable_Pair:
  11.148 -  assumes rvs: "X \<in> measurable M S" "Y \<in> measurable M T"
  11.149 -  shows "(\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
  11.150 -proof -
  11.151 -  have [simp]: "fst \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. X x)" "snd \<circ> (\<lambda>x. (X x, Y x)) = (\<lambda>x. Y x)"
  11.152 -    by auto
  11.153 -  show " (\<lambda>x. (X x, Y x)) \<in> measurable M (S \<Otimes>\<^isub>M T)"
  11.154 -    by (auto simp: measurable_pair_iff rvs)
  11.155 -qed
  11.156 -
  11.157  lemma (in prob_space) indep_var_distribution_eq:
  11.158    "indep_var S X T Y \<longleftrightarrow> random_variable S X \<and> random_variable T Y \<and>
  11.159      distr M S X \<Otimes>\<^isub>M distr M T Y = distr M (S \<Otimes>\<^isub>M T) (\<lambda>x. (X x, Y x))" (is "_ \<longleftrightarrow> _ \<and> _ \<and> ?S \<Otimes>\<^isub>M ?T = ?J")
    12.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 16 18:49:46 2012 +0100
    12.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 16 18:45:57 2012 +0100
    12.3 @@ -9,16 +9,6 @@
    12.4    imports Measure_Space Borel_Space
    12.5  begin
    12.6  
    12.7 -lemma ereal_minus_eq_PInfty_iff:
    12.8 -  fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
    12.9 -  by (cases x y rule: ereal2_cases) simp_all
   12.10 -
   12.11 -lemma real_ereal_1[simp]: "real (1::ereal) = 1"
   12.12 -  unfolding one_ereal_def by simp
   12.13 -
   12.14 -lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
   12.15 -  unfolding indicator_def by auto
   12.16 -
   12.17  lemma tendsto_real_max:
   12.18    fixes x y :: real
   12.19    assumes "(X ---> x) net"
   12.20 @@ -42,11 +32,6 @@
   12.21    then show ?thesis using assms by (auto intro: measurable_sets)
   12.22  qed
   12.23  
   12.24 -lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
   12.25 -proof
   12.26 -  assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
   12.27 -qed (auto simp: incseq_def)
   12.28 -
   12.29  section "Simple function"
   12.30  
   12.31  text {*
    13.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
    13.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
    13.3 @@ -9,14 +9,32 @@
    13.4    imports Finite_Product_Measure
    13.5  begin
    13.6  
    13.7 -lemma borel_measurable_indicator':
    13.8 -  "A \<in> sets borel \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
    13.9 -  using measurable_comp[OF _ borel_measurable_indicator, of f M borel A] by (auto simp add: comp_def)
   13.10 +lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
   13.11 +  by metis
   13.12 +
   13.13 +lemma absolutely_integrable_on_indicator[simp]:
   13.14 +  fixes A :: "'a::ordered_euclidean_space set"
   13.15 +  shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
   13.16 +    (indicator A :: _ \<Rightarrow> real) integrable_on X"
   13.17 +  unfolding absolutely_integrable_on_def by simp
   13.18  
   13.19 -lemma borel_measurable_sets:
   13.20 -  assumes "f \<in> measurable borel M" "A \<in> sets M"
   13.21 -  shows "f -` A \<in> sets borel"
   13.22 -  using measurable_sets[OF assms] by simp
   13.23 +lemma has_integral_indicator_UNIV:
   13.24 +  fixes s A :: "'a::ordered_euclidean_space set" and x :: real
   13.25 +  shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
   13.26 +proof -
   13.27 +  have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
   13.28 +    by (auto simp: fun_eq_iff indicator_def)
   13.29 +  then show ?thesis
   13.30 +    unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
   13.31 +qed
   13.32 +
   13.33 +lemma
   13.34 +  fixes s a :: "'a::ordered_euclidean_space set"
   13.35 +  shows integral_indicator_UNIV:
   13.36 +    "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
   13.37 +  and integrable_indicator_UNIV:
   13.38 +    "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
   13.39 +  unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
   13.40  
   13.41  subsection {* Standard Cubes *}
   13.42  
   13.43 @@ -62,6 +80,23 @@
   13.44  lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
   13.45    unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
   13.46  
   13.47 +lemma has_integral_interval_cube:
   13.48 +  fixes a b :: "'a::ordered_euclidean_space"
   13.49 +  shows "(indicator {a .. b} has_integral
   13.50 +    content ({\<chi>\<chi> i. max (- real n) (a $$ i) .. \<chi>\<chi> i. min (real n) (b $$ i)} :: 'a set)) (cube n)"
   13.51 +    (is "(?I has_integral content ?R) (cube n)")
   13.52 +proof -
   13.53 +  let "{?N .. ?P}" = ?R
   13.54 +  have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
   13.55 +    by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
   13.56 +  have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
   13.57 +    unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
   13.58 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
   13.59 +    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
   13.60 +  finally show ?thesis
   13.61 +    using has_integral_const[of "1::real" "?N" "?P"] by simp
   13.62 +qed
   13.63 +
   13.64  subsection {* Lebesgue measure *}
   13.65  
   13.66  definition lebesgue :: "'a::ordered_euclidean_space measure" where
   13.67 @@ -74,26 +109,6 @@
   13.68  lemma lebesgueI: "(\<And>n. (indicator A :: _ \<Rightarrow> real) integrable_on cube n) \<Longrightarrow> A \<in> sets lebesgue"
   13.69    unfolding lebesgue_def by simp
   13.70  
   13.71 -lemma absolutely_integrable_on_indicator[simp]:
   13.72 -  fixes A :: "'a::ordered_euclidean_space set"
   13.73 -  shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
   13.74 -    (indicator A :: _ \<Rightarrow> real) integrable_on X"
   13.75 -  unfolding absolutely_integrable_on_def by simp
   13.76 -
   13.77 -lemma LIMSEQ_indicator_UN:
   13.78 -  "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
   13.79 -proof cases
   13.80 -  assume "\<exists>i. x \<in> A i" then guess i .. note i = this
   13.81 -  then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
   13.82 -    "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
   13.83 -  show ?thesis
   13.84 -    apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
   13.85 -qed (auto simp: indicator_def)
   13.86 -
   13.87 -lemma indicator_add:
   13.88 -  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
   13.89 -  unfolding indicator_def by auto
   13.90 -
   13.91  lemma sigma_algebra_lebesgue:
   13.92    defines "leb \<equiv> {A. \<forall>n. (indicator A :: 'a::ordered_euclidean_space \<Rightarrow> real) integrable_on cube n}"
   13.93    shows "sigma_algebra UNIV leb"
   13.94 @@ -198,23 +213,6 @@
   13.95    qed
   13.96  qed (auto, fact)
   13.97  
   13.98 -lemma has_integral_interval_cube:
   13.99 -  fixes a b :: "'a::ordered_euclidean_space"
  13.100 -  shows "(indicator {a .. b} has_integral
  13.101 -    content ({\<chi>\<chi> i. max (- real n) (a $$ i) .. \<chi>\<chi> i. min (real n) (b $$ i)} :: 'a set)) (cube n)"
  13.102 -    (is "(?I has_integral content ?R) (cube n)")
  13.103 -proof -
  13.104 -  let "{?N .. ?P}" = ?R
  13.105 -  have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
  13.106 -    by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
  13.107 -  have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
  13.108 -    unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
  13.109 -  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
  13.110 -    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
  13.111 -  finally show ?thesis
  13.112 -    using has_integral_const[of "1::real" "?N" "?P"] by simp
  13.113 -qed
  13.114 -
  13.115  lemma lebesgueI_borel[intro, simp]:
  13.116    fixes s::"'a::ordered_euclidean_space set"
  13.117    assumes "s \<in> sets borel" shows "s \<in> sets lebesgue"
  13.118 @@ -261,24 +259,6 @@
  13.119      using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD)
  13.120  qed
  13.121  
  13.122 -lemma has_integral_indicator_UNIV:
  13.123 -  fixes s A :: "'a::ordered_euclidean_space set" and x :: real
  13.124 -  shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
  13.125 -proof -
  13.126 -  have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
  13.127 -    by (auto simp: fun_eq_iff indicator_def)
  13.128 -  then show ?thesis
  13.129 -    unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
  13.130 -qed
  13.131 -
  13.132 -lemma
  13.133 -  fixes s a :: "'a::ordered_euclidean_space set"
  13.134 -  shows integral_indicator_UNIV:
  13.135 -    "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
  13.136 -  and integrable_indicator_UNIV:
  13.137 -    "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
  13.138 -  unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
  13.139 -
  13.140  lemma lmeasure_finite_has_integral:
  13.141    fixes s :: "'a::ordered_euclidean_space set"
  13.142    assumes "s \<in> sets lebesgue" "emeasure lebesgue s = ereal m"
  13.143 @@ -429,11 +409,6 @@
  13.144    qed
  13.145  qed
  13.146  
  13.147 -lemma integral_const[simp]:
  13.148 -  fixes a b :: "'a::ordered_euclidean_space"
  13.149 -  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
  13.150 -  by (rule integral_unique) (rule has_integral_const)
  13.151 -
  13.152  lemma lmeasure_UNIV[intro]: "emeasure lebesgue (UNIV::'a::ordered_euclidean_space set) = \<infinity>"
  13.153  proof (simp add: emeasure_lebesgue, intro SUP_PInfty bexI)
  13.154    fix n :: nat
  13.155 @@ -467,17 +442,6 @@
  13.156      by (simp add: indicator_def [abs_def])
  13.157  qed
  13.158  
  13.159 -lemma atLeastAtMost_singleton_euclidean[simp]:
  13.160 -  fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}"
  13.161 -  by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a])
  13.162 -
  13.163 -lemma content_singleton[simp]: "content {a} = 0"
  13.164 -proof -
  13.165 -  have "content {a .. a} = 0"
  13.166 -    by (subst content_closed_interval) auto
  13.167 -  then show ?thesis by simp
  13.168 -qed
  13.169 -
  13.170  lemma lmeasure_singleton[simp]:
  13.171    fixes a :: "'a::ordered_euclidean_space" shows "emeasure lebesgue {a} = 0"
  13.172    using lmeasure_atLeastAtMost[of a a] by simp
  13.173 @@ -609,16 +573,6 @@
  13.174  
  13.175  subsection {* Lebesgue integrable implies Gauge integrable *}
  13.176  
  13.177 -lemma has_integral_cmult_real:
  13.178 -  fixes c :: real
  13.179 -  assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
  13.180 -  shows "((\<lambda>x. c * f x) has_integral c * x) A"
  13.181 -proof cases
  13.182 -  assume "c \<noteq> 0"
  13.183 -  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
  13.184 -    unfolding real_scaleR_def .
  13.185 -qed simp
  13.186 -
  13.187  lemma simple_function_has_integral:
  13.188    fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
  13.189    assumes f:"simple_function lebesgue f"
  13.190 @@ -657,10 +611,6 @@
  13.191    finally show "((\<lambda>x. real (\<Sum>y\<in>range f. y * ?F y x)) has_integral real (\<Sum>x\<in>range f. x * ?M x)) UNIV" .
  13.192  qed fact
  13.193  
  13.194 -lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
  13.195 -  unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
  13.196 -  using assms by auto
  13.197 -
  13.198  lemma simple_function_has_integral':
  13.199    fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
  13.200    assumes f: "simple_function lebesgue f" "\<And>x. 0 \<le> f x"
  13.201 @@ -695,9 +645,6 @@
  13.202    qed
  13.203  qed
  13.204  
  13.205 -lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
  13.206 -  by (auto simp: indicator_def one_ereal_def)
  13.207 -
  13.208  lemma positive_integral_has_integral:
  13.209    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
  13.210    assumes f: "f \<in> borel_measurable lebesgue" "range f \<subseteq> {0..<\<infinity>}" "integral\<^isup>P lebesgue f \<noteq> \<infinity>"
  13.211 @@ -843,12 +790,6 @@
  13.212      unfolding lebesgue_integral_eq_borel[OF borel] by simp
  13.213  qed
  13.214  
  13.215 -lemma integrable_on_cmult_iff:
  13.216 -  fixes c :: real assumes "c \<noteq> 0"
  13.217 -  shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
  13.218 -  using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
  13.219 -  by auto
  13.220 -
  13.221  lemma positive_integral_lebesgue_has_integral:
  13.222    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
  13.223    assumes f_borel: "f \<in> borel_measurable lebesgue" and nonneg: "\<And>x. 0 \<le> f x"
  13.224 @@ -983,9 +924,6 @@
  13.225  interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure" "{..<n}" for n :: nat
  13.226    by default auto
  13.227  
  13.228 -lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
  13.229 -  by metis
  13.230 -
  13.231  lemma sets_product_borel:
  13.232    assumes I: "finite I"
  13.233    shows "sets (\<Pi>\<^isub>M i\<in>I. lborel) = sigma_sets (\<Pi>\<^isub>E i\<in>I. UNIV) { \<Pi>\<^isub>E i\<in>I. {..< x i :: real} | x. True}" (is "_ = ?G")
    14.1 --- a/src/HOL/Probability/Measure_Space.thy	Fri Nov 16 18:49:46 2012 +0100
    14.2 +++ b/src/HOL/Probability/Measure_Space.thy	Fri Nov 16 18:45:57 2012 +0100
    14.3 @@ -18,6 +18,28 @@
    14.4    apply (subst LIMSEQ_Suc_iff[symmetric])
    14.5    unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
    14.6  
    14.7 +subsection "Relate extended reals and the indicator function"
    14.8 +
    14.9 +lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
   14.10 +  by (auto simp: indicator_def one_ereal_def)
   14.11 +
   14.12 +lemma ereal_indicator_pos[simp,intro]: "0 \<le> (indicator A x ::ereal)"
   14.13 +  unfolding indicator_def by auto
   14.14 +
   14.15 +lemma LIMSEQ_indicator_UN:
   14.16 +  "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
   14.17 +proof cases
   14.18 +  assume "\<exists>i. x \<in> A i" then guess i .. note i = this
   14.19 +  then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
   14.20 +    "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
   14.21 +  show ?thesis
   14.22 +    apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
   14.23 +qed (auto simp: indicator_def)
   14.24 +
   14.25 +lemma indicator_add:
   14.26 +  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
   14.27 +  unfolding indicator_def by auto
   14.28 +
   14.29  lemma suminf_cmult_indicator:
   14.30    fixes f :: "nat \<Rightarrow> ereal"
   14.31    assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
   14.32 @@ -111,7 +133,7 @@
   14.33    "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>M \<Longrightarrow> y\<in>M \<Longrightarrow> f x \<le> f y"
   14.34    by (auto simp add: increasing_def)
   14.35  
   14.36 -lemma countably_additiveI:
   14.37 +lemma countably_additiveI[case_names countably]:
   14.38    "(\<And>A. range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> M \<Longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>i. A i))
   14.39    \<Longrightarrow> countably_additive M f"
   14.40    by (simp add: countably_additive_def)
   14.41 @@ -1114,6 +1136,9 @@
   14.42    show "sigma_algebra (space N) (sets N)" ..
   14.43  qed fact
   14.44  
   14.45 +lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
   14.46 +  by (rule measure_eqI) (auto simp: emeasure_distr)
   14.47 +
   14.48  lemma measure_distr:
   14.49    "f \<in> measurable M N \<Longrightarrow> S \<in> sets N \<Longrightarrow> measure (distr M N f) S = measure M (f -` S \<inter> space M)"
   14.50    by (simp add: emeasure_distr measure_def)
   14.51 @@ -1389,6 +1414,107 @@
   14.52    shows "measure M A = measure M B"
   14.53    using assms emeasure_eq_AE[OF assms] by (simp add: emeasure_eq_measure)
   14.54  
   14.55 +lemma (in finite_measure) measure_increasing: "increasing M (measure M)"
   14.56 +  by (auto intro!: finite_measure_mono simp: increasing_def)
   14.57 +
   14.58 +lemma (in finite_measure) measure_zero_union:
   14.59 +  assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0"
   14.60 +  shows "measure M (s \<union> t) = measure M s"
   14.61 +using assms
   14.62 +proof -
   14.63 +  have "measure M (s \<union> t) \<le> measure M s"
   14.64 +    using finite_measure_subadditive[of s t] assms by auto
   14.65 +  moreover have "measure M (s \<union> t) \<ge> measure M s"
   14.66 +    using assms by (blast intro: finite_measure_mono)
   14.67 +  ultimately show ?thesis by simp
   14.68 +qed
   14.69 +
   14.70 +lemma (in finite_measure) measure_eq_compl:
   14.71 +  assumes "s \<in> sets M" "t \<in> sets M"
   14.72 +  assumes "measure M (space M - s) = measure M (space M - t)"
   14.73 +  shows "measure M s = measure M t"
   14.74 +  using assms finite_measure_compl by auto
   14.75 +
   14.76 +lemma (in finite_measure) measure_eq_bigunion_image:
   14.77 +  assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
   14.78 +  assumes "disjoint_family f" "disjoint_family g"
   14.79 +  assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
   14.80 +  shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
   14.81 +using assms
   14.82 +proof -
   14.83 +  have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
   14.84 +    by (rule finite_measure_UNION[OF assms(1,3)])
   14.85 +  have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
   14.86 +    by (rule finite_measure_UNION[OF assms(2,4)])
   14.87 +  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
   14.88 +qed
   14.89 +
   14.90 +lemma (in finite_measure) measure_countably_zero:
   14.91 +  assumes "range c \<subseteq> sets M"
   14.92 +  assumes "\<And> i. measure M (c i) = 0"
   14.93 +  shows "measure M (\<Union> i :: nat. c i) = 0"
   14.94 +proof (rule antisym)
   14.95 +  show "measure M (\<Union> i :: nat. c i) \<le> 0"
   14.96 +    using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
   14.97 +qed (simp add: measure_nonneg)
   14.98 +
   14.99 +lemma (in finite_measure) measure_space_inter:
  14.100 +  assumes events:"s \<in> sets M" "t \<in> sets M"
  14.101 +  assumes "measure M t = measure M (space M)"
  14.102 +  shows "measure M (s \<inter> t) = measure M s"
  14.103 +proof -
  14.104 +  have "measure M ((space M - s) \<union> (space M - t)) = measure M (space M - s)"
  14.105 +    using events assms finite_measure_compl[of "t"] by (auto intro!: measure_zero_union)
  14.106 +  also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
  14.107 +    by blast
  14.108 +  finally show "measure M (s \<inter> t) = measure M s"
  14.109 +    using events by (auto intro!: measure_eq_compl[of "s \<inter> t" s])
  14.110 +qed
  14.111 +
  14.112 +lemma (in finite_measure) measure_equiprobable_finite_unions:
  14.113 +  assumes s: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> sets M"
  14.114 +  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> measure M {x} = measure M {y}"
  14.115 +  shows "measure M s = real (card s) * measure M {SOME x. x \<in> s}"
  14.116 +proof cases
  14.117 +  assume "s \<noteq> {}"
  14.118 +  then have "\<exists> x. x \<in> s" by blast
  14.119 +  from someI_ex[OF this] assms
  14.120 +  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> measure M {x} = measure M {SOME y. y \<in> s}" by blast
  14.121 +  have "measure M s = (\<Sum> x \<in> s. measure M {x})"
  14.122 +    using finite_measure_eq_setsum_singleton[OF s] by simp
  14.123 +  also have "\<dots> = (\<Sum> x \<in> s. measure M {SOME y. y \<in> s})" using prob_some by auto
  14.124 +  also have "\<dots> = real (card s) * measure M {(SOME x. x \<in> s)}"
  14.125 +    using setsum_constant assms by (simp add: real_eq_of_nat)
  14.126 +  finally show ?thesis by simp
  14.127 +qed simp
  14.128 +
  14.129 +lemma (in finite_measure) measure_real_sum_image_fn:
  14.130 +  assumes "e \<in> sets M"
  14.131 +  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> sets M"
  14.132 +  assumes "finite s"
  14.133 +  assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
  14.134 +  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
  14.135 +  shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
  14.136 +proof -
  14.137 +  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
  14.138 +    using `e \<in> sets M` sets_into_space upper by blast
  14.139 +  hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
  14.140 +  also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
  14.141 +  proof (rule finite_measure_finite_Union)
  14.142 +    show "finite s" by fact
  14.143 +    show "(\<lambda>i. e \<inter> f i)`s \<subseteq> sets M" using assms(2) by auto
  14.144 +    show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
  14.145 +      using disjoint by (auto simp: disjoint_family_on_def)
  14.146 +  qed
  14.147 +  finally show ?thesis .
  14.148 +qed
  14.149 +
  14.150 +lemma (in finite_measure) measure_exclude:
  14.151 +  assumes "A \<in> sets M" "B \<in> sets M"
  14.152 +  assumes "measure M A = measure M (space M)" "A \<inter> B = {}"
  14.153 +  shows "measure M B = 0"
  14.154 +  using measure_space_inter[of B A] assms by (auto simp: ac_simps)
  14.155 +
  14.156  section {* Counting space *}
  14.157  
  14.158  lemma strict_monoI_Suc:
    15.1 --- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
    15.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
    15.3 @@ -9,125 +9,6 @@
    15.4    imports Lebesgue_Measure Radon_Nikodym
    15.5  begin
    15.6  
    15.7 -lemma funset_eq_UN_fun_upd_I:
    15.8 -  assumes *: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f(a := d) \<in> F A"
    15.9 -  and **: "\<And>f. f \<in> F (insert a A) \<Longrightarrow> f a \<in> G (f(a:=d))"
   15.10 -  and ***: "\<And>f x. \<lbrakk> f \<in> F A ; x \<in> G f \<rbrakk> \<Longrightarrow> f(a:=x) \<in> F (insert a A)"
   15.11 -  shows "F (insert a A) = (\<Union>f\<in>F A. fun_upd f a ` (G f))"
   15.12 -proof safe
   15.13 -  fix f assume f: "f \<in> F (insert a A)"
   15.14 -  show "f \<in> (\<Union>f\<in>F A. fun_upd f a ` G f)"
   15.15 -  proof (rule UN_I[of "f(a := d)"])
   15.16 -    show "f(a := d) \<in> F A" using *[OF f] .
   15.17 -    show "f \<in> fun_upd (f(a:=d)) a ` G (f(a:=d))"
   15.18 -    proof (rule image_eqI[of _ _ "f a"])
   15.19 -      show "f a \<in> G (f(a := d))" using **[OF f] .
   15.20 -    qed simp
   15.21 -  qed
   15.22 -next
   15.23 -  fix f x assume "f \<in> F A" "x \<in> G f"
   15.24 -  from ***[OF this] show "f(a := x) \<in> F (insert a A)" .
   15.25 -qed
   15.26 -
   15.27 -lemma extensional_funcset_insert_eq[simp]:
   15.28 -  assumes "a \<notin> A"
   15.29 -  shows "extensional (insert a A) \<inter> (insert a A \<rightarrow> B) = (\<Union>f \<in> extensional A \<inter> (A \<rightarrow> B). (\<lambda>b. f(a := b)) ` B)"
   15.30 -  apply (rule funset_eq_UN_fun_upd_I)
   15.31 -  using assms
   15.32 -  by (auto intro!: inj_onI dest: inj_onD split: split_if_asm simp: extensional_def)
   15.33 -
   15.34 -lemma finite_extensional_funcset[simp, intro]:
   15.35 -  assumes "finite A" "finite B"
   15.36 -  shows "finite (extensional A \<inter> (A \<rightarrow> B))"
   15.37 -  using assms by induct auto
   15.38 -
   15.39 -lemma finite_PiE[simp, intro]:
   15.40 -  assumes fin: "finite A" "\<And>i. i \<in> A \<Longrightarrow> finite (B i)"
   15.41 -  shows "finite (Pi\<^isub>E A B)"
   15.42 -proof -
   15.43 -  have *: "(Pi\<^isub>E A B) \<subseteq> extensional A \<inter> (A \<rightarrow> (\<Union>i\<in>A. B i))" by auto
   15.44 -  show ?thesis
   15.45 -    using fin by (intro finite_subset[OF *] finite_extensional_funcset) auto
   15.46 -qed
   15.47 -
   15.48 -
   15.49 -lemma countably_additiveI[case_names countably]:
   15.50 -  assumes "\<And>A. \<lbrakk> range A \<subseteq> M ; disjoint_family A ; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
   15.51 -  shows "countably_additive M \<mu>"
   15.52 -  using assms unfolding countably_additive_def by auto
   15.53 -
   15.54 -lemma convex_le_Inf_differential:
   15.55 -  fixes f :: "real \<Rightarrow> real"
   15.56 -  assumes "convex_on I f"
   15.57 -  assumes "x \<in> interior I" "y \<in> I"
   15.58 -  shows "f y \<ge> f x + Inf ((\<lambda>t. (f x - f t) / (x - t)) ` ({x<..} \<inter> I)) * (y - x)"
   15.59 -    (is "_ \<ge> _ + Inf (?F x) * (y - x)")
   15.60 -proof -
   15.61 -  show ?thesis
   15.62 -  proof (cases rule: linorder_cases)
   15.63 -    assume "x < y"
   15.64 -    moreover
   15.65 -    have "open (interior I)" by auto
   15.66 -    from openE[OF this `x \<in> interior I`] guess e . note e = this
   15.67 -    moreover def t \<equiv> "min (x + e / 2) ((x + y) / 2)"
   15.68 -    ultimately have "x < t" "t < y" "t \<in> ball x e"
   15.69 -      by (auto simp: dist_real_def field_simps split: split_min)
   15.70 -    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
   15.71 -
   15.72 -    have "open (interior I)" by auto
   15.73 -    from openE[OF this `x \<in> interior I`] guess e .
   15.74 -    moreover def K \<equiv> "x - e / 2"
   15.75 -    with `0 < e` have "K \<in> ball x e" "K < x" by (auto simp: dist_real_def)
   15.76 -    ultimately have "K \<in> I" "K < x" "x \<in> I"
   15.77 -      using interior_subset[of I] `x \<in> interior I` by auto
   15.78 -
   15.79 -    have "Inf (?F x) \<le> (f x - f y) / (x - y)"
   15.80 -    proof (rule Inf_lower2)
   15.81 -      show "(f x - f t) / (x - t) \<in> ?F x"
   15.82 -        using `t \<in> I` `x < t` by auto
   15.83 -      show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"
   15.84 -        using `convex_on I f` `x \<in> I` `y \<in> I` `x < t` `t < y` by (rule convex_on_diff)
   15.85 -    next
   15.86 -      fix y assume "y \<in> ?F x"
   15.87 -      with order_trans[OF convex_on_diff[OF `convex_on I f` `K \<in> I` _ `K < x` _]]
   15.88 -      show "(f K - f x) / (K - x) \<le> y" by auto
   15.89 -    qed
   15.90 -    then show ?thesis
   15.91 -      using `x < y` by (simp add: field_simps)
   15.92 -  next
   15.93 -    assume "y < x"
   15.94 -    moreover
   15.95 -    have "open (interior I)" by auto
   15.96 -    from openE[OF this `x \<in> interior I`] guess e . note e = this
   15.97 -    moreover def t \<equiv> "x + e / 2"
   15.98 -    ultimately have "x < t" "t \<in> ball x e"
   15.99 -      by (auto simp: dist_real_def field_simps)
  15.100 -    with `x \<in> interior I` e interior_subset[of I] have "t \<in> I" "x \<in> I" by auto
  15.101 -
  15.102 -    have "(f x - f y) / (x - y) \<le> Inf (?F x)"
  15.103 -    proof (rule Inf_greatest)
  15.104 -      have "(f x - f y) / (x - y) = (f y - f x) / (y - x)"
  15.105 -        using `y < x` by (auto simp: field_simps)
  15.106 -      also
  15.107 -      fix z  assume "z \<in> ?F x"
  15.108 -      with order_trans[OF convex_on_diff[OF `convex_on I f` `y \<in> I` _ `y < x`]]
  15.109 -      have "(f y - f x) / (y - x) \<le> z" by auto
  15.110 -      finally show "(f x - f y) / (x - y) \<le> z" .
  15.111 -    next
  15.112 -      have "open (interior I)" by auto
  15.113 -      from openE[OF this `x \<in> interior I`] guess e . note e = this
  15.114 -      then have "x + e / 2 \<in> ball x e" by (auto simp: dist_real_def)
  15.115 -      with e interior_subset[of I] have "x + e / 2 \<in> {x<..} \<inter> I" by auto
  15.116 -      then show "?F x \<noteq> {}" by blast
  15.117 -    qed
  15.118 -    then show ?thesis
  15.119 -      using `y < x` by (simp add: field_simps)
  15.120 -  qed simp
  15.121 -qed
  15.122 -
  15.123 -lemma distr_id[simp]: "distr N N (\<lambda>x. x) = N"
  15.124 -  by (rule measure_eqI) (auto simp: emeasure_distr)
  15.125 -
  15.126  locale prob_space = finite_measure +
  15.127    assumes emeasure_space_1: "emeasure M (space M) = 1"
  15.128  
  15.129 @@ -230,101 +111,6 @@
  15.130    then show False by auto
  15.131  qed
  15.132  
  15.133 -lemma (in finite_measure) prob_space_increasing: "increasing M (measure M)"
  15.134 -  by (auto intro!: finite_measure_mono simp: increasing_def)
  15.135 -
  15.136 -lemma (in finite_measure) prob_zero_union:
  15.137 -  assumes "s \<in> sets M" "t \<in> sets M" "measure M t = 0"
  15.138 -  shows "measure M (s \<union> t) = measure M s"
  15.139 -using assms
  15.140 -proof -
  15.141 -  have "measure M (s \<union> t) \<le> measure M s"
  15.142 -    using finite_measure_subadditive[of s t] assms by auto
  15.143 -  moreover have "measure M (s \<union> t) \<ge> measure M s"
  15.144 -    using assms by (blast intro: finite_measure_mono)
  15.145 -  ultimately show ?thesis by simp
  15.146 -qed
  15.147 -
  15.148 -lemma (in finite_measure) prob_eq_compl:
  15.149 -  assumes "s \<in> sets M" "t \<in> sets M"
  15.150 -  assumes "measure M (space M - s) = measure M (space M - t)"
  15.151 -  shows "measure M s = measure M t"
  15.152 -  using assms finite_measure_compl by auto
  15.153 -
  15.154 -lemma (in prob_space) prob_one_inter:
  15.155 -  assumes events:"s \<in> events" "t \<in> events"
  15.156 -  assumes "prob t = 1"
  15.157 -  shows "prob (s \<inter> t) = prob s"
  15.158 -proof -
  15.159 -  have "prob ((space M - s) \<union> (space M - t)) = prob (space M - s)"
  15.160 -    using events assms  prob_compl[of "t"] by (auto intro!: prob_zero_union)
  15.161 -  also have "(space M - s) \<union> (space M - t) = space M - (s \<inter> t)"
  15.162 -    by blast
  15.163 -  finally show "prob (s \<inter> t) = prob s"
  15.164 -    using events by (auto intro!: prob_eq_compl[of "s \<inter> t" s])
  15.165 -qed
  15.166 -
  15.167 -lemma (in finite_measure) prob_eq_bigunion_image:
  15.168 -  assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
  15.169 -  assumes "disjoint_family f" "disjoint_family g"
  15.170 -  assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
  15.171 -  shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
  15.172 -using assms
  15.173 -proof -
  15.174 -  have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
  15.175 -    by (rule finite_measure_UNION[OF assms(1,3)])
  15.176 -  have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
  15.177 -    by (rule finite_measure_UNION[OF assms(2,4)])
  15.178 -  show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
  15.179 -qed
  15.180 -
  15.181 -lemma (in finite_measure) prob_countably_zero:
  15.182 -  assumes "range c \<subseteq> sets M"
  15.183 -  assumes "\<And> i. measure M (c i) = 0"
  15.184 -  shows "measure M (\<Union> i :: nat. c i) = 0"
  15.185 -proof (rule antisym)
  15.186 -  show "measure M (\<Union> i :: nat. c i) \<le> 0"
  15.187 -    using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
  15.188 -qed (simp add: measure_nonneg)
  15.189 -
  15.190 -lemma (in prob_space) prob_equiprobable_finite_unions:
  15.191 -  assumes "s \<in> events"
  15.192 -  assumes s_finite: "finite s" "\<And>x. x \<in> s \<Longrightarrow> {x} \<in> events"
  15.193 -  assumes "\<And> x y. \<lbrakk>x \<in> s; y \<in> s\<rbrakk> \<Longrightarrow> (prob {x} = prob {y})"
  15.194 -  shows "prob s = real (card s) * prob {SOME x. x \<in> s}"
  15.195 -proof (cases "s = {}")
  15.196 -  case False hence "\<exists> x. x \<in> s" by blast
  15.197 -  from someI_ex[OF this] assms
  15.198 -  have prob_some: "\<And> x. x \<in> s \<Longrightarrow> prob {x} = prob {SOME y. y \<in> s}" by blast
  15.199 -  have "prob s = (\<Sum> x \<in> s. prob {x})"
  15.200 -    using finite_measure_eq_setsum_singleton[OF s_finite] by simp
  15.201 -  also have "\<dots> = (\<Sum> x \<in> s. prob {SOME y. y \<in> s})" using prob_some by auto
  15.202 -  also have "\<dots> = real (card s) * prob {(SOME x. x \<in> s)}"
  15.203 -    using setsum_constant assms by (simp add: real_eq_of_nat)
  15.204 -  finally show ?thesis by simp
  15.205 -qed simp
  15.206 -
  15.207 -lemma (in prob_space) prob_real_sum_image_fn:
  15.208 -  assumes "e \<in> events"
  15.209 -  assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> events"
  15.210 -  assumes "finite s"
  15.211 -  assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
  15.212 -  assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
  15.213 -  shows "prob e = (\<Sum> x \<in> s. prob (e \<inter> f x))"
  15.214 -proof -
  15.215 -  have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
  15.216 -    using `e \<in> events` sets_into_space upper by blast
  15.217 -  hence "prob e = prob (\<Union> i \<in> s. e \<inter> f i)" by simp
  15.218 -  also have "\<dots> = (\<Sum> x \<in> s. prob (e \<inter> f x))"
  15.219 -  proof (rule finite_measure_finite_Union)
  15.220 -    show "finite s" by fact
  15.221 -    show "(\<lambda>i. e \<inter> f i)`s \<subseteq> events" using assms(2) by auto
  15.222 -    show "disjoint_family_on (\<lambda>i. e \<inter> f i) s"
  15.223 -      using disjoint by (auto simp: disjoint_family_on_def)
  15.224 -  qed
  15.225 -  finally show ?thesis .
  15.226 -qed
  15.227 -
  15.228  lemma (in prob_space) expectation_less:
  15.229    assumes [simp]: "integrable M X"
  15.230    assumes gt: "AE x in M. X x < b"
  15.231 @@ -398,14 +184,6 @@
  15.232    finally show "q (expectation X) \<le> expectation (\<lambda>x. q (X x))" .
  15.233  qed
  15.234  
  15.235 -lemma (in prob_space) prob_x_eq_1_imp_prob_y_eq_0:
  15.236 -  assumes "{x} \<in> events"
  15.237 -  assumes "prob {x} = 1"
  15.238 -  assumes "{y} \<in> events"
  15.239 -  assumes "y \<noteq> x"
  15.240 -  shows "prob {y} = 0"
  15.241 -  using prob_one_inter[of "{y}" "{x}"] assms by auto
  15.242 -
  15.243  subsection  {* Introduce binder for probability *}
  15.244  
  15.245  syntax
    16.1 --- a/src/HOL/Product_Type.thy	Fri Nov 16 18:49:46 2012 +0100
    16.2 +++ b/src/HOL/Product_Type.thy	Fri Nov 16 18:45:57 2012 +0100
    16.3 @@ -393,6 +393,9 @@
    16.4    from `PROP P (fst x, snd x)` show "PROP P x" by simp
    16.5  qed
    16.6  
    16.7 +lemma case_prod_distrib: "f (case x of (x, y) \<Rightarrow> g x y) = (case x of (x, y) \<Rightarrow> f (g x y))"
    16.8 +  by (cases x) simp
    16.9 +
   16.10  text {*
   16.11    The rule @{thm [source] split_paired_all} does not work with the
   16.12    Simplifier because it also affects premises in congrence rules,
   16.13 @@ -495,6 +498,10 @@
   16.14  lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
   16.15    by (subst surjective_pairing, rule split_conv)
   16.16  
   16.17 +lemma split_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))"
   16.18 +  by (auto simp: fun_eq_iff)
   16.19 +
   16.20 +
   16.21  lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
   16.22    -- {* For use with @{text split} and the Simplifier. *}
   16.23    by (insert surj_pair [of p], clarify, simp)
   16.24 @@ -1019,6 +1026,9 @@
   16.25  lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
   16.26    by auto
   16.27  
   16.28 +lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> ((A = {} \<or> B = {}) \<and> (C = {} \<or> D = {}))"
   16.29 +  by auto
   16.30 +
   16.31  lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
   16.32    by force
   16.33  
   16.34 @@ -1036,6 +1046,9 @@
   16.35    apply auto
   16.36    done
   16.37  
   16.38 +lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   16.39 +  by auto
   16.40 +
   16.41  lemma swap_inj_on:
   16.42    "inj_on (\<lambda>(i, j). (j, i)) A"
   16.43    by (auto intro!: inj_onI)