# HG changeset patch
# User hoelzl
# Date 1349863938 -7200
# Node ID 6ac97ab9b295da4099f6ce164fe676f781ae3708
# Parent  199d1d5bb17e65344fde047d1fd136ad8d7dc560
tuned Lebesgue measure proofs

diff -r 199d1d5bb17e -r 6ac97ab9b295 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Oct 10 12:12:18 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Oct 10 12:12:18 2012 +0200
@@ -9,20 +9,23 @@
   imports Finite_Product_Measure
 begin
 
+lemma borel_measurable_indicator':
+  "A \<in> sets borel \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
+  using measurable_comp[OF _ borel_measurable_indicator, of f M borel A] by (auto simp add: comp_def)
+
 lemma borel_measurable_sets:
   assumes "f \<in> measurable borel M" "A \<in> sets M"
   shows "f -` A \<in> sets borel"
   using measurable_sets[OF assms] by simp
 
-lemma measurable_identity[intro,simp]:
-  "(\<lambda>x. x) \<in> measurable M M"
-  unfolding measurable_def by auto
-
 subsection {* Standard Cubes *}
 
 definition cube :: "nat \<Rightarrow> 'a::ordered_euclidean_space set" where
   "cube n \<equiv> {\<chi>\<chi> i. - real n .. \<chi>\<chi> i. real n}"
 
+lemma borel_cube[intro]: "cube n \<in> sets borel"
+  unfolding cube_def by auto
+
 lemma cube_closed[intro]: "closed (cube n)"
   unfolding cube_def by auto
 
@@ -154,7 +157,7 @@
     then have UN_A[simp, intro]: "\<And>i n. (indicator (\<Union>i. A i) :: _ \<Rightarrow> real) integrable_on cube n"
       by (auto simp: sets_lebesgue)
     show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (\<Union>i. A i)"
-    proof (subst suminf_SUP_eq, safe intro!: incseq_SucI)
+    proof (subst suminf_SUP_eq, safe intro!: incseq_SucI) 
       fix i n show "ereal (?m n i) \<le> ereal (?m (Suc n) i)"
         using cube_subset[of n "Suc n"] by (auto intro!: integral_subset_le incseq_SucI)
     next
@@ -193,7 +196,6 @@
       qed
     qed
   qed
-next
 qed (auto, fact)
 
 lemma has_integral_interval_cube:
@@ -279,14 +281,16 @@
 
 lemma lmeasure_finite_has_integral:
   fixes s :: "'a::ordered_euclidean_space set"
-  assumes "s \<in> sets lebesgue" "emeasure lebesgue s = ereal m" "0 \<le> m"
+  assumes "s \<in> sets lebesgue" "emeasure lebesgue s = ereal m"
   shows "(indicator s has_integral m) UNIV"
 proof -
   let ?I = "indicator :: 'a set \<Rightarrow> 'a \<Rightarrow> real"
+  have "0 \<le> m"
+    using emeasure_nonneg[of lebesgue s] `emeasure lebesgue s = ereal m` by simp
   have **: "(?I s) integrable_on UNIV \<and> (\<lambda>k. integral UNIV (?I (s \<inter> cube k))) ----> integral UNIV (?I s)"
   proof (intro monotone_convergence_increasing allI ballI)
     have LIMSEQ: "(\<lambda>n. integral (cube n) (?I s)) ----> m"
-      using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1, 3)] .
+      using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1) `0 \<le> m`] .
     { fix n have "integral (cube n) (?I s) \<le> m"
         using cube_subset assms
         by (intro incseq_le[where L=m] LIMSEQ incseq_def[THEN iffD2] integral_subset_le allI impI)
@@ -316,7 +320,7 @@
   note ** = conjunctD2[OF this]
   have m: "m = integral UNIV (?I s)"
     apply (intro LIMSEQ_unique[OF _ **(2)])
-    using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1,3)] integral_indicator_UNIV .
+    using assms(2) unfolding lmeasure_iff_LIMSEQ[OF assms(1) `0 \<le> m`] integral_indicator_UNIV .
   show ?thesis
     unfolding m by (intro integrable_integral **)
 qed
