src/HOL/Probability/Radon_Nikodym.thy
author hoelzl
Wed Dec 01 19:20:30 2010 +0100 (2010-12-01)
changeset 40859 de0b30e6c2d2
parent 39097 943c7b348524
child 40871 688f6ff859e1
permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
hoelzl@38656
     1
theory Radon_Nikodym
hoelzl@38656
     2
imports Lebesgue_Integration
hoelzl@38656
     3
begin
hoelzl@38656
     4
hoelzl@40859
     5
lemma less_\<omega>_Ex_of_nat: "x < \<omega> \<longleftrightarrow> (\<exists>n. x < of_nat n)"
hoelzl@40859
     6
proof safe
hoelzl@40859
     7
  assume "x < \<omega>"
hoelzl@40859
     8
  then obtain r where "0 \<le> r" "x = Real r" by (cases x) auto
hoelzl@40859
     9
  moreover obtain n where "r < of_nat n" using ex_less_of_nat by auto
hoelzl@40859
    10
  ultimately show "\<exists>n. x < of_nat n" by (auto simp: real_eq_of_nat)
hoelzl@40859
    11
qed auto
hoelzl@40859
    12
hoelzl@38656
    13
lemma (in sigma_finite_measure) Ex_finite_integrable_function:
hoelzl@38656
    14
  shows "\<exists>h\<in>borel_measurable M. positive_integral h \<noteq> \<omega> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<omega>)"
hoelzl@38656
    15
proof -
hoelzl@38656
    16
  obtain A :: "nat \<Rightarrow> 'a set" where
hoelzl@38656
    17
    range: "range A \<subseteq> sets M" and
hoelzl@38656
    18
    space: "(\<Union>i. A i) = space M" and
hoelzl@38656
    19
    measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>" and
hoelzl@38656
    20
    disjoint: "disjoint_family A"
hoelzl@38656
    21
    using disjoint_sigma_finite by auto
hoelzl@38656
    22
  let "?B i" = "2^Suc i * \<mu> (A i)"
hoelzl@38656
    23
  have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
hoelzl@38656
    24
  proof
hoelzl@38656
    25
    fix i show "\<exists>x. 0 < x \<and> x < inverse (?B i)"
hoelzl@38656
    26
    proof cases
hoelzl@38656
    27
      assume "\<mu> (A i) = 0"
hoelzl@38656
    28
      then show ?thesis by (auto intro!: exI[of _ 1])
hoelzl@38656
    29
    next
hoelzl@38656
    30
      assume not_0: "\<mu> (A i) \<noteq> 0"
hoelzl@38656
    31
      then have "?B i \<noteq> \<omega>" using measure[of i] by auto
hoelzl@38656
    32
      then have "inverse (?B i) \<noteq> 0" unfolding pinfreal_inverse_eq_0 by simp
hoelzl@38656
    33
      then show ?thesis using measure[of i] not_0
hoelzl@38656
    34
        by (auto intro!: exI[of _ "inverse (?B i) / 2"]
hoelzl@38656
    35
                 simp: pinfreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq)
hoelzl@38656
    36
    qed
hoelzl@38656
    37
  qed
hoelzl@38656
    38
  from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
hoelzl@38656
    39
    "\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
hoelzl@38656
    40
  let "?h x" = "\<Sum>\<^isub>\<infinity> i. n i * indicator (A i) x"
hoelzl@38656
    41
  show ?thesis
hoelzl@38656
    42
  proof (safe intro!: bexI[of _ ?h] del: notI)
hoelzl@39092
    43
    have "\<And>i. A i \<in> sets M"
hoelzl@39092
    44
      using range by fastsimp+
hoelzl@39092
    45
    then have "positive_integral ?h = (\<Sum>\<^isub>\<infinity> i. n i * \<mu> (A i))"
hoelzl@39092
    46
      by (simp add: positive_integral_psuminf positive_integral_cmult_indicator)
hoelzl@38656
    47
    also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. Real ((1 / 2)^Suc i))"
hoelzl@38656
    48
    proof (rule psuminf_le)
hoelzl@38656
    49
      fix N show "n N * \<mu> (A N) \<le> Real ((1 / 2) ^ Suc N)"
hoelzl@38656
    50
        using measure[of N] n[of N]
hoelzl@39092
    51
        by (cases "n N")
hoelzl@39092
    52
           (auto simp: pinfreal_noteq_omega_Ex field_simps zero_le_mult_iff
hoelzl@39092
    53
                       mult_le_0_iff mult_less_0_iff power_less_zero_eq
hoelzl@39092
    54
                       power_le_zero_eq inverse_eq_divide less_divide_eq
hoelzl@39092
    55
                       power_divide split: split_if_asm)
hoelzl@38656
    56
    qed
hoelzl@38656
    57
    also have "\<dots> = Real 1"
hoelzl@38656
    58
      by (rule suminf_imp_psuminf, rule power_half_series, auto)
hoelzl@38656
    59
    finally show "positive_integral ?h \<noteq> \<omega>" by auto
hoelzl@38656
    60
  next
hoelzl@38656
    61
    fix x assume "x \<in> space M"
hoelzl@38656
    62
    then obtain i where "x \<in> A i" using space[symmetric] by auto
hoelzl@38656
    63
    from psuminf_cmult_indicator[OF disjoint, OF this]
hoelzl@38656
    64
    have "?h x = n i" by simp
hoelzl@38656
    65
    then show "0 < ?h x" and "?h x < \<omega>" using n[of i] by auto
hoelzl@38656
    66
  next
hoelzl@38656
    67
    show "?h \<in> borel_measurable M" using range
hoelzl@39092
    68
      by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times)
hoelzl@38656
    69
  qed
hoelzl@38656
    70
qed
hoelzl@38656
    71
hoelzl@38656
    72
definition (in measure_space)
hoelzl@38656
    73
  "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pinfreal))"
hoelzl@38656
    74
hoelzl@40859
    75
lemma (in sigma_finite_measure) absolutely_continuous_AE:
hoelzl@40859
    76
  assumes "measure_space M \<nu>" "absolutely_continuous \<nu>" "AE x. P x"
hoelzl@40859
    77
  shows "measure_space.almost_everywhere M \<nu> P"
hoelzl@40859
    78
proof -
hoelzl@40859
    79
  interpret \<nu>: measure_space M \<nu> by fact
hoelzl@40859
    80
  from `AE x. P x` obtain N where N: "N \<in> null_sets" and "{x\<in>space M. \<not> P x} \<subseteq> N"
hoelzl@40859
    81
    unfolding almost_everywhere_def by auto
hoelzl@40859
    82
  show "\<nu>.almost_everywhere P"
