src/HOL/Probability/Radon_Nikodym.thy
 changeset 41832 27cb9113b1a0 parent 41705 1100512e16d8 child 41981 cdf7693bbe08
```     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 23 11:40:12 2011 +0100
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Feb 23 11:40:17 2011 +0100
1.3 @@ -74,7 +74,7 @@
1.4  definition (in measure_space)
1.5    "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pextreal))"
1.6
1.7 -lemma (in sigma_finite_measure) absolutely_continuous_AE:
1.8 +lemma (in measure_space) absolutely_continuous_AE:
1.9    assumes "measure_space M'" and [simp]: "sets M' = sets M" "space M' = space M"
1.10      and "absolutely_continuous (measure M')" "AE x. P x"
1.11    shows "measure_space.almost_everywhere M' P"
1.12 @@ -1113,6 +1113,76 @@
1.13      unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
1.14  qed
1.15
1.16 +lemma (in sigma_finite_measure) RN_deriv_vimage:
1.17 +  assumes T: "T \<in> measure_preserving M M'"
1.18 +    and T': "T' \<in> measure_preserving (M'\<lparr> measure := \<nu>' \<rparr>) (M\<lparr> measure := \<nu> \<rparr>)"
1.19 +    and inv: "\<And>x. x \<in> space M \<Longrightarrow> T' (T x) = x"
1.20 +  and \<nu>': "measure_space (M'\<lparr>measure := \<nu>'\<rparr>)" "measure_space.absolutely_continuous M' \<nu>'"
1.21 +  shows "AE x. RN_deriv M' \<nu>' (T x) = RN_deriv M \<nu> x"
1.22 +proof (rule RN_deriv_unique)
1.23 +  interpret \<nu>': measure_space "M'\<lparr>measure := \<nu>'\<rparr>" by fact
1.24 +  show "measure_space (M\<lparr> measure := \<nu>\<rparr>)"
1.25 +    by (rule \<nu>'.measure_space_vimage[OF _ T'], simp) default
1.26 +  interpret M': measure_space M'
1.27 +  proof (rule measure_space_vimage)
1.28 +    have "sigma_algebra (M'\<lparr> measure := \<nu>'\<rparr>)" by default
1.29 +    then show "sigma_algebra M'" by simp
1.30 +  qed fact
1.31 +  show "absolutely_continuous \<nu>" unfolding absolutely_continuous_def
1.32 +  proof safe
1.33 +    fix N assume N: "N \<in> sets M" and N_0: "\<mu> N = 0"
1.34 +    then have N': "T' -` N \<inter> space M' \<in> sets M'"
1.35 +      using T' by (auto simp: measurable_def measure_preserving_def)
1.36 +    have "T -` (T' -` N \<inter> space M') \<inter> space M = N"
1.37 +      using inv T N sets_into_space[OF N] by (auto simp: measurable_def measure_preserving_def)
1.38 +    then have "measure M' (T' -` N \<inter> space M') = 0"
1.39 +      using measure_preservingD[OF T N'] N_0 by auto
1.40 +    with \<nu>'(2) N' show "\<nu> N = 0" using measure_preservingD[OF T', of N] N
1.41 +      unfolding M'.absolutely_continuous_def measurable_def by auto
1.42 +  qed
1.43 +  interpret M': sigma_finite_measure M'
1.44 +  proof
1.45 +    from sigma_finite guess F .. note F = this
1.46 +    show "\<exists>A::nat \<Rightarrow> 'c set. range A \<subseteq> sets M' \<and> (\<Union>i. A i) = space M' \<and> (\<forall>i. M'.\<mu> (A i) \<noteq> \<omega>)"
1.47 +    proof (intro exI conjI allI)
1.48 +      show *: "range (\<lambda>i. T' -` F i \<inter> space M') \<subseteq> sets M'"
1.49 +        using F T' by (auto simp: measurable_def measure_preserving_def)
1.50 +      show "(\<Union>i. T' -` F i \<inter> space M') = space M'"
1.51 +        using F T' by (force simp: measurable_def measure_preserving_def)
1.52 +      fix i
1.53 +      have "T' -` F i \<inter> space M' \<in> sets M'" using * by auto
1.54 +      note measure_preservingD[OF T this, symmetric]
1.55 +      moreover
1.56 +      have Fi: "F i \<in> sets M" using F by auto
1.57 +      then have "T -` (T' -` F i \<inter> space M') \<inter> space M = F i"
1.58 +        using T inv sets_into_space[OF Fi]
1.59 +        by (auto simp: measurable_def measure_preserving_def)
1.60 +      ultimately show "measure M' (T' -` F i \<inter> space M') \<noteq> \<omega>"
1.61 +        using F by simp
1.62 +    qed
1.63 +  qed
1.64 +  have "(RN_deriv M' \<nu>') \<circ> T \<in> borel_measurable M"
1.65 +    by (intro measurable_comp[where b=M'] M'.RN_deriv(1) measure_preservingD2[OF T]) fact+
1.66 +  then show "(\<lambda>x. RN_deriv M' \<nu>' (T x)) \<in> borel_measurable M"
1.67 +    by (simp add: comp_def)
1.68 +  fix A let ?A = "T' -` A \<inter> space M'"
1.69 +  assume A: "A \<in> sets M"
1.70 +  then have A': "?A \<in> sets M'" using T' unfolding measurable_def measure_preserving_def
1.71 +    by auto
1.72 +  from A have "\<nu> A = \<nu>' ?A" using T'[THEN measure_preservingD] by simp
1.73 +  also have "\<dots> = \<integral>\<^isup>+ x. RN_deriv M' \<nu>' x * indicator ?A x \<partial>M'"
1.74 +    using A' by (rule M'.RN_deriv(2)[OF \<nu>'])
1.75 +  also have "\<dots> = \<integral>\<^isup>+ x. RN_deriv M' \<nu>' (T x) * indicator ?A (T x) \<partial>M"
1.76 +  proof (rule positive_integral_vimage)
1.77 +    show "sigma_algebra M'" by default
1.78 +    show "(\<lambda>x. RN_deriv M' \<nu>' x * indicator (T' -` A \<inter> space M') x) \<in> borel_measurable M'"
1.79 +      by (auto intro!: A' M'.RN_deriv(1)[OF \<nu>'])
1.80 +  qed fact
1.81 +  also have "\<dots> = \<integral>\<^isup>+ x. RN_deriv M' \<nu>' (T x) * indicator A x \<partial>M"
1.82 +    using T inv by (auto intro!: positive_integral_cong simp: measure_preserving_def measurable_def indicator_def)
1.83 +  finally show "\<nu> A = \<integral>\<^isup>+ x. RN_deriv M' \<nu>' (T x) * indicator A x \<partial>M" .
1.84 +qed
1.85 +
1.86  lemma (in sigma_finite_measure) RN_deriv_finite:
1.87    assumes sfm: "sigma_finite_measure (M\<lparr>measure := \<nu>\<rparr>)" and ac: "absolutely_continuous \<nu>"
1.88    shows "AE x. RN_deriv M \<nu> x \<noteq> \<omega>"
```