src/HOL/Probability/Measure.thy
author hoelzl
Tue Jan 18 21:37:23 2011 +0100 (2011-01-18)
changeset 41654 32fe42892983
parent 41545 9c869baf1c66
child 41660 7795aaab6038
permissions -rw-r--r--
Gauge measure removed
hoelzl@40859
     1
(* Author: Lawrence C Paulson; Armin Heller, Johannes Hoelzl, TU Muenchen *)
paulson@33271
     2
paulson@33271
     3
theory Measure
hoelzl@38656
     4
  imports Caratheodory
paulson@33271
     5
begin
paulson@33271
     6
hoelzl@40859
     7
lemma inj_on_image_eq_iff:
hoelzl@40859
     8
  assumes "inj_on f S"
hoelzl@40859
     9
  assumes "A \<subseteq> S" "B \<subseteq> S"
hoelzl@40859
    10
  shows "(f ` A = f ` B) \<longleftrightarrow> (A = B)"
hoelzl@40859
    11
proof -
hoelzl@40859
    12
  have "inj_on f (A \<union> B)"
hoelzl@40859
    13
    using assms by (auto intro: subset_inj_on)
hoelzl@40859
    14
  from inj_on_Un_image_eq_iff[OF this]
hoelzl@40859
    15
  show ?thesis .
hoelzl@40859
    16
qed
hoelzl@40859
    17
hoelzl@40859
    18
lemma image_vimage_inter_eq:
hoelzl@40859
    19
  assumes "f ` S = T" "X \<subseteq> T"
hoelzl@40859
    20
  shows "f ` (f -` X \<inter> S) = X"
hoelzl@40859
    21
proof (intro antisym)
hoelzl@40859
    22
  have "f ` (f -` X \<inter> S) \<subseteq> f ` (f -` X)" by auto
hoelzl@40859
    23
  also have "\<dots> = X \<inter> range f" by simp
hoelzl@40859
    24
  also have "\<dots> = X" using assms by auto
hoelzl@40859
    25
  finally show "f ` (f -` X \<inter> S) \<subseteq> X" by auto
hoelzl@40859
    26
next
hoelzl@40859
    27
  show "X \<subseteq> f ` (f -` X \<inter> S)"
hoelzl@40859
    28
  proof
hoelzl@40859
    29
    fix x assume "x \<in> X"
hoelzl@40859
    30
    then have "x \<in> T" using `X \<subseteq> T` by auto
hoelzl@40859
    31
    then obtain y where "x = f y" "y \<in> S"
hoelzl@40859
    32
      using assms by auto
hoelzl@40859
    33
    then have "{y} \<subseteq> f -` X \<inter> S" using `x \<in> X` by auto
hoelzl@40859
    34
    moreover have "x \<in> f ` {y}" using `x = f y` by auto
hoelzl@40859
    35
    ultimately show "x \<in> f ` (f -` X \<inter> S)" by auto
hoelzl@40859
    36
  qed
hoelzl@40859
    37
qed
hoelzl@40859
    38
hoelzl@40859
    39
text {*
hoelzl@40859
    40
  This formalisation of measure theory is based on the work of Hurd/Coble wand
hoelzl@40859
    41
  was later translated by Lawrence Paulson to Isabelle/HOL. Later it was
hoelzl@40859
    42
  modified to use the positive infinite reals and to prove the uniqueness of
hoelzl@40859
    43
  cut stable measures.
hoelzl@40859
    44
*}
paulson@33271
    45
hoelzl@38656
    46
section {* Equations for the measure function @{text \<mu>} *}
paulson@33271
    47
hoelzl@38656
    48
lemma (in measure_space) measure_countably_additive:
hoelzl@38656
    49
  assumes "range A \<subseteq> sets M" "disjoint_family A"
hoelzl@38656
    50
  shows "psuminf (\<lambda>i. \<mu> (A i)) = \<mu> (\<Union>i. A i)"
paulson@33271
    51
proof -
hoelzl@38656
    52
  have "(\<Union> i. A i) \<in> sets M" using assms(1) by (rule countable_UN)
hoelzl@38656
    53
  with ca assms show ?thesis by (simp add: countably_additive_def)
paulson@33271
    54
qed
paulson@33271
    55
hoelzl@38656
    56
lemma (in measure_space) measure_space_cong:
hoelzl@38656
    57
  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<mu> A"
hoelzl@38656
    58
  shows "measure_space M \<nu>"
hoelzl@38656
    59
proof
hoelzl@38656
    60
  show "\<nu> {} = 0" using assms by auto
hoelzl@38656
    61
  show "countably_additive M \<nu>" unfolding countably_additive_def
hoelzl@38656
    62
  proof safe
hoelzl@38656
    63
    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A"
hoelzl@38656
    64
    then have "\<And>i. A i \<in> sets M" "(UNION UNIV A) \<in> sets M" by auto
hoelzl@38656
    65
    from this[THEN assms] measure_countably_additive[OF A]
hoelzl@38656
    66
    show "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (UNION UNIV A)" by simp
hoelzl@38656
    67
  qed
paulson@33271
    68
qed
paulson@33271
    69
hoelzl@38656
    70
lemma (in measure_space) additive: "additive M \<mu>"
hoelzl@38656
    71
proof (rule algebra.countably_additive_additive [OF _ _ ca])
hoelzl@38656
    72
  show "algebra M" by default
hoelzl@38656
    73
  show "positive \<mu>" by (simp add: positive_def)
paulson@33271
    74
qed
paulson@33271
    75
paulson@33271
    76
lemma (in measure_space) measure_additive:
hoelzl@38656
    77
     "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {}
hoelzl@38656
    78
      \<Longrightarrow> \<mu> a + \<mu> b = \<mu> (a \<union> b)"
paulson@33271
    79
  by (metis additiveD additive)
paulson@33271
    80
hoelzl@36624
    81
lemma (in measure_space) measure_mono:
hoelzl@36624
    82
  assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M"
hoelzl@38656
    83
  shows "\<mu> a \<le> \<mu> b"
hoelzl@36624
    84
proof -
hoelzl@36624
    85
  have "b = a \<union> (b - a)" using assms by auto
hoelzl@36624
    86
  moreover have "{} = a \<inter> (b - a)" by auto
hoelzl@38656
    87
  ultimately have "\<mu> b = \<mu> a + \<mu> (b - a)"
hoelzl@36624
    88
    using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto
hoelzl@38656
    89
  moreover have "\<mu> (b - a) \<ge> 0" using assms by auto
hoelzl@38656
    90
  ultimately show "\<mu> a \<le> \<mu> b" by auto
hoelzl@36624
    91
qed
hoelzl@36624
    92
hoelzl@38656
    93
lemma (in measure_space) measure_compl:
hoelzl@38656
    94
  assumes s: "s \<in> sets M" and fin: "\<mu> s \<noteq> \<omega>"
hoelzl@38656
    95
  shows "\<mu> (space M - s) = \<mu> (space M) - \<mu> s"
paulson@33271
    96
proof -
hoelzl@38656
    97
  have s_less_space: "\<mu> s \<le> \<mu> (space M)"
hoelzl@38656
    98
    using s by (auto intro!: measure_mono sets_into_space)
hoelzl@38656
    99
hoelzl@38656
   100
  have "\<mu> (space M) = \<mu> (s \<union> (space M - s))" using s
hoelzl@38656
   101
    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
hoelzl@38656
   102
  also have "... = \<mu> s + \<mu> (space M - s)"
hoelzl@38656
   103
    by (rule additiveD [OF additive]) (auto simp add: s)
hoelzl@38656
   104
  finally have "\<mu> (space M) = \<mu> s + \<mu> (space M - s)" .
paulson@33271
   105
  thus ?thesis
hoelzl@41023
   106
    unfolding minus_pextreal_eq2[OF s_less_space fin]
hoelzl@38656
   107
    by (simp add: ac_simps)
paulson@33271
   108
qed
paulson@33271
   109
hoelzl@38656
   110
lemma (in measure_space) measure_Diff:
hoelzl@38656
   111
  assumes finite: "\<mu> B \<noteq> \<omega>"
hoelzl@38656
   112
  and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
hoelzl@38656
   113
  shows "\<mu> (A - B) = \<mu> A - \<mu> B"
hoelzl@38656
   114
proof -
hoelzl@38656
   115
  have *: "(A - B) \<union> B = A" using `B \<subseteq> A` by auto
hoelzl@38656
   116
hoelzl@38656
   117
  have "\<mu> ((A - B) \<union> B) = \<mu> (A - B) + \<mu> B"
hoelzl@38656
   118
    using measurable by (rule_tac measure_additive[symmetric]) auto
hoelzl@38656
   119
  thus ?thesis unfolding * using `\<mu> B \<noteq> \<omega>`
hoelzl@41023
   120
    by (simp add: pextreal_cancel_plus_minus)
hoelzl@38656
   121
qed
paulson@33271
   122
paulson@33271
   123
lemma (in measure_space) measure_countable_increasing:
paulson@33271
   124
  assumes A: "range A \<subseteq> sets M"
paulson@33271
   125
      and A0: "A 0 = {}"
hoelzl@38656
   126
      and ASuc: "\<And>n.  A n \<subseteq> A (Suc n)"
hoelzl@38656
   127
  shows "(SUP n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
paulson@33271
   128
proof -
paulson@33271
   129
  {
paulson@33271
   130
    fix n
hoelzl@38656
   131
    have "\<mu> (A n) =
hoelzl@38656
   132
          setsum (\<mu> \<circ> (\<lambda>i. A (Suc i) - A i)) {..<n}"
paulson@33271
   133
      proof (induct n)
huffman@37032
   134
        case 0 thus ?case by (auto simp add: A0)
paulson@33271
   135
      next
hoelzl@38656
   136
        case (Suc m)
wenzelm@33536
   137
        have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
wenzelm@33536
   138
          by (metis ASuc Un_Diff_cancel Un_absorb1)
hoelzl@38656
   139
        hence "\<mu> (A (Suc m)) =
hoelzl@38656
   140
               \<mu> (A m) + \<mu> (A (Suc m) - A m)"
hoelzl@38656
   141
          by (subst measure_additive)
hoelzl@38656
   142
             (auto simp add: measure_additive range_subsetD [OF A])
wenzelm@33536
   143
        with Suc show ?case
wenzelm@33536
   144
          by simp
hoelzl@38656
   145
      qed }
hoelzl@38656
   146
  note Meq = this
paulson@33271
   147
  have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
hoelzl@38656
   148
    proof (rule UN_finite2_eq [where k=1], simp)
paulson@33271
   149
      fix i
paulson@33271
   150
      show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
wenzelm@33536
   151
        proof (induct i)
wenzelm@33536
   152
          case 0 thus ?case by (simp add: A0)
wenzelm@33536
   153
        next
hoelzl@38656
   154
          case (Suc i)
wenzelm@33536
   155
          thus ?case
wenzelm@33536
   156
            by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
wenzelm@33536
   157
        qed
paulson@33271
   158
    qed
paulson@33271
   159
  have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
paulson@33271
   160
    by (metis A Diff range_subsetD)
paulson@33271
   161
  have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
huffman@37032
   162
    by (blast intro: range_subsetD [OF A])
hoelzl@38656
   163
  have "psuminf ( (\<lambda>i. \<mu> (A (Suc i) - A i))) = \<mu> (\<Union>i. A (Suc i) - A i)"
hoelzl@38656
   164
    by (rule measure_countably_additive)
paulson@33271
   165
       (auto simp add: disjoint_family_Suc ASuc A1 A2)
hoelzl@38656
   166
  also have "... =  \<mu> (\<Union>i. A i)"
hoelzl@38656
   167
    by (simp add: Aeq)
hoelzl@38656
   168
  finally have "psuminf (\<lambda>i. \<mu> (A (Suc i) - A i)) = \<mu> (\<Union>i. A i)" .
paulson@33271
   169
  thus ?thesis
hoelzl@38656
   170
    by (auto simp add: Meq psuminf_def)
paulson@33271
   171
qed
paulson@33271
   172
hoelzl@38656
   173
lemma (in measure_space) continuity_from_below:
hoelzl@38656
   174
  assumes A: "range A \<subseteq> sets M"
hoelzl@38656
   175
      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
hoelzl@38656
   176
  shows "(SUP n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
hoelzl@38656
   177
proof -
hoelzl@38656
   178
  have *: "(SUP n. \<mu> (nat_case {} A (Suc n))) = (SUP n. \<mu> (nat_case {} A n))"
hoelzl@38656
   179
    apply (rule Sup_mono_offset_Suc)
hoelzl@38656
   180
    apply (rule measure_mono)
hoelzl@38656
   181
    using assms by (auto split: nat.split)
paulson@33271
   182
hoelzl@38656
   183
  have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)"
hoelzl@38656
   184
    by (auto simp add: split: nat.splits)
hoelzl@38656
   185
  have meq: "\<And>n. \<mu> (A n) = (\<mu> \<circ> nat_case {} A) (Suc n)"
hoelzl@38656
   186
    by simp
hoelzl@38656
   187
  have "(SUP n. \<mu> (nat_case {} A n)) = \<mu> (\<Union>i. nat_case {} A i)"
hoelzl@38656
   188
    by (rule measure_countable_increasing)
hoelzl@38656
   189
       (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits)
hoelzl@38656
   190
  also have "\<mu> (\<Union>i. nat_case {} A i) = \<mu> (\<Union>i. A i)"
hoelzl@38656
   191
    by (simp add: ueq)
hoelzl@38656
   192
  finally have "(SUP n. \<mu> (nat_case {} A n)) = \<mu> (\<Union>i. A i)" .
hoelzl@38656
   193
  thus ?thesis unfolding meq * comp_def .
paulson@33271
   194
qed
paulson@33271
   195
hoelzl@38656
   196
lemma (in measure_space) measure_up:
hoelzl@40859
   197
  assumes "\<And>i. B i \<in> sets M" "B \<up> P"
hoelzl@38656
   198
  shows "(\<lambda>i. \<mu> (B i)) \<up> \<mu> P"
hoelzl@38656
   199
  using assms unfolding isoton_def
hoelzl@38656
   200
  by (auto intro!: measure_mono continuity_from_below)
paulson@33271
   201
hoelzl@40859
   202
lemma (in measure_space) continuity_from_below':
hoelzl@40859
   203
  assumes A: "range A \<subseteq> sets M" "\<And>i. A i \<subseteq> A (Suc i)"
hoelzl@40859
   204
  shows "(\<lambda>i. (\<mu> (A i))) ----> (\<mu> (\<Union>i. A i))"