hoelzl@40859
    83
  proof (rule \<nu>.AE_I')
hoelzl@40859
    84
    show "{x\<in>space M. \<not> P x} \<subseteq> N" by fact
hoelzl@40859
    85
    from `absolutely_continuous \<nu>` show "N \<in> \<nu>.null_sets"
hoelzl@40859
    86
      using N unfolding absolutely_continuous_def by auto
hoelzl@40859
    87
  qed
hoelzl@40859
    88
qed
hoelzl@40859
    89
hoelzl@39097
    90
lemma (in finite_measure_space) absolutely_continuousI:
hoelzl@39097
    91
  assumes "finite_measure_space M \<nu>"
hoelzl@39097
    92
  assumes v: "\<And>x. \<lbrakk> x \<in> space M ; \<mu> {x} = 0 \<rbrakk> \<Longrightarrow> \<nu> {x} = 0"
hoelzl@39097
    93
  shows "absolutely_continuous \<nu>"
hoelzl@39097
    94
proof (unfold absolutely_continuous_def sets_eq_Pow, safe)
hoelzl@39097
    95
  fix N assume "\<mu> N = 0" "N \<subseteq> space M"
hoelzl@39097
    96
  interpret v: finite_measure_space M \<nu> by fact
hoelzl@39097
    97
  have "\<nu> N = \<nu> (\<Union>x\<in>N. {x})" by simp
hoelzl@39097
    98
  also have "\<dots> = (\<Sum>x\<in>N. \<nu> {x})"
hoelzl@39097
    99
  proof (rule v.measure_finitely_additive''[symmetric])
hoelzl@39097
   100
    show "finite N" using `N \<subseteq> space M` finite_space by (auto intro: finite_subset)
hoelzl@39097
   101
    show "disjoint_family_on (\<lambda>i. {i}) N" unfolding disjoint_family_on_def by auto
hoelzl@39097
   102
    fix x assume "x \<in> N" thus "{x} \<in> sets M" using `N \<subseteq> space M` sets_eq_Pow by auto
hoelzl@39097
   103
  qed
hoelzl@39097
   104
  also have "\<dots> = 0"
hoelzl@39097
   105
  proof (safe intro!: setsum_0')
hoelzl@39097
   106
    fix x assume "x \<in> N"
hoelzl@39097
   107
    hence "\<mu> {x} \<le> \<mu> N" using sets_eq_Pow `N \<subseteq> space M` by (auto intro!: measure_mono)
hoelzl@39097
   108
    hence "\<mu> {x} = 0" using `\<mu> N = 0` by simp
hoelzl@39097
   109
    thus "\<nu> {x} = 0" using v[of x] `x \<in> N` `N \<subseteq> space M` by auto
hoelzl@39097
   110
  qed
hoelzl@39097
   111
  finally show "\<nu> N = 0" .
hoelzl@39097
   112
qed
hoelzl@39097
   113
hoelzl@38656
   114
lemma (in finite_measure) Radon_Nikodym_aux_epsilon:
hoelzl@38656
   115
  fixes e :: real assumes "0 < e"
hoelzl@38656
   116
  assumes "finite_measure M s"
hoelzl@38656
   117
  shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
hoelzl@38656
   118
                    real (\<mu> A) - real (s A) \<and>
hoelzl@38656
   119
                    (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < real (\<mu> B) - real (s B))"
hoelzl@38656
   120
proof -
hoelzl@38656
   121
  let "?d A" = "real (\<mu> A) - real (s A)"
hoelzl@38656
   122
  interpret M': finite_measure M s by fact
hoelzl@38656
   123
hoelzl@38656
   124
  let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
hoelzl@38656
   125
    then {}
hoelzl@38656
   126
    else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
hoelzl@38656
   127
  def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
hoelzl@38656
   128
hoelzl@38656
   129
  have A_simps[simp]:
hoelzl@38656
   130
    "A 0 = {}"
hoelzl@38656
   131
    "\<And>n. A (Suc n) = (A n \<union> ?A (A n))" unfolding A_def by simp_all
hoelzl@38656
   132
hoelzl@38656
   133
  { fix A assume "A \<in> sets M"
hoelzl@38656
   134
    have "?A A \<in> sets M"
hoelzl@38656
   135
      by (auto intro!: someI2[of _ _ "\<lambda>A. A \<in> sets M"] simp: not_less) }
hoelzl@38656
   136
  note A'_in_sets = this
hoelzl@38656
   137
hoelzl@38656
   138
  { fix n have "A n \<in> sets M"
hoelzl@38656
   139
    proof (induct n)
hoelzl@38656
   140
      case (Suc n) thus "A (Suc n) \<in> sets M"
hoelzl@38656
   141
        using A'_in_sets[of "A n"] by (auto split: split_if_asm)
hoelzl@38656
   142
    qed (simp add: A_def) }
hoelzl@38656
   143
  note A_in_sets = this
hoelzl@38656
   144
  hence "range A \<subseteq> sets M" by auto
hoelzl@38656
   145
hoelzl@38656
   146
  { fix n B
hoelzl@38656
   147
    assume Ex: "\<exists>B. B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> -e"
hoelzl@38656
   148
    hence False: "\<not> (\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B)" by (auto simp: not_less)
hoelzl@38656
   149
    have "?d (A (Suc n)) \<le> ?d (A n) - e" unfolding A_simps if_not_P[OF False]
hoelzl@38656
   150
    proof (rule someI2_ex[OF Ex])
hoelzl@38656
   151
      fix B assume "B \<in> sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
hoelzl@38656
   152
      hence "A n \<inter> B = {}" "B \<in> sets M" and dB: "?d B \<le> -e" by auto
hoelzl@38656
   153
      hence "?d (A n \<union> B) = ?d (A n) + ?d B"
hoelzl@38656
   154
        using `A n \<in> sets M` real_finite_measure_Union M'.real_finite_measure_Union by simp
hoelzl@38656
   155
      also have "\<dots> \<le> ?d (A n) - e" using dB by simp
hoelzl@38656
   156
      finally show "?d (A n \<union> B) \<le> ?d (A n) - e" .
hoelzl@38656
   157
    qed }
hoelzl@38656
   158
  note dA_epsilon = this
hoelzl@38656
   159
hoelzl@38656
   160
  { fix n have "?d (A (Suc n)) \<le> ?d (A n)"
hoelzl@38656
   161
    proof (cases "\<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e")
hoelzl@38656
   162
      case True from dA_epsilon[OF this] show ?thesis using `0 < e` by simp
hoelzl@38656
   163
    next
hoelzl@38656
   164
      case False
hoelzl@38656
   165
      hence "\<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B" by (auto simp: not_le)
hoelzl@38656
   166
      thus ?thesis by simp
hoelzl@38656
   167
    qed }
hoelzl@38656
   168
  note dA_mono = this
hoelzl@38656
   169
hoelzl@38656
   170
  show ?thesis
hoelzl@38656
   171
  proof (cases "\<exists>n. \<forall>B\<in>sets M. B \<subseteq> space M - A n \<longrightarrow> -e < ?d B")
hoelzl@38656
   172
    case True then obtain n where B: "\<And>B. \<lbrakk> B \<in> sets M; B \<subseteq> space M - A n\<rbrakk> \<Longrightarrow> -e < ?d B" by blast
hoelzl@38656
   173
    show ?thesis
hoelzl@38656
   174
    proof (safe intro!: bexI[of _ "space M - A n"])
hoelzl@38656
   175
      fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
hoelzl@38656
   176
      from B[OF this] show "-e < ?d B" .
hoelzl@38656
   177
    next
hoelzl@38656
   178
      show "space M - A n \<in> sets M" by (rule compl_sets) fact
hoelzl@38656
   179
    next
hoelzl@38656
   180
      show "?d (space M) \<le> ?d (space M - A n)"
hoelzl@38656
   181
      proof (induct n)
hoelzl@38656
   182
        fix n assume "?d (space M) \<le> ?d (space M - A n)"
hoelzl@38656
   183
        also have "\<dots> \<le> ?d (space M - A (Suc n))"
hoelzl@38656
   184
          using A_in_sets sets_into_space dA_mono[of n]
hoelzl@38656
   185
            real_finite_measure_Diff[of "space M"]
hoelzl@38656
   186
            real_finite_measure_Diff[of "space M"]
hoelzl@38656
   187
            M'.real_finite_measure_Diff[of "space M"]
hoelzl@38656
   188
            M'.real_finite_measure_Diff[of "space M"]
hoelzl@38656
   189
          by (simp del: A_simps)
hoelzl@38656
   190
        finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
hoelzl@38656
   191
      qed simp
hoelzl@38656
   192
    qed
hoelzl@38656
   193
  next
hoelzl@38656
   194
    case False hence B: "\<And>n. \<exists>B. B\<in>sets M \<and> B \<subseteq> space M - A n \<and> ?d B \<le> - e"
hoelzl@38656
   195
      by (auto simp add: not_less)
hoelzl@38656
   196
    { fix n have "?d (A n) \<le> - real n * e"
hoelzl@38656
   197
      proof (induct n)
hoelzl@38656
   198
        case (Suc n) with dA_epsilon[of n, OF B] show ?case by (simp del: A_simps add: real_of_nat_Suc field_simps)
hoelzl@38656
   199
      qed simp } note dA_less = this
hoelzl@38656
   200
    have decseq: "decseq (\<lambda>n. ?d (A n))" unfolding decseq_eq_incseq
hoelzl@38656
   201
    proof (rule incseq_SucI)
hoelzl@38656
   202
      fix n show "- ?d (A n) \<le> - ?d (A (Suc n))" using dA_mono[of n] by auto
hoelzl@38656
   203
    qed
hoelzl@38656
   204
    from real_finite_continuity_from_below[of A] `range A \<subseteq> sets M`
hoelzl@38656
   205
      M'.real_finite_continuity_from_below[of A]
hoelzl@38656
   206
    have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
hoelzl@38656
   207
      by (auto intro!: LIMSEQ_diff)
hoelzl@38656
   208
    obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
hoelzl@38656
   209
    moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
hoelzl@38656
   210
    have "real n \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
hoelzl@38656
   211
    ultimately show ?thesis by auto
hoelzl@38656
   212
  qed
hoelzl@38656
   213
qed
hoelzl@38656
   214
hoelzl@38656
   215
lemma (in finite_measure) Radon_Nikodym_aux:
hoelzl@38656
   216
  assumes "finite_measure M s"
hoelzl@38656
   217
  shows "\<exists>A\<in>sets M. real (\<mu> (space M)) - real (s (space M)) \<le>
hoelzl@38656
   218
                    real (\<mu> A) - real (s A) \<and>
hoelzl@38656
   219
                    (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> 0 \<le> real (\<mu> B) - real (s B))"
hoelzl@38656
   220
proof -
hoelzl@38656
   221
  let "?d A" = "real (\<mu> A) - real (s A)"
hoelzl@38656
   222
  let "?P A B n" = "A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
hoelzl@38656
   223
hoelzl@38656
   224
  interpret M': finite_measure M s by fact
hoelzl@38656
   225
hoelzl@39092
   226
  let "?r S" = "restricted_space S"
hoelzl@38656
   227
hoelzl@38656
   228
  { fix S n
hoelzl@38656
   229
    assume S: "S \<in> sets M"
hoelzl@38656
   230
    hence **: "\<And>X. X \<in> op \<inter> S ` sets M \<longleftrightarrow> X \<in> sets M \<and> X \<subseteq> S" by auto
hoelzl@38656
   231
    from M'.restricted_finite_measure[of S] restricted_finite_measure[of S] S
hoelzl@38656
   232
    have "finite_measure (?r S) \<mu>" "0 < 1 / real (Suc n)"
hoelzl@38656
   233
      "finite_measure (?r S) s" by auto
hoelzl@38656
   234
    from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X ..
hoelzl@38656
   235
    hence "?P X S n"
hoelzl@38656
   236
    proof (simp add: **, safe)
hoelzl@38656
   237
      fix C assume C: "C \<in> sets M" "C \<subseteq> X" "X \<subseteq> S" and
hoelzl@38656
   238
        *: "\<forall>B\<in>sets M. S \<inter> B \<subseteq> X \<longrightarrow> - (1 / real (Suc n)) < ?d (S \<inter> B)"
hoelzl@38656
   239
      hence "C \<subseteq> S" "C \<subseteq> X" "S \<inter> C = C" by auto
hoelzl@38656
   240
      with *[THEN bspec, OF `C \<in> sets M`]
hoelzl@38656
   241
      show "- (1 / real (Suc n)) < ?d C" by auto
hoelzl@38656
   242
    qed
hoelzl@38656
   243
    hence "\<exists>A. ?P A S n" by auto }
hoelzl@38656
   244
  note Ex_P = this
hoelzl@38656
   245
hoelzl@38656
   246
  def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
hoelzl@38656
   247
  have A_Suc: "\<And>n. A (Suc n) = (SOME B. ?P B (A n) n)" by (simp add: A_def)
hoelzl@38656
   248
  have A_0[simp]: "A 0 = space M" unfolding A_def by simp
hoelzl@38656
   249
hoelzl@38656
   250
  { fix i have "A i \<in> sets M" unfolding A_def
hoelzl@38656
   251
    proof (induct i)
hoelzl@38656
   252
      case (Suc i)
hoelzl@38656
   253
      from Ex_P[OF this, of i] show ?case unfolding nat_rec_Suc
hoelzl@38656
   254
        by (rule someI2_ex) simp
hoelzl@38656
   255
    qed simp }
hoelzl@38656
   256
  note A_in_sets = this
hoelzl@38656
   257
hoelzl@38656
   258
  { fix n have "?P (A (Suc n)) (A n) n"
hoelzl@38656
   259
      using Ex_P[OF A_in_sets] unfolding A_Suc
hoelzl@38656
   260
      by (rule someI2_ex) simp }
hoelzl@38656
   261
  note P_A = this
hoelzl@38656
   262
hoelzl@38656
   263
  have "range A \<subseteq> sets M" using A_in_sets by auto
hoelzl@38656
   264
hoelzl@38656
   265
  have A_mono: "\<And>i. A (Suc i) \<subseteq> A i" using P_A by simp
hoelzl@38656
   266
  have mono_dA: "mono (\<lambda>i. ?d (A i))" using P_A by (simp add: mono_iff_le_Suc)
hoelzl@38656
   267
  have epsilon: "\<And>C i. \<lbrakk> C \<in> sets M; C \<subseteq> A (Suc i) \<rbrakk> \<Longrightarrow> - 1 / real (Suc i) < ?d C"
hoelzl@38656
   268
      using P_A by auto
hoelzl@38656
   269
hoelzl@38656
   270
  show ?thesis
hoelzl@38656
   271
  proof (safe intro!: bexI[of _ "\<Inter>i. A i"])
hoelzl@38656
   272
    show "(\<Inter>i. A i) \<in> sets M" using A_in_sets by auto
hoelzl@38656
   273
    from `range A \<subseteq> sets M` A_mono
hoelzl@38656
   274
      real_finite_continuity_from_above[of A]
hoelzl@38656
   275
      M'.real_finite_continuity_from_above[of A]
hoelzl@38656
   276
    have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (auto intro!: LIMSEQ_diff)
hoelzl@38656
   277
    thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
hoelzl@38656
   278
      by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
hoelzl@38656
   279
  next
hoelzl@38656
   280
    fix B assume B: "B \<in> sets M" "B \<subseteq> (\<Inter>i. A i)"
hoelzl@38656
   281
    show "0 \<le> ?d B"
hoelzl@38656
   282
    proof (rule ccontr)
hoelzl@38656
   283
      assume "\<not> 0 \<le> ?d B"
hoelzl@38656
   284
      hence "0 < - ?d B" by auto
hoelzl@38656
   285
      from ex_inverse_of_nat_Suc_less[OF this]
hoelzl@38656
   286
      obtain n where *: "?d B < - 1 / real (Suc n)"
hoelzl@38656
   287
        by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
hoelzl@38656
   288
      have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat_rec_Suc)
hoelzl@38656
   289
      from epsilon[OF B(1) this] *
hoelzl@38656
   290
      show False by auto
hoelzl@38656
   291
    qed
hoelzl@38656
   292
  qed
hoelzl@38656
   293
qed
hoelzl@38656
   294
hoelzl@38656
   295
lemma (in finite_measure) Radon_Nikodym_finite_measure:
hoelzl@38656
   296
  assumes "finite_measure M \<nu>"
hoelzl@38656
   297
  assumes "absolutely_continuous \<nu>"
hoelzl@38656
   298
  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@38656
   299
proof -
hoelzl@38656
   300
  interpret M': finite_measure M \<nu> using assms(1) .
hoelzl@38656
   301
hoelzl@38656
   302
  def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A}"
