src/HOL/Probability/Lebesgue_Measure.thy
 changeset 50104 de19856feb54 parent 50003 8c213922ed49 child 50105 65d5b18e1626
```     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 16 18:49:46 2012 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
1.3 @@ -9,14 +9,32 @@
1.4    imports Finite_Product_Measure
1.5  begin
1.6
1.7 -lemma borel_measurable_indicator':
1.8 -  "A \<in> sets borel \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
1.9 -  using measurable_comp[OF _ borel_measurable_indicator, of f M borel A] by (auto simp add: comp_def)
1.10 +lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
1.11 +  by metis
1.12 +
1.13 +lemma absolutely_integrable_on_indicator[simp]:
1.14 +  fixes A :: "'a::ordered_euclidean_space set"
1.15 +  shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
1.16 +    (indicator A :: _ \<Rightarrow> real) integrable_on X"
1.17 +  unfolding absolutely_integrable_on_def by simp
1.18
1.19 -lemma borel_measurable_sets:
1.20 -  assumes "f \<in> measurable borel M" "A \<in> sets M"
1.21 -  shows "f -` A \<in> sets borel"
1.22 -  using measurable_sets[OF assms] by simp
1.23 +lemma has_integral_indicator_UNIV:
1.24 +  fixes s A :: "'a::ordered_euclidean_space set" and x :: real
1.25 +  shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
1.26 +proof -
1.27 +  have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
1.28 +    by (auto simp: fun_eq_iff indicator_def)
1.29 +  then show ?thesis
1.30 +    unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
1.31 +qed
1.32 +
1.33 +lemma
1.34 +  fixes s a :: "'a::ordered_euclidean_space set"
1.35 +  shows integral_indicator_UNIV:
1.36 +    "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
1.37 +  and integrable_indicator_UNIV:
1.38 +    "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
1.39 +  unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
1.40
1.41  subsection {* Standard Cubes *}
1.42
1.43 @@ -62,6 +80,23 @@
1.44  lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
1.45    unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
1.46
1.47 +lemma has_integral_interval_cube:
1.48 +  fixes a b :: "'a::ordered_euclidean_space"
1.49 +  shows "(indicator {a .. b} has_integral
1.50 +    content ({\<chi>\<chi> i. max (- real n) (a \$\$ i) .. \<chi>\<chi> i. min (real n) (b \$\$ i)} :: 'a set)) (cube n)"
1.51 +    (is "(?I has_integral content ?R) (cube n)")
1.52 +proof -
1.53 +  let "{?N .. ?P}" = ?R
1.54 +  have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
1.55 +    by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
1.56 +  have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
1.57 +    unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
1.58 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
1.59 +    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
1.60 +  finally show ?thesis
1.61 +    using has_integral_const[of "1::real" "?N" "?P"] by simp
1.62 +qed
1.63 +
1.64  subsection {* Lebesgue measure *}
1.65
1.66  definition lebesgue :: "'a::ordered_euclidean_space measure" where
1.67 @@ -74,26 +109,6 @@
1.68  lemma lebesgueI: "(\<And>n. (indicator A :: _ \<Rightarrow> real) integrable_on cube n) \<Longrightarrow> A \<in> sets lebesgue"
1.69    unfolding lebesgue_def by simp
1.70
1.71 -lemma absolutely_integrable_on_indicator[simp]:
1.72 -  fixes A :: "'a::ordered_euclidean_space set"
1.73 -  shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
1.74 -    (indicator A :: _ \<Rightarrow> real) integrable_on X"
1.75 -  unfolding absolutely_integrable_on_def by simp
1.76 -
1.77 -lemma LIMSEQ_indicator_UN:
1.78 -  "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
1.79 -proof cases
1.80 -  assume "\<exists>i. x \<in> A i" then guess i .. note i = this
1.81 -  then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
1.82 -    "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
1.83 -  show ?thesis
1.84 -    apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
1.85 -qed (auto simp: indicator_def)
1.86 -
1.88 -  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
1.89 -  unfolding indicator_def by auto
1.90 -
1.91  lemma sigma_algebra_lebesgue:
1.92    defines "leb \<equiv> {A. \<forall>n. (indicator A :: 'a::ordered_euclidean_space \<Rightarrow> real) integrable_on cube n}"
1.93    shows "sigma_algebra UNIV leb"
1.94 @@ -198,23 +213,6 @@
1.95    qed
1.96  qed (auto, fact)
1.97
1.98 -lemma has_integral_interval_cube:
1.99 -  fixes a b :: "'a::ordered_euclidean_space"
1.100 -  shows "(indicator {a .. b} has_integral
1.101 -    content ({\<chi>\<chi> i. max (- real n) (a \$\$ i) .. \<chi>\<chi> i. min (real n) (b \$\$ i)} :: 'a set)) (cube n)"
1.102 -    (is "(?I has_integral content ?R) (cube n)")
1.103 -proof -
1.104 -  let "{?N .. ?P}" = ?R
1.105 -  have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
1.106 -    by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
1.107 -  have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
1.108 -    unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
1.109 -  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
1.110 -    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
1.111 -  finally show ?thesis
1.112 -    using has_integral_const[of "1::real" "?N" "?P"] by simp
1.113 -qed
1.114 -
1.115  lemma lebesgueI_borel[intro, simp]:
1.116    fixes s::"'a::ordered_euclidean_space set"
1.117    assumes "s \<in> sets borel" shows "s \<in> sets lebesgue"
1.118 @@ -261,24 +259,6 @@
1.119      using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD)
1.120  qed
1.121
1.122 -lemma has_integral_indicator_UNIV:
1.123 -  fixes s A :: "'a::ordered_euclidean_space set" and x :: real
1.124 -  shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
1.125 -proof -
1.126 -  have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
1.127 -    by (auto simp: fun_eq_iff indicator_def)
1.128 -  then show ?thesis
1.129 -    unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
1.130 -qed
1.131 -
1.132 -lemma
1.133 -  fixes s a :: "'a::ordered_euclidean_space set"
1.134 -  shows integral_indicator_UNIV:
1.135 -    "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
1.136 -  and integrable_indicator_UNIV:
1.137 -    "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
1.138 -  unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
1.139 -
1.140  lemma lmeasure_finite_has_integral:
1.141    fixes s :: "'a::ordered_euclidean_space set"
1.142    assumes "s \<in> sets lebesgue" "emeasure lebesgue s = ereal m"
1.143 @@ -429,11 +409,6 @@
1.144    qed
1.145  qed
1.146
1.147 -lemma integral_const[simp]:
1.148 -  fixes a b :: "'a::ordered_euclidean_space"
1.149 -  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
1.150 -  by (rule integral_unique) (rule has_integral_const)
1.151 -
1.152  lemma lmeasure_UNIV[intro]: "emeasure lebesgue (UNIV::'a::ordered_euclidean_space set) = \<infinity>"
1.153  proof (simp add: emeasure_lebesgue, intro SUP_PInfty bexI)
1.154    fix n :: nat
1.155 @@ -467,17 +442,6 @@
1.156      by (simp add: indicator_def [abs_def])
1.157  qed
1.158
1.159 -lemma atLeastAtMost_singleton_euclidean[simp]:
1.160 -  fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}"
1.161 -  by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a])
1.162 -
1.163 -lemma content_singleton[simp]: "content {a} = 0"
1.164 -proof -
1.165 -  have "content {a .. a} = 0"
1.166 -    by (subst content_closed_interval) auto
1.167 -  then show ?thesis by simp
1.168 -qed
1.169 -
1.170  lemma lmeasure_singleton[simp]:
1.171    fixes a :: "'a::ordered_euclidean_space" shows "emeasure lebesgue {a} = 0"
1.172    using lmeasure_atLeastAtMost[of a a] by simp
1.173 @@ -609,16 +573,6 @@
1.174
1.175  subsection {* Lebesgue integrable implies Gauge integrable *}
1.176
1.177 -lemma has_integral_cmult_real:
1.178 -  fixes c :: real
1.179 -  assumes "c \<noteq> 0 \<Longrightarrow> (f has_integral x) A"
1.180 -  shows "((\<lambda>x. c * f x) has_integral c * x) A"
1.181 -proof cases
1.182 -  assume "c \<noteq> 0"
1.183 -  from has_integral_cmul[OF assms[OF this], of c] show ?thesis
1.184 -    unfolding real_scaleR_def .
1.185 -qed simp
1.186 -
1.187  lemma simple_function_has_integral:
1.188    fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
1.189    assumes f:"simple_function lebesgue f"
1.190 @@ -657,10 +611,6 @@
1.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" .
1.192  qed fact
1.193
1.194 -lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
1.195 -  unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
1.196 -  using assms by auto
1.197 -
1.198  lemma simple_function_has_integral':
1.199    fixes f::"'a::ordered_euclidean_space \<Rightarrow> ereal"
1.200    assumes f: "simple_function lebesgue f" "\<And>x. 0 \<le> f x"
1.201 @@ -695,9 +645,6 @@
1.202    qed
1.203  qed
1.204
1.205 -lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
1.206 -  by (auto simp: indicator_def one_ereal_def)
1.207 -
1.208  lemma positive_integral_has_integral:
1.209    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
1.210    assumes f: "f \<in> borel_measurable lebesgue" "range f \<subseteq> {0..<\<infinity>}" "integral\<^isup>P lebesgue f \<noteq> \<infinity>"
1.211 @@ -843,12 +790,6 @@
1.212      unfolding lebesgue_integral_eq_borel[OF borel] by simp
1.213  qed
1.214
1.215 -lemma integrable_on_cmult_iff:
1.216 -  fixes c :: real assumes "c \<noteq> 0"
1.217 -  shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
1.218 -  using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
1.219 -  by auto
1.220 -
1.221  lemma positive_integral_lebesgue_has_integral:
1.222    fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
1.223    assumes f_borel: "f \<in> borel_measurable lebesgue" and nonneg: "\<And>x. 0 \<le> f x"
1.224 @@ -983,9 +924,6 @@
1.225  interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure" "{..<n}" for n :: nat
1.226    by default auto
1.227
1.228 -lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
1.229 -  by metis
1.230 -
1.231  lemma sets_product_borel:
1.232    assumes I: "finite I"
1.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")
```