hoelzl@40859
   205
proof- let ?A = "\<Union>i. A i"
hoelzl@40859
   206
  have " (\<lambda>i. \<mu> (A i)) \<up> \<mu> ?A" apply(rule measure_up)
hoelzl@40859
   207
    using assms unfolding complete_lattice_class.isoton_def by auto
hoelzl@40859
   208
  thus ?thesis by(rule isotone_Lim(1))
hoelzl@40859
   209
qed
paulson@33271
   210
hoelzl@38656
   211
lemma (in measure_space) continuity_from_above:
hoelzl@38656
   212
  assumes A: "range A \<subseteq> sets M"
hoelzl@38656
   213
  and mono_Suc: "\<And>n.  A (Suc n) \<subseteq> A n"
hoelzl@38656
   214
  and finite: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
hoelzl@38656
   215
  shows "(INF n. \<mu> (A n)) = \<mu> (\<Inter>i. A i)"
paulson@33271
   216
proof -
hoelzl@38656
   217
  { fix n have "A n \<subseteq> A 0" using mono_Suc by (induct n) auto }
hoelzl@38656
   218
  note mono = this
hoelzl@38656
   219
hoelzl@38656
   220
  have le_MI: "\<mu> (\<Inter>i. A i) \<le> \<mu> (A 0)"
hoelzl@38656
   221
    using A by (auto intro!: measure_mono)
hoelzl@38656
   222
  hence *: "\<mu> (\<Inter>i. A i) \<noteq> \<omega>" using finite[of 0] by auto
hoelzl@38656
   223
hoelzl@38656
   224
  have le_IM: "(INF n. \<mu> (A n)) \<le> \<mu> (A 0)"
hoelzl@38656
   225
    by (rule INF_leI) simp
paulson@33271
   226
hoelzl@38656
   227
  have "\<mu> (A 0) - (INF n. \<mu> (A n)) = (SUP n. \<mu> (A 0 - A n))"
hoelzl@41023
   228
    unfolding pextreal_SUP_minus[symmetric]
hoelzl@38656
   229
    using mono A finite by (subst measure_Diff) auto
hoelzl@38656
   230
  also have "\<dots> = \<mu> (\<Union>i. A 0 - A i)"
hoelzl@38656
   231
  proof (rule continuity_from_below)
hoelzl@38656
   232
    show "range (\<lambda>n. A 0 - A n) \<subseteq> sets M"
hoelzl@38656
   233
      using A by auto
hoelzl@38656
   234
    show "\<And>n. A 0 - A n \<subseteq> A 0 - A (Suc n)"
hoelzl@38656
   235
      using mono_Suc by auto
hoelzl@38656
   236
  qed
hoelzl@38656
   237
  also have "\<dots> = \<mu> (A 0) - \<mu> (\<Inter>i. A i)"
hoelzl@38656
   238
    using mono A finite * by (simp, subst measure_Diff) auto
hoelzl@38656
   239
  finally show ?thesis
hoelzl@41023
   240
    by (rule pextreal_diff_eq_diff_imp_eq[OF finite[of 0] le_IM le_MI])
paulson@33271
   241
qed
paulson@33271
   242
hoelzl@38656
   243
lemma (in measure_space) measure_down:
hoelzl@40859
   244
  assumes "\<And>i. B i \<in> sets M" "B \<down> P"
hoelzl@38656
   245
  and finite: "\<And>i. \<mu> (B i) \<noteq> \<omega>"
hoelzl@38656
   246
  shows "(\<lambda>i. \<mu> (B i)) \<down> \<mu> P"
hoelzl@38656
   247
  using assms unfolding antiton_def
hoelzl@38656
   248
  by (auto intro!: measure_mono continuity_from_above)
hoelzl@38656
   249
lemma (in measure_space) measure_insert:
hoelzl@38656
   250
  assumes sets: "{x} \<in> sets M" "A \<in> sets M" and "x \<notin> A"
hoelzl@38656
   251
  shows "\<mu> (insert x A) = \<mu> {x} + \<mu> A"
paulson@33271
   252
proof -
hoelzl@38656
   253
  have "{x} \<inter> A = {}" using `x \<notin> A` by auto
hoelzl@38656
   254
  from measure_additive[OF sets this] show ?thesis by simp
paulson@33271
   255
qed
paulson@33271
   256
hoelzl@38656
   257
lemma (in measure_space) measure_finite_singleton:
hoelzl@38656
   258
  assumes fin: "finite S"
hoelzl@38656
   259
  and ssets: "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
hoelzl@38656
   260
  shows "\<mu> S = (\<Sum>x\<in>S. \<mu> {x})"
hoelzl@38656
   261
using assms proof induct
hoelzl@38656
   262
  case (insert x S)
hoelzl@38656
   263
  have *: "\<mu> S = (\<Sum>x\<in>S. \<mu> {x})" "{x} \<in> sets M"
hoelzl@38656
   264
    using insert.prems by (blast intro!: insert.hyps(3))+
paulson@33271
   265
hoelzl@38656
   266
  have "(\<Union>x\<in>S. {x}) \<in> sets M"
hoelzl@38656
   267
    using  insert.prems `finite S` by (blast intro!: finite_UN)
hoelzl@38656
   268
  hence "S \<in> sets M" by auto
hoelzl@38656
   269
  from measure_insert[OF `{x} \<in> sets M` this `x \<notin> S`]
hoelzl@38656
   270
  show ?case using `x \<notin> S` `finite S` * by simp
hoelzl@38656
   271
qed simp
hoelzl@35582
   272
hoelzl@35582
   273
lemma (in measure_space) measure_finitely_additive':
hoelzl@38656
   274
  assumes "f \<in> ({..< n :: nat} \<rightarrow> sets M)"
hoelzl@35582
   275
  assumes "\<And> a b. \<lbrakk>a < n ; b < n ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
hoelzl@38656
   276
  assumes "s = \<Union> (f ` {..< n})"
hoelzl@38656
   277
  shows "(\<Sum>i<n. (\<mu> \<circ> f) i) = \<mu> s"
hoelzl@35582
   278
proof -
hoelzl@35582
   279
  def f' == "\<lambda> i. (if i < n then f i else {})"
hoelzl@38656
   280
  have rf: "range f' \<subseteq> sets M" unfolding f'_def
hoelzl@35582
   281
    using assms empty_sets by auto
hoelzl@38656
   282
  have df: "disjoint_family f'" unfolding f'_def disjoint_family_on_def
hoelzl@35582
   283
    using assms by simp
hoelzl@38656
   284
  have "\<Union> range f' = (\<Union> i \<in> {..< n}. f i)"
hoelzl@35582
   285
    unfolding f'_def by auto
hoelzl@38656
   286
  then have "\<mu> s = \<mu> (\<Union> range f')"
hoelzl@35582
   287
    using assms by simp
hoelzl@38656
   288
  then have part1: "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = \<mu> s"
hoelzl@35582
   289
    using df rf ca[unfolded countably_additive_def, rule_format, of f']
hoelzl@35582
   290
    by auto
hoelzl@35582
   291
hoelzl@38656
   292
  have "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = (\<Sum> i< n. \<mu> (f' i))"
hoelzl@38656
   293
    by (rule psuminf_finite) (simp add: f'_def)
hoelzl@38656
   294
  also have "\<dots> = (\<Sum>i<n. \<mu> (f i))"
hoelzl@35582
   295
    unfolding f'_def by auto
hoelzl@38656
   296
  finally have part2: "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = (\<Sum>i<n. \<mu> (f i))" by simp
hoelzl@38656
   297
  show ?thesis using part1 part2 by auto
hoelzl@35582
   298
qed
hoelzl@35582
   299
hoelzl@35582
   300
hoelzl@35582
   301
lemma (in measure_space) measure_finitely_additive:
hoelzl@35582
   302
  assumes "finite r"
hoelzl@35582
   303
  assumes "r \<subseteq> sets M"
hoelzl@35582
   304
  assumes d: "\<And> a b. \<lbrakk>a \<in> r ; b \<in> r ; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
hoelzl@38656
   305
  shows "(\<Sum> i \<in> r. \<mu> i) = \<mu> (\<Union> r)"
hoelzl@35582
   306
using assms
hoelzl@35582
   307
proof -
hoelzl@35582
   308
  (* counting the elements in r is enough *)
hoelzl@38656
   309
  let ?R = "{..<card r}"
hoelzl@35582
   310
  obtain f where f: "f ` ?R = r" "inj_on f ?R"
hoelzl@35582
   311
    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite r`]
hoelzl@38656
   312
    unfolding atLeast0LessThan by auto
hoelzl@35582
   313
  hence f_into_sets: "f \<in> ?R \<rightarrow> sets M" using assms by auto
hoelzl@35582
   314
  have disj: "\<And> a b. \<lbrakk>a \<in> ?R ; b \<in> ?R ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
hoelzl@35582
   315
  proof -
hoelzl@35582
   316
    fix a b assume asm: "a \<in> ?R" "b \<in> ?R" "a \<noteq> b"
hoelzl@35582
   317
    hence neq: "f a \<noteq> f b" using f[unfolded inj_on_def, rule_format] by blast
hoelzl@35582
   318
    from asm have "f a \<in> r" "f b \<in> r" using f by auto
hoelzl@35582
   319
    thus "f a \<inter> f b = {}" using d[of "f a" "f b"] f using neq by auto
hoelzl@35582
   320
  qed
hoelzl@35582
   321
  have "(\<Union> r) = (\<Union> i \<in> ?R. f i)"
hoelzl@35582
   322
    using f by auto
hoelzl@38656
   323
  hence "\<mu> (\<Union> r)= \<mu> (\<Union> i \<in> ?R. f i)" by simp
hoelzl@38656
   324
  also have "\<dots> = (\<Sum> i \<in> ?R. \<mu> (f i))"
hoelzl@35582
   325
    using measure_finitely_additive'[OF f_into_sets disj] by simp
hoelzl@38656
   326
  also have "\<dots> = (\<Sum> a \<in> r. \<mu> a)"
hoelzl@38656
   327
    using f[rule_format] setsum_reindex[of f ?R "\<lambda> a. \<mu> a"] by auto
hoelzl@35582
   328
  finally show ?thesis by simp
hoelzl@35582
   329
qed
hoelzl@35582
   330
hoelzl@35582
   331
lemma (in measure_space) measure_finitely_additive'':
hoelzl@35582
   332
  assumes "finite s"
hoelzl@35582
   333
  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<in> sets M"
hoelzl@35582
   334
  assumes d: "disjoint_family_on a s"
hoelzl@38656
   335
  shows "(\<Sum> i \<in> s. \<mu> (a i)) = \<mu> (\<Union> i \<in> s. a i)"
hoelzl@35582
   336
using assms
hoelzl@35582
   337
proof -
hoelzl@35582
   338
  (* counting the elements in s is enough *)
hoelzl@38656
   339
  let ?R = "{..< card s}"
hoelzl@35582
   340
  obtain f where f: "f ` ?R = s" "inj_on f ?R"
hoelzl@35582
   341
    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite s`]
hoelzl@38656
   342
    unfolding atLeast0LessThan by auto
hoelzl@35582
   343
  hence f_into_sets: "a \<circ> f \<in> ?R \<rightarrow> sets M" using assms unfolding o_def by auto
hoelzl@35582
   344
  have disj: "\<And> i j. \<lbrakk>i \<in> ?R ; j \<in> ?R ; i \<noteq> j\<rbrakk> \<Longrightarrow> (a \<circ> f) i \<inter> (a \<circ> f) j = {}"
hoelzl@35582
   345
  proof -
hoelzl@35582
   346
    fix i j assume asm: "i \<in> ?R" "j \<in> ?R" "i \<noteq> j"
hoelzl@35582
   347
    hence neq: "f i \<noteq> f j" using f[unfolded inj_on_def, rule_format] by blast
hoelzl@35582
   348
    from asm have "f i \<in> s" "f j \<in> s" using f by auto
hoelzl@35582
   349
    thus "(a \<circ> f) i \<inter> (a \<circ> f) j = {}"
hoelzl@35582
   350
      using d f neq unfolding disjoint_family_on_def by auto
hoelzl@35582
   351
  qed
hoelzl@35582
   352
  have "(\<Union> i \<in> s. a i) = (\<Union> i \<in> f ` ?R. a i)" using f by auto
hoelzl@35582
   353
  hence "(\<Union> i \<in> s. a i) = (\<Union> i \<in> ?R. a (f i))" by auto
hoelzl@38656
   354
  hence "\<mu> (\<Union> i \<in> s. a i) = (\<Sum> i \<in> ?R. \<mu> (a (f i)))"
hoelzl@35582
   355
    using measure_finitely_additive'[OF f_into_sets disj] by simp
hoelzl@38656
   356
  also have "\<dots> = (\<Sum> i \<in> s. \<mu> (a i))"
hoelzl@38656
   357
    using f[rule_format] setsum_reindex[of f ?R "\<lambda> i. \<mu> (a i)"] by auto
hoelzl@35582
   358
  finally show ?thesis by simp
hoelzl@35582
   359
qed
hoelzl@35582
   360
paulson@33271
   361
lemma (in sigma_algebra) finite_additivity_sufficient:
hoelzl@38656
   362
  assumes fin: "finite (space M)" and pos: "positive \<mu>" and add: "additive M \<mu>"
hoelzl@38656
   363
  shows "measure_space M \<mu>"
hoelzl@38656
   364
proof
hoelzl@38656
   365
  show [simp]: "\<mu> {} = 0" using pos by (simp add: positive_def)
hoelzl@38656
   366
  show "countably_additive M \<mu>"
hoelzl@38656
   367
    proof (auto simp add: countably_additive_def)
paulson@33271
   368
      fix A :: "nat \<Rightarrow> 'a set"
hoelzl@38656
   369
      assume A: "range A \<subseteq> sets M"
paulson@33271
   370
         and disj: "disjoint_family A"
hoelzl@38656
   371
         and UnA: "(\<Union>i. A i) \<in> sets M"
paulson@33271
   372
      def I \<equiv> "{i. A i \<noteq> {}}"
paulson@33271
   373
      have "Union (A ` I) \<subseteq> space M" using A
hoelzl@38656
   374
        by auto (metis range_subsetD subsetD sets_into_space)
paulson@33271
   375
      hence "finite (A ` I)"
hoelzl@38656
   376
        by (metis finite_UnionD finite_subset fin)
paulson@33271
   377
      moreover have "inj_on A I" using disj
hoelzl@38656
   378
        by (auto simp add: I_def disjoint_family_on_def inj_on_def)
paulson@33271
   379
      ultimately have finI: "finite I"
paulson@33271
   380
        by (metis finite_imageD)
paulson@33271
   381
      hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
paulson@33271
   382
        proof (cases "I = {}")
hoelzl@38656
   383
          case True thus ?thesis by (simp add: I_def)
paulson@33271
   384
        next
paulson@33271
   385
          case False
paulson@33271
   386
          hence "\<forall>i\<in>I. i < Suc(Max I)"
hoelzl@38656
   387
            by (simp add: Max_less_iff [symmetric] finI)
paulson@33271
   388
          hence "\<forall>m \<ge> Suc(Max I). A m = {}"
hoelzl@38656
   389
            by (simp add: I_def) (metis less_le_not_le)
paulson@33271
   390
          thus ?thesis
paulson@33271
   391
            by blast
paulson@33271
   392
        qed
paulson@33271
   393
      then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast
hoelzl@38656
   394
      then have "\<forall>m\<ge>N. \<mu> (A m) = 0" by simp
hoelzl@38656
   395
      then have "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = setsum (\<lambda>m. \<mu> (A m)) {..<N}"
hoelzl@38656
   396
        by (simp add: psuminf_finite)
hoelzl@38656
   397
      also have "... = \<mu> (\<Union>i<N. A i)"
paulson@33271
   398
        proof (induct N)
paulson@33271
   399
          case 0 thus ?case by simp
paulson@33271
   400
        next
hoelzl@38656
   401
          case (Suc n)
hoelzl@38656
   402
          have "\<mu> (A n \<union> (\<Union> x<n. A x)) = \<mu> (A n) + \<mu> (\<Union> i<n. A i)"
hoelzl@38656
   403
            proof (rule Caratheodory.additiveD [OF add])
paulson@33271
   404
              show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
hoelzl@35582
   405
                by (auto simp add: disjoint_family_on_def nat_less_le) blast
hoelzl@38656
   406
              show "A n \<in> sets M" using A
hoelzl@38656
   407
                by force
paulson@33271
   408
              show "(\<Union>i<n. A i) \<in> sets M"
paulson@33271
   409
                proof (induct n)
paulson@33271
   410
                  case 0 thus ?case by simp
paulson@33271
   411
                next
paulson@33271
   412
                  case (Suc n) thus ?case using A
hoelzl@38656
   413
                    by (simp add: lessThan_Suc Un range_subsetD)
paulson@33271
   414
                qed
paulson@33271
   415
            qed
paulson@33271
   416
          thus ?case using Suc
hoelzl@38656
   417
            by (simp add: lessThan_Suc)
paulson@33271
   418
        qed
hoelzl@38656
   419
      also have "... = \<mu> (\<Union>i. A i)"
paulson@33271
   420
        proof -
paulson@33271
   421
          have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N
paulson@33271
   422
            by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE)
