# HG changeset patch
# User hoelzl
# Date 1335359358 -7200
# Node ID 5e6fe71e2390c0fef77be921b566e091da090bb7
# Parent  7b2836a43cc9504e23afc49bf113c4f89c216804
equate positive Lebesgue integral and MV-Analysis' Gauge integral

diff -r 7b2836a43cc9 -r 5e6fe71e2390 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Apr 25 15:06:59 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Apr 25 15:09:18 2012 +0200
@@ -59,7 +59,7 @@
 lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
   unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
 
-subsection {* Lebesgue measure *} 
+subsection {* Lebesgue measure *}
 
 definition lebesgue :: "'a::ordered_euclidean_space measure" where
   "lebesgue = measure_of UNIV {A. \<forall>n. (indicator A :: 'a \<Rightarrow> real) integrable_on cube n}
@@ -129,7 +129,7 @@
 lemma lebesgueD: "A \<in> sets lebesgue \<Longrightarrow> (indicator A :: _ \<Rightarrow> real) integrable_on cube n"
   unfolding sets_lebesgue by simp
 
-lemma emeasure_lebesgue: 
+lemma emeasure_lebesgue:
   assumes "A \<in> sets lebesgue"
   shows "emeasure lebesgue A = (SUP n. ereal (integral (cube n) (indicator A)))"
     (is "_ = ?\<mu> A")
@@ -231,6 +231,10 @@
   finally show ?thesis .
 qed
 
+lemma borel_measurable_lebesgueI:
+  "f \<in> borel_measurable borel \<Longrightarrow> f \<in> borel_measurable lebesgue"
+  unfolding measurable_def by simp
+
 lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set"
   assumes "negligible s" shows "s \<in> sets lebesgue"
   using assms by (force simp: cube_def integrable_on_def negligible_def intro!: lebesgueI)
@@ -735,6 +739,13 @@
              intro!: measurable_If)
 qed
 
+lemma lebesgue_simple_integral_eq_borel:
+  assumes f: "f \<in> borel_measurable borel"
+  shows "integral\<^isup>S lebesgue f = integral\<^isup>S lborel f"
+  using f[THEN measurable_sets]
+  by (auto intro!: setsum_cong arg_cong2[where f="op *"] emeasure_lborel[symmetric]
+           simp: simple_integral_def)
+
 lemma lebesgue_positive_integral_eq_borel:
   assumes f: "f \<in> borel_measurable borel"
   shows "integral\<^isup>P lebesgue f = integral\<^isup>P lborel f"
@@ -839,7 +850,7 @@
   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 }
@@ -940,4 +951,122 @@
   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:
+  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 I: "(f has_integral I) UNIV"
+  shows "(\<integral>\<^isup>+x. f x \<partial>lborel) = I"
+proof -
+  from f_borel have "(\<lambda>x. ereal (f x)) \<in> borel_measurable borel" 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))"
+    using F
+    by (subst positive_integral_monotone_convergence_simple)
+       (simp_all add: positive_integral_max_0 simple_function_def)
+  also have "\<dots> \<le> ereal I"
+  proof (rule SUP_least)
+    fix i :: nat
+
+    { fix z
+      from F(4)[of z] have "F i z \<le> ereal (f z)"
+        by (metis SUP_upper UNIV_I ereal_max_0 min_max.sup_absorb2 nonneg)
+      with F(5)[of i z] have "real (F i z) \<le> f z"
+        by (cases "F i z") simp_all }
+    note F_bound = this
+
+    { fix x :: ereal assume x: "x \<noteq> 0" "x \<in> range (F i)"
+      with F(3,5)[of i] have [simp]: "real x \<noteq> 0"
+        by (metis image_iff order_eq_iff real_of_ereal_le_0)
+      let ?s = "(\<lambda>n z. real x * indicator (F i -` {x} \<inter> cube n) z) :: nat \<Rightarrow> 'a \<Rightarrow> real"
+      have "(\<lambda>z::'a. real x * indicator (F i -` {x}) z) integrable_on UNIV"
+      proof (rule dominated_convergence(1))
+        fix n :: nat
+        have "(\<lambda>z. indicator (F i -` {x} \<inter> cube n) z :: real) integrable_on cube n"
+          using x F(1)[of i]
+          by (intro lebesgueD) (auto simp: simple_function_def)
+        then have cube: "?s n integrable_on cube n"
+          by (simp add: integrable_on_cmult_iff)
+        show "?s n integrable_on UNIV"
+          by (rule integrable_on_superset[OF _ _ cube]) auto
+      next
+        show "f integrable_on UNIV"
+          unfolding integrable_on_def using I by auto
+      next
+        fix n from F_bound show "\<forall>x\<in>UNIV. norm (?s n x) \<le> f x"
+          using nonneg F(5) by (auto split: split_indicator)
+      next
+        show "\<forall>z\<in>UNIV. (\<lambda>n. ?s n z) ----> real x * indicator (F i -` {x}) z"
+        proof
+          fix z :: 'a
+          from mem_big_cube[of z] guess j .
+          then have x: "eventually (\<lambda>n. ?s n z = real x * indicator (F i -` {x}) z) sequentially"
+            by (auto intro!: eventually_sequentiallyI[where c=j] dest!: cube_subset split: split_indicator)
+          then show "(\<lambda>n. ?s n z) ----> real x * indicator (F i -` {x}) z"
+            by (rule Lim_eventually)
+        qed
+      qed
+      then have "(indicator (F i -` {x}) :: 'a \<Rightarrow> real) integrable_on UNIV"
+        by (simp add: integrable_on_cmult_iff) }
+    note F_finite = lmeasure_finite[OF this]
+
+    have "((\<lambda>x. real (F i x)) has_integral real (integral\<^isup>S lebesgue (F i))) UNIV"
+    proof (rule simple_function_has_integral[of "F i"])
+      show "simple_function lebesgue (F i)"
+        using F(1) by (simp add: simple_function_def)
+      show "range (F i) \<subseteq> {0..<\<infinity>}"
+        using F(3,5)[of i] by (auto simp: image_iff) metis
+    next
+      fix x assume "x \<in> range (F i)" "emeasure lebesgue (F i -` {x} \<inter> UNIV) = \<infinity>"
+      with F_finite[of x] show "x = 0" by auto
+    qed
+    from this I have "real (integral\<^isup>S lebesgue (F i)) \<le> I"
+      by (rule has_integral_le) (intro ballI F_bound)
+    moreover
+    { fix x assume x: "x \<in> range (F i)"
+      with F(3,5)[of i] have "x = 0 \<or> (0 < x \<and> x \<noteq> \<infinity>)"
+        by (auto  simp: image_iff le_less) metis
+      with F_finite[OF _ x] x have "x * emeasure lebesgue (F i -` {x} \<inter> UNIV) \<noteq> \<infinity>"
+        by auto }
+    then have "integral\<^isup>S lebesgue (F i) \<noteq> \<infinity>"
+      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
+  qed
+  also have "\<dots> < \<infinity>" by simp
+  finally have finite: "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue) \<noteq> \<infinity>" by simp
+  have borel: "(\<lambda>x. ereal (f x)) \<in> borel_measurable lebesgue"
+    using f_borel by (auto intro: borel_measurable_lebesgueI)
+  from positive_integral_has_integral[OF borel _ finite]
+  have "(f has_integral real (\<integral>\<^isup>+ x. ereal (f x) \<partial>lebesgue)) UNIV"
+    using nonneg by (simp add: subset_eq)
+  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)
+qed
+
+lemma has_integral_iff_positive_integral:
+  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)
+
 end