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