src/HOL/Probability/Lebesgue.thy
author hoelzl
Thu Mar 04 21:52:26 2010 +0100 (2010-03-04)
changeset 35582 b16d99a72dc9
child 35692 f1315bbf1bc9
permissions -rw-r--r--
Add Lebesgue integral and probability space.
hoelzl@35582
     1
header {*Lebesgue Integration*}
hoelzl@35582
     2
hoelzl@35582
     3
theory Lebesgue
hoelzl@35582
     4
imports Measure Borel
hoelzl@35582
     5
begin
hoelzl@35582
     6
hoelzl@35582
     7
text{*From the HOL4 Hurd/Coble Lebesgue integration, translated by Armin Heller and Johannes Hoelzl.*}
hoelzl@35582
     8
hoelzl@35582
     9
definition
hoelzl@35582
    10
  "pos_part f = (\<lambda>x. max 0 (f x))"
hoelzl@35582
    11
hoelzl@35582
    12
definition
hoelzl@35582
    13
  "neg_part f = (\<lambda>x. - min 0 (f x))"
hoelzl@35582
    14
hoelzl@35582
    15
definition
hoelzl@35582
    16
  "nonneg f = (\<forall>x. 0 \<le> f x)"
hoelzl@35582
    17
hoelzl@35582
    18
lemma nonneg_pos_part[intro!]:
hoelzl@35582
    19
  fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,zero}"
hoelzl@35582
    20
  shows "nonneg (pos_part f)"
hoelzl@35582
    21
  unfolding nonneg_def pos_part_def by auto
hoelzl@35582
    22
hoelzl@35582
    23
lemma nonneg_neg_part[intro!]:
hoelzl@35582
    24
  fixes f :: "'c \<Rightarrow> 'd\<Colon>{linorder,ordered_ab_group_add}"
hoelzl@35582
    25
  shows "nonneg (neg_part f)"
hoelzl@35582
    26
  unfolding nonneg_def neg_part_def min_def by auto
hoelzl@35582
    27
hoelzl@35582
    28
context measure_space
hoelzl@35582
    29
begin
hoelzl@35582
    30
hoelzl@35582
    31
definition
hoelzl@35582
    32
 "pos_simple f =
hoelzl@35582
    33
  { (s :: nat set, a, x).
hoelzl@35582
    34
    finite s \<and> nonneg f \<and> nonneg x \<and> a ` s \<subseteq> sets M \<and>
hoelzl@35582
    35
    (\<forall>t \<in> space M. (\<exists>!i\<in>s. t\<in>a i) \<and> (\<forall>i\<in>s. t \<in> a i \<longrightarrow> f t = x i)) }"
hoelzl@35582
    36
hoelzl@35582
    37
definition
hoelzl@35582
    38
  "pos_simple_integral \<equiv> \<lambda>(s, a, x). \<Sum> i \<in> s. x i * measure M (a i)"
hoelzl@35582
    39
hoelzl@35582
    40
definition
hoelzl@35582
    41
  "psfis f = pos_simple_integral ` (pos_simple f)"
hoelzl@35582
    42
hoelzl@35582
    43
definition
hoelzl@35582
    44
  "nnfis f = { y. \<exists>u x. mono_convergent u f (space M) \<and>
hoelzl@35582
    45
                        (\<forall>n. x n \<in> psfis (u n)) \<and> x ----> y }"
hoelzl@35582
    46
hoelzl@35582
    47
definition
hoelzl@35582
    48
  "integrable f \<longleftrightarrow> (\<exists>x. x \<in> nnfis (pos_part f)) \<and> (\<exists>y. y \<in> nnfis (neg_part f))"
hoelzl@35582
    49
hoelzl@35582
    50
definition
hoelzl@35582
    51
  "integral f = (THE i :: real. i \<in> nnfis (pos_part f)) - (THE j. j \<in> nnfis (neg_part f))"
hoelzl@35582
    52
hoelzl@35582
    53
definition
hoelzl@35582
    54
  "enumerate s \<equiv> SOME f. bij_betw f UNIV s"
hoelzl@35582
    55
hoelzl@35582
    56
definition
hoelzl@35582
    57
  "countable_space_integral f \<equiv>
hoelzl@35582
    58
    let e = enumerate (f ` space M) in
hoelzl@35582
    59
      suminf (\<lambda>r. e r * measure M (f -` {e r} \<inter> space M))"
hoelzl@35582
    60
hoelzl@35582
    61
definition
hoelzl@35582
    62
  "RN_deriv v \<equiv> SOME f. measure_space (M\<lparr>measure := v\<rparr>) \<and>
hoelzl@35582
    63
    f \<in> borel_measurable M \<and>
hoelzl@35582
    64
    (\<forall>a \<in> sets M. (integral (\<lambda>x. f x * indicator_fn a x) = v a))"
hoelzl@35582
    65
hoelzl@35582
    66
lemma pos_simpleE[consumes 1]:
hoelzl@35582
    67
  assumes ps: "(s, a, x) \<in> pos_simple f"
hoelzl@35582
    68
  obtains "finite s" and "nonneg f" and "nonneg x"
hoelzl@35582
    69
    and "a ` s \<subseteq> sets M" and "(\<Union>i\<in>s. a i) = space M"
hoelzl@35582
    70
    and "disjoint_family_on a s"
hoelzl@35582
    71
    and "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
hoelzl@35582
    72
    and "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
hoelzl@35582
    73
proof
hoelzl@35582
    74
  show "finite s" and "nonneg f" and "nonneg x"
hoelzl@35582
    75
    and as_in_M: "a ` s \<subseteq> sets M"
hoelzl@35582
    76
    and *: "\<And>t. t \<in> space M \<Longrightarrow> (\<exists>!i. i \<in> s \<and> t \<in> a i)"
hoelzl@35582
    77
    and **: "\<And>t i. \<lbrakk> t \<in> space M ; i \<in> s ; t \<in> a i \<rbrakk> \<Longrightarrow> f t = x i"
hoelzl@35582
    78
    using ps unfolding pos_simple_def by auto
hoelzl@35582
    79
hoelzl@35582
    80
  thus t: "(\<Union>i\<in>s. a i) = space M"
hoelzl@35582
    81
  proof safe
hoelzl@35582
    82
    fix x assume "x \<in> space M"
hoelzl@35582
    83
    from *[OF this] show "x \<in> (\<Union>i\<in>s. a i)" by auto
hoelzl@35582
    84
  next
hoelzl@35582
    85
    fix t i assume "i \<in> s"
hoelzl@35582
    86
    hence "a i \<in> sets M" using as_in_M by auto
hoelzl@35582
    87
    moreover assume "t \<in> a i"
hoelzl@35582
    88
    ultimately show "t \<in> space M" using sets_into_space by blast
hoelzl@35582
    89
  qed
hoelzl@35582
    90
hoelzl@35582
    91
  show "disjoint_family_on a s" unfolding disjoint_family_on_def
hoelzl@35582
    92
  proof safe
hoelzl@35582
    93
    fix i j and t assume "i \<in> s" "t \<in> a i" and "j \<in> s" "t \<in> a j" and "i \<noteq> j"
hoelzl@35582
    94
    with t * show "t \<in> {}" by auto
hoelzl@35582
    95
  qed
hoelzl@35582
    96
qed
hoelzl@35582
    97
hoelzl@35582
    98
lemma pos_simple_cong:
hoelzl@35582
    99
  assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
hoelzl@35582
   100
  shows "pos_simple f = pos_simple g"
hoelzl@35582
   101
  unfolding pos_simple_def using assms by auto
hoelzl@35582
   102
hoelzl@35582
   103
lemma psfis_cong:
hoelzl@35582
   104
  assumes "nonneg f" and "nonneg g" and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
hoelzl@35582
   105
  shows "psfis f = psfis g"
hoelzl@35582
   106
  unfolding psfis_def using pos_simple_cong[OF assms] by simp
hoelzl@35582
   107
hoelzl@35582
   108
lemma pos_simple_setsum_indicator_fn:
hoelzl@35582
   109
  assumes ps: "(s, a, x) \<in> pos_simple f"
hoelzl@35582
   110
  and "t \<in> space M"
hoelzl@35582
   111
  shows "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) = f t"
hoelzl@35582
   112
proof -
hoelzl@35582
   113
  from assms obtain i where *: "i \<in> s" "t \<in> a i"
hoelzl@35582
   114
    and "finite s" and xi: "x i = f t" by (auto elim!: pos_simpleE)
hoelzl@35582
   115
hoelzl@35582
   116
  have **: "(\<Sum>i\<in>s. x i * indicator_fn (a i) t) =
hoelzl@35582
   117
    (\<Sum>j\<in>s. if j \<in> {i} then x i else 0)"
hoelzl@35582
   118
    unfolding indicator_fn_def using assms *
hoelzl@35582
   119
    by (auto intro!: setsum_cong elim!: pos_simpleE)
hoelzl@35582
   120
  show ?thesis unfolding ** setsum_cases[OF `finite s`] xi
hoelzl@35582
   121
    using `i \<in> s` by simp
hoelzl@35582
   122
qed
hoelzl@35582
   123
hoelzl@35582
   124
lemma (in measure_space) measure_setsum_split:
hoelzl@35582
   125
  assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
hoelzl@35582
   126
  assumes "(\<Union>i \<in> r. b i) = space M"
hoelzl@35582
   127
  assumes "disjoint_family_on b r"
hoelzl@35582
   128
  shows "(measure M) a = (\<Sum> i \<in> r. measure M (a \<inter> (b i)))"
hoelzl@35582
   129
proof -
hoelzl@35582
   130
  have *: "measure M a = measure M (\<Union>i \<in> r. a \<inter> b i)"
hoelzl@35582
   131
    using assms by auto
hoelzl@35582
   132
  show ?thesis unfolding *
hoelzl@35582
   133
  proof (rule measure_finitely_additive''[symmetric])
hoelzl@35582
   134
    show "finite r" using `finite r` by auto
hoelzl@35582
   135
    { fix i assume "i \<in> r"
hoelzl@35582
   136
      hence "b i \<in> sets M" using br_in_M by auto
hoelzl@35582
   137
      thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
hoelzl@35582
   138
    }
hoelzl@35582
   139
    show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
hoelzl@35582
   140
      using `disjoint_family_on b r`
hoelzl@35582
   141
      unfolding disjoint_family_on_def by auto
hoelzl@35582
   142
  qed
hoelzl@35582
   143
qed
hoelzl@35582
   144
hoelzl@35582
   145
lemma (in measure_space) pos_simple_common_partition:
hoelzl@35582
   146
  assumes psf: "(s, a, x) \<in> pos_simple f"
hoelzl@35582
   147
  assumes psg: "(s', b, y) \<in> pos_simple g"
hoelzl@35582
   148
  obtains z z' c k where "(k, c, z) \<in> pos_simple f" "(k, c, z') \<in> pos_simple g"
hoelzl@35582
   149
proof -
hoelzl@35582
   150
  (* definitions *)
hoelzl@35582
   151
hoelzl@35582
   152
  def k == "{0 ..< card (s \<times> s')}"
hoelzl@35582
   153
  have fs: "finite s" "finite s'" "finite k" unfolding k_def
hoelzl@35582
   154
    using psf psg unfolding pos_simple_def by auto
hoelzl@35582
   155
  hence "finite (s \<times> s')" by simp
hoelzl@35582
   156
  then obtain p where p: "p ` k = s \<times> s'" "inj_on p k"
hoelzl@35582
   157
    using ex_bij_betw_nat_finite[of "s \<times> s'"] unfolding bij_betw_def k_def by blast
hoelzl@35582
   158
  def c == "\<lambda> i. a (fst (p i)) \<inter> b (snd (p i))"
hoelzl@35582
   159
  def z == "\<lambda> i. x (fst (p i))"
hoelzl@35582
   160
  def z' == "\<lambda> i. y (snd (p i))"
hoelzl@35582
   161
hoelzl@35582
   162
  have "finite k" unfolding k_def by simp
hoelzl@35582
   163
hoelzl@35582
   164
  have "nonneg z" and "nonneg z'"
hoelzl@35582
   165
    using psf psg unfolding z_def z'_def pos_simple_def nonneg_def by auto
hoelzl@35582
   166
hoelzl@35582
   167
  have ck_subset_M: "c ` k \<subseteq> sets M"
hoelzl@35582
   168
  proof
hoelzl@35582
   169
    fix x assume "x \<in> c ` k"
hoelzl@35582
   170
    then obtain j where "j \<in> k" and "x = c j" by auto
hoelzl@35582
   171
    hence "p j \<in> s \<times> s'" using p(1) by auto
hoelzl@35582
   172
    hence "a (fst (p j)) \<in> sets M" (is "?a \<in> _")
hoelzl@35582
   173
      and "b (snd (p j)) \<in> sets M" (is "?b \<in> _")
hoelzl@35582
   174
      using psf psg unfolding pos_simple_def by auto
hoelzl@35582
   175
    thus "x \<in> sets M" unfolding `x = c j` c_def using Int by simp
hoelzl@35582
   176
  qed
hoelzl@35582
   177
hoelzl@35582
   178
  { fix t assume "t \<in> space M"
hoelzl@35582
   179
    hence ex1s: "\<exists>!i\<in>s. t \<in> a i" and ex1s': "\<exists>!i\<in>s'. t \<in> b i"
hoelzl@35582
   180
      using psf psg unfolding pos_simple_def by auto
hoelzl@35582
   181
    then obtain j j' where j: "j \<in> s" "t \<in> a j" and j': "j' \<in> s'" "t \<in> b j'"
hoelzl@35582
   182
      by auto
hoelzl@35582
   183
    then obtain i :: nat where i: "(j,j') = p i" and "i \<in> k" using p by auto
hoelzl@35582
   184
    have "\<exists>!i\<in>k. t \<in> c i"
hoelzl@35582
   185
    proof (rule ex1I[of _ i])
hoelzl@35582
   186
      show "\<And>x. x \<in> k \<Longrightarrow> t \<in> c x \<Longrightarrow> x = i"
hoelzl@35582
   187
      proof -
hoelzl@35582
   188
        fix l assume "l \<in> k" "t \<in> c l"
hoelzl@35582
   189
        hence "p l \<in> s \<times> s'" and t_in: "t \<in> a (fst (p l))" "t \<in> b (snd (p l))"
hoelzl@35582
   190
          using p unfolding c_def by auto
hoelzl@35582
   191
        hence "fst (p l) \<in> s" and "snd (p l) \<in> s'" by auto
hoelzl@35582
   192
        with t_in j j' ex1s ex1s' have "p l = (j, j')" by (cases "p l", auto)
hoelzl@35582
   193
        thus "l = i"
hoelzl@35582
   194
          using `(j, j') = p i` p(2)[THEN inj_onD] `l \<in> k` `i \<in> k` by auto
hoelzl@35582
   195
      qed
hoelzl@35582
   196
hoelzl@35582
   197
      show "i \<in> k \<and> t \<in> c i"
hoelzl@35582
   198
        using `i \<in> k` `t \<in> a j` `t \<in> b j'` c_def i[symmetric] by auto
hoelzl@35582
   199
    qed auto
hoelzl@35582
   200
  } note ex1 = this
hoelzl@35582
   201
hoelzl@35582
   202
  show thesis
hoelzl@35582
   203
  proof (rule that)
hoelzl@35582
   204
    { fix t i assume "t \<in> space M" and "i \<in> k"
hoelzl@35582
   205
      hence "p i \<in> s \<times> s'" using p(1) by auto
hoelzl@35582
   206
      hence "fst (p i) \<in> s" by auto
hoelzl@35582
   207
      moreover
hoelzl@35582
   208
      assume "t \<in> c i"
hoelzl@35582
   209
      hence "t \<in> a (fst (p i))" unfolding c_def by auto
hoelzl@35582
   210
      ultimately have "f t = z i" using psf `t \<in> space M`
hoelzl@35582
   211
        unfolding z_def pos_simple_def by auto
hoelzl@35582
   212
    }
hoelzl@35582
   213
    thus "(k, c, z) \<in> pos_simple f"
hoelzl@35582
   214
      using psf `finite k` `nonneg z` ck_subset_M ex1
hoelzl@35582
   215
      unfolding pos_simple_def by auto
hoelzl@35582
   216
hoelzl@35582
   217
    { fix t i assume "t \<in> space M" and "i \<in> k"
hoelzl@35582
   218
      hence "p i \<in> s \<times> s'" using p(1) by auto
hoelzl@35582
   219
      hence "snd (p i) \<in> s'" by auto
hoelzl@35582
   220
      moreover
hoelzl@35582
   221
      assume "t \<in> c i"
hoelzl@35582
   222
      hence "t \<in> b (snd (p i))" unfolding c_def by auto
hoelzl@35582
   223
      ultimately have "g t = z' i" using psg `t \<in> space M`
hoelzl@35582
   224
        unfolding z'_def pos_simple_def by auto
hoelzl@35582
   225
    }
hoelzl@35582
   226
    thus "(k, c, z') \<in> pos_simple g"
hoelzl@35582
   227
      using psg `finite k` `nonneg z'` ck_subset_M ex1
hoelzl@35582
   228
      unfolding pos_simple_def by auto
hoelzl@35582
   229
  qed
hoelzl@35582
   230
qed
hoelzl@35582
   231
hoelzl@35582
   232
lemma (in measure_space) pos_simple_integral_equal:
hoelzl@35582
   233
  assumes psx: "(s, a, x) \<in> pos_simple f"
hoelzl@35582
   234
  assumes psy: "(s', b, y) \<in> pos_simple f"
hoelzl@35582
   235
  shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
hoelzl@35582
   236
  unfolding pos_simple_integral_def
hoelzl@35582
   237
