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>"