src/HOL/Probability/Lebesgue_Measure.thy
 changeset 41654 32fe42892983 parent 41546 2a12c23b7a34 child 41661 baf1964bc468
```     1.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jan 14 16:00:13 2011 +0100
1.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Jan 18 21:37:23 2011 +0100
1.3 @@ -1,7 +1,7 @@
1.4  (*  Author: Robert Himmelmann, TU Muenchen *)
1.5  header {* Lebsegue measure *}
1.6  theory Lebesgue_Measure
1.7 -  imports Product_Measure Gauge_Measure Complete_Measure
1.8 +  imports Product_Measure Complete_Measure
1.9  begin
1.10
1.11  subsection {* Standard Cubes *}
1.12 @@ -42,144 +42,165 @@
1.14  qed
1.15
1.16 -lemma Union_inter_cube:"\<Union>{s \<inter> cube n |n. n \<in> UNIV} = s"
1.17 -proof safe case goal1
1.18 -  from mem_big_cube[of x] guess n . note n=this
1.19 -  show ?case unfolding Union_iff apply(rule_tac x="s \<inter> cube n" in bexI)
1.20 -    using n goal1 by auto
1.21 -qed
1.22 +definition lebesgue :: "'a::ordered_euclidean_space algebra" where
1.23 +  "lebesgue = \<lparr> space = UNIV, sets = {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n} \<rparr>"
1.24 +
1.25 +lemma space_lebesgue[simp]: "space lebesgue = UNIV"
1.26 +  unfolding lebesgue_def by simp
1.27 +
1.28 +lemma lebesgueD: "A \<in> sets lebesgue \<Longrightarrow> (indicator A :: _ \<Rightarrow> real) integrable_on cube n"
1.29 +  unfolding lebesgue_def by simp
1.30 +
1.31 +lemma lebesgueI: "(\<And>n. (indicator A :: _ \<Rightarrow> real) integrable_on cube n) \<Longrightarrow> A \<in> sets lebesgue"
1.32 +  unfolding lebesgue_def by simp
1.33 +
1.34 +lemma absolutely_integrable_on_indicator[simp]:
1.35 +  fixes A :: "'a::ordered_euclidean_space set"
1.36 +  shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>
1.37 +    (indicator A :: _ \<Rightarrow> real) integrable_on X"
1.38 +  unfolding absolutely_integrable_on_def by simp
1.39 +
1.40 +lemma LIMSEQ_indicator_UN:
1.41 +  "(\<lambda>k. indicator (\<Union> i<k. A i) x) ----> (indicator (\<Union>i. A i) x :: real)"
1.42 +proof cases
1.43 +  assume "\<exists>i. x \<in> A i" then guess i .. note i = this
1.44 +  then have *: "\<And>n. (indicator (\<Union> i<n + Suc i. A i) x :: real) = 1"
1.45 +    "(indicator (\<Union> i. A i) x :: real) = 1" by (auto simp: indicator_def)
1.46 +  show ?thesis
1.47 +    apply (rule LIMSEQ_offset[of _ "Suc i"]) unfolding * by auto
1.48 +qed (auto simp: indicator_def)
1.49
1.50 -lemma gmeasurable_cube[intro]:"gmeasurable (cube n)"
1.51 -  unfolding cube_def by auto
1.53 +  "A \<inter> B = {} \<Longrightarrow> (indicator A x::_::monoid_add) + indicator B x = indicator (A \<union> B) x"
1.54 +  unfolding indicator_def by auto
1.55
1.56 -lemma gmeasure_le_inter_cube[intro]: fixes s::"'a::ordered_euclidean_space set"
1.57 -  assumes "gmeasurable (s \<inter> cube n)" shows "gmeasure (s \<inter> cube n) \<le> gmeasure (cube n::'a set)"
1.58 -  apply(rule has_gmeasure_subset[of "s\<inter>cube n" _ "cube n"])
1.59 -  unfolding has_gmeasure_measure[THEN sym] using assms by auto
1.60 +interpretation lebesgue: sigma_algebra lebesgue
1.61 +proof (intro sigma_algebra_iff2[THEN iffD2] conjI allI ballI impI lebesgueI)
1.62 +  fix A n assume A: "A \<in> sets lebesgue"
1.63 +  have "indicator (space lebesgue - A) = (\<lambda>x. 1 - indicator A x :: real)"
1.64 +    by (auto simp: fun_eq_iff indicator_def)
1.65 +  then show "(indicator (space lebesgue - A) :: _ \<Rightarrow> real) integrable_on cube n"
1.66 +    using A by (auto intro!: integrable_sub dest: lebesgueD simp: cube_def)
1.67 +next
1.68 +  fix n show "(indicator {} :: _\<Rightarrow>real) integrable_on cube n"
1.69 +    by (auto simp: cube_def indicator_def_raw)
1.70 +next
1.71 +  fix A :: "nat \<Rightarrow> 'a set" and n ::nat assume "range A \<subseteq> sets lebesgue"
1.72 +  then have A: "\<And>i. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
1.73 +    by (auto dest: lebesgueD)
1.74 +  show "(indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n" (is "?g integrable_on _")
1.75 +  proof (intro dominated_convergence[where g="?g"] ballI)
1.76 +    fix k show "(indicator (\<Union>i<k. A i) :: _ \<Rightarrow> real) integrable_on cube n"
1.77 +    proof (induct k)
1.78 +      case (Suc k)
1.79 +      have *: "(\<Union> i<Suc k. A i) = (\<Union> i<k. A i) \<union> A k"
1.80 +        unfolding lessThan_Suc UN_insert by auto
1.81 +      have *: "(\<lambda>x. max (indicator (\<Union> i<k. A i) x) (indicator (A k) x) :: real) =
1.82 +          indicator (\<Union> i<Suc k. A i)" (is "(\<lambda>x. max (?f x) (?g x)) = _")
1.83 +        by (auto simp: fun_eq_iff * indicator_def)
1.84 +      show ?case
1.85 +        using absolutely_integrable_max[of ?f "cube n" ?g] A Suc by (simp add: *)
1.86 +    qed auto
1.87 +  qed (auto intro: LIMSEQ_indicator_UN simp: cube_def)
1.88 +qed simp
1.89
1.90 -lemma has_gmeasure_cube[intro]: "(cube n::('a::ordered_euclidean_space) set)
1.91 -  has_gmeasure ((2 * real n) ^ (DIM('a)))"
1.92 -proof-
1.93 -  have "content {\<chi>\<chi> i. - real n..(\<chi>\<chi> i. real n)::'a} = (2 * real n) ^ (DIM('a))"
1.94 -    apply(subst content_closed_interval) defer
1.95 -    by (auto simp add:setprod_constant)
1.96 -  thus ?thesis unfolding cube_def
1.97 -    using has_gmeasure_interval(1)[of "(\<chi>\<chi> i. - real n)::'a" "(\<chi>\<chi> i. real n)::'a"]
1.98 -    by auto
1.99 -qed
1.100 +definition "lmeasure A = (SUP n. Real (integral (cube n) (indicator A)))"
1.101
1.102 -lemma gmeasure_cube_eq[simp]:
1.103 -  "gmeasure (cube n::('a::ordered_euclidean_space) set) = (2 * real n) ^ DIM('a)"
1.104 -  by (intro measure_unique) auto
1.105 -
1.106 -lemma gmeasure_cube_ge_n: "gmeasure (cube n::('a::ordered_euclidean_space) set) \<ge> real n"
1.107 -proof cases
1.108 -  assume "n = 0" then show ?thesis by simp
1.109 +interpretation lebesgue: measure_space lebesgue lmeasure
1.110 +proof
1.111 +  have *: "indicator {} = (\<lambda>x. 0 :: real)" by (simp add: fun_eq_iff)
1.112 +  show "lmeasure {} = 0" by (simp add: integral_0 * lmeasure_def)
1.113  next
1.114 -  assume "n \<noteq> 0"
1.115 -  have "real n \<le> (2 * real n)^1" by simp
1.116 -  also have "\<dots> \<le> (2 * real n)^DIM('a)"
1.117 -    using DIM_positive[where 'a='a] `n \<noteq> 0`
1.118 -    by (intro power_increasing) auto
1.119 -  also have "\<dots> = gmeasure (cube n::'a set)" by simp
1.120 -  finally show ?thesis .
1.121 +  show "countably_additive lebesgue lmeasure"
1.122 +  proof (intro countably_additive_def[THEN iffD2] allI impI)
1.123 +    fix A :: "nat \<Rightarrow> 'b set" assume rA: "range A \<subseteq> sets lebesgue" "disjoint_family A"
1.124 +    then have A[simp, intro]: "\<And>i n. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
1.125 +      by (auto dest: lebesgueD)
1.126 +    let "?m n i" = "integral (cube n) (indicator (A i) :: _\<Rightarrow>real)"
1.127 +    let "?M n I" = "integral (cube n) (indicator (\<Union>i\<in>I. A i) :: _\<Rightarrow>real)"
1.128 +    have nn[simp, intro]: "\<And>i n. 0 \<le> ?m n i" by (auto intro!: integral_nonneg)
1.129 +    assume "(\<Union>i. A i) \<in> sets lebesgue"
1.130 +    then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n"
1.131 +      by (auto dest: lebesgueD)
1.132 +    show "(\<Sum>\<^isub>\<infinity>n. lmeasure (A n)) = lmeasure (\<Union>i. A i)" unfolding lmeasure_def
1.133 +    proof (subst psuminf_SUP_eq)
1.134 +      fix n i show "Real (?m n i) \<le> Real (?m (Suc n) i)"
1.135 +        using cube_subset[of n "Suc n"] by (auto intro!: integral_subset_le)
1.136 +    next
1.137 +      show "(SUP n. \<Sum>\<^isub>\<infinity>i. Real (?m n i)) = (SUP n. Real (?M n UNIV))"
1.138 +        unfolding psuminf_def
1.139 +      proof (subst setsum_Real, (intro arg_cong[where f="SUPR UNIV"] ext ballI nn SUP_eq_LIMSEQ[THEN iffD2])+)
1.140 +        fix n :: nat show "mono (\<lambda>m. \<Sum>x<m. ?m n x)"
1.141 +        proof (intro mono_iff_le_Suc[THEN iffD2] allI)
1.142 +          fix m show "(\<Sum>x<m. ?m n x) \<le> (\<Sum>x<Suc m. ?m n x)"
1.143 +            using nn[of n m] by auto
1.144 +        qed
1.145 +        show "0 \<le> ?M n UNIV"
1.146 +          using UN_A by (auto intro!: integral_nonneg)
1.147 +        fix m show "0 \<le> (\<Sum>x<m. ?m n x)" by (auto intro!: setsum_nonneg)
1.148 +      next
1.149 +        fix n
1.150 +        have "\<And>m. (UNION {..<m} A) \<in> sets lebesgue" using rA by auto
1.151 +        from lebesgueD[OF this]
1.152 +        have "(\<lambda>m. ?M n {..< m}) ----> ?M n UNIV"
1.153 +          (is "(\<lambda>m. integral _ (?A m)) ----> ?I")
1.154 +          by (intro dominated_convergence(2)[where f="?A" and h="\<lambda>x. 1::real"])
1.155 +             (auto intro: LIMSEQ_indicator_UN simp: cube_def)
1.156 +        moreover
1.157 +        { fix m have *: "(\<Sum>x<m. ?m n x) = ?M n {..< m}"
1.158 +          proof (induct m)
1.159 +            case (Suc m)
1.160 +            have "(\<Union>i<m. A i) \<in> sets lebesgue" using rA by auto
1.161 +            then have "(indicator (\<Union>i<m. A i) :: _\<Rightarrow>real) integrable_on (cube n)"
1.162 +              by (auto dest!: lebesgueD)
1.163 +            moreover
1.164 +            have "(\<Union>i<m. A i) \<inter> A m = {}"
1.165 +              using rA(2)[unfolded disjoint_family_on_def, THEN bspec, of m]
1.166 +              by auto
1.167 +            then have "\<And>x. indicator (\<Union>i<Suc m. A i) x =
1.168 +              indicator (\<Union>i<m. A i) x + (indicator (A m) x :: real)"
1.169 +              by (auto simp: indicator_add lessThan_Suc ac_simps)
1.170 +            ultimately show ?case
1.172 +          qed auto }
1.173 +        ultimately show "(\<lambda>m. \<Sum>x<m. ?m n x) ----> ?M n UNIV"
1.174 +          by simp
1.175 +      qed
1.176 +    qed
1.177 +  qed
1.178  qed
1.179
1.180 -lemma gmeasure_setsum:
1.181 -  assumes "finite A" and "\<And>s t. s \<in> A \<Longrightarrow> t \<in> A \<Longrightarrow> s \<noteq> t \<Longrightarrow> f s \<inter> f t = {}"
1.182 -    and "\<And>i. i \<in> A \<Longrightarrow> gmeasurable (f i)"
1.183 -  shows "gmeasure (\<Union>i\<in>A. f i) = (\<Sum>i\<in>A. gmeasure (f i))"
1.184 +lemma has_integral_interval_cube:
1.185 +  fixes a b :: "'a::ordered_euclidean_space"
1.186 +  shows "(indicator {a .. b} has_integral
1.187 +    content ({\<chi>\<chi> i. max (- real n) (a \$\$ i) .. \<chi>\<chi> i. min (real n) (b \$\$ i)} :: 'a set)) (cube n)"
1.188 +    (is "(?I has_integral content ?R) (cube n)")
1.189  proof -
1.190 -  have "gmeasure (\<Union>i\<in>A. f i) = gmeasure (\<Union>f ` A)" by auto
1.191 -  also have "\<dots> = setsum gmeasure (f ` A)" using assms
1.192 -  proof (intro measure_negligible_unions)
1.193 -    fix X Y assume "X \<in> f`A" "Y \<in> f`A" "X \<noteq> Y"
1.194 -    then have "X \<inter> Y = {}" using assms by auto
1.195 -    then show "negligible (X \<inter> Y)" by auto
1.196 -  qed auto
1.197 -  also have "\<dots> = setsum gmeasure (f ` A - {{}})"
1.198 -    using assms by (intro setsum_mono_zero_cong_right) auto
1.199 -  also have "\<dots> = (\<Sum>i\<in>A - {i. f i = {}}. gmeasure (f i))"
1.200 -  proof (intro setsum_reindex_cong inj_onI)
1.201 -    fix s t assume *: "s \<in> A - {i. f i = {}}" "t \<in> A - {i. f i = {}}" "f s = f t"
1.202 -    show "s = t"
1.203 -    proof (rule ccontr)
1.204 -      assume "s \<noteq> t" with assms(2)[of s t] * show False by auto
1.205 -    qed
1.206 -  qed auto
1.207 -  also have "\<dots> = (\<Sum>i\<in>A. gmeasure (f i))"
1.208 -    using assms by (intro setsum_mono_zero_cong_left) auto
1.209 -  finally show ?thesis .
1.210 -qed
1.211 -
1.212 -lemma gmeasurable_finite_UNION[intro]:
1.213 -  assumes "\<And>i. i \<in> S \<Longrightarrow> gmeasurable (A i)" "finite S"
1.214 -  shows "gmeasurable (\<Union>i\<in>S. A i)"
1.215 -  unfolding UNION_eq_Union_image using assms
1.216 -  by (intro gmeasurable_finite_unions) auto
1.217 -
1.218 -lemma gmeasurable_countable_UNION[intro]:
1.219 -  fixes A :: "nat \<Rightarrow> ('a::ordered_euclidean_space) set"
1.220 -  assumes measurable: "\<And>i. gmeasurable (A i)"
1.221 -    and finite: "\<And>n. gmeasure (UNION {.. n} A) \<le> B"
1.222 -  shows "gmeasurable (\<Union>i. A i)"
1.223 -proof -
1.224 -  have *: "\<And>n. \<Union>{A k |k. k \<le> n} = (\<Union>i\<le>n. A i)"
1.225 -    "(\<Union>{A n |n. n \<in> UNIV}) = (\<Union>i. A i)" by auto
1.226 -  show ?thesis
1.227 -    by (rule gmeasurable_countable_unions_strong[of A B, unfolded *, OF assms])
1.228 +  let "{?N .. ?P}" = ?R
1.229 +  have [simp]: "(\<lambda>x. if x \<in> cube n then ?I x else 0) = indicator ?R"
1.230 +    by (auto simp: indicator_def cube_def fun_eq_iff eucl_le[where 'a='a])
1.231 +  have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
1.232 +    unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
1.233 +  also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
1.234 +    unfolding indicator_def_raw has_integral_restrict_univ ..
1.235 +  finally show ?thesis
1.236 +    using has_integral_const[of "1::real" "?N" "?P"] by simp
1.237  qed
1.238
1.239 -subsection {* Measurability *}
1.240 -
1.241 -definition lebesgue :: "'a::ordered_euclidean_space algebra" where
1.242 -  "lebesgue = \<lparr> space = UNIV, sets = {A. \<forall>n. gmeasurable (A \<inter> cube n)} \<rparr>"
1.243 -
1.244 -lemma space_lebesgue[simp]:"space lebesgue = UNIV"
1.245 -  unfolding lebesgue_def by auto
1.246 -
1.247 -lemma lebesgueD[dest]: assumes "S \<in> sets lebesgue"
1.248 -  shows "\<And>n. gmeasurable (S \<inter> cube n)"
1.249 -  using assms unfolding lebesgue_def by auto
1.250 -
1.251 -lemma lebesgueI[intro]: assumes "gmeasurable S"
1.252 -  shows "S \<in> sets lebesgue" unfolding lebesgue_def cube_def
1.253 -  using assms gmeasurable_interval by auto
1.254 -
1.255 -lemma lebesgueI2: "(\<And>n. gmeasurable (S \<inter> cube n)) \<Longrightarrow> S \<in> sets lebesgue"
1.256 -  using assms unfolding lebesgue_def by auto
1.257 -
1.258 -interpretation lebesgue: sigma_algebra lebesgue
1.259 -proof
1.260 -  show "sets lebesgue \<subseteq> Pow (space lebesgue)"
1.261 -    unfolding lebesgue_def by auto
1.262 -  show "{} \<in> sets lebesgue"
1.263 -    using gmeasurable_empty by auto
1.264 -  { fix A B :: "'a set" assume "A \<in> sets lebesgue" "B \<in> sets lebesgue"
1.265 -    then show "A \<union> B \<in> sets lebesgue"
1.266 -      by (auto intro: gmeasurable_union simp: lebesgue_def Int_Un_distrib2) }
1.267 -  { fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets lebesgue"
1.268 -    show "(\<Union>i. A i) \<in> sets lebesgue"
1.269 -    proof (rule lebesgueI2)
1.270 -      fix n show "gmeasurable ((\<Union>i. A i) \<inter> cube n)" unfolding UN_extend_simps
1.271 -        using A
1.272 -        by (intro gmeasurable_countable_UNION[where B="gmeasure (cube n::'a set)"])
1.273 -           (auto intro!: measure_subset gmeasure_setsum simp: UN_extend_simps simp del: gmeasure_cube_eq UN_simps)
1.274 -    qed }
1.275 -  { fix A assume A: "A \<in> sets lebesgue" show "space lebesgue - A \<in> sets lebesgue"
1.276 -    proof (rule lebesgueI2)
1.277 -      fix n
1.278 -      have *: "(space lebesgue - A) \<inter> cube n = cube n - (A \<inter> cube n)"
1.279 -        unfolding lebesgue_def by auto
1.280 -      show "gmeasurable ((space lebesgue - A) \<inter> cube n)" unfolding *
1.281 -        using A by (auto intro!: gmeasurable_diff)
1.282 -    qed }
1.283 -qed
1.284 -
1.285 -lemma lebesgueI_borel[intro, simp]: fixes s::"'a::ordered_euclidean_space set"
1.286 +lemma lebesgueI_borel[intro, simp]:
1.287 +  fixes s::"'a::ordered_euclidean_space set"
1.288    assumes "s \<in> sets borel" shows "s \<in> sets lebesgue"
1.289 -proof- let ?S = "range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)})"
1.290 -  have *:"?S \<subseteq> sets lebesgue" by auto
1.291 +proof -
1.292 +  let ?S = "range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)})"
1.293 +  have *:"?S \<subseteq> sets lebesgue"
1.294 +  proof (safe intro!: lebesgueI)
1.295 +    fix n :: nat and a b :: 'a
1.296 +    let ?N = "\<chi>\<chi> i. max (- real n) (a \$\$ i)"
1.297 +    let ?P = "\<chi>\<chi> i. min (real n) (b \$\$ i)"
1.298 +    show "(indicator {a..b} :: 'a\<Rightarrow>real) integrable_on cube n"
1.299 +      unfolding integrable_on_def
1.300 +      using has_integral_interval_cube[of a b] by auto
1.301 +  qed
1.302    have "s \<in> sigma_sets UNIV ?S" using assms
1.303      unfolding borel_eq_atLeastAtMost by (simp add: sigma_def)
1.304    thus ?thesis
1.305 @@ -189,171 +210,153 @@
1.306
1.307  lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set"
1.308    assumes "negligible s" shows "s \<in> sets lebesgue"
1.309 -proof (rule lebesgueI2)
1.310 -  fix n
1.311 -  have *:"\<And>x. (if x \<in> cube n then indicator s x else 0) = (if x \<in> s \<inter> cube n then 1 else 0)"
1.312 -    unfolding indicator_def_raw by auto
1.313 -  note assms[unfolded negligible_def,rule_format,of "(\<chi>\<chi> i. - real n)::'a" "\<chi>\<chi> i. real n"]
1.314 -  thus "gmeasurable (s \<inter> cube n)" apply-apply(rule gmeasurableI[of _ 0]) unfolding has_gmeasure_def
1.315 -    apply(subst(asm) has_integral_restrict_univ[THEN sym]) unfolding cube_def[symmetric]
1.316 -    apply(subst has_integral_restrict_univ[THEN sym]) unfolding * .
1.317 -qed
1.318 +  using assms by (force simp: cube_def integrable_on_def negligible_def intro!: lebesgueI)
1.319
1.320 -section {* The Lebesgue Measure *}
1.321 -
1.322 -definition "lmeasure A = (SUP n. Real (gmeasure (A \<inter> cube n)))"
1.323 -
1.324 -lemma lmeasure_eq_0: assumes "negligible S" shows "lmeasure S = 0"
1.325 +lemma lmeasure_eq_0:
1.326 +  fixes S :: "'a::ordered_euclidean_space set" assumes "negligible S" shows "lmeasure S = 0"
1.327  proof -
1.328 -  from lebesgueI_negligible[OF assms]
1.329 -  have "\<And>n. gmeasurable (S \<inter> cube n)" by auto
1.330 -  from gmeasurable_measure_eq_0[OF this]
1.331 -  have "\<And>n. gmeasure (S \<inter> cube n) = 0" using assms by auto
1.332 -  then show ?thesis unfolding lmeasure_def by simp
1.333 +  have "\<And>n. integral (cube n) (indicator S :: 'a\<Rightarrow>real) = 0"
1.334 +    unfolding integral_def using assms
1.335 +    by (intro some1_equality ex_ex1I has_integral_unique)
1.336 +       (auto simp: cube_def negligible_def intro: )
1.337 +  then show ?thesis unfolding lmeasure_def by auto
1.338  qed
1.339
1.340  lemma lmeasure_iff_LIMSEQ:
1.341    assumes "A \<in> sets lebesgue" "0 \<le> m"
1.342 -  shows "lmeasure A = Real m \<longleftrightarrow> (\<lambda>n. (gmeasure (A \<inter> cube n))) ----> m"
1.343 -  unfolding lmeasure_def using assms cube_subset[where 'a='a]
1.344 -  by (intro SUP_eq_LIMSEQ monoI measure_subset) force+
1.345 +  shows "lmeasure A = Real m \<longleftrightarrow> (\<lambda>n. integral (cube n) (indicator A :: _ \<Rightarrow> real)) ----> m"
1.346 +  unfolding lmeasure_def
1.347 +proof (intro SUP_eq_LIMSEQ)
1.348 +  show "mono (\<lambda>n. integral (cube n) (indicator A::_=>real))"
1.349 +    using cube_subset assms by (intro monoI integral_subset_le) (auto dest!: lebesgueD)
1.350 +  fix n show "0 \<le> integral (cube n) (indicator A::_=>real)"
1.351 +    using assms by (auto dest!: lebesgueD intro!: integral_nonneg)
1.352 +qed fact
1.353
1.354 -interpretation lebesgue: measure_space lebesgue lmeasure
1.355 -proof
1.356 -  show "lmeasure {} = 0"
1.357 -    by (auto intro!: lmeasure_eq_0)
1.358 -  show "countably_additive lebesgue lmeasure"
1.359 -  proof (unfold countably_additive_def, intro allI impI conjI)
1.360 -    fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets lebesgue" "disjoint_family A"
1.361 -    then have A: "\<And>i. A i \<in> sets lebesgue" by auto
1.362 -    show "(\<Sum>\<^isub>\<infinity>n. lmeasure (A n)) = lmeasure (\<Union>i. A i)" unfolding lmeasure_def
1.363 -    proof (subst psuminf_SUP_eq)
1.364 -      { fix i n
1.365 -        have "gmeasure (A i \<inter> cube n) \<le> gmeasure (A i \<inter> cube (Suc n))"
1.366 -          using A cube_subset[of n "Suc n"] by (auto intro!: measure_subset)
1.367 -        then show "Real (gmeasure (A i \<inter> cube n)) \<le> Real (gmeasure (A i \<inter> cube (Suc n)))"
1.368 -          by auto }
1.369 -      show "(SUP n. \<Sum>\<^isub>\<infinity>i. Real (gmeasure (A i \<inter> cube n))) = (SUP n. Real (gmeasure ((\<Union>i. A i) \<inter> cube n)))"
1.370 -      proof (intro arg_cong[where f="SUPR UNIV"] ext)
1.371 -        fix n
1.372 -        have sums: "(\<lambda>i. gmeasure (A i \<inter> cube n)) sums gmeasure (\<Union>{A i \<inter> cube n |i. i \<in> UNIV})"
1.373 -        proof (rule has_gmeasure_countable_negligible_unions(2))
1.374 -          fix i show "gmeasurable (A i \<inter> cube n)" using A by auto
1.375 -        next
1.376 -          fix i m :: nat assume "m \<noteq> i"
1.377 -          then have "A m \<inter> cube n \<inter> (A i \<inter> cube n) = {}"
1.378 -            using `disjoint_family A` unfolding disjoint_family_on_def by auto
1.379 -          then show "negligible (A m \<inter> cube n \<inter> (A i \<inter> cube n))" by auto
1.380 -        next
1.381 -          fix i
1.382 -          have "(\<Sum>k = 0..i. gmeasure (A k \<inter> cube n)) = gmeasure (\<Union>k\<le>i . A k \<inter> cube n)"
1.383 -            unfolding atLeast0AtMost using A
1.384 -          proof (intro gmeasure_setsum[symmetric])
1.385 -            fix s t :: nat assume "s \<noteq> t" then have "A t \<inter> A s = {}"
1.386 -              using `disjoint_family A` unfolding disjoint_family_on_def by auto
1.387 -            then show "A s \<inter> cube n \<inter> (A t \<inter> cube n) = {}" by auto
1.388 -          qed auto
1.389 -          also have "\<dots> \<le> gmeasure (cube n :: 'b set)" using A
1.390 -            by (intro measure_subset gmeasurable_finite_UNION) auto
1.391 -          finally show "(\<Sum>k = 0..i. gmeasure (A k \<inter> cube n)) \<le> gmeasure (cube n :: 'b set)" .
1.392 -        qed
1.393 -        show "(\<Sum>\<^isub>\<infinity>i. Real (gmeasure (A i \<inter> cube n))) = Real (gmeasure ((\<Union>i. A i) \<inter> cube n))"
1.394 -          unfolding psuminf_def
1.395 -          apply (subst setsum_Real)
1.396 -          apply (simp add: measure_pos_le)
1.397 -        proof (rule SUP_eq_LIMSEQ[THEN iffD2])
1.398 -          have "(\<Union>{A i \<inter> cube n |i. i \<in> UNIV}) = (\<Union>i. A i) \<inter> cube n" by auto
1.399 -          with sums show "(\<lambda>i. \<Sum>k<i. gmeasure (A k \<inter> cube n)) ----> gmeasure ((\<Union>i. A i) \<inter> cube n)"
1.400 -            unfolding sums_def atLeast0LessThan by simp
1.401 -        qed (auto intro!: monoI setsum_nonneg setsum_mono2)
1.402 -      qed
1.403 -    qed
1.404 -  qed
1.405 +lemma has_integral_indicator_UNIV:
1.406 +  fixes s A :: "'a::ordered_euclidean_space set" and x :: real
1.407 +  shows "((indicator (s \<inter> A) :: 'a\<Rightarrow>real) has_integral x) UNIV = ((indicator s :: _\<Rightarrow>real) has_integral x) A"
1.408 +proof -
1.409 +  have "(\<lambda>x. if x \<in> A then indicator s x else 0) = (indicator (s \<inter> A) :: _\<Rightarrow>real)"
1.410 +    by (auto simp: fun_eq_iff indicator_def)
1.411 +  then show ?thesis
1.412 +    unfolding has_integral_restrict_univ[where s=A, symmetric] by simp
1.413  qed
1.414
1.415 -lemma lmeasure_finite_has_gmeasure: assumes "s \<in> sets lebesgue" "lmeasure s = Real m" "0 \<le> m"
1.416 -  shows "s has_gmeasure m"
1.417 -proof-
1.418 -  have *:"(\<lambda>n. (gmeasure (s \<inter> cube n))) ----> m"
1.419 -    using `lmeasure s = Real m` unfolding lmeasure_iff_LIMSEQ[OF `s \<in> sets lebesgue` `0 \<le> m`] .
1.420 -  have s: "\<And>n. gmeasurable (s \<inter> cube n)" using assms by auto
1.421 -  have "(\<lambda>x. if x \<in> s then 1 else (0::real)) integrable_on UNIV \<and>
1.422 -    (\<lambda>k. integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)))
1.423 -    ----> integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)"
1.424 -  proof(rule monotone_convergence_increasing)
1.425 -    have "lmeasure s \<le> Real m" using `lmeasure s = Real m` by simp
1.426 -    then have "\<forall>n. gmeasure (s \<inter> cube n) \<le> m"
1.427 -      unfolding lmeasure_def complete_lattice_class.SUP_le_iff
1.428 -      using `0 \<le> m` by (auto simp: measure_pos_le)
1.429 -    thus *:"bounded {integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)) |k. True}"
1.430 -      unfolding integral_measure_univ[OF s] bounded_def apply-
1.431 -      apply(rule_tac x=0 in exI,rule_tac x=m in exI) unfolding dist_real_def
1.432 -      by (auto simp: measure_pos_le)
1.433 -    show "\<forall>k. (\<lambda>x. if x \<in> s \<inter> cube k then (1::real) else 0) integrable_on UNIV"
1.434 -      unfolding integrable_restrict_univ
1.435 -      using s unfolding gmeasurable_def has_gmeasure_def by auto
1.436 -    have *:"\<And>n. n \<le> Suc n" by auto
1.437 -    show "\<forall>k. \<forall>x\<in>UNIV. (if x \<in> s \<inter> cube k then 1 else 0) \<le> (if x \<in> s \<inter> cube (Suc k) then 1 else (0::real))"
1.438 -      using cube_subset[OF *] by fastsimp
1.439 -    show "\<forall>x\<in>UNIV. (\<lambda>k. if x \<in> s \<inter> cube k then 1 else 0) ----> (if x \<in> s then 1 else (0::real))"
1.440 -      unfolding Lim_sequentially
1.441 -    proof safe case goal1 from real_arch_lt[of "norm x"] guess N .. note N = this
1.442 -      show ?case apply(rule_tac x=N in exI)
1.443 -      proof safe case goal1
1.444 -        have "x \<in> cube n" using cube_subset[OF goal1] N
1.445 -          using ball_subset_cube[of N] by(auto simp: dist_norm)
1.446 -        thus ?case using `e>0` by auto
1.447 -      qed
1.448 -    qed
1.449 -  qed note ** = conjunctD2[OF this]
1.450 -  hence *:"m = integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)" apply-
1.451 -    apply(rule LIMSEQ_unique[OF _ **(2)]) unfolding measure_integral_univ[THEN sym,OF s] using * .
1.452 -  show ?thesis unfolding has_gmeasure * apply(rule integrable_integral) using ** by auto
1.453 +lemma
1.454 +  fixes s a :: "'a::ordered_euclidean_space set"
1.455 +  shows integral_indicator_UNIV:
1.456 +    "integral UNIV (indicator (s \<inter> A) :: 'a\<Rightarrow>real) = integral A (indicator s :: _\<Rightarrow>real)"
1.457 +  and integrable_indicator_UNIV:
1.458 +    "(indicator (s \<inter> A) :: 'a\<Rightarrow>real) integrable_on UNIV \<longleftrightarrow> (indicator s :: 'a\<Rightarrow>real) integrable_on A"
1.459 +  unfolding integral_def integrable_on_def has_integral_indicator_UNIV by auto
1.460 +
1.461 +lemma lmeasure_finite_has_integral:
1.462 +  fixes s :: "'a::ordered_euclidean_space set"
1.463 +  assumes "s \<in> sets lebesgue" "lmeasure s = Real m" "0 \<le> m"
1.464 +  shows "(indicator s has_integral m) UNIV"
1.465 +proof -
1.466 +  let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real"
1.467 +  have **: "(?I s) integrable_on UNIV \<and> (\<lambda>k. integral UNIV (?I (s \<inter> cube k))) ----> integral UNIV (?I s)"
1.468 +  proof (intro monotone_convergence_increasing allI ballI)
1.469 +    have LIMSEQ: "(\<lambda>n. integral (cube n) (?I s)) ----> m"
1.470 +      using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1, 3)] .
1.471 +    { fix n have "integral (cube n) (?I s) \<le> m"
1.472 +        using cube_subset assms
1.473 +        by (intro incseq_le[where L=m] LIMSEQ incseq_def[THEN iffD2] integral_subset_le allI impI)
1.474 +           (auto dest!: lebesgueD) }
1.475 +    moreover
1.476 +    { fix n have "0 \<le> integral (cube n) (?I s)"
1.477 +      using assms by (auto dest!: lebesgueD intro!: integral_nonneg) }
1.478 +    ultimately
1.479 +    show "bounded {integral UNIV (?I (s \<inter> cube k)) |k. True}"
1.480 +      unfolding bounded_def
1.481 +      apply (rule_tac exI[of _ 0])
1.482 +      apply (rule_tac exI[of _ m])
1.483 +      by (auto simp: dist_real_def integral_indicator_UNIV)
1.484 +    fix k show "?I (s \<inter> cube k) integrable_on UNIV"
1.485 +      unfolding integrable_indicator_UNIV using assms by (auto dest!: lebesgueD)
1.486 +    fix x show "?I (s \<inter> cube k) x \<le> ?I (s \<inter> cube (Suc k)) x"
1.487 +      using cube_subset[of k "Suc k"] by (auto simp: indicator_def)
1.488 +  next
1.489 +    fix x :: 'a
1.490 +    from mem_big_cube obtain k where k: "x \<in> cube k" .
1.491 +    { fix n have "?I (s \<inter> cube (n + k)) x = ?I s x"
1.492 +      using k cube_subset[of k "n + k"] by (auto simp: indicator_def) }
1.493 +    note * = this
1.494 +    show "(\<lambda>k. ?I (s \<inter> cube k) x) ----> ?I s x"
1.495 +      by (rule LIMSEQ_offset[where k=k]) (auto simp: *)
1.496 +  qed
1.497 +  note ** = conjunctD2[OF this]
1.498 +  have m: "m = integral UNIV (?I s)"
1.499 +    apply (intro LIMSEQ_unique[OF _ **(2)])
1.500 +    using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1,3)] integral_indicator_UNIV .
1.501 +  show ?thesis
1.502 +    unfolding m by (intro integrable_integral **)
1.503  qed
1.504
1.505 -lemma lmeasure_finite_gmeasurable: assumes "s \<in> sets lebesgue" "lmeasure s \<noteq> \<omega>"
1.506 -  shows "gmeasurable s"
1.507 +lemma lmeasure_finite_integrable: assumes "s \<in> sets lebesgue" "lmeasure s \<noteq> \<omega>"
1.508 +  shows "(indicator s :: _ \<Rightarrow> real) integrable_on UNIV"
1.509  proof (cases "lmeasure s")
1.510 -  case (preal m) from lmeasure_finite_has_gmeasure[OF `s \<in> sets lebesgue` this]
1.511 -  show ?thesis unfolding gmeasurable_def by auto
1.512 +  case (preal m) from lmeasure_finite_has_integral[OF `s \<in> sets lebesgue` this]
1.513 +  show ?thesis unfolding integrable_on_def by auto
1.514  qed (insert assms, auto)
1.515
1.516 -lemma has_gmeasure_lmeasure: assumes "s has_gmeasure m"
1.517 -  shows "lmeasure s = Real m"
1.518 -proof-
1.519 -  have gmea:"gmeasurable s" using assms by auto
1.520 -  then have s: "s \<in> sets lebesgue" by auto
1.521 -  have m:"m \<ge> 0" using assms by auto
1.522 -  have *:"m = gmeasure (\<Union>{s \<inter> cube n |n. n \<in> UNIV})" unfolding Union_inter_cube
1.523 -    using assms by(rule measure_unique[THEN sym])
1.524 -  show ?thesis
1.525 -    unfolding lmeasure_iff_LIMSEQ[OF s `0 \<le> m`] unfolding *
1.526 -    apply(rule gmeasurable_nested_unions[THEN conjunct2, where B1="gmeasure s"])
1.527 -  proof- fix n::nat show *:"gmeasurable (s \<inter> cube n)"
1.528 -      using gmeasurable_inter[OF gmea gmeasurable_cube] .
1.529 -    show "gmeasure (s \<inter> cube n) \<le> gmeasure s" apply(rule measure_subset)
1.530 -      apply(rule * gmea)+ by auto
1.531 -    show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)" using cube_subset[of n "Suc n"] by auto
1.532 -  qed
1.533 +lemma has_integral_lebesgue: assumes "((indicator s :: _\<Rightarrow>real) has_integral m) UNIV"
1.534 +  shows "s \<in> sets lebesgue"
1.535 +proof (intro lebesgueI)
1.536 +  let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real"
1.537 +  fix n show "(?I s) integrable_on cube n" unfolding cube_def
1.538 +  proof (intro integrable_on_subinterval)
1.539 +    show "(?I s) integrable_on UNIV"
1.540 +      unfolding integrable_on_def using assms by auto
1.541 +  qed auto
1.542  qed
1.543
1.544 -lemma has_gmeasure_iff_lmeasure:
1.545 -  "A has_gmeasure m \<longleftrightarrow> (A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m)"
1.546 +lemma has_integral_lmeasure: assumes "((indicator s :: _\<Rightarrow>real) has_integral m) UNIV"
1.547 +  shows "lmeasure s = Real m"
1.548 +proof (intro lmeasure_iff_LIMSEQ[THEN iffD2])
1.549 +  let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real"
1.550 +  show "s \<in> sets lebesgue" using has_integral_lebesgue[OF assms] .
1.551 +  show "0 \<le> m" using assms by (rule has_integral_nonneg) auto
1.552 +  have "(\<lambda>n. integral UNIV (?I (s \<inter> cube n))) ----> integral UNIV (?I s)"
1.553 +  proof (intro dominated_convergence(2) ballI)
1.554 +    show "(?I s) integrable_on UNIV" unfolding integrable_on_def using assms by auto
1.555 +    fix n show "?I (s \<inter> cube n) integrable_on UNIV"
1.556 +      unfolding integrable_indicator_UNIV using `s \<in> sets lebesgue` by (auto dest: lebesgueD)
1.557 +    fix x show "norm (?I (s \<inter> cube n) x) \<le> ?I s x" by (auto simp: indicator_def)
1.558 +  next
1.559 +    fix x :: 'a
1.560 +    from mem_big_cube obtain k where k: "x \<in> cube k" .
1.561 +    { fix n have "?I (s \<inter> cube (n + k)) x = ?I s x"
1.562 +      using k cube_subset[of k "n + k"] by (auto simp: indicator_def) }
1.563 +    note * = this
1.564 +    show "(\<lambda>k. ?I (s \<inter> cube k) x) ----> ?I s x"
1.565 +      by (rule LIMSEQ_offset[where k=k]) (auto simp: *)
1.566 +  qed
1.567 +  then show "(\<lambda>n. integral (cube n) (?I s)) ----> m"
1.568 +    unfolding integral_unique[OF assms] integral_indicator_UNIV by simp
1.569 +qed
1.570 +
1.571 +lemma has_integral_iff_lmeasure:
1.572 +  "(indicator A has_integral m) UNIV \<longleftrightarrow> (A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m)"
1.573  proof
1.574 -  assume "A has_gmeasure m"
1.575 -  with has_gmeasure_lmeasure[OF this]
1.576 -  have "gmeasurable A" "0 \<le> m" "lmeasure A = Real m" by auto
1.577 -  then show "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m" by auto
1.578 +  assume "(indicator A has_integral m) UNIV"
1.579 +  with has_integral_lmeasure[OF this] has_integral_lebesgue[OF this]
1.580 +  show "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m"
1.581 +    by (auto intro: has_integral_nonneg)
1.582  next
1.583    assume "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m"
1.584 -  then show "A has_gmeasure m" by (intro lmeasure_finite_has_gmeasure) auto
1.585 +  then show "(indicator A has_integral m) UNIV" by (intro lmeasure_finite_has_integral) auto
1.586  qed
1.587
1.588 -lemma gmeasure_lmeasure: assumes "gmeasurable s" shows "lmeasure s = Real (gmeasure s)"
1.589 -proof -
1.590 -  note has_gmeasure_measureI[OF assms]
1.591 -  note has_gmeasure_lmeasure[OF this]
1.592 -  thus ?thesis .
1.593 +lemma lmeasure_eq_integral: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV"
1.594 +  shows "lmeasure s = Real (integral UNIV (indicator s))"
1.595 +  using assms unfolding integrable_on_def
1.596 +proof safe
1.597 +  fix y :: real assume "(indicator s has_integral y) UNIV"
1.598 +  from this[unfolded has_integral_iff_lmeasure] integral_unique[OF this]
1.599 +  show "lmeasure s = Real (integral UNIV (indicator s))" by simp
1.600  qed
1.601
1.602  lemma lebesgue_simple_function_indicator:
1.603 @@ -362,12 +365,12 @@
1.604    shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))"
1.605    apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto
1.606
1.607 -lemma lmeasure_gmeasure:
1.608 -  "gmeasurable s \<Longrightarrow> gmeasure s = real (lmeasure s)"
1.609 -  by (subst gmeasure_lmeasure) auto
1.610 +lemma integral_eq_lmeasure:
1.611 +  "(indicator s::_\<Rightarrow>real) integrable_on UNIV \<Longrightarrow> integral UNIV (indicator s) = real (lmeasure s)"
1.612 +  by (subst lmeasure_eq_integral) (auto intro!: integral_nonneg)
1.613
1.614 -lemma lmeasure_finite: assumes "gmeasurable s" shows "lmeasure s \<noteq> \<omega>"
1.615 -  using gmeasure_lmeasure[OF assms] by auto
1.616 +lemma lmeasure_finite: assumes "(indicator s::_\<Rightarrow>real) integrable_on UNIV" shows "lmeasure s \<noteq> \<omega>"
1.617 +  using lmeasure_eq_integral[OF assms] by auto
1.618
1.619  lemma negligible_iff_lebesgue_null_sets:
1.620    "negligible A \<longleftrightarrow> A \<in> lebesgue.null_sets"
1.621 @@ -377,35 +380,65 @@
1.622    show "A \<in> lebesgue.null_sets" by auto
1.623  next
1.624    assume A: "A \<in> lebesgue.null_sets"
1.625 -  then have *:"gmeasurable A" using lmeasure_finite_gmeasurable[of A] by auto
1.626 -  show "negligible A"
1.627 -    unfolding gmeasurable_measure_eq_0[OF *, symmetric]
1.628 -    unfolding lmeasure_gmeasure[OF *] using A by auto
1.629 +  then have *:"((indicator A) has_integral (0::real)) UNIV" using lmeasure_finite_has_integral[of A] by auto
1.630 +  show "negligible A" unfolding negligible_def
1.631 +  proof (intro allI)
1.632 +    fix a b :: 'a
1.633 +    have integrable: "(indicator A :: _\<Rightarrow>real) integrable_on {a..b}"
1.634 +      by (intro integrable_on_subinterval has_integral_integrable) (auto intro: *)
1.635 +    then have "integral {a..b} (indicator A) \<le> (integral UNIV (indicator A) :: real)"
1.636 +      using * by (auto intro!: integral_subset_le has_integral_integrable)
1.637 +    moreover have "(0::real) \<le> integral {a..b} (indicator A)"
1.638 +      using integrable by (auto intro!: integral_nonneg)
1.639 +    ultimately have "integral {a..b} (indicator A) = (0::real)"
1.640 +      using integral_unique[OF *] by auto
1.641 +    then show "(indicator A has_integral (0::real)) {a..b}"
1.642 +      using integrable_integral[OF integrable] by simp
1.643 +  qed
1.644 +qed
1.645 +
1.646 +lemma integral_const[simp]:
1.647 +  fixes a b :: "'a::ordered_euclidean_space"
1.648 +  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
1.649 +  by (rule integral_unique) (rule has_integral_const)
1.650 +
1.651 +lemma lmeasure_UNIV[intro]: "lmeasure (UNIV::'a::ordered_euclidean_space set) = \<omega>"
1.652 +  unfolding lmeasure_def SUP_\<omega>
1.653 +proof (intro allI impI)
1.654 +  fix x assume "x < \<omega>"
1.655 +  then obtain r where r: "x = Real r" "0 \<le> r" by (cases x) auto
1.656 +  then obtain n where n: "r < of_nat n" using ex_less_of_nat by auto
1.657 +  show "\<exists>i\<in>UNIV. x < Real (integral (cube i) (indicator UNIV::'a\<Rightarrow>real))"
1.658 +  proof (intro bexI[of _ n])
1.659 +    have [simp]: "indicator UNIV = (\<lambda>x. 1)" by (auto simp: fun_eq_iff)
1.660 +    { fix m :: nat assume "0 < m" then have "real n \<le> (\<Prod>x<m. 2 * real n)"
1.661 +      proof (induct m)
1.662 +        case (Suc m)
1.663 +        show ?case
1.664 +        proof cases
1.665 +          assume "m = 0" then show ?thesis by (simp add: lessThan_Suc)
1.666 +        next
1.667 +          assume "m \<noteq> 0" then have "real n \<le> (\<Prod>x<m. 2 * real n)" using Suc by auto
1.668 +          then show ?thesis
1.669 +            by (auto simp: lessThan_Suc field_simps mult_le_cancel_left1)
1.670 +        qed
1.671 +      qed auto } note this[OF DIM_positive[where 'a='a], simp]
1.672 +    then have [simp]: "0 \<le> (\<Prod>x<DIM('a). 2 * real n)" using real_of_nat_ge_zero by arith
1.673 +    have "x < Real (of_nat n)" using n r by auto
1.674 +    also have "Real (of_nat n) \<le> Real (integral (cube n) (indicator UNIV::'a\<Rightarrow>real))"
1.675 +      by (auto simp: real_eq_of_nat[symmetric] cube_def content_closed_interval_cases)
1.676 +    finally show "x < Real (integral (cube n) (indicator UNIV::'a\<Rightarrow>real))" .
1.677 +  qed auto
1.678  qed
1.679
1.680  lemma
1.681    fixes a b ::"'a::ordered_euclidean_space"
1.682    shows lmeasure_atLeastAtMost[simp]: "lmeasure {a..b} = Real (content {a..b})"
1.683 -    and lmeasure_greaterThanLessThan[simp]: "lmeasure {a <..< b} = Real (content {a..b})"
1.684 -  using has_gmeasure_interval[of a b] by (auto intro!: has_gmeasure_lmeasure)
1.685 -
1.686 -lemma lmeasure_cube:
1.687 -  "lmeasure (cube n::('a::ordered_euclidean_space) set) = (Real ((2 * real n) ^ (DIM('a))))"
1.688 -  by (intro has_gmeasure_lmeasure) auto
1.689 -
1.690 -lemma lmeasure_UNIV[intro]: "lmeasure UNIV = \<omega>"
1.691 -  unfolding lmeasure_def SUP_\<omega>
1.692 -proof (intro allI impI)
1.693 -  fix x assume "x < \<omega>"
1.694 -  then obtain r where r: "x = Real r" "0 \<le> r" by (cases x) auto
1.695 -  then obtain n where n: "r < of_nat n" using ex_less_of_nat by auto
1.696 -  show "\<exists>i\<in>UNIV. x < Real (gmeasure (UNIV \<inter> cube i))"
1.697 -  proof (intro bexI[of _ n])
1.698 -    have "x < Real (of_nat n)" using n r by auto
1.699 -    also have "Real (of_nat n) \<le> Real (gmeasure (UNIV \<inter> cube n))"
1.700 -      using gmeasure_cube_ge_n[of n] by (auto simp: real_eq_of_nat[symmetric])
1.701 -    finally show "x < Real (gmeasure (UNIV \<inter> cube n))" .
1.702 -  qed auto
1.703 +proof -
1.704 +  have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
1.705 +    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def_raw)
1.706 +  from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
1.707 +    by (simp add: indicator_def_raw)
1.708  qed
1.709
1.710  lemma atLeastAtMost_singleton_euclidean[simp]:
1.711 @@ -421,9 +454,7 @@
1.712
1.713  lemma lmeasure_singleton[simp]:
1.714    fixes a :: "'a::ordered_euclidean_space" shows "lmeasure {a} = 0"
1.715 -  using has_gmeasure_interval[of a a] unfolding zero_pextreal_def
1.716 -  by (intro has_gmeasure_lmeasure)
1.717 -     (simp add: content_closed_interval DIM_positive)
1.718 +  using lmeasure_atLeastAtMost[of a a] by simp
1.719
1.720  declare content_real[simp]
1.721
1.722 @@ -433,21 +464,33 @@
1.723      "lmeasure {a <.. b} = Real (if a \<le> b then b - a else 0)"
1.724  proof cases
1.725    assume "a < b"
1.726 -  then have "lmeasure {a <.. b} = lmeasure {a <..< b} + lmeasure {b}"
1.728 -       (auto intro!: lebesgueI_borel arg_cong[where f=lmeasure])
1.729 +  then have "lmeasure {a <.. b} = lmeasure {a .. b} - lmeasure {a}"
1.730 +    by (subst lebesgue.measure_Diff[symmetric])
1.731 +       (auto intro!: arg_cong[where f=lmeasure])
1.732    then show ?thesis by auto
1.733  qed auto
1.734
1.735  lemma
1.736    fixes a b :: real
1.737    shows lmeasure_real_atLeastLessThan[simp]:
1.738 -    "lmeasure {a ..< b} = Real (if a \<le> b then b - a else 0)" (is ?eqlt)
1.739 +    "lmeasure {a ..< b} = Real (if a \<le> b then b - a else 0)"
1.740  proof cases
1.741    assume "a < b"
1.742 -  then have "lmeasure {a ..< b} = lmeasure {a} + lmeasure {a <..< b}"
1.744 -       (auto intro!: lebesgueI_borel arg_cong[where f=lmeasure])
1.745 +  then have "lmeasure {a ..< b} = lmeasure {a .. b} - lmeasure {b}"
1.746 +    by (subst lebesgue.measure_Diff[symmetric])
1.747 +       (auto intro!: arg_cong[where f=lmeasure])
1.748 +  then show ?thesis by auto
1.749 +qed auto
1.750 +
1.751 +lemma
1.752 +  fixes a b :: real
1.753 +  shows lmeasure_real_greaterThanLessThan[simp]:
1.754 +    "lmeasure {a <..< b} = Real (if a \<le> b then b - a else 0)"
1.755 +proof cases
1.756 +  assume "a < b"
1.757 +  then have "lmeasure {a <..< b} = lmeasure {a <.. b} - lmeasure {b}"
1.758 +    by (subst lebesgue.measure_Diff[symmetric])
1.759 +       (auto intro!: arg_cong[where f=lmeasure])
1.760    then show ?thesis by auto
1.761  qed auto
1.762
1.763 @@ -463,7 +506,7 @@
1.764    show "range cube \<subseteq> sets borel" by (auto intro: borel_closed)
1.765    { fix x have "\<exists>n. x\<in>cube n" using mem_big_cube by auto }
1.766    thus "(\<Union>i. cube i) = space borel" by auto
1.767 -  show "\<forall>i. lmeasure (cube i) \<noteq> \<omega>" unfolding lmeasure_cube by auto
1.768 +  show "\<forall>i. lmeasure (cube i) \<noteq> \<omega>" unfolding cube_def by auto
1.769  qed
1.770
1.771  interpretation lebesgue: sigma_finite_measure lebesgue lmeasure
1.772 @@ -482,7 +525,8 @@
1.773    shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV"
1.774    unfolding lebesgue.simple_integral_def
1.775    apply(subst lebesgue_simple_function_indicator[OF f])
1.776 -proof- case goal1
1.777 +proof -
1.778 +  case goal1
1.779    have *:"\<And>x. \<forall>y\<in>range f. y * indicator (f -` {y}) x \<noteq> \<omega>"
1.780      "\<forall>x\<in>range f. x * lmeasure (f -` {x} \<inter> UNIV) \<noteq> \<omega>"
1.781      using f' om unfolding indicator_def by auto
1.782 @@ -494,16 +538,19 @@
1.783      fix y::'a show "((\<lambda>x. real (f y * indicator (f -` {f y}) x)) has_integral
1.784        real (f y * lmeasure (f -` {f y} \<inter> UNIV))) UNIV"
1.785      proof(cases "f y = 0") case False
1.786 -      have mea:"gmeasurable (f -` {f y})" apply(rule lmeasure_finite_gmeasurable)
1.787 +      have mea:"(indicator (f -` {f y}) ::_\<Rightarrow>real) integrable_on UNIV"
1.788 +        apply(rule lmeasure_finite_integrable)
1.789          using assms unfolding lebesgue.simple_function_def using False by auto
1.790 -      have *:"\<And>x. real (indicator (f -` {f y}) x::pextreal) = (if x \<in> f -` {f y} then 1 else 0)" by auto
1.791 +      have *:"\<And>x. real (indicator (f -` {f y}) x::pextreal) = (indicator (f -` {f y}) x)"
1.792 +        by (auto simp: indicator_def)
1.793        show ?thesis unfolding real_of_pextreal_mult[THEN sym]
1.794          apply(rule has_integral_cmul[where 'b=real, unfolded real_scaleR_def])
1.795 -        unfolding Int_UNIV_right lmeasure_gmeasure[OF mea,THEN sym]
1.796 -        unfolding measure_integral_univ[OF mea] * apply(rule integrable_integral)
1.797 -        unfolding gmeasurable_integrable[THEN sym] using mea .
1.798 +        unfolding Int_UNIV_right lmeasure_eq_integral[OF mea,THEN sym]
1.799 +        unfolding integral_eq_lmeasure[OF mea, symmetric] *
1.800 +        apply(rule integrable_integral) using mea .
1.801      qed auto
1.802 -  qed qed
1.803 +  qed
1.804 +qed
1.805
1.806  lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
1.807    unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
1.808 @@ -826,7 +873,7 @@
1.809    show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
1.810      (is "Int_stable ?E" ) using Int_stable_cuboids' .
1.811    show "borel = sigma ?E" using borel_eq_atLeastAtMost .
1.812 -  show "\<And>i. lmeasure (cube i) \<noteq> \<omega>" unfolding lmeasure_cube by auto
1.813 +  show "\<And>i. lmeasure (cube i) \<noteq> \<omega>" unfolding cube_def by auto
1.814    show "\<And>X. X \<in> sets ?E \<Longrightarrow>
1.815      lmeasure X = borel_product.product_measure {..<DIM('a)} (e2p ` X :: (nat \<Rightarrow> real) set)"
1.816    proof- case goal1 then obtain a b where X:"X = {a..b}" by auto
```