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