src/HOL/Probability/Lebesgue_Measure.thy
author hoelzl
Wed Dec 01 19:20:30 2010 +0100 (2010-12-01)
changeset 40859 de0b30e6c2d2
parent 38656 d5d342611edb
child 40871 688f6ff859e1
permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
     1 (*  Author: Robert Himmelmann, TU Muenchen *)
     2 header {* Lebsegue measure *}
     3 theory Lebesgue_Measure
     4   imports Product_Measure Gauge_Measure Complete_Measure
     5 begin
     6 
     7 lemma (in complete_lattice) SUP_pair:
     8   "(SUP i:A. SUP j:B. f i j) = (SUP p:A\<times>B. (\<lambda> (i, j). f i j) p)" (is "?l = ?r")
     9 proof (intro antisym SUP_leI)
    10   fix i j assume "i \<in> A" "j \<in> B"
    11   then have "(case (i,j) of (i,j) \<Rightarrow> f i j) \<le> ?r"
    12     by (intro SUPR_upper) auto
    13   then show "f i j \<le> ?r" by auto
    14 next
    15   fix p assume "p \<in> A \<times> B"
    16   then obtain i j where "p = (i,j)" "i \<in> A" "j \<in> B" by auto
    17   have "f i j \<le> (SUP j:B. f i j)" using `j \<in> B` by (intro SUPR_upper)
    18   also have "(SUP j:B. f i j) \<le> ?l" using `i \<in> A` by (intro SUPR_upper)
    19   finally show "(case p of (i, j) \<Rightarrow> f i j) \<le> ?l" using `p = (i,j)` by simp
    20 qed
    21 
    22 lemma (in complete_lattice) SUP_surj_compose:
    23   assumes *: "f`A = B" shows "SUPR A (g \<circ> f) = SUPR B g"
    24   unfolding SUPR_def unfolding *[symmetric]
    25   by (simp add: image_compose)
    26 
    27 lemma (in complete_lattice) SUP_swap:
    28   "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
    29 proof -
    30   have *: "(\<lambda>(i,j). (j,i)) ` (B \<times> A) = A \<times> B" by auto
    31   show ?thesis
    32     unfolding SUP_pair SUP_surj_compose[symmetric, OF *]
    33     by (auto intro!: arg_cong[where f=Sup] image_eqI simp: comp_def SUPR_def)
    34 qed
    35 
    36 lemma SUP_\<omega>: "(SUP i:A. f i) = \<omega> \<longleftrightarrow> (\<forall>x<\<omega>. \<exists>i\<in>A. x < f i)"
    37 proof
    38   assume *: "(SUP i:A. f i) = \<omega>"
    39   show "(\<forall>x<\<omega>. \<exists>i\<in>A. x < f i)" unfolding *[symmetric]
    40   proof (intro allI impI)
    41     fix x assume "x < SUPR A f" then show "\<exists>i\<in>A. x < f i"
    42       unfolding less_SUP_iff by auto
    43   qed
    44 next
    45   assume *: "\<forall>x<\<omega>. \<exists>i\<in>A. x < f i"
    46   show "(SUP i:A. f i) = \<omega>"
    47   proof (rule pinfreal_SUPI)
    48     fix y assume **: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> y"
    49     show "\<omega> \<le> y"
    50     proof cases
    51       assume "y < \<omega>"
    52       from *[THEN spec, THEN mp, OF this]
    53       obtain i where "i \<in> A" "\<not> (f i \<le> y)" by auto
    54       with ** show ?thesis by auto
    55     qed auto
    56   qed auto
    57 qed
    58 
    59 lemma psuminf_commute:
    60   shows "(\<Sum>\<^isub>\<infinity> i j. f i j) = (\<Sum>\<^isub>\<infinity> j i. f i j)"
    61 proof -
    62   have "(SUP n. \<Sum> i < n. SUP m. \<Sum> j < m. f i j) = (SUP n. SUP m. \<Sum> i < n. \<Sum> j < m. f i j)"
    63     apply (subst SUPR_pinfreal_setsum)
    64     by auto
    65   also have "\<dots> = (SUP m n. \<Sum> j < m. \<Sum> i < n. f i j)"
    66     apply (subst SUP_swap)
    67     apply (subst setsum_commute)
    68     by auto
    69   also have "\<dots> = (SUP m. \<Sum> j < m. SUP n. \<Sum> i < n. f i j)"
    70     apply (subst SUPR_pinfreal_setsum)
    71     by auto
    72   finally show ?thesis
    73     unfolding psuminf_def by auto
    74 qed
    75 
    76 lemma psuminf_SUP_eq:
    77   assumes "\<And>n i. f n i \<le> f (Suc n) i"
    78   shows "(\<Sum>\<^isub>\<infinity> i. SUP n::nat. f n i) = (SUP n::nat. \<Sum>\<^isub>\<infinity> i. f n i)"
    79 proof -
    80   { fix n :: nat
    81     have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
    82       using assms by (auto intro!: SUPR_pinfreal_setsum[symmetric]) }
    83   note * = this
    84   show ?thesis
    85     unfolding psuminf_def
    86     unfolding *
    87     apply (subst SUP_swap) ..
    88 qed
    89 
    90 subsection {* Standard Cubes *}
    91 
    92 definition cube :: "nat \<Rightarrow> 'a::ordered_euclidean_space set" where
    93   "cube n \<equiv> {\<chi>\<chi> i. - real n .. \<chi>\<chi> i. real n}"
    94 
    95 lemma cube_closed[intro]: "closed (cube n)"
    96   unfolding cube_def by auto
    97 
    98 lemma cube_subset[intro]: "n \<le> N \<Longrightarrow> cube n \<subseteq> cube N"
    99   by (fastsimp simp: eucl_le[where 'a='a] cube_def)
   100 
   101 lemma cube_subset_iff:
   102   "cube n \<subseteq> cube N \<longleftrightarrow> n \<le> N"
   103 proof
   104   assume subset: "cube n \<subseteq> (cube N::'a set)"
   105   then have "((\<chi>\<chi> i. real n)::'a) \<in> cube N"
   106     using DIM_positive[where 'a='a]
   107     by (fastsimp simp: cube_def eucl_le[where 'a='a])
   108   then show "n \<le> N"
   109     by (fastsimp simp: cube_def eucl_le[where 'a='a])
   110 next
   111   assume "n \<le> N" then show "cube n \<subseteq> (cube N::'a set)" by (rule cube_subset)
   112 qed
   113 
   114 lemma ball_subset_cube:"ball (0::'a::ordered_euclidean_space) (real n) \<subseteq> cube n"
   115   unfolding cube_def subset_eq mem_interval apply safe unfolding euclidean_lambda_beta'
   116 proof- fix x::'a and i assume as:"x\<in>ball 0 (real n)" "i<DIM('a)"
   117   thus "- real n \<le> x $$ i" "real n \<ge> x $$ i"
   118     using component_le_norm[of x i] by(auto simp: dist_norm)
   119 qed
   120 
   121 lemma mem_big_cube: obtains n where "x \<in> cube n"
   122 proof- from real_arch_lt[of "norm x"] guess n ..
   123   thus ?thesis apply-apply(rule that[where n=n])
   124     apply(rule ball_subset_cube[unfolded subset_eq,rule_format])
   125     by (auto simp add:dist_norm)
   126 qed
   127 
   128 lemma Union_inter_cube:"\<Union>{s \<inter> cube n |n. n \<in> UNIV} = s"
   129 proof safe case goal1
   130   from mem_big_cube[of x] guess n . note n=this
   131   show ?case unfolding Union_iff apply(rule_tac x="s \<inter> cube n" in bexI)
   132     using n goal1 by auto
   133 qed
   134 
   135 lemma gmeasurable_cube[intro]:"gmeasurable (cube n)"
   136   unfolding cube_def by auto
   137 
   138 lemma gmeasure_le_inter_cube[intro]: fixes s::"'a::ordered_euclidean_space set"
   139   assumes "gmeasurable (s \<inter> cube n)" shows "gmeasure (s \<inter> cube n) \<le> gmeasure (cube n::'a set)"
   140   apply(rule has_gmeasure_subset[of "s\<inter>cube n" _ "cube n"])
   141   unfolding has_gmeasure_measure[THEN sym] using assms by auto
   142 
   143 lemma has_gmeasure_cube[intro]: "(cube n::('a::ordered_euclidean_space) set)
   144   has_gmeasure ((2 * real n) ^ (DIM('a)))"
   145 proof-
   146   have "content {\<chi>\<chi> i. - real n..(\<chi>\<chi> i. real n)::'a} = (2 * real n) ^ (DIM('a))"
   147     apply(subst content_closed_interval) defer
   148     by (auto simp add:setprod_constant)
   149   thus ?thesis unfolding cube_def
   150     using has_gmeasure_interval(1)[of "(\<chi>\<chi> i. - real n)::'a" "(\<chi>\<chi> i. real n)::'a"]
   151     by auto
   152 qed
   153 
   154 lemma gmeasure_cube_eq[simp]:
   155   "gmeasure (cube n::('a::ordered_euclidean_space) set) = (2 * real n) ^ DIM('a)"
   156   by (intro measure_unique) auto
   157 
   158 lemma gmeasure_cube_ge_n: "gmeasure (cube n::('a::ordered_euclidean_space) set) \<ge> real n"
   159 proof cases
   160   assume "n = 0" then show ?thesis by simp
   161 next
   162   assume "n \<noteq> 0"
   163   have "real n \<le> (2 * real n)^1" by simp
   164   also have "\<dots> \<le> (2 * real n)^DIM('a)"
   165     using DIM_positive[where 'a='a] `n \<noteq> 0`
   166     by (intro power_increasing) auto
   167   also have "\<dots> = gmeasure (cube n::'a set)" by simp
   168   finally show ?thesis .
   169 qed
   170 
   171 lemma gmeasure_setsum:
   172   assumes "finite A" and "\<And>s t. s \<in> A \<Longrightarrow> t \<in> A \<Longrightarrow> s \<noteq> t \<Longrightarrow> f s \<inter> f t = {}"
   173     and "\<And>i. i \<in> A \<Longrightarrow> gmeasurable (f i)"
   174   shows "gmeasure (\<Union>i\<in>A. f i) = (\<Sum>i\<in>A. gmeasure (f i))"
   175 proof -
   176   have "gmeasure (\<Union>i\<in>A. f i) = gmeasure (\<Union>f ` A)" by auto
   177   also have "\<dots> = setsum gmeasure (f ` A)" using assms
   178   proof (intro measure_negligible_unions)
   179     fix X Y assume "X \<in> f`A" "Y \<in> f`A" "X \<noteq> Y"
   180     then have "X \<inter> Y = {}" using assms by auto
   181     then show "negligible (X \<inter> Y)" by auto
   182   qed auto
   183   also have "\<dots> = setsum gmeasure (f ` A - {{}})"
   184     using assms by (intro setsum_mono_zero_cong_right) auto
   185   also have "\<dots> = (\<Sum>i\<in>A - {i. f i = {}}. gmeasure (f i))"
   186   proof (intro setsum_reindex_cong inj_onI)
   187     fix s t assume *: "s \<in> A - {i. f i = {}}" "t \<in> A - {i. f i = {}}" "f s = f t"
   188     show "s = t"
   189     proof (rule ccontr)
   190       assume "s \<noteq> t" with assms(2)[of s t] * show False by auto
   191     qed
   192   qed auto
   193   also have "\<dots> = (\<Sum>i\<in>A. gmeasure (f i))"
   194     using assms by (intro setsum_mono_zero_cong_left) auto
   195   finally show ?thesis .
   196 qed
   197 
   198 lemma gmeasurable_finite_UNION[intro]:
   199   assumes "\<And>i. i \<in> S \<Longrightarrow> gmeasurable (A i)" "finite S"
   200   shows "gmeasurable (\<Union>i\<in>S. A i)"
   201   unfolding UNION_eq_Union_image using assms
   202   by (intro gmeasurable_finite_unions) auto
   203 
   204 lemma gmeasurable_countable_UNION[intro]:
   205   fixes A :: "nat \<Rightarrow> ('a::ordered_euclidean_space) set"
   206   assumes measurable: "\<And>i. gmeasurable (A i)"
   207     and finite: "\<And>n. gmeasure (UNION {.. n} A) \<le> B"
   208   shows "gmeasurable (\<Union>i. A i)"
   209 proof -
   210   have *: "\<And>n. \<Union>{A k |k. k \<le> n} = (\<Union>i\<le>n. A i)"
   211     "(\<Union>{A n |n. n \<in> UNIV}) = (\<Union>i. A i)" by auto
   212   show ?thesis
   213     by (rule gmeasurable_countable_unions_strong[of A B, unfolded *, OF assms])
   214 qed
   215 
   216 subsection {* Measurability *}
   217 
   218 definition lebesgue :: "'a::ordered_euclidean_space algebra" where
   219   "lebesgue = \<lparr> space = UNIV, sets = {A. \<forall>n. gmeasurable (A \<inter> cube n)} \<rparr>"
   220 
   221 lemma space_lebesgue[simp]:"space lebesgue = UNIV"
   222   unfolding lebesgue_def by auto
   223 
   224 lemma lebesgueD[dest]: assumes "S \<in> sets lebesgue"
   225   shows "\<And>n. gmeasurable (S \<inter> cube n)"
   226   using assms unfolding lebesgue_def by auto
   227 
   228 lemma lebesgueI[intro]: assumes "gmeasurable S"
   229   shows "S \<in> sets lebesgue" unfolding lebesgue_def cube_def
   230   using assms gmeasurable_interval by auto
   231 
   232 lemma lebesgueI2: "(\<And>n. gmeasurable (S \<inter> cube n)) \<Longrightarrow> S \<in> sets lebesgue"
   233   using assms unfolding lebesgue_def by auto
   234 
   235 interpretation lebesgue: sigma_algebra lebesgue
   236 proof
   237   show "sets lebesgue \<subseteq> Pow (space lebesgue)"
   238     unfolding lebesgue_def by auto
   239   show "{} \<in> sets lebesgue"
   240     using gmeasurable_empty by auto
   241   { fix A B :: "'a set" assume "A \<in> sets lebesgue" "B \<in> sets lebesgue"
   242     then show "A \<union> B \<in> sets lebesgue"
   243       by (auto intro: gmeasurable_union simp: lebesgue_def Int_Un_distrib2) }
   244   { fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets lebesgue"
   245     show "(\<Union>i. A i) \<in> sets lebesgue"
   246     proof (rule lebesgueI2)
   247       fix n show "gmeasurable ((\<Union>i. A i) \<inter> cube n)" unfolding UN_extend_simps
   248         using A
   249         by (intro gmeasurable_countable_UNION[where B="gmeasure (cube n::'a set)"])
   250            (auto intro!: measure_subset gmeasure_setsum simp: UN_extend_simps simp del: gmeasure_cube_eq UN_simps)
   251     qed }
   252   { fix A assume A: "A \<in> sets lebesgue" show "space lebesgue - A \<in> sets lebesgue"
   253     proof (rule lebesgueI2)
   254       fix n
   255       have *: "(space lebesgue - A) \<inter> cube n = cube n - (A \<inter> cube n)"
   256         unfolding lebesgue_def by auto
   257       show "gmeasurable ((space lebesgue - A) \<inter> cube n)" unfolding *
   258         using A by (auto intro!: gmeasurable_diff)
   259     qed }
   260 qed
   261 
   262 lemma lebesgueI_borel[intro, simp]: fixes s::"'a::ordered_euclidean_space set"
   263   assumes "s \<in> sets borel" shows "s \<in> sets lebesgue"
   264 proof- let ?S = "range (\<lambda>(a, b). {a .. (b :: 'a\<Colon>ordered_euclidean_space)})"
   265   have *:"?S \<subseteq> sets lebesgue" by auto
   266   have "s \<in> sigma_sets UNIV ?S" using assms
   267     unfolding borel_eq_atLeastAtMost by (simp add: sigma_def)
   268   thus ?thesis
   269     using lebesgue.sigma_subset[of "\<lparr> space = UNIV, sets = ?S\<rparr>", simplified, OF *]
   270     by (auto simp: sigma_def)
   271 qed
   272 
   273 lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set"
   274   assumes "negligible s" shows "s \<in> sets lebesgue"
   275 proof (rule lebesgueI2)
   276   fix n
   277   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)"
   278     unfolding indicator_def_raw by auto
   279   note assms[unfolded negligible_def,rule_format,of "(\<chi>\<chi> i. - real n)::'a" "\<chi>\<chi> i. real n"]
   280   thus "gmeasurable (s \<inter> cube n)" apply-apply(rule gmeasurableI[of _ 0]) unfolding has_gmeasure_def
   281     apply(subst(asm) has_integral_restrict_univ[THEN sym]) unfolding cube_def[symmetric]
   282     apply(subst has_integral_restrict_univ[THEN sym]) unfolding * .
   283 qed
   284 
   285 section {* The Lebesgue Measure *}
   286 
   287 definition "lmeasure A = (SUP n. Real (gmeasure (A \<inter> cube n)))"
   288 
   289 lemma lmeasure_eq_0: assumes "negligible S" shows "lmeasure S = 0"
   290 proof -
   291   from lebesgueI_negligible[OF assms]
   292   have "\<And>n. gmeasurable (S \<inter> cube n)" by auto
   293   from gmeasurable_measure_eq_0[OF this]
   294   have "\<And>n. gmeasure (S \<inter> cube n) = 0" using assms by auto
   295   then show ?thesis unfolding lmeasure_def by simp
   296 qed
   297 
   298 lemma lmeasure_iff_LIMSEQ:
   299   assumes "A \<in> sets lebesgue" "0 \<le> m"
   300   shows "lmeasure A = Real m \<longleftrightarrow> (\<lambda>n. (gmeasure (A \<inter> cube n))) ----> m"
   301   unfolding lmeasure_def using assms cube_subset[where 'a='a]
   302   by (intro SUP_eq_LIMSEQ monoI measure_subset) force+
   303 
   304 interpretation lebesgue: measure_space lebesgue lmeasure
   305 proof
   306   show "lmeasure {} = 0"
   307     by (auto intro!: lmeasure_eq_0)
   308   show "countably_additive lebesgue lmeasure"
   309   proof (unfold countably_additive_def, intro allI impI conjI)
   310     fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets lebesgue" "disjoint_family A"
   311     then have A: "\<And>i. A i \<in> sets lebesgue" by auto
   312     show "(\<Sum>\<^isub>\<infinity>n. lmeasure (A n)) = lmeasure (\<Union>i. A i)" unfolding lmeasure_def
   313     proof (subst psuminf_SUP_eq)
   314       { fix i n
   315         have "gmeasure (A i \<inter> cube n) \<le> gmeasure (A i \<inter> cube (Suc n))"
   316           using A cube_subset[of n "Suc n"] by (auto intro!: measure_subset)
   317         then show "Real (gmeasure (A i \<inter> cube n)) \<le> Real (gmeasure (A i \<inter> cube (Suc n)))"
   318           by auto }
   319       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)))"
   320       proof (intro arg_cong[where f="SUPR UNIV"] ext)
   321         fix n
   322         have sums: "(\<lambda>i. gmeasure (A i \<inter> cube n)) sums gmeasure (\<Union>{A i \<inter> cube n |i. i \<in> UNIV})"
   323         proof (rule has_gmeasure_countable_negligible_unions(2))
   324           fix i show "gmeasurable (A i \<inter> cube n)" using A by auto
   325         next
   326           fix i m :: nat assume "m \<noteq> i"
   327           then have "A m \<inter> cube n \<inter> (A i \<inter> cube n) = {}"
   328             using `disjoint_family A` unfolding disjoint_family_on_def by auto
   329           then show "negligible (A m \<inter> cube n \<inter> (A i \<inter> cube n))" by auto
   330         next
   331           fix i
   332           have "(\<Sum>k = 0..i. gmeasure (A k \<inter> cube n)) = gmeasure (\<Union>k\<le>i . A k \<inter> cube n)"
   333             unfolding atLeast0AtMost using A
   334           proof (intro gmeasure_setsum[symmetric])
   335             fix s t :: nat assume "s \<noteq> t" then have "A t \<inter> A s = {}"
   336               using `disjoint_family A` unfolding disjoint_family_on_def by auto
   337             then show "A s \<inter> cube n \<inter> (A t \<inter> cube n) = {}" by auto
   338           qed auto
   339           also have "\<dots> \<le> gmeasure (cube n :: 'b set)" using A
   340             by (intro measure_subset gmeasurable_finite_UNION) auto
   341           finally show "(\<Sum>k = 0..i. gmeasure (A k \<inter> cube n)) \<le> gmeasure (cube n :: 'b set)" .
   342         qed
   343         show "(\<Sum>\<^isub>\<infinity>i. Real (gmeasure (A i \<inter> cube n))) = Real (gmeasure ((\<Union>i. A i) \<inter> cube n))"
   344           unfolding psuminf_def
   345           apply (subst setsum_Real)
   346           apply (simp add: measure_pos_le)
   347         proof (rule SUP_eq_LIMSEQ[THEN iffD2])
   348           have "(\<Union>{A i \<inter> cube n |i. i \<in> UNIV}) = (\<Union>i. A i) \<inter> cube n" by auto
   349           with sums show "(\<lambda>i. \<Sum>k<i. gmeasure (A k \<inter> cube n)) ----> gmeasure ((\<Union>i. A i) \<inter> cube n)"
   350             unfolding sums_def atLeast0LessThan by simp
   351         qed (auto intro!: monoI setsum_nonneg setsum_mono2)
   352       qed
   353     qed
   354   qed
   355 qed
   356 
   357 lemma lmeasure_finite_has_gmeasure: assumes "s \<in> sets lebesgue" "lmeasure s = Real m" "0 \<le> m"
   358   shows "s has_gmeasure m"
   359 proof-
   360   have *:"(\<lambda>n. (gmeasure (s \<inter> cube n))) ----> m"
   361     using `lmeasure s = Real m` unfolding lmeasure_iff_LIMSEQ[OF `s \<in> sets lebesgue` `0 \<le> m`] .
   362   have s: "\<And>n. gmeasurable (s \<inter> cube n)" using assms by auto
   363   have "(\<lambda>x. if x \<in> s then 1 else (0::real)) integrable_on UNIV \<and>
   364     (\<lambda>k. integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)))
   365     ----> integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)"
   366   proof(rule monotone_convergence_increasing)
   367     have "lmeasure s \<le> Real m" using `lmeasure s = Real m` by simp
   368     then have "\<forall>n. gmeasure (s \<inter> cube n) \<le> m"
   369       unfolding lmeasure_def complete_lattice_class.SUP_le_iff
   370       using `0 \<le> m` by (auto simp: measure_pos_le)
   371     thus *:"bounded {integral UNIV (\<lambda>x. if x \<in> s \<inter> cube k then 1 else (0::real)) |k. True}"
   372       unfolding integral_measure_univ[OF s] bounded_def apply-
   373       apply(rule_tac x=0 in exI,rule_tac x=m in exI) unfolding dist_real_def
   374       by (auto simp: measure_pos_le)
   375     show "\<forall>k. (\<lambda>x. if x \<in> s \<inter> cube k then (1::real) else 0) integrable_on UNIV"
   376       unfolding integrable_restrict_univ
   377       using s unfolding gmeasurable_def has_gmeasure_def by auto
   378     have *:"\<And>n. n \<le> Suc n" by auto
   379     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))"
   380       using cube_subset[OF *] by fastsimp
   381     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))"
   382       unfolding Lim_sequentially
   383     proof safe case goal1 from real_arch_lt[of "norm x"] guess N .. note N = this
   384       show ?case apply(rule_tac x=N in exI)
   385       proof safe case goal1
   386         have "x \<in> cube n" using cube_subset[OF goal1] N
   387           using ball_subset_cube[of N] by(auto simp: dist_norm)
   388         thus ?case using `e>0` by auto
   389       qed
   390     qed
   391   qed note ** = conjunctD2[OF this]
   392   hence *:"m = integral UNIV (\<lambda>x. if x \<in> s then 1 else 0)" apply-
   393     apply(rule LIMSEQ_unique[OF _ **(2)]) unfolding measure_integral_univ[THEN sym,OF s] using * .
   394   show ?thesis unfolding has_gmeasure * apply(rule integrable_integral) using ** by auto
   395 qed
   396 
   397 lemma lmeasure_finite_gmeasurable: assumes "s \<in> sets lebesgue" "lmeasure s \<noteq> \<omega>"
   398   shows "gmeasurable s"
   399 proof (cases "lmeasure s")
   400   case (preal m) from lmeasure_finite_has_gmeasure[OF `s \<in> sets lebesgue` this]
   401   show ?thesis unfolding gmeasurable_def by auto
   402 qed (insert assms, auto)
   403 
   404 lemma has_gmeasure_lmeasure: assumes "s has_gmeasure m"
   405   shows "lmeasure s = Real m"
   406 proof-
   407   have gmea:"gmeasurable s" using assms by auto
   408   then have s: "s \<in> sets lebesgue" by auto
   409   have m:"m \<ge> 0" using assms by auto
   410   have *:"m = gmeasure (\<Union>{s \<inter> cube n |n. n \<in> UNIV})" unfolding Union_inter_cube
   411     using assms by(rule measure_unique[THEN sym])
   412   show ?thesis
   413     unfolding lmeasure_iff_LIMSEQ[OF s `0 \<le> m`] unfolding *
   414     apply(rule gmeasurable_nested_unions[THEN conjunct2, where B1="gmeasure s"])
   415   proof- fix n::nat show *:"gmeasurable (s \<inter> cube n)"
   416       using gmeasurable_inter[OF gmea gmeasurable_cube] .
   417     show "gmeasure (s \<inter> cube n) \<le> gmeasure s" apply(rule measure_subset)
   418       apply(rule * gmea)+ by auto
   419     show "s \<inter> cube n \<subseteq> s \<inter> cube (Suc n)" using cube_subset[of n "Suc n"] by auto
   420   qed
   421 qed
   422 
   423 lemma has_gmeasure_iff_lmeasure:
   424   "A has_gmeasure m \<longleftrightarrow> (A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m)"
   425 proof
   426   assume "A has_gmeasure m"
   427   with has_gmeasure_lmeasure[OF this]
   428   have "gmeasurable A" "0 \<le> m" "lmeasure A = Real m" by auto
   429   then show "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m" by auto
   430 next
   431   assume "A \<in> sets lebesgue \<and> 0 \<le> m \<and> lmeasure A = Real m"
   432   then show "A has_gmeasure m" by (intro lmeasure_finite_has_gmeasure) auto
   433 qed
   434 
   435 lemma gmeasure_lmeasure: assumes "gmeasurable s" shows "lmeasure s = Real (gmeasure s)"
   436 proof -
   437   note has_gmeasure_measureI[OF assms]
   438   note has_gmeasure_lmeasure[OF this]
   439   thus ?thesis .
   440 qed
   441 
   442 lemma lebesgue_simple_function_indicator:
   443   fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
   444   assumes f:"lebesgue.simple_function f"
   445   shows "f = (\<lambda>x. (\<Sum>y \<in> f ` UNIV. y * indicator (f -` {y}) x))"
   446   apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto
   447 
   448 lemma lmeasure_gmeasure:
   449   "gmeasurable s \<Longrightarrow> gmeasure s = real (lmeasure s)"
   450   by (subst gmeasure_lmeasure) auto
   451 
   452 lemma lmeasure_finite: assumes "gmeasurable s" shows "lmeasure s \<noteq> \<omega>"
   453   using gmeasure_lmeasure[OF assms] by auto
   454 
   455 lemma negligible_iff_lebesgue_null_sets:
   456   "negligible A \<longleftrightarrow> A \<in> lebesgue.null_sets"
   457 proof
   458   assume "negligible A"
   459   from this[THEN lebesgueI_negligible] this[THEN lmeasure_eq_0]
   460   show "A \<in> lebesgue.null_sets" by auto
   461 next
   462   assume A: "A \<in> lebesgue.null_sets"
   463   then have *:"gmeasurable A" using lmeasure_finite_gmeasurable[of A] by auto
   464   show "negligible A"
   465     unfolding gmeasurable_measure_eq_0[OF *, symmetric]
   466     unfolding lmeasure_gmeasure[OF *] using A by auto
   467 qed
   468 
   469 lemma
   470   fixes a b ::"'a::ordered_euclidean_space"
   471   shows lmeasure_atLeastAtMost[simp]: "lmeasure {a..b} = Real (content {a..b})"
   472     and lmeasure_greaterThanLessThan[simp]: "lmeasure {a <..< b} = Real (content {a..b})"
   473   using has_gmeasure_interval[of a b] by (auto intro!: has_gmeasure_lmeasure)
   474 
   475 lemma lmeasure_cube:
   476   "lmeasure (cube n::('a::ordered_euclidean_space) set) = (Real ((2 * real n) ^ (DIM('a))))"
   477   by (intro has_gmeasure_lmeasure) auto
   478 
   479 lemma lmeasure_UNIV[intro]: "lmeasure UNIV = \<omega>"
   480   unfolding lmeasure_def SUP_\<omega>
   481 proof (intro allI impI)
   482   fix x assume "x < \<omega>"
   483   then obtain r where r: "x = Real r" "0 \<le> r" by (cases x) auto
   484   then obtain n where n: "r < of_nat n" using ex_less_of_nat by auto
   485   show "\<exists>i\<in>UNIV. x < Real (gmeasure (UNIV \<inter> cube i))"
   486   proof (intro bexI[of _ n])
   487     have "x < Real (of_nat n)" using n r by auto
   488     also have "Real (of_nat n) \<le> Real (gmeasure (UNIV \<inter> cube n))"
   489       using gmeasure_cube_ge_n[of n] by (auto simp: real_eq_of_nat[symmetric])
   490     finally show "x < Real (gmeasure (UNIV \<inter> cube n))" .
   491   qed auto
   492 qed
   493 
   494 lemma atLeastAtMost_singleton_euclidean[simp]:
   495   fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}"
   496   by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a])
   497 
   498 lemma content_singleton[simp]: "content {a} = 0"
   499 proof -
   500   have "content {a .. a} = 0"
   501     by (subst content_closed_interval) auto
   502   then show ?thesis by simp
   503 qed
   504 
   505 lemma lmeasure_singleton[simp]:
   506   fixes a :: "'a::ordered_euclidean_space" shows "lmeasure {a} = 0"
   507   using has_gmeasure_interval[of a a] unfolding zero_pinfreal_def
   508   by (intro has_gmeasure_lmeasure)
   509      (simp add: content_closed_interval DIM_positive)
   510 
   511 declare content_real[simp]
   512 
   513 lemma
   514   fixes a b :: real
   515   shows lmeasure_real_greaterThanAtMost[simp]:
   516     "lmeasure {a <.. b} = Real (if a \<le> b then b - a else 0)"
   517 proof cases
   518   assume "a < b"
   519   then have "lmeasure {a <.. b} = lmeasure {a <..< b} + lmeasure {b}"
   520     by (subst lebesgue.measure_additive)
   521        (auto intro!: lebesgueI_borel arg_cong[where f=lmeasure])
   522   then show ?thesis by auto
   523 qed auto
   524 
   525 lemma
   526   fixes a b :: real
   527   shows lmeasure_real_atLeastLessThan[simp]:
   528     "lmeasure {a ..< b} = Real (if a \<le> b then b - a else 0)" (is ?eqlt)
   529 proof cases
   530   assume "a < b"
   531   then have "lmeasure {a ..< b} = lmeasure {a} + lmeasure {a <..< b}"
   532     by (subst lebesgue.measure_additive)
   533        (auto intro!: lebesgueI_borel arg_cong[where f=lmeasure])
   534   then show ?thesis by auto
   535 qed auto
   536 
   537 interpretation borel: measure_space borel lmeasure
   538 proof
   539   show "countably_additive borel lmeasure"
   540     using lebesgue.ca unfolding countably_additive_def
   541     apply safe apply (erule_tac x=A in allE) by auto
   542 qed auto
   543 
   544 interpretation borel: sigma_finite_measure borel lmeasure
   545 proof (default, intro conjI exI[of _ "\<lambda>n. cube n"])
   546   show "range cube \<subseteq> sets borel" by (auto intro: borel_closed)
   547   { fix x have "\<exists>n. x\<in>cube n" using mem_big_cube by auto }
   548   thus "(\<Union>i. cube i) = space borel" by auto
   549   show "\<forall>i. lmeasure (cube i) \<noteq> \<omega>" unfolding lmeasure_cube by auto
   550 qed
   551 
   552 interpretation lebesgue: sigma_finite_measure lebesgue lmeasure
   553 proof
   554   from borel.sigma_finite guess A ..
   555   moreover then have "range A \<subseteq> sets lebesgue" using lebesgueI_borel by blast
   556   ultimately show "\<exists>A::nat \<Rightarrow> 'b set. range A \<subseteq> sets lebesgue \<and> (\<Union>i. A i) = space lebesgue \<and> (\<forall>i. lmeasure (A i) \<noteq> \<omega>)"
   557     by auto
   558 qed
   559 
   560 lemma simple_function_has_integral:
   561   fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
   562   assumes f:"lebesgue.simple_function f"
   563   and f':"\<forall>x. f x \<noteq> \<omega>"
   564   and om:"\<forall>x\<in>range f. lmeasure (f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0"
   565   shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV"
   566   unfolding lebesgue.simple_integral_def
   567   apply(subst lebesgue_simple_function_indicator[OF f])
   568 proof- case goal1
   569   have *:"\<And>x. \<forall>y\<in>range f. y * indicator (f -` {y}) x \<noteq> \<omega>"
   570     "\<forall>x\<in>range f. x * lmeasure (f -` {x} \<inter> UNIV) \<noteq> \<omega>"
   571     using f' om unfolding indicator_def by auto
   572   show ?case unfolding space_lebesgue real_of_pinfreal_setsum'[OF *(1),THEN sym]
   573     unfolding real_of_pinfreal_setsum'[OF *(2),THEN sym]
   574     unfolding real_of_pinfreal_setsum space_lebesgue
   575     apply(rule has_integral_setsum)
   576   proof safe show "finite (range f)" using f by (auto dest: lebesgue.simple_functionD)
   577     fix y::'a show "((\<lambda>x. real (f y * indicator (f -` {f y}) x)) has_integral
   578       real (f y * lmeasure (f -` {f y} \<inter> UNIV))) UNIV"
   579     proof(cases "f y = 0") case False
   580       have mea:"gmeasurable (f -` {f y})" apply(rule lmeasure_finite_gmeasurable)
   581         using assms unfolding lebesgue.simple_function_def using False by auto
   582       have *:"\<And>x. real (indicator (f -` {f y}) x::pinfreal) = (if x \<in> f -` {f y} then 1 else 0)" by auto
   583       show ?thesis unfolding real_of_pinfreal_mult[THEN sym]
   584         apply(rule has_integral_cmul[where 'b=real, unfolded real_scaleR_def])
   585         unfolding Int_UNIV_right lmeasure_gmeasure[OF mea,THEN sym]
   586         unfolding measure_integral_univ[OF mea] * apply(rule integrable_integral)
   587         unfolding gmeasurable_integrable[THEN sym] using mea .
   588     qed auto
   589   qed qed
   590 
   591 lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
   592   unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
   593   using assms by auto
   594 
   595 lemma simple_function_has_integral':
   596   fixes f::"'a::ordered_euclidean_space \<Rightarrow> pinfreal"
   597   assumes f:"lebesgue.simple_function f"
   598   and i: "lebesgue.simple_integral f \<noteq> \<omega>"
   599   shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV"
   600 proof- let ?f = "\<lambda>x. if f x = \<omega> then 0 else f x"
   601   { fix x have "real (f x) = real (?f x)" by (cases "f x") auto } note * = this
   602   have **:"{x. f x \<noteq> ?f x} = f -` {\<omega>}" by auto
   603   have **:"lmeasure {x\<in>space lebesgue. f x \<noteq> ?f x} = 0"
   604     using lebesgue.simple_integral_omega[OF assms] by(auto simp add:**)
   605   show ?thesis apply(subst lebesgue.simple_integral_cong'[OF f _ **])
   606     apply(rule lebesgue.simple_function_compose1[OF f])
   607     unfolding * defer apply(rule simple_function_has_integral)
   608   proof-
   609     show "lebesgue.simple_function ?f"
   610       using lebesgue.simple_function_compose1[OF f] .
   611     show "\<forall>x. ?f x \<noteq> \<omega>" by auto
   612     show "\<forall>x\<in>range ?f. lmeasure (?f -` {x} \<inter> UNIV) = \<omega> \<longrightarrow> x = 0"
   613     proof (safe, simp, safe, rule ccontr)
   614       fix y assume "f y \<noteq> \<omega>" "f y \<noteq> 0"
   615       hence "(\<lambda>x. if f x = \<omega> then 0 else f x) -` {if f y = \<omega> then 0 else f y} = f -` {f y}"
   616         by (auto split: split_if_asm)
   617       moreover assume "lmeasure ((\<lambda>x. if f x = \<omega> then 0 else f x) -` {if f y = \<omega> then 0 else f y}) = \<omega>"
   618       ultimately have "lmeasure (f -` {f y}) = \<omega>" by simp
   619       moreover
   620       have "f y * lmeasure (f -` {f y}) \<noteq> \<omega>" using i f
   621         unfolding lebesgue.simple_integral_def setsum_\<omega> lebesgue.simple_function_def
   622         by auto
   623       ultimately have "f y = 0" by (auto split: split_if_asm)
   624       then show False using `f y \<noteq> 0` by simp
   625     qed
   626   qed
   627 qed
   628 
   629 lemma (in measure_space) positive_integral_monotone_convergence:
   630   fixes f::"nat \<Rightarrow> 'a \<Rightarrow> pinfreal"
   631   assumes i: "\<And>i. f i \<in> borel_measurable M" and mono: "\<And>x. mono (\<lambda>n. f n x)"
   632   and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
   633   shows "u \<in> borel_measurable M"
   634   and "(\<lambda>i. positive_integral (f i)) ----> positive_integral u" (is ?ilim)
   635 proof -
   636   from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
   637   show ?ilim using mono lim i by auto
   638   have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal
   639     unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
   640   moreover have "(SUP i. f i) \<in> borel_measurable M"
   641     using i by (rule borel_measurable_SUP)
   642   ultimately show "u \<in> borel_measurable M" by simp
   643 qed
   644 
   645 lemma positive_integral_has_integral:
   646   fixes f::"'a::ordered_euclidean_space => pinfreal"
   647   assumes f:"f \<in> borel_measurable lebesgue"
   648   and int_om:"lebesgue.positive_integral f \<noteq> \<omega>"
   649   and f_om:"\<forall>x. f x \<noteq> \<omega>" (* TODO: remove this *)
   650   shows "((\<lambda>x. real (f x)) has_integral (real (lebesgue.positive_integral f))) UNIV"
   651 proof- let ?i = "lebesgue.positive_integral f"
   652   from lebesgue.borel_measurable_implies_simple_function_sequence[OF f]
   653   guess u .. note conjunctD2[OF this,rule_format] note u = conjunctD2[OF this(1)] this(2)
   654   let ?u = "\<lambda>i x. real (u i x)" and ?f = "\<lambda>x. real (f x)"
   655   have u_simple:"\<And>k. lebesgue.simple_integral (u k) = lebesgue.positive_integral (u k)"
   656     apply(subst lebesgue.positive_integral_eq_simple_integral[THEN sym,OF u(1)]) ..
   657   have int_u_le:"\<And>k. lebesgue.simple_integral (u k) \<le> lebesgue.positive_integral f"
   658     unfolding u_simple apply(rule lebesgue.positive_integral_mono)
   659     using isoton_Sup[OF u(3)] unfolding le_fun_def by auto
   660   have u_int_om:"\<And>i. lebesgue.simple_integral (u i) \<noteq> \<omega>"
   661   proof- case goal1 thus ?case using int_u_le[of i] int_om by auto qed
   662 
   663   note u_int = simple_function_has_integral'[OF u(1) this]
   664   have "(\<lambda>x. real (f x)) integrable_on UNIV \<and>
   665     (\<lambda>k. Integration.integral UNIV (\<lambda>x. real (u k x))) ----> Integration.integral UNIV (\<lambda>x. real (f x))"
   666     apply(rule monotone_convergence_increasing) apply(rule,rule,rule u_int)
   667   proof safe case goal1 show ?case apply(rule real_of_pinfreal_mono) using u(2,3) by auto
   668   next case goal2 show ?case using u(3) apply(subst lim_Real[THEN sym])
   669       prefer 3 apply(subst Real_real') defer apply(subst Real_real')
   670       using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] using f_om u by auto
   671   next case goal3
   672     show ?case apply(rule bounded_realI[where B="real (lebesgue.positive_integral f)"])
   673       apply safe apply(subst abs_of_nonneg) apply(rule integral_nonneg,rule) apply(rule u_int)
   674       unfolding integral_unique[OF u_int] defer apply(rule real_of_pinfreal_mono[OF _ int_u_le])
   675       using u int_om by auto
   676   qed note int = conjunctD2[OF this]
   677 
   678   have "(\<lambda>i. lebesgue.simple_integral (u i)) ----> ?i" unfolding u_simple
   679     apply(rule lebesgue.positive_integral_monotone_convergence(2))
   680     apply(rule lebesgue.borel_measurable_simple_function[OF u(1)])
   681     using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] by auto
   682   hence "(\<lambda>i. real (lebesgue.simple_integral (u i))) ----> real ?i" apply-
   683     apply(subst lim_Real[THEN sym]) prefer 3
   684     apply(subst Real_real') defer apply(subst Real_real')
   685     using u f_om int_om u_int_om by auto
   686   note * = LIMSEQ_unique[OF this int(2)[unfolded integral_unique[OF u_int]]]
   687   show ?thesis unfolding * by(rule integrable_integral[OF int(1)])
   688 qed
   689 
   690 lemma lebesgue_integral_has_integral:
   691   fixes f::"'a::ordered_euclidean_space => real"
   692   assumes f:"lebesgue.integrable f"
   693   shows "(f has_integral (lebesgue.integral f)) UNIV"
   694 proof- let ?n = "\<lambda>x. - min (f x) 0" and ?p = "\<lambda>x. max (f x) 0"
   695   have *:"f = (\<lambda>x. ?p x - ?n x)" apply rule by auto
   696   note f = lebesgue.integrableD[OF f]
   697   show ?thesis unfolding lebesgue.integral_def apply(subst *)
   698   proof(rule has_integral_sub) case goal1
   699     have *:"\<forall>x. Real (f x) \<noteq> \<omega>" by auto
   700     note lebesgue.borel_measurable_Real[OF f(1)]
   701     from positive_integral_has_integral[OF this f(2) *]
   702     show ?case unfolding real_Real_max .
   703   next case goal2
   704     have *:"\<forall>x. Real (- f x) \<noteq> \<omega>" by auto
   705     note lebesgue.borel_measurable_uminus[OF f(1)]
   706     note lebesgue.borel_measurable_Real[OF this]
   707     from positive_integral_has_integral[OF this f(3) *]
   708     show ?case unfolding real_Real_max minus_min_eq_max by auto
   709   qed
   710 qed
   711 
   712 lemma continuous_on_imp_borel_measurable:
   713   fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::ordered_euclidean_space"
   714   assumes "continuous_on UNIV f"
   715   shows "f \<in> borel_measurable lebesgue"
   716   apply(rule lebesgue.borel_measurableI)
   717   using continuous_open_preimage[OF assms] unfolding vimage_def by auto
   718 
   719 lemma (in measure_space) integral_monotone_convergence_pos':
   720   assumes i: "\<And>i. integrable (f i)" and mono: "\<And>x. mono (\<lambda>n. f n x)"
   721   and pos: "\<And>x i. 0 \<le> f i x"
   722   and lim: "\<And>x. (\<lambda>i. f i x) ----> u x"
   723   and ilim: "(\<lambda>i. integral (f i)) ----> x"
   724   shows "integrable u \<and> integral u = x"
   725   using integral_monotone_convergence_pos[OF assms] by auto
   726 
   727 definition e2p :: "'a::ordered_euclidean_space \<Rightarrow> (nat \<Rightarrow> real)" where
   728   "e2p x = (\<lambda>i\<in>{..<DIM('a)}. x$$i)"
   729 
   730 definition p2e :: "(nat \<Rightarrow> real) \<Rightarrow> 'a::ordered_euclidean_space" where
   731   "p2e x = (\<chi>\<chi> i. x i)"
   732 
   733 lemma bij_euclidean_component:
   734   "bij_betw (e2p::'a::ordered_euclidean_space \<Rightarrow> _) (UNIV :: 'a set)
   735   ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))"
   736   unfolding bij_betw_def e2p_def_raw
   737 proof let ?e = "\<lambda>x.\<lambda>i\<in>{..<DIM('a::ordered_euclidean_space)}. (x::'a)$$i"
   738   show "inj ?e" unfolding inj_on_def restrict_def apply(subst euclidean_eq) apply safe
   739     apply(drule_tac x=i in fun_cong) by auto
   740   { fix x::"nat \<Rightarrow> real" assume x:"\<forall>i. i \<notin> {..<DIM('a)} \<longrightarrow> x i = undefined"
   741     hence "x = ?e (\<chi>\<chi> i. x i)" apply-apply(rule,case_tac "xa<DIM('a)") by auto
   742     hence "x \<in> range ?e" by fastsimp
   743   } thus "range ?e = ({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}"
   744     unfolding extensional_def using DIM_positive by auto
   745 qed
   746 
   747 lemma bij_p2e:
   748   "bij_betw (p2e::_ \<Rightarrow> 'a::ordered_euclidean_space) ({..<DIM('a)} \<rightarrow>\<^isub>E (UNIV :: real set))
   749   (UNIV :: 'a set)" (is "bij_betw ?p ?U _")
   750   unfolding bij_betw_def
   751 proof show "inj_on ?p ?U" unfolding inj_on_def p2e_def
   752     apply(subst euclidean_eq) apply(safe,rule) unfolding extensional_def
   753     apply(case_tac "xa<DIM('a)") by auto
   754   { fix x::'a have "x \<in> ?p ` extensional {..<DIM('a)}"
   755       unfolding image_iff apply(rule_tac x="\<lambda>i. if i<DIM('a) then x$$i else undefined" in bexI)
   756       apply(subst euclidean_eq,safe) unfolding p2e_def extensional_def by auto
   757   } thus "?p ` ?U = UNIV" by auto
   758 qed
   759 
   760 lemma e2p_p2e[simp]: fixes z::"'a::ordered_euclidean_space"
   761   assumes "x \<in> extensional {..<DIM('a)}"
   762   shows "e2p (p2e x::'a) = x"
   763 proof fix i::nat
   764   show "e2p (p2e x::'a) i = x i" unfolding e2p_def p2e_def restrict_def
   765     using assms unfolding extensional_def by auto
   766 qed
   767 
   768 lemma p2e_e2p[simp]: fixes x::"'a::ordered_euclidean_space"
   769   shows "p2e (e2p x) = x"
   770   apply(subst euclidean_eq) unfolding e2p_def p2e_def restrict_def by auto
   771 
   772 interpretation borel_product: product_sigma_finite "\<lambda>x. borel::real algebra" "\<lambda>x. lmeasure"
   773   by default
   774 
   775 lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
   776   unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
   777 
   778 lemma borel_vimage_algebra_eq:
   779   "sigma_algebra.vimage_algebra
   780          (borel :: ('a::ordered_euclidean_space) algebra) ({..<DIM('a)} \<rightarrow>\<^isub>E UNIV) p2e =
   781   sigma (product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)} )"
   782 proof- note bor = borel_eq_lessThan
   783   def F \<equiv> "product_algebra (\<lambda>x. \<lparr> space = UNIV::real set, sets = range (\<lambda>a. {..<a}) \<rparr>) {..<DIM('a)}"
   784   def E \<equiv> "\<lparr>space = (UNIV::'a set), sets = range lessThan\<rparr>"
   785   have *:"(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}) = space F" unfolding F_def by auto
   786   show ?thesis unfolding F_def[symmetric] * bor
   787   proof(rule vimage_algebra_sigma,unfold E_def[symmetric])
   788     show "sets E \<subseteq> Pow (space E)" "p2e \<in> space F \<rightarrow> space E" unfolding E_def by auto
   789   next fix A assume "A \<in> sets F"
   790     hence A:"A \<in> (Pi\<^isub>E {..<DIM('a)}) ` ({..<DIM('a)} \<rightarrow> range lessThan)"
   791       unfolding F_def product_algebra_def algebra.simps .
   792     then guess B unfolding image_iff .. note B=this
   793     hence "\<forall>x<DIM('a). B x \<in> range lessThan" by auto
   794     hence "\<forall>x. \<exists>xa. x<DIM('a) \<longrightarrow> B x = {..<xa}" unfolding image_iff by auto
   795     from choice[OF this] guess b .. note b=this
   796     hence b':"\<forall>i<DIM('a). Sup (B i) = b i" using Sup_lessThan by auto
   797 
   798     show "A \<in> (\<lambda>X. p2e -` X \<inter> space F) ` sets E" unfolding image_iff B
   799     proof(rule_tac x="{..< \<chi>\<chi> i. Sup (B i)}" in bexI)
   800       show "Pi\<^isub>E {..<DIM('a)} B = p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter> space F"
   801         unfolding F_def E_def product_algebra_def algebra.simps
   802       proof(rule,unfold subset_eq,rule_tac[!] ballI)
   803         fix x assume "x \<in> Pi\<^isub>E {..<DIM('a)} B"
   804         hence *:"\<forall>i<DIM('a). x i < b i" "\<forall>i\<ge>DIM('a). x i = undefined"
   805           unfolding Pi_def extensional_def using b by auto
   806         have "(p2e x::'a) < (\<chi>\<chi> i. Sup (B i))" unfolding less_prod_def eucl_less[of "p2e x"]
   807           apply safe unfolding euclidean_lambda_beta b'[rule_format] p2e_def using * by auto
   808         moreover have "x \<in> extensional {..<DIM('a)}"
   809           using *(2) unfolding extensional_def by auto
   810         ultimately show "x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i)) ::'a} \<inter>
   811           (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
   812       next fix x assume as:"x \<in> p2e -` {..<(\<chi>\<chi> i. Sup (B i))::'a} \<inter>
   813           (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   814         hence "p2e x < ((\<chi>\<chi> i. Sup (B i))::'a)" by auto
   815         hence "\<forall>i<DIM('a). x i \<in> B i" apply-apply(subst(asm) eucl_less)
   816           unfolding p2e_def using b b' by auto
   817         thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
   818       qed
   819       show "{..<(\<chi>\<chi> i. Sup (B i))::'a} \<in> sets E" unfolding E_def algebra.simps by auto
   820     qed
   821   next fix A assume "A \<in> sets E"
   822     then guess a unfolding E_def algebra.simps image_iff .. note a = this(2)
   823     def B \<equiv> "\<lambda>i. {..<a $$ i}"
   824     show "p2e -` A \<inter> space F \<in> sets F" unfolding F_def
   825       unfolding product_algebra_def algebra.simps image_iff
   826       apply(rule_tac x=B in bexI) apply rule unfolding subset_eq apply(rule_tac[1-2] ballI)
   827     proof- show "B \<in> {..<DIM('a)} \<rightarrow> range lessThan" unfolding B_def by auto
   828       fix x assume as:"x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   829       hence "p2e x \<in> A" by auto
   830       hence "\<forall>i<DIM('a). x i \<in> B i" unfolding B_def a lessThan_iff
   831         apply-apply(subst (asm) eucl_less) unfolding p2e_def by auto
   832       thus "x \<in> Pi\<^isub>E {..<DIM('a)} B" using as unfolding Pi_def extensional_def by auto
   833     next fix x assume x:"x \<in> Pi\<^isub>E {..<DIM('a)} B"
   834       moreover have "p2e x \<in> A" unfolding a lessThan_iff p2e_def apply(subst eucl_less)
   835         using x unfolding Pi_def extensional_def B_def by auto
   836       ultimately show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})" by auto
   837     qed
   838   qed
   839 qed
   840 
   841 lemma Real_mult_nonneg: assumes "x \<ge> 0" "y \<ge> 0"
   842   shows "Real (x * y) = Real x * Real y" using assms by auto
   843 
   844 lemma Real_setprod: assumes "\<forall>x\<in>A. f x \<ge> 0" shows "Real (setprod f A) = setprod (\<lambda>x. Real (f x)) A"
   845 proof(cases "finite A")
   846   case True thus ?thesis using assms
   847   proof(induct A) case (insert x A)
   848     have "0 \<le> setprod f A" apply(rule setprod_nonneg) using insert by auto
   849     thus ?case unfolding setprod_insert[OF insert(1-2)] apply-
   850       apply(subst Real_mult_nonneg) prefer 3 apply(subst insert(3)[THEN sym])
   851       using insert by auto
   852   qed auto
   853 qed auto
   854 
   855 lemma e2p_Int:"e2p ` A \<inter> e2p ` B = e2p ` (A \<inter> B)" (is "?L = ?R")
   856   apply(rule image_Int[THEN sym]) using bij_euclidean_component
   857   unfolding bij_betw_def by auto
   858 
   859 lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space"
   860   shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). e2p ` {a..b})\<rparr>"
   861   unfolding Int_stable_def algebra.select_convs
   862 proof safe fix a b x y::'a
   863   have *:"e2p ` {a..b} \<inter> e2p ` {x..y} =
   864     (\<lambda>(a, b). e2p ` {a..b}) (\<chi>\<chi> i. max (a $$ i) (x $$ i), \<chi>\<chi> i. min (b $$ i) (y $$ i)::'a)"
   865     unfolding e2p_Int inter_interval by auto
   866   show "e2p ` {a..b} \<inter> e2p ` {x..y} \<in> range (\<lambda>(a, b). e2p ` {a..b::'a})" unfolding *
   867     apply(rule range_eqI) ..
   868 qed
   869 
   870 lemma Int_stable_cuboids': fixes x::"'a::ordered_euclidean_space"
   871   shows "Int_stable \<lparr>space = UNIV, sets = range (\<lambda>(a, b::'a). {a..b})\<rparr>"
   872   unfolding Int_stable_def algebra.select_convs
   873   apply safe unfolding inter_interval by auto
   874 
   875 lemma product_borel_eq_vimage:
   876   "sigma (product_algebra (\<lambda>x. borel) {..<DIM('a::ordered_euclidean_space)}) =
   877   sigma_algebra.vimage_algebra borel (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})
   878   (p2e:: _ \<Rightarrow> 'a::ordered_euclidean_space)"
   879   unfolding borel_vimage_algebra_eq unfolding borel_eq_lessThan
   880   apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>i. \<lambda>n. lessThan (real n)"])
   881   unfolding lessThan_iff
   882 proof- fix i assume i:"i<DIM('a)"
   883   show "(\<lambda>n. {..<real n}) \<up> space \<lparr>space = UNIV, sets = range lessThan\<rparr>"
   884     by(auto intro!:real_arch_lt isotoneI)
   885 qed auto
   886 
   887 lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f"
   888   shows "disjoint_family_on (\<lambda>x. f ` A x) S"
   889   unfolding disjoint_family_on_def
   890 proof(rule,rule,rule)
   891   fix x1 x2 assume x:"x1 \<in> S" "x2 \<in> S" "x1 \<noteq> x2"
   892   show "f ` A x1 \<inter> f ` A x2 = {}"
   893   proof(rule ccontr) case goal1
   894     then obtain z where z:"z \<in> f ` A x1 \<inter> f ` A x2" by auto
   895     then obtain z1 z2 where z12:"z1 \<in> A x1" "z2 \<in> A x2" "f z1 = z" "f z2 = z" by auto
   896     hence "z1 = z2" using assms(2) unfolding inj_on_def by blast
   897     hence "x1 = x2" using z12(1-2) using assms[unfolded disjoint_family_on_def] using x by auto
   898     thus False using x(3) by auto
   899   qed
   900 qed
   901 
   902 declare restrict_extensional[intro]
   903 
   904 lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \<in> extensional {..<DIM('a)}"
   905   unfolding e2p_def by auto
   906 
   907 lemma e2p_image_vimage: fixes A::"'a::ordered_euclidean_space set"
   908   shows "e2p ` A = p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   909 proof(rule set_eqI,rule)
   910   fix x assume "x \<in> e2p ` A" then guess y unfolding image_iff .. note y=this
   911   show "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   912     apply safe apply(rule vimageI[OF _ y(1)]) unfolding y p2e_e2p by auto
   913 next fix x assume "x \<in> p2e -` A \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)})"
   914   thus "x \<in> e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto
   915 qed
   916 
   917 lemma lmeasure_measure_eq_borel_prod:
   918   fixes A :: "('a::ordered_euclidean_space) set"
   919   assumes "A \<in> sets borel"
   920   shows "lmeasure A = borel_product.product_measure {..<DIM('a)} (e2p ` A :: (nat \<Rightarrow> real) set)"
   921 proof (rule measure_unique_Int_stable[where X=A and A=cube])
   922   interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
   923   show "Int_stable \<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
   924     (is "Int_stable ?E" ) using Int_stable_cuboids' .
   925   show "borel = sigma ?E" using borel_eq_atLeastAtMost .
   926   show "\<And>i. lmeasure (cube i) \<noteq> \<omega>" unfolding lmeasure_cube by auto
   927   show "\<And>X. X \<in> sets ?E \<Longrightarrow>
   928     lmeasure X = borel_product.product_measure {..<DIM('a)} (e2p ` X :: (nat \<Rightarrow> real) set)"
   929   proof- case goal1 then obtain a b where X:"X = {a..b}" by auto
   930     { presume *:"X \<noteq> {} \<Longrightarrow> ?case"
   931       show ?case apply(cases,rule *,assumption) by auto }
   932     def XX \<equiv> "\<lambda>i. {a $$ i .. b $$ i}" assume  "X \<noteq> {}"  note X' = this[unfolded X interval_ne_empty]
   933     have *:"Pi\<^isub>E {..<DIM('a)} XX = e2p ` X" apply(rule set_eqI)
   934     proof fix x assume "x \<in> Pi\<^isub>E {..<DIM('a)} XX"
   935       thus "x \<in> e2p ` X" unfolding image_iff apply(rule_tac x="\<chi>\<chi> i. x i" in bexI)
   936         unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by rule auto
   937     next fix x assume "x \<in> e2p ` X" then guess y unfolding image_iff .. note y = this
   938       show "x \<in> Pi\<^isub>E {..<DIM('a)} XX" unfolding y using y(1)
   939         unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by auto
   940     qed
   941     have "lmeasure X = (\<Prod>x<DIM('a). Real (b $$ x - a $$ x))"  using X' apply- unfolding X
   942       unfolding lmeasure_atLeastAtMost content_closed_interval apply(subst Real_setprod) by auto
   943     also have "... = (\<Prod>i<DIM('a). lmeasure (XX i))" apply(rule setprod_cong2)
   944       unfolding XX_def lmeasure_atLeastAtMost apply(subst content_real) using X' by auto
   945     also have "... = borel_product.product_measure {..<DIM('a)} (e2p ` X)" unfolding *[THEN sym]
   946       apply(rule fprod.measure_times[THEN sym]) unfolding XX_def by auto
   947     finally show ?case .
   948   qed
   949 
   950   show "range cube \<subseteq> sets \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>"
   951     unfolding cube_def_raw by auto
   952   have "\<And>x. \<exists>xa. x \<in> cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp
   953   thus "cube \<up> space \<lparr>space = UNIV, sets = range (\<lambda>(a, b). {a..b})\<rparr>"
   954     apply-apply(rule isotoneI) apply(rule cube_subset_Suc) by auto
   955   show "A \<in> sets borel " by fact
   956   show "measure_space borel lmeasure" by default
   957   show "measure_space borel
   958      (\<lambda>a::'a set. finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` a))"
   959     apply default unfolding countably_additive_def
   960   proof safe fix A::"nat \<Rightarrow> 'a set" assume A:"range A \<subseteq> sets borel" "disjoint_family A"
   961       "(\<Union>i. A i) \<in> sets borel"
   962     note fprod.ca[unfolded countably_additive_def,rule_format]
   963     note ca = this[of "\<lambda> n. e2p ` (A n)"]
   964     show "(\<Sum>\<^isub>\<infinity>n. finite_product_sigma_finite.measure
   965         (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` A n)) =
   966            finite_product_sigma_finite.measure (\<lambda>x. borel)
   967             (\<lambda>x. lmeasure) {..<DIM('a)} (e2p ` (\<Union>i. A i))" unfolding image_UN
   968     proof(rule ca) show "range (\<lambda>n. e2p ` A n) \<subseteq> sets
   969        (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
   970         unfolding product_borel_eq_vimage
   971       proof case goal1
   972         then guess y unfolding image_iff .. note y=this(2)
   973         show ?case unfolding borel.in_vimage_algebra y apply-
   974           apply(rule_tac x="A y" in bexI,rule e2p_image_vimage)
   975           using A(1) by auto
   976       qed
   977 
   978       show "disjoint_family (\<lambda>n. e2p ` A n)" apply(rule inj_on_disjoint_family_on)
   979         using bij_euclidean_component using A(2) unfolding bij_betw_def by auto
   980       show "(\<Union>n. e2p ` A n) \<in> sets (sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)}))"
   981         unfolding product_borel_eq_vimage borel.in_vimage_algebra
   982       proof(rule bexI[OF _ A(3)],rule set_eqI,rule)
   983         fix x assume x:"x \<in> (\<Union>n. e2p ` A n)" hence "p2e x \<in> (\<Union>i. A i)" by auto
   984         moreover have "x \<in> extensional {..<DIM('a)}"
   985           using x unfolding extensional_def e2p_def_raw by auto
   986         ultimately show "x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
   987           extensional {..<DIM('a)})" by auto
   988       next fix x assume x:"x \<in> p2e -` (\<Union>i. A i) \<inter> (({..<DIM('a)} \<rightarrow> UNIV) \<inter>
   989           extensional {..<DIM('a)})"
   990         hence "p2e x \<in> (\<Union>i. A i)" by auto
   991         hence "\<exists>n. x \<in> e2p ` A n" apply safe apply(rule_tac x=i in exI)
   992           unfolding image_iff apply(rule_tac x="p2e x" in bexI)
   993           apply(subst e2p_p2e) using x by auto
   994         thus "x \<in> (\<Union>n. e2p ` A n)" by auto
   995       qed
   996     qed
   997   qed auto
   998 qed
   999 
  1000 lemma e2p_p2e'[simp]: fixes x::"'a::ordered_euclidean_space"
  1001   assumes "A \<subseteq> extensional {..<DIM('a)}"
  1002   shows "e2p ` (p2e ` A ::'a set) = A"
  1003   apply(rule set_eqI) unfolding image_iff Bex_def apply safe defer
  1004   apply(rule_tac x="p2e x" in exI,safe) using assms by auto
  1005 
  1006 lemma range_p2e:"range (p2e::_\<Rightarrow>'a::ordered_euclidean_space) = UNIV"
  1007   apply safe defer unfolding image_iff apply(rule_tac x="\<lambda>i. x $$ i" in bexI)
  1008   unfolding p2e_def by auto
  1009 
  1010 lemma p2e_inv_extensional:"(A::'a::ordered_euclidean_space set)
  1011   = p2e ` (p2e -` A \<inter> extensional {..<DIM('a)})"
  1012   unfolding p2e_def_raw apply safe unfolding image_iff
  1013 proof- fix x assume "x\<in>A"
  1014   let ?y = "\<lambda>i. if i<DIM('a) then x$$i else undefined"
  1015   have *:"Chi ?y = x" apply(subst euclidean_eq) by auto
  1016   show "\<exists>xa\<in>Chi -` A \<inter> extensional {..<DIM('a)}. x = Chi xa" apply(rule_tac x="?y" in bexI)
  1017     apply(subst euclidean_eq) unfolding extensional_def using `x\<in>A` by(auto simp: *)
  1018 qed
  1019 
  1020 lemma borel_fubini_positiv_integral:
  1021   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> pinfreal"
  1022   assumes f: "f \<in> borel_measurable borel"
  1023   shows "borel.positive_integral f =
  1024           borel_product.product_positive_integral {..<DIM('a)} (f \<circ> p2e)"
  1025 proof- def U \<equiv> "(({..<DIM('a)} \<rightarrow> UNIV) \<inter> extensional {..<DIM('a)}):: (nat \<Rightarrow> real) set"
  1026   interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
  1027   have "\<And>x. \<exists>i::nat. x < real i" by (metis real_arch_lt)
  1028   hence "(\<lambda>n::nat. {..<real n}) \<up> UNIV" apply-apply(rule isotoneI) by auto
  1029   hence *:"sigma_algebra.vimage_algebra borel U (p2e:: _ \<Rightarrow> 'a)
  1030     = sigma (product_algebra (\<lambda>x. borel) {..<DIM('a)})"
  1031     unfolding U_def apply-apply(subst borel_vimage_algebra_eq)
  1032     apply(subst sigma_product_algebra_sigma_eq[where S="\<lambda>x. \<lambda>n. {..<(\<chi>\<chi> i. real n)}", THEN sym])
  1033     unfolding borel_eq_lessThan[THEN sym] by auto
  1034   show ?thesis unfolding borel.positive_integral_vimage[unfolded space_borel,OF bij_p2e]
  1035     apply(subst fprod.positive_integral_cong_measure[THEN sym, of "\<lambda>A. lmeasure (p2e ` A)"])
  1036     unfolding U_def[symmetric] *[THEN sym] o_def
  1037   proof- fix A assume A:"A \<in> sets (sigma_algebra.vimage_algebra borel U (p2e ::_ \<Rightarrow> 'a))"
  1038     hence *:"A \<subseteq> extensional {..<DIM('a)}" unfolding U_def by auto
  1039     from A guess B unfolding borel.in_vimage_algebra U_def .. note B=this
  1040     have "(p2e ` A::'a set) \<in> sets borel" unfolding B apply(subst Int_left_commute)
  1041       apply(subst Int_absorb1) unfolding p2e_inv_extensional[of B,THEN sym] using B(1) by auto
  1042     from lmeasure_measure_eq_borel_prod[OF this] show "lmeasure (p2e ` A::'a set) =
  1043       finite_product_sigma_finite.measure (\<lambda>x. borel) (\<lambda>x. lmeasure) {..<DIM('a)} A"
  1044       unfolding e2p_p2e'[OF *] .
  1045   qed auto
  1046 qed
  1047 
  1048 lemma borel_fubini:
  1049   fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
  1050   assumes f: "f \<in> borel_measurable borel"
  1051   shows "borel.integral f = borel_product.product_integral {..<DIM('a)} (f \<circ> p2e)"
  1052 proof- interpret fprod: finite_product_sigma_finite "\<lambda>x. borel" "\<lambda>x. lmeasure" "{..<DIM('a)}" by default auto
  1053   have 1:"(\<lambda>x. Real (f x)) \<in> borel_measurable borel" using f by auto
  1054   have 2:"(\<lambda>x. Real (- f x)) \<in> borel_measurable borel" using f by auto
  1055   show ?thesis unfolding fprod.integral_def borel.integral_def
  1056     unfolding borel_fubini_positiv_integral[OF 1] borel_fubini_positiv_integral[OF 2]
  1057     unfolding o_def ..
  1058 qed
  1059 
  1060 end