paulson@33271
   423
          thus ?thesis by simp
paulson@33271
   424
        qed
hoelzl@38656
   425
      finally show "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" .
paulson@33271
   426
    qed
paulson@33271
   427
qed
paulson@33271
   428
hoelzl@35692
   429
lemma (in measure_space) measure_setsum_split:
hoelzl@35692
   430
  assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
hoelzl@35692
   431
  assumes "(\<Union>i \<in> r. b i) = space M"
hoelzl@35692
   432
  assumes "disjoint_family_on b r"
hoelzl@38656
   433
  shows "\<mu> a = (\<Sum> i \<in> r. \<mu> (a \<inter> (b i)))"
hoelzl@35692
   434
proof -
hoelzl@38656
   435
  have *: "\<mu> a = \<mu> (\<Union>i \<in> r. a \<inter> b i)"
hoelzl@35692
   436
    using assms by auto
hoelzl@35692
   437
  show ?thesis unfolding *
hoelzl@35692
   438
  proof (rule measure_finitely_additive''[symmetric])
hoelzl@35692
   439
    show "finite r" using `finite r` by auto
hoelzl@35692
   440
    { fix i assume "i \<in> r"
hoelzl@35692
   441
      hence "b i \<in> sets M" using br_in_M by auto
hoelzl@35692
   442
      thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
hoelzl@35692
   443
    }
hoelzl@35692
   444
    show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
hoelzl@35692
   445
      using `disjoint_family_on b r`
hoelzl@35692
   446
      unfolding disjoint_family_on_def by auto
hoelzl@35692
   447
  qed
hoelzl@35692
   448
qed
hoelzl@35692
   449
hoelzl@38656
   450
lemma (in measure_space) measure_subadditive:
hoelzl@38656
   451
  assumes measurable: "A \<in> sets M" "B \<in> sets M"
hoelzl@38656
   452
  shows "\<mu> (A \<union> B) \<le> \<mu> A + \<mu> B"
hoelzl@38656
   453
proof -
hoelzl@38656
   454
  from measure_additive[of A "B - A"]
hoelzl@38656
   455
  have "\<mu> (A \<union> B) = \<mu> A + \<mu> (B - A)"
hoelzl@38656
   456
    using assms by (simp add: Diff)
hoelzl@38656
   457
  also have "\<dots> \<le> \<mu> A + \<mu> B"
hoelzl@38656
   458
    using assms by (auto intro!: add_left_mono measure_mono)
hoelzl@38656
   459
  finally show ?thesis .
hoelzl@38656
   460
qed
hoelzl@38656
   461
hoelzl@40859
   462
lemma (in measure_space) measure_eq_0:
hoelzl@40859
   463
  assumes "N \<in> sets M" and "\<mu> N = 0" and "K \<subseteq> N" and "K \<in> sets M"
hoelzl@40859
   464
  shows "\<mu> K = 0"
hoelzl@40859
   465
using measure_mono[OF assms(3,4,1)] assms(2) by auto
hoelzl@40859
   466
hoelzl@39092
   467
lemma (in measure_space) measure_finitely_subadditive:
hoelzl@39092
   468
  assumes "finite I" "A ` I \<subseteq> sets M"
hoelzl@39092
   469
  shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))"
hoelzl@39092
   470
using assms proof induct
hoelzl@39092
   471
  case (insert i I)
hoelzl@39092
   472
  then have "(\<Union>i\<in>I. A i) \<in> sets M" by (auto intro: finite_UN)
hoelzl@39092
   473
  then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)"
hoelzl@39092
   474
    using insert by (simp add: measure_subadditive)
hoelzl@39092
   475
  also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))"
hoelzl@39092
   476
    using insert by (auto intro!: add_left_mono)
hoelzl@39092
   477
  finally show ?case .
hoelzl@39092
   478
qed simp
hoelzl@39092
   479
hoelzl@40859
   480
lemma (in measure_space) measure_countably_subadditive:
hoelzl@38656
   481
  assumes "range f \<subseteq> sets M"
hoelzl@38656
   482
  shows "\<mu> (\<Union>i. f i) \<le> (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))"
hoelzl@38656
   483
proof -
hoelzl@38656
   484
  have "\<mu> (\<Union>i. f i) = \<mu> (\<Union>i. disjointed f i)"
hoelzl@38656
   485
    unfolding UN_disjointed_eq ..
hoelzl@38656
   486
  also have "\<dots> = (\<Sum>\<^isub>\<infinity> i. \<mu> (disjointed f i))"
hoelzl@38656
   487
    using range_disjointed_sets[OF assms] measure_countably_additive
hoelzl@38656
   488
    by (simp add:  disjoint_family_disjointed comp_def)
hoelzl@38656
   489
  also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))"
hoelzl@38656
   490
  proof (rule psuminf_le, rule measure_mono)
hoelzl@38656
   491
    fix i show "disjointed f i \<subseteq> f i" by (rule disjointed_subset)
hoelzl@38656
   492
    show "f i \<in> sets M" "disjointed f i \<in> sets M"
hoelzl@38656
   493
      using assms range_disjointed_sets[OF assms] by auto
hoelzl@38656
   494
  qed
hoelzl@38656
   495
  finally show ?thesis .
hoelzl@38656
   496
qed
hoelzl@38656
   497
hoelzl@40859
   498
lemma (in measure_space) measure_UN_eq_0:
hoelzl@40859
   499
  assumes "\<And> i :: nat. \<mu> (N i) = 0" and "range N \<subseteq> sets M"
hoelzl@40859
   500
  shows "\<mu> (\<Union> i. N i) = 0"
hoelzl@40859
   501
using measure_countably_subadditive[OF assms(2)] assms(1) by auto
hoelzl@40859
   502
hoelzl@39092
   503
lemma (in measure_space) measure_inter_full_set:
hoelzl@39092
   504
  assumes "S \<in> sets M" "T \<in> sets M" and not_\<omega>: "\<mu> (T - S) \<noteq> \<omega>"
hoelzl@39092
   505
  assumes T: "\<mu> T = \<mu> (space M)"
hoelzl@39092
   506
  shows "\<mu> (S \<inter> T) = \<mu> S"
hoelzl@39092
   507
proof (rule antisym)
hoelzl@39092
   508
  show " \<mu> (S \<inter> T) \<le> \<mu> S"
hoelzl@39092
   509
    using assms by (auto intro!: measure_mono)
hoelzl@39092
   510
hoelzl@39092
   511
  show "\<mu> S \<le> \<mu> (S \<inter> T)"
hoelzl@39092
   512
  proof (rule ccontr)
hoelzl@39092
   513
    assume contr: "\<not> ?thesis"
hoelzl@39092
   514
    have "\<mu> (space M) = \<mu> ((T - S) \<union> (S \<inter> T))"
hoelzl@39092
   515
      unfolding T[symmetric] by (auto intro!: arg_cong[where f="\<mu>"])
hoelzl@39092
   516
    also have "\<dots> \<le> \<mu> (T - S) + \<mu> (S \<inter> T)"
hoelzl@39092
   517
      using assms by (auto intro!: measure_subadditive)
hoelzl@39092
   518
    also have "\<dots> < \<mu> (T - S) + \<mu> S"
hoelzl@41023
   519
      by (rule pextreal_less_add[OF not_\<omega>]) (insert contr, auto)
hoelzl@39092
   520
    also have "\<dots> = \<mu> (T \<union> S)"
hoelzl@39092
   521
      using assms by (subst measure_additive) auto
hoelzl@39092
   522
    also have "\<dots> \<le> \<mu> (space M)"
hoelzl@39092
   523
      using assms sets_into_space by (auto intro!: measure_mono)
hoelzl@39092
   524
    finally show False ..
hoelzl@39092
   525
  qed
hoelzl@39092
   526
qed
hoelzl@39092
   527
hoelzl@40859
   528
lemma measure_unique_Int_stable:
hoelzl@40859
   529
  fixes M E :: "'a algebra" and A :: "nat \<Rightarrow> 'a set"
hoelzl@40859
   530
  assumes "Int_stable E" "M = sigma E"
hoelzl@40859
   531
  and A: "range  A \<subseteq> sets E" "A \<up> space E"
hoelzl@40859
   532
  and ms: "measure_space M \<mu>" "measure_space M \<nu>"
hoelzl@40859
   533
  and eq: "\<And>X. X \<in> sets E \<Longrightarrow> \<mu> X = \<nu> X"
hoelzl@40859
   534
  and finite: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
hoelzl@40859
   535
  assumes "X \<in> sets M"
hoelzl@40859
   536
  shows "\<mu> X = \<nu> X"
hoelzl@40859
   537
proof -
hoelzl@40859
   538
  let "?D F" = "{D. D \<in> sets M \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}"
hoelzl@40859
   539
  interpret M: measure_space M \<mu> by fact
hoelzl@40859
   540
  interpret M': measure_space M \<nu> by fact
hoelzl@40859
   541
  have "space E = space M"
hoelzl@40859
   542
    using `M = sigma E` by simp
hoelzl@40859
   543
  have sets_E: "sets E \<subseteq> Pow (space E)"
hoelzl@40859
   544
  proof
hoelzl@40859
   545
    fix X assume "X \<in> sets E"
hoelzl@40859
   546
    then have "X \<in> sets M" unfolding `M = sigma E`
hoelzl@40859
   547
      unfolding sigma_def by (auto intro!: sigma_sets.Basic)
hoelzl@40859
   548
    with M.sets_into_space show "X \<in> Pow (space E)"
hoelzl@40859
   549
      unfolding `space E = space M` by auto
hoelzl@40859
   550
  qed
hoelzl@40859
   551
  have A': "range A \<subseteq> sets M" using `M = sigma E` A
hoelzl@40859
   552
    by (auto simp: sets_sigma intro!: sigma_sets.Basic)