@@ -366,14 +370,14 @@
 qed
 
 lemma has_integral_iff_lmeasure:
-  "(indicator A has_integral m) UNIV \<longleftrightarrow> (A \<in> sets lebesgue \<and> 0 \<le> m \<and> emeasure lebesgue A = ereal m)"
+  "(indicator A has_integral m) UNIV \<longleftrightarrow> (A \<in> sets lebesgue \<and> emeasure lebesgue A = ereal m)"
 proof
   assume "(indicator A has_integral m) UNIV"
   with has_integral_lmeasure[OF this] has_integral_lebesgue[OF this]
-  show "A \<in> sets lebesgue \<and> 0 \<le> m \<and> emeasure lebesgue A = ereal m"
+  show "A \<in> sets lebesgue \<and> emeasure lebesgue A = ereal m"
     by (auto intro: has_integral_nonneg)
 next
-  assume "A \<in> sets lebesgue \<and> 0 \<le> m \<and> emeasure lebesgue A = ereal m"
+  assume "A \<in> sets lebesgue \<and> emeasure lebesgue A = ereal m"
   then show "(indicator A has_integral m) UNIV" by (intro lmeasure_finite_has_integral) auto
 qed
 
@@ -450,6 +454,9 @@
     by (auto simp: cube_def content_closed_interval_cases setprod_constant)
 qed simp
 
+lemma lmeasure_complete: "A \<subseteq> B \<Longrightarrow> B \<in> null_sets lebesgue \<Longrightarrow> A \<in> null_sets lebesgue"
+  unfolding negligible_iff_lebesgue_null_sets[symmetric] by (auto simp: negligible_subset)
+
 lemma
   fixes a b ::"'a::ordered_euclidean_space"
   shows lmeasure_atLeastAtMost[simp]: "emeasure lebesgue {a..b} = ereal (content {a..b})"
@@ -475,43 +482,44 @@
   fixes a :: "'a::ordered_euclidean_space" shows "emeasure lebesgue {a} = 0"
   using lmeasure_atLeastAtMost[of a a] by simp
 
+lemma AE_lebesgue_singleton:
+  fixes a :: "'a::ordered_euclidean_space" shows "AE x in lebesgue. x \<noteq> a"
+  by (rule AE_I[where N="{a}"]) auto
+
 declare content_real[simp]
 
 lemma
   fixes a b :: real
   shows lmeasure_real_greaterThanAtMost[simp]:
     "emeasure lebesgue {a <.. b} = ereal (if a \<le> b then b - a else 0)"
-proof cases
-  assume "a < b"
-  then have "emeasure lebesgue {a <.. b} = emeasure lebesgue {a .. b} - emeasure lebesgue {a}"
-    by (subst emeasure_Diff[symmetric])
-       (auto intro!: arg_cong[where f="emeasure lebesgue"])
+proof -
+  have "emeasure lebesgue {a <.. b} = emeasure lebesgue {a .. b}"
+    using AE_lebesgue_singleton[of a]
+    by (intro emeasure_eq_AE) auto
   then show ?thesis by auto
-qed auto
+qed
 
 lemma
   fixes a b :: real
   shows lmeasure_real_atLeastLessThan[simp]:
     "emeasure lebesgue {a ..< b} = ereal (if a \<le> b then b - a else 0)"
-proof cases
-  assume "a < b"
-  then have "emeasure lebesgue {a ..< b} = emeasure lebesgue {a .. b} - emeasure lebesgue {b}"
-    by (subst emeasure_Diff[symmetric])
-       (auto intro!: arg_cong[where f="emeasure lebesgue"])
+proof -
+  have "emeasure lebesgue {a ..< b} = emeasure lebesgue {a .. b}"
+    using AE_lebesgue_singleton[of b]
+    by (intro emeasure_eq_AE) auto
   then show ?thesis by auto
