src/HOL/Probability/Radon_Nikodym.thy
 changeset 49785 0a8adca22974 parent 49778 bbbc0f492780 child 50003 8c213922ed49
```     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Oct 10 12:12:23 2012 +0200
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Oct 10 12:12:24 2012 +0200
1.3 @@ -776,15 +776,16 @@
1.4    assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.5    assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
1.6    and fin: "integral\<^isup>P M f \<noteq> \<infinity>"
1.7 -  shows "(\<forall>A\<in>sets M. (\<integral>\<^isup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^isup>+x. g x * indicator A x \<partial>M))
1.8 -    \<longleftrightarrow> (AE x in M. f x = g x)"
1.9 -    (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
1.10 +  shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
1.11  proof (intro iffI ballI)
1.12    fix A assume eq: "AE x in M. f x = g x"
1.13 -  then show "?P f A = ?P g A"
1.14 -    by (auto intro: positive_integral_cong_AE)
1.15 +  with borel show "density M f = density M g"
1.16 +    by (auto intro: density_cong)
1.17  next
1.18 -  assume eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
1.19 +  let ?P = "\<lambda>f A. \<integral>\<^isup>+ x. f x * indicator A x \<partial>M"
1.20 +  assume "density M f = density M g"
1.21 +  with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
1.22 +    by (simp add: emeasure_density[symmetric])
1.23    from this[THEN bspec, OF top] fin
1.24    have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
1.25    { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.26 @@ -844,7 +845,7 @@
1.27      unfolding indicator_def by auto
1.28    have "\<forall>i. AE x in M. ?f (Q i) x = ?f' (Q i) x" using borel Q_fin Q pos
1.29      by (intro finite_density_unique[THEN iffD1] allI)
1.30 -       (auto intro!: borel_measurable_ereal_times f Int simp: *)
1.31 +       (auto intro!: borel_measurable_ereal_times f measure_eqI Int simp: emeasure_density * subset_eq)
1.32    moreover have "AE x in M. ?f Q0 x = ?f' Q0 x"
1.33    proof (rule AE_I')
1.34      { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
1.35 @@ -933,6 +934,41 @@
1.36    shows "density M f = density M f' \<longleftrightarrow> (AE x in M. f x = f' x)"
1.37    using density_unique[OF assms] density_cong[OF f f'] by auto
1.38
1.39 +lemma sigma_finite_density_unique:
1.40 +  assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
1.41 +  assumes pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
1.42 +  and fin: "sigma_finite_measure (density M f)"
1.43 +  shows "density M f = density M g \<longleftrightarrow> (AE x in M. f x = g x)"
1.44 +proof
1.45 +  assume "AE x in M. f x = g x" with borel show "density M f = density M g"
1.46 +    by (auto intro: density_cong)
1.47 +next
1.48 +  assume eq: "density M f = density M g"
1.49 +  interpret f!: sigma_finite_measure "density M f" by fact
1.50 +  from f.sigma_finite_incseq guess A . note cover = this
1.51 +
1.52 +  have "AE x in M. \<forall>i. x \<in> A i \<longrightarrow> f x = g x"
1.53 +    unfolding AE_all_countable
1.54 +  proof
1.55 +    fix i
1.56 +    have "density (density M f) (indicator (A i)) = density (density M g) (indicator (A i))"
1.57 +      unfolding eq ..
1.58 +    moreover have "(\<integral>\<^isup>+x. f x * indicator (A i) x \<partial>M) \<noteq> \<infinity>"
1.59 +      using cover(1) cover(3)[of i] borel by (auto simp: emeasure_density subset_eq)
1.60 +    ultimately have "AE x in M. f x * indicator (A i) x = g x * indicator (A i) x"
1.61 +      using borel pos cover(1) pos
1.62 +      by (intro finite_density_unique[THEN iffD1])
1.63 +         (auto simp: density_density_eq subset_eq)
1.64 +    then show "AE x in M. x \<in> A i \<longrightarrow> f x = g x"
1.65 +      by auto
1.66 +  qed
1.67 +  with AE_space show "AE x in M. f x = g x"
1.68 +    apply eventually_elim
1.69 +    using cover(2)[symmetric]
1.70 +    apply auto
1.71 +    done
1.72 +qed
1.73 +
1.74  lemma (in sigma_finite_measure) sigma_finite_iff_density_finite':
1.75    assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
1.76    shows "sigma_finite_measure (density M f) \<longleftrightarrow> (AE x in M. f x \<noteq> \<infinity>)"
1.77 @@ -1076,15 +1112,17 @@
1.78    assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
1.79    and eq: "density M f = N"
1.80    shows "AE x in M. f x = RN_deriv M N x"
1.81 -proof (rule density_unique)
1.82 -  have ac: "absolutely_continuous M N"
1.83 -    using f(1) unfolding eq[symmetric] by (rule absolutely_continuousI_density)
1.84 -  have eq2: "sets N = sets M"
1.85 -    unfolding eq[symmetric] by simp
1.86 -  show "RN_deriv M N \<in> borel_measurable M" "AE x in M. 0 \<le> RN_deriv M N x"
1.87 -    "density M f = density M (RN_deriv M N)"
1.88 -    using RN_deriv[OF ac eq2] eq by auto
1.89 -qed fact+
1.90 +  unfolding eq[symmetric]
1.91 +  by (intro density_unique_iff[THEN iffD1] f borel_measurable_RN_deriv_density
1.92 +            RN_deriv_density_nonneg[THEN AE_I2] density_RN_deriv_density[symmetric])
1.93 +
1.94 +lemma RN_deriv_unique_sigma_finite:
1.95 +  assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
1.96 +  and eq: "density M f = N" and fin: "sigma_finite_measure N"
1.97 +  shows "AE x in M. f x = RN_deriv M N x"
1.98 +  using fin unfolding eq[symmetric]
1.99 +  by (intro sigma_finite_density_unique[THEN iffD1] f borel_measurable_RN_deriv_density
1.100 +            RN_deriv_density_nonneg[THEN AE_I2] density_RN_deriv_density[symmetric])
1.101
1.102  lemma (in sigma_finite_measure) RN_deriv_distr:
1.103    fixes T :: "'a \<Rightarrow> 'b"
```