hoelzl@40859
   553
  { fix F assume "F \<in> sets E" and "\<mu> F \<noteq> \<omega>"
hoelzl@40859
   554
    then have [intro]: "F \<in> sets M" unfolding `M = sigma E` sets_sigma
hoelzl@40859
   555
      by (intro sigma_sets.Basic)
hoelzl@40859
   556
    have "\<nu> F \<noteq> \<omega>" using `\<mu> F \<noteq> \<omega>` `F \<in> sets E` eq by simp
hoelzl@40859
   557
    interpret D: dynkin_system "\<lparr>space=space E, sets=?D F\<rparr>"
hoelzl@40859
   558
    proof (rule dynkin_systemI, simp_all)
hoelzl@40859
   559
      fix A assume "A \<in> sets M \<and> \<mu> (F \<inter> A) = \<nu> (F \<inter> A)"
hoelzl@40859
   560
      then show "A \<subseteq> space E"
hoelzl@40859
   561
        unfolding `space E = space M` using M.sets_into_space by auto
hoelzl@40859
   562
    next
hoelzl@40859
   563
      have "F \<inter> space E = F" using `F \<in> sets E` sets_E by auto
hoelzl@40859
   564
      then show "space E \<in> sets M \<and> \<mu> (F \<inter> space E) = \<nu> (F \<inter> space E)"
hoelzl@40859
   565
        unfolding `space E = space M` using `F \<in> sets E` eq by auto
hoelzl@40859
   566
    next
hoelzl@40859
   567
      fix A assume *: "A \<in> sets M \<and> \<mu> (F \<inter> A) = \<nu> (F \<inter> A)"
hoelzl@40859
   568
      then have **: "F \<inter> (space M - A) = F - (F \<inter> A)"
hoelzl@40859
   569
        and [intro]: "F \<inter> A \<in> sets M"
hoelzl@40859
   570
        using `F \<in> sets E` sets_E `space E = space M` by auto
hoelzl@40859
   571
      have "\<nu> (F \<inter> A) \<le> \<nu> F" by (auto intro!: M'.measure_mono)
hoelzl@40859
   572
      then have "\<nu> (F \<inter> A) \<noteq> \<omega>" using `\<nu> F \<noteq> \<omega>` by auto
hoelzl@40859
   573
      have "\<mu> (F \<inter> A) \<le> \<mu> F" by (auto intro!: M.measure_mono)
hoelzl@40859
   574
      then have "\<mu> (F \<inter> A) \<noteq> \<omega>" using `\<mu> F \<noteq> \<omega>` by auto
hoelzl@40859
   575
      then have "\<mu> (F \<inter> (space M - A)) = \<mu> F - \<mu> (F \<inter> A)" unfolding **
hoelzl@40859
   576
        using `F \<inter> A \<in> sets M` by (auto intro!: M.measure_Diff)
hoelzl@40859
   577
      also have "\<dots> = \<nu> F - \<nu> (F \<inter> A)" using eq `F \<in> sets E` * by simp
hoelzl@40859
   578
      also have "\<dots> = \<nu> (F \<inter> (space M - A))" unfolding **
hoelzl@40859
   579
        using `F \<inter> A \<in> sets M` `\<nu> (F \<inter> A) \<noteq> \<omega>` by (auto intro!: M'.measure_Diff[symmetric])
hoelzl@40859
   580
      finally show "space E - A \<in> sets M \<and> \<mu> (F \<inter> (space E - A)) = \<nu> (F \<inter> (space E - A))"
hoelzl@40859
   581
        using `space E = space M` * by auto
hoelzl@40859
   582
    next
hoelzl@40859
   583
      fix A :: "nat \<Rightarrow> 'a set"
hoelzl@40859
   584
      assume "disjoint_family A" "range A \<subseteq> {X \<in> sets M. \<mu> (F \<inter> X) = \<nu> (F \<inter> X)}"
hoelzl@40859
   585
      then have A: "range (\<lambda>i. F \<inter> A i) \<subseteq> sets M" "F \<inter> (\<Union>x. A x) = (\<Union>x. F \<inter> A x)"
hoelzl@40859
   586
        "disjoint_family (\<lambda>i. F \<inter> A i)" "\<And>i. \<mu> (F \<inter> A i) = \<nu> (F \<inter> A i)" "range A \<subseteq> sets M"
hoelzl@40859
   587
        by ((fastsimp simp: disjoint_family_on_def)+)
hoelzl@40859
   588
      then show "(\<Union>x. A x) \<in> sets M \<and> \<mu> (F \<inter> (\<Union>x. A x)) = \<nu> (F \<inter> (\<Union>x. A x))"
hoelzl@40859
   589
        by (auto simp: M.measure_countably_additive[symmetric]
hoelzl@40859
   590
                       M'.measure_countably_additive[symmetric]
hoelzl@40859
   591
            simp del: UN_simps)
hoelzl@40859
   592
    qed
hoelzl@40859
   593
    have *: "sigma E = \<lparr>space = space E, sets = ?D F\<rparr>"
hoelzl@40859
   594
      using `M = sigma E` `F \<in> sets E` `Int_stable E`
hoelzl@40859
   595
      by (intro D.dynkin_lemma)
hoelzl@40859
   596
         (auto simp add: sets_sigma Int_stable_def eq intro: sigma_sets.Basic)
hoelzl@40859
   597
    have "\<And>D. D \<in> sets M \<Longrightarrow> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)"
hoelzl@40859
   598
      unfolding `M = sigma E` by (auto simp: *) }
hoelzl@40859
   599
  note * = this
hoelzl@40859
   600
  { fix i have "\<mu> (A i \<inter> X) = \<nu> (A i \<inter> X)"
hoelzl@40859
   601
      using *[of "A i" X] `X \<in> sets M` A finite by auto }
hoelzl@40859
   602
  moreover
hoelzl@40859
   603
  have "(\<lambda>i. A i \<inter> X) \<up> X"
hoelzl@40859
   604
    using `X \<in> sets M` M.sets_into_space A `space E = space M`
hoelzl@40859
   605
    by (auto simp: isoton_def)
hoelzl@40859
   606
  then have "(\<lambda>i. \<mu> (A i \<inter> X)) \<up> \<mu> X" "(\<lambda>i. \<nu> (A i \<inter> X)) \<up> \<nu> X"
hoelzl@40859
   607
    using `X \<in> sets M` A' by (auto intro!: M.measure_up M'.measure_up M.Int)
hoelzl@40859
   608
  ultimately show ?thesis by (simp add: isoton_def)
hoelzl@40859
   609
qed
hoelzl@40859
   610
hoelzl@40859
   611
section "Isomorphisms between measure spaces"
hoelzl@40859
   612
hoelzl@40859
   613
lemma (in measure_space) measure_space_isomorphic:
hoelzl@40859
   614
  fixes f :: "'c \<Rightarrow> 'a"
hoelzl@40859
   615
  assumes "bij_betw f S (space M)"
hoelzl@40859
   616
  shows "measure_space (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
hoelzl@40859
   617
    (is "measure_space ?T ?\<mu>")
hoelzl@40859
   618
proof -
hoelzl@40859
   619
  have "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto
hoelzl@40859
   620
  then interpret T: sigma_algebra ?T by (rule sigma_algebra_vimage)
hoelzl@40859
   621
  show ?thesis
hoelzl@40859
   622
  proof
hoelzl@40859
   623
    show "\<mu> (f`{}) = 0" by simp
hoelzl@40859
   624
    show "countably_additive ?T (\<lambda>A. \<mu> (f ` A))"
hoelzl@40859
   625
    proof (unfold countably_additive_def, intro allI impI)
hoelzl@40859
   626
      fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets ?T" "disjoint_family A"
hoelzl@40859
   627
      then have "\<forall>i. \<exists>F'. F' \<in> sets M \<and> A i = f -` F' \<inter> S"
hoelzl@40859
   628
        by (auto simp: image_iff image_subset_iff Bex_def vimage_algebra_def)
hoelzl@40859
   629
      from choice[OF this] obtain F where F: "\<And>i. F i \<in> sets M" and A: "\<And>i. A i = f -` F i \<inter> S" by auto
hoelzl@40859
   630
      then have [simp]: "\<And>i. f ` (A i) = F i"
hoelzl@40859
   631
        using sets_into_space assms
hoelzl@40859
   632
        by (force intro!: image_vimage_inter_eq[where T="space M"] simp: bij_betw_def)
hoelzl@40859
   633
      have "disjoint_family F"
hoelzl@40859
   634
      proof (intro disjoint_family_on_bisimulation[OF `disjoint_family A`])
hoelzl@40859
   635
        fix n m assume "A n \<inter> A m = {}"
hoelzl@40859
   636
        then have "f -` (F n \<inter> F m) \<inter> S = {}" unfolding A by auto
hoelzl@40859
   637
        moreover
hoelzl@40859
   638
        have "F n \<in> sets M" "F m \<in> sets M" using F by auto
hoelzl@40859
   639
        then have "f`S = space M" "F n \<inter> F m \<subseteq> space M"
hoelzl@40859
   640
          using sets_into_space assms by (auto simp: bij_betw_def)
hoelzl@40859
   641
        note image_vimage_inter_eq[OF this, symmetric]
hoelzl@40859
   642
        ultimately show "F n \<inter> F m = {}" by simp
hoelzl@40859
   643
      qed
hoelzl@40859
   644
      with F show "(\<Sum>\<^isub>\<infinity> i. \<mu> (f ` A i)) = \<mu> (f ` (\<Union>i. A i))"
hoelzl@40859
   645
        by (auto simp add: image_UN intro!: measure_countably_additive)
hoelzl@40859
   646
    qed
hoelzl@40859
   647
  qed
hoelzl@40859
   648
qed
hoelzl@40859
   649
hoelzl@40859
   650
section "@{text \<mu>}-null sets"
hoelzl@40859
   651
hoelzl@40859
   652
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}"
hoelzl@40859
   653
hoelzl@40859
   654
lemma (in measure_space) null_sets_Un[intro]:
hoelzl@40859
   655
  assumes "N \<in> null_sets" "N' \<in> null_sets"
hoelzl@40859
   656
  shows "N \<union> N' \<in> null_sets"
hoelzl@40859
   657
proof (intro conjI CollectI)
hoelzl@40859
   658
  show "N \<union> N' \<in> sets M" using assms by auto
hoelzl@40859
   659
  have "\<mu> (N \<union> N') \<le> \<mu> N + \<mu> N'"
hoelzl@40859
   660
    using assms by (intro measure_subadditive) auto
hoelzl@40859
   661
  then show "\<mu> (N \<union> N') = 0"
hoelzl@40859
   662
    using assms by auto
hoelzl@40859
   663
qed
hoelzl@40859
   664
hoelzl@40859
   665
lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
hoelzl@40859
   666
proof -
hoelzl@40859
   667
  have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
hoelzl@40859
   668
    unfolding SUPR_def image_compose
hoelzl@40859
   669
    unfolding surj_from_nat ..
hoelzl@40859
   670
  then show ?thesis by simp
hoelzl@40859
   671
qed
hoelzl@40859
   672
hoelzl@40859
   673
lemma (in measure_space) null_sets_UN[intro]:
hoelzl@40859
   674
  assumes "\<And>i::'i::countable. N i \<in> null_sets"
hoelzl@40859
   675
  shows "(\<Union>i. N i) \<in> null_sets"
hoelzl@40859
   676
proof (intro conjI CollectI)
hoelzl@40859
   677
  show "(\<Union>i. N i) \<in> sets M" using assms by auto
hoelzl@40859
   678
  have "\<mu> (\<Union>i. N i) \<le> (\<Sum>\<^isub>\<infinity> n. \<mu> (N (Countable.from_nat n)))"
hoelzl@40859
   679
    unfolding UN_from_nat[of N]
hoelzl@40859
   680
    using assms by (intro measure_countably_subadditive) auto
hoelzl@40859
   681
  then show "\<mu> (\<Union>i. N i) = 0"
hoelzl@40859
   682
    using assms by auto
hoelzl@40859
   683
qed
hoelzl@40859
   684
hoelzl@40871
   685
lemma (in measure_space) null_sets_finite_UN:
hoelzl@40871
   686
  assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets"
hoelzl@40871
   687
  shows "(\<Union>i\<in>S. A i) \<in> null_sets"
hoelzl@40871
   688
proof (intro CollectI conjI)
hoelzl@40871
   689
  show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto
hoelzl@40871
   690
  have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))"
hoelzl@40871
   691
    using assms by (intro measure_finitely_subadditive) auto
hoelzl@40871
   692
  then show "\<mu> (\<Union>i\<in>S. A i) = 0"
hoelzl@40871
   693
    using assms by auto
hoelzl@40871
   694
qed
hoelzl@40871
   695
hoelzl@40859
   696
lemma (in measure_space) null_set_Int1:
hoelzl@40859
   697
  assumes "B \<in> null_sets" "A \<in> sets M" shows "A \<inter> B \<in> null_sets"
hoelzl@40859
   698
using assms proof (intro CollectI conjI)
hoelzl@40859
   699
  show "\<mu> (A \<inter> B) = 0" using assms by (intro measure_eq_0[of B "A \<inter> B"]) auto
hoelzl@40859
   700
qed auto
hoelzl@40859
   701
hoelzl@40859
   702
lemma (in measure_space) null_set_Int2:
hoelzl@40859
   703
  assumes "B \<in> null_sets" "A \<in> sets M" shows "B \<inter> A \<in> null_sets"
hoelzl@40859
   704
  using assms by (subst Int_commute) (rule null_set_Int1)
hoelzl@40859
   705
hoelzl@40859
   706
lemma (in measure_space) measure_Diff_null_set:
hoelzl@40859
   707
  assumes "B \<in> null_sets" "A \<in> sets M"
hoelzl@40859
   708
  shows "\<mu> (A - B) = \<mu> A"
hoelzl@40859
   709
proof -
hoelzl@40859
   710
  have *: "A - B = (A - (A \<inter> B))" by auto
hoelzl@40859
   711
  have "A \<inter> B \<in> null_sets" using assms by (rule null_set_Int1)
hoelzl@40859
   712
  then show ?thesis
hoelzl@40859
   713
    unfolding * using assms
hoelzl@40859
   714
    by (subst measure_Diff) auto
hoelzl@40859
   715
qed
hoelzl@40859
   716
hoelzl@40859
   717
lemma (in measure_space) null_set_Diff:
hoelzl@40859
   718
  assumes "B \<in> null_sets" "A \<in> sets M" shows "B - A \<in> null_sets"
hoelzl@40859
   719
using assms proof (intro CollectI conjI)
hoelzl@40859
   720
  show "\<mu> (B - A) = 0" using assms by (intro measure_eq_0[of B "B - A"]) auto
hoelzl@40859
   721
qed auto
hoelzl@40859
   722
hoelzl@40859
   723
lemma (in measure_space) measure_Un_null_set:
hoelzl@40859
   724
  assumes "A \<in> sets M" "B \<in> null_sets"
hoelzl@40859
   725
  shows "\<mu> (A \<union> B) = \<mu> A"
hoelzl@40859
   726
proof -
hoelzl@40859
   727
  have *: "A \<union> B = A \<union> (B - A)" by auto
hoelzl@40859
   728
  have "B - A \<in> null_sets" using assms(2,1) by (rule null_set_Diff)
hoelzl@40859
   729
  then show ?thesis
hoelzl@40859
   730
    unfolding * using assms
hoelzl@40859
   731
    by (subst measure_additive[symmetric]) auto
hoelzl@40859
   732
qed
hoelzl@40859
   733
hoelzl@40871
   734
section "Formalise almost everywhere"
hoelzl@40871
   735
hoelzl@40871
   736
definition (in measure_space)
hoelzl@40871
   737
  almost_everywhere :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "AE " 10) where
hoelzl@40871
   738
  "almost_everywhere P \<longleftrightarrow> (\<exists>N\<in>null_sets. { x \<in> space M. \<not> P x } \<subseteq> N)"
hoelzl@40871
   739
hoelzl@40871
   740
lemma (in measure_space) AE_I':
hoelzl@40871
   741
  "N \<in> null_sets \<Longrightarrow> {x\<in>space M. \<not> P x} \<subseteq> N \<Longrightarrow> (AE x. P x)"
hoelzl@40871
   742
  unfolding almost_everywhere_def by auto
hoelzl@40871
   743