hoelzl@38656
   303
  have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
hoelzl@38656
   304
  hence "G \<noteq> {}" by auto
hoelzl@38656
   305
hoelzl@38656
   306
  { fix f g assume f: "f \<in> G" and g: "g \<in> G"
hoelzl@38656
   307
    have "(\<lambda>x. max (g x) (f x)) \<in> G" (is "?max \<in> G") unfolding G_def
hoelzl@38656
   308
    proof safe
hoelzl@38656
   309
      show "?max \<in> borel_measurable M" using f g unfolding G_def by auto
hoelzl@38656
   310
hoelzl@38656
   311
      let ?A = "{x \<in> space M. f x \<le> g x}"
hoelzl@38656
   312
      have "?A \<in> sets M" using f g unfolding G_def by auto
hoelzl@38656
   313
hoelzl@38656
   314
      fix A assume "A \<in> sets M"
hoelzl@38656
   315
      hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
hoelzl@38656
   316
      have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
hoelzl@38656
   317
        using sets_into_space[OF `A \<in> sets M`] by auto
hoelzl@38656
   318
hoelzl@38656
   319
      have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
hoelzl@38656
   320
        g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
hoelzl@38656
   321
        by (auto simp: indicator_def max_def)
hoelzl@38656
   322
      hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
hoelzl@38656
   323
        positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
hoelzl@38656
   324
        positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
hoelzl@38656
   325
        using f g sets unfolding G_def
hoelzl@38656
   326
        by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
hoelzl@38656
   327
      also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
hoelzl@38656
   328
        using f g sets unfolding G_def by (auto intro!: add_mono)
hoelzl@38656
   329
      also have "\<dots> = \<nu> A"
hoelzl@38656
   330
        using M'.measure_additive[OF sets] union by auto
hoelzl@38656
   331
      finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
hoelzl@38656
   332
    qed }
hoelzl@38656
   333
  note max_in_G = this
hoelzl@38656
   334
hoelzl@38656
   335
  { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
hoelzl@38656
   336
    have "g \<in> G" unfolding G_def
hoelzl@38656
   337
    proof safe
hoelzl@38656
   338
      from `f \<up> g` have [simp]: "g = (SUP i. f i)" unfolding isoton_def by simp
hoelzl@38656
   339
      have f_borel: "\<And>i. f i \<in> borel_measurable M" using f unfolding G_def by simp
hoelzl@38656
   340
      thus "g \<in> borel_measurable M" by (auto intro!: borel_measurable_SUP)
hoelzl@38656
   341
hoelzl@38656
   342
      fix A assume "A \<in> sets M"
hoelzl@38656
   343
      hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
hoelzl@38656
   344
        using f_borel by (auto intro!: borel_measurable_indicator)
hoelzl@38656
   345
      from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
hoelzl@38656
   346
      have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
hoelzl@38656
   347
          (SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
hoelzl@38656
   348
        unfolding isoton_def by simp
hoelzl@38656
   349
      show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
hoelzl@38656
   350
        using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
hoelzl@38656
   351
    qed }
hoelzl@38656
   352
  note SUP_in_G = this
hoelzl@38656
   353
hoelzl@38656
   354
  let ?y = "SUP g : G. positive_integral g"
hoelzl@38656
   355
  have "?y \<le> \<nu> (space M)" unfolding G_def
hoelzl@38656
   356
  proof (safe intro!: SUP_leI)
hoelzl@38656
   357
    fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
hoelzl@38656
   358
    from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
hoelzl@38656
   359
      by (simp cong: positive_integral_cong)
hoelzl@38656
   360
  qed
hoelzl@38656
   361
  hence "?y \<noteq> \<omega>" using M'.finite_measure_of_space by auto
hoelzl@38656
   362
  from SUPR_countable_SUPR[OF this `G \<noteq> {}`] guess ys .. note ys = this
hoelzl@38656
   363
  hence "\<forall>n. \<exists>g. g\<in>G \<and> positive_integral g = ys n"
hoelzl@38656
   364
  proof safe
hoelzl@38656
   365
    fix n assume "range ys \<subseteq> positive_integral ` G"
hoelzl@38656
   366
    hence "ys n \<in> positive_integral ` G" by auto
hoelzl@38656
   367
    thus "\<exists>g. g\<in>G \<and> positive_integral g = ys n" by auto
hoelzl@38656
   368
  qed
hoelzl@38656
   369
  from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. positive_integral (gs n) = ys n" by auto
hoelzl@38656
   370
  hence y_eq: "?y = (SUP i. positive_integral (gs i))" using ys by auto
hoelzl@38656
   371
  let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
hoelzl@38656
   372
  def f \<equiv> "SUP i. ?g i"
hoelzl@38656
   373
  have gs_not_empty: "\<And>i. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
hoelzl@38656
   374
  { fix i have "?g i \<in> G"
hoelzl@38656
   375
    proof (induct i)
hoelzl@38656
   376
      case 0 thus ?case by simp fact
hoelzl@38656
   377
    next
hoelzl@38656
   378
      case (Suc i)
hoelzl@38656
   379
      with Suc gs_not_empty `gs (Suc i) \<in> G` show ?case
hoelzl@38656
   380
        by (auto simp add: atMost_Suc intro!: max_in_G)
hoelzl@38656
   381
    qed }
hoelzl@38656
   382
  note g_in_G = this
hoelzl@38656
   383
  have "\<And>x. \<forall>i. ?g i x \<le> ?g (Suc i) x"
hoelzl@38656
   384
    using gs_not_empty by (simp add: atMost_Suc)
hoelzl@38656
   385
  hence isoton_g: "?g \<up> f" by (simp add: isoton_def le_fun_def f_def)
hoelzl@38656
   386
  from SUP_in_G[OF this g_in_G] have "f \<in> G" .
hoelzl@38656
   387
  hence [simp, intro]: "f \<in> borel_measurable M" unfolding G_def by auto
hoelzl@38656
   388
hoelzl@38656
   389
  have "(\<lambda>i. positive_integral (?g i)) \<up> positive_integral f"
hoelzl@38656
   390
    using isoton_g g_in_G by (auto intro!: positive_integral_isoton simp: G_def f_def)
hoelzl@38656
   391
  hence "positive_integral f = (SUP i. positive_integral (?g i))"
hoelzl@38656
   392
    unfolding isoton_def by simp
hoelzl@38656
   393
  also have "\<dots> = ?y"
hoelzl@38656
   394
  proof (rule antisym)
hoelzl@38656
   395
    show "(SUP i. positive_integral (?g i)) \<le> ?y"
hoelzl@38656
   396
      using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def)
hoelzl@38656
   397
    show "?y \<le> (SUP i. positive_integral (?g i))" unfolding y_eq
hoelzl@38656
   398
      by (auto intro!: SUP_mono positive_integral_mono Max_ge)
hoelzl@38656
   399
  qed
hoelzl@38656
   400
  finally have int_f_eq_y: "positive_integral f = ?y" .
hoelzl@38656
   401
hoelzl@38656
   402
  let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@38656
   403
hoelzl@38656
   404
  have "finite_measure M ?t"
hoelzl@38656
   405
  proof
hoelzl@38656
   406
    show "?t {} = 0" by simp
hoelzl@38656
   407
    show "?t (space M) \<noteq> \<omega>" using M'.finite_measure by simp
hoelzl@38656
   408
    show "countably_additive M ?t" unfolding countably_additive_def
hoelzl@38656
   409
    proof safe
hoelzl@38656
   410
      fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
hoelzl@38656
   411
      have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
hoelzl@38656
   412
        = positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
hoelzl@38656
   413
        using `range A \<subseteq> sets M`
hoelzl@38656
   414
        by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
hoelzl@38656
   415
      also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
hoelzl@38656
   416
        apply (rule positive_integral_cong)
hoelzl@38656
   417
        apply (subst psuminf_cmult_right)
hoelzl@38656
   418
        unfolding psuminf_indicator[OF `disjoint_family A`] ..
hoelzl@38656
   419
      finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
hoelzl@38656
   420
        = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
hoelzl@38656
   421
      moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
hoelzl@38656
   422
        using M'.measure_countably_additive A by (simp add: comp_def)
hoelzl@38656
   423
      moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
hoelzl@38656
   424
          using A `f \<in> G` unfolding G_def by auto
hoelzl@38656
   425
      moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
hoelzl@38656
   426
      moreover {
hoelzl@38656
   427
        have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
hoelzl@38656
   428
          using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
hoelzl@38656
   429
        also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pinfreal_less_\<omega>)
hoelzl@38656
   430
        finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
hoelzl@38656
   431
          by (simp add: pinfreal_less_\<omega>) }
hoelzl@38656
   432
      ultimately
hoelzl@38656
   433
      show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
hoelzl@38656
   434
        apply (subst psuminf_minus) by simp_all
hoelzl@38656
   435
    qed
hoelzl@38656
   436
  qed
hoelzl@38656
   437
  then interpret M: finite_measure M ?t .
hoelzl@38656
   438
hoelzl@38656
   439
  have ac: "absolutely_continuous ?t" using `absolutely_continuous \<nu>` unfolding absolutely_continuous_def by auto
hoelzl@38656
   440
hoelzl@38656
   441
  have upper_bound: "\<forall>A\<in>sets M. ?t A \<le> 0"
hoelzl@38656
   442
  proof (rule ccontr)
hoelzl@38656
   443
    assume "\<not> ?thesis"
hoelzl@38656
   444
    then obtain A where A: "A \<in> sets M" and pos: "0 < ?t A"
hoelzl@38656
   445
      by (auto simp: not_le)
hoelzl@38656
   446
    note pos
hoelzl@38656
   447
    also have "?t A \<le> ?t (space M)"
hoelzl@38656
   448
      using M.measure_mono[of A "space M"] A sets_into_space by simp
hoelzl@38656
   449
    finally have pos_t: "0 < ?t (space M)" by simp
hoelzl@38656
   450
    moreover
hoelzl@38656
   451
    hence pos_M: "0 < \<mu> (space M)"
hoelzl@38656
   452
      using ac top unfolding absolutely_continuous_def by auto
hoelzl@38656
   453
    moreover
hoelzl@38656
   454
    have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
hoelzl@38656
   455
      using `f \<in> G` unfolding G_def by auto
hoelzl@38656
   456
    hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
hoelzl@38656
   457
      using M'.finite_measure_of_space by auto
hoelzl@38656
   458
    moreover
hoelzl@38656
   459
    def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
hoelzl@38656
   460
    ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>"
hoelzl@38656
   461
      using M'.finite_measure_of_space
hoelzl@38656
   462
      by (auto simp: pinfreal_inverse_eq_0 finite_measure_of_space)
hoelzl@38656
   463
hoelzl@38656
   464
    have "finite_measure M (\<lambda>A. b * \<mu> A)" (is "finite_measure M ?b")
hoelzl@38656
   465
    proof
hoelzl@38656
   466
      show "?b {} = 0" by simp
hoelzl@38656
   467
      show "?b (space M) \<noteq> \<omega>" using finite_measure_of_space b by auto
hoelzl@38656
   468
      show "countably_additive M ?b"
hoelzl@38656
   469
        unfolding countably_additive_def psuminf_cmult_right
hoelzl@38656
   470
        using measure_countably_additive by auto
hoelzl@38656
   471
    qed
hoelzl@38656
   472
hoelzl@38656
   473
    from M.Radon_Nikodym_aux[OF this]
hoelzl@38656
   474
    obtain A0 where "A0 \<in> sets M" and
hoelzl@38656
   475
      space_less_A0: "real (?t (space M)) - real (b * \<mu> (space M)) \<le> real (?t A0) - real (b * \<mu> A0)" and
