src/HOL/Probability/Radon_Nikodym.thy
changeset 41544 c3b977fee8a3
parent 41097 a1abfa4e2b44
child 41661 baf1964bc468
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 14 14:21:26 2011 +0100
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Jan 14 14:21:48 2011 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4  qed
     1.5  
     1.6  lemma (in measure_space) density_is_absolutely_continuous:
     1.7 -  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
     1.8 +  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
     1.9    shows "absolutely_continuous \<nu>"
    1.10    using assms unfolding absolutely_continuous_def
    1.11    by (simp add: positive_integral_null_set)
    1.12 @@ -289,10 +289,10 @@
    1.13  lemma (in finite_measure) Radon_Nikodym_finite_measure:
    1.14    assumes "finite_measure M \<nu>"
    1.15    assumes "absolutely_continuous \<nu>"
    1.16 -  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
    1.17 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
    1.18  proof -
    1.19    interpret M': finite_measure M \<nu> using assms(1) .
    1.20 -  def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A}"
    1.21 +  def G \<equiv> "{g \<in> borel_measurable M. \<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A}"
    1.22    have "(\<lambda>x. 0) \<in> G" unfolding G_def by auto
    1.23    hence "G \<noteq> {}" by auto
    1.24    { fix f g assume f: "f \<in> G" and g: "g \<in> G"
    1.25 @@ -308,16 +308,16 @@
    1.26        have "\<And>x. x \<in> space M \<Longrightarrow> max (g x) (f x) * indicator A x =
    1.27          g x * indicator (?A \<inter> A) x + f x * indicator ((space M - ?A) \<inter> A) x"
    1.28          by (auto simp: indicator_def max_def)
    1.29 -      hence "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) =
    1.30 -        positive_integral (\<lambda>x. g x * indicator (?A \<inter> A) x) +
    1.31 -        positive_integral (\<lambda>x. f x * indicator ((space M - ?A) \<inter> A) x)"
    1.32 +      hence "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x) =
    1.33 +        (\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x) +
    1.34 +        (\<integral>\<^isup>+x. f x * indicator ((space M - ?A) \<inter> A) x)"
    1.35          using f g sets unfolding G_def
    1.36          by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
    1.37        also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
    1.38          using f g sets unfolding G_def by (auto intro!: add_mono)
    1.39        also have "\<dots> = \<nu> A"
    1.40          using M'.measure_additive[OF sets] union by auto
    1.41 -      finally show "positive_integral (\<lambda>x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
    1.42 +      finally show "(\<integral>\<^isup>+x. max (g x) (f x) * indicator A x) \<le> \<nu> A" .
    1.43      qed }
    1.44    note max_in_G = this
    1.45    { fix f g assume  "f \<up> g" and f: "\<And>i. f i \<in> G"
    1.46 @@ -331,17 +331,17 @@
    1.47        hence "\<And>i. (\<lambda>x. f i x * indicator A x) \<in> borel_measurable M"
    1.48          using f_borel by (auto intro!: borel_measurable_indicator)
    1.49        from positive_integral_isoton[OF isoton_indicator[OF `f \<up> g`] this]
    1.50 -      have SUP: "positive_integral (\<lambda>x. g x * indicator A x) =
    1.51 -          (SUP i. positive_integral (\<lambda>x. f i x * indicator A x))"
    1.52 +      have SUP: "(\<integral>\<^isup>+x. g x * indicator A x) =
    1.53 +          (SUP i. (\<integral>\<^isup>+x. f i x * indicator A x))"
    1.54          unfolding isoton_def by simp
    1.55 -      show "positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
    1.56 +      show "(\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A" unfolding SUP
    1.57          using f `A \<in> sets M` unfolding G_def by (auto intro!: SUP_leI)
    1.58      qed }
    1.59    note SUP_in_G = this
    1.60    let ?y = "SUP g : G. positive_integral g"
    1.61    have "?y \<le> \<nu> (space M)" unfolding G_def
    1.62    proof (safe intro!: SUP_leI)
    1.63 -    fix g assume "\<forall>A\<in>sets M. positive_integral (\<lambda>x. g x * indicator A x) \<le> \<nu> A"
    1.64 +    fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x) \<le> \<nu> A"
    1.65      from this[THEN bspec, OF top] show "positive_integral g \<le> \<nu> (space M)"
    1.66        by (simp cong: positive_integral_cong)
    1.67    qed
    1.68 @@ -384,7 +384,7 @@
    1.69        by (auto intro!: SUP_mono positive_integral_mono Max_ge)
    1.70    qed
    1.71    finally have int_f_eq_y: "positive_integral f = ?y" .
    1.72 -  let "?t A" = "\<nu> A - positive_integral (\<lambda>x. f x * indicator A x)"
    1.73 +  let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. f x * indicator A x)"
    1.74    have "finite_measure M ?t"
    1.75    proof
    1.76      show "?t {} = 0" by simp
    1.77 @@ -392,26 +392,26 @@
    1.78      show "countably_additive M ?t" unfolding countably_additive_def
    1.79      proof safe
    1.80        fix A :: "nat \<Rightarrow> 'a set"  assume A: "range A \<subseteq> sets M" "disjoint_family A"
    1.81 -      have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
    1.82 -        = positive_integral (\<lambda>x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
    1.83 +      have "(\<Sum>\<^isub>\<infinity> n. (\<integral>\<^isup>+x. f x * indicator (A n) x))
    1.84 +        = (\<integral>\<^isup>+x. (\<Sum>\<^isub>\<infinity>n. f x * indicator (A n) x))"
    1.85          using `range A \<subseteq> sets M`
    1.86          by (rule_tac positive_integral_psuminf[symmetric]) (auto intro!: borel_measurable_indicator)
    1.87 -      also have "\<dots> = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)"
    1.88 +      also have "\<dots> = (\<integral>\<^isup>+x. f x * indicator (\<Union>n. A n) x)"
    1.89          apply (rule positive_integral_cong)
    1.90          apply (subst psuminf_cmult_right)
    1.91          unfolding psuminf_indicator[OF `disjoint_family A`] ..
    1.92 -      finally have "(\<Sum>\<^isub>\<infinity> n. positive_integral (\<lambda>x. f x * indicator (A n) x))
    1.93 -        = positive_integral (\<lambda>x. f x * indicator (\<Union>n. A n) x)" .
    1.94 +      finally have "(\<Sum>\<^isub>\<infinity> n. (\<integral>\<^isup>+x. f x * indicator (A n) x))
    1.95 +        = (\<integral>\<^isup>+x. f x * indicator (\<Union>n. A n) x)" .
    1.96        moreover have "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (\<Union>n. A n)"
    1.97          using M'.measure_countably_additive A by (simp add: comp_def)
    1.98 -      moreover have "\<And>i. positive_integral (\<lambda>x. f x * indicator (A i) x) \<le> \<nu> (A i)"
    1.99 +      moreover have "\<And>i. (\<integral>\<^isup>+x. f x * indicator (A i) x) \<le> \<nu> (A i)"
   1.100            using A `f \<in> G` unfolding G_def by auto
   1.101        moreover have v_fin: "\<nu> (\<Union>i. A i) \<noteq> \<omega>" using M'.finite_measure A by (simp add: countable_UN)
   1.102        moreover {
   1.103 -        have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
   1.104 +        have "(\<integral>\<^isup>+x. f x * indicator (\<Union>i. A i) x) \<le> \<nu> (\<Union>i. A i)"
   1.105            using A `f \<in> G` unfolding G_def by (auto simp: countable_UN)
   1.106          also have "\<nu> (\<Union>i. A i) < \<omega>" using v_fin by (simp add: pextreal_less_\<omega>)
   1.107 -        finally have "positive_integral (\<lambda>x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
   1.108 +        finally have "(\<integral>\<^isup>+x. f x * indicator (\<Union>i. A i) x) \<noteq> \<omega>"
   1.109            by (simp add: pextreal_less_\<omega>) }
   1.110        ultimately
   1.111        show "(\<Sum>\<^isub>\<infinity> n. ?t (A n)) = ?t (\<Union>i. A i)"
   1.112 @@ -433,9 +433,9 @@
   1.113      hence pos_M: "0 < \<mu> (space M)"
   1.114        using ac top unfolding absolutely_continuous_def by auto
   1.115      moreover
   1.116 -    have "positive_integral (\<lambda>x. f x * indicator (space M) x) \<le> \<nu> (space M)"
   1.117 +    have "(\<integral>\<^isup>+x. f x * indicator (space M) x) \<le> \<nu> (space M)"
   1.118        using `f \<in> G` unfolding G_def by auto
   1.119 -    hence "positive_integral (\<lambda>x. f x * indicator (space M) x) \<noteq> \<omega>"
   1.120 +    hence "(\<integral>\<^isup>+x. f x * indicator (space M) x) \<noteq> \<omega>"
   1.121        using M'.finite_measure_of_space by auto
   1.122      moreover
   1.123      def b \<equiv> "?t (space M) / \<mu> (space M) / 2"
   1.124 @@ -462,30 +462,30 @@
   1.125      let "?f0 x" = "f x + b * indicator A0 x"
   1.126      { fix A assume A: "A \<in> sets M"
   1.127        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   1.128 -      have "positive_integral (\<lambda>x. ?f0 x  * indicator A x) =
   1.129 -        positive_integral (\<lambda>x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
   1.130 +      have "(\<integral>\<^isup>+x. ?f0 x  * indicator A x) =
   1.131 +        (\<integral>\<^isup>+x. f x * indicator A x + b * indicator (A \<inter> A0) x)"
   1.132          by (auto intro!: positive_integral_cong simp: field_simps indicator_inter_arith)
   1.133 -      hence "positive_integral (\<lambda>x. ?f0 x * indicator A x) =
   1.134 -          positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
   1.135 +      hence "(\<integral>\<^isup>+x. ?f0 x * indicator A x) =
   1.136 +          (\<integral>\<^isup>+x. f x * indicator A x) + b * \<mu> (A \<inter> A0)"
   1.137          using `A0 \<in> sets M` `A \<inter> A0 \<in> sets M` A
   1.138          by (simp add: borel_measurable_indicator positive_integral_add positive_integral_cmult_indicator) }
   1.139      note f0_eq = this
   1.140      { fix A assume A: "A \<in> sets M"
   1.141        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
   1.142 -      have f_le_v: "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
   1.143 +      have f_le_v: "(\<integral>\<^isup>+x. f x * indicator A x) \<le> \<nu> A"
   1.144          using `f \<in> G` A unfolding G_def by auto
   1.145        note f0_eq[OF A]
   1.146 -      also have "positive_integral (\<lambda>x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
   1.147 -          positive_integral (\<lambda>x. f x * indicator A x) + ?t (A \<inter> A0)"
   1.148 +      also have "(\<integral>\<^isup>+x. f x * indicator A x) + b * \<mu> (A \<inter> A0) \<le>
   1.149 +          (\<integral>\<^isup>+x. f x * indicator A x) + ?t (A \<inter> A0)"
   1.150          using bM_le_t[OF `A \<inter> A0 \<in> sets M`] `A \<in> sets M` `A0 \<in> sets M`
   1.151          by (auto intro!: add_left_mono)
   1.152 -      also have "\<dots> \<le> positive_integral (\<lambda>x. f x * indicator A x) + ?t A"
   1.153 +      also have "\<dots> \<le> (\<integral>\<^isup>+x. f x * indicator A x) + ?t A"
   1.154          using M.measure_mono[simplified, OF _ `A \<inter> A0 \<in> sets M` `A \<in> sets M`]
   1.155          by (auto intro!: add_left_mono)
   1.156        also have "\<dots> \<le> \<nu> A"
   1.157          using f_le_v M'.finite_measure[simplified, OF `A \<in> sets M`]
   1.158 -        by (cases "positive_integral (\<lambda>x. f x * indicator A x)", cases "\<nu> A", auto)
   1.159 -      finally have "positive_integral (\<lambda>x. ?f0 x * indicator A x) \<le> \<nu> A" . }
   1.160 +        by (cases "(\<integral>\<^isup>+x. f x * indicator A x)", cases "\<nu> A", auto)
   1.161 +      finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x) \<le> \<nu> A" . }
   1.162      hence "?f0 \<in> G" using `A0 \<in> sets M` unfolding G_def
   1.163        by (auto intro!: borel_measurable_indicator borel_measurable_pextreal_add borel_measurable_pextreal_times)
   1.164      have real: "?t (space M) \<noteq> \<omega>" "?t A0 \<noteq> \<omega>"
   1.165 @@ -525,11 +525,11 @@
   1.166    show ?thesis
   1.167    proof (safe intro!: bexI[of _ f])
   1.168      fix A assume "A\<in>sets M"
   1.169 -    show "\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   1.170 +    show "\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   1.171      proof (rule antisym)
   1.172 -      show "positive_integral (\<lambda>x. f x * indicator A x) \<le> \<nu> A"
   1.173 +      show "(\<integral>\<^isup>+x. f x * indicator A x) \<le> \<nu> A"
   1.174          using `f \<in> G` `A \<in> sets M` unfolding G_def by auto
   1.175 -      show "\<nu> A \<le> positive_integral (\<lambda>x. f x * indicator A x)"
   1.176 +      show "\<nu> A \<le> (\<integral>\<^isup>+x. f x * indicator A x)"
   1.177          using upper_bound[THEN bspec, OF `A \<in> sets M`]
   1.178           by (simp add: pextreal_zero_le_diff)
   1.179      qed
   1.180 @@ -669,7 +669,7 @@
   1.181  lemma (in finite_measure) Radon_Nikodym_finite_measure_infinite:
   1.182    assumes "measure_space M \<nu>"
   1.183    assumes "absolutely_continuous \<nu>"
   1.184 -  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   1.185 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   1.186  proof -
   1.187    interpret v: measure_space M \<nu> by fact
   1.188    from split_space_into_finite_sets_and_rest[OF assms]
   1.189 @@ -680,7 +680,7 @@
   1.190      and Q_fin: "\<And>i. \<nu> (Q i) \<noteq> \<omega>" by force
   1.191    from Q have Q_sets: "\<And>i. Q i \<in> sets M" by auto
   1.192    have "\<forall>i. \<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   1.193 -    \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
   1.194 +    \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x))"
   1.195    proof
   1.196      fix i
   1.197      have indicator_eq: "\<And>f x A. (f x :: pextreal) * indicator (Q i \<inter> A) x * indicator (Q i) x
   1.198 @@ -702,17 +702,17 @@
   1.199        by (auto simp: R.absolutely_continuous_def absolutely_continuous_def)
   1.200      from finite_measure.Radon_Nikodym_finite_measure[OF fm fmv this]
   1.201      obtain f where f: "(\<lambda>x. f x * indicator (Q i) x) \<in> borel_measurable M"
   1.202 -      and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. (f x * indicator (Q i) x) * indicator A x)"
   1.203 +      and f_int: "\<And>A. A\<in>sets M \<Longrightarrow> \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. (f x * indicator (Q i) x) * indicator A x)"
   1.204        unfolding Bex_def borel_measurable_restricted[OF `Q i \<in> sets M`]
   1.205          positive_integral_restricted[OF `Q i \<in> sets M`] by (auto simp: indicator_eq)
   1.206      then show "\<exists>f. f\<in>borel_measurable M \<and> (\<forall>A\<in>sets M.
   1.207 -      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f x * indicator (Q i \<inter> A) x))"
   1.208 +      \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f x * indicator (Q i \<inter> A) x))"
   1.209        by (fastsimp intro!: exI[of _ "\<lambda>x. f x * indicator (Q i) x"] positive_integral_cong
   1.210            simp: indicator_def)
   1.211    qed
   1.212    from choice[OF this] obtain f where borel: "\<And>i. f i \<in> borel_measurable M"
   1.213      and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
   1.214 -      \<nu> (Q i \<inter> A) = positive_integral (\<lambda>x. f i x * indicator (Q i \<inter> A) x)"
   1.215 +      \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x)"
   1.216      by auto
   1.217    let "?f x" =
   1.218      "(\<Sum>\<^isub>\<infinity> i. f i x * indicator (Q i) x) + \<omega> * indicator Q0 x"
   1.219 @@ -728,7 +728,7 @@
   1.220          f i x * indicator (Q i \<inter> A) x"
   1.221        "\<And>x i. (indicator A x * indicator Q0 x :: pextreal) =
   1.222          indicator (Q0 \<inter> A) x" by (auto simp: indicator_def)
   1.223 -    have "positive_integral (\<lambda>x. ?f x * indicator A x) =
   1.224 +    have "(\<integral>\<^isup>+x. ?f x * indicator A x) =
   1.225        (\<Sum>\<^isub>\<infinity> i. \<nu> (Q i \<inter> A)) + \<omega> * \<mu> (Q0 \<inter> A)"
   1.226        unfolding f[OF `A \<in> sets M`]
   1.227        apply (simp del: pextreal_times(2) add: field_simps *)
   1.228 @@ -755,7 +755,7 @@
   1.229        using Q_sets `A \<in> sets M` Q0(1) by (auto intro!: countable_UN)
   1.230      moreover have "((\<Union>i. Q i) \<inter> A) \<union> (Q0 \<inter> A) = A" "((\<Union>i. Q i) \<inter> A) \<inter> (Q0 \<inter> A) = {}"
   1.231        using `A \<in> sets M` sets_into_space Q0 by auto
   1.232 -    ultimately show "\<nu> A = positive_integral (\<lambda>x. ?f x * indicator A x)"
   1.233 +    ultimately show "\<nu> A = (\<integral>\<^isup>+x. ?f x * indicator A x)"
   1.234        using v.measure_additive[simplified, of "(\<Union>i. Q i) \<inter> A" "Q0 \<inter> A"]
   1.235        by simp
   1.236    qed
   1.237 @@ -764,14 +764,14 @@
   1.238  lemma (in sigma_finite_measure) Radon_Nikodym:
   1.239    assumes "measure_space M \<nu>"
   1.240    assumes "absolutely_continuous \<nu>"
   1.241 -  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   1.242 +  shows "\<exists>f \<in> borel_measurable M. \<forall>A\<in>sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   1.243  proof -
   1.244    from Ex_finite_integrable_function
   1.245    obtain h where finite: "positive_integral h \<noteq> \<omega>" and
   1.246      borel: "h \<in> borel_measurable M" and
   1.247      pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
   1.248      "\<And>x. x \<in> space M \<Longrightarrow> h x < \<omega>" by auto
   1.249 -  let "?T A" = "positive_integral (\<lambda>x. h x * indicator A x)"
   1.250 +  let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x)"
   1.251    from measure_space_density[OF borel] finite
   1.252    interpret T: finite_measure M ?T
   1.253      unfolding finite_measure_def finite_measure_axioms_def
   1.254 @@ -792,7 +792,7 @@
   1.255      then have "(\<lambda>x. f x * indicator A x) \<in> borel_measurable M"
   1.256        using f_borel by (auto intro: borel_measurable_pextreal_times borel_measurable_indicator)
   1.257      from positive_integral_translated_density[OF borel this]
   1.258 -    show "\<nu> A = positive_integral (\<lambda>x. h x * f x * indicator A x)"
   1.259 +    show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x)"
   1.260        unfolding fT[OF `A \<in> sets M`] by (simp add: field_simps)
   1.261    qed
   1.262  qed
   1.263 @@ -802,7 +802,7 @@
   1.264  lemma (in measure_space) finite_density_unique:
   1.265    assumes borel: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   1.266    and fin: "positive_integral f < \<omega>"
   1.267 -  shows "(\<forall>A\<in>sets M. positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. g x * indicator A x))
   1.268 +  shows "(\<forall>A\<in>sets M. (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. g x * indicator A x))
   1.269      \<longleftrightarrow> (AE x. f x = g x)"
   1.270      (is "(\<forall>A\<in>sets M. ?P f A = ?P g A) \<longleftrightarrow> _")
   1.271  proof (intro iffI ballI)
   1.272 @@ -817,7 +817,7 @@
   1.273        and g_fin: "positive_integral g < \<omega>" and eq: "\<forall>A\<in>sets M. ?P f A = ?P g A"
   1.274      let ?N = "{x\<in>space M. g x < f x}"
   1.275      have N: "?N \<in> sets M" using borel by simp
   1.276 -    have "?P (\<lambda>x. (f x - g x)) ?N = positive_integral (\<lambda>x. f x * indicator ?N x - g x * indicator ?N x)"
   1.277 +    have "?P (\<lambda>x. (f x - g x)) ?N = (\<integral>\<^isup>+x. f x * indicator ?N x - g x * indicator ?N x)"
   1.278        by (auto intro!: positive_integral_cong simp: indicator_def)
   1.279      also have "\<dots> = ?P f ?N - ?P g ?N"
   1.280      proof (rule positive_integral_diff)
   1.281 @@ -848,7 +848,7 @@
   1.282  
   1.283  lemma (in finite_measure) density_unique_finite_measure:
   1.284    assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   1.285 -  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
   1.286 +  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. f' x * indicator A x)"
   1.287      (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   1.288    shows "AE x. f x = f' x"
   1.289  proof -
   1.290 @@ -876,13 +876,13 @@
   1.291    have 2: "AE x. ?f Q0 x = ?f' Q0 x"
   1.292    proof (rule AE_I')
   1.293      { fix f :: "'a \<Rightarrow> pextreal" assume borel: "f \<in> borel_measurable M"
   1.294 -        and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   1.295 +        and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   1.296        let "?A i" = "Q0 \<inter> {x \<in> space M. f x < of_nat i}"
   1.297        have "(\<Union>i. ?A i) \<in> null_sets"
   1.298        proof (rule null_sets_UN)
   1.299          fix i have "?A i \<in> sets M"
   1.300            using borel Q0(1) by auto
   1.301 -        have "?\<nu> (?A i) \<le> positive_integral (\<lambda>x. of_nat i * indicator (?A i) x)"
   1.302 +        have "?\<nu> (?A i) \<le> (\<integral>\<^isup>+x. of_nat i * indicator (?A i) x)"
   1.303            unfolding eq[OF `?A i \<in> sets M`]
   1.304            by (auto intro!: positive_integral_mono simp: indicator_def)
   1.305          also have "\<dots> = of_nat i * \<mu> (?A i)"
   1.306 @@ -912,38 +912,38 @@
   1.307  
   1.308  lemma (in sigma_finite_measure) density_unique:
   1.309    assumes borel: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   1.310 -  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. f' x * indicator A x)"
   1.311 +  assumes f: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. f' x * indicator A x)"
   1.312      (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
   1.313    shows "AE x. f x = f' x"
   1.314  proof -
   1.315    obtain h where h_borel: "h \<in> borel_measurable M"
   1.316      and fin: "positive_integral h \<noteq> \<omega>" and pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>"
   1.317      using Ex_finite_integrable_function by auto
   1.318 -  interpret h: measure_space M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
   1.319 +  interpret h: measure_space M "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x)"
   1.320      using h_borel by (rule measure_space_density)
   1.321 -  interpret h: finite_measure M "\<lambda>A. positive_integral (\<lambda>x. h x * indicator A x)"
   1.322 +  interpret h: finite_measure M "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x)"
   1.323      by default (simp cong: positive_integral_cong add: fin)
   1.324 -  interpret f: measure_space M "\<lambda>A. positive_integral (\<lambda>x. f x * indicator A x)"
   1.325 +  interpret f: measure_space M "\<lambda>A. (\<integral>\<^isup>+x. f x * indicator A x)"
   1.326      using borel(1) by (rule measure_space_density)
   1.327 -  interpret f': measure_space M "\<lambda>A. positive_integral (\<lambda>x. f' x * indicator A x)"
   1.328 +  interpret f': measure_space M "\<lambda>A. (\<integral>\<^isup>+x. f' x * indicator A x)"
   1.329      using borel(2) by (rule measure_space_density)
   1.330    { fix A assume "A \<in> sets M"
   1.331      then have " {x \<in> space M. h x \<noteq> 0 \<and> indicator A x \<noteq> (0::pextreal)} = A"
   1.332        using pos sets_into_space by (force simp: indicator_def)
   1.333 -    then have "positive_integral (\<lambda>xa. h xa * indicator A xa) = 0 \<longleftrightarrow> A \<in> null_sets"
   1.334 +    then have "(\<integral>\<^isup>+x. h x * indicator A x) = 0 \<longleftrightarrow> A \<in> null_sets"
   1.335        using h_borel `A \<in> sets M` by (simp add: positive_integral_0_iff) }
   1.336    note h_null_sets = this
   1.337    { fix A assume "A \<in> sets M"
   1.338 -    have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) =
   1.339 +    have "(\<integral>\<^isup>+x. h x * (f x * indicator A x)) =
   1.340        f.positive_integral (\<lambda>x. h x * indicator A x)"
   1.341        using `A \<in> sets M` h_borel borel
   1.342        by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
   1.343      also have "\<dots> = f'.positive_integral (\<lambda>x. h x * indicator A x)"
   1.344        by (rule f'.positive_integral_cong_measure) (rule f)
   1.345 -    also have "\<dots> = positive_integral (\<lambda>x. h x * (f' x * indicator A x))"
   1.346 +    also have "\<dots> = (\<integral>\<^isup>+x. h x * (f' x * indicator A x))"
   1.347        using `A \<in> sets M` h_borel borel
   1.348        by (simp add: positive_integral_translated_density ac_simps cong: positive_integral_cong)
   1.349 -    finally have "positive_integral (\<lambda>x. h x * (f x * indicator A x)) = positive_integral (\<lambda>x. h x * (f' x * indicator A x))" . }
   1.350 +    finally have "(\<integral>\<^isup>+x. h x * (f x * indicator A x)) = (\<integral>\<^isup>+x. h x * (f' x * indicator A x))" . }
   1.351    then have "h.almost_everywhere (\<lambda>x. f x = f' x)"
   1.352      using h_borel borel
   1.353      by (intro h.density_unique_finite_measure[OF borel])
   1.354 @@ -955,7 +955,7 @@
   1.355  
   1.356  lemma (in sigma_finite_measure) sigma_finite_iff_density_finite:
   1.357    assumes \<nu>: "measure_space M \<nu>" and f: "f \<in> borel_measurable M"
   1.358 -    and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   1.359 +    and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   1.360    shows "sigma_finite_measure M \<nu> \<longleftrightarrow> (AE x. f x \<noteq> \<omega>)"
   1.361  proof
   1.362    assume "sigma_finite_measure M \<nu>"
   1.363 @@ -965,10 +965,10 @@
   1.364      and fin: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x \<and> h x < \<omega>" by auto
   1.365    have "AE x. f x * h x \<noteq> \<omega>"
   1.366    proof (rule AE_I')
   1.367 -    have "\<nu>.positive_integral h = positive_integral (\<lambda>x. f x * h x)"
   1.368 +    have "\<nu>.positive_integral h = (\<integral>\<^isup>+x. f x * h x)"
   1.369        by (simp add: \<nu>.positive_integral_cong_measure[symmetric, OF eq[symmetric]])
   1.370           (intro positive_integral_translated_density f h)
   1.371 -    then have "positive_integral (\<lambda>x. f x * h x) \<noteq> \<omega>"
   1.372 +    then have "(\<integral>\<^isup>+x. f x * h x) \<noteq> \<omega>"
   1.373        using h(2) by simp
   1.374      then show "(\<lambda>x. f x * h x) -` {\<omega>} \<inter> space M \<in> null_sets"
   1.375        using f h(1) by (auto intro!: positive_integral_omega borel_measurable_vimage)
   1.376 @@ -1018,12 +1018,12 @@
   1.377    next
   1.378      fix n obtain i j where
   1.379        [simp]: "prod_decode n = (i, j)" by (cases "prod_decode n") auto
   1.380 -    have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
   1.381 +    have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) \<noteq> \<omega>"
   1.382      proof (cases i)
   1.383        case 0
   1.384        have "AE x. f x * indicator (A i \<inter> Q j) x = 0"
   1.385          using AE by (rule AE_mp) (auto intro!: AE_cong simp: A_def `i = 0`)
   1.386 -      then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) = 0"
   1.387 +      then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) = 0"
   1.388          using A_in_sets f
   1.389          apply (subst positive_integral_0_iff)
   1.390          apply fast
   1.391 @@ -1034,8 +1034,8 @@
   1.392        then show ?thesis by simp
   1.393      next
   1.394        case (Suc n)
   1.395 -      then have "positive_integral (\<lambda>x. f x * indicator (A i \<inter> Q j) x) \<le>
   1.396 -        positive_integral (\<lambda>x. of_nat (Suc n) * indicator (Q j) x)"
   1.397 +      then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x) \<le>
   1.398 +        (\<integral>\<^isup>+x. of_nat (Suc n) * indicator (Q j) x)"
   1.399          by (auto intro!: positive_integral_mono simp: indicator_def A_def)
   1.400        also have "\<dots> = of_nat (Suc n) * \<mu> (Q j)"
   1.401          using Q by (auto intro!: positive_integral_cmult_indicator)
   1.402 @@ -1052,7 +1052,7 @@
   1.403  
   1.404  definition (in sigma_finite_measure)
   1.405    "RN_deriv \<nu> \<equiv> SOME f. f \<in> borel_measurable M \<and>
   1.406 -    (\<forall>A \<in> sets M. \<nu> A = positive_integral (\<lambda>x. f x * indicator A x))"
   1.407 +    (\<forall>A \<in> sets M. \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x))"
   1.408  
   1.409  lemma (in sigma_finite_measure) RN_deriv_cong:
   1.410    assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" "\<And>A. A \<in> sets M \<Longrightarrow> \<nu>' A = \<nu> A"
   1.411 @@ -1069,7 +1069,7 @@
   1.412    assumes "measure_space M \<nu>"
   1.413    assumes "absolutely_continuous \<nu>"
   1.414    shows "RN_deriv \<nu> \<in> borel_measurable M" (is ?borel)
   1.415 -  and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
   1.416 +  and "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)"
   1.417      (is "\<And>A. _ \<Longrightarrow> ?int A")
   1.418  proof -
   1.419    note Ex = Radon_Nikodym[OF assms, unfolded Bex_def]
   1.420 @@ -1082,13 +1082,13 @@
   1.421  lemma (in sigma_finite_measure) RN_deriv_positive_integral:
   1.422    assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
   1.423      and f: "f \<in> borel_measurable M"
   1.424 -  shows "measure_space.positive_integral M \<nu> f = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
   1.425 +  shows "measure_space.positive_integral M \<nu> f = (\<integral>\<^isup>+x. RN_deriv \<nu> x * f x)"
   1.426  proof -
   1.427    interpret \<nu>: measure_space M \<nu> by fact
   1.428    have "\<nu>.positive_integral f =
   1.429 -    measure_space.positive_integral M (\<lambda>A. positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)) f"
   1.430 +    measure_space.positive_integral M (\<lambda>A. (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)) f"
   1.431      by (intro \<nu>.positive_integral_cong_measure[symmetric] RN_deriv(2)[OF \<nu>, symmetric])
   1.432 -  also have "\<dots> = positive_integral (\<lambda>x. RN_deriv \<nu> x * f x)"
   1.433 +  also have "\<dots> = (\<integral>\<^isup>+x. RN_deriv \<nu> x * f x)"
   1.434      by (intro positive_integral_translated_density RN_deriv[OF \<nu>] f)
   1.435    finally show ?thesis .
   1.436  qed
   1.437 @@ -1096,11 +1096,11 @@
   1.438  lemma (in sigma_finite_measure) RN_deriv_unique:
   1.439    assumes \<nu>: "measure_space M \<nu>" "absolutely_continuous \<nu>"
   1.440    and f: "f \<in> borel_measurable M"
   1.441 -  and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = positive_integral (\<lambda>x. f x * indicator A x)"
   1.442 +  and eq: "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = (\<integral>\<^isup>+x. f x * indicator A x)"
   1.443    shows "AE x. f x = RN_deriv \<nu> x"
   1.444  proof (rule density_unique[OF f RN_deriv(1)[OF \<nu>]])
   1.445    fix A assume A: "A \<in> sets M"
   1.446 -  show "positive_integral (\<lambda>x. f x * indicator A x) = positive_integral (\<lambda>x. RN_deriv \<nu> x * indicator A x)"
   1.447 +  show "(\<integral>\<^isup>+x. f x * indicator A x) = (\<integral>\<^isup>+x. RN_deriv \<nu> x * indicator A x)"
   1.448      unfolding eq[OF A, symmetric] RN_deriv(2)[OF \<nu> A, symmetric] ..
   1.449  qed
   1.450  
   1.451 @@ -1130,10 +1130,10 @@
   1.452      using f by (auto simp: bij_inv_def indicator_def)
   1.453    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.454      using `A \<in> sets M` by (force intro!: sf.RN_deriv(2)[OF \<nu>' ac])
   1.455 -  also have "\<dots> = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
   1.456 +  also have "\<dots> = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
   1.457      unfolding positive_integral_vimage_inv[OF f]
   1.458      by (simp add: * cong: positive_integral_cong)
   1.459 -  finally show "\<nu> A = positive_integral (\<lambda>x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
   1.460 +  finally show "\<nu> A = (\<integral>\<^isup>+x. sf.RN_deriv (\<lambda>A. \<nu> (f ` A)) (g x) * indicator A x)"
   1.461      unfolding A_f[OF `A \<in> sets M`] .
   1.462  qed
   1.463  
   1.464 @@ -1150,7 +1150,7 @@
   1.465  lemma (in sigma_finite_measure)
   1.466    assumes \<nu>: "sigma_finite_measure M \<nu>" "absolutely_continuous \<nu>"
   1.467      and f: "f \<in> borel_measurable M"
   1.468 -  shows RN_deriv_integral: "measure_space.integral M \<nu> f = integral (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
   1.469 +  shows RN_deriv_integral: "measure_space.integral M \<nu> f = (\<integral>x. real (RN_deriv \<nu> x) * f x)" (is ?integral)
   1.470      and RN_deriv_integrable: "measure_space.integrable M \<nu> f \<longleftrightarrow> integrable (\<lambda>x. real (RN_deriv \<nu> x) * f x)" (is ?integrable)
   1.471  proof -
   1.472    interpret \<nu>: sigma_finite_measure M \<nu> by fact
   1.473 @@ -1164,7 +1164,7 @@
   1.474        then have "RN_deriv \<nu> x * Real (f x) = Real (real (RN_deriv \<nu> x) * f x)"
   1.475          using * by (simp add: Real_real) }
   1.476      note * = this
   1.477 -    have "positive_integral (\<lambda>x. RN_deriv \<nu> x * Real (f x)) = positive_integral (\<lambda>x. Real (real (RN_deriv \<nu> x) * f x))"
   1.478 +    have "(\<integral>\<^isup>+x. RN_deriv \<nu> x * Real (f x)) = (\<integral>\<^isup>+x. Real (real (RN_deriv \<nu> x) * f x))"
   1.479        apply (rule positive_integral_cong_AE)
   1.480        apply (rule AE_mp[OF RN_deriv_finite[OF \<nu>]])
   1.481        by (auto intro!: AE_cong simp: *) }
   1.482 @@ -1182,7 +1182,7 @@
   1.483  proof -
   1.484    note deriv = RN_deriv[OF assms(1, 2)]
   1.485    from deriv(2)[OF `{x} \<in> sets M`]
   1.486 -  have "\<nu> {x} = positive_integral (\<lambda>w. RN_deriv \<nu> x * indicator {x} w)"
   1.487 +  have "\<nu> {x} = (\<integral>\<^isup>+w. RN_deriv \<nu> x * indicator {x} w)"
   1.488      by (auto simp: indicator_def intro!: positive_integral_cong)
   1.489    thus ?thesis using positive_integral_cmult_indicator[OF `{x} \<in> sets M`]
   1.490      by auto