hoelzl@40871
   744
lemma (in measure_space) AE_iff_null_set:
hoelzl@40871
   745
  assumes "{x\<in>space M. \<not> P x} \<in> sets M" (is "?P \<in> sets M")
hoelzl@40871
   746
  shows "(AE x. P x) \<longleftrightarrow> {x\<in>space M. \<not> P x} \<in> null_sets"
hoelzl@40871
   747
proof
hoelzl@40871
   748
  assume "AE x. P x" then obtain N where N: "N \<in> sets M" "?P \<subseteq> N" "\<mu> N = 0"
hoelzl@40871
   749
    unfolding almost_everywhere_def by auto
hoelzl@40871
   750
  moreover have "\<mu> ?P \<le> \<mu> N"
hoelzl@40871
   751
    using assms N(1,2) by (auto intro: measure_mono)
hoelzl@40871
   752
  ultimately show "?P \<in> null_sets" using assms by auto
hoelzl@40871
   753
next
hoelzl@40871
   754
  assume "?P \<in> null_sets" with assms show "AE x. P x" by (auto intro: AE_I')
hoelzl@40871
   755
qed
hoelzl@40871
   756
hoelzl@40859
   757
lemma (in measure_space) AE_True[intro, simp]: "AE x. True"
hoelzl@40859
   758
  unfolding almost_everywhere_def by auto
hoelzl@40859
   759
hoelzl@40859
   760
lemma (in measure_space) AE_E[consumes 1]:
hoelzl@40859
   761
  assumes "AE x. P x"
hoelzl@40859
   762
  obtains N where "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
hoelzl@40859
   763
  using assms unfolding almost_everywhere_def by auto
hoelzl@40859
   764
hoelzl@40859
   765
lemma (in measure_space) AE_I:
hoelzl@40859
   766
  assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M"
hoelzl@40859
   767
  shows "AE x. P x"
hoelzl@40859
   768
  using assms unfolding almost_everywhere_def by auto
hoelzl@40859
   769
hoelzl@40859
   770
lemma (in measure_space) AE_mp:
hoelzl@40859
   771
  assumes AE_P: "AE x. P x" and AE_imp: "AE x. P x \<longrightarrow> Q x"
hoelzl@40859
   772
  shows "AE x. Q x"
hoelzl@40859
   773
proof -
hoelzl@40859
   774
  from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
hoelzl@40859
   775
    and A: "A \<in> sets M" "\<mu> A = 0"
hoelzl@40859
   776
    by (auto elim!: AE_E)
hoelzl@40859
   777
hoelzl@40859
   778
  from AE_imp obtain B where imp: "{x\<in>space M. P x \<and> \<not> Q x} \<subseteq> B"
hoelzl@40859
   779
    and B: "B \<in> sets M" "\<mu> B = 0"
hoelzl@40859
   780
    by (auto elim!: AE_E)
hoelzl@40859
   781
hoelzl@40859
   782
  show ?thesis
hoelzl@40859
   783
  proof (intro AE_I)
hoelzl@40859
   784
    show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B
hoelzl@40859
   785
      using measure_subadditive[of A B] by auto
hoelzl@40859
   786
    show "{x\<in>space M. \<not> Q x} \<subseteq> A \<union> B"
hoelzl@40859
   787
      using P imp by auto
hoelzl@40859
   788
  qed
hoelzl@40859
   789
qed
hoelzl@40859
   790
hoelzl@40859
   791
lemma (in measure_space) AE_iffI:
hoelzl@40859
   792
  assumes P: "AE x. P x" and Q: "AE x. P x \<longleftrightarrow> Q x" shows "AE x. Q x"
hoelzl@40859
   793
  using AE_mp[OF Q, of "\<lambda>x. P x \<longrightarrow> Q x"] AE_mp[OF P, of Q] by auto
hoelzl@40859
   794
hoelzl@40859
   795
lemma (in measure_space) AE_disjI1:
hoelzl@40859
   796
  assumes P: "AE x. P x" shows "AE x. P x \<or> Q x"
hoelzl@40859
   797
  by (rule AE_mp[OF P]) auto
hoelzl@40859
   798
hoelzl@40859
   799
lemma (in measure_space) AE_disjI2:
hoelzl@40859
   800
  assumes P: "AE x. Q x" shows "AE x. P x \<or> Q x"
hoelzl@40859
   801
  by (rule AE_mp[OF P]) auto
hoelzl@40859
   802
hoelzl@40859
   803
lemma (in measure_space) AE_conjI:
hoelzl@40859
   804
  assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
hoelzl@40859
   805
  shows "AE x. P x \<and> Q x"
hoelzl@40859
   806
proof -
hoelzl@40859
   807
  from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
hoelzl@40859
   808
    and A: "A \<in> sets M" "\<mu> A = 0"
hoelzl@40859
   809
    by (auto elim!: AE_E)
hoelzl@40859
   810
hoelzl@40859
   811
  from AE_Q obtain B where Q: "{x\<in>space M. \<not> Q x} \<subseteq> B"
hoelzl@40859
   812
    and B: "B \<in> sets M" "\<mu> B = 0"
hoelzl@40859
   813
    by (auto elim!: AE_E)
hoelzl@40859
   814
hoelzl@40859
   815
  show ?thesis
hoelzl@40859
   816
  proof (intro AE_I)
hoelzl@40859
   817
    show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B
hoelzl@40859
   818
      using measure_subadditive[of A B] by auto
hoelzl@40859
   819
    show "{x\<in>space M. \<not> (P x \<and> Q x)} \<subseteq> A \<union> B"
hoelzl@40859
   820
      using P Q by auto
hoelzl@40859
   821
  qed
hoelzl@40859
   822
qed
hoelzl@40859
   823
hoelzl@40859
   824
lemma (in measure_space) AE_E2:
hoelzl@40859
   825
  assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
hoelzl@40859
   826
  shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0")
hoelzl@40859
   827
proof -
hoelzl@40859
   828
  obtain A where A: "?P \<subseteq> A" "A \<in> sets M" "\<mu> A = 0"
hoelzl@40859
   829
    using assms by (auto elim!: AE_E)
hoelzl@40859
   830
  have "?P = space M - {x\<in>space M. P x}" by auto
hoelzl@40859
   831
  then have "?P \<in> sets M" using assms by auto
hoelzl@40859
   832
  with assms `?P \<subseteq> A` `A \<in> sets M` have "\<mu> ?P \<le> \<mu> A"
hoelzl@40859
   833
    by (auto intro!: measure_mono)
hoelzl@40859
   834
  then show "\<mu> ?P = 0" using A by simp
hoelzl@40859
   835
qed
hoelzl@40859
   836
hoelzl@40859
   837
lemma (in measure_space) AE_space[simp, intro]: "AE x. x \<in> space M"
hoelzl@40859
   838
  by (rule AE_I[where N="{}"]) auto
hoelzl@40859
   839
hoelzl@40859
   840
lemma (in measure_space) AE_cong:
hoelzl@40859
   841
  assumes "\<And>x. x \<in> space M \<Longrightarrow> P x" shows "AE x. P x"
hoelzl@40859
   842
proof -
hoelzl@40859
   843
  have [simp]: "\<And>x. (x \<in> space M \<longrightarrow> P x) \<longleftrightarrow> True" using assms by auto
hoelzl@40859
   844
  show ?thesis
hoelzl@40859
   845
    by (rule AE_mp[OF AE_space]) auto
hoelzl@40859
   846
qed
hoelzl@40859
   847
hoelzl@40859
   848
lemma (in measure_space) AE_conj_iff[simp]:
hoelzl@40859
   849
  shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
hoelzl@40859
   850
proof (intro conjI iffI AE_conjI)
hoelzl@40859
   851
  assume *: "AE x. P x \<and> Q x"
hoelzl@40859
   852
  from * show "AE x. P x" by (rule AE_mp) auto
hoelzl@40859
   853
  from * show "AE x. Q x" by (rule AE_mp) auto
hoelzl@40859
   854
qed auto
hoelzl@40859
   855
hoelzl@40859
   856
lemma (in measure_space) all_AE_countable:
hoelzl@40859
   857
  "(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
hoelzl@40859
   858
proof
hoelzl@40859
   859
  assume "\<forall>i. AE x. P i x"
hoelzl@40859
   860
  from this[unfolded almost_everywhere_def Bex_def, THEN choice]
hoelzl@40859
   861
  obtain N where N: "\<And>i. N i \<in> null_sets" "\<And>i. {x\<in>space M. \<not> P i x} \<subseteq> N i" by auto
hoelzl@40859
   862
  have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. {x\<in>space M. \<not> P i x})" by auto
hoelzl@40859
   863
  also have "\<dots> \<subseteq> (\<Union>i. N i)" using N by auto
hoelzl@40859
   864
  finally have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. N i)" .
hoelzl@40859
   865
  moreover from N have "(\<Union>i. N i) \<in> null_sets"
hoelzl@40859
   866
    by (intro null_sets_UN) auto
hoelzl@40859
   867
  ultimately show "AE x. \<forall>i. P i x"
hoelzl@40859
   868
    unfolding almost_everywhere_def by auto
hoelzl@40859
   869
next
hoelzl@40859
   870
  assume *: "AE x. \<forall>i. P i x"
hoelzl@40859
   871
  show "\<forall>i. AE x. P i x"
hoelzl@40859
   872
    by (rule allI, rule AE_mp[OF *]) simp
hoelzl@40859
   873
qed
hoelzl@40859
   874
hoelzl@38656
   875
lemma (in measure_space) restricted_measure_space:
hoelzl@38656
   876
  assumes "S \<in> sets M"
hoelzl@39092
   877
  shows "measure_space (restricted_space S) \<mu>"
hoelzl@38656
   878
    (is "measure_space ?r \<mu>")
hoelzl@38656
   879
  unfolding measure_space_def measure_space_axioms_def
hoelzl@38656
   880
proof safe
hoelzl@38656
   881
  show "sigma_algebra ?r" using restricted_sigma_algebra[OF assms] .
hoelzl@38656
   882
  show "\<mu> {} = 0" by simp
hoelzl@38656
   883
  show "countably_additive ?r \<mu>"
hoelzl@38656
   884
    unfolding countably_additive_def
hoelzl@38656
   885
  proof safe
hoelzl@38656
   886
    fix A :: "nat \<Rightarrow> 'a set"
hoelzl@38656
   887
    assume *: "range A \<subseteq> sets ?r" and **: "disjoint_family A"
hoelzl@38656
   888
    from restriction_in_sets[OF assms *[simplified]] **
hoelzl@38656
   889
    show "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
hoelzl@38656
   890
      using measure_countably_additive by simp
hoelzl@38656
   891
  qed
hoelzl@38656
   892
qed
hoelzl@38656
   893
hoelzl@39089
   894
lemma (in measure_space) measure_space_vimage:
hoelzl@40859
   895
  fixes M' :: "'b algebra"
hoelzl@39089
   896
  assumes "f \<in> measurable M M'"
hoelzl@39089
   897
  and "sigma_algebra M'"
hoelzl@39089
   898
  shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T")
hoelzl@39089
   899
proof -
hoelzl@39089
   900
  interpret M': sigma_algebra M' by fact
hoelzl@39089
   901
hoelzl@39089
   902
  show ?thesis
hoelzl@39089
   903
  proof
hoelzl@39089
   904
    show "?T {} = 0" by simp
hoelzl@39089
   905
hoelzl@39089
   906
    show "countably_additive M' ?T"
hoelzl@39089
   907
    proof (unfold countably_additive_def, safe)
hoelzl@40859
   908
      fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets M'" "disjoint_family A"
hoelzl@39089
   909
      hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M"
hoelzl@39089
   910
        using `f \<in> measurable M M'` by (auto simp: measurable_def)
hoelzl@39089
   911
      moreover have "(\<Union>i. f -`  A i \<inter> space M) \<in> sets M"
hoelzl@39089
   912
        using * by blast
hoelzl@39089
   913
      moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)"
hoelzl@39089
   914
        using `disjoint_family A` by (auto simp: disjoint_family_on_def)
hoelzl@39089
   915
      ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)"
hoelzl@39089
   916
        using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN)
hoelzl@39089
   917
    qed
hoelzl@39089
   918
  qed
hoelzl@39089
   919
qed
hoelzl@39089
   920
hoelzl@39092
   921
lemma (in measure_space) measure_space_subalgebra:
hoelzl@41545
   922
  assumes "sigma_algebra N" and [simp]: "sets N \<subseteq> sets M" "space N = space M"
hoelzl@41545
   923
  shows "measure_space N \<mu>"
hoelzl@39092
   924
proof -
hoelzl@41545
   925
  interpret N: sigma_algebra N by fact
hoelzl@39092
   926
  show ?thesis
hoelzl@39092
   927
  proof
hoelzl@41545
   928
    from `sets N \<subseteq> sets M` have "\<And>A. range A \<subseteq> sets N \<Longrightarrow> range A \<subseteq> sets M" by blast
hoelzl@41545
   929
    then show "countably_additive N \<mu>"
hoelzl@41545
   930
      by (auto intro!: measure_countably_additive simp: countably_additive_def)
hoelzl@39092
   931
  qed simp
hoelzl@39092
   932
qed
hoelzl@39092
   933
hoelzl@38656
   934
section "@{text \<sigma>}-finite Measures"
hoelzl@38656
   935
hoelzl@38656
   936
locale sigma_finite_measure = measure_space +
hoelzl@38656
   937
  assumes sigma_finite: "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)"
hoelzl@38656
   938
hoelzl@38656
   939
lemma (in sigma_finite_measure) restricted_sigma_finite_measure:
hoelzl@38656
   940
  assumes "S \<in> sets M"
hoelzl@39092
   941
  shows "sigma_finite_measure (restricted_space S) \<mu>"
hoelzl@38656
   942
    (is "sigma_finite_measure ?r _")
hoelzl@38656
   943
  unfolding sigma_finite_measure_def sigma_finite_measure_axioms_def
hoelzl@38656
   944
proof safe
hoelzl@38656
   945
  show "measure_space ?r \<mu>" using restricted_measure_space[OF assms] .
hoelzl@38656
   946
next
hoelzl@38656
   947
  obtain A :: "nat \<Rightarrow> 'a set" where
hoelzl@38656
   948
      "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. \<mu> (A i) \<noteq> \<omega>"
hoelzl@38656
   949
    using sigma_finite by auto
hoelzl@38656
   950
  show "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets ?r \<and> (\<Union>i. A i) = space ?r \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)"