hoelzl@38656
   476
      *: "\<And>B. \<lbrakk> B \<in> sets M ; B \<subseteq> A0 \<rbrakk> \<Longrightarrow> 0 \<le> real (?t B) - real (b * \<mu> B)" by auto
hoelzl@38656
   477
    { fix B assume "B \<in> sets M" "B \<subseteq> A0"
hoelzl@38656
   478
      with *[OF this] have "b * \<mu> B \<le> ?t B"
hoelzl@38656
   479
        using M'.finite_measure b finite_measure
hoelzl@38656
   480
        by (cases "b * \<mu> B", cases "?t B") (auto simp: field_simps) }
hoelzl@38656
   481
    note bM_le_t = this
hoelzl@38656
   482
hoelzl@38656
   483
    let "?f0 x" = "f x + b * indicator A0 x"
hoelzl@38656
   484
hoelzl@38656
   485
    { fix A assume A: "A \<in> sets M"
hoelzl@38656
   486
      hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
hoelzl@38656
   487
      have "positive_integral (\<lambda>x. ?f0 x  * indicator A x) =
hoelzl@38656
   488
        positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
hoelzl@38656
   489
        by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
hoelzl@38656
   490
      hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
hoelzl@38656
   491
          positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
hoelzl@38656
   492
        using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
hoelzl@38656
   493
        by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
hoelzl@38656
   494
    note f0_eq = this
hoelzl@38656
   495
hoelzl@38656
   496
    { fix A assume A: "A \<in> sets M"
hoelzl@38656
   497
      hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
hoelzl@38656
   498
      have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
hoelzl@38656
   499
        using `f \<in> G` A unfolding G_def by auto
hoelzl@38656
   500
      note f0_eq[OF A]
hoelzl@38656
   501
      also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
hoelzl@38656
   502
          positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
hoelzl@38656
   503
        using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
hoelzl@38656
   504
        by (auto intro!: add_left_mono)
hoelzl@38656
   505
      also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
hoelzl@38656
   506
        using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
hoelzl@38656
   507
        by (auto intro!: add_left_mono)
hoelzl@38656
   508
      also have "\<dots> \<le> \<nu> A"
hoelzl@38656
   509
        using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
hoelzl@38656
   510
        by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
hoelzl@38656
   511
      finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
hoelzl@38656
   512
    hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
hoelzl@38656
   513
      by (auto intro!: borel_measurable_indicator borel_measurable_pinfreal_add borel_measurable_pinfreal_times)
hoelzl@38656
   514
hoelzl@38656
   515
    have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
hoelzl@38656
   516
      "b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>"
hoelzl@38656
   517
      using `A0 \<in> sets M` b
hoelzl@38656
   518
        finite_measure[of A0] M.finite_measure[of A0]
hoelzl@38656
   519
        finite_measure_of_space M.finite_measure_of_space
hoelzl@38656
   520
      by auto
hoelzl@38656
   521
hoelzl@38656
   522
    have int_f_finite: "positive_integral f \<noteq> \<omega>"
hoelzl@38656
   523
      using M'.finite_measure_of_space pos_t unfolding pinfreal_zero_less_diff_iff
hoelzl@38656
   524
      by (auto cong: positive_integral_cong)
hoelzl@38656
   525
hoelzl@38656
   526
    have "?t (space M) > b * \<mu> (space M)" unfolding b_def
hoelzl@38656
   527
      apply (simp add: field_simps)
hoelzl@38656
   528
      apply (subst mult_assoc[symmetric])
hoelzl@38656
   529
      apply (subst pinfreal_mult_inverse)
hoelzl@38656
   530
      using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M
hoelzl@38656
   531
      using pinfreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"]
hoelzl@38656
   532
      by simp_all
hoelzl@38656
   533
    hence  "0 < ?t (space M) - b * \<mu> (space M)"
hoelzl@38656
   534
      by (simp add: pinfreal_zero_less_diff_iff)
hoelzl@38656
   535
    also have "\<dots> \<le> ?t A0 - b * \<mu> A0"
hoelzl@38656
   536
      using space_less_A0 pos_M pos_t b real[unfolded pinfreal_noteq_omega_Ex] by auto
hoelzl@38656
   537
    finally have "b * \<mu> A0 < ?t A0" unfolding pinfreal_zero_less_diff_iff .
hoelzl@38656
   538
    hence "0 < ?t A0" by auto
hoelzl@38656
   539
    hence "0 < \<mu> A0" using ac unfolding absolutely_continuous_def
hoelzl@38656
   540
      using `A0 \<in> sets M` by auto
hoelzl@38656
   541
    hence "0 < b * \<mu> A0" using b by auto
hoelzl@38656
   542
hoelzl@38656
   543
    from int_f_finite this
hoelzl@38656
   544
    have "?y + 0 < positive_integral f + b * \<mu> A0" unfolding int_f_eq_y
hoelzl@38656
   545
      by (rule pinfreal_less_add)
hoelzl@38656
   546
    also have "\<dots> = positive_integral ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
hoelzl@38656
   547
      by (simp cong: positive_integral_cong)
hoelzl@38656
   548
    finally have "?y < positive_integral ?f0" by simp
hoelzl@38656
   549
hoelzl@38656
   550
    moreover from `?f0 \<in> G` have "positive_integral ?f0 \<le> ?y" by (auto intro!: le_SUPI)
hoelzl@38656
   551
    ultimately show False by auto
hoelzl@38656
   552
  qed
hoelzl@38656
   553
hoelzl@38656
   554
  show ?thesis
hoelzl@38656
   555
  proof (safe intro!: bexI[of _ f])
hoelzl@38656
   556
    fix A assume "A\<in>sets M"
hoelzl@38656
   557
    show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@38656
   558
    proof (rule antisym)
hoelzl@38656
   559
      show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
hoelzl@38656
   560
        using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
hoelzl@38656
   561
      show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@38656
   562
        using upper_bound[THEN bspec, OF `A \<in> sets M`]
hoelzl@38656
   563
         by (simp add: pinfreal_zero_le_diff)
hoelzl@38656
   564
    qed
hoelzl@38656
   565
  qed simp
hoelzl@38656
   566
qed
hoelzl@38656
   567
hoelzl@40859
   568
lemma (in finite_measure) split_space_into_finite_sets_and_rest:
hoelzl@38656
   569
  assumes "measure_space M \<nu>"
hoelzl@40859
   570
  assumes ac: "absolutely_continuous \<nu>"
hoelzl@40859
   571
  shows "\<exists>\<Omega>0\<in>sets M. \<exists>\<Omega>::nat\<Rightarrow>'a set. disjoint_family \<Omega> \<and> range \<Omega> \<subseteq> sets M \<and> \<Omega>0 = space M - (\<Union>i. \<Omega> i) \<and>
hoelzl@40859
   572
    (\<forall>A\<in>sets M. A \<subseteq> \<Omega>0 \<longrightarrow> (\<mu> A = 0 \<and> \<nu> A = 0) \<or> (\<mu> A > 0 \<and> \<nu> A = \<omega>)) \<and>
hoelzl@40859
   573
    (\<forall>i. \<nu> (\<Omega> i) \<noteq> \<omega>)"
hoelzl@38656
   574
proof -
hoelzl@38656
   575
  interpret v: measure_space M \<nu> by fact
hoelzl@38656
   576
  let ?Q = "{Q\<in>sets M. \<nu> Q \<noteq> \<omega>}"
hoelzl@38656
   577
  let ?a = "SUP Q:?Q. \<mu> Q"
hoelzl@38656
   578
hoelzl@38656
   579
  have "{} \<in> ?Q" using v.empty_measure by auto
hoelzl@38656
   580
  then have Q_not_empty: "?Q \<noteq> {}" by blast
hoelzl@38656
   581
hoelzl@38656
   582
  have "?a \<le> \<mu> (space M)" using sets_into_space
hoelzl@38656
   583
    by (auto intro!: SUP_leI measure_mono top)
hoelzl@38656
   584
  then have "?a \<noteq> \<omega>" using finite_measure_of_space
hoelzl@38656
   585
    by auto
hoelzl@38656
   586
  from SUPR_countable_SUPR[OF this Q_not_empty]
hoelzl@38656
   587
  obtain Q'' where "range Q'' \<subseteq> \<mu> ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
hoelzl@38656
   588
    by auto
hoelzl@38656
   589
  then have "\<forall>i. \<exists>Q'. Q'' i = \<mu> Q' \<and> Q' \<in> ?Q" by auto
hoelzl@38656
   590
  from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
hoelzl@38656
   591
    by auto
hoelzl@38656
   592
  then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
hoelzl@38656
   593
  let "?O n" = "\<Union>i\<le>n. Q' i"
hoelzl@38656
   594
  have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
hoelzl@38656
   595
  proof (rule continuity_from_below[of ?O])
hoelzl@38656
   596
    show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
hoelzl@38656
   597
    show "\<And>i. ?O i \<subseteq> ?O (Suc i)" by fastsimp
hoelzl@38656
   598
  qed
hoelzl@38656
   599
hoelzl@38656
   600
  have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto
hoelzl@38656
   601
hoelzl@38656
   602
  have O_sets: "\<And>i. ?O i \<in> sets M"
hoelzl@38656
   603
     using Q' by (auto intro!: finite_UN Un)
hoelzl@38656
   604
  then have O_in_G: "\<And>i. ?O i \<in> ?Q"
hoelzl@38656
   605
  proof (safe del: notI)
hoelzl@38656
   606
    fix i have "Q' ` {..i} \<subseteq> sets M"
hoelzl@38656
   607
      using Q' by (auto intro: finite_UN)
hoelzl@38656
   608
    with v.measure_finitely_subadditive[of "{.. i}" Q']
hoelzl@38656
   609
    have "\<nu> (?O i) \<le> (\<Sum>i\<le>i. \<nu> (Q' i))" by auto
hoelzl@38656
   610
    also have "\<dots> < \<omega>" unfolding setsum_\<omega> pinfreal_less_\<omega> using Q' by auto
hoelzl@38656
   611
    finally show "\<nu> (?O i) \<noteq> \<omega>" unfolding pinfreal_less_\<omega> by auto
hoelzl@38656
   612
  qed auto
hoelzl@38656
   613
  have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp
hoelzl@38656
   614
hoelzl@38656
   615
  have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric]
hoelzl@38656
   616
  proof (rule antisym)
hoelzl@38656
   617
    show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
hoelzl@38656
   618
      using Q' by (auto intro!: SUP_mono measure_mono finite_UN)
hoelzl@38656
   619
    show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUPR_def
hoelzl@38656
   620
    proof (safe intro!: Sup_mono, unfold bex_simps)
hoelzl@38656
   621
      fix i
hoelzl@38656
   622
      have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
hoelzl@38656
   623
      then show "\<exists>x. (x \<in> sets M \<and> \<nu> x \<noteq> \<omega>) \<and>
hoelzl@38656
   624
        \<mu> (\<Union>Q' ` {..i}) \<le> \<mu> x"
hoelzl@38656
   625
        using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
hoelzl@38656
   626
    qed
hoelzl@38656
   627
  qed
hoelzl@38656
   628
hoelzl@38656
   629
  let "?O_0" = "(\<Union>i. ?O i)"
hoelzl@38656
   630
  have "?O_0 \<in> sets M" using Q' by auto
hoelzl@38656
   631
hoelzl@40859
   632
  def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> Q' 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
hoelzl@38656
   633
  { fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
hoelzl@38656
   634
  note Q_sets = this
hoelzl@38656
   635
hoelzl@40859
   636
  show ?thesis
hoelzl@40859
   637
  proof (intro bexI exI conjI ballI impI allI)
hoelzl@40859
   638
    show "disjoint_family Q"
hoelzl@40859
   639
      by (fastsimp simp: disjoint_family_on_def Q_def
hoelzl@40859
   640
        split: nat.split_asm)
hoelzl@40859
   641
    show "range Q \<subseteq> sets M"
hoelzl@40859
   642
      using Q_sets by auto
hoelzl@38656
   643
hoelzl@40859
   644
    { fix A assume A: "A \<in> sets M" "A \<subseteq> space M - ?O_0"
hoelzl@40859
   645
      show "\<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<omega>"
hoelzl@40859
   646
      proof (rule disjCI, simp)
hoelzl@40859
   647
        assume *: "0 < \<mu> A \<longrightarrow> \<nu> A \<noteq> \<omega>"
hoelzl@40859
   648
        show "\<mu> A = 0 \<and> \<nu> A = 0"
hoelzl@40859
   649
        proof cases
hoelzl@40859
   650
          assume "\<mu> A = 0" moreover with ac A have "\<nu> A = 0"
hoelzl@40859
   651
            unfolding absolutely_continuous_def by auto
hoelzl@40859
   652
          ultimately show ?thesis by simp
hoelzl@40859
   653
        next
hoelzl@40859
   654
          assume "\<mu> A \<noteq> 0" with * have "\<nu> A \<noteq> \<omega>" by auto
hoelzl@40859
   655
          with A have "\<mu> ?O_0 + \<mu> A = \<mu> (?O_0 \<union> A)"
hoelzl@40859
   656
            using Q' by (auto intro!: measure_additive countable_UN)
hoelzl@40859
   657
          also have "\<dots> = (SUP i. \<mu> (?O i \<union> A))"
hoelzl@40859
   658
          proof (rule continuity_from_below[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
hoelzl@40859
   659
            show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
hoelzl@40859
   660
              using `\<nu> A \<noteq> \<omega>` O_sets A by auto
hoelzl@40859
   661
          qed fastsimp
hoelzl@40859
   662
          also have "\<dots> \<le> ?a"
hoelzl@40859
   663
          proof (safe intro!: SUPR_bound)
hoelzl@40859
   664
            fix i have "?O i \<union> A \<in> ?Q"
hoelzl@40859
   665
            proof (safe del: notI)
hoelzl@40859
   666
              show "?O i \<union> A \<in> sets M" using O_sets A by auto
hoelzl@40859
   667
              from O_in_G[of i]
hoelzl@40859
   668
              moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
hoelzl@40859
   669
                using v.measure_subadditive[of "?O i" A] A O_sets by auto
hoelzl@40859
   670
              ultimately show "\<nu> (?O i \<union> A) \<noteq> \<omega>"
hoelzl@40859
   671
                using `\<nu> A \<noteq> \<omega>` by auto
hoelzl@40859
   672
            qed
hoelzl@40859
   673
            then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI)
hoelzl@40859
   674
          qed
hoelzl@40859
   675
          finally have "\<mu> A = 0" unfolding a_eq using finite_measure[OF `?O_0 \<in> sets M`]
hoelzl@40859
   676
            by (cases "\<mu> A") (auto simp: pinfreal_noteq_omega_Ex)
hoelzl@40859
   677
          with `\<mu> A \<noteq> 0` show ?thesis by auto
hoelzl@40859
   678
        qed
hoelzl@40859
   679
      qed }
hoelzl@40859
   680
hoelzl@40859
   681
    { fix i show "\<nu> (Q i) \<noteq> \<omega>"
hoelzl@40859
   682
      proof (cases i)
hoelzl@40859
   683
        case 0 then show ?thesis
hoelzl@40859
   684
          unfolding Q_def using Q'[of 0] by simp
hoelzl@40859
   685
      next
hoelzl@40859
   686
        case (Suc n)
hoelzl@40859
   687
        then show ?thesis unfolding Q_def
hoelzl@40859
   688
          using `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q` O_mono
hoelzl@40859
   689
          using v.measure_Diff[of "?O n" "?O (Suc n)"] by auto
hoelzl@40859
   690
      qed }
hoelzl@40859
   691
hoelzl@40859
   692
    show "space M - ?O_0 \<in> sets M" using Q'_sets by auto
hoelzl@40859
   693
hoelzl@40859
   694
    { fix j have "(\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q i)"
hoelzl@40859
   695
      proof (induct j)
hoelzl@40859
   696
        case 0 then show ?case by (simp add: Q_def)
hoelzl@40859
   697
      next
hoelzl@40859
   698
        case (Suc j)
hoelzl@40859
   699
        have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastsimp
hoelzl@40859
   700
        have "{..j} \<union> {..Suc j} = {..Suc j}" by auto
hoelzl@40859
   701
        then have "(\<Union>i\<le>Suc j. Q' i) = (\<Union>i\<le>j. Q' i) \<union> Q (Suc j)"
hoelzl@40859
   702
          by (simp add: UN_Un[symmetric] Q_def del: UN_Un)
hoelzl@40859
   703
        then show ?case using Suc by (auto simp add: eq atMost_Suc)
hoelzl@40859
   704
      qed }
hoelzl@40859
   705
    then have "(\<Union>j. (\<Union>i\<le>j. ?O i)) = (\<Union>j. (\<Union>i\<le>j. Q i))" by simp
hoelzl@40859
   706
    then show "space M - ?O_0 = space M - (\<Union>i. Q i)" by fastsimp
hoelzl@40859
   707
  qed
hoelzl@40859
   708
qed
hoelzl@40859
   709
hoelzl@40859
   710
lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
hoelzl@40859
   711
  assumes "measure_space M \<nu>"
hoelzl@40859
   712
  assumes "absolutely_continuous \<nu>"
hoelzl@40859
   713
  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@40859
   714
proof -
hoelzl@40859
   715
  interpret v: measure_space M \<nu> by fact
hoelzl@40859
   716
hoelzl@40859
   717
  from split_space_into_finite_sets_and_rest[OF assms]
hoelzl@40859
   718
  obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
hoelzl@40859
   719
    where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
hoelzl@40859
   720
    and Q0: "Q0 \<in> sets M" "Q0 = space M - (\<Union>i. Q i)"
hoelzl@40859
   721
    and in_Q0: "\<And>A. A \<in> sets M \<Longrightarrow> A \<subseteq> Q0 \<Longrightarrow> \<mu> A = 0 \<and> \<nu> A = 0 \<or> 0 < \<mu> A \<and> \<nu> A = \<omega>"
hoelzl@40859
   722
    and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force
hoelzl@40859
   723
  from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
hoelzl@38656
   724
hoelzl@38656
   725
  have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
hoelzl@38656
   726
    \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
hoelzl@38656
   727
  proof
hoelzl@38656
   728
    fix i
hoelzl@38656
   729
    have indicator_eq: "\<And>f x A. (f x :: pinfreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
hoelzl@38656
   730
      = (f x * indicator (Q i) x) * indicator A x"
hoelzl@38656
   731
      unfolding indicator_def by auto
hoelzl@38656
   732
hoelzl@39092
   733
    have fm: "finite_measure (restricted_space (Q i)) \<mu>"
hoelzl@38656
   734
      (is "finite_measure ?R \<mu>") by (rule restricted_finite_measure[OF Q_sets[of i]])
hoelzl@38656
   735
    then interpret R: finite_measure ?R .
hoelzl@38656
   736
    have fmv: "finite_measure ?R \<nu>"
hoelzl@38656
   737
      unfolding finite_measure_def finite_measure_axioms_def
hoelzl@38656
   738
    proof
hoelzl@38656
   739
      show "measure_space ?R \<nu>"
hoelzl@38656
   740
        using v.restricted_measure_space Q_sets[of i] by auto
hoelzl@38656
   741
      show "\<nu>  (space ?R) \<noteq> \<omega>"
hoelzl@40859
   742
        using Q_fin by simp
hoelzl@38656
   743
    qed
hoelzl@38656
   744
    have "R.absolutely_continuous \<nu>"
hoelzl@38656
   745
      using `absolutely_continuous \<nu>` `Q i \<in> sets M`
hoelzl@38656
   746
      by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
hoelzl@38656
   747
    from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
hoelzl@38656
   748
    obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
hoelzl@38656
   749
      and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. (f x * indicator (Q i) x) * indicator A x)"
hoelzl@38656
   750
      unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
hoelzl@38656
   751
        positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
hoelzl@38656
   752
    then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
hoelzl@38656
   753
      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
hoelzl@38656
   754
      by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
hoelzl@38656
   755
          simp: indicator_def)
hoelzl@38656
   756
  qed
hoelzl@38656
   757
  from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
hoelzl@38656
   758
    and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
hoelzl@38656
   759
      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
hoelzl@38656
   760
    by auto
hoelzl@38656
   761
  let "?f x" =
hoelzl@40859
   762
    "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x"
hoelzl@38656
   763
  show ?thesis
hoelzl@38656
   764
  proof (safe intro!: bexI[of _ ?f])
hoelzl@38656
   765
    show "?f \<in> borel_measurable M"
hoelzl@38656
   766
      by (safe intro!: borel_measurable_psuminf borel_measurable_pinfreal_times
hoelzl@38656
   767
        borel_measurable_pinfreal_add borel_measurable_indicator
hoelzl@40859
   768
        borel_measurable_const borel Q_sets Q0 Diff countable_UN)
hoelzl@38656
   769
    fix A assume "A \<in> sets M"
hoelzl@40859
   770
    have *:
hoelzl@38656
   771
      "\<And>x i. indicator A x * (f i x * indicator (Q i) x) =
hoelzl@38656
   772
        f i x * indicator (Q i \<inter> A) x"
hoelzl@40859
   773
      "\<And>x i. (indicator A x * indicator Q0 x :: pinfreal) =
hoelzl@40859
   774
        indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
hoelzl@38656
   775
    have "positive_integral (\<lambda>x. ?f x * indicator A x) =
hoelzl@40859
   776
      (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
hoelzl@38656
   777
      unfolding f[OF `A \<in> sets M`]
hoelzl@40859
   778
      apply (simp del: pinfreal_times(2) add: field_simps *)
hoelzl@38656
   779
      apply (subst positive_integral_add)
hoelzl@40859
   780
      apply (fastsimp intro: Q0 `A \<in> sets M`)
hoelzl@40859
   781
      apply (fastsimp intro: Q_sets `A \<in> sets M` borel_measurable_psuminf borel)
hoelzl@40859
   782
      apply (subst positive_integral_cmult_indicator)
hoelzl@40859
   783
      apply (fastsimp intro: Q0 `A \<in> sets M`)
hoelzl@38656
   784
      unfolding psuminf_cmult_right[symmetric]
hoelzl@38656
   785
      apply (subst positive_integral_psuminf)
hoelzl@40859
   786
      apply (fastsimp intro: `A \<in> sets M` Q_sets borel)
hoelzl@40859
   787
      apply (simp add: *)
hoelzl@40859
   788
      done
hoelzl@38656
   789
    moreover have "(\<Sum>\<^isub>\<infinity>i. \<nu> (Q i \<inter> A)) = \<nu> ((\<Union>i. Q i) \<inter> A)"
hoelzl@40859
   790
      using Q Q_sets `A \<in> sets M`
hoelzl@40859
   791
      by (intro v.measure_countably_additive[of "\<lambda>i. Q i \<inter> A", unfolded comp_def, simplified])
hoelzl@40859
   792
         (auto simp: disjoint_family_on_def)
hoelzl@40859
   793
    moreover have "\<omega> * \<mu> (Q0 \<inter> A) = \<nu> (Q0 \<inter> A)"
hoelzl@40859
   794
    proof -
hoelzl@40859
   795
      have "Q0 \<inter> A \<in> sets M" using Q0(1) `A \<in> sets M` by blast
hoelzl@40859
   796
      from in_Q0[OF this] show ?thesis by auto
hoelzl@38656
   797
    qed
hoelzl@40859
   798
    moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
hoelzl@40859
   799
      using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN)
hoelzl@40859
   800
    moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
hoelzl@40859
   801
      using `A \<in> sets M` sets_into_space Q0 by auto
hoelzl@38656
   802
    ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
hoelzl@40859
   803
      using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"]
hoelzl@40859
   804
      by simp
hoelzl@38656
   805
  qed
hoelzl@38656
   806
qed
hoelzl@38656
   807
hoelzl@38656
   808
lemma (in sigma_finite_measure) Radon_Nikodym:
hoelzl@38656
   809
  assumes "measure_space M \<nu>"
hoelzl@38656
   810
  assumes "absolutely_continuous \<nu>"
hoelzl@38656
   811
  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@38656
   812
proof -
hoelzl@38656
   813
  from Ex_finite_integrable_function
hoelzl@38656
   814
  obtain h where finite: "positive_integral h \<noteq> \<omega>" and
hoelzl@38656
   815
    borel: "h \<in> borel_measurable M" and
hoelzl@38656
   816
    pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
hoelzl@38656
   817
    "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
hoelzl@38656
   818
  let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
hoelzl@38656
   819
  from measure_space_density[OF borel] finite
hoelzl@38656
   820
  interpret T: finite_measure M ?T
hoelzl@38656
   821
    unfolding finite_measure_def finite_measure_axioms_def
hoelzl@38656
   822
    by (simp cong: positive_integral_cong)
hoelzl@38656
   823
  have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pinfreal)} = N"
hoelzl@38656
   824
    using sets_into_space pos by (force simp: indicator_def)
hoelzl@38656
   825
  then have "T.absolutely_continuous \<nu>" using assms(2) borel
hoelzl@38656
   826
    unfolding T.absolutely_continuous_def absolutely_continuous_def
hoelzl@38656
   827
    by (fastsimp simp: borel_measurable_indicator positive_integral_0_iff)
hoelzl@38656
   828
  from T.Radon_Nikodym_finite_measure_infinite[simplified, OF assms(1) this]
hoelzl@38656
   829
  obtain f where f_borel: "f \<in> borel_measurable M" and
hoelzl@38656
   830
    fT: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = T.positive_integral (\<lambda>x. f x * indicator A x)" by auto
hoelzl@38656
   831
  show ?thesis
hoelzl@38656
   832
  proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
hoelzl@38656
   833
    show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
hoelzl@38656
   834
      using borel f_borel by (auto intro: borel_measurable_pinfreal_times)
hoelzl@38656
   835
    fix A assume "A \<in> sets M"
hoelzl@38656
   836
    then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
hoelzl@38656
   837
      using f_borel by (auto intro: borel_measurable_pinfreal_times borel_measurable_indicator)
hoelzl@38656
   838
    from positive_integral_translated_density[OF borel this]
hoelzl@38656
   839
    show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
hoelzl@38656
   840
      unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
hoelzl@38656
   841
  qed
hoelzl@38656
   842
qed
hoelzl@38656
   843
hoelzl@40859
   844
section "Uniqueness of densities"
hoelzl@40859
   845
hoelzl@40859
   846
lemma (in measure_space) density_is_absolutely_continuous:
hoelzl@40859
   847
  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@40859
   848
  shows "absolutely_continuous \<nu>"
hoelzl@40859
   849
  using assms unfolding absolutely_continuous_def
hoelzl@40859
   850
  by (simp add: positive_integral_null_set)
hoelzl@40859
   851
hoelzl@40859
   852
lemma (in measure_space) finite_density_unique:
hoelzl@40859
   853
  assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
hoelzl@40859
   854
  and fin: "positive_integral f < \<omega>"
hoelzl@40859
   855
  shows "(\<forall>A\<in>sets M. positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. g x * indicator A x))
hoelzl@40859
   856
    \<longleftrightarrow> (AE x. f x = g x)"
hoelzl@40859
   857
    (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
hoelzl@40859
   858
proof (intro iffI ballI)
hoelzl@40859
   859
  fix A assume eq: "AE x. f x = g x"
hoelzl@40859
   860
  show "?P f A = ?P g A"
hoelzl@40859
   861
    by (rule positive_integral_cong_AE[OF AE_mp[OF eq]]) simp
hoelzl@40859
   862
next
hoelzl@40859
   863
  assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
hoelzl@40859
   864
  from this[THEN bspec, OF top] fin
hoelzl@40859
   865
  have g_fin: "positive_integral g < \<omega>" by (simp cong: positive_integral_cong)
hoelzl@40859
   866
  { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
hoelzl@40859
   867
      and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
hoelzl@40859
   868
    let ?N = "{x\<in>space M. g x < f x}"
hoelzl@40859
   869
    have N: "?N \<in> sets M" using borel by simp
hoelzl@40859
   870
    have "?P (\<lambda>x. (f x - g x)) ?N = positive_integral (\<lambda>x. f x * indicator ?N x - g x * indicator ?N x)"
hoelzl@40859
   871
      by (auto intro!: positive_integral_cong simp: indicator_def)
hoelzl@40859
   872
    also have "\<dots> = ?P f ?N - ?P g ?N"
hoelzl@40859
   873
    proof (rule positive_integral_diff)
hoelzl@40859
   874
      show "(\<lambda>x. f x * indicator ?N x) \<in> borel_measurable M" "(\<lambda>x. g x * indicator ?N x) \<in> borel_measurable M"
hoelzl@40859
   875
        using borel N by auto
hoelzl@40859
   876
      have "?P g ?N \<le> positive_integral g"
hoelzl@40859
   877
        by (auto intro!: positive_integral_mono simp: indicator_def)
hoelzl@40859
   878
      then show "?P g ?N \<noteq> \<omega>" using g_fin by auto
hoelzl@40859
   879
      fix x assume "x \<in> space M"
hoelzl@40859
   880
      show "g x * indicator ?N x \<le> f x * indicator ?N x"
hoelzl@40859
   881
        by (auto simp: indicator_def)
hoelzl@40859
   882
    qed
hoelzl@40859
   883
    also have "\<dots> = 0"
hoelzl@40859
   884
      using eq[THEN bspec, OF N] by simp
hoelzl@40859
   885
    finally have "\<mu> {x\<in>space M. (f x - g x) * indicator ?N x \<noteq> 0} = 0"
hoelzl@40859
   886
      using borel N by (subst (asm) positive_integral_0_iff) auto
hoelzl@40859
   887
    moreover have "{x\<in>space M. (f x - g x) * indicator ?N x \<noteq> 0} = ?N"
hoelzl@40859
   888
      by (auto simp: pinfreal_zero_le_diff)
hoelzl@40859
   889
    ultimately have "?N \<in> null_sets" using N by simp }
hoelzl@40859
   890
  from this[OF borel g_fin eq] this[OF borel(2,1) fin]
hoelzl@40859
   891
  have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} \<in> null_sets"
hoelzl@40859
   892
    using eq by (intro null_sets_Un) auto
hoelzl@40859
   893
  also have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} = {x\<in>space M. f x \<noteq> g x}"
