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