hoelzl@38656
   951
  proof (safe intro!: exI[of _ "\<lambda>i. A i \<inter> S"] del: notI)
hoelzl@38656
   952
    fix i
hoelzl@38656
   953
    show "A i \<inter> S \<in> sets ?r"
hoelzl@38656
   954
      using `range A \<subseteq> sets M` `S \<in> sets M` by auto
hoelzl@38656
   955
  next
hoelzl@38656
   956
    fix x i assume "x \<in> S" thus "x \<in> space ?r" by simp
hoelzl@38656
   957
  next
hoelzl@38656
   958
    fix x assume "x \<in> space ?r" thus "x \<in> (\<Union>i. A i \<inter> S)"
hoelzl@38656
   959
      using `(\<Union>i. A i) = space M` `S \<in> sets M` by auto
hoelzl@38656
   960
  next
hoelzl@38656
   961
    fix i
hoelzl@38656
   962
    have "\<mu> (A i \<inter> S) \<le> \<mu> (A i)"
hoelzl@38656
   963
      using `range A \<subseteq> sets M` `S \<in> sets M` by (auto intro!: measure_mono)
hoelzl@41023
   964
    also have "\<dots> < \<omega>" using `\<mu> (A i) \<noteq> \<omega>` by (auto simp: pextreal_less_\<omega>)
hoelzl@41023
   965
    finally show "\<mu> (A i \<inter> S) \<noteq> \<omega>" by (auto simp: pextreal_less_\<omega>)
hoelzl@38656
   966
  qed
hoelzl@38656
   967
qed
hoelzl@38656
   968
hoelzl@40859
   969
lemma (in sigma_finite_measure) sigma_finite_measure_cong:
hoelzl@40859
   970
  assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A"
hoelzl@40859
   971
  shows "sigma_finite_measure M \<mu>'"
hoelzl@40859
   972
proof -
hoelzl@40859
   973
  interpret \<mu>': measure_space M \<mu>'
hoelzl@40859
   974
    using cong by (rule measure_space_cong)
hoelzl@40859
   975
  from sigma_finite guess A .. note A = this
hoelzl@40859
   976
  then have "\<And>i. A i \<in> sets M" by auto
hoelzl@40859
   977
  with A have fin: "(\<forall>i. \<mu>' (A i) \<noteq> \<omega>)" using cong by auto
hoelzl@40859
   978
  show ?thesis
hoelzl@40859
   979
    apply default
hoelzl@40859
   980
    using A fin by auto
hoelzl@40859
   981
qed
hoelzl@40859
   982
hoelzl@39092
   983
lemma (in sigma_finite_measure) disjoint_sigma_finite:
hoelzl@39092
   984
  "\<exists>A::nat\<Rightarrow>'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and>
hoelzl@39092
   985
    (\<forall>i. \<mu> (A i) \<noteq> \<omega>) \<and> disjoint_family A"
hoelzl@39092
   986
proof -
hoelzl@39092
   987
  obtain A :: "nat \<Rightarrow> 'a set" where
hoelzl@39092
   988
    range: "range A \<subseteq> sets M" and
hoelzl@39092
   989
    space: "(\<Union>i. A i) = space M" and
hoelzl@39092
   990
    measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
hoelzl@39092
   991
    using sigma_finite by auto
hoelzl@39092
   992
  note range' = range_disjointed_sets[OF range] range
hoelzl@39092
   993
  { fix i
hoelzl@39092
   994
    have "\<mu> (disjointed A i) \<le> \<mu> (A i)"
hoelzl@39092
   995
      using range' disjointed_subset[of A i] by (auto intro!: measure_mono)
hoelzl@39092
   996
    then have "\<mu> (disjointed A i) \<noteq> \<omega>"
hoelzl@39092
   997
      using measure[of i] by auto }
hoelzl@39092
   998
  with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
hoelzl@39092
   999
  show ?thesis by (auto intro!: exI[of _ "disjointed A"])
hoelzl@39092
  1000
qed
hoelzl@39092
  1001
hoelzl@40859
  1002
lemma (in sigma_finite_measure) sigma_finite_up:
hoelzl@40859
  1003
  "\<exists>F. range F \<subseteq> sets M \<and> F \<up> space M \<and> (\<forall>i. \<mu> (F i) \<noteq> \<omega>)"
hoelzl@40859
  1004
proof -
hoelzl@40859
  1005
  obtain F :: "nat \<Rightarrow> 'a set" where
hoelzl@40859
  1006
    F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. \<mu> (F i) \<noteq> \<omega>"
hoelzl@40859
  1007
    using sigma_finite by auto
hoelzl@40859
  1008
  then show ?thesis unfolding isoton_def
hoelzl@40859
  1009
  proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
hoelzl@40859
  1010
    from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
hoelzl@40859
  1011
    then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
hoelzl@40859
  1012
      using F by fastsimp
hoelzl@40859
  1013
  next
hoelzl@40859
  1014
    fix n
hoelzl@40859
  1015
    have "\<mu> (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. \<mu> (F i))" using F
hoelzl@40859
  1016
      by (auto intro!: measure_finitely_subadditive)
hoelzl@40859
  1017
    also have "\<dots> < \<omega>"
hoelzl@40859
  1018
      using F by (auto simp: setsum_\<omega>)
hoelzl@40859
  1019
    finally show "\<mu> (\<Union> i\<le>n. F i) \<noteq> \<omega>" by simp
hoelzl@40859
  1020
  qed force+
hoelzl@40859
  1021
qed
hoelzl@40859
  1022
hoelzl@40859
  1023
lemma (in sigma_finite_measure) sigma_finite_measure_isomorphic:
hoelzl@40859
  1024
  assumes f: "bij_betw f S (space M)"
hoelzl@40859
  1025
  shows "sigma_finite_measure (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))"
hoelzl@40859
  1026
proof -
hoelzl@40859
  1027
  interpret M: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
hoelzl@40859
  1028
    using f by (rule measure_space_isomorphic)
hoelzl@40859
  1029
  show ?thesis
hoelzl@40859
  1030
  proof default
hoelzl@40859
  1031
    from sigma_finite guess A::"nat \<Rightarrow> 'a set" .. note A = this
hoelzl@40859
  1032
    show "\<exists>A::nat\<Rightarrow>'b set. range A \<subseteq> sets (vimage_algebra S f) \<and> (\<Union>i. A i) = space (vimage_algebra S f) \<and> (\<forall>i. \<mu> (f ` A i) \<noteq> \<omega>)"
hoelzl@40859
  1033
    proof (intro exI conjI)
hoelzl@40859
  1034
      show "(\<Union>i::nat. f -` A i \<inter> S) = space (vimage_algebra S f)"
hoelzl@40859
  1035
        using A f[THEN bij_betw_imp_funcset] by (auto simp: vimage_UN[symmetric])
hoelzl@40859
  1036
      show "range (\<lambda>i. f -` A i \<inter> S) \<subseteq> sets (vimage_algebra S f)"
hoelzl@40859
  1037
        using A by (auto simp: vimage_algebra_def)
hoelzl@40859
  1038
      have "\<And>i. f ` (f -` A i \<inter> S) = A i"
hoelzl@40859
  1039
        using f A sets_into_space
hoelzl@40859
  1040
        by (intro image_vimage_inter_eq) (auto simp: bij_betw_def)
hoelzl@40859
  1041
      then show "\<forall>i. \<mu> (f ` (f -` A i \<inter> S)) \<noteq> \<omega>"  using A by simp
hoelzl@40859
  1042
    qed
hoelzl@40859
  1043
  qed
hoelzl@40859
  1044
qed
hoelzl@40859
  1045
hoelzl@38656
  1046
section "Real measure values"
hoelzl@38656
  1047
hoelzl@38656
  1048
lemma (in measure_space) real_measure_Union:
hoelzl@38656
  1049
  assumes finite: "\<mu> A \<noteq> \<omega>" "\<mu> B \<noteq> \<omega>"
hoelzl@38656
  1050
  and measurable: "A \<in> sets M" "B \<in> sets M" "A \<inter> B = {}"
hoelzl@38656
  1051
  shows "real (\<mu> (A \<union> B)) = real (\<mu> A) + real (\<mu> B)"
hoelzl@38656
  1052
  unfolding measure_additive[symmetric, OF measurable]
hoelzl@41023
  1053
  using finite by (auto simp: real_of_pextreal_add)
hoelzl@38656
  1054
hoelzl@38656
  1055
lemma (in measure_space) real_measure_finite_Union:
hoelzl@38656
  1056
  assumes measurable:
hoelzl@38656
  1057
    "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M" "disjoint_family_on A S"
hoelzl@38656
  1058
  assumes finite: "\<And>i. i \<in> S \<Longrightarrow> \<mu> (A i) \<noteq> \<omega>"
hoelzl@38656
  1059
  shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))"
hoelzl@41023
  1060
  using real_of_pextreal_setsum[of S, OF finite]
hoelzl@38656
  1061
        measure_finitely_additive''[symmetric, OF measurable]
hoelzl@38656
  1062
  by simp
hoelzl@38656
  1063
hoelzl@38656
  1064
lemma (in measure_space) real_measure_Diff:
hoelzl@38656
  1065
  assumes finite: "\<mu> A \<noteq> \<omega>"
hoelzl@38656
  1066
  and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
hoelzl@38656
  1067
  shows "real (\<mu> (A - B)) = real (\<mu> A) - real (\<mu> B)"
hoelzl@38656
  1068
proof -
hoelzl@38656
  1069
  have "\<mu> (A - B) \<le> \<mu> A"
hoelzl@38656
  1070
    "\<mu> B \<le> \<mu> A"
hoelzl@38656
  1071
    using measurable by (auto intro!: measure_mono)
hoelzl@38656
  1072
  hence "real (\<mu> ((A - B) \<union> B)) = real (\<mu> (A - B)) + real (\<mu> B)"
hoelzl@38656
  1073
    using measurable finite by (rule_tac real_measure_Union) auto
hoelzl@38656
  1074
  thus ?thesis using `B \<subseteq> A` by (auto simp: Un_absorb2)
hoelzl@38656
  1075
qed
hoelzl@38656
  1076
hoelzl@38656
  1077
lemma (in measure_space) real_measure_UNION:
hoelzl@38656
  1078
  assumes measurable: "range A \<subseteq> sets M" "disjoint_family A"
hoelzl@38656
  1079
  assumes finite: "\<mu> (\<Union>i. A i) \<noteq> \<omega>"
hoelzl@38656
  1080
  shows "(\<lambda>i. real (\<mu> (A i))) sums (real (\<mu> (\<Union>i. A i)))"
hoelzl@38656
  1081
proof -
hoelzl@38656
  1082
  have *: "(\<Sum>\<^isub>\<infinity> i. \<mu> (A i)) = \<mu> (\<Union>i. A i)"
hoelzl@38656
  1083
    using measure_countably_additive[OF measurable] by (simp add: comp_def)
hoelzl@38656
  1084
  hence "(\<Sum>\<^isub>\<infinity> i. \<mu> (A i)) \<noteq> \<omega>" using finite by simp
hoelzl@38656
  1085
  from psuminf_imp_suminf[OF this]
hoelzl@38656
  1086
  show ?thesis using * by simp
hoelzl@38656
  1087
qed
hoelzl@38656
  1088
hoelzl@38656
  1089
lemma (in measure_space) real_measure_subadditive:
hoelzl@38656
  1090
  assumes measurable: "A \<in> sets M" "B \<in> sets M"
hoelzl@38656
  1091
  and fin: "\<mu> A \<noteq> \<omega>" "\<mu> B \<noteq> \<omega>"
hoelzl@38656
  1092
  shows "real (\<mu> (A \<union> B)) \<le> real (\<mu> A) + real (\<mu> B)"
hoelzl@38656
  1093
proof -
hoelzl@38656
  1094
  have "real (\<mu> (A \<union> B)) \<le> real (\<mu> A + \<mu> B)"
hoelzl@41023
  1095
    using measure_subadditive[OF measurable] fin by (auto intro!: real_of_pextreal_mono)
hoelzl@38656
  1096
  also have "\<dots> = real (\<mu> A) + real (\<mu> B)"
hoelzl@41023
  1097
    using fin by (simp add: real_of_pextreal_add)
hoelzl@38656
  1098
  finally show ?thesis .
hoelzl@38656
  1099
qed
hoelzl@38656
  1100
hoelzl@40859
  1101
lemma (in measure_space) real_measure_countably_subadditive:
hoelzl@38656
  1102
  assumes "range f \<subseteq> sets M" and "(\<Sum>\<^isub>\<infinity> i. \<mu> (f i)) \<noteq> \<omega>"
hoelzl@38656
  1103
  shows "real (\<mu> (\<Union>i. f i)) \<le> (\<Sum> i. real (\<mu> (f i)))"
hoelzl@38656
  1104
proof -
hoelzl@38656
  1105
  have "real (\<mu> (\<Union>i. f i)) \<le> real (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))"
hoelzl@41023
  1106
    using assms by (auto intro!: real_of_pextreal_mono measure_countably_subadditive)
hoelzl@38656
  1107
  also have "\<dots> = (\<Sum> i. real (\<mu> (f i)))"
hoelzl@38656
  1108
    using assms by (auto intro!: sums_unique psuminf_imp_suminf)
hoelzl@38656
  1109
  finally show ?thesis .
hoelzl@38656
  1110
qed
hoelzl@38656
  1111
hoelzl@38656
  1112
lemma (in measure_space) real_measure_setsum_singleton:
hoelzl@38656
  1113
  assumes S: "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
hoelzl@38656
  1114
  and fin: "\<And>x. x \<in> S \<Longrightarrow> \<mu> {x} \<noteq> \<omega>"
hoelzl@38656
  1115
  shows "real (\<mu> S) = (\<Sum>x\<in>S. real (\<mu> {x}))"
hoelzl@41023
  1116
  using measure_finite_singleton[OF S] fin by (simp add: real_of_pextreal_setsum)
hoelzl@38656
  1117
hoelzl@38656
  1118
lemma (in measure_space) real_continuity_from_below:
hoelzl@38656
  1119
  assumes A: "range A \<subseteq> sets M" "\<And>i. A i \<subseteq> A (Suc i)" and "\<mu> (\<Union>i. A i) \<noteq> \<omega>"
hoelzl@38656
  1120
  shows "(\<lambda>i. real (\<mu> (A i))) ----> real (\<mu> (\<Union>i. A i))"
hoelzl@38656
  1121