hoelzl@40859
   894
    by auto
hoelzl@40859
   895
  finally show "AE x. f x = g x"
hoelzl@40859
   896
    unfolding almost_everywhere_def by auto
hoelzl@40859
   897
qed
hoelzl@40859
   898
hoelzl@40859
   899
lemma (in finite_measure) density_unique_finite_measure:
hoelzl@40859
   900
  assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
hoelzl@40859
   901
  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
hoelzl@40859
   902
    (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
hoelzl@40859
   903
  shows "AE x. f x = f' x"
hoelzl@40859
   904
proof -
hoelzl@40859
   905
  let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
hoelzl@40859
   906
  let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
hoelzl@40859
   907
  interpret M: measure_space M ?\<nu>
hoelzl@40859
   908
    using borel(1) by (rule measure_space_density)
hoelzl@40859
   909
  have ac: "absolutely_continuous ?\<nu>"
hoelzl@40859
   910
    using f by (rule density_is_absolutely_continuous)
hoelzl@40859
   911
  from split_space_into_finite_sets_and_rest[OF `measure_space M ?\<nu>` ac]
hoelzl@40859
   912
  obtain Q0 and Q :: "nat \<Rightarrow> 'a set"
hoelzl@40859
   913
    where Q: "disjoint_family Q" "range Q \<subseteq> sets M"
hoelzl@40859
   914
    and Q0: "Q0 \<in> sets M" "Q0 = space M - (\<Union>i. Q i)"
hoelzl@40859
   915
    and in_Q0: "\<And>A. A \<in> sets M \<Longrightarrow> A \<subseteq> Q0 \<Longrightarrow> \<mu> A = 0 \<and> ?\<nu> A = 0 \<or> 0 < \<mu> A \<and> ?\<nu> A = \<omega>"
hoelzl@40859
   916
    and Q_fin: "\<And>i. ?\<nu> (Q i) \<noteq> \<omega>" by force
hoelzl@40859
   917
  from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
hoelzl@40859
   918
  let ?N = "{x\<in>space M. f x \<noteq> f' x}"
hoelzl@40859
   919
  have "?N \<in> sets M" using borel by auto
hoelzl@40859
   920
  have *: "\<And>i x A. \<And>y::pinfreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x"
hoelzl@40859
   921
    unfolding indicator_def by auto
hoelzl@40859
   922
  have 1: "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x"
hoelzl@40859
   923
    using borel Q_fin Q
hoelzl@40859
   924
    by (intro finite_density_unique[THEN iffD1] allI)
hoelzl@40859
   925
       (auto intro!: borel_measurable_pinfreal_times f Int simp: *)
hoelzl@40859
   926
  have 2: "AE x. ?f Q0 x = ?f' Q0 x"
hoelzl@40859
   927
  proof (rule AE_I')
hoelzl@40859
   928
    { fix f :: "'a \<Rightarrow> pinfreal" assume borel: "f \<in> borel_measurable M"
hoelzl@40859
   929
        and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@40859
   930
      let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
hoelzl@40859
   931
      have "(\<Union>i. ?A i) \<in> null_sets"
hoelzl@40859
   932
      proof (rule null_sets_UN)
hoelzl@40859
   933
        fix i have "?A i \<in> sets M"
hoelzl@40859
   934
          using borel Q0(1) by auto
hoelzl@40859
   935
        have "?\<nu> (?A i) \<le> positive_integral (\<lambda>x. of_nat i * indicator (?A i) x)"
hoelzl@40859
   936
          unfolding eq[OF `?A i \<in> sets M`]
hoelzl@40859
   937
          by (auto intro!: positive_integral_mono simp: indicator_def)
hoelzl@40859
   938
        also have "\<dots> = of_nat i * \<mu> (?A i)"
hoelzl@40859
   939
          using `?A i \<in> sets M` by (auto intro!: positive_integral_cmult_indicator)
hoelzl@40859
   940
        also have "\<dots> < \<omega>"
hoelzl@40859
   941
          using `?A i \<in> sets M`[THEN finite_measure] by auto
hoelzl@40859
   942
        finally have "?\<nu> (?A i) \<noteq> \<omega>" by simp
hoelzl@40859
   943
        then show "?A i \<in> null_sets" using in_Q0[OF `?A i \<in> sets M`] `?A i \<in> sets M` by auto
hoelzl@40859
   944
      qed
hoelzl@40859
   945
      also have "(\<Union>i. ?A i) = Q0 \<inter> {x\<in>space M. f x < \<omega>}"
hoelzl@40859
   946
        by (auto simp: less_\<omega>_Ex_of_nat)
hoelzl@40859
   947
      finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" by (simp add: pinfreal_less_\<omega>) }
hoelzl@40859
   948
    from this[OF borel(1) refl] this[OF borel(2) f]
hoelzl@40859
   949
    have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>} \<in> null_sets" by simp_all
hoelzl@40859
   950
    then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>}) \<in> null_sets" by (rule null_sets_Un)
