src/HOL/Probability/Radon_Nikodym.thy
changeset 50244 de72bbe42190
parent 50021 d96a3f468203
child 51329 4a3c453f99a1
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Thu Nov 22 10:09:54 2012 +0100
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Nov 27 11:29:47 2012 +0100
     1.3 @@ -189,13 +189,13 @@
     1.4        fix B assume "B \<in> sets M" "B \<subseteq> space M - A n"
     1.5        from B[OF this] show "-e < ?d B" .
     1.6      next
     1.7 -      show "space M - A n \<in> sets M" by (rule compl_sets) fact
     1.8 +      show "space M - A n \<in> sets M" by (rule sets.compl_sets) fact
     1.9      next
    1.10        show "?d (space M) \<le> ?d (space M - A n)"
    1.11        proof (induct n)
    1.12          fix n assume "?d (space M) \<le> ?d (space M - A n)"
    1.13          also have "\<dots> \<le> ?d (space M - A (Suc n))"
    1.14 -          using A_in_sets sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
    1.15 +          using A_in_sets sets.sets_into_space dA_mono[of n] finite_measure_compl M'.finite_measure_compl
    1.16            by (simp del: A_simps add: sets_eq sets_eq_imp_space_eq[OF sets_eq])
    1.17          finally show "?d (space M) \<le> ?d (space M - A (Suc n))" .
    1.18        qed simp
    1.19 @@ -241,7 +241,7 @@
    1.20        by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
    1.21      from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
    1.22      with S have "?P (S \<inter> X) S n"
    1.23 -      by (simp add: measure_restricted sets_eq Int) (metis inf_absorb2)
    1.24 +      by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
    1.25      hence "\<exists>A. ?P A S n" .. }
    1.26    note Ex_P = this
    1.27    def A \<equiv> "nat_rec (space M) (\<lambda>n A. SOME B. ?P B A n)"
    1.28 @@ -309,7 +309,7 @@
    1.29        hence sets: "?A \<inter> A \<in> sets M" "(space M - ?A) \<inter> A \<in> sets M" using `?A \<in> sets M` by auto
    1.30        hence sets': "?A \<inter> A \<in> sets N" "(space M - ?A) \<inter> A \<in> sets N" by (auto simp: sets_eq)
    1.31        have union: "((?A \<inter> A) \<union> ((space M - ?A) \<inter> A)) = A"
    1.32 -        using sets_into_space[OF `A \<in> sets M`] by auto
    1.33 +        using sets.sets_into_space[OF `A \<in> sets M`] by auto
    1.34        have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
    1.35          g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
    1.36          by (auto simp: indicator_def max_def)
    1.37 @@ -351,7 +351,7 @@
    1.38    have y_le: "?y \<le> N (space M)" unfolding G_def
    1.39    proof (safe intro!: SUP_least)
    1.40      fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> N A"
    1.41 -    from this[THEN bspec, OF top] show "integral\<^isup>P M g \<le> N (space M)"
    1.42 +    from this[THEN bspec, OF sets.top] show "integral\<^isup>P M g \<le> N (space M)"
    1.43        by (simp cong: positive_integral_cong)
    1.44    qed
    1.45    from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^isup>P M"] guess ys .. note ys = this
    1.46 @@ -507,7 +507,7 @@
    1.47      with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * emeasure M A0" unfolding int_f_eq_y
    1.48        using `f \<in> G`
    1.49        by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
    1.50 -    also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
    1.51 +    also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF sets.top] `A0 \<in> sets M` sets.sets_into_space
    1.52        by (simp cong: positive_integral_cong)
    1.53      finally have "?y < integral\<^isup>P M ?f0" by simp
    1.54      moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
    1.55 @@ -536,7 +536,7 @@
    1.56    let ?a = "SUP Q:?Q. emeasure M Q"
    1.57    have "{} \<in> ?Q" by auto
    1.58    then have Q_not_empty: "?Q \<noteq> {}" by blast
    1.59 -  have "?a \<le> emeasure M (space M)" using sets_into_space
    1.60 +  have "?a \<le> emeasure M (space M)" using sets.sets_into_space
    1.61      by (auto intro!: SUP_least emeasure_mono)
    1.62    then have "?a \<noteq> \<infinity>" using finite_emeasure_space
    1.63      by auto
    1.64 @@ -601,7 +601,7 @@
    1.65          next
    1.66            assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
    1.67            with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
    1.68 -            using Q' by (auto intro!: plus_emeasure countable_UN)
    1.69 +            using Q' by (auto intro!: plus_emeasure sets.countable_UN)
    1.70            also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"
    1.71            proof (rule SUP_emeasure_incseq[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
    1.72              show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
    1.73 @@ -712,7 +712,7 @@
    1.74        also have "\<dots> = (\<integral>\<^isup>+x. (\<Sum>i. f i x * indicator (Q i \<inter> A) x) \<partial>M) + \<infinity> * emeasure M (Q0 \<inter> A)"
    1.75          using borel Qi Q0(1) `A \<in> sets M`
    1.76          by (subst positive_integral_add) (auto simp del: ereal_infty_mult
    1.77 -            simp add: positive_integral_cmult_indicator Int intro!: suminf_0_le)
    1.78 +            simp add: positive_integral_cmult_indicator sets.Int intro!: suminf_0_le)
    1.79        also have "\<dots> = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)"
    1.80          by (subst integral_eq[OF `A \<in> sets M`], subst positive_integral_suminf) auto
    1.81        finally have "(\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M) = (\<Sum>i. N (Q i \<inter> A)) + \<infinity> * emeasure M (Q0 \<inter> A)" .
    1.82 @@ -727,7 +727,7 @@
    1.83        moreover have "Q0 \<inter> A \<in> sets M" "((\<Union>i. Q i) \<inter> A) \<in> sets M"
    1.84          using Q_sets `A \<in> sets M` Q0(1) by auto
    1.85        moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
    1.86 -        using `A \<in> sets M` sets_into_space Q0 by auto
    1.87 +        using `A \<in> sets M` sets.sets_into_space Q0 by auto
    1.88        ultimately have "N A = (\<integral>\<^isup>+x. ?f x * indicator A x \<partial>M)"
    1.89          using plus_emeasure[of "(\<Union>i. Q i) \<inter> A" N "Q0 \<inter> A"] by (simp add: sets_eq)
    1.90        with `A \<in> sets M` borel Q Q0(1) show "emeasure (density M ?f) A = N A"
    1.91 @@ -755,7 +755,7 @@
    1.92      fix A assume "A \<in> null_sets ?MT"
    1.93      with borel have "A \<in> sets M" "AE x in M. x \<in> A \<longrightarrow> h x \<le> 0"
    1.94        by (auto simp add: null_sets_density_iff)
    1.95 -    with pos sets_into_space have "AE x in M. x \<notin> A"
    1.96 +    with pos sets.sets_into_space have "AE x in M. x \<notin> A"
    1.97        by (elim eventually_elim1) (auto simp: not_le[symmetric])
    1.98      then have "A \<in> null_sets M"
    1.99        using `A \<in> sets M` by (simp add: AE_iff_null_sets)
   1.100 @@ -784,7 +784,7 @@
   1.101    assume "density M f = density M g"
   1.102    with borel have eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
   1.103      by (simp add: emeasure_density[symmetric])
   1.104 -  from this[THEN bspec, OF top] fin
   1.105 +  from this[THEN bspec, OF sets.top] fin
   1.106    have g_fin: "integral\<^isup>P M g \<noteq> \<infinity>" by (simp cong: positive_integral_cong)
   1.107    { fix f g assume borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   1.108        and pos: "AE x in M. 0 \<le> f x" "AE x in M. 0 \<le> g x"
   1.109 @@ -898,7 +898,7 @@
   1.110    let ?f'M = "density M f'"
   1.111    { fix A assume "A \<in> sets M"
   1.112      then have "{x \<in> space M. h x * indicator A x \<noteq> 0} = A"
   1.113 -      using pos(1) sets_into_space by (force simp: indicator_def)
   1.114 +      using pos(1) sets.sets_into_space by (force simp: indicator_def)
   1.115      then have "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M) = 0 \<longleftrightarrow> A \<in> null_sets M"
   1.116        using h_borel `A \<in> sets M` h_nn by (subst positive_integral_0_iff) auto }
   1.117    note h_null_sets = this
   1.118 @@ -994,7 +994,7 @@
   1.119    def A \<equiv> "\<lambda>i. f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ereal(of_nat (Suc n))}) \<inter> space M"
   1.120    { fix i j have "A i \<inter> Q j \<in> sets M"
   1.121      unfolding A_def using f Q
   1.122 -    apply (rule_tac Int)
   1.123 +    apply (rule_tac sets.Int)
   1.124      by (cases i) (auto intro: measurable_sets[OF f(1)]) }
   1.125    note A_in_sets = this
   1.126    let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
   1.127 @@ -1133,12 +1133,12 @@
   1.128    note sets_eq_imp_space_eq[OF N, simp]
   1.129    have measurable_N[simp]: "\<And>M'. measurable N M' = measurable M M'" by (auto simp: measurable_def)
   1.130    { fix A assume "A \<in> sets M"
   1.131 -    with inv T T' sets_into_space[OF this]
   1.132 +    with inv T T' sets.sets_into_space[OF this]
   1.133      have "T -` T' -` A \<inter> T -` space M' \<inter> space M = A"
   1.134        by (auto simp: measurable_def) }
   1.135    note eq = this[simp]
   1.136    { fix A assume "A \<in> sets M"
   1.137 -    with inv T T' sets_into_space[OF this]
   1.138 +    with inv T T' sets.sets_into_space[OF this]
   1.139      have "(T' \<circ> T) -` A \<inter> space M = A"
   1.140        by (auto simp: measurable_def) }
   1.141    note eq2 = this[simp]
   1.142 @@ -1168,7 +1168,7 @@
   1.143  
   1.144    have "N = distr N M (T' \<circ> T)"
   1.145      by (subst measure_of_of_measure[of N, symmetric])
   1.146 -       (auto simp add: distr_def sigma_sets_eq intro!: measure_of_eq space_closed)
   1.147 +       (auto simp add: distr_def sets.sigma_sets_eq intro!: measure_of_eq sets.space_closed)
   1.148    also have "\<dots> = distr (distr N M' T) M T'"
   1.149      using T T' by (simp add: distr_distr)
   1.150    also have "\<dots> = distr (density (distr M M' T) (RN_deriv (distr M M' T) (distr N M' T))) M T'"