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