hoelzl@40859
   951
    show "{x \<in> space M. ?f Q0 x \<noteq> ?f' Q0 x} \<subseteq>
hoelzl@40859
   952
      (Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>})" by (auto simp: indicator_def)
hoelzl@40859
   953
  qed
hoelzl@40859
   954
  have **: "\<And>x. (?f Q0 x = ?f' Q0 x) \<longrightarrow> (\<forall>i. ?f (Q i) x = ?f' (Q i) x) \<longrightarrow>
hoelzl@40859
   955
    ?f (space M) x = ?f' (space M) x"
hoelzl@40859
   956
    by (auto simp: indicator_def Q0)
hoelzl@40859
   957
  have 3: "AE x. ?f (space M) x = ?f' (space M) x"
hoelzl@40859
   958
    by (rule AE_mp[OF 1[unfolded all_AE_countable] AE_mp[OF 2]]) (simp add: **)
hoelzl@40859
   959
  then show "AE x. f x = f' x"
hoelzl@40859
   960
    by (rule AE_mp) (auto intro!: AE_cong simp: indicator_def)
hoelzl@40859
   961
qed
hoelzl@40859
   962
hoelzl@40859
   963
lemma (in sigma_finite_measure) density_unique:
hoelzl@40859
   964
  assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
hoelzl@40859
   965
  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