-qed auto
+qed
 
 lemma
   fixes a b :: real
   shows lmeasure_real_greaterThanLessThan[simp]:
     "emeasure lebesgue {a <..< b} = ereal (if a \<le> b then b - a else 0)"
-proof cases
-  assume "a < b"
-  then have "emeasure lebesgue {a <..< b} = emeasure lebesgue {a <.. b} - emeasure lebesgue {b}"
-    by (subst emeasure_Diff[symmetric])
-       (auto intro!: arg_cong[where f="emeasure lebesgue"])
+proof -
+  have "emeasure lebesgue {a <..< b} = emeasure lebesgue {a .. b}"
+    using AE_lebesgue_singleton[of a] AE_lebesgue_singleton[of b]
+    by (intro emeasure_eq_AE) auto
   then show ?thesis by auto
-qed auto
+qed
 
 subsection {* Lebesgue-Borel measure *}
 
@@ -544,6 +552,62 @@
     by (intro exI[of _ A]) (auto simp: subset_eq)
 qed
 
+lemma Int_stable_atLeastAtMost:
+  fixes x::"'a::ordered_euclidean_space"
+  shows "Int_stable (range (\<lambda>(a, b::'a). {a..b}))"
+  by (auto simp: inter_interval Int_stable_def)
+
+lemma lborel_eqI:
+  fixes M :: "'a::ordered_euclidean_space measure"
+  assumes emeasure_eq: "\<And>a b. emeasure M {a .. b} = content {a .. b}"
+  assumes sets_eq: "sets M = sets borel"
+  shows "lborel = M"
+proof (rule measure_eqI_generator_eq[OF Int_stable_atLeastAtMost])
+  let ?P = "\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel"
+  let ?E = "range (\<lambda>(a, b). {a..b} :: 'a set)"
+  show "?E \<subseteq> Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E"
+    by (simp_all add: borel_eq_atLeastAtMost sets_eq)
+
+  show "range cube \<subseteq> ?E" unfolding cube_def [abs_def] by auto
+  show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
+  { fix x :: 'a have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
+  then show "(\<Union>i. cube i :: 'a set) = UNIV" by auto
+
+  { fix i show "emeasure lborel (cube i) \<noteq> \<infinity>" unfolding cube_def by auto }
+  { fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X"
+      by (auto simp: emeasure_eq) }
+qed
+
+lemma lebesgue_real_affine:
+  fixes c :: real assumes "c \<noteq> 0"
+  shows "lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. \<bar>c\<bar>)" (is "_ = ?D")
+proof (rule lborel_eqI)
+  fix a b show "emeasure ?D {a..b} = content {a .. b}"
+  proof cases
+    assume "0 < c"
+    then have "(\<lambda>x. t + c * x) -` {a..b} = {(a - t) / c .. (b - t) / c}"
+      by (auto simp: field_simps)
+    with `0 < c` show ?thesis
+      by (cases "a \<le> b")
+         (auto simp: field_simps emeasure_density positive_integral_distr positive_integral_cmult
+                     borel_measurable_indicator' emeasure_distr)
+  next
+    assume "\<not> 0 < c" with `c \<noteq> 0` have "c < 0" by auto
+    then have *: "(\<lambda>x. t + c * x) -` {a..b} = {(b - t) / c .. (a - t) / c}"
+      by (auto simp: field_simps)
+    with `c < 0` show ?thesis
+      by (cases "a \<le> b")
+         (auto simp: field_simps emeasure_density positive_integral_distr
+                     positive_integral_cmult borel_measurable_indicator' emeasure_distr)
+  qed
+qed simp
+
+lemma lebesgue_integral_real_affine:
+  fixes c :: real assumes c: "c \<noteq> 0" and f: "f \<in> borel_measurable borel"
+  shows "(\<integral> x. f x \<partial> lborel) = \<bar>c\<bar> * (\<integral> x. f (t + c * x) \<partial>lborel)"
+  by (subst lebesgue_real_affine[OF c, of t])
+     (simp add: f integral_density integral_distr lebesgue_integral_cmult)
+
 subsection {* Lebesgue integrable implies Gauge integrable *}
 
 lemma has_integral_cmult_real:
@@ -777,201 +841,22 @@
     unfolding lebesgue_integral_eq_borel[OF borel] by simp
 qed
 
-subsection {* Equivalence between product spaces and euclidean spaces *}
-
-definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> (nat \<Rightarrow> real)" where
-  "e2p x = (\<lambda>i\<in>{..<DIM('a)}. x$$i)"
-
-definition p2e :: "(nat \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where
-  "p2e x = (\<chi>\<chi> i. x i)"
-
-lemma e2p_p2e[simp]:
-  "x \<in> extensional {..<DIM('a)} \<Longrightarrow> e2p (p2e x::'a::ordered_euclidean_space) = x"
-  by (auto simp: fun_eq_iff extensional_def p2e_def e2p_def)
-
-lemma p2e_e2p[simp]:
-  "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
-  by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
-
-interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure"
-  by default
-
-interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure" "{..<n}" for n :: nat
-  by default auto
-
-lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
-  by metis
-
-lemma sets_product_borel:
-  assumes I: "finite I"
-  shows "sets (\<Pi>\<^isub>M i\<in>I. lborel) = sigma_sets (\<Pi>\<^isub>E i\<in>I. UNIV) { \<Pi>\<^isub>E i\<in>I. {..< x i :: real} | x. True}" (is "_ = ?G")
-proof (subst sigma_prod_algebra_sigma_eq[where S="\<lambda>_ i::nat. {..<real i}" and E="\<lambda>_. range lessThan", OF I])
-  show "sigma_sets (space (Pi\<^isub>M I (\<lambda>i. lborel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> range lessThan} = ?G"
-    by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
-qed (auto simp: borel_eq_lessThan incseq_def reals_Archimedean2 image_iff intro: real_natceiling_ge)
-
-lemma measurable_e2p:
-  "e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))"
-proof (rule measurable_sigma_sets[OF sets_product_borel])
-  fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
-  then obtain x where  "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i})" by auto
-  then have "e2p -` A = {..< (\<chi>\<chi> i. x i) :: 'a}"
-    using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def
-      euclidean_eq[where 'a='a] eucl_less[where 'a='a])
-  then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
-qed (auto simp: e2p_def)
-
-lemma measurable_p2e:
-  "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))
-    (borel :: 'a::ordered_euclidean_space measure)"
-  (is "p2e \<in> measurable ?P _")
-proof (safe intro!: borel_measurable_iff_halfspace_le[THEN iffD2])
-  fix x i
-  let ?A = "{w \<in> space ?P. (p2e w :: 'a) $$ i \<le> x}"
-  assume "i < DIM('a)"
-  then have "?A = (\<Pi>\<^isub>E j\<in>{..<DIM('a)}. if i = j then {.. x} else UNIV)"
-    using DIM_positive by (auto simp: space_PiM p2e_def split: split_if_asm)
-  then show "?A \<in> sets ?P"
-    by auto
-qed
-
-lemma Int_stable_atLeastAtMost:
-  fixes x::"'a::ordered_euclidean_space"
-  shows "Int_stable (range (\<lambda>(a, b::'a). {a..b}))"
-  by (auto simp: inter_interval Int_stable_def)
-
-lemma lborel_eqI:
-  fixes M :: "'a::ordered_euclidean_space measure"
-  assumes emeasure_eq: "\<And>a b. emeasure M {a .. b} = content {a .. b}"
-  assumes sets_eq: "sets M = sets borel"
-  shows "lborel = M"
-proof (rule measure_eqI_generator_eq[OF Int_stable_atLeastAtMost])
-  let ?P = "\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel"
-  let ?E = "range (\<lambda>(a, b). {a..b} :: 'a set)"
-  show "?E \<subseteq> Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E"
-    by (simp_all add: borel_eq_atLeastAtMost sets_eq)
-
-  show "range cube \<subseteq> ?E" unfolding cube_def [abs_def] by auto
-  show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
-  { fix x :: 'a have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
-  then show "(\<Union>i. cube i :: 'a set) = UNIV" by auto
-
-  { fix i show "emeasure lborel (cube i) \<noteq> \<infinity>" unfolding cube_def by auto }
-  { fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X"
-      by (auto simp: emeasure_eq) }
-qed
-
-lemma lborel_eq_lborel_space:
-  "(lborel :: 'a measure) = distr (\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel) lborel p2e"
-  (is "?B = ?D")
-proof (rule lborel_eqI)
-  show "sets ?D = sets borel" by simp
-  let ?P = "(\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel)"
-  fix a b :: 'a
-  have *: "p2e -` {a .. b} \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a $$ i .. b $$ i})"
-    by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def space_PiM)
-  have "emeasure ?P (p2e -` {a..b} \<inter> space ?P) = content {a..b}"
-  proof cases
-    assume "{a..b} \<noteq> {}"
-    then have "a \<le> b"
-      by (simp add: interval_ne_empty eucl_le[where 'a='a])
-    then have "emeasure lborel {a..b} = (\<Prod>x<DIM('a). emeasure lborel {a $$ x .. b $$ x})"
-      by (auto simp: content_closed_interval eucl_le[where 'a='a]
-               intro!: setprod_ereal[symmetric])
-    also have "\<dots> = emeasure ?P (p2e -` {a..b} \<inter> space ?P)"
-      unfolding * by (subst lborel_space.measure_times) auto
-    finally show ?thesis by simp
-  qed simp
-  then show "emeasure ?D {a .. b} = content {a .. b}"
-    by (simp add: emeasure_distr measurable_p2e)
-qed
-
-lemma borel_fubini_positiv_integral:
-  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
-  assumes f: "f \<in> borel_measurable borel"
-  shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel)"
-  by (subst lborel_eq_lborel_space) (simp add: positive_integral_distr measurable_p2e f)
-
-lemma borel_fubini_integrable:
-  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
-  shows "integrable lborel f \<longleftrightarrow>
-    integrable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel) (\<lambda>x. f (p2e x))"
-    (is "_ \<longleftrightarrow> integrable ?B ?f")
-proof
-  assume "integrable lborel f"
-  moreover then have f: "f \<in> borel_measurable borel"
-    by auto
-  moreover with measurable_p2e
-  have "f \<circ> p2e \<in> borel_measurable ?B"
-    by (rule measurable_comp)
-  ultimately show "integrable ?B ?f"
-    by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
-next
-  assume "integrable ?B ?f"
-  moreover
-  then have "?f \<circ> e2p \<in> borel_measurable (borel::'a measure)"
-    by (auto intro!: measurable_e2p)
-  then have "f \<in> borel_measurable borel"
-    by (simp cong: measurable_cong)
-  ultimately show "integrable lborel f"
-    by (simp add: borel_fubini_positiv_integral integrable_def)
-qed
-
-lemma borel_fubini:
-  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable borel"
-  shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>((\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel))"
-  using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def)
-
-lemma borel_measurable_indicator':
-  "A \<in> sets borel \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
-  using measurable_comp[OF _ borel_measurable_indicator, of f M borel A] by (auto simp add: comp_def)
-
-lemma lebesgue_real_affine:
-  fixes c :: real assumes "c \<noteq> 0"
-  shows "lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. \<bar>c\<bar>)" (is "_ = ?D")
-proof (rule lborel_eqI)
-  fix a b show "emeasure ?D {a..b} = content {a .. b}"
-  proof cases
-    assume "0 < c"
-    then have "(\<lambda>x. t + c * x) -` {a..b} = {(a - t) / c .. (b - t) / c}"
-      by (auto simp: field_simps)
-    with `0 < c` show ?thesis
-      by (cases "a \<le> b")
-         (auto simp: field_simps emeasure_density positive_integral_distr positive_integral_cmult
-                     borel_measurable_indicator' emeasure_distr)
-  next
-    assume "\<not> 0 < c" with `c \<noteq> 0` have "c < 0" by auto
-    then have *: "(\<lambda>x. t + c * x) -` {a..b} = {(b - t) / c .. (a - t) / c}"
-      by (auto simp: field_simps)
-    with `c < 0` show ?thesis
-      by (cases "a \<le> b")
-         (auto simp: field_simps emeasure_density positive_integral_distr
-                     positive_integral_cmult borel_measurable_indicator' emeasure_distr)
-  qed
-qed simp
-
-lemma borel_cube[intro]: "cube n \<in> sets borel"
-  unfolding cube_def by auto
-
 lemma integrable_on_cmult_iff:
   fixes c :: real assumes "c \<noteq> 0"
   shows "(\<lambda>x. c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
   using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] `c \<noteq> 0`
   by auto
 
-lemma positive_integral_borel_has_integral:
+lemma positive_integral_lebesgue_has_integral:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
-  assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
+  assumes f_borel: "f \<in> borel_measurable lebesgue" and nonneg: "\<And>x. 0 \<le> f x"
   assumes I: "(f has_integral I) UNIV"
-  shows "(\<integral>\<^isup>+x. f x \<partial>lborel) = I"
+  shows "(\<integral>\<^isup>+x. f x \<partial>lebesgue) = I"
 proof -
-  from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable borel" by auto
+  from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable lebesgue" by auto
   from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
 
-  have lebesgue_eq: "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) = (\<integral>\<^isup>+ x. ereal (f x) \<partial>lborel)"
-    using f_borel by (intro lebesgue_positive_integral_eq_borel) auto
-  also have "\<dots> = (SUP i. integral\<^isup>S lborel (F i))"
+  have "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) = (SUP i. integral\<^isup>S lebesgue (F i))"
     using F
     by (subst positive_integral_monotone_convergence_simple)
        (simp_all add: positive_integral_max_0 simple_function_def)
@@ -1043,11 +928,8 @@
       unfolding simple_integral_def setsum_Pinfty space_lebesgue by blast
     moreover have "0 \<le> integral\<^isup>S lebesgue (F i)"
       using F(1,5) by (intro simple_integral_positive) (auto simp: simple_function_def)
-    moreover have "integral\<^isup>S lebesgue (F i) = integral\<^isup>S lborel (F i)"
-      using F(1)[of i, THEN borel_measurable_simple_function]
-      by (rule lebesgue_simple_integral_eq_borel)
-    ultimately show "integral\<^isup>S lborel (F i) \<le> ereal I"
-      by (cases "integral\<^isup>S lborel (F i)") auto
+    ultimately show "integral\<^isup>S lebesgue (F i) \<le> ereal I"
+      by (cases "integral\<^isup>S lebesgue (F i)") auto
   qed
   also have "\<dots> < \<infinity>" by simp
   finally have finite: "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) \<noteq> \<infinity>" by simp
@@ -1059,14 +941,142 @@
   with I have "I = real (\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue)"
     by (rule has_integral_unique)
   with finite positive_integral_positive[of _ "\<lambda>x. ereal (f x)"] show ?thesis
-    by (cases "\<integral>\<^isup>+ x. ereal (f x) \<partial>lborel") (auto simp: lebesgue_eq)
+    by (cases "\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue") auto
 qed
 
-lemma has_integral_iff_positive_integral:
+lemma has_integral_iff_positive_integral_lebesgue:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
+  assumes f: "f \<in> borel_measurable lebesgue" "\<And>x. 0 \<le> f x"
+  shows "(f has_integral I) UNIV \<longleftrightarrow> integral\<^isup>P lebesgue f = I"
+  using f positive_integral_lebesgue_has_integral[of f I] positive_integral_has_integral[of f]
+  by (auto simp: subset_eq)
+
+lemma has_integral_iff_positive_integral_lborel:
   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x"
   shows "(f has_integral I) UNIV \<longleftrightarrow> integral\<^isup>P lborel f = I"
-  using f positive_integral_borel_has_integral[of f I] positive_integral_has_integral[of f]
-  by (auto simp: subset_eq borel_measurable_lebesgueI lebesgue_positive_integral_eq_borel)
+  using assms
+  by (subst has_integral_iff_positive_integral_lebesgue)
+     (auto simp: borel_measurable_lebesgueI lebesgue_positive_integral_eq_borel)
+
+subsection {* Equivalence between product spaces and euclidean spaces *}
+
+definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> (nat \<Rightarrow> real)" where
+  "e2p x = (\<lambda>i\<in>{..<DIM('a)}. x$$i)"
+
+definition p2e :: "(nat \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where
+  "p2e x = (\<chi>\<chi> i. x i)"
+
+lemma e2p_p2e[simp]:
+  "x \<in> extensional {..<DIM('a)} \<Longrightarrow> e2p (p2e x::'a::ordered_euclidean_space) = x"
+  by (auto simp: fun_eq_iff extensional_def p2e_def e2p_def)
+
+lemma p2e_e2p[simp]:
+  "p2e (e2p x) = (x::'a::ordered_euclidean_space)"
+  by (auto simp: euclidean_eq[where 'a='a] p2e_def e2p_def)
+
+interpretation lborel_product: product_sigma_finite "\<lambda>x. lborel::real measure"
+  by default
+
+interpretation lborel_space: finite_product_sigma_finite "\<lambda>x. lborel::real measure" "{..<n}" for n :: nat
+  by default auto
+
+lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
+  by metis
+
+lemma sets_product_borel:
+  assumes I: "finite I"
+  shows "sets (\<Pi>\<^isub>M i\<in>I. lborel) = sigma_sets (\<Pi>\<^isub>E i\<in>I. UNIV) { \<Pi>\<^isub>E i\<in>I. {..< x i :: real} | x. True}" (is "_ = ?G")
+proof (subst sigma_prod_algebra_sigma_eq[where S="\<lambda>_ i::nat. {..<real i}" and E="\<lambda>_. range lessThan", OF I])
+  show "sigma_sets (space (Pi\<^isub>M I (\<lambda>i. lborel))) {Pi\<^isub>E I F |F. \<forall>i\<in>I. F i \<in> range lessThan} = ?G"
+    by (intro arg_cong2[where f=sigma_sets]) (auto simp: space_PiM image_iff bchoice_iff)
+qed (auto simp: borel_eq_lessThan incseq_def reals_Archimedean2 image_iff intro: real_natceiling_ge)
+
+lemma measurable_e2p:
+  "e2p \<in> measurable (borel::'a::ordered_euclidean_space measure) (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))"
+proof (rule measurable_sigma_sets[OF sets_product_borel])
+  fix A :: "(nat \<Rightarrow> real) set" assume "A \<in> {\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i} |x. True} "
+  then obtain x where  "A = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {..<x i})" by auto
+  then have "e2p -` A = {..< (\<chi>\<chi> i. x i) :: 'a}"
+    using DIM_positive by (auto simp add: Pi_iff set_eq_iff e2p_def
+      euclidean_eq[where 'a='a] eucl_less[where 'a='a])
+  then show "e2p -` A \<inter> space (borel::'a measure) \<in> sets borel" by simp
+qed (auto simp: e2p_def)
+
+lemma measurable_p2e:
+  "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))
+    (borel :: 'a::ordered_euclidean_space measure)"
+  (is "p2e \<in> measurable ?P _")
+proof (safe intro!: borel_measurable_iff_halfspace_le[THEN iffD2])
+  fix x i
+  let ?A = "{w \<in> space ?P. (p2e w :: 'a) $$ i \<le> x}"
+  assume "i < DIM('a)"
+  then have "?A = (\<Pi>\<^isub>E j\<in>{..<DIM('a)}. if i = j then {.. x} else UNIV)"
+    using DIM_positive by (auto simp: space_PiM p2e_def split: split_if_asm)
+  then show "?A \<in> sets ?P"
+    by auto
+qed
+
+lemma lborel_eq_lborel_space:
+  "(lborel :: 'a measure) = distr (\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel) borel p2e"
+  (is "?B = ?D")
+proof (rule lborel_eqI)
+  show "sets ?D = sets borel" by simp
+  let ?P = "(\<Pi>\<^isub>M i\<in>{..<DIM('a::ordered_euclidean_space)}. lborel)"
+  fix a b :: 'a
+  have *: "p2e -` {a .. b} \<inter> space ?P = (\<Pi>\<^isub>E i\<in>{..<DIM('a)}. {a $$ i .. b $$ i})"
+    by (auto simp: Pi_iff eucl_le[where 'a='a] p2e_def space_PiM)
+  have "emeasure ?P (p2e -` {a..b} \<inter> space ?P) = content {a..b}"
+  proof cases
+    assume "{a..b} \<noteq> {}"
+    then have "a \<le> b"
+      by (simp add: interval_ne_empty eucl_le[where 'a='a])
+    then have "emeasure lborel {a..b} = (\<Prod>x<DIM('a). emeasure lborel {a $$ x .. b $$ x})"
+      by (auto simp: content_closed_interval eucl_le[where 'a='a]
+               intro!: setprod_ereal[symmetric])
+    also have "\<dots> = emeasure ?P (p2e -` {a..b} \<inter> space ?P)"
+      unfolding * by (subst lborel_space.measure_times) auto
+    finally show ?thesis by simp
+  qed simp
+  then show "emeasure ?D {a .. b} = content {a .. b}"
+    by (simp add: emeasure_distr measurable_p2e)
+qed
+
+lemma borel_fubini_positiv_integral:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> ereal"
+  assumes f: "f \<in> borel_measurable borel"
+  shows "integral\<^isup>P lborel f = \<integral>\<^isup>+x. f (p2e x) \<partial>(\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel)"
+  by (subst lborel_eq_lborel_space) (simp add: positive_integral_distr measurable_p2e f)
+
+lemma borel_fubini_integrable:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
+  shows "integrable lborel f \<longleftrightarrow>
+    integrable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel) (\<lambda>x. f (p2e x))"
+    (is "_ \<longleftrightarrow> integrable ?B ?f")
+proof
+  assume "integrable lborel f"
+  moreover then have f: "f \<in> borel_measurable borel"
+    by auto
+  moreover with measurable_p2e
+  have "f \<circ> p2e \<in> borel_measurable ?B"
+    by (rule measurable_comp)
+  ultimately show "integrable ?B ?f"
+    by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
+next
+  assume "integrable ?B ?f"
+  moreover
+  then have "?f \<circ> e2p \<in> borel_measurable (borel::'a measure)"
+    by (auto intro!: measurable_e2p)
+  then have "f \<in> borel_measurable borel"
+    by (simp cong: measurable_cong)
+  ultimately show "integrable lborel f"
+    by (simp add: borel_fubini_positiv_integral integrable_def)
+qed
+
+lemma borel_fubini:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
+  assumes f: "f \<in> borel_measurable borel"
+  shows "integral\<^isup>L lborel f = \<integral>x. f (p2e x) \<partial>((\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel))"
+  using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def)
 
 end