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.87 -lemma indicator_add:
    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")