hoelzl@40859
   966
    (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
hoelzl@40859
   967
  shows "AE x. f x = f' x"
hoelzl@40859
   968
proof -
hoelzl@40859
   969
  obtain h where h_borel: "h \<in> borel_measurable M"
hoelzl@40859
   970
    and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>"
hoelzl@40859
   971
    using Ex_finite_integrable_function by auto
hoelzl@40859
   972
  interpret h: measure_space M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
hoelzl@40859
   973
    using h_borel by (rule measure_space_density)
hoelzl@40859
   974
  interpret h: finite_measure M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
hoelzl@40859
   975
    by default (simp cong: positive_integral_cong add: fin)
hoelzl@40859
   976
hoelzl@40859
   977
  interpret f: measure_space M "\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@40859
   978
    using borel(1) by (rule measure_space_density)
hoelzl@40859
   979
  interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)"
hoelzl@40859
   980
    using borel(2) by (rule measure_space_density)
hoelzl@40859
   981
hoelzl@40859
   982
  { fix A assume "A \<in> sets M"
hoelzl@40859
   983
    then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pinfreal)} = A"
hoelzl@40859
   984
      using pos sets_into_space by (force simp: indicator_def)
hoelzl@40859
   985
    then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets"
hoelzl@40859
   986
      using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
hoelzl@40859
   987
  note h_null_sets = this
hoelzl@40859
   988
hoelzl@40859
   989
  { fix A assume "A \<in> sets M"
hoelzl@40859
   990
    have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) =
hoelzl@40859
   991
      f.positive_integral (\<lambda>x. h x * indicator A x)"
hoelzl@40859
   992
      using `A \<in> sets M` h_borel borel
hoelzl@40859
   993
      by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
hoelzl@40859
   994
    also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)"
hoelzl@40859
   995
      by (rule f'.positive_integral_cong_measure) (rule f)
hoelzl@40859
   996
    also have "\<dots> = positive_integral (\<lambda>x. h x * (f' x * indicator A x))"
hoelzl@40859
   997
      using `A \<in> sets M` h_borel borel
hoelzl@40859
   998
      by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
hoelzl@40859
   999
    finally have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" . }
hoelzl@40859
  1000
  then have "h.almost_everywhere (\<lambda>x. f x = f' x)"
hoelzl@40859
  1001
    using h_borel borel
hoelzl@40859
  1002
    by (intro h.density_unique_finite_measure[OF borel])
hoelzl@40859
  1003
       (simp add: positive_integral_translated_density)
hoelzl@40859
  1004
  then show "AE x. f x = f' x"
hoelzl@40859
  1005
    unfolding h.almost_everywhere_def almost_everywhere_def
hoelzl@40859
  1006
    by (auto simp add: h_null_sets)
hoelzl@40859
  1007
qed
hoelzl@40859
  1008
hoelzl@40859
  1009
lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
hoelzl@40859
  1010
  assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M"
hoelzl@40859
  1011
    and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@40859
  1012
  shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)"
hoelzl@40859
  1013
proof
hoelzl@40859
  1014
  assume "sigma_finite_measure M \<nu>"
hoelzl@40859
  1015
  then interpret \<nu>: sigma_finite_measure M \<nu> .
hoelzl@40859
  1016
  from \<nu>.Ex_finite_integrable_function obtain h where
hoelzl@40859
  1017
    h: "h \<in> borel_measurable M" "\<nu>.positive_integral h \<noteq> \<omega>"
hoelzl@40859
  1018
    and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
hoelzl@40859
  1019
  have "AE x. f x * h x \<noteq> \<omega>"
hoelzl@40859
  1020
  proof (rule AE_I')
hoelzl@40859
  1021
    have "\<nu>.positive_integral h = positive_integral (\<lambda>x. f x * h x)"
hoelzl@40859
  1022
      by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]])
hoelzl@40859
  1023
         (intro positive_integral_translated_density f h)
hoelzl@40859
  1024
    then have "positive_integral (\<lambda>x. f x * h x) \<noteq> \<omega>"
hoelzl@40859
  1025
      using h(2) by simp
hoelzl@40859
  1026
    then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
hoelzl@40859
  1027
      using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
hoelzl@40859
  1028
  qed auto
hoelzl@40859
  1029
  then show "AE x. f x \<noteq> \<omega>"
hoelzl@40859
  1030
  proof (rule AE_mp, intro AE_cong)
hoelzl@40859
  1031
    fix x assume "x \<in> space M" from this[THEN fin]
hoelzl@40859
  1032
    show "f x * h x \<noteq> \<omega> \<longrightarrow> f x \<noteq> \<omega>" by auto
hoelzl@40859
  1033
  qed
hoelzl@40859
  1034
next
hoelzl@40859
  1035
  assume AE: "AE x. f x \<noteq> \<omega>"
hoelzl@40859
  1036
  from sigma_finite guess Q .. note Q = this
hoelzl@40859
  1037
  interpret \<nu>: measure_space M \<nu> by fact
hoelzl@40859
  1038
  def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<omega>} | Suc n \<Rightarrow> {.. of_nat (Suc n)}) \<inter> space M"
hoelzl@40859
  1039
  { fix i j have "A i \<inter> Q j \<in> sets M"
hoelzl@40859
  1040
    unfolding A_def using f Q
hoelzl@40859
  1041
    apply (rule_tac Int)
hoelzl@40859
  1042
    by (cases i) (auto intro: measurable_sets[OF f]) }
hoelzl@40859
  1043
  note A_in_sets = this
hoelzl@40859
  1044
  let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
hoelzl@40859
  1045
  show "sigma_finite_measure M \<nu>"
hoelzl@40859
  1046
  proof (default, intro exI conjI subsetI allI)
hoelzl@40859
  1047
    fix x assume "x \<in> range ?A"
hoelzl@40859
  1048
    then obtain n where n: "x = ?A n" by auto
hoelzl@40859
  1049
    then show "x \<in> sets M" using A_in_sets by (cases "prod_decode n") auto
hoelzl@40859
  1050
  next
hoelzl@40859
  1051
    have "(\<Union>i. ?A i) = (\<Union>i j. A i \<inter> Q j)"
hoelzl@40859
  1052
    proof safe
hoelzl@40859
  1053
      fix x i j assume "x \<in> A i" "x \<in> Q j"
hoelzl@40859
  1054
      then show "x \<in> (\<Union>i. case prod_decode i of (i, j) \<Rightarrow> A i \<inter> Q j)"
hoelzl@40859
  1055
        by (intro UN_I[of "prod_encode (i,j)"]) auto
hoelzl@40859
  1056
    qed auto
hoelzl@40859
  1057
    also have "\<dots> = (\<Union>i. A i) \<inter> space M" using Q by auto
hoelzl@40859
  1058
    also have "(\<Union>i. A i) = space M"
hoelzl@40859
  1059
    proof safe
hoelzl@40859
  1060
      fix x assume x: "x \<in> space M"
hoelzl@40859
  1061
      show "x \<in> (\<Union>i. A i)"
hoelzl@40859
  1062
      proof (cases "f x")
hoelzl@40859
  1063
        case infinite then show ?thesis using x unfolding A_def by (auto intro: exI[of _ 0])
hoelzl@40859
  1064
      next
hoelzl@40859
  1065
        case (preal r)
hoelzl@40859
  1066
        with less_\<omega>_Ex_of_nat[of "f x"] obtain n where "f x < of_nat n" by auto
hoelzl@40859
  1067
        then show ?thesis using x preal unfolding A_def by (auto intro!: exI[of _ "Suc n"])
hoelzl@40859
  1068
      qed
hoelzl@40859
  1069
    qed (auto simp: A_def)
hoelzl@40859
  1070
    finally show "(\<Union>i. ?A i) = space M" by simp
hoelzl@40859
  1071
  next
hoelzl@40859
  1072
    fix n obtain i j where
hoelzl@40859
  1073
      [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
hoelzl@40859
  1074
    have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
hoelzl@40859
  1075
    proof (cases i)
hoelzl@40859
  1076
      case 0
hoelzl@40859
  1077
      have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
hoelzl@40859
  1078
        using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
hoelzl@40859
  1079
      then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) = 0"
hoelzl@40859
  1080
        using A_in_sets f
hoelzl@40859
  1081
        apply (subst positive_integral_0_iff)
hoelzl@40859
  1082
        apply fast
hoelzl@40859
  1083
        apply (subst (asm) AE_iff_null_set)
hoelzl@40859
  1084
        apply (intro borel_measurable_pinfreal_neq_const)
hoelzl@40859
  1085
        apply fast
hoelzl@40859
  1086
        by simp
hoelzl@40859
  1087
      then show ?thesis by simp
hoelzl@40859
  1088
    next
hoelzl@40859
  1089
      case (Suc n)
hoelzl@40859
  1090
      then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<le>
hoelzl@40859
  1091
        positive_integral (\<lambda>x. of_nat (Suc n) * indicator (Q j) x)"
hoelzl@40859
  1092
        by (auto intro!: positive_integral_mono simp: indicator_def A_def)
hoelzl@40859
  1093
      also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
hoelzl@40859
  1094
        using Q by (auto intro!: positive_integral_cmult_indicator)
hoelzl@40859
  1095
      also have "\<dots> < \<omega>"
hoelzl@40859
  1096
        using Q by auto
hoelzl@40859
  1097
      finally show ?thesis by simp
hoelzl@40859
  1098
    qed
hoelzl@40859
  1099
    then show "\<nu> (?A n) \<noteq> \<omega>"
hoelzl@40859
  1100
      using A_in_sets Q eq by auto
hoelzl@40859
  1101
  qed
hoelzl@40859
  1102
qed
hoelzl@40859
  1103
hoelzl@38656
  1104
section "Radon Nikodym derivative"
hoelzl@38656
  1105
hoelzl@38656
  1106
definition (in sigma_finite_measure)
hoelzl@38656
  1107
  "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