proof simp
hoelzl@35582
   238
  have "(\<Sum>i\<in>s. x i * measure M (a i)) =
hoelzl@35582
   239
    (\<Sum>i\<in>s. (\<Sum>j \<in> s'. x i * measure M (a i \<inter> b j)))" (is "?left = _")
hoelzl@35582
   240
    using psy psx unfolding setsum_right_distrib[symmetric]
hoelzl@35582
   241
    by (auto intro!: setsum_cong measure_setsum_split elim!: pos_simpleE)
hoelzl@35582
   242
  also have "... = (\<Sum>i\<in>s. (\<Sum>j \<in> s'. y j * measure M (a i \<inter> b j)))"
hoelzl@35582
   243
  proof (rule setsum_cong, simp, rule setsum_cong, simp_all)
hoelzl@35582
   244
    fix i j assume i: "i \<in> s" and j: "j \<in> s'"
hoelzl@35582
   245
    hence "a i \<in> sets M" using psx by (auto elim!: pos_simpleE)
hoelzl@35582
   246
hoelzl@35582
   247
    show "measure M (a i \<inter> b j) = 0 \<or> x i = y j"
hoelzl@35582
   248
    proof (cases "a i \<inter> b j = {}")
hoelzl@35582
   249
      case True thus ?thesis using empty_measure by simp
hoelzl@35582
   250
    next
hoelzl@35582
   251
      case False then obtain t where t: "t \<in> a i" "t \<in> b j" by auto
hoelzl@35582
   252
      hence "t \<in> space M" using `a i \<in> sets M` sets_into_space by auto
hoelzl@35582
   253
      with psx psy t i j have "x i = f t" and "y j = f t"
hoelzl@35582
   254
        unfolding pos_simple_def by auto
hoelzl@35582
   255
      thus ?thesis by simp
hoelzl@35582
   256
    qed
hoelzl@35582
   257
  qed
hoelzl@35582
   258
  also have "... = (\<Sum>j\<in>s'. (\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)))"
hoelzl@35582
   259
    by (subst setsum_commute) simp
hoelzl@35582
   260
  also have "... = (\<Sum>i\<in>s'. y i * measure M (b i))" (is "?sum_sum = ?right")
hoelzl@35582
   261
  proof (rule setsum_cong)
hoelzl@35582
   262
    fix j assume "j \<in> s'"
hoelzl@35582
   263
    have "y j * measure M (b j) = (\<Sum>i\<in>s. y j * measure M (b j \<inter> a i))"
hoelzl@35582
   264
      using psx psy `j \<in> s'` unfolding setsum_right_distrib[symmetric]
hoelzl@35582
   265
      by (auto intro!: measure_setsum_split elim!: pos_simpleE)
hoelzl@35582
   266
    thus "(\<Sum>i\<in>s. y j * measure M (a i \<inter> b j)) = y j * measure M (b j)"
hoelzl@35582
   267
      by (auto intro!: setsum_cong arg_cong[where f="measure M"])
hoelzl@35582
   268
  qed simp
hoelzl@35582
   269
  finally show "?left = ?right" .
hoelzl@35582
   270
qed
hoelzl@35582
   271
hoelzl@35582
   272
lemma (in measure_space)psfis_present:
hoelzl@35582
   273
  assumes "A \<in> psfis f"
hoelzl@35582
   274
  assumes "B \<in> psfis g"
hoelzl@35582
   275
  obtains z z' c k where
hoelzl@35582
   276
  "A = pos_simple_integral (k, c, z)"
hoelzl@35582
   277
  "B = pos_simple_integral (k, c, z')"
hoelzl@35582
   278
  "(k, c, z) \<in> pos_simple f"
hoelzl@35582
   279
  "(k, c, z') \<in> pos_simple g"
hoelzl@35582
   280
using assms
hoelzl@35582
   281
proof -
hoelzl@35582
   282
  from assms obtain s a x s' b y where
hoelzl@35582
   283
    ps: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g" and
hoelzl@35582
   284
    A: "A = pos_simple_integral (s, a, x)" and
hoelzl@35582
   285
    B: "B = pos_simple_integral (s', b, y)"
hoelzl@35582
   286
    unfolding psfis_def pos_simple_integral_def by auto
hoelzl@35582
   287
hoelzl@35582
   288
  guess z z' c k using pos_simple_common_partition[OF ps] . note part = this
hoelzl@35582
   289
  show thesis
hoelzl@35582
   290
  proof (rule that[of k c z z', OF _ _ part])
hoelzl@35582
   291
    show "A = pos_simple_integral (k, c, z)"
hoelzl@35582
   292
      unfolding A by (rule pos_simple_integral_equal[OF ps(1) part(1)])
hoelzl@35582
   293
    show "B = pos_simple_integral (k, c, z')"
hoelzl@35582
   294
      unfolding B by (rule pos_simple_integral_equal[OF ps(2) part(2)])
hoelzl@35582
   295
  qed
hoelzl@35582
   296
qed
hoelzl@35582
   297
hoelzl@35582
   298
lemma (in measure_space) pos_simple_integral_add:
hoelzl@35582
   299
  assumes "(s, a, x) \<in> pos_simple f"
hoelzl@35582
   300
  assumes "(s', b, y) \<in> pos_simple g"
hoelzl@35582
   301
  obtains s'' c z where
hoelzl@35582
   302
    "(s'', c, z) \<in> pos_simple (\<lambda>x. f x + g x)"
hoelzl@35582
   303
    "(pos_simple_integral (s, a, x) +
hoelzl@35582
   304
      pos_simple_integral (s', b, y) =
hoelzl@35582
   305
      pos_simple_integral (s'', c, z))"
hoelzl@35582
   306
using assms
hoelzl@35582
   307
proof -
hoelzl@35582
   308
  guess z z' c k
hoelzl@35582
   309
    by (rule pos_simple_common_partition[OF `(s, a, x) \<in> pos_simple f ` `(s', b, y) \<in> pos_simple g`])
hoelzl@35582
   310
  note kczz' = this
hoelzl@35582
   311
  have x: "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
hoelzl@35582
   312
    by (rule pos_simple_integral_equal) (fact, fact)
hoelzl@35582
   313
  have y: "pos_simple_integral (s', b, y) = pos_simple_integral (k, c, z')"
hoelzl@35582
   314
    by (rule pos_simple_integral_equal) (fact, fact)
hoelzl@35582
   315
hoelzl@35582
   316
  have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))
hoelzl@35582
   317
    = (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"
hoelzl@35582
   318
    unfolding pos_simple_integral_def by auto
hoelzl@35582
   319
  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto
hoelzl@35582
   320
  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x)) + (\<Sum> x \<in> k. z' x * measure M (c x))" using setsum_addf by auto
hoelzl@35582
   321
  also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto
hoelzl@35582
   322
  finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =
hoelzl@35582
   323
    pos_simple_integral (k, c, (\<lambda> x. z x + z' x))" using x y by auto
hoelzl@35582
   324
  show ?thesis
hoelzl@35582
   325
    apply (rule that[of k c "(\<lambda> x. z x + z' x)", OF _ ths])
hoelzl@35582
   326
    using kczz' unfolding pos_simple_def nonneg_def by (auto intro!: add_nonneg_nonneg)
hoelzl@35582
   327
qed
hoelzl@35582
   328
hoelzl@35582
   329
lemma psfis_add:
hoelzl@35582
   330
  assumes "a \<in> psfis f" "b \<in> psfis g"
hoelzl@35582
   331
  shows "a + b \<in> psfis (\<lambda>x. f x + g x)"
hoelzl@35582
   332
using assms pos_simple_integral_add
hoelzl@35582
   333
unfolding psfis_def by auto blast
hoelzl@35582
   334
hoelzl@35582
   335
lemma pos_simple_integral_mono_on_mspace:
hoelzl@35582
   336
  assumes f: "(s, a, x) \<in> pos_simple f"
hoelzl@35582
   337
  assumes g: "(s', b, y) \<in> pos_simple g"
hoelzl@35582
   338
  assumes mono: "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
hoelzl@35582
   339
  shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
hoelzl@35582
   340
using assms
hoelzl@35582
   341
proof -
hoelzl@35582
   342
  guess z z' c k by (rule pos_simple_common_partition[OF f g])
hoelzl@35582
   343
  note kczz' = this
hoelzl@35582
   344
  (* w = z and w' = z'  except where c _ = {} or undef *)
hoelzl@35582
   345
  def w == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z i"
hoelzl@35582
   346
  def w' == "\<lambda> i. if i \<notin> k \<or> c i = {} then 0 else z' i"
hoelzl@35582
   347
  { fix i
hoelzl@35582
   348
    have "w i \<le> w' i"
hoelzl@35582
   349
    proof (cases "i \<notin> k \<or> c i = {}")
hoelzl@35582
   350
      case False hence "i \<in> k" "c i \<noteq> {}" by auto
hoelzl@35582
   351
      then obtain v where v: "v \<in> c i" and "c i \<in> sets M"
hoelzl@35582
   352
        using kczz'(1) unfolding pos_simple_def by blast
hoelzl@35582
   353
      hence "v \<in> space M" using sets_into_space by blast
hoelzl@35582
   354
      with mono[OF `v \<in> space M`] kczz' `i \<in> k` `v \<in> c i`
hoelzl@35582
   355
      have "z i \<le> z' i" unfolding pos_simple_def by simp
hoelzl@35582
   356
      thus ?thesis unfolding w_def w'_def using False by auto
hoelzl@35582
   357
    next
hoelzl@35582
   358
      case True thus ?thesis unfolding w_def w'_def by auto
hoelzl@35582
   359
   qed
hoelzl@35582
   360
  } note w_mn = this
hoelzl@35582
   361
hoelzl@35582
   362
  (* some technical stuff for the calculation*)
hoelzl@35582
   363
  have "\<And> i. i \<in> k \<Longrightarrow> c i \<in> sets M" using kczz' unfolding pos_simple_def by auto
hoelzl@35582
   364
  hence "\<And> i. i \<in> k \<Longrightarrow> measure M (c i) \<ge> 0" using positive by auto
hoelzl@35582
   365
  hence w_mono: "\<And> i. i \<in> k \<Longrightarrow> w i * measure M (c i) \<le> w' i * measure M (c i)"
hoelzl@35582
   366
    using mult_right_mono w_mn by blast
hoelzl@35582
   367
hoelzl@35582
   368
  { fix i have "\<lbrakk>i \<in> k ; z i \<noteq> w i\<rbrakk> \<Longrightarrow> measure M (c i) = 0"
hoelzl@35582
   369
      unfolding w_def by (cases "c i = {}") auto }
hoelzl@35582
   370
  hence zw: "\<And> i. i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)" by auto
hoelzl@35582
   371
hoelzl@35582
   372
  { fix i have "i \<in> k \<Longrightarrow> z i * measure M (c i) = w i * measure M (c i)"
hoelzl@35582
   373
      unfolding w_def by (cases "c i = {}") simp_all }
hoelzl@35582
   374
  note zw = this
hoelzl@35582
   375
hoelzl@35582
   376
  { fix i have "i \<in> k \<Longrightarrow> z' i * measure M (c i) = w' i * measure M (c i)"
hoelzl@35582
   377
      unfolding w'_def by (cases "c i = {}") simp_all }
hoelzl@35582
   378
  note z'w' = this
hoelzl@35582
   379
hoelzl@35582
   380
  (* the calculation *)
hoelzl@35582
   381
  have "pos_simple_integral (s, a, x) = pos_simple_integral (k, c, z)"
hoelzl@35582
   382
    using f kczz'(1) by (rule pos_simple_integral_equal)
hoelzl@35582
   383
  also have "\<dots> = (\<Sum> i \<in> k. z i * measure M (c i))"
hoelzl@35582
   384
    unfolding pos_simple_integral_def by auto
hoelzl@35582
   385
  also have "\<dots> = (\<Sum> i \<in> k. w i * measure M (c i))"
hoelzl@35582
   386
    using setsum_cong2[of k, OF zw] by auto
hoelzl@35582
   387
  also have "\<dots> \<le> (\<Sum> i \<in> k. w' i * measure M (c i))"
hoelzl@35582
   388
    using setsum_mono[OF w_mono, of k] by auto
hoelzl@35582
   389
  also have "\<dots> = (\<Sum> i \<in> k. z' i * measure M (c i))"
hoelzl@35582
   390
    using setsum_cong2[of k, OF z'w'] by auto
hoelzl@35582
   391
  also have "\<dots> = pos_simple_integral (k, c, z')"
hoelzl@35582
   392
    unfolding pos_simple_integral_def by auto
hoelzl@35582
   393
  also have "\<dots> = pos_simple_integral (s', b, y)"
hoelzl@35582
   394
    using kczz'(2) g by (rule pos_simple_integral_equal)
hoelzl@35582
   395
  finally show "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
hoelzl@35582
   396
    by simp
hoelzl@35582
   397
qed
hoelzl@35582
   398
hoelzl@35582
   399
lemma pos_simple_integral_mono:
hoelzl@35582
   400
  assumes a: "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple g"
hoelzl@35582
   401
  assumes "\<And> z. f z \<le> g z"
hoelzl@35582
   402
  shows "pos_simple_integral (s, a, x) \<le> pos_simple_integral (s', b, y)"
hoelzl@35582
   403
using assms pos_simple_integral_mono_on_mspace by auto
hoelzl@35582
   404
hoelzl@35582
   405
lemma psfis_mono:
hoelzl@35582
   406
  assumes "a \<in> psfis f" "b \<in> psfis g"
hoelzl@35582
   407
  assumes "\<And> x. x \<in> space M \<Longrightarrow> f x \<le> g x"
hoelzl@35582
   408
  shows "a \<le> b"
hoelzl@35582
   409
using assms pos_simple_integral_mono_on_mspace unfolding psfis_def by auto
hoelzl@35582
   410
hoelzl@35582
   411
lemma pos_simple_fn_integral_unique:
hoelzl@35582
   412
  assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"
hoelzl@35582
   413
  shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
hoelzl@35582
   414
using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis
hoelzl@35582
   415
hoelzl@35582
   416
lemma psfis_unique:
hoelzl@35582
   417
  assumes "a \<in> psfis f" "b \<in> psfis f"
hoelzl@35582
   418
  shows "a = b"
hoelzl@35582
   419
using assms real_le_antisym real_le_refl psfis_mono by metis
hoelzl@35582
   420
hoelzl@35582
   421
lemma pos_simple_integral_indicator:
hoelzl@35582
   422
  assumes "A \<in> sets M"
hoelzl@35582
   423
  obtains s a x where
hoelzl@35582
   424
  "(s, a, x) \<in> pos_simple (indicator_fn A)"
hoelzl@35582
   425
  "measure M A = pos_simple_integral (s, a, x)"
hoelzl@35582
   426
using assms
hoelzl@35582
   427
proof -
hoelzl@35582
   428
  def s == "{0, 1} :: nat set"
hoelzl@35582
   429
  def a == "\<lambda> i :: nat. if i = 0 then A else space M - A"
hoelzl@35582
   430
  def x == "\<lambda> i :: nat. if i = 0 then 1 else (0 :: real)"
hoelzl@35582
   431
  have eq: "pos_simple_integral (s, a, x) = measure M A"
hoelzl@35582
   432
    unfolding s_def a_def x_def pos_simple_integral_def by auto
hoelzl@35582
   433
  have "(s, a, x) \<in> pos_simple (indicator_fn A)"
hoelzl@35582
   434
    unfolding pos_simple_def indicator_fn_def s_def a_def x_def nonneg_def
hoelzl@35582
   435
    using assms sets_into_space by auto
hoelzl@35582
   436
   from that[OF this] eq show thesis by auto
hoelzl@35582
   437
qed
hoelzl@35582
   438
hoelzl@35582
   439
lemma psfis_indicator:
hoelzl@35582
   440
  assumes "A \<in> sets M"
hoelzl@35582
   441
  shows "measure M A \<in> psfis (indicator_fn A)"
hoelzl@35582
   442
using pos_simple_integral_indicator[OF assms]
hoelzl@35582
   443
  unfolding psfis_def image_def by auto
hoelzl@35582
   444
hoelzl@35582
   445
lemma pos_simple_integral_mult:
hoelzl@35582
   446
  assumes f: "(s, a, x) \<in> pos_simple f"
hoelzl@35582
   447
  assumes "0 \<le> z"
hoelzl@35582
   448
  obtains s' b y where
hoelzl@35582
   449
  "(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
hoelzl@35582
   450
  "pos_simple_integral (s', b, y) = z * pos_simple_integral (s, a, x)"
hoelzl@35582
   451
  using assms that[of s a "\<lambda>i. z * x i"]
hoelzl@35582
   452
  by (simp add: pos_simple_def pos_simple_integral_def setsum_right_distrib algebra_simps nonneg_def mult_nonneg_nonneg)
hoelzl@35582
   453
hoelzl@35582
   454
lemma psfis_mult:
hoelzl@35582
   455
  assumes "r \<in> psfis f"
hoelzl@35582
   456
  assumes "0 \<le> z"
hoelzl@35582
   457
  shows "z * r \<in> psfis (\<lambda>x. z * f x)"
hoelzl@35582
   458
using assms
hoelzl@35582
   459
proof -
hoelzl@35582
   460
  from assms obtain s a x
hoelzl@35582
   461
    where sax: "(s, a, x) \<in> pos_simple f"
hoelzl@35582
   462
    and r: "r = pos_simple_integral (s, a, x)"
hoelzl@35582
   463
    unfolding psfis_def image_def by auto
hoelzl@35582
   464
  obtain s' b y where
hoelzl@35582
   465
    "(s', b, y) \<in> pos_simple (\<lambda>x. z * f x)"
hoelzl@35582
   466
    "z * pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
hoelzl@35582
   467
    using pos_simple_integral_mult[OF sax `0 \<le> z`, of thesis] by auto
hoelzl@35582
   468
  thus ?thesis using r unfolding psfis_def image_def by auto
hoelzl@35582
   469
qed
hoelzl@35582
   470
hoelzl@35582
   471
lemma pos_simple_integral_setsum_image:
hoelzl@35582
   472
  assumes "finite P"
hoelzl@35582
   473
  assumes "\<And> i. i \<in> P \<Longrightarrow> (s i, a i, x i) \<in> pos_simple (f i)"
hoelzl@35582
   474
  obtains s' a' x' where
hoelzl@35582
   475
  "(s', a', x') \<in> pos_simple (\<lambda>t. (\<Sum> i \<in> P. f i t))"
hoelzl@35582
   476
  "pos_simple_integral (s', a', x') = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))"
hoelzl@35582
   477
using assms that
hoelzl@35582
   478
proof (induct P arbitrary:thesis rule:finite.induct)
hoelzl@35582
   479
  case emptyI note asms = this
hoelzl@35582
   480
  def s' == "{0 :: nat}"
hoelzl@35582
   481
  def a' == "\<lambda> x. if x = (0 :: nat) then space M else {}"
hoelzl@35582
   482
  def x' == "\<lambda> x :: nat. (0 :: real)"
hoelzl@35582
   483
  have "(s', a', x') \<in> pos_simple (\<lambda> t. 0)"
hoelzl@35582
   484
    unfolding s'_def a'_def x'_def pos_simple_def nonneg_def by auto
hoelzl@35582
   485
  moreover have "pos_simple_integral (s', a', x') = 0"
hoelzl@35582
   486
    unfolding s'_def a'_def x'_def pos_simple_integral_def by auto
hoelzl@35582
   487
  ultimately show ?case using asms by auto
hoelzl@35582
   488
next
hoelzl@35582
   489
hoelzl@35582
   490
  case (insertI P c) note asms = this
hoelzl@35582
   491
  then obtain s' a' x' where
hoelzl@35582
   492
    sax: "(s', a', x') \<in> pos_simple (\<lambda>t. \<Sum>i\<in>P. f i t)"
hoelzl@35582
   493
         "pos_simple_integral (s', a', x') =
hoelzl@35582
   494
             (\<Sum>i\<in>P. pos_simple_integral (s i, a i, x i))"
hoelzl@35582
   495
    by auto
hoelzl@35582
   496
hoelzl@35582
   497
  { assume "c \<in> P"
hoelzl@35582
   498
    hence "P = insert c P" by auto
hoelzl@35582
   499
    hence thesis using asms sax by auto
hoelzl@35582
   500
  }
hoelzl@35582
   501
  moreover
hoelzl@35582
   502
  { assume "c \<notin> P"
hoelzl@35582
   503
    from asms obtain s'' a'' x'' where
hoelzl@35582
   504
      sax': "s'' = s c" "a'' = a c" "x'' = x c"
hoelzl@35582
   505
            "(s'', a'', x'') \<in> pos_simple (f c)" by auto
hoelzl@35582
   506
    from sax sax' obtain k :: "nat \<Rightarrow> bool" and b :: "nat \<Rightarrow> 'a \<Rightarrow> bool" and z :: "nat \<Rightarrow> real" where
hoelzl@35582
   507
      tybbie:
hoelzl@35582
   508
      "(k, b, z) \<in> pos_simple (\<lambda>t. ((\<Sum>i\<in>P. f i t) + f c t))"
hoelzl@35582
   509
      "(pos_simple_integral (s', a', x') +
hoelzl@35582
   510
      pos_simple_integral (s'', a'', x'') =
hoelzl@35582
   511
      pos_simple_integral (k, b, z))"
hoelzl@35582
   512
      using pos_simple_integral_add by blast
hoelzl@35582
   513
hoelzl@35582
   514
    from tybbie have
hoelzl@35582
   515
      "pos_simple_integral (k, b, z) =
hoelzl@35582
   516
      pos_simple_integral (s', a', x') +
hoelzl@35582
   517
      pos_simple_integral (s'', a'', x'')" by simp
hoelzl@35582
   518
    also have "\<dots> = (\<Sum> i \<in> P. pos_simple_integral (s i, a i, x i))
hoelzl@35582
   519
                  + pos_simple_integral (s c, a c, x c)"
hoelzl@35582
   520
      using sax sax' by auto
hoelzl@35582
   521
    also have "\<dots> = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
hoelzl@35582
   522
      using asms `c \<notin> P` by auto
hoelzl@35582
   523
    finally have A: "pos_simple_integral (k, b, z) = (\<Sum> i \<in> insert c P. pos_simple_integral (s i, a i, x i))"
hoelzl@35582
   524
      by simp
hoelzl@35582
   525
hoelzl@35582
   526
    have "\<And> t. (\<Sum> i \<in> P. f i t) + f c t = (\<Sum> i \<in> insert c P. f i t)"
hoelzl@35582
   527
      using `c \<notin> P` `finite P` by auto
hoelzl@35582
   528
    hence B: "(k, b, z) \<in> pos_simple (\<lambda> t. (\<Sum> i \<in> insert c P. f i t))"
hoelzl@35582
   529
      using tybbie by simp
hoelzl@35582
   530
hoelzl@35582
   531
    from A B have thesis using asms by auto
hoelzl@35582
   532
    } ultimately show thesis by blast
hoelzl@35582
   533
qed
hoelzl@35582
   534
hoelzl@35582
   535
lemma psfis_setsum_image:
hoelzl@35582
   536
  assumes "finite P"
hoelzl@35582
   537
  assumes "\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)"
hoelzl@35582
   538
  shows "(setsum a P) \<in> psfis (\<lambda>t. \<Sum>i \<in> P. f i t)"
hoelzl@35582
   539
using assms
hoelzl@35582
   540
proof (induct P)
hoelzl@35582
   541
  case empty
hoelzl@35582
   542
  let ?s = "{0 :: nat}"
hoelzl@35582
   543
  let ?a = "\<lambda> i. if i = (0 :: nat) then space M else {}"
hoelzl@35582
   544
  let ?x = "\<lambda> (i :: nat). (0 :: real)"
hoelzl@35582
   545
  have "(?s, ?a, ?x) \<in> pos_simple (\<lambda> t. (0 :: real))"
hoelzl@35582
   546
    unfolding pos_simple_def image_def nonneg_def by auto
hoelzl@35582
   547
  moreover have "(\<Sum> i \<in> ?s. ?x i * measure M (?a i)) = 0" by auto
hoelzl@35582
   548
  ultimately have "0 \<in> psfis (\<lambda> t. 0)"
hoelzl@35582
   549
    unfolding psfis_def image_def pos_simple_integral_def nonneg_def
hoelzl@35582
   550
    by (auto intro!:bexI[of _ "(?s, ?a, ?x)"])
hoelzl@35582
   551
  thus ?case by auto
hoelzl@35582
   552
next
hoelzl@35582
   553
  case (insert x P) note asms = this
hoelzl@35582
   554
  have "finite P" by fact
hoelzl@35582
   555
  have "x \<notin> P" by fact
hoelzl@35582
   556
  have "(\<And>i. i \<in> P \<Longrightarrow> a i \<in> psfis (f i)) \<Longrightarrow>
hoelzl@35582
   557
    setsum a P \<in> psfis (\<lambda>t. \<Sum>i\<in>P. f i t)" by fact
hoelzl@35582
   558
  have "setsum a (insert x P) = a x + setsum a P" using `finite P` `x \<notin> P` by auto
hoelzl@35582
   559
  also have "\<dots> \<in> psfis (\<lambda> t. f x t + (\<Sum> i \<in> P. f i t))"
hoelzl@35582
   560
    using asms psfis_add by auto
hoelzl@35582
   561
  also have "\<dots> = psfis (\<lambda> t. \<Sum> i \<in> insert x P. f i t)"
hoelzl@35582
   562
    using `x \<notin> P` `finite P` by auto
hoelzl@35582
   563
  finally show ?case by simp
hoelzl@35582
   564
qed
hoelzl@35582
   565
hoelzl@35582
   566
lemma psfis_intro:
hoelzl@35582
   567
  assumes "a ` P \<subseteq> sets M" and "nonneg x" and "finite P"
hoelzl@35582
   568
  shows "(\<Sum>i\<in>P. x i * measure M (a i)) \<in> psfis (\<lambda>t. \<Sum>i\<in>P. x i * indicator_fn (a i) t)"
hoelzl@35582
   569
using assms psfis_mult psfis_indicator
hoelzl@35582
   570
unfolding image_def nonneg_def
hoelzl@35582
   571
by (auto intro!:psfis_setsum_image)
hoelzl@35582
   572
hoelzl@35582
   573
lemma psfis_nonneg: "a \<in> psfis f \<Longrightarrow> nonneg f"
hoelzl@35582
   574
unfolding psfis_def pos_simple_def by auto
hoelzl@35582
   575
hoelzl@35582
   576
lemma pos_psfis: "r \<in> psfis f \<Longrightarrow> 0 \<le> r"
hoelzl@35582
   577
unfolding psfis_def pos_simple_integral_def image_def pos_simple_def nonneg_def
hoelzl@35582
   578
using positive[unfolded positive_def] by (auto intro!:setsum_nonneg mult_nonneg_nonneg)
hoelzl@35582
   579
hoelzl@35582
   580
lemma pos_part_neg_part_borel_measurable:
hoelzl@35582
   581
  assumes "f \<in> borel_measurable M"
hoelzl@35582
   582
  shows "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M"
hoelzl@35582
   583
using assms
hoelzl@35582
   584
proof -
hoelzl@35582
   585
  { fix a :: real
hoelzl@35582
   586
    { assume asm: "0 \<le> a"
hoelzl@35582
   587
      from asm have pp: "\<And> w. (pos_part f w \<le> a) = (f w \<le> a)" unfolding pos_part_def by auto
hoelzl@35582
   588
      have "{w | w. w \<in> space M \<and> f w \<le> a} \<in> sets M"
hoelzl@35582
   589
        unfolding pos_part_def using assms borel_measurable_le_iff by auto
hoelzl@35582
   590
      hence "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M" using pp by auto }
hoelzl@35582
   591
    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. pos_part f w \<le> a} \<in> sets M"
hoelzl@35582
   592
      unfolding pos_part_def using empty_sets by auto
hoelzl@35582
   593
    ultimately have "{w . w \<in> space M \<and> pos_part f w \<le> a} \<in> sets M"
hoelzl@35582
   594
      using le_less_linear by auto
hoelzl@35582
   595
  } hence pos: "pos_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
hoelzl@35582
   596
  { fix a :: real
hoelzl@35582
   597
    { assume asm: "0 \<le> a"
hoelzl@35582
   598
      from asm have pp: "\<And> w. (neg_part f w \<le> a) = (f w \<ge> - a)" unfolding neg_part_def by auto
hoelzl@35582
   599
      have "{w | w. w \<in> space M \<and> f w \<ge> - a} \<in> sets M"
hoelzl@35582
   600
        unfolding neg_part_def using assms borel_measurable_ge_iff by auto
hoelzl@35582
   601
      hence "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M" using pp by auto }
hoelzl@35582
   602
    moreover have "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} = {}" unfolding neg_part_def by auto
hoelzl@35582
   603
    moreover hence "a < 0 \<Longrightarrow> {w \<in> space M. neg_part f w \<le> a} \<in> sets M" by (simp only: empty_sets)
hoelzl@35582
   604
    ultimately have "{w . w \<in> space M \<and> neg_part f w \<le> a} \<in> sets M"
hoelzl@35582
   605
      using le_less_linear by auto
hoelzl@35582
   606
  } hence neg: "neg_part f \<in> borel_measurable M" using borel_measurable_le_iff by auto
hoelzl@35582
   607
  from pos neg show "pos_part f \<in> borel_measurable M" and "neg_part f \<in> borel_measurable M" by auto
hoelzl@35582
   608
qed
hoelzl@35582
   609
hoelzl@35582
   610
lemma pos_part_neg_part_borel_measurable_iff:
hoelzl@35582
   611
  "f \<in> borel_measurable M \<longleftrightarrow>
hoelzl@35582
   612
  pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
hoelzl@35582
   613
proof -
hoelzl@35582
   614
  { fix x
hoelzl@35582
   615
    have "f x = pos_part f x - neg_part f x"
hoelzl@35582
   616
      unfolding pos_part_def neg_part_def unfolding max_def min_def
hoelzl@35582
   617
      by auto }
hoelzl@35582
   618
  hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
hoelzl@35582
   619
  hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
hoelzl@35582
   620
  from pos_part_neg_part_borel_measurable[of f]
hoelzl@35582
   621
    borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
hoelzl@35582
   622
    this
hoelzl@35582
   623
  show ?thesis by auto
hoelzl@35582
   624
qed
hoelzl@35582
   625
hoelzl@35582
   626
lemma borel_measurable_cong:
hoelzl@35582
   627
  assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w"
hoelzl@35582
   628
  shows "f \<in> borel_measurable M \<longleftrightarrow> g \<in> borel_measurable M"
hoelzl@35582
   629
using assms unfolding in_borel_measurable by (simp cong: vimage_inter_cong)
hoelzl@35582
   630
hoelzl@35582
   631
lemma psfis_borel_measurable:
hoelzl@35582
   632
  assumes "a \<in> psfis f"
hoelzl@35582
   633
  shows "f \<in> borel_measurable M"
hoelzl@35582
   634
using assms
hoelzl@35582
   635
proof -
hoelzl@35582
   636
  from assms obtain s a' x where sa'x: "(s, a', x) \<in> pos_simple f" and sa'xa: "pos_simple_integral (s, a', x) = a"
hoelzl@35582
   637
    and fs: "finite s"
hoelzl@35582
   638
    unfolding psfis_def pos_simple_integral_def image_def
hoelzl@35582
   639
    by (auto elim:pos_simpleE)
hoelzl@35582
   640
  { fix w assume "w \<in> space M"
hoelzl@35582
   641
    hence "(f w \<le> a) = ((\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
hoelzl@35582
   642
      using pos_simple_setsum_indicator_fn[OF sa'x, of w] by simp
hoelzl@35582
   643
  } hence "\<And> w. (w \<in> space M \<and> f w \<le> a) = (w \<in> space M \<and> (\<Sum> i \<in> s. x i * indicator_fn (a' i) w) \<le> a)"
hoelzl@35582
   644
    by auto
hoelzl@35582
   645
  { fix i assume "i \<in> s"
hoelzl@35582
   646
    hence "indicator_fn (a' i) \<in> borel_measurable M"
hoelzl@35582
   647
      using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto
hoelzl@35582
   648
    hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"
hoelzl@35582
   649
      using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]
hoelzl@35582
   650
        real_mult_commute by auto }
hoelzl@35582
   651
  from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable
hoelzl@35582
   652
  have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto
hoelzl@35582
   653
  from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this
hoelzl@35582
   654
  show ?thesis by simp
hoelzl@35582
   655
qed
hoelzl@35582
   656
hoelzl@35582
   657
lemma mono_conv_outgrow:
hoelzl@35582
   658
  assumes "incseq x" "x ----> y" "z < y"
hoelzl@35582
   659
  shows "\<exists>b. \<forall> a \<ge> b. z < x a"
hoelzl@35582
   660
using assms
hoelzl@35582
   661
proof -
hoelzl@35582
   662
  from assms have "y - z > 0" by simp
hoelzl@35582
   663
  hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
hoelzl@35582
   664
    unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
hoelzl@35582
   665
    by simp
hoelzl@35582
   666
  have "\<forall>m. x m \<le> y" using incseq_le assms by auto
hoelzl@35582
   667
  hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
hoelzl@35582
   668
    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
hoelzl@35582
   669
  from A B show ?thesis by auto
hoelzl@35582
   670
qed
hoelzl@35582
   671
hoelzl@35582
   672
lemma psfis_mono_conv_mono:
hoelzl@35582
   673
  assumes mono: "mono_convergent u f (space M)"
hoelzl@35582
   674
  and ps_u: "\<And>n. x n \<in> psfis (u n)"
hoelzl@35582
   675
  and "x ----> y"
hoelzl@35582
   676
  and "r \<in> psfis s"
hoelzl@35582
   677
  and f_upper_bound: "\<And>t. t \<in> space M \<Longrightarrow> s t \<le> f t"
hoelzl@35582
   678
  shows "r <= y"
hoelzl@35582
   679
proof (rule field_le_mult_one_interval)
hoelzl@35582
   680
  fix z :: real assume "0 < z" and "z < 1"
hoelzl@35582
   681
  hence "0 \<le> z" by auto
hoelzl@35582
   682
(*  def B' \<equiv> "\<lambda>n. {w \<in> space M. z * s w <= u n w}" *)
hoelzl@35582
   683
  let "?B' n" = "{w \<in> space M. z * s w <= u n w}"
hoelzl@35582
   684
hoelzl@35582
   685
  have "incseq x" unfolding incseq_def
hoelzl@35582
   686
  proof safe
hoelzl@35582
   687
    fix m n :: nat assume "m \<le> n"
hoelzl@35582
   688
    show "x m \<le> x n"
hoelzl@35582
   689
    proof (rule psfis_mono[OF `x m \<in> psfis (u m)` `x n \<in> psfis (u n)`])
hoelzl@35582
   690
      fix t assume "t \<in> space M"
hoelzl@35582
   691
      with mono_convergentD[OF mono this] `m \<le> n` show "u m t \<le> u n t"
hoelzl@35582
   692
        unfolding incseq_def by auto
hoelzl@35582
   693
    qed
hoelzl@35582
   694
  qed
hoelzl@35582
   695
hoelzl@35582
   696
  from `r \<in> psfis s`
hoelzl@35582
   697
  obtain s' a x' where r: "r = pos_simple_integral (s', a, x')"
hoelzl@35582
   698
    and ps_s: "(s', a, x') \<in> pos_simple s"
hoelzl@35582
   699
    unfolding psfis_def by auto
hoelzl@35582
   700
hoelzl@35582
   701
  { fix t i assume "i \<in> s'" "t \<in> a i"
hoelzl@35582
   702
    hence "t \<in> space M" using ps_s by (auto elim!: pos_simpleE) }
hoelzl@35582
   703
  note t_in_space = this
hoelzl@35582
   704
hoelzl@35582
   705
  { fix n
hoelzl@35582
   706
    from psfis_borel_measurable[OF `r \<in> psfis s`]
hoelzl@35582
   707
       psfis_borel_measurable[OF ps_u]
hoelzl@35582
   708
    have "?B' n \<in> sets M"
hoelzl@35582
   709
      by (auto intro!:
hoelzl@35582
   710
        borel_measurable_leq_borel_measurable
hoelzl@35582
   711
        borel_measurable_times_borel_measurable
hoelzl@35582
   712
        borel_measurable_const) }
hoelzl@35582
   713
  note B'_in_M = this
hoelzl@35582
   714
hoelzl@35582
   715
  { fix n have "(\<lambda>i. a i \<inter> ?B' n) ` s' \<subseteq> sets M" using B'_in_M ps_s
hoelzl@35582
   716
      by (auto intro!: Int elim!: pos_simpleE) }
hoelzl@35582
   717
  note B'_inter_a_in_M = this
hoelzl@35582
   718
hoelzl@35582
   719
  let "?sum n" = "(\<Sum>i\<in>s'. x' i * measure M (a i \<inter> ?B' n))"
hoelzl@35582
   720
  { fix n
hoelzl@35582
   721
    have "z * ?sum n \<le> x n"
hoelzl@35582
   722
    proof (rule psfis_mono[OF _ ps_u])
hoelzl@35582
   723
      have *: "\<And>i t. indicator_fn (?B' n) t * (x' i * indicator_fn (a i) t) =
hoelzl@35582
   724
        x' i * indicator_fn (a i \<inter> ?B' n) t" unfolding indicator_fn_def by auto
hoelzl@35582
   725
      have ps': "?sum n \<in> psfis (\<lambda>t. indicator_fn (?B' n) t * (\<Sum>i\<in>s'. x' i * indicator_fn (a i) t))"
hoelzl@35582
   726
        unfolding setsum_right_distrib * using B'_in_M ps_s
hoelzl@35582
   727
        by (auto intro!: psfis_intro Int elim!: pos_simpleE)
hoelzl@35582
   728
      also have "... = psfis (\<lambda>t. indicator_fn (?B' n) t * s t)" (is "psfis ?l = psfis ?r")
hoelzl@35582
   729
      proof (rule psfis_cong)
hoelzl@35582
   730
        show "nonneg ?l" using psfis_nonneg[OF ps'] .
hoelzl@35582
   731
        show "nonneg ?r" using psfis_nonneg[OF `r \<in> psfis s`] unfolding nonneg_def indicator_fn_def by auto
hoelzl@35582
   732
        fix t assume "t \<in> space M"
hoelzl@35582
   733
        show "?l t = ?r t" unfolding pos_simple_setsum_indicator_fn[OF ps_s `t \<in> space M`] ..
hoelzl@35582
   734
      qed
hoelzl@35582
   735
      finally show "z * ?sum n \<in> psfis (\<lambda>t. z * ?r t)" using psfis_mult[OF _ `0 \<le> z`] by simp
hoelzl@35582
   736
    next
hoelzl@35582
   737
      fix t assume "t \<in> space M"
hoelzl@35582
   738
      show "z * (indicator_fn (?B' n) t * s t) \<le> u n t"
hoelzl@35582
   739
         using psfis_nonneg[OF ps_u] unfolding nonneg_def indicator_fn_def by auto
hoelzl@35582
   740
    qed }
hoelzl@35582
   741
  hence *: "\<exists>N. \<forall>n\<ge>N. z * ?sum n \<le> x n" by (auto intro!: exI[of _ 0])
hoelzl@35582
   742
hoelzl@35582
   743
  show "z * r \<le> y" unfolding r pos_simple_integral_def
hoelzl@35582
   744
  proof (rule LIMSEQ_le[OF mult_right.LIMSEQ `x ----> y` *],
hoelzl@35582
   745
         simp, rule LIMSEQ_setsum, rule mult_right.LIMSEQ)
hoelzl@35582
   746
    fix i assume "i \<in> s'"
hoelzl@35582
   747
    from psfis_nonneg[OF `r \<in> psfis s`, unfolded nonneg_def]
hoelzl@35582
   748
    have "\<And>t. 0 \<le> s t" by simp
hoelzl@35582
   749
hoelzl@35582
   750
    have *: "(\<Union>j. a i \<inter> ?B' j) = a i"
hoelzl@35582
   751
    proof (safe, simp, safe)
hoelzl@35582
   752
      fix t assume "t \<in> a i"
hoelzl@35582
   753
      thus "t \<in> space M" using t_in_space[OF `i \<in> s'`] by auto
hoelzl@35582
   754
      show "\<exists>j. z * s t \<le> u j t"
hoelzl@35582
   755
      proof (cases "s t = 0")
hoelzl@35582
   756
        case True thus ?thesis
hoelzl@35582
   757
          using psfis_nonneg[OF ps_u] unfolding nonneg_def by auto
hoelzl@35582
   758
      next
hoelzl@35582
   759
        case False with `0 \<le> s t`
hoelzl@35582
   760
        have "0 < s t" by auto
hoelzl@35582
   761
        hence "z * s t < 1 * s t" using `0 < z` `z < 1`
hoelzl@35582
   762
          by (auto intro!: mult_strict_right_mono simp del: mult_1_left)
hoelzl@35582
   763
        also have "... \<le> f t" using f_upper_bound `t \<in> space M` by auto
hoelzl@35582
   764
        finally obtain b where "\<And>j. b \<le> j \<Longrightarrow> z * s t < u j t" using `t \<in> space M`
hoelzl@35582
   765
          using mono_conv_outgrow[of "\<lambda>n. u n t" "f t" "z * s t"]
hoelzl@35582
   766
          using mono_convergentD[OF mono] by auto
hoelzl@35582
   767
        from this[of b] show ?thesis by (auto intro!: exI[of _ b])
hoelzl@35582
   768
      qed
hoelzl@35582
   769
    qed
hoelzl@35582
   770
hoelzl@35582
   771
    show "(\<lambda>n. measure M (a i \<inter> ?B' n)) ----> measure M (a i)"
hoelzl@35582
   772
    proof (safe intro!:
hoelzl@35582
   773
        monotone_convergence[of "\<lambda>n. a i \<inter> ?B' n", unfolded comp_def *])
hoelzl@35582
   774
      fix n show "a i \<inter> ?B' n \<in> sets M"
hoelzl@35582
   775
        using B'_inter_a_in_M[of n] `i \<in> s'` by auto
hoelzl@35582
   776
    next
hoelzl@35582
   777
      fix j t assume "t \<in> space M" and "z * s t \<le> u j t"
hoelzl@35582
   778
      thus "z * s t \<le> u (Suc j) t"
hoelzl@35582
   779
        using mono_convergentD(1)[OF mono, unfolded incseq_def,
hoelzl@35582
   780
          rule_format, of t j "Suc j"]
hoelzl@35582
   781
        by auto
hoelzl@35582
   782
    qed
hoelzl@35582
   783
  qed
hoelzl@35582
   784
qed
hoelzl@35582
   785
hoelzl@35582
   786
lemma psfis_nnfis:
hoelzl@35582
   787
  "a \<in> psfis f \<Longrightarrow> a \<in> nnfis f"
hoelzl@35582
   788
  unfolding nnfis_def mono_convergent_def incseq_def
hoelzl@35582
   789
  by (auto intro!: exI[of _ "\<lambda>n. f"] exI[of _ "\<lambda>n. a"] LIMSEQ_const)
hoelzl@35582
   790
hoelzl@35582
   791
lemma nnfis_times:
hoelzl@35582
   792
  assumes "a \<in> nnfis f" and "0 \<le> z"
hoelzl@35582
   793
  shows "z * a \<in> nnfis (\<lambda>t. z * f t)"
hoelzl@35582
   794
proof -
hoelzl@35582
   795
  obtain u x where "mono_convergent u f (space M)" and
hoelzl@35582
   796
    "\<And>n. x n \<in> psfis (u n)" "x ----> a"
hoelzl@35582
   797
    using `a \<in> nnfis f` unfolding nnfis_def by auto
hoelzl@35582
   798
  with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
hoelzl@35582
   799
    by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
hoelzl@35582
   800
      LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
hoelzl@35582
   801
qed
hoelzl@35582
   802
hoelzl@35582
   803
lemma nnfis_add:
hoelzl@35582
   804
  assumes "a \<in> nnfis f" and "b \<in> nnfis g"
hoelzl@35582
   805
  shows "a + b \<in> nnfis (\<lambda>t. f t + g t)"
hoelzl@35582
   806
proof -
hoelzl@35582
   807
  obtain u x w y
hoelzl@35582
   808
    where "mono_convergent u f (space M)" and
hoelzl@35582
   809
    "\<And>n. x n \<in> psfis (u n)" "x ----> a" and
hoelzl@35582
   810
    "mono_convergent w g (space M)" and
hoelzl@35582
   811
    "\<And>n. y n \<in> psfis (w n)" "y ----> b"
hoelzl@35582
   812
    using `a \<in> nnfis f` `b \<in> nnfis g` unfolding nnfis_def by auto
hoelzl@35582
   813
  thus ?thesis unfolding nnfis_def mono_convergent_def incseq_def
hoelzl@35582
   814
    by (auto intro!: exI[of _ "\<lambda>n a. u n a + w n a"] exI[of _ "\<lambda>n. x n + y n"]
hoelzl@35582
   815
      LIMSEQ_add LIMSEQ_const psfis_add add_mono)
hoelzl@35582
   816
qed
hoelzl@35582
   817
hoelzl@35582
   818
lemma nnfis_mono:
hoelzl@35582
   819
  assumes nnfis: "a \<in> nnfis f" "b \<in> nnfis g"
hoelzl@35582
   820
  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
hoelzl@35582
   821
  shows "a \<le> b"
hoelzl@35582
   822
proof -
hoelzl@35582
   823
  obtain u x w y where
hoelzl@35582
   824
    mc: "mono_convergent u f (space M)" "mono_convergent w g (space M)" and
hoelzl@35582
   825
    psfis: "\<And>n. x n \<in> psfis (u n)" "\<And>n. y n \<in> psfis (w n)" and
hoelzl@35582
   826
    limseq: "x ----> a" "y ----> b" using nnfis unfolding nnfis_def by auto
hoelzl@35582
   827
  show ?thesis
hoelzl@35582
   828
  proof (rule LIMSEQ_le_const2[OF limseq(1)], rule exI[of _ 0], safe)
hoelzl@35582
   829
    fix n
hoelzl@35582
   830
    show "x n \<le> b"
hoelzl@35582
   831
    proof (rule psfis_mono_conv_mono[OF mc(2) psfis(2) limseq(2) psfis(1)])
hoelzl@35582
   832
      fix t assume "t \<in> space M"
hoelzl@35582
   833
      from mono_convergent_le[OF mc(1) this] mono[OF this]
hoelzl@35582
   834
      show "u n t \<le> g t" by (rule order_trans)
hoelzl@35582
   835
    qed
hoelzl@35582
   836
  qed
hoelzl@35582
   837
qed
hoelzl@35582
   838
hoelzl@35582
   839
lemma nnfis_unique:
hoelzl@35582
   840
  assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"
hoelzl@35582
   841
  shows "a = b"
hoelzl@35582
   842
  using nnfis_mono[OF a b] nnfis_mono[OF b a]
hoelzl@35582
   843
  by (auto intro!: real_le_antisym[of a b])
hoelzl@35582
   844
hoelzl@35582
   845
lemma psfis_equiv:
hoelzl@35582
   846
  assumes "a \<in> psfis f" and "nonneg g"
hoelzl@35582
   847
  and "\<And>t. t \<in> space M \<Longrightarrow> f t = g t"
hoelzl@35582
   848
  shows "a \<in> psfis g"
hoelzl@35582
   849
  using assms unfolding psfis_def pos_simple_def by auto
hoelzl@35582
   850
hoelzl@35582
   851
lemma psfis_mon_upclose:
hoelzl@35582
   852
  assumes "\<And>m. a m \<in> psfis (u m)"
hoelzl@35582
   853
  shows "\<exists>c. c \<in> psfis (mon_upclose n u)"
hoelzl@35582
   854
proof (induct n)
hoelzl@35582
   855
  case 0 thus ?case unfolding mon_upclose.simps using assms ..
hoelzl@35582
   856
next
hoelzl@35582
   857
  case (Suc n)
hoelzl@35582
   858
  then obtain sn an xn where ps: "(sn, an, xn) \<in> pos_simple (mon_upclose n u)"
hoelzl@35582
   859
    unfolding psfis_def by auto
hoelzl@35582
   860
  obtain ss as xs where ps': "(ss, as, xs) \<in> pos_simple (u (Suc n))"
hoelzl@35582
   861
    using assms[of "Suc n"] unfolding psfis_def by auto
hoelzl@35582
   862
  from pos_simple_common_partition[OF ps ps'] guess x x' a s .
hoelzl@35582
   863
  hence "(s, a, upclose x x') \<in> pos_simple (mon_upclose (Suc n) u)"
hoelzl@35582
   864
    by (simp add: upclose_def pos_simple_def nonneg_def max_def)
hoelzl@35582
   865
  thus ?case unfolding psfis_def by auto
hoelzl@35582
   866
qed
hoelzl@35582
   867
hoelzl@35582
   868
text {* Beppo-Levi monotone convergence theorem *}
hoelzl@35582
   869
lemma nnfis_mon_conv:
hoelzl@35582
   870
  assumes mc: "mono_convergent f h (space M)"
hoelzl@35582
   871
  and nnfis: "\<And>n. x n \<in> nnfis (f n)"
hoelzl@35582
   872
  and "x ----> z"
hoelzl@35582
   873
  shows "z \<in> nnfis h"
hoelzl@35582
   874
proof -
hoelzl@35582
   875
  have "\<forall>n. \<exists>u y. mono_convergent u (f n) (space M) \<and> (\<forall>m. y m \<in> psfis (u m)) \<and>
hoelzl@35582
   876
    y ----> x n"
hoelzl@35582
   877
    using nnfis unfolding nnfis_def by auto
hoelzl@35582
   878
  from choice[OF this] guess u ..
hoelzl@35582
   879
  from choice[OF this] guess y ..
hoelzl@35582
   880
  hence mc_u: "\<And>n. mono_convergent (u n) (f n) (space M)"
hoelzl@35582
   881
    and psfis: "\<And>n m. y n m \<in> psfis (u n m)" and "\<And>n. y n ----> x n"
hoelzl@35582
   882
    by auto
hoelzl@35582
   883
hoelzl@35582
   884
  let "?upclose n" = "mon_upclose n (\<lambda>m. u m n)"
hoelzl@35582
   885
hoelzl@35582
   886
  have "\<exists>c. \<forall>n. c n \<in> psfis (?upclose n)"
hoelzl@35582
   887
    by (safe intro!: choice psfis_mon_upclose) (rule psfis)
hoelzl@35582
   888
  then guess c .. note c = this[rule_format]
hoelzl@35582
   889
hoelzl@35582
   890
  show ?thesis unfolding nnfis_def
hoelzl@35582
   891
  proof (safe intro!: exI)
hoelzl@35582
   892
    show mc_upclose: "mono_convergent ?upclose h (space M)"
hoelzl@35582
   893
      by (rule mon_upclose_mono_convergent[OF mc_u mc])
hoelzl@35582
   894
    show psfis_upclose: "\<And>n. c n \<in> psfis (?upclose n)"
hoelzl@35582
   895
      using c .
hoelzl@35582
   896
hoelzl@35582
   897
    { fix n m :: nat assume "n \<le> m"
hoelzl@35582
   898
      hence "c n \<le> c m"
hoelzl@35582
   899
        using psfis_mono[OF c c]
hoelzl@35582
   900
        using mono_convergentD(1)[OF mc_upclose, unfolded incseq_def]
hoelzl@35582
   901
        by auto }
hoelzl@35582
   902
    hence "incseq c" unfolding incseq_def by auto
hoelzl@35582
   903
hoelzl@35582
   904
    { fix n
hoelzl@35582
   905
      have c_nnfis: "c n \<in> nnfis (?upclose n)" using c by (rule psfis_nnfis)
hoelzl@35582
   906
      from nnfis_mono[OF c_nnfis nnfis]
hoelzl@35582
   907
        mon_upclose_le_mono_convergent[OF mc_u]
hoelzl@35582
   908
        mono_convergentD(1)[OF mc]
hoelzl@35582
   909
      have "c n \<le> x n" by fast }
hoelzl@35582
   910
    note c_less_x = this
hoelzl@35582
   911
hoelzl@35582
   912
    { fix n
hoelzl@35582
   913
      note c_less_x[of n]
hoelzl@35582
   914
      also have "x n \<le> z"
hoelzl@35582
   915
      proof (rule incseq_le)
hoelzl@35582
   916
        show "x ----> z" by fact
hoelzl@35582
   917
        from mono_convergentD(1)[OF mc]
hoelzl@35582
   918
        show "incseq x" unfolding incseq_def
hoelzl@35582
   919
          by (auto intro!: nnfis_mono[OF nnfis nnfis])
hoelzl@35582
   920
      qed
hoelzl@35582
   921
      finally have "c n \<le> z" . }
hoelzl@35582
   922
    note c_less_z = this
hoelzl@35582
   923
hoelzl@35582
   924
    have "convergent c"
hoelzl@35582
   925
    proof (rule Bseq_mono_convergent[unfolded incseq_def[symmetric]])
hoelzl@35582
   926
      show "Bseq c"
hoelzl@35582
   927
        using pos_psfis[OF c] c_less_z
hoelzl@35582
   928
        by (auto intro!: BseqI'[of _ z])
hoelzl@35582
   929
      show "incseq c" by fact
hoelzl@35582
   930
    qed
hoelzl@35582
   931
    then obtain l where l: "c ----> l" unfolding convergent_def by auto
hoelzl@35582
   932
hoelzl@35582
   933
    have "l \<le> z" using c_less_x l
hoelzl@35582
   934
      by (auto intro!: LIMSEQ_le[OF _ `x ----> z`])
hoelzl@35582
   935
    moreover have "z \<le> l"
hoelzl@35582
   936
    proof (rule LIMSEQ_le_const2[OF `x ----> z`], safe intro!: exI[of _ 0])
hoelzl@35582
   937
      fix n
hoelzl@35582
   938
      have "l \<in> nnfis h"
hoelzl@35582
   939
        unfolding nnfis_def using l mc_upclose psfis_upclose by auto
hoelzl@35582
   940
      from nnfis this mono_convergent_le[OF mc]
hoelzl@35582
   941
      show "x n \<le> l" by (rule nnfis_mono)
hoelzl@35582
   942
    qed
hoelzl@35582
   943
    ultimately have "l = z" by (rule real_le_antisym)
hoelzl@35582
   944
    thus "c ----> z" using `c ----> l` by simp
hoelzl@35582
   945
  qed
hoelzl@35582
   946
qed
hoelzl@35582
   947
hoelzl@35582
   948
lemma nnfis_pos_on_mspace:
hoelzl@35582
   949
  assumes "a \<in> nnfis f" and "x \<in>space M"
hoelzl@35582
   950
  shows "0 \<le> f x"
hoelzl@35582
   951
using assms
hoelzl@35582
   952
proof -
hoelzl@35582
   953
  from assms[unfolded nnfis_def] guess u y by auto note uy = this
hoelzl@35582
   954
  hence "\<And> n. 0 \<le> u n x" 
hoelzl@35582
   955
    unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
hoelzl@35582
   956
    by auto
hoelzl@35582
   957
  thus "0 \<le> f x" using uy[rule_format]
hoelzl@35582
   958
    unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
hoelzl@35582
   959
    using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans
hoelzl@35582
   960
    by fast
hoelzl@35582
   961
qed
hoelzl@35582
   962
hoelzl@35582
   963
lemma nnfis_borel_measurable:
hoelzl@35582
   964
  assumes "a \<in> nnfis f"
hoelzl@35582
   965
  shows "f \<in> borel_measurable M"
hoelzl@35582
   966
using assms unfolding nnfis_def
hoelzl@35582
   967
apply auto
hoelzl@35582
   968
apply (rule mono_convergent_borel_measurable)
hoelzl@35582
   969
using psfis_borel_measurable
hoelzl@35582
   970
by auto
hoelzl@35582
   971
hoelzl@35582
   972
lemma borel_measurable_mon_conv_psfis:
hoelzl@35582
   973
  assumes f_borel: "f \<in> borel_measurable M"
hoelzl@35582
   974
  and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
hoelzl@35582
   975
  shows"\<exists>u x. mono_convergent u f (space M) \<and> (\<forall>n. x n \<in> psfis (u n))"
hoelzl@35582
   976
proof (safe intro!: exI)
hoelzl@35582
   977
  let "?I n" = "{0<..<n * 2^n}"
hoelzl@35582
   978
  let "?A n i" = "{w \<in> space M. real (i :: nat) / 2^(n::nat) \<le> f w \<and> f w < real (i + 1) / 2^n}"
hoelzl@35582
   979
  let "?u n t" = "\<Sum>i\<in>?I n. real i / 2^n * indicator_fn (?A n i) t"
hoelzl@35582
   980
  let "?x n" = "\<Sum>i\<in>?I n. real i / 2^n * measure M (?A n i)"
hoelzl@35582
   981
hoelzl@35582
   982
  let "?w n t" = "if f t < real n then real (natfloor (f t * 2^n)) / 2^n else 0"
hoelzl@35582
   983
hoelzl@35582
   984
  { fix t n assume t: "t \<in> space M"
hoelzl@35582
   985
    have "?u n t = ?w n t" (is "_ = (if _ then real ?i / _ else _)")
hoelzl@35582
   986
    proof (cases "f t < real n")
hoelzl@35582
   987
      case True
hoelzl@35582
   988
      with nonneg t
hoelzl@35582
   989
      have i: "?i < n * 2^n"
hoelzl@35582
   990
        by (auto simp: real_of_nat_power[symmetric]
hoelzl@35582
   991
                 intro!: less_natfloor mult_nonneg_nonneg)
hoelzl@35582
   992
hoelzl@35582
   993
      hence t_in_A: "t \<in> ?A n ?i"
hoelzl@35582
   994
        unfolding divide_le_eq less_divide_eq
hoelzl@35582
   995
        using nonneg t True
hoelzl@35582
   996
        by (auto intro!: real_natfloor_le
hoelzl@35582
   997
          real_natfloor_gt_diff_one[unfolded diff_less_eq]
hoelzl@35582
   998
          simp: real_of_nat_Suc zero_le_mult_iff)
hoelzl@35582
   999
hoelzl@35582
  1000
      hence *: "real ?i / 2^n \<le> f t"
hoelzl@35582
  1001
        "f t < real (?i + 1) / 2^n" by auto
hoelzl@35582
  1002
      { fix j assume "t \<in> ?A n j"
hoelzl@35582
  1003
        hence "real j / 2^n \<le> f t"
hoelzl@35582
  1004
          and "f t < real (j + 1) / 2^n" by auto
hoelzl@35582
  1005
        with * have "j \<in> {?i}" unfolding divide_le_eq less_divide_eq
hoelzl@35582
  1006
          by auto }
hoelzl@35582
  1007
      hence *: "\<And>j. t \<in> ?A n j \<longleftrightarrow> j \<in> {?i}" using t_in_A by auto
hoelzl@35582
  1008
hoelzl@35582
  1009
      have "?u n t = real ?i / 2^n"
hoelzl@35582
  1010
        unfolding indicator_fn_def if_distrib *
hoelzl@35582
  1011
          setsum_cases[OF finite_greaterThanLessThan]
hoelzl@35582
  1012
        using i by (cases "?i = 0") simp_all
hoelzl@35582
  1013
      thus ?thesis using True by auto
hoelzl@35582
  1014
    next
hoelzl@35582
  1015
      case False
hoelzl@35582
  1016
      have "?u n t = (\<Sum>i \<in> {0 <..< n*2^n}. 0)"
hoelzl@35582
  1017
      proof (rule setsum_cong)
hoelzl@35582
  1018
        fix i assume "i \<in> {0 <..< n*2^n}"
hoelzl@35582
  1019
        hence "i + 1 \<le> n * 2^n" by simp
hoelzl@35582
  1020
        hence "real (i + 1) \<le> real n * 2^n"
hoelzl@35582
  1021
          unfolding real_of_nat_le_iff[symmetric]
hoelzl@35582
  1022
          by (auto simp: real_of_nat_power[symmetric])
hoelzl@35582
  1023
        also have "... \<le> f t * 2^n"
hoelzl@35582
  1024
          using False by (auto intro!: mult_nonneg_nonneg)
hoelzl@35582
  1025
        finally have "t \<notin> ?A n i"
hoelzl@35582
  1026
          by (auto simp: divide_le_eq less_divide_eq)
hoelzl@35582
  1027
        thus "real i / 2^n * indicator_fn (?A n i) t = 0"
hoelzl@35582
  1028
          unfolding indicator_fn_def by auto
hoelzl@35582
  1029
      qed simp
hoelzl@35582
  1030
      thus ?thesis using False by auto
hoelzl@35582
  1031
    qed }
hoelzl@35582
  1032
  note u_at_t = this
hoelzl@35582
  1033
hoelzl@35582
  1034
  show "mono_convergent ?u f (space M)" unfolding mono_convergent_def
hoelzl@35582
  1035
  proof safe
hoelzl@35582
  1036
    fix t assume t: "t \<in> space M"
hoelzl@35582
  1037
    { fix m n :: nat assume "m \<le> n"
hoelzl@35582
  1038
      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
hoelzl@35582
  1039
      have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
hoelzl@35582
  1040
        apply (subst *)
hoelzl@35582
  1041
        apply (subst class_semiring.mul_a)
hoelzl@35582
  1042
        apply (subst real_of_nat_le_iff)
hoelzl@35582
  1043
        apply (rule le_mult_natfloor)
hoelzl@35582
  1044
        using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
hoelzl@35582
  1045
      hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
hoelzl@35582
  1046
        apply (subst *)
hoelzl@35582
  1047
        apply (subst (3) class_semiring.mul_c)
hoelzl@35582
  1048
        apply (subst class_semiring.mul_a)
hoelzl@35582
  1049
        by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
hoelzl@35582
  1050
    thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
hoelzl@35582
  1051
      by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)
hoelzl@35582
  1052
hoelzl@35582
  1053
    show "(\<lambda>i. ?u i t) ----> f t" unfolding u_at_t[OF t]
hoelzl@35582
  1054
    proof (rule LIMSEQ_I, safe intro!: exI)
hoelzl@35582
  1055
      fix r :: real and n :: nat
hoelzl@35582
  1056
      let ?N = "natfloor (1/r) + 1"
hoelzl@35582
  1057
      assume "0 < r" and N: "max ?N (natfloor (f t) + 1) \<le> n"
hoelzl@35582
  1058
      hence "?N \<le> n" by auto
hoelzl@35582
  1059
hoelzl@35582
  1060
      have "1 / r < real (natfloor (1/r) + 1)" using real_natfloor_add_one_gt
hoelzl@35582
  1061
        by (simp add: real_of_nat_Suc)
hoelzl@35582
  1062
      also have "... < 2^?N" by (rule two_realpow_gt)
hoelzl@35582
  1063
      finally have less_r: "1 / 2^?N < r" using `0 < r`
hoelzl@35582
  1064
        by (auto simp: less_divide_eq divide_less_eq algebra_simps)
hoelzl@35582
  1065
hoelzl@35582
  1066
      have "f t < real (natfloor (f t) + 1)" using real_natfloor_add_one_gt[of "f t"] by auto
hoelzl@35582
  1067
      also have "... \<le> real n" unfolding real_of_nat_le_iff using N by auto
hoelzl@35582
  1068
      finally have "f t < real n" .
hoelzl@35582
  1069
hoelzl@35582
  1070
      have "real (natfloor (f t * 2^n)) \<le> f t * 2^n"
hoelzl@35582
  1071
        using nonneg[OF t] by (auto intro!: real_natfloor_le mult_nonneg_nonneg)
hoelzl@35582
  1072
      hence less: "real (natfloor (f t * 2^n)) / 2^n \<le> f t" unfolding divide_le_eq by auto
hoelzl@35582
  1073
hoelzl@35582
  1074
      have "f t * 2 ^ n - 1 < real (natfloor (f t * 2^n))" using real_natfloor_gt_diff_one .
hoelzl@35582
  1075
      hence "f t - real (natfloor (f t * 2^n)) / 2^n < 1 / 2^n"
hoelzl@35582
  1076
        by (auto simp: less_divide_eq divide_less_eq algebra_simps)
hoelzl@35582
  1077
      also have "... \<le> 1 / 2^?N" using `?N \<le> n`
hoelzl@35582
  1078
        by (auto intro!: divide_left_mono mult_pos_pos simp del: power_Suc)
hoelzl@35582
  1079
      also have "... < r" using less_r .
hoelzl@35582
  1080
      finally show "norm (?w n t - f t) < r" using `f t < real n` less by auto
hoelzl@35582
  1081
    qed
hoelzl@35582
  1082
  qed
hoelzl@35582
  1083
hoelzl@35582
  1084
  fix n
hoelzl@35582
  1085
  show "?x n \<in> psfis (?u n)"
hoelzl@35582
  1086
  proof (rule psfis_intro)
hoelzl@35582
  1087
    show "?A n ` ?I n \<subseteq> sets M"
hoelzl@35582
  1088
    proof safe
hoelzl@35582
  1089
      fix i :: nat
hoelzl@35582
  1090
      from Int[OF
hoelzl@35582
  1091
        f_borel[unfolded borel_measurable_less_iff, rule_format, of "real (i+1) / 2^n"]
hoelzl@35582
  1092
        f_borel[unfolded borel_measurable_ge_iff, rule_format, of "real i / 2^n"]]
hoelzl@35582
  1093
      show "?A n i \<in> sets M"
hoelzl@35582
  1094
        by (metis Collect_conj_eq Int_commute Int_left_absorb Int_left_commute)
hoelzl@35582
  1095
    qed
hoelzl@35582
  1096
    show "nonneg (\<lambda>i :: nat. real i / 2 ^ n)"
hoelzl@35582
  1097
      unfolding nonneg_def by (auto intro!: divide_nonneg_pos)
hoelzl@35582
  1098
  qed auto
hoelzl@35582
  1099
qed
hoelzl@35582
  1100
hoelzl@35582
  1101
lemma nnfis_dom_conv:
hoelzl@35582
  1102
  assumes borel: "f \<in> borel_measurable M"
hoelzl@35582
  1103
  and nnfis: "b \<in> nnfis g"
hoelzl@35582
  1104
  and ord: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
hoelzl@35582
  1105
  and nonneg: "\<And>t. t \<in> space M \<Longrightarrow> 0 \<le> f t"
hoelzl@35582
  1106
  shows "\<exists>a. a \<in> nnfis f \<and> a \<le> b"
hoelzl@35582
  1107
proof -
hoelzl@35582
  1108
  obtain u x where mc_f: "mono_convergent u f (space M)" and
hoelzl@35582
  1109
    psfis: "\<And>n. x n \<in> psfis (u n)"
hoelzl@35582
  1110
    using borel_measurable_mon_conv_psfis[OF borel nonneg] by auto
hoelzl@35582
  1111
hoelzl@35582
  1112
  { fix n
hoelzl@35582
  1113
    { fix t assume t: "t \<in> space M"
hoelzl@35582
  1114
      note mono_convergent_le[OF mc_f this, of n]
hoelzl@35582
  1115
      also note ord[OF t]
hoelzl@35582
  1116
      finally have "u n t \<le> g t" . }
hoelzl@35582
  1117
    from nnfis_mono[OF psfis_nnfis[OF psfis] nnfis this]
hoelzl@35582
  1118
    have "x n \<le> b" by simp }
hoelzl@35582
  1119
  note x_less_b = this
hoelzl@35582
  1120
hoelzl@35582
  1121
  have "convergent x"
hoelzl@35582
  1122
  proof (safe intro!: Bseq_mono_convergent)
hoelzl@35582
  1123
    from x_less_b pos_psfis[OF psfis]
hoelzl@35582
  1124
    show "Bseq x" by (auto intro!: BseqI'[of _ b])
hoelzl@35582
  1125
hoelzl@35582
  1126
    fix n m :: nat assume *: "n \<le> m"
hoelzl@35582
  1127
    show "x n \<le> x m"
hoelzl@35582
  1128
    proof (rule psfis_mono[OF `x n \<in> psfis (u n)` `x m \<in> psfis (u m)`])
hoelzl@35582
  1129
      fix t assume "t \<in> space M"
hoelzl@35582
  1130
      from mc_f[THEN mono_convergentD(1), unfolded incseq_def, OF this]
hoelzl@35582
  1131
      show "u n t \<le> u m t" using * by auto
hoelzl@35582
  1132
    qed
hoelzl@35582
  1133
  qed
hoelzl@35582
  1134
  then obtain a where "x ----> a" unfolding convergent_def by auto
hoelzl@35582
  1135
  with LIMSEQ_le_const2[OF `x ----> a`] x_less_b mc_f psfis
hoelzl@35582
  1136
  show ?thesis unfolding nnfis_def by auto
hoelzl@35582
  1137
qed
hoelzl@35582
  1138
hoelzl@35582
  1139
lemma psfis_0: "0 \<in> psfis (\<lambda>x. 0)"
hoelzl@35582
  1140
  unfolding psfis_def pos_simple_def pos_simple_integral_def
hoelzl@35582
  1141
  by (auto simp: nonneg_def
hoelzl@35582
  1142
      intro: image_eqI[where x="({0}, (\<lambda>i. space M), (\<lambda>i. 0))"])
hoelzl@35582
  1143
hoelzl@35582
  1144
lemma the_nnfis[simp]: "a \<in> nnfis f \<Longrightarrow> (THE a. a \<in> nnfis f) = a"
hoelzl@35582
  1145
  by (auto intro: the_equality nnfis_unique)
hoelzl@35582
  1146
hoelzl@35582
  1147
lemma nnfis_cong:
hoelzl@35582
  1148
  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
hoelzl@35582
  1149
  shows "nnfis f = nnfis g"
hoelzl@35582
  1150
proof -
hoelzl@35582
  1151
  { fix f g :: "'a \<Rightarrow> real" assume cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
hoelzl@35582
  1152
    fix x assume "x \<in> nnfis f"
hoelzl@35582
  1153
    then guess u y unfolding nnfis_def by safe note x = this
hoelzl@35582
  1154
    hence "mono_convergent u g (space M)"
hoelzl@35582
  1155
      unfolding mono_convergent_def using cong by auto
hoelzl@35582
  1156
    with x(2,3) have "x \<in> nnfis g" unfolding nnfis_def by auto }
hoelzl@35582
  1157
  from this[OF cong] this[OF cong[symmetric]]
hoelzl@35582
  1158
  show ?thesis by safe
hoelzl@35582
  1159
qed
hoelzl@35582
  1160
hoelzl@35582
  1161
lemma integral_cong:
hoelzl@35582
  1162
  assumes cong: "\<And>x. x \<in> space M \<Longrightarrow> f x = g x"
hoelzl@35582
  1163
  shows "integral f = integral g"
hoelzl@35582
  1164
proof -
hoelzl@35582
  1165
  have "nnfis (pos_part f) = nnfis (pos_part g)"
hoelzl@35582
  1166
    using cong by (auto simp: pos_part_def intro!: nnfis_cong)
hoelzl@35582
  1167
  moreover
hoelzl@35582
  1168
  have "nnfis (neg_part f) = nnfis (neg_part g)"
hoelzl@35582
  1169
    using cong by (auto simp: neg_part_def intro!: nnfis_cong)
hoelzl@35582
  1170
  ultimately show ?thesis
hoelzl@35582
  1171
    unfolding integral_def by auto
hoelzl@35582
  1172
qed
hoelzl@35582
  1173
hoelzl@35582
  1174
lemma nnfis_integral:
hoelzl@35582
  1175
  assumes "a \<in> nnfis f"
hoelzl@35582
  1176
  shows "integrable f" and "integral f = a"
hoelzl@35582
  1177
proof -
hoelzl@35582
  1178
  have a: "a \<in> nnfis (pos_part f)"
hoelzl@35582
  1179
    using assms nnfis_pos_on_mspace[OF assms]
hoelzl@35582
  1180
    by (auto intro!: nnfis_mon_conv[of "\<lambda>i. f" _ "\<lambda>i. a"]
hoelzl@35582
  1181
      LIMSEQ_const simp: mono_convergent_def pos_part_def incseq_def max_def)
hoelzl@35582
  1182
hoelzl@35582
  1183
  have "\<And>t. t \<in> space M \<Longrightarrow> neg_part f t = 0"
hoelzl@35582
  1184
    unfolding neg_part_def min_def
hoelzl@35582
  1185
    using nnfis_pos_on_mspace[OF assms] by auto
hoelzl@35582
  1186
  hence 0: "0 \<in> nnfis (neg_part f)"
hoelzl@35582
  1187
    by (auto simp: nnfis_def mono_convergent_def psfis_0 incseq_def
hoelzl@35582
  1188
          intro!: LIMSEQ_const exI[of _ "\<lambda> x n. 0"] exI[of _ "\<lambda> n. 0"])
hoelzl@35582
  1189
hoelzl@35582
  1190
  from 0 a show "integrable f" "integral f = a"
hoelzl@35582
  1191
    unfolding integrable_def integral_def by auto
hoelzl@35582
  1192
qed
hoelzl@35582
  1193
hoelzl@35582
  1194
lemma nnfis_minus_nnfis_integral:
hoelzl@35582
  1195
  assumes "a \<in> nnfis f" and "b \<in> nnfis g"
hoelzl@35582
  1196
  shows "integrable (\<lambda>t. f t - g t)" and "integral (\<lambda>t. f t - g t) = a - b"
hoelzl@35582
  1197
proof -
hoelzl@35582
  1198
  have borel: "(\<lambda>t. f t - g t) \<in> borel_measurable M" using assms
hoelzl@35582
  1199
    by (blast intro:
hoelzl@35582
  1200
      borel_measurable_diff_borel_measurable nnfis_borel_measurable)
hoelzl@35582
  1201
hoelzl@35582
  1202
  have "\<exists>x. x \<in> nnfis (pos_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
hoelzl@35582
  1203
    (is "\<exists>x. x \<in> nnfis ?pp \<and> _")
hoelzl@35582
  1204
  proof (rule nnfis_dom_conv)
hoelzl@35582
  1205
    show "?pp \<in> borel_measurable M"
hoelzl@35582
  1206
      using borel by (rule pos_part_neg_part_borel_measurable)
hoelzl@35582
  1207
    show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
hoelzl@35582
  1208
    fix t assume "t \<in> space M"
hoelzl@35582
  1209
    with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
hoelzl@35582
  1210
    show "?pp t \<le> f t + g t" unfolding pos_part_def by auto
hoelzl@35582
  1211
    show "0 \<le> ?pp t" using nonneg_pos_part[of "\<lambda>t. f t - g t"]
hoelzl@35582
  1212
      unfolding nonneg_def by auto
hoelzl@35582
  1213
  qed
hoelzl@35582
  1214
  then obtain x where x: "x \<in> nnfis ?pp" by auto
hoelzl@35582
  1215
  moreover
hoelzl@35582
  1216
  have "\<exists>x. x \<in> nnfis (neg_part (\<lambda>t. f t - g t)) \<and> x \<le> a + b"
hoelzl@35582
  1217
    (is "\<exists>x. x \<in> nnfis ?np \<and> _")
hoelzl@35582
  1218
  proof (rule nnfis_dom_conv)
hoelzl@35582
  1219
    show "?np \<in> borel_measurable M"
hoelzl@35582
  1220
      using borel by (rule pos_part_neg_part_borel_measurable)
hoelzl@35582
  1221
    show "a + b \<in> nnfis (\<lambda>t. f t + g t)" using assms by (rule nnfis_add)
hoelzl@35582
  1222
    fix t assume "t \<in> space M"
hoelzl@35582
  1223
    with assms nnfis_add assms[THEN nnfis_pos_on_mspace[OF _ this]]
hoelzl@35582
  1224
    show "?np t \<le> f t + g t" unfolding neg_part_def by auto
hoelzl@35582
  1225
    show "0 \<le> ?np t" using nonneg_neg_part[of "\<lambda>t. f t - g t"]
hoelzl@35582
  1226
      unfolding nonneg_def by auto
hoelzl@35582
  1227
  qed
hoelzl@35582
  1228
  then obtain y where y: "y \<in> nnfis ?np" by auto
hoelzl@35582
  1229
  ultimately show "integrable (\<lambda>t. f t - g t)"
hoelzl@35582
  1230
    unfolding integrable_def by auto
hoelzl@35582
  1231
hoelzl@35582
  1232
  from x and y
hoelzl@35582
  1233
  have "a + y \<in> nnfis (\<lambda>t. f t + ?np t)"
hoelzl@35582
  1234
    and "b + x \<in> nnfis (\<lambda>t. g t + ?pp t)" using assms by (auto intro: nnfis_add)
hoelzl@35582
  1235
  moreover
hoelzl@35582
  1236
  have "\<And>t. f t + ?np t = g t + ?pp t"
hoelzl@35582
  1237
    unfolding pos_part_def neg_part_def by auto
hoelzl@35582
  1238
  ultimately have "a - b = x - y"
hoelzl@35582
  1239
    using nnfis_unique by (auto simp: algebra_simps)
hoelzl@35582
  1240
  thus "integral (\<lambda>t. f t - g t) = a - b"
hoelzl@35582
  1241
    unfolding integral_def
hoelzl@35582
  1242
    using the_nnfis[OF x] the_nnfis[OF y] by simp
hoelzl@35582
  1243
qed
hoelzl@35582
  1244
hoelzl@35582
  1245
lemma integral_borel_measurable:
hoelzl@35582
  1246
  "integrable f \<Longrightarrow> f \<in> borel_measurable M"
hoelzl@35582
  1247
  unfolding integrable_def
hoelzl@35582
  1248
  by (subst pos_part_neg_part_borel_measurable_iff)
hoelzl@35582
  1249
   (auto intro: nnfis_borel_measurable)
hoelzl@35582
  1250
hoelzl@35582
  1251
lemma integral_indicator_fn:
hoelzl@35582
  1252
  assumes "a \<in> sets M"
hoelzl@35582
  1253
  shows "integral (indicator_fn a) = measure M a"
hoelzl@35582
  1254
  and "integrable (indicator_fn a)"
hoelzl@35582
  1255
  using psfis_indicator[OF assms, THEN psfis_nnfis]
hoelzl@35582
  1256
  by (auto intro!: nnfis_integral)
hoelzl@35582
  1257
hoelzl@35582
  1258
lemma integral_add:
hoelzl@35582
  1259
  assumes "integrable f" and "integrable g"
hoelzl@35582
  1260
  shows "integrable (\<lambda>t. f t + g t)"
hoelzl@35582
  1261
  and "integral (\<lambda>t. f t + g t) = integral f + integral g"
hoelzl@35582
  1262
proof -
hoelzl@35582
  1263
  { fix t
hoelzl@35582
  1264
    have "pos_part f t + pos_part g t - (neg_part f t + neg_part g t) =
hoelzl@35582
  1265
      f t + g t"
hoelzl@35582
  1266
      unfolding pos_part_def neg_part_def by auto }
hoelzl@35582
  1267
  note part_sum = this
hoelzl@35582
  1268
hoelzl@35582
  1269
  from assms obtain a b c d where
hoelzl@35582
  1270
    a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
hoelzl@35582
  1271
    c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
hoelzl@35582
  1272
    unfolding integrable_def by auto
hoelzl@35582
  1273
  note sums = nnfis_add[OF a c] nnfis_add[OF b d]
hoelzl@35582
  1274
  note int = nnfis_minus_nnfis_integral[OF sums, unfolded part_sum]
hoelzl@35582
  1275
hoelzl@35582
  1276
  show "integrable (\<lambda>t. f t + g t)" using int(1) .
hoelzl@35582
  1277
hoelzl@35582
  1278
  show "integral (\<lambda>t. f t + g t) = integral f + integral g"
hoelzl@35582
  1279
    using int(2) sums a b c d by (simp add: the_nnfis integral_def)
hoelzl@35582
  1280
qed
hoelzl@35582
  1281
hoelzl@35582
  1282
lemma integral_mono:
hoelzl@35582
  1283
  assumes "integrable f" and "integrable g"
hoelzl@35582
  1284
  and mono: "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
hoelzl@35582
  1285
  shows "integral f \<le> integral g"
hoelzl@35582
  1286
proof -
hoelzl@35582
  1287
  from assms obtain a b c d where
hoelzl@35582
  1288
    a: "a \<in> nnfis (pos_part f)" and b: "b \<in> nnfis (neg_part f)" and
hoelzl@35582
  1289
    c: "c \<in> nnfis (pos_part g)" and d: "d \<in> nnfis (neg_part g)"
hoelzl@35582
  1290
    unfolding integrable_def by auto
hoelzl@35582
  1291
hoelzl@35582
  1292
  have "a \<le> c"
hoelzl@35582
  1293
  proof (rule nnfis_mono[OF a c])
hoelzl@35582
  1294
    fix t assume "t \<in> space M"
hoelzl@35582
  1295
    from mono[OF this] show "pos_part f t \<le> pos_part g t"
hoelzl@35582
  1296
      unfolding pos_part_def by auto
hoelzl@35582
  1297
  qed
hoelzl@35582
  1298
  moreover have "d \<le> b"
hoelzl@35582
  1299
  proof (rule nnfis_mono[OF d b])
hoelzl@35582
  1300
    fix t assume "t \<in> space M"
hoelzl@35582
  1301
    from mono[OF this] show "neg_part g t \<le> neg_part f t"
hoelzl@35582
  1302
      unfolding neg_part_def by auto
hoelzl@35582
  1303
  qed
hoelzl@35582
  1304
  ultimately have "a - b \<le> c - d" by auto
hoelzl@35582
  1305
  thus ?thesis unfolding integral_def
hoelzl@35582
  1306
    using a b c d by (simp add: the_nnfis)
hoelzl@35582
  1307
qed
hoelzl@35582
  1308
hoelzl@35582
  1309
lemma integral_uminus:
hoelzl@35582
  1310
  assumes "integrable f"
hoelzl@35582
  1311
  shows "integrable (\<lambda>t. - f t)"
hoelzl@35582
  1312
  and "integral (\<lambda>t. - f t) = - integral f"
hoelzl@35582
  1313
proof -
hoelzl@35582
  1314
  have "pos_part f = neg_part (\<lambda>t.-f t)" and "neg_part f = pos_part (\<lambda>t.-f t)"
hoelzl@35582
  1315
    unfolding pos_part_def neg_part_def by (auto intro!: ext)
hoelzl@35582
  1316
  with assms show "integrable (\<lambda>t.-f t)" and "integral (\<lambda>t.-f t) = -integral f"
hoelzl@35582
  1317
    unfolding integrable_def integral_def by simp_all
hoelzl@35582
  1318
qed
hoelzl@35582
  1319
hoelzl@35582
  1320
lemma integral_times_const:
hoelzl@35582
  1321
  assumes "integrable f"
hoelzl@35582
  1322
  shows "integrable (\<lambda>t. a * f t)" (is "?P a")
hoelzl@35582
  1323
  and "integral (\<lambda>t. a * f t) = a * integral f" (is "?I a")
hoelzl@35582
  1324
proof -
hoelzl@35582
  1325
  { fix a :: real assume "0 \<le> a"
hoelzl@35582
  1326
    hence "pos_part (\<lambda>t. a * f t) = (\<lambda>t. a * pos_part f t)"
hoelzl@35582
  1327
      and "neg_part (\<lambda>t. a * f t) = (\<lambda>t. a * neg_part f t)"
hoelzl@35582
  1328
      unfolding pos_part_def neg_part_def max_def min_def
hoelzl@35582
  1329
      by (auto intro!: ext simp: zero_le_mult_iff)
hoelzl@35582
  1330
    moreover
hoelzl@35582
  1331
    obtain x y where x: "x \<in> nnfis (pos_part f)" and y: "y \<in> nnfis (neg_part f)"
hoelzl@35582
  1332
      using assms unfolding integrable_def by auto
hoelzl@35582
  1333
    ultimately
hoelzl@35582
  1334
    have "a * x \<in> nnfis (pos_part (\<lambda>t. a * f t))" and
hoelzl@35582
  1335
      "a * y \<in> nnfis (neg_part (\<lambda>t. a * f t))"
hoelzl@35582
  1336
      using nnfis_times[OF _ `0 \<le> a`] by auto
hoelzl@35582
  1337
    with x y have "?P a \<and> ?I a"
hoelzl@35582
  1338
      unfolding integrable_def integral_def by (auto simp: algebra_simps) }
hoelzl@35582
  1339
  note int = this
hoelzl@35582
  1340
hoelzl@35582
  1341
  have "?P a \<and> ?I a"
hoelzl@35582
  1342
  proof (cases "0 \<le> a")
hoelzl@35582
  1343
    case True from int[OF this] show ?thesis .
hoelzl@35582
  1344
  next
hoelzl@35582
  1345
    case False with int[of "- a"] integral_uminus[of "\<lambda>t. - a * f t"]
hoelzl@35582
  1346
    show ?thesis by auto
hoelzl@35582
  1347
  qed
hoelzl@35582
  1348
  thus "integrable (\<lambda>t. a * f t)"
hoelzl@35582
  1349
    and "integral (\<lambda>t. a * f t) = a * integral f" by simp_all
hoelzl@35582
  1350
qed
hoelzl@35582
  1351
hoelzl@35582
  1352
lemma integral_cmul_indicator:
hoelzl@35582
  1353
  assumes "s \<in> sets M"
hoelzl@35582
  1354
  shows "integral (\<lambda>x. c * indicator_fn s x) = c * (measure M s)"
hoelzl@35582
  1355
  and "integrable (\<lambda>x. c * indicator_fn s x)"
hoelzl@35582
  1356
using assms integral_times_const integral_indicator_fn by auto
hoelzl@35582
  1357
hoelzl@35582
  1358
lemma integral_zero:
hoelzl@35582
  1359
  shows "integral (\<lambda>x. 0) = 0"
hoelzl@35582
  1360
  and "integrable (\<lambda>x. 0)"
hoelzl@35582
  1361
  using integral_cmul_indicator[OF empty_sets, of 0]
hoelzl@35582
  1362
  unfolding indicator_fn_def by auto
hoelzl@35582
  1363
hoelzl@35582
  1364
lemma integral_setsum:
hoelzl@35582
  1365
  assumes "finite S"
hoelzl@35582
  1366
  assumes "\<And>n. n \<in> S \<Longrightarrow> integrable (f n)"
hoelzl@35582
  1367
  shows "integral (\<lambda>x. \<Sum> i \<in> S. f i x) = (\<Sum> i \<in> S. integral (f i))" (is "?int S")
hoelzl@35582
  1368
    and "integrable (\<lambda>x. \<Sum> i \<in> S. f i x)" (is "?I s")
hoelzl@35582
  1369
proof -
hoelzl@35582
  1370
  from assms have "?int S \<and> ?I S"
hoelzl@35582
  1371
  proof (induct S)
hoelzl@35582
  1372
    case empty thus ?case by (simp add: integral_zero)
hoelzl@35582
  1373
  next
hoelzl@35582
  1374
    case (insert i S)
hoelzl@35582
  1375
    thus ?case
hoelzl@35582
  1376
      apply simp
hoelzl@35582
  1377
      apply (subst integral_add)
hoelzl@35582
  1378
      using assms apply auto
hoelzl@35582
  1379
      apply (subst integral_add)
hoelzl@35582
  1380
      using assms by auto
hoelzl@35582
  1381
  qed
hoelzl@35582
  1382
  thus "?int S" and "?I S" by auto
hoelzl@35582
  1383
qed
hoelzl@35582
  1384
hoelzl@35582
  1385
lemma markov_ineq:
hoelzl@35582
  1386
  assumes "integrable f" "0 < a" "integrable (\<lambda>x. \<bar>f x\<bar>^n)"
hoelzl@35582
  1387
  shows "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
hoelzl@35582
  1388
using assms
hoelzl@35582
  1389
proof -
hoelzl@35582
  1390
  from assms have "0 < a ^ n" using real_root_pow_pos by auto
hoelzl@35582
  1391
  from assms have "f \<in> borel_measurable M"
hoelzl@35582
  1392
    using integral_borel_measurable[OF `integrable f`] by auto
hoelzl@35582
  1393
  hence w: "{w . w \<in> space M \<and> a \<le> f w} \<in> sets M"
hoelzl@35582
  1394
    using borel_measurable_ge_iff by auto
hoelzl@35582
  1395
  have i: "integrable (indicator_fn {w . w \<in> space M \<and> a \<le> f w})"
hoelzl@35582
  1396
    using integral_indicator_fn[OF w] by simp
hoelzl@35582
  1397
  have v1: "\<And> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t 
hoelzl@35582
  1398
            \<le> (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t"
hoelzl@35582
  1399
    unfolding indicator_fn_def
hoelzl@35582
  1400
    using `0 < a` power_mono[of a] assms by auto
hoelzl@35582
  1401
  have v2: "\<And> t. (f t) ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t \<le> \<bar>f t\<bar> ^ n"
hoelzl@35582
  1402
    unfolding indicator_fn_def 
hoelzl@35582
  1403
    using power_mono[of a _ n] abs_ge_self `a > 0` 
hoelzl@35582
  1404
    by auto
hoelzl@35582
  1405
  have "{w \<in> space M. a \<le> f w} \<inter> space M = {w . a \<le> f w} \<inter> space M"
hoelzl@35582
  1406
    using Collect_eq by auto
hoelzl@35582
  1407
  from Int_absorb2[OF sets_into_space[OF w]] `0 < a ^ n` sets_into_space[OF w] w this
hoelzl@35582
  1408
  have "(a ^ n) * (measure M ((f -` {y . a \<le> y}) \<inter> space M)) =
hoelzl@35582
  1409
        (a ^ n) * measure M {w . w \<in> space M \<and> a \<le> f w}"
hoelzl@35582
  1410
    unfolding vimage_Collect_eq[of f] by simp
hoelzl@35582
  1411
  also have "\<dots> = integral (\<lambda> t. a ^ n * (indicator_fn {w . w \<in> space M \<and> a \<le> f w}) t)"
hoelzl@35582
  1412
    using integral_cmul_indicator[OF w] i by auto
hoelzl@35582
  1413
  also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"
hoelzl@35582
  1414
    apply (rule integral_mono)
hoelzl@35582
  1415
    using integral_cmul_indicator[OF w]
hoelzl@35582
  1416
      `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto
hoelzl@35582
  1417
  finally show "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
hoelzl@35582
  1418
    unfolding atLeast_def
hoelzl@35582
  1419
    by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
hoelzl@35582
  1420
qed
hoelzl@35582
  1421
hoelzl@35582
  1422
lemma integral_finite_on_sets:
hoelzl@35582
  1423
  assumes "f \<in> borel_measurable M" and "finite (space M)" and "a \<in> sets M"
hoelzl@35582
  1424
  shows "integral (\<lambda>x. f x * indicator_fn a x) =
hoelzl@35582
  1425
    (\<Sum> r \<in> f`a. r * measure M (f -` {r} \<inter> a))" (is "integral ?f = _")
hoelzl@35582
  1426
proof -
hoelzl@35582
  1427
  { fix x assume "x \<in> a"
hoelzl@35582
  1428
    with assms have "f -` {f x} \<inter> space M \<in> sets M"
hoelzl@35582
  1429
      by (subst Int_commute)
hoelzl@35582
  1430
         (auto simp: vimage_def Int_def
hoelzl@35582
  1431
               intro!: borel_measurable_const
hoelzl@35582
  1432
                      borel_measurable_eq_borel_measurable)
hoelzl@35582
  1433
    from Int[OF this assms(3)]
hoelzl@35582
  1434
         sets_into_space[OF assms(3), THEN Int_absorb1]
hoelzl@35582
  1435
    have "f -` {f x} \<inter> a \<in> sets M" by (simp add: Int_assoc) }
hoelzl@35582
  1436
  note vimage_f = this
hoelzl@35582
  1437
hoelzl@35582
  1438
  have "finite a"
hoelzl@35582
  1439
    using assms(2,3) sets_into_space
hoelzl@35582
  1440
    by (auto intro: finite_subset)
hoelzl@35582
  1441
hoelzl@35582
  1442
  have "integral (\<lambda>x. f x * indicator_fn a x) =
hoelzl@35582
  1443
    integral (\<lambda>x. \<Sum>i\<in>f ` a. i * indicator_fn (f -` {i} \<inter> a) x)"
hoelzl@35582
  1444
    (is "_ = integral (\<lambda>x. setsum (?f x) _)")
hoelzl@35582
  1445
    unfolding indicator_fn_def if_distrib
hoelzl@35582
  1446
    using `finite a` by (auto simp: setsum_cases intro!: integral_cong)
hoelzl@35582
  1447
  also have "\<dots> = (\<Sum>i\<in>f`a. integral (\<lambda>x. ?f x i))"
hoelzl@35582
  1448
  proof (rule integral_setsum, safe)
hoelzl@35582
  1449
    fix n x assume "x \<in> a"
hoelzl@35582
  1450
    thus "integrable (\<lambda>y. ?f y (f x))"
hoelzl@35582
  1451
      using integral_indicator_fn(2)[OF vimage_f]
hoelzl@35582
  1452
      by (auto intro!: integral_times_const)
hoelzl@35582
  1453
  qed (simp add: `finite a`)
hoelzl@35582
  1454
  also have "\<dots> = (\<Sum>i\<in>f`a. i * measure M (f -` {i} \<inter> a))"
hoelzl@35582
  1455
    using integral_cmul_indicator[OF vimage_f]
hoelzl@35582
  1456
    by (auto intro!: setsum_cong)
hoelzl@35582
  1457
  finally show ?thesis .
hoelzl@35582
  1458
qed
hoelzl@35582
  1459
hoelzl@35582
  1460
lemma integral_finite:
hoelzl@35582
  1461
  assumes "f \<in> borel_measurable M" and "finite (space M)"
hoelzl@35582
  1462
  shows "integral f = (\<Sum> r \<in> f ` space M. r * measure M (f -` {r} \<inter> space M))"
hoelzl@35582
  1463
  using integral_finite_on_sets[OF assms top]
hoelzl@35582
  1464
    integral_cong[of "\<lambda>x. f x * indicator_fn (space M) x" f]
hoelzl@35582
  1465
  by (auto simp add: indicator_fn_def)
hoelzl@35582
  1466
hoelzl@35582
  1467
lemma integral_finite_singleton:
hoelzl@35582
  1468
  assumes fin: "finite (space M)" and "Pow (space M) = sets M"
hoelzl@35582
  1469
  shows "integral f = (\<Sum>x \<in> space M. f x * measure M {x})"
hoelzl@35582
  1470
proof -
hoelzl@35582
  1471
  have "f \<in> borel_measurable M"
hoelzl@35582
  1472
    unfolding borel_measurable_le_iff
hoelzl@35582
  1473
    using assms by auto
hoelzl@35582
  1474
  { fix r let ?x = "f -` {r} \<inter> space M"
hoelzl@35582
  1475
    have "?x \<subseteq> space M" by auto
hoelzl@35582
  1476
    with assms have "measure M ?x = (\<Sum>i \<in> ?x. measure M {i})"
hoelzl@35582
  1477
      by (auto intro!: measure_real_sum_image) }
hoelzl@35582
  1478
  note measure_eq_setsum = this
hoelzl@35582
  1479
  show ?thesis
hoelzl@35582
  1480
    unfolding integral_finite[OF `f \<in> borel_measurable M` fin]
hoelzl@35582
  1481
      measure_eq_setsum setsum_right_distrib
hoelzl@35582
  1482
    apply (subst setsum_Sigma)
hoelzl@35582
  1483
    apply (simp add: assms)
hoelzl@35582
  1484
    apply (simp add: assms)
hoelzl@35582
  1485
  proof (rule setsum_reindex_cong[symmetric])
hoelzl@35582
  1486
    fix a assume "a \<in> Sigma (f ` space M) (\<lambda>x. f -` {x} \<inter> space M)"
hoelzl@35582
  1487
    thus "(\<lambda>(x, y). x * measure M {y}) a = f (snd a) * measure_space.measure M {snd a}"
hoelzl@35582
  1488
      by auto
hoelzl@35582
  1489
  qed (auto intro!: image_eqI inj_onI)
hoelzl@35582
  1490
qed
hoelzl@35582
  1491
hoelzl@35582
  1492
lemma borel_measurable_inverse:
hoelzl@35582
  1493
  assumes "f \<in> borel_measurable M"
hoelzl@35582
  1494
  shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
hoelzl@35582
  1495
  unfolding borel_measurable_ge_iff
hoelzl@35582
  1496
proof (safe, rule linorder_cases)
hoelzl@35582
  1497
  fix a :: real assume "0 < a"
hoelzl@35582
  1498
  { fix w
hoelzl@35582
  1499
    from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
hoelzl@35582
  1500
      by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
hoelzl@35582
  1501
                linorder_not_le real_le_refl real_le_trans real_less_def
hoelzl@35582
  1502
                xt1(7) zero_less_divide_1_iff) }
hoelzl@35582
  1503
  hence "{w \<in> space M. a \<le> inverse (f w)} =
hoelzl@35582
  1504
    {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
hoelzl@35582
  1505
  with Int assms[unfolded borel_measurable_gr_iff]
hoelzl@35582
  1506
    assms[unfolded borel_measurable_le_iff]
hoelzl@35582
  1507
  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
hoelzl@35582
  1508
next
hoelzl@35582
  1509
  fix a :: real assume "0 = a"
hoelzl@35582
  1510
  { fix w have "a \<le> inverse (f w) \<longleftrightarrow> 0 \<le> f w"
hoelzl@35582
  1511
      unfolding `0 = a`[symmetric] by auto }
hoelzl@35582
  1512
  thus "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M"
hoelzl@35582
  1513
    using assms[unfolded borel_measurable_ge_iff] by simp
hoelzl@35582
  1514
next
hoelzl@35582
  1515
  fix a :: real assume "a < 0"
hoelzl@35582
  1516
  { fix w
hoelzl@35582
  1517
    from `a < 0` have "a \<le> inverse (f w) \<longleftrightarrow> f w \<le> 1 / a \<or> 0 \<le> f w"
hoelzl@35582
  1518
      apply (cases "0 \<le> f w")
hoelzl@35582
  1519
      apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
hoelzl@35582
  1520
                   zero_le_divide_1_iff)
hoelzl@35582
  1521
      apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
hoelzl@35582
  1522
                   linorder_not_le real_le_refl real_le_trans)
hoelzl@35582
  1523
      done }
hoelzl@35582
  1524
  hence "{w \<in> space M. a \<le> inverse (f w)} =
hoelzl@35582
  1525
    {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
hoelzl@35582
  1526
  with Un assms[unfolded borel_measurable_ge_iff]
hoelzl@35582
  1527
    assms[unfolded borel_measurable_le_iff]
hoelzl@35582
  1528
  show "{w \<in> space M. a \<le> inverse (f w)} \<in> sets M" by simp
hoelzl@35582
  1529
qed
hoelzl@35582
  1530
hoelzl@35582
  1531
lemma borel_measurable_divide:
hoelzl@35582
  1532
  assumes "f \<in> borel_measurable M"
hoelzl@35582
  1533
  and "g \<in> borel_measurable M"
hoelzl@35582
  1534
  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
hoelzl@35582
  1535
  unfolding field_divide_inverse
hoelzl@35582
  1536
  by (rule borel_measurable_inverse borel_measurable_times_borel_measurable assms)+
hoelzl@35582
  1537
hoelzl@35582
  1538
lemma RN_deriv_finite_singleton:
hoelzl@35582
  1539
  fixes v :: "'a set \<Rightarrow> real"
hoelzl@35582
  1540
  assumes finite: "finite (space M)" and Pow: "Pow (space M) = sets M"
hoelzl@35582
  1541
  and ms_v: "measure_space (M\<lparr>measure := v\<rparr>)"
hoelzl@35582
  1542
  and eq_0: "\<And>x. measure M {x} = 0 \<Longrightarrow> v {x} = 0"
hoelzl@35582
  1543
  and "x \<in> space M" and "measure M {x} \<noteq> 0"
hoelzl@35582
  1544
  shows "RN_deriv v x = v {x} / (measure M {x})" (is "_ = ?v x")
hoelzl@35582
  1545
  unfolding RN_deriv_def
hoelzl@35582
  1546
proof (rule someI2_ex[where Q = "\<lambda>f. f x = ?v x"], rule exI[where x = ?v], safe)
hoelzl@35582
  1547
  show "(\<lambda>a. v {a} / measure_space.measure M {a}) \<in> borel_measurable M"
hoelzl@35582
  1548
    unfolding borel_measurable_le_iff using Pow by auto
hoelzl@35582
  1549
next
hoelzl@35582
  1550
  fix a assume "a \<in> sets M"
hoelzl@35582
  1551
  hence "a \<subseteq> space M" and "finite a"
hoelzl@35582
  1552
    using sets_into_space finite by (auto intro: finite_subset)
hoelzl@35582
  1553
  have *: "\<And>x a. (if measure M {x} = 0 then 0 else v {x} * indicator_fn a x) =
hoelzl@35582
  1554
    v {x} * indicator_fn a x" using eq_0 by auto
hoelzl@35582
  1555
hoelzl@35582
  1556
  from measure_space.measure_real_sum_image[OF ms_v, of a]
hoelzl@35582
  1557
    Pow `a \<in> sets M` sets_into_space `finite a`
hoelzl@35582
  1558
  have "v a = (\<Sum>x\<in>a. v {x})" by auto
hoelzl@35582
  1559
  thus "integral (\<lambda>x. v {x} / measure_space.measure M {x} * indicator_fn a x) = v a"
hoelzl@35582
  1560
    apply (simp add: eq_0 integral_finite_singleton[OF finite Pow])
hoelzl@35582
  1561
    apply (unfold divide_1)
hoelzl@35582
  1562
    by (simp add: * indicator_fn_def if_distrib setsum_cases finite `a \<subseteq> space M` Int_absorb1)
hoelzl@35582
  1563
next
hoelzl@35582
  1564
  fix w assume "w \<in> borel_measurable M"
hoelzl@35582
  1565
  assume int_eq_v: "\<forall>a\<in>sets M. integral (\<lambda>x. w x * indicator_fn a x) = v a"
hoelzl@35582
  1566
  have "{x} \<in> sets M" using Pow `x \<in> space M` by auto
hoelzl@35582
  1567
hoelzl@35582
  1568
  have "w x * measure M {x} =
hoelzl@35582
  1569
    (\<Sum>y\<in>space M. w y * indicator_fn {x} y * measure M {y})"
hoelzl@35582
  1570
    apply (subst (3) mult_commute)
hoelzl@35582
  1571
    unfolding indicator_fn_def if_distrib setsum_cases[OF finite]
hoelzl@35582
  1572
    using `x \<in> space M` by simp
hoelzl@35582
  1573
  also have "... = v {x}"
hoelzl@35582
  1574
    using int_eq_v[rule_format, OF `{x} \<in> sets M`]
hoelzl@35582
  1575
    by (simp add: integral_finite_singleton[OF finite Pow])
hoelzl@35582
  1576
  finally show "w x = v {x} / measure M {x}"
hoelzl@35582
  1577
    using `measure M {x} \<noteq> 0` by (simp add: eq_divide_eq)
hoelzl@35582
  1578
qed fact
hoelzl@35582
  1579
hoelzl@35582
  1580
lemma countable_space_integral_reduce:
hoelzl@35582
  1581
  assumes "positive M (measure M)" and "f \<in> borel_measurable M"
hoelzl@35582
  1582
  and "countable (f ` space M)"
hoelzl@35582
  1583
  and "\<not> finite (pos_part f ` space M)"
hoelzl@35582
  1584
  and "\<not> finite (neg_part f ` space M)"
hoelzl@35582
  1585
  and "((\<lambda>r. r * measure m (neg_part f -` {r} \<inter> space m)) o enumerate (neg_part f ` space M)) sums n"
hoelzl@35582
  1586
  and "((\<lambda>r. r * measure m (pos_part f -` {r} \<inter> space m)) o enumerate (pos_part f ` space M)) sums p"
hoelzl@35582
  1587
  shows "integral f = p - n"
hoelzl@35582
  1588
oops
hoelzl@35582
  1589
hoelzl@35582
  1590
(*
hoelzl@35582
  1591
val countable_space_integral_reduce = store_thm
hoelzl@35582
  1592
  ("countable_space_integral_reduce",
hoelzl@35582
  1593
   "\<forall>m f p n. measure_space m \<and>
hoelzl@35582
  1594
	     positive m \<and>
hoelzl@35582
  1595
	     f \<in> borel_measurable (space m, sets m) \<and>
hoelzl@35582
  1596
	     countable (IMAGE f (space m)) \<and>
hoelzl@35582
  1597
	     ~(FINITE (IMAGE (pos_part f) (space m))) \<and>
hoelzl@35582
  1598
	     ~(FINITE (IMAGE (neg_part f) (space m))) \<and>
hoelzl@35582
  1599
	     (\<lambda>r. r *
hoelzl@35582
  1600
		  measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
hoelzl@35582
  1601
		enumerate ((IMAGE (neg_part f) (space m))) sums n \<and>
hoelzl@35582
  1602
	     (\<lambda>r. r *
hoelzl@35582
  1603
		  measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
hoelzl@35582
  1604
		enumerate ((IMAGE (pos_part f) (space m))) sums p ==>
hoelzl@35582
  1605
	     (integral m f = p - n)",
hoelzl@35582
  1606
   RW_TAC std_ss [integral_def]
hoelzl@35582
  1607
   ++ Suff `((@i. i \<in> nnfis m (pos_part f)) = p) \<and> ((@i. i \<in> nnfis m (neg_part f)) = n)`
hoelzl@35582
  1608
   >> RW_TAC std_ss []
hoelzl@35582
  1609
   ++ (CONJ_TAC ++ MATCH_MP_TAC SELECT_UNIQUE ++ RW_TAC std_ss [])
hoelzl@35582
  1610
   >> (Suff `p \<in> nnfis m (pos_part f)` >> METIS_TAC [nnfis_unique]
hoelzl@35582
  1611
       ++ MATCH_MP_TAC nnfis_mon_conv
hoelzl@35582
  1612
       ++ `BIJ (enumerate(IMAGE (pos_part f) (space m))) UNIV (IMAGE (pos_part f) (space m))`
hoelzl@35582
  1613
		by (`countable (IMAGE (pos_part f) (space m))`
hoelzl@35582
  1614
			by (MATCH_MP_TAC COUNTABLE_SUBSET
hoelzl@35582
  1615
			    ++ Q.EXISTS_TAC `0 INSERT (IMAGE f (space m))`
hoelzl@35582
  1616
			    ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, pos_part_def, COUNTABLE_INSERT, IN_INSERT]
hoelzl@35582
  1617
			    ++ METIS_TAC [])
hoelzl@35582
  1618
		     ++ METIS_TAC [COUNTABLE_ALT])
hoelzl@35582
  1619
       ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
hoelzl@35582
  1620
       ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m)))
hoelzl@35582
  1621
			(pred_set$count n) then pos_part f t else 0)`
hoelzl@35582
  1622
       ++ Q.EXISTS_TAC `(\<lambda>n.
hoelzl@35582
  1623
         sum (0,n)
hoelzl@35582
  1624
           ((\<lambda>r.
hoelzl@35582
  1625
               r *
hoelzl@35582
  1626
               measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
hoelzl@35582
  1627
            enumerate (IMAGE (pos_part f) (space m))))`
hoelzl@35582
  1628
       ++ ASM_SIMP_TAC std_ss []
hoelzl@35582
  1629
       ++ CONJ_TAC
hoelzl@35582
  1630
       >> (RW_TAC std_ss [mono_convergent_def]
hoelzl@35582
  1631
	   >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, pos_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS])
hoelzl@35582
  1632
	   ++ RW_TAC std_ss [SEQ]
hoelzl@35582
  1633
	   ++ `\<exists>N. enumerate (IMAGE (pos_part f) (space m)) N = (pos_part f) t`
hoelzl@35582
  1634
		by METIS_TAC [IN_IMAGE]
hoelzl@35582
  1635
	   ++ Q.EXISTS_TAC `SUC N`
hoelzl@35582
  1636
	   ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
hoelzl@35582
  1637
	   ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
hoelzl@35582
  1638
	   ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, pos_part_def])
hoelzl@35582
  1639
       ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
hoelzl@35582
  1640
	   ++ `(\<lambda>t. (if t \<in> space m \<and> pos_part f t \<in> IMAGE (enumerate (IMAGE (pos_part f) (space m))) (pred_set$count n')
hoelzl@35582
  1641
      			then pos_part f t else  0)) =
hoelzl@35582
  1642
		(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
hoelzl@35582
  1643
			indicator_fn ((\<lambda>i. PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i}
hoelzl@35582
  1644
					   \<inter> (space m)) i) t)
hoelzl@35582
  1645
		     (pred_set$count n'))`
hoelzl@35582
  1646
		by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
hoelzl@35582
  1647
		    >> (`pred_set$count n' = x INSERT (pred_set$count n')`
hoelzl@35582
  1648
				by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
hoelzl@35582
  1649
			++ POP_ORW
hoelzl@35582
  1650
			++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
hoelzl@35582
  1651
			++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
hoelzl@35582
  1652
				REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
hoelzl@35582
  1653
			++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
hoelzl@35582
  1654
			++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
hoelzl@35582
  1655
				enumerate (IMAGE (pos_part f) (space m)) x' *
hoelzl@35582
  1656
				(if enumerate (IMAGE (pos_part f) (space m)) x =
hoelzl@35582
  1657
				enumerate (IMAGE (pos_part f) (space m)) x'
hoelzl@35582
  1658
				then 1 else 0) else 0)) = (\<lambda>x. 0)`
hoelzl@35582
  1659
				by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
hoelzl@35582
  1660
			++ POP_ORW
hoelzl@35582
  1661
			++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
hoelzl@35582
  1662
		    ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
hoelzl@35582
  1663
		    >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
hoelzl@35582
  1664
		    ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
hoelzl@35582
  1665
			REAL_SUM_IMAGE_IN_IF]
hoelzl@35582
  1666
		    ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
hoelzl@35582
  1667
			(\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i *
hoelzl@35582
  1668
           		(if (pos_part f t = enumerate (IMAGE (pos_part f) (space m)) i) \<and>
hoelzl@35582
  1669
             		 t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
hoelzl@35582
  1670
			by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
hoelzl@35582
  1671
		    ++ POP_ORW
hoelzl@35582
  1672
		    ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
hoelzl@35582
  1673
	   ++ POP_ORW
hoelzl@35582
  1674
	   ++ `((\<lambda>r. r * measure m (PREIMAGE (pos_part f) {r} \<inter> space m)) o
hoelzl@35582
  1675
		enumerate (IMAGE (pos_part f) (space m))) =
hoelzl@35582
  1676
		(\<lambda>i. (\<lambda>i. enumerate (IMAGE (pos_part f) (space m)) i) i *
hoelzl@35582
  1677
			measure m ((\<lambda>i.
hoelzl@35582
  1678
                PREIMAGE (pos_part f)
hoelzl@35582
  1679
                  {enumerate (IMAGE (pos_part f) (space m)) i} \<inter>
hoelzl@35582
  1680
                space m) i))`
hoelzl@35582
  1681
		by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
hoelzl@35582
  1682
	   ++ POP_ORW
hoelzl@35582
  1683
	   ++ MATCH_MP_TAC psfis_intro
hoelzl@35582
  1684
	   ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
hoelzl@35582
  1685
	   ++ REVERSE CONJ_TAC
hoelzl@35582
  1686
	   >> (FULL_SIMP_TAC real_ss [IN_IMAGE, pos_part_def]
hoelzl@35582
  1687
	       ++ METIS_TAC [REAL_LE_REFL])
hoelzl@35582
  1688
	   ++ `(pos_part f) \<in> borel_measurable (space m, sets m)`
hoelzl@35582
  1689
		by METIS_TAC [pos_part_neg_part_borel_measurable]
hoelzl@35582
  1690
	   ++ REPEAT STRIP_TAC
hoelzl@35582
  1691
	   ++ `PREIMAGE (pos_part f) {enumerate (IMAGE (pos_part f) (space m)) i} \<inter> space m =
hoelzl@35582
  1692
		{w | w \<in> space m \<and> ((pos_part f) w = (\<lambda>w. enumerate (IMAGE (pos_part f) (space m)) i) w)}`
hoelzl@35582
  1693
		by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
hoelzl@35582
  1694
		    ++ DECIDE_TAC)
hoelzl@35582
  1695
	   ++ POP_ORW
hoelzl@35582
  1696
	   ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
hoelzl@35582
  1697
	   ++ METIS_TAC [borel_measurable_const, measure_space_def])
hoelzl@35582
  1698
   ++ Suff `n \<in> nnfis m (neg_part f)` >> METIS_TAC [nnfis_unique]
hoelzl@35582
  1699
   ++ MATCH_MP_TAC nnfis_mon_conv
hoelzl@35582
  1700
   ++ `BIJ (enumerate(IMAGE (neg_part f) (space m))) UNIV (IMAGE (neg_part f) (space m))`
hoelzl@35582
  1701
		by (`countable (IMAGE (neg_part f) (space m))`
hoelzl@35582
  1702
			by (MATCH_MP_TAC COUNTABLE_SUBSET
hoelzl@35582
  1703
			    ++ Q.EXISTS_TAC `0 INSERT (IMAGE abs (IMAGE f (space m)))`
hoelzl@35582
  1704
			    ++ RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, abs, neg_part_def, COUNTABLE_INSERT, IN_INSERT, COUNTABLE_IMAGE]
hoelzl@35582
  1705
			    ++ METIS_TAC [])
hoelzl@35582
  1706
		     ++ METIS_TAC [COUNTABLE_ALT])
hoelzl@35582
  1707
   ++ FULL_SIMP_TAC std_ss [sums, BIJ_DEF, INJ_DEF, SURJ_DEF, IN_UNIV]
hoelzl@35582
  1708
   ++ Q.EXISTS_TAC `(\<lambda>n t. if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m)))
hoelzl@35582
  1709
			(pred_set$count n) then neg_part f t else 0)`
hoelzl@35582
  1710
   ++ Q.EXISTS_TAC `(\<lambda>n.
hoelzl@35582
  1711
         sum (0,n)
hoelzl@35582
  1712
           ((\<lambda>r.
hoelzl@35582
  1713
               r *
hoelzl@35582
  1714
               measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
hoelzl@35582
  1715
            enumerate (IMAGE (neg_part f) (space m))))`
hoelzl@35582
  1716
   ++ ASM_SIMP_TAC std_ss []
hoelzl@35582
  1717
   ++ CONJ_TAC
hoelzl@35582
  1718
   >> (RW_TAC std_ss [mono_convergent_def]
hoelzl@35582
  1719
	   >> (RW_TAC real_ss [IN_IMAGE, pred_setTheory.IN_COUNT, neg_part_def] ++ METIS_TAC [LESS_LESS_EQ_TRANS, REAL_LE_NEGTOTAL])
hoelzl@35582
  1720
	   ++ RW_TAC std_ss [SEQ]
hoelzl@35582
  1721
	   ++ `\<exists>N. enumerate (IMAGE (neg_part f) (space m)) N = (neg_part f) t`
hoelzl@35582
  1722
		by METIS_TAC [IN_IMAGE]
hoelzl@35582
  1723
	   ++ Q.EXISTS_TAC `SUC N`
hoelzl@35582
  1724
	   ++ RW_TAC real_ss [GREATER_EQ, real_ge, IN_IMAGE, REAL_SUB_LZERO]
hoelzl@35582
  1725
	   ++ FULL_SIMP_TAC std_ss [pred_setTheory.IN_COUNT]
hoelzl@35582
  1726
	   ++ METIS_TAC [DECIDE "!n:num. n < SUC n", LESS_LESS_EQ_TRANS, neg_part_def])
hoelzl@35582
  1727
   ++ STRIP_TAC ++ MATCH_MP_TAC psfis_nnfis ++ ASM_SIMP_TAC std_ss [GSYM REAL_SUM_IMAGE_COUNT]
hoelzl@35582
  1728
	   ++ `(\<lambda>t. (if t \<in> space m \<and> neg_part f t \<in> IMAGE (enumerate (IMAGE (neg_part f) (space m))) (pred_set$count n')
hoelzl@35582
  1729
      			then neg_part f t else  0)) =
hoelzl@35582
  1730
		(\<lambda>t. SIGMA (\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
hoelzl@35582
  1731
			indicator_fn ((\<lambda>i. PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i}
hoelzl@35582
  1732
					   \<inter> (space m)) i) t)
hoelzl@35582
  1733
		     (pred_set$count n'))`
hoelzl@35582
  1734
		by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [IN_IMAGE]
hoelzl@35582
  1735
		    >> (`pred_set$count n' = x INSERT (pred_set$count n')`
hoelzl@35582
  1736
				by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [IN_INSERT] ++ METIS_TAC [])
hoelzl@35582
  1737
			++ POP_ORW
hoelzl@35582
  1738
			++ RW_TAC std_ss [REAL_SUM_IMAGE_THM, pred_setTheory.FINITE_COUNT]
hoelzl@35582
  1739
			++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o
hoelzl@35582
  1740
				REWRITE_RULE [FINITE_DELETE] o Q.ISPEC `pred_set$count n' DELETE x`) REAL_SUM_IMAGE_IN_IF]
hoelzl@35582
  1741
			++ RW_TAC real_ss [IN_DELETE, indicator_fn_def, IN_INTER, IN_SING, IN_PREIMAGE]
hoelzl@35582
  1742
			++ `(\x'. (if x' \<in> pred_set$count n' \<and> ~(x' = x) then
hoelzl@35582
  1743
				enumerate (IMAGE (neg_part f) (space m)) x' *
hoelzl@35582
  1744
				(if enumerate (IMAGE (neg_part f) (space m)) x =
hoelzl@35582
  1745
				enumerate (IMAGE (neg_part f) (space m)) x'
hoelzl@35582
  1746
				then 1 else 0) else 0)) = (\<lambda>x. 0)`
hoelzl@35582
  1747
				by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
hoelzl@35582
  1748
			++ POP_ORW
hoelzl@35582
  1749
			++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE])
