changeset 41023 9118eb4eb8dc parent 40871 688f6ff859e1 child 41095 c335d880ff82
1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 06 19:18:02 2010 +0100
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Dec 03 15:25:14 2010 +0100
1.3 @@ -29,10 +29,10 @@
1.4      next
1.5        assume not_0: "\<mu> (A i) \<noteq> 0"
1.6        then have "?B i \<noteq> \<omega>" using measure[of i] by auto
1.7 -      then have "inverse (?B i) \<noteq> 0" unfolding pinfreal_inverse_eq_0 by simp
1.8 +      then have "inverse (?B i) \<noteq> 0" unfolding pextreal_inverse_eq_0 by simp
1.9        then show ?thesis using measure[of i] not_0
1.10          by (auto intro!: exI[of _ "inverse (?B i) / 2"]
1.11 -                 simp: pinfreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq)
1.12 +                 simp: pextreal_noteq_omega_Ex zero_le_mult_iff zero_less_mult_iff mult_le_0_iff power_le_zero_eq)
1.13      qed
1.14    qed
1.15    from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
1.16 @@ -49,7 +49,7 @@
1.17        fix N show "n N * \<mu> (A N) \<le> Real ((1 / 2) ^ Suc N)"
1.18          using measure[of N] n[of N]
1.19          by (cases "n N")
1.20 -           (auto simp: pinfreal_noteq_omega_Ex field_simps zero_le_mult_iff
1.21 +           (auto simp: pextreal_noteq_omega_Ex field_simps zero_le_mult_iff
1.22                         mult_le_0_iff mult_less_0_iff power_less_zero_eq
1.23                         power_le_zero_eq inverse_eq_divide less_divide_eq
1.24                         power_divide split: split_if_asm)
1.25 @@ -65,14 +65,14 @@
1.26      then show "0 < ?h x" and "?h x < \<omega>" using n[of i] by auto
1.27    next
1.28      show "?h \<in> borel_measurable M" using range
1.29 -      by (auto intro!: borel_measurable_psuminf borel_measurable_pinfreal_times)
1.30 +      by (auto intro!: borel_measurable_psuminf borel_measurable_pextreal_times)
1.31    qed
1.32  qed
1.34  subsection "Absolutely continuous"
1.36  definition (in measure_space)
1.37 -  "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pinfreal))"
1.38 +  "absolutely_continuous \<nu> = (\<forall>N\<in>null_sets. \<nu> N = (0 :: pextreal))"
1.40  lemma (in sigma_finite_measure) absolutely_continuous_AE:
1.41    assumes "measure_space M \<nu>" "absolutely_continuous \<nu>" "AE x. P x"
1.42 @@ -409,9 +409,9 @@
1.43        moreover {
1.44          have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
1.45            using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
1.46 -        also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pinfreal_less_\<omega>)
1.47 +        also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pextreal_less_\<omega>)
1.48          finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
1.49 -          by (simp add: pinfreal_less_\<omega>) }
1.50 +          by (simp add: pextreal_less_\<omega>) }
1.51        ultimately
1.52        show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
1.53          apply (subst psuminf_minus) by simp_all
1.54 @@ -440,7 +440,7 @@
1.55      def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
1.56      ultimately have b: "b \<noteq> 0" "b \<noteq> \<omega>"
1.57        using M'.finite_measure_of_space
1.58 -      by (auto simp: pinfreal_inverse_eq_0 finite_measure_of_space)
1.59 +      by (auto simp: pextreal_inverse_eq_0 finite_measure_of_space)
1.60      have "finite_measure M (\<lambda>A. b * \<mu> A)" (is "finite_measure M ?b")
1.61      proof
1.62        show "?b {} = 0" by simp
1.63 @@ -486,7 +486,7 @@
1.64          by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
1.65        finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
1.66      hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
1.67 -      by (auto intro!: borel_measurable_indicator borel_measurable_pinfreal_add borel_measurable_pinfreal_times)
1.68 +      by (auto intro!: borel_measurable_indicator borel_measurable_pextreal_add borel_measurable_pextreal_times)
1.69      have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
1.70        "b * \<mu> (space M) \<noteq> \<omega>" "b * \<mu> A0 \<noteq> \<omega>"
1.71        using `A0 \<in> sets M` b
1.72 @@ -494,27 +494,27 @@
1.73          finite_measure_of_space M.finite_measure_of_space
1.74        by auto
1.75      have int_f_finite: "positive_integral f \<noteq> \<omega>"
1.76 -      using M'.finite_measure_of_space pos_t unfolding pinfreal_zero_less_diff_iff
1.77 +      using M'.finite_measure_of_space pos_t unfolding pextreal_zero_less_diff_iff
1.78        by (auto cong: positive_integral_cong)
1.79      have "?t (space M) > b * \<mu> (space M)" unfolding b_def
1.80        apply (simp add: field_simps)
1.81        apply (subst mult_assoc[symmetric])
1.82 -      apply (subst pinfreal_mult_inverse)
1.83 +      apply (subst pextreal_mult_inverse)
1.84        using finite_measure_of_space M'.finite_measure_of_space pos_t pos_M
1.85 -      using pinfreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"]
1.86 +      using pextreal_mult_strict_right_mono[of "Real (1/2)" 1 "?t (space M)"]
1.87        by simp_all
1.88      hence  "0 < ?t (space M) - b * \<mu> (space M)"
1.89 -      by (simp add: pinfreal_zero_less_diff_iff)
1.90 +      by (simp add: pextreal_zero_less_diff_iff)
1.91      also have "\<dots> \<le> ?t A0 - b * \<mu> A0"
1.92 -      using space_less_A0 pos_M pos_t b real[unfolded pinfreal_noteq_omega_Ex] by auto
1.93 -    finally have "b * \<mu> A0 < ?t A0" unfolding pinfreal_zero_less_diff_iff .
1.94 +      using space_less_A0 pos_M pos_t b real[unfolded pextreal_noteq_omega_Ex] by auto
1.95 +    finally have "b * \<mu> A0 < ?t A0" unfolding pextreal_zero_less_diff_iff .
1.96      hence "0 < ?t A0" by auto
1.97      hence "0 < \<mu> A0" using ac unfolding absolutely_continuous_def
1.98        using `A0 \<in> sets M` by auto
1.99      hence "0 < b * \<mu> A0" using b by auto
1.100      from int_f_finite this
1.101      have "?y + 0 < positive_integral f + b * \<mu> A0" unfolding int_f_eq_y
1.102 -      by (rule pinfreal_less_add)
1.103 +      by (rule pextreal_less_add)
1.104      also have "\<dots> = positive_integral ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
1.105        by (simp cong: positive_integral_cong)
1.106      finally have "?y < positive_integral ?f0" by simp
1.107 @@ -530,7 +530,7 @@
1.108          using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
1.109        show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
1.110          using upper_bound[THEN bspec, OF `A \<in> sets M`]
1.111 -         by (simp add: pinfreal_zero_le_diff)
1.112 +         by (simp add: pextreal_zero_le_diff)
1.113      qed
1.114    qed simp
1.115  qed
1.116 @@ -573,8 +573,8 @@
1.117        using Q' by (auto intro: finite_UN)
1.118      with v.measure_finitely_subadditive[of "{.. i}" Q']
1.119      have "\<nu> (?O i) \<le> (\<Sum>i\<le>i. \<nu> (Q' i))" by auto
1.120 -    also have "\<dots> < \<omega>" unfolding setsum_\<omega> pinfreal_less_\<omega> using Q' by auto
1.121 -    finally show "\<nu> (?O i) \<noteq> \<omega>" unfolding pinfreal_less_\<omega> by auto
1.122 +    also have "\<dots> < \<omega>" unfolding setsum_\<omega> pextreal_less_\<omega> using Q' by auto
1.123 +    finally show "\<nu> (?O i) \<noteq> \<omega>" unfolding pextreal_less_\<omega> by auto
1.124    qed auto
1.125    have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp
1.126    have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric]
1.127 @@ -634,7 +634,7 @@
1.128              then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI)
1.129            qed
1.130            finally have "\<mu> A = 0" unfolding a_eq using finite_measure[OF `?O_0 \<in> sets M`]
1.131 -            by (cases "\<mu> A") (auto simp: pinfreal_noteq_omega_Ex)
1.132 +            by (cases "\<mu> A") (auto simp: pextreal_noteq_omega_Ex)
1.133            with `\<mu> A \<noteq> 0` show ?thesis by auto
1.134          qed
1.135        qed }
1.136 @@ -682,7 +682,7 @@
1.137      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
1.138    proof
1.139      fix i
1.140 -    have indicator_eq: "\<And>f x A. (f x :: pinfreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
1.141 +    have indicator_eq: "\<And>f x A. (f x :: pextreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
1.142        = (f x * indicator (Q i) x) * indicator A x"
1.143        unfolding indicator_def by auto
1.144      have fm: "finite_measure (restricted_space (Q i)) \<mu>"
1.145 @@ -718,19 +718,19 @@
1.146    show ?thesis
1.147    proof (safe intro!: bexI[of _ ?f])
1.148      show "?f \<in> borel_measurable M"
1.149 -      by (safe intro!: borel_measurable_psuminf borel_measurable_pinfreal_times
1.150 -        borel_measurable_pinfreal_add borel_measurable_indicator
1.151 +      by (safe intro!: borel_measurable_psuminf borel_measurable_pextreal_times
1.152 +        borel_measurable_pextreal_add borel_measurable_indicator
1.153          borel_measurable_const borel Q_sets Q0 Diff countable_UN)
1.154      fix A assume "A \<in> sets M"
1.155      have *:
1.156        "\<And>x i. indicator A x * (f i x * indicator (Q i) x) =
1.157          f i x * indicator (Q i \<inter> A) x"
1.158 -      "\<And>x i. (indicator A x * indicator Q0 x :: pinfreal) =
1.159 +      "\<And>x i. (indicator A x * indicator Q0 x :: pextreal) =
1.160          indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
1.161      have "positive_integral (\<lambda>x. ?f x * indicator A x) =
1.162        (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
1.163        unfolding f[OF `A \<in> sets M`]
1.164 -      apply (simp del: pinfreal_times(2) add: field_simps *)
1.165 +      apply (simp del: pextreal_times(2) add: field_simps *)
1.166        apply (subst positive_integral_add)
1.167        apply (fastsimp intro: Q0 `A \<in> sets M`)
1.168        apply (fastsimp intro: Q_sets `A \<in> sets M` borel_measurable_psuminf borel)
1.169 @@ -775,7 +775,7 @@
1.170    interpret T: finite_measure M ?T
1.171      unfolding finite_measure_def finite_measure_axioms_def
1.172      by (simp cong: positive_integral_cong)
1.173 -  have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pinfreal)} = N"
1.174 +  have "\<And>N. N \<in> sets M \<Longrightarrow> {x \<in> space M. h x \<noteq> 0 \<and> indicator N x \<noteq> (0::pextreal)} = N"
1.175      using sets_into_space pos by (force simp: indicator_def)
1.176    then have "T.absolutely_continuous \<nu>" using assms(2) borel
1.177      unfolding T.absolutely_continuous_def absolutely_continuous_def
1.178 @@ -786,10 +786,10 @@
1.179    show ?thesis
1.180    proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
1.181      show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
1.182 -      using borel f_borel by (auto intro: borel_measurable_pinfreal_times)
1.183 +      using borel f_borel by (auto intro: borel_measurable_pextreal_times)
1.184      fix A assume "A \<in> sets M"
1.185      then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
1.186 -      using f_borel by (auto intro: borel_measurable_pinfreal_times borel_measurable_indicator)
1.187 +      using f_borel by (auto intro: borel_measurable_pextreal_times borel_measurable_indicator)
1.188      from positive_integral_translated_density[OF borel this]
1.189      show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
1.190        unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
1.191 @@ -834,7 +834,7 @@
1.192      finally have "\<mu> {x\<in>space M. (f x - g x) * indicator ?N x \<noteq> 0} = 0"
1.193        using borel N by (subst (asm) positive_integral_0_iff) auto
1.194      moreover have "{x\<in>space M. (f x - g x) * indicator ?N x \<noteq> 0} = ?N"
1.195 -      by (auto simp: pinfreal_zero_le_diff)
1.196 +      by (auto simp: pextreal_zero_le_diff)
1.197      ultimately have "?N \<in> null_sets" using N by simp }
1.198    from this[OF borel g_fin eq] this[OF borel(2,1) fin]
1.199    have "{x\<in>space M. g x < f x} \<union> {x\<in>space M. f x < g x} \<in> null_sets"
1.200 @@ -866,15 +866,15 @@
1.201    from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
1.202    let ?N = "{x\<in>space M. f x \<noteq> f' x}"
1.203    have "?N \<in> sets M" using borel by auto
1.204 -  have *: "\<And>i x A. \<And>y::pinfreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x"
1.205 +  have *: "\<And>i x A. \<And>y::pextreal. y * indicator (Q i) x * indicator A x = y * indicator (Q i \<inter> A) x"
1.206      unfolding indicator_def by auto
1.207    have 1: "\<forall>i. AE x. ?f (Q i) x = ?f' (Q i) x"
1.208      using borel Q_fin Q
1.209      by (intro finite_density_unique[THEN iffD1] allI)
1.210 -       (auto intro!: borel_measurable_pinfreal_times f Int simp: *)
1.211 +       (auto intro!: borel_measurable_pextreal_times f Int simp: *)
1.212    have 2: "AE x. ?f Q0 x = ?f' Q0 x"
1.213    proof (rule AE_I')
1.214 -    { fix f :: "'a \<Rightarrow> pinfreal" assume borel: "f \<in> borel_measurable M"
1.215 +    { fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
1.216          and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
1.217        let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
1.218        have "(\<Union>i. ?A i) \<in> null_sets"
1.219 @@ -893,7 +893,7 @@
1.220        qed
1.221        also have "(\<Union>i. ?A i) = Q0 \<inter> {x\<in>space M. f x < \<omega>}"
1.222          by (auto simp: less_\<omega>_Ex_of_nat)
1.223 -      finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" by (simp add: pinfreal_less_\<omega>) }
1.224 +      finally have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" by (simp add: pextreal_less_\<omega>) }
1.225      from this[OF borel(1) refl] this[OF borel(2) f]
1.226      have "Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>} \<in> null_sets" "Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>} \<in> null_sets" by simp_all
1.227      then show "(Q0 \<inter> {x\<in>space M. f x \<noteq> \<omega>}) \<union> (Q0 \<inter> {x\<in>space M. f' x \<noteq> \<omega>}) \<in> null_sets" by (rule null_sets_Un)
1.228 @@ -927,7 +927,7 @@
1.229    interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)"
1.230      using borel(2) by (rule measure_space_density)
1.231    { fix A assume "A \<in> sets M"
1.232 -    then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pinfreal)} = A"
1.233 +    then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pextreal)} = A"
1.234        using pos sets_into_space by (force simp: indicator_def)
1.235      then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets"
1.236        using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
1.237 @@ -1027,7 +1027,7 @@
1.238          apply (subst positive_integral_0_iff)
1.239          apply fast
1.240          apply (subst (asm) AE_iff_null_set)
1.241 -        apply (intro borel_measurable_pinfreal_neq_const)
1.242 +        apply (intro borel_measurable_pextreal_neq_const)
1.243          apply fast
1.244          by simp
1.245        then show ?thesis by simp
1.246 @@ -1130,7 +1130,7 @@
1.247      using sf.RN_deriv(1)[OF \<nu>' ac]
1.248      unfolding measurable_vimage_iff_inv[OF f] comp_def .
1.249    fix A assume "A \<in> sets M"
1.250 -  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (the_inv_into S f x) = (indicator A x :: pinfreal)"
1.251 +  then have *: "\<And>x. x \<in> space M \<Longrightarrow> indicator (f -` A \<inter> S) (the_inv_into S f x) = (indicator A x :: pextreal)"
1.252      using f[unfolded bij_betw_def]
1.253      unfolding indicator_def by (auto simp: f_the_inv_into_f the_inv_into_in)
1.254    have "\<nu> (f ` (f -` A \<inter> S)) = sf.positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) x * indicator (f -` A \<inter> S) x)"
1.255 @@ -1160,7 +1160,7 @@
1.256  proof -
1.257    interpret \<nu>: sigma_finite_measure M \<nu> by fact
1.258    have ms: "measure_space M \<nu>" by default
1.259 -  have minus_cong: "\<And>A B A' B'::pinfreal. A = A' \<Longrightarrow> B = B' \<Longrightarrow> real A - real B = real A' - real B'" by simp
1.260 +  have minus_cong: "\<And>A B A' B'::pextreal. A = A' \<Longrightarrow> B = B' \<Longrightarrow> real A - real B = real A' - real B'" by simp
1.261    have f': "(\<lambda>x. - f x) \<in> borel_measurable M" using f by auto
1.262    { fix f :: "'a \<Rightarrow> real" assume "f \<in> borel_measurable M"
1.263      { fix x assume *: "RN_deriv \<nu> x \<noteq> \<omega>"