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.13      by (auto simp add:dist_norm)
    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.52 +lemma indicator_add:
    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.171 +              using Suc A by (simp add: integral_add[symmetric])
   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.727 -    by (subst lebesgue.measure_additive)
   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.743 -    by (subst lebesgue.measure_additive)
   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