src/HOL/Probability/Radon_Nikodym.thy
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.33  
    1.34  subsection "Absolutely continuous"
    1.35  
    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.39  
    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>"