proof (rule SUP_eq_LIMSEQ[THEN iffD1])
hoelzl@38656
  1122
  { fix n have "\<mu> (A n) \<le> \<mu> (\<Union>i. A i)"
hoelzl@38656
  1123
      using A by (auto intro!: measure_mono)
hoelzl@38656
  1124
    hence "\<mu> (A n) \<noteq> \<omega>" using assms by auto }
hoelzl@38656
  1125
  note this[simp]
hoelzl@38656
  1126
hoelzl@38656
  1127
  show "mono (\<lambda>i. real (\<mu> (A i)))" unfolding mono_iff_le_Suc using A
hoelzl@41023
  1128
    by (auto intro!: real_of_pextreal_mono measure_mono)
hoelzl@38656
  1129
hoelzl@38656
  1130
  show "(SUP n. Real (real (\<mu> (A n)))) = Real (real (\<mu> (\<Union>i. A i)))"
hoelzl@38656
  1131
    using continuity_from_below[OF A(1), OF A(2)]
hoelzl@38656
  1132
    using assms by (simp add: Real_real)
hoelzl@38656
  1133
qed simp_all
hoelzl@38656
  1134
hoelzl@38656
  1135
lemma (in measure_space) real_continuity_from_above:
hoelzl@38656
  1136
  assumes A: "range A \<subseteq> sets M"
hoelzl@38656
  1137
  and mono_Suc: "\<And>n.  A (Suc n) \<subseteq> A n"
hoelzl@38656
  1138
  and finite: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
hoelzl@38656
  1139
  shows "(\<lambda>n. real (\<mu> (A n))) ----> real (\<mu> (\<Inter>i. A i))"
hoelzl@38656
  1140
proof (rule INF_eq_LIMSEQ[THEN iffD1])
hoelzl@38656
  1141
  { fix n have "\<mu> (\<Inter>i. A i) \<le> \<mu> (A n)"
hoelzl@38656
  1142
      using A by (auto intro!: measure_mono)
hoelzl@38656
  1143
    hence "\<mu> (\<Inter>i. A i) \<noteq> \<omega>" using assms by auto }
hoelzl@38656
  1144
  note this[simp]
hoelzl@38656
  1145
hoelzl@38656
  1146
  show "mono (\<lambda>i. - real (\<mu> (A i)))" unfolding mono_iff_le_Suc using assms
hoelzl@41023
  1147
    by (auto intro!: real_of_pextreal_mono measure_mono)
hoelzl@38656
  1148
hoelzl@38656
  1149
  show "(INF n. Real (real (\<mu> (A n)))) =
hoelzl@38656
  1150
    Real (real (\<mu> (\<Inter>i. A i)))"
hoelzl@38656
  1151
    using continuity_from_above[OF A, OF mono_Suc finite]
hoelzl@38656
  1152
    using assms by (simp add: Real_real)
hoelzl@38656
  1153
qed simp_all
hoelzl@38656
  1154
hoelzl@38656
  1155
locale finite_measure = measure_space +
hoelzl@38656
  1156
  assumes finite_measure_of_space: "\<mu> (space M) \<noteq> \<omega>"
hoelzl@38656
  1157
hoelzl@38656
  1158
sublocale finite_measure < sigma_finite_measure
hoelzl@38656
  1159
proof
hoelzl@38656
  1160
  show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)"
hoelzl@38656
  1161
    using finite_measure_of_space by (auto intro!: exI[of _ "\<lambda>x. space M"])
hoelzl@38656
  1162
qed
hoelzl@38656
  1163
hoelzl@39092
  1164
lemma (in finite_measure) finite_measure[simp, intro]:
hoelzl@38656
  1165
  assumes "A \<in> sets M"
hoelzl@38656
  1166
  shows "\<mu> A \<noteq> \<omega>"
hoelzl@38656
  1167
proof -
hoelzl@38656
  1168
  from `A \<in> sets M` have "A \<subseteq> space M"
hoelzl@38656
  1169
    using sets_into_space by blast
hoelzl@38656
  1170
  hence "\<mu> A \<le> \<mu> (space M)"
hoelzl@38656
  1171
    using assms top by (rule measure_mono)
hoelzl@38656
  1172
  also have "\<dots> < \<omega>"
hoelzl@41023
  1173
    using finite_measure_of_space unfolding pextreal_less_\<omega> .
hoelzl@41023
  1174
  finally show ?thesis unfolding pextreal_less_\<omega> .
hoelzl@38656
  1175
qed
hoelzl@38656
  1176
hoelzl@38656
  1177
lemma (in finite_measure) restricted_finite_measure:
hoelzl@38656
  1178
  assumes "S \<in> sets M"
hoelzl@39092
  1179
  shows "finite_measure (restricted_space S) \<mu>"
hoelzl@38656
  1180
    (is "finite_measure ?r _")
hoelzl@38656
  1181
  unfolding finite_measure_def finite_measure_axioms_def
hoelzl@38656
  1182
proof (safe del: notI)
hoelzl@38656
  1183
  show "measure_space ?r \<mu>" using restricted_measure_space[OF assms] .
hoelzl@38656
  1184
next
hoelzl@38656
  1185
  show "\<mu> (space ?r) \<noteq> \<omega>" using finite_measure[OF `S \<in> sets M`] by auto
hoelzl@38656
  1186
qed
hoelzl@38656
  1187
hoelzl@40859
  1188
lemma (in measure_space) restricted_to_finite_measure:
hoelzl@40859
  1189
  assumes "S \<in> sets M" "\<mu> S \<noteq> \<omega>"
hoelzl@40859
  1190
  shows "finite_measure (restricted_space S) \<mu>"
hoelzl@40859
  1191
proof -
hoelzl@40859
  1192
  have "measure_space (restricted_space S) \<mu>"
hoelzl@40859
  1193
    using `S \<in> sets M` by (rule restricted_measure_space)
hoelzl@40859
  1194
  then show ?thesis
hoelzl@40859
  1195
    unfolding finite_measure_def finite_measure_axioms_def
hoelzl@40859
  1196
    using assms by auto
hoelzl@40859
  1197
qed
hoelzl@40859
  1198
hoelzl@38656
  1199
lemma (in finite_measure) real_finite_measure_Diff:
hoelzl@38656
  1200
  assumes "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
hoelzl@38656
  1201
  shows "real (\<mu> (A - B)) = real (\<mu> A) - real (\<mu> B)"
hoelzl@38656
  1202
  using finite_measure[OF `A \<in> sets M`] by (rule real_measure_Diff[OF _ assms])
hoelzl@38656
  1203
hoelzl@38656
  1204
lemma (in finite_measure) real_finite_measure_Union:
hoelzl@38656
  1205
  assumes sets: "A \<in> sets M" "B \<in> sets M" and "A \<inter> B = {}"
hoelzl@38656
  1206
  shows "real (\<mu> (A \<union> B)) = real (\<mu> A) + real (\<mu> B)"
hoelzl@38656
  1207
  using sets by (auto intro!: real_measure_Union[OF _ _ assms] finite_measure)
hoelzl@38656
  1208
hoelzl@38656
  1209
lemma (in finite_measure) real_finite_measure_finite_Union:
hoelzl@38656
  1210
  assumes "finite S" and dis: "disjoint_family_on A S"
hoelzl@38656
  1211
  and *: "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M"
hoelzl@38656
  1212
  shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))"
hoelzl@38656
  1213
proof (rule real_measure_finite_Union[OF `finite S` _ dis])
hoelzl@38656
  1214
  fix i assume "i \<in> S" from *[OF this] show "A i \<in> sets M" .
hoelzl@38656
  1215
  from finite_measure[OF this] show "\<mu> (A i) \<noteq> \<omega>" .
hoelzl@38656
  1216
qed
hoelzl@38656
  1217
hoelzl@38656
  1218
lemma (in finite_measure) real_finite_measure_UNION:
hoelzl@38656
  1219
  assumes measurable: "range A \<subseteq> sets M" "disjoint_family A"
hoelzl@38656
  1220
  shows "(\<lambda>i. real (\<mu> (A i))) sums (real (\<mu> (\<Union>i. A i)))"
hoelzl@38656
  1221
proof (rule real_measure_UNION[OF assms])
hoelzl@38656
  1222
  have "(\<Union>i. A i) \<in> sets M" using measurable(1) by (rule countable_UN)
hoelzl@38656
  1223
  thus "\<mu> (\<Union>i. A i) \<noteq> \<omega>" by (rule finite_measure)
hoelzl@38656
  1224
qed
hoelzl@38656
  1225
hoelzl@38656
  1226
lemma (in finite_measure) real_measure_mono:
hoelzl@38656
  1227
  "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A \<subseteq> B \<Longrightarrow> real (\<mu> A) \<le> real (\<mu> B)"
hoelzl@41023
  1228
  by (auto intro!: measure_mono real_of_pextreal_mono finite_measure)
hoelzl@38656
  1229
hoelzl@38656
  1230
lemma (in finite_measure) real_finite_measure_subadditive:
hoelzl@38656
  1231
  assumes measurable: "A \<in> sets M" "B \<in> sets M"
hoelzl@38656
  1232
  shows "real (\<mu> (A \<union> B)) \<le> real (\<mu> A) + real (\<mu> B)"
hoelzl@38656
  1233
  using measurable measurable[THEN finite_measure] by (rule real_measure_subadditive)
hoelzl@38656
  1234
hoelzl@40859
  1235
lemma (in finite_measure) real_finite_measure_countably_subadditive:
hoelzl@38656
  1236
  assumes "range f \<subseteq> sets M" and "summable (\<lambda>i. real (\<mu> (f i)))"
hoelzl@38656
  1237
  shows "real (\<mu> (\<Union>i. f i)) \<le> (\<Sum> i. real (\<mu> (f i)))"
hoelzl@40859
  1238
proof (rule real_measure_countably_subadditive[OF assms(1)])
hoelzl@38656
  1239
  have *: "\<And>i. f i \<in> sets M" using assms by auto
hoelzl@38656
  1240
  have "(\<lambda>i. real (\<mu> (f i))) sums (\<Sum>i. real (\<mu> (f i)))"
hoelzl@38656
  1241
    using assms(2) by (rule summable_sums)
hoelzl@38656
  1242
  from suminf_imp_psuminf[OF this]
hoelzl@38656
  1243
  have "(\<Sum>\<^isub>\<infinity>i. \<mu> (f i)) = Real (\<Sum>i. real (\<mu> (f i)))"
hoelzl@38656
  1244
    using * by (simp add: Real_real finite_measure)
hoelzl@38656
  1245
  thus "(\<Sum>\<^isub>\<infinity>i. \<mu> (f i)) \<noteq> \<omega>" by simp
hoelzl@38656
  1246
qed
hoelzl@38656
  1247
hoelzl@38656
  1248
lemma (in finite_measure) real_finite_measure_finite_singelton:
hoelzl@38656
  1249
  assumes "finite S" and *: "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
hoelzl@38656
  1250
  shows "real (\<mu> S) = (\<Sum>x\<in>S. real (\<mu> {x}))"
hoelzl@38656
  1251
proof (rule real_measure_setsum_singleton[OF `finite S`])
hoelzl@38656
  1252
  fix x assume "x \<in> S" thus "{x} \<in> sets M" by (rule *)
hoelzl@38656
  1253
  with finite_measure show "\<mu> {x} \<noteq> \<omega>" .
hoelzl@38656
  1254
qed
hoelzl@38656
  1255
hoelzl@38656
  1256
lemma (in finite_measure) real_finite_continuity_from_below:
hoelzl@38656
  1257
  assumes "range A \<subseteq> sets M" "\<And>i. A i \<subseteq> A (Suc i)"
hoelzl@38656
  1258
  shows "(\<lambda>i. real (\<mu> (A i))) ----> real (\<mu> (\<Union>i. A i))"
hoelzl@38656
  1259
  using real_continuity_from_below[OF assms(1), OF assms(2) finite_measure] assms by auto
hoelzl@38656
  1260
hoelzl@38656
  1261
lemma (in finite_measure) real_finite_continuity_from_above:
hoelzl@38656
  1262
  assumes A: "range A \<subseteq> sets M"
hoelzl@38656
  1263
  and mono_Suc: "\<And>n.  A (Suc n) \<subseteq> A n"
hoelzl@38656
  1264
  shows "(\<lambda>n. real (\<mu> (A n))) ----> real (\<mu> (\<Inter>i. A i))"
hoelzl@38656
  1265
  using real_continuity_from_above[OF A, OF mono_Suc finite_measure] A
hoelzl@38656
  1266
  by auto
hoelzl@38656
  1267
hoelzl@38656
  1268
lemma (in finite_measure) real_finite_measure_finite_Union':
hoelzl@38656
  1269
  assumes "finite S" "A`S \<subseteq> sets M" "disjoint_family_on A S"
hoelzl@38656
  1270
  shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))"
hoelzl@38656
  1271
  using assms real_finite_measure_finite_Union[of S A] by auto
hoelzl@38656
  1272
hoelzl@38656
  1273
lemma (in finite_measure) finite_measure_compl:
hoelzl@38656
  1274
  assumes s: "s \<in> sets M"
hoelzl@38656
  1275
  shows "\<mu> (space M - s) = \<mu> (space M) - \<mu> s"
hoelzl@38656
  1276
  using measure_compl[OF s, OF finite_measure, OF s] .
hoelzl@38656
  1277
hoelzl@39092
  1278
lemma (in finite_measure) finite_measure_inter_full_set:
hoelzl@39092
  1279
  assumes "S \<in> sets M" "T \<in> sets M"
hoelzl@39092
  1280
  assumes T: "\<mu> T = \<mu> (space M)"
hoelzl@39092
  1281
  shows "\<mu> (S \<inter> T) = \<mu> S"
hoelzl@39092
  1282
  using measure_inter_full_set[OF assms(1,2) finite_measure assms(3)] assms
hoelzl@39092
  1283
  by auto
hoelzl@39092
  1284
hoelzl@38656
  1285
section {* Measure preserving *}
hoelzl@38656
  1286
hoelzl@38656
  1287