hoelzl@35582
  1750
		    ++ FULL_SIMP_TAC real_ss [IN_IMAGE, indicator_fn_def, IN_INTER, IN_PREIMAGE, IN_SING]
hoelzl@35582
  1751
		    >> RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT, FINITE_DELETE]
hoelzl@35582
  1752
		    ++ ONCE_REWRITE_TAC [(REWRITE_RULE [pred_setTheory.FINITE_COUNT] o Q.ISPEC `pred_set$count n'`)
hoelzl@35582
  1753
			REAL_SUM_IMAGE_IN_IF]
hoelzl@35582
  1754
		    ++ `(\<lambda>x. (if x \<in> pred_set$count n' then
hoelzl@35582
  1755
			(\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i *
hoelzl@35582
  1756
           		(if (neg_part f t = enumerate (IMAGE (neg_part f) (space m)) i) \<and>
hoelzl@35582
  1757
             		 t \<in> space m then 1 else 0)) x else 0)) = (\<lambda>x. 0)`
hoelzl@35582
  1758
			by (RW_TAC std_ss [FUN_EQ_THM] ++ RW_TAC real_ss [] ++ METIS_TAC [])
hoelzl@35582
  1759
		    ++ POP_ORW
hoelzl@35582
  1760
		    ++ RW_TAC real_ss [REAL_SUM_IMAGE_0, pred_setTheory.FINITE_COUNT])
hoelzl@35582
  1761
	   ++ POP_ORW
hoelzl@35582
  1762
	   ++ `((\<lambda>r. r * measure m (PREIMAGE (neg_part f) {r} \<inter> space m)) o
hoelzl@35582
  1763
		enumerate (IMAGE (neg_part f) (space m))) =
hoelzl@35582
  1764
		(\<lambda>i. (\<lambda>i. enumerate (IMAGE (neg_part f) (space m)) i) i *
hoelzl@35582
  1765
			measure m ((\<lambda>i.
hoelzl@35582
  1766
                PREIMAGE (neg_part f)
hoelzl@35582
  1767
                  {enumerate (IMAGE (neg_part f) (space m)) i} \<inter>
hoelzl@35582
  1768
                space m) i))`
hoelzl@35582
  1769
		by (RW_TAC std_ss [FUN_EQ_THM, o_DEF] ++ RW_TAC real_ss [])
hoelzl@35582
  1770
	   ++ POP_ORW
hoelzl@35582
  1771
	   ++ MATCH_MP_TAC psfis_intro
hoelzl@35582
  1772
	   ++ ASM_SIMP_TAC std_ss [pred_setTheory.FINITE_COUNT]
hoelzl@35582
  1773
	   ++ REVERSE CONJ_TAC
hoelzl@35582
  1774
	   >> (FULL_SIMP_TAC real_ss [IN_IMAGE, neg_part_def]
hoelzl@35582
  1775
	       ++ METIS_TAC [REAL_LE_REFL, REAL_LE_NEGTOTAL])
hoelzl@35582
  1776
	   ++ `(neg_part f) \<in> borel_measurable (space m, sets m)`
hoelzl@35582
  1777
		by METIS_TAC [pos_part_neg_part_borel_measurable]
hoelzl@35582
  1778
	   ++ REPEAT STRIP_TAC
hoelzl@35582
  1779
	   ++ `PREIMAGE (neg_part f) {enumerate (IMAGE (neg_part f) (space m)) i} \<inter> space m =
hoelzl@35582
  1780
		{w | w \<in> space m \<and> ((neg_part f) w = (\<lambda>w. enumerate (IMAGE (neg_part f) (space m)) i) w)}`
hoelzl@35582
  1781
		by (ONCE_REWRITE_TAC [EXTENSION] ++ RW_TAC std_ss [GSPECIFICATION, IN_INTER, IN_PREIMAGE, IN_SING]
hoelzl@35582
  1782
		    ++ DECIDE_TAC)
hoelzl@35582
  1783
	   ++ POP_ORW
hoelzl@35582
  1784
	   ++ MATCH_MP_TAC borel_measurable_eq_borel_measurable
hoelzl@35582
  1785
	   ++ METIS_TAC [borel_measurable_const, measure_space_def]);
hoelzl@35582
  1786
*)
hoelzl@35582
  1787
hoelzl@35582
  1788
end
hoelzl@35582
  1789
hoelzl@35582
  1790
end