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"