definition "measure_preserving A \<mu> B \<nu> =
hoelzl@38656
  1288
    {f \<in> measurable A B. (\<forall>y \<in> sets B. \<mu> (f -` y \<inter> space A) = \<nu> y)}"
hoelzl@38656
  1289
hoelzl@38656
  1290
lemma (in finite_measure) measure_preserving_lift:
hoelzl@40859
  1291
  fixes f :: "'a \<Rightarrow> 'a2" and A :: "'a2 algebra"
hoelzl@38656
  1292
  assumes "algebra A"
hoelzl@40859
  1293
  assumes "finite_measure (sigma A) \<nu>" (is "finite_measure ?sA _")
hoelzl@38656
  1294
  assumes fmp: "f \<in> measure_preserving M \<mu> A \<nu>"
hoelzl@40859
  1295
  shows "f \<in> measure_preserving M \<mu> (sigma A) \<nu>"
hoelzl@38656
  1296
proof -
hoelzl@38656
  1297
  interpret sA: finite_measure ?sA \<nu> by fact
hoelzl@38656
  1298
  interpret A: algebra A by fact
hoelzl@38656
  1299
  show ?thesis using fmp
hoelzl@38656
  1300
    proof (clarsimp simp add: measure_preserving_def)
hoelzl@38656
  1301
      assume fm: "f \<in> measurable M A"
hoelzl@38656
  1302
         and meq: "\<forall>y\<in>sets A. \<mu> (f -` y \<inter> space M) = \<nu> y"
hoelzl@38656
  1303
      have f12: "f \<in> measurable M ?sA"
hoelzl@38656
  1304
        using measurable_subset[OF A.sets_into_space] fm by auto
hoelzl@38656
  1305
      hence ffn: "f \<in> space M \<rightarrow> space A"
hoelzl@38656
  1306
        by (simp add: measurable_def)
hoelzl@38656
  1307
      have "space M \<subseteq> f -` (space A)"
hoelzl@38656
  1308
        by auto (metis PiE ffn)
hoelzl@38656
  1309
      hence fveq [simp]: "(f -` (space A)) \<inter> space M = space M"
hoelzl@38656
  1310
        by blast
hoelzl@38656
  1311
      {
hoelzl@38656
  1312
        fix y
hoelzl@38656
  1313
        assume y: "y \<in> sets ?sA"
hoelzl@38656
  1314
        have "sets ?sA = sigma_sets (space A) (sets A)" (is "_ = ?A") by (auto simp: sigma_def)
hoelzl@38656
  1315
        also have "\<dots> \<subseteq> {s . \<mu> ((f -` s) \<inter> space M) = \<nu> s}"
hoelzl@38656
  1316
          proof (rule A.sigma_property_disjoint, auto)
hoelzl@38656
  1317
            fix x assume "x \<in> sets A" then show "\<mu> (f -` x \<inter> space M) = \<nu> x" by (simp add: meq)
hoelzl@38656
  1318
          next
hoelzl@38656
  1319
            fix s
hoelzl@38656
  1320
            assume eq: "\<mu> (f -` s \<inter> space M) = \<nu> s" and s: "s \<in> ?A"
hoelzl@38656
  1321
            then have s': "s \<in> sets ?sA" by (simp add: sigma_def)
hoelzl@38656
  1322
            show "\<mu> (f -` (space A - s) \<inter> space M) = \<nu> (space A - s)"
hoelzl@38656
  1323
              using sA.finite_measure_compl[OF s']
hoelzl@38656
  1324
              using measurable_sets[OF f12 s'] meq[THEN bspec, OF A.top]
hoelzl@38656
  1325
              by (simp add: vimage_Diff Diff_Int_distrib2 finite_measure_compl eq)
hoelzl@38656
  1326
          next
hoelzl@38656
  1327
            fix S
hoelzl@38656
  1328
            assume S0: "S 0 = {}"
hoelzl@38656
  1329
               and SSuc: "\<And>n.  S n \<subseteq> S (Suc n)"
hoelzl@38656
  1330
               and rS1: "range S \<subseteq> {s. \<mu> (f -` s \<inter> space M) = \<nu> s}"
hoelzl@38656
  1331
               and "range S \<subseteq> ?A"
hoelzl@38656
  1332
            hence rS2: "range S \<subseteq> sets ?sA" by (simp add: sigma_def)
hoelzl@38656
  1333
            have eq1: "\<And>i. \<mu> (f -` S i \<inter> space M) = \<nu> (S i)"
hoelzl@38656
  1334
              using rS1 by blast
hoelzl@38656
  1335
            have *: "(\<lambda>n. \<nu> (S n)) = (\<lambda>n. \<mu> (f -` S n \<inter> space M))"
hoelzl@38656
  1336
              by (simp add: eq1)
hoelzl@38656
  1337
            have "(SUP n. ... n) = \<mu> (\<Union>i. f -` S i \<inter> space M)"
hoelzl@38656
  1338
              proof (rule measure_countable_increasing)
hoelzl@38656
  1339
                show "range (\<lambda>i. f -` S i \<inter> space M) \<subseteq> sets M"
hoelzl@38656
  1340
                  using f12 rS2 by (auto simp add: measurable_def)
hoelzl@38656
  1341
                show "f -` S 0 \<inter> space M = {}" using S0
hoelzl@38656
  1342
                  by blast
hoelzl@38656
  1343
                show "\<And>n. f -` S n \<inter> space M \<subseteq> f -` S (Suc n) \<inter> space M"
hoelzl@38656
  1344
                  using SSuc by auto
hoelzl@38656
  1345
              qed
hoelzl@38656
  1346
            also have "\<mu> (\<Union>i. f -` S i \<inter> space M) = \<mu> (f -` (\<Union>i. S i) \<inter> space M)"
hoelzl@38656
  1347
              by (simp add: vimage_UN)
hoelzl@38656
  1348
            finally have "(SUP n. \<nu> (S n)) = \<mu> (f -` (\<Union>i. S i) \<inter> space M)" unfolding * .
hoelzl@38656
  1349
            moreover
hoelzl@38656
  1350
            have "(SUP n. \<nu> (S n)) = \<nu> (\<Union>i. S i)"
hoelzl@38656
  1351
              by (rule sA.measure_countable_increasing[OF rS2, OF S0 SSuc])
hoelzl@38656
  1352
            ultimately
hoelzl@38656
  1353
            show "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<nu> (\<Union>i. S i)" by simp
hoelzl@38656
  1354
          next
hoelzl@38656
  1355
            fix S :: "nat => 'a2 set"
hoelzl@38656
  1356
              assume dS: "disjoint_family S"
hoelzl@38656
  1357
                 and rS1: "range S \<subseteq> {s. \<mu> (f -` s \<inter> space M) = \<nu> s}"
hoelzl@38656
  1358
                 and "range S \<subseteq> ?A"
hoelzl@38656
  1359
              hence rS2: "range S \<subseteq> sets ?sA" by (simp add: sigma_def)
hoelzl@38656
  1360
              have "\<And>i. \<mu> (f -` S i \<inter> space M) = \<nu> (S i)"
hoelzl@38656
  1361
                using rS1 by blast
hoelzl@38656
  1362
              hence *: "(\<lambda>i. \<nu> (S i)) = (\<lambda>n. \<mu> (f -` S n \<inter> space M))"
hoelzl@38656
  1363
                by simp
hoelzl@38656
  1364
              have "psuminf ... = \<mu> (\<Union>i. f -` S i \<inter> space M)"
hoelzl@38656
  1365
                proof (rule measure_countably_additive)
hoelzl@38656
  1366
                  show "range (\<lambda>i. f -` S i \<inter> space M) \<subseteq> sets M"
hoelzl@38656
  1367
                    using f12 rS2 by (auto simp add: measurable_def)
hoelzl@38656
  1368
                  show "disjoint_family (\<lambda>i. f -` S i \<inter> space M)" using dS
hoelzl@38656
  1369
                    by (auto simp add: disjoint_family_on_def)
hoelzl@38656
  1370
                qed
hoelzl@38656
  1371
              hence "(\<Sum>\<^isub>\<infinity> i. \<nu> (S i)) = \<mu> (\<Union>i. f -` S i \<inter> space M)" unfolding * .
hoelzl@38656
  1372
              with sA.measure_countably_additive [OF rS2 dS]
hoelzl@38656
  1373
              have "\<mu> (\<Union>i. f -` S i \<inter> space M) = \<nu> (\<Union>i. S i)"
hoelzl@38656
  1374
                by simp
hoelzl@38656
  1375
              moreover have "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<mu> (\<Union>i. f -` S i \<inter> space M)"
hoelzl@38656
  1376
                by (simp add: vimage_UN)
hoelzl@38656
  1377
              ultimately show "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<nu> (\<Union>i. S i)"
hoelzl@38656
  1378
                by metis
hoelzl@38656
  1379
          qed
hoelzl@38656
  1380
        finally have "sets ?sA \<subseteq> {s . \<mu> ((f -` s) \<inter> space M) = \<nu> s}" .
hoelzl@38656
  1381
        hence "\<mu> (f -` y \<inter> space M) = \<nu> y" using y by force
hoelzl@38656
  1382
      }
hoelzl@38656
  1383
      thus "f \<in> measurable M ?sA \<and> (\<forall>y\<in>sets ?sA. \<mu> (f -` y \<inter> space M) = \<nu> y)"
hoelzl@38656
  1384
        by (blast intro: f12)
hoelzl@38656
  1385
    qed
hoelzl@38656
  1386
qed
hoelzl@38656
  1387
hoelzl@38656
  1388
section "Finite spaces"
hoelzl@38656
  1389
hoelzl@40859
  1390
locale finite_measure_space = measure_space + finite_sigma_algebra +
hoelzl@40859
  1391
  assumes finite_single_measure[simp]: "\<And>x. x \<in> space M \<Longrightarrow> \<mu> {x} \<noteq> \<omega>"
hoelzl@39092
  1392
hoelzl@38656
  1393
lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)"
hoelzl@36624
  1394
  using measure_finitely_additive''[of "space M" "\<lambda>i. {i}"]
hoelzl@36624
  1395
  by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)
hoelzl@36624
  1396
hoelzl@39092
  1397
lemma finite_measure_spaceI:
hoelzl@39092
  1398
  assumes "finite (space M)" "sets M = Pow(space M)" and space: "\<mu> (space M) \<noteq> \<omega>"
hoelzl@39092
  1399
    and add: "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> \<mu> (A \<union> B) = \<mu> A + \<mu> B"
hoelzl@39092
  1400
    and "\<mu> {} = 0"
hoelzl@39092
  1401
  shows "finite_measure_space M \<mu>"
hoelzl@39092
  1402
    unfolding finite_measure_space_def finite_measure_space_axioms_def
hoelzl@40859
  1403
proof (intro allI impI conjI)
hoelzl@39092
  1404
  show "measure_space M \<mu>"
hoelzl@39092
  1405
  proof (rule sigma_algebra.finite_additivity_sufficient)
hoelzl@40859
  1406
    have *: "\<lparr>space = space M, sets = sets M\<rparr> = M" by auto
hoelzl@39092
  1407
    show "sigma_algebra M"
hoelzl@40859
  1408
      using sigma_algebra_Pow[of "space M" "more M"] assms(2)[symmetric] by (simp add: *)
hoelzl@39092
  1409
    show "finite (space M)" by fact
hoelzl@39092
  1410
    show "positive \<mu>" unfolding positive_def by fact
hoelzl@39092
  1411
    show "additive M \<mu>" unfolding additive_def using assms by simp
hoelzl@39092
  1412
  qed
hoelzl@40859
  1413
  then interpret measure_space M \<mu> .
hoelzl@40859
  1414
  show "finite_sigma_algebra M"
hoelzl@40859
  1415
  proof
hoelzl@40859
  1416
    show "finite (space M)" by fact
hoelzl@40859
  1417
    show "sets M = Pow (space M)" using assms by auto
hoelzl@40859
  1418
  qed
hoelzl@39092
  1419
  { fix x assume *: "x \<in> space M"
hoelzl@39092
  1420
    with add[of "{x}" "space M - {x}"] space
hoelzl@39092
  1421
    show "\<mu> {x} \<noteq> \<omega>" by (auto simp: insert_absorb[OF *] Diff_subset) }
hoelzl@39092
  1422
qed
hoelzl@39092
  1423
hoelzl@40871
  1424
sublocale finite_measure_space \<subseteq> finite_measure
hoelzl@38656
  1425
proof
hoelzl@38656
  1426
  show "\<mu> (space M) \<noteq> \<omega>"
hoelzl@38656
  1427
    unfolding sum_over_space[symmetric] setsum_\<omega>
hoelzl@38656
  1428
    using finite_space finite_single_measure by auto
hoelzl@38656
  1429
qed
hoelzl@38656
  1430
hoelzl@39092
  1431
lemma finite_measure_space_iff:
hoelzl@39092
  1432
  "finite_measure_space M \<mu> \<longleftrightarrow>
hoelzl@39092
  1433
    finite (space M) \<and> sets M = Pow(space M) \<and> \<mu> (space M) \<noteq> \<omega> \<and> \<mu> {} = 0 \<and>
hoelzl@39092
  1434
    (\<forall>A\<subseteq>space M. \<forall>B\<subseteq>space M. A \<inter> B = {} \<longrightarrow> \<mu> (A \<union> B) = \<mu> A + \<mu> B)"
hoelzl@39092
  1435
    (is "_ = ?rhs")
hoelzl@39092
  1436
proof (intro iffI)
hoelzl@39092
  1437
  assume "finite_measure_space M \<mu>"
hoelzl@39092
  1438
  then interpret finite_measure_space M \<mu> .
hoelzl@39092
  1439
  show ?rhs
hoelzl@39092
  1440
    using finite_space sets_eq_Pow measure_additive empty_measure finite_measure
hoelzl@39092
  1441
    by auto
hoelzl@39092
  1442
next
hoelzl@39092
  1443
  assume ?rhs then show "finite_measure_space M \<mu>"
hoelzl@39092
  1444
    by (auto intro!: finite_measure_spaceI)
hoelzl@39092
  1445
qed
hoelzl@39092
  1446
hoelzl@38656
  1447
lemma psuminf_cmult_indicator:
hoelzl@38656
  1448
  assumes "disjoint_family A" "x \<in> A i"
hoelzl@38656
  1449
  shows "(\<Sum>\<^isub>\<infinity> n. f n * indicator (A n) x) = f i"
hoelzl@38656
  1450
proof -
hoelzl@41023
  1451
  have **: "\<And>n. f n * indicator (A n) x = (if n = i then f n else 0 :: pextreal)"
hoelzl@38656
  1452
    using `x \<in> A i` assms unfolding disjoint_family_on_def indicator_def by auto
hoelzl@41023
  1453
  then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: pextreal)"
hoelzl@38656
  1454
    by (auto simp: setsum_cases)
hoelzl@41023
  1455
  moreover have "(SUP n. if i < n then f i else 0) = (f i :: pextreal)"