hoelzl@38656
  1108
    (\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
hoelzl@38656
  1109
hoelzl@40859
  1110
lemma (in sigma_finite_measure) RN_deriv_cong:
hoelzl@40859
  1111
  assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A"
hoelzl@40859
  1112
  shows "sigma_finite_measure.RN_deriv M \<mu>' \<nu>' x = RN_deriv \<nu> x"
hoelzl@40859
  1113
proof -
hoelzl@40859
  1114
  interpret \<mu>': sigma_finite_measure M \<mu>'
hoelzl@40859
  1115
    using cong(1) by (rule sigma_finite_measure_cong)
hoelzl@40859
  1116
  show ?thesis
hoelzl@40859
  1117
    unfolding RN_deriv_def \<mu>'.RN_deriv_def
hoelzl@40859
  1118
    by (simp add: cong positive_integral_cong_measure[OF cong(1)])
hoelzl@40859
  1119
qed
hoelzl@40859
  1120
hoelzl@38656
  1121
lemma (in sigma_finite_measure) RN_deriv:
hoelzl@38656
  1122
  assumes "measure_space M \<nu>"
hoelzl@38656
  1123
  assumes "absolutely_continuous \<nu>"
hoelzl@38656
  1124
  shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
hoelzl@38656
  1125
  and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
hoelzl@38656
  1126
    (is "\<And>A. _ \<Longrightarrow> ?int A")
hoelzl@38656
  1127
proof -
hoelzl@38656
  1128
  note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
hoelzl@38656
  1129
  thus ?borel unfolding RN_deriv_def by (rule someI2_ex) auto
hoelzl@38656
  1130
  fix A assume "A \<in> sets M"
hoelzl@38656
  1131
  from Ex show "?int A" unfolding RN_deriv_def
hoelzl@38656
  1132
    by (rule someI2_ex) (simp add: `A \<in> sets M`)
hoelzl@38656
  1133
qed
hoelzl@38656
  1134
hoelzl@40859
  1135
lemma (in sigma_finite_measure) RN_deriv_positive_integral:
hoelzl@40859
  1136
  assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
hoelzl@40859
  1137
    and f: "f \<in> borel_measurable M"
hoelzl@40859
  1138
  shows "measure_space.positive_integral M \<nu> f = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
hoelzl@40859
  1139
proof -
hoelzl@40859
  1140
  interpret \<nu>: measure_space M \<nu> by fact
hoelzl@40859
  1141
  have "\<nu>.positive_integral f =
hoelzl@40859
  1142
    measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)) f"
hoelzl@40859
  1143
    by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric])
hoelzl@40859
  1144
  also have "\<dots> = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
hoelzl@40859
  1145
    by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f)
hoelzl@40859
  1146
  finally show ?thesis .
hoelzl@40859
  1147
qed
hoelzl@40859
  1148
hoelzl@40859
  1149
lemma (in sigma_finite_measure) RN_deriv_unique:
hoelzl@40859
  1150
  assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
hoelzl@40859
  1151
  and f: "f \<in> borel_measurable M"
hoelzl@40859
  1152
  and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
hoelzl@40859
  1153
  shows "AE x. f x = RN_deriv \<nu> x"
hoelzl@40859
  1154
proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]])
hoelzl@40859
  1155
  fix A assume A: "A \<in> sets M"
hoelzl@40859
  1156
  show "positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
hoelzl@40859
  1157
    unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
hoelzl@40859
  1158
qed
hoelzl@40859
  1159
hoelzl@40859
  1160
lemma the_inv_into_in:
hoelzl@40859
  1161
  assumes "inj_on f A" and x: "x \<in> f`A"
hoelzl@40859
  1162
  shows "the_inv_into A f x \<in> A"
hoelzl@40859
  1163
  using assms by (auto simp: the_inv_into_f_f)
hoelzl@40859
  1164
hoelzl@40859
  1165
lemma (in sigma_finite_measure) RN_deriv_vimage:
hoelzl@40859
  1166
  fixes f :: "'b \<Rightarrow> 'a"
hoelzl@40859
  1167
  assumes f: "bij_betw f S (space M)"
hoelzl@40859
  1168
  assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
hoelzl@40859
  1169
  shows "AE x.
hoelzl@40859
  1170
    sigma_finite_measure.RN_deriv (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A)) (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) = RN_deriv \<nu> x"
hoelzl@40859
  1171
proof (rule RN_deriv_unique[OF \<nu>])
hoelzl@40859
  1172
  interpret sf: sigma_finite_measure "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)"
hoelzl@40859
  1173
    using f by (rule sigma_finite_measure_isomorphic)
hoelzl@40859
  1174
  interpret \<nu>: measure_space M \<nu> using \<nu>(1) .
hoelzl@40859
  1175
  have \<nu>': "measure_space (vimage_algebra S f) (\<lambda>A. \<nu> (f ` A))"
hoelzl@40859
  1176
    using f by (rule \<nu>.measure_space_isomorphic)
hoelzl@40859
  1177
  { fix A assume "A \<in> sets M" then have "f ` (f -` A \<inter> S) = A"
hoelzl@40859
  1178
      using sets_into_space f[unfolded bij_betw_def]
hoelzl@40859
  1179
      by (intro image_vimage_inter_eq[where T="space M"]) auto }
hoelzl@40859
  1180
  note A_f = this
hoelzl@40859
  1181
  then have ac: "sf.absolutely_continuous (\<lambda>A. \<nu> (f ` A))"
hoelzl@40859
  1182
    using \<nu>(2) by (auto simp: sf.absolutely_continuous_def absolutely_continuous_def)
hoelzl@40859
  1183
  show "(\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x)) \<in> borel_measurable M"
hoelzl@40859
  1184
    using sf.RN_deriv(1)[OF \<nu>' ac]
hoelzl@40859
  1185
    unfolding measurable_vimage_iff_inv[OF f] comp_def .
hoelzl@40859
  1186
  fix A assume "A \<in> sets M"
hoelzl@40859
  1187
  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (the_inv_into S f x) = (indicator A x :: pinfreal)"
hoelzl@40859
  1188
    using f[unfolded bij_betw_def]
hoelzl@40859
  1189
    unfolding indicator_def by (auto simp: f_the_inv_into_f the_inv_into_in)
hoelzl@40859
  1190
  have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
hoelzl@40859
  1191
    using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
hoelzl@40859
  1192
  also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
hoelzl@40859
  1193
    unfolding positive_integral_vimage_inv[OF f]
hoelzl@40859
  1194
    by (simp add: * cong: positive_integral_cong)
hoelzl@40859
  1195
  finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (the_inv_into S f x) * indicator A x)"
hoelzl@40859
  1196
    unfolding A_f[OF `A \<in> sets M`] .
hoelzl@40859
  1197
qed
hoelzl@40859
  1198
hoelzl@40859
  1199
lemma (in sigma_finite_measure) RN_deriv_finite:
hoelzl@40859
  1200
  assumes sfm: "sigma_finite_measure M \<nu>" and ac: "absolutely_continuous \<nu>"
hoelzl@40859
  1201
  shows "AE x. RN_deriv \<nu> x \<noteq> \<omega>"
hoelzl@40859
  1202
proof -
hoelzl@40859
  1203
  interpret \<nu>: sigma_finite_measure M \<nu> by fact
hoelzl@40859
  1204
  have \<nu>: "measure_space M \<nu>" by default
hoelzl@40859
  1205
  from sfm show ?thesis
hoelzl@40859
  1206
    using sigma_finite_iff_density_finite[OF \<nu> RN_deriv[OF \<nu> ac]] by simp
hoelzl@40859
  1207
qed
hoelzl@40859
  1208
hoelzl@40859
  1209
lemma (in sigma_finite_measure)
hoelzl@40859
  1210
  assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>"
hoelzl@40859
  1211
    and f: "f \<in> borel_measurable M"
hoelzl@40859
  1212
  shows RN_deriv_integral: "measure_space.integral M \<nu> f = integral (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
hoelzl@40859
  1213
    and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable)
hoelzl@40859
  1214
proof -
hoelzl@40859
  1215
  interpret \<nu>: sigma_finite_measure M \<nu> by fact
hoelzl@40859
  1216
  have ms: "measure_space M \<nu>" by default
hoelzl@40859
  1217
  have minus_cong: "\<And>A B A' B'::pinfreal. A = A' \<Longrightarrow> B = B' \<Longrightarrow> real A - real B = real A' - real B'" by simp
hoelzl@40859
  1218
  have f': "(\<lambda>x. - f x) \<in> borel_measurable M" using f by auto
hoelzl@40859
  1219
  { fix f :: "'a \<Rightarrow> real" assume "f \<in> borel_measurable M"
hoelzl@40859
  1220
    { fix x assume *: "RN_deriv \<nu> x \<noteq> \<omega>"
hoelzl@40859
  1221
      have "Real (real (RN_deriv \<nu> x)) * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
hoelzl@40859
  1222
        by (simp add: mult_le_0_iff)
hoelzl@40859
  1223
      then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
hoelzl@40859
  1224
        using * by (simp add: Real_real) }
hoelzl@40859
  1225
    note * = this
hoelzl@40859
  1226
    have "positive_integral (\<lambda>x. RN_deriv \<nu> x * Real (f x)) = positive_integral (\<lambda>x. Real (real (RN_deriv \<nu> x) * f x))"
hoelzl@40859
  1227
      apply (rule positive_integral_cong_AE)
hoelzl@40859
  1228
      apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
hoelzl@40859
  1229
      by (auto intro!: AE_cong simp: *) }
hoelzl@40859
  1230
  with this[OF f] this[OF f'] f f'
hoelzl@40859
  1231
  show ?integral ?integrable
hoelzl@40859
  1232
    unfolding \<nu>.integral_def integral_def \<nu>.integrable_def integrable_def
hoelzl@40859
  1233
    by (auto intro!: RN_deriv(1)[OF ms \<nu>(2)] minus_cong simp: RN_deriv_positive_integral[OF ms \<nu>(2)])
hoelzl@40859
  1234
qed
hoelzl@40859
  1235
hoelzl@38656
  1236
lemma (in sigma_finite_measure) RN_deriv_singleton:
hoelzl@38656
  1237
  assumes "measure_space M \<nu>"
hoelzl@38656
  1238
  and ac: "absolutely_continuous \<nu>"
hoelzl@38656
  1239
  and "{x} \<in> sets M"
hoelzl@38656
  1240
  shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
hoelzl@38656
  1241
proof -
hoelzl@38656
  1242
  note deriv = RN_deriv[OF assms(1, 2)]
hoelzl@38656
  1243
  from deriv(2)[OF `{x} \<in> sets M`]
hoelzl@38656
  1244
  have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
hoelzl@38656
  1245
    by (auto simp: indicator_def intro!: positive_integral_cong)
hoelzl@38656
  1246
  thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
hoelzl@38656
  1247
    by auto
hoelzl@38656
  1248
qed
hoelzl@38656
  1249
hoelzl@38656
  1250
theorem (in finite_measure_space) RN_deriv_finite_measure:
hoelzl@38656
  1251
  assumes "measure_space M \<nu>"
hoelzl@38656
  1252
  and ac: "absolutely_continuous \<nu>"
hoelzl@38656
  1253
  and "x \<in> space M"
hoelzl@38656
  1254
  shows "\<nu> {x} = RN_deriv \<nu> x * \<mu> {x}"
hoelzl@38656
  1255
proof -
hoelzl@38656
  1256
  have "{x} \<in> sets M" using sets_eq_Pow `x \<in> space M` by auto
hoelzl@38656
  1257
  from RN_deriv_singleton[OF assms(1,2) this] show ?thesis .
hoelzl@38656
  1258
qed
hoelzl@38656
  1259
hoelzl@38656
  1260
end