changeset 46731 5302e932d1e5 parent 45777 c36637603821 child 47694 05663f75964c
```     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Feb 28 20:20:09 2012 +0100
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Feb 28 21:53:36 2012 +0100
1.3 @@ -17,7 +17,7 @@
1.4      measure: "\<And>i. \<mu> (A i) \<noteq> \<infinity>" and
1.5      disjoint: "disjoint_family A"
1.6      using disjoint_sigma_finite by auto
1.7 -  let "?B i" = "2^Suc i * \<mu> (A i)"
1.8 +  let ?B = "\<lambda>i. 2^Suc i * \<mu> (A i)"
1.9    have "\<forall>i. \<exists>x. 0 < x \<and> x < inverse (?B i)"
1.10    proof
1.11      fix i have Ai: "A i \<in> sets M" using range by auto
1.12 @@ -28,7 +28,7 @@
1.13    from choice[OF this] obtain n where n: "\<And>i. 0 < n i"
1.14      "\<And>i. n i < inverse (2^Suc i * \<mu> (A i))" by auto
1.15    { fix i have "0 \<le> n i" using n(1)[of i] by auto } note pos = this
1.16 -  let "?h x" = "\<Sum>i. n i * indicator (A i) x"
1.17 +  let ?h = "\<lambda>x. \<Sum>i. n i * indicator (A i) x"
1.18    show ?thesis
1.19    proof (safe intro!: bexI[of _ ?h] del: notI)
1.20      have "\<And>i. A i \<in> sets M"
1.21 @@ -132,8 +132,8 @@
1.22                      (\<forall>B\<in>sets M. B \<subseteq> A \<longrightarrow> - e < \<mu>' B - finite_measure.\<mu>' (M\<lparr>measure := \<nu>\<rparr>) B)"
1.23  proof -
1.24    interpret M': finite_measure "M\<lparr>measure := \<nu>\<rparr>" by fact
1.25 -  let "?d A" = "\<mu>' A - M'.\<mu>' A"
1.26 -  let "?A A" = "if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
1.27 +  let ?d = "\<lambda>A. \<mu>' A - M'.\<mu>' A"
1.28 +  let ?A = "\<lambda>A. if (\<forall>B\<in>sets M. B \<subseteq> space M - A \<longrightarrow> -e < ?d B)
1.29      then {}
1.30      else (SOME B. B \<in> sets M \<and> B \<subseteq> space M - A \<and> ?d B \<le> -e)"
1.31    def A \<equiv> "\<lambda>n. ((\<lambda>B. B \<union> ?A B) ^^ n) {}"
1.32 @@ -247,9 +247,9 @@
1.33  proof -
1.34    interpret M': finite_measure ?M' where
1.35      "space ?M' = space M" and "sets ?M' = sets M" and "measure ?M' = \<nu>" by fact auto
1.36 -  let "?d A" = "\<mu>' A - M'.\<mu>' A"
1.37 -  let "?P A B n" = "A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
1.38 -  let "?r S" = "restricted_space S"
1.39 +  let ?d = "\<lambda>A. \<mu>' A - M'.\<mu>' A"
1.40 +  let ?P = "\<lambda>A B n. A \<in> sets M \<and> A \<subseteq> B \<and> ?d B \<le> ?d A \<and> (\<forall>C\<in>sets M. C \<subseteq> A \<longrightarrow> - 1 / real (Suc n) < ?d C)"
1.41 +  let ?r = "\<lambda>S. restricted_space S"
1.42    { fix S n assume S: "S \<in> sets M"
1.43      note r = M'.restricted_finite_measure[of S] restricted_finite_measure[OF S] S
1.44      then have "finite_measure (?r S)" "0 < 1 / real (Suc n)"
1.45 @@ -342,7 +342,7 @@
1.46          (\<integral>\<^isup>+x. g x * indicator (?A \<inter> A) x \<partial>M) +
1.47          (\<integral>\<^isup>+x. f x * indicator ((space M - ?A) \<inter> A) x \<partial>M)"
1.48          using f g sets unfolding G_def
1.49 -        by (auto cong: positive_integral_cong intro!: positive_integral_add borel_measurable_indicator)
1.50 +        by (auto cong: positive_integral_cong intro!: positive_integral_add)
1.51        also have "\<dots> \<le> \<nu> (?A \<inter> A) + \<nu> ((space M - ?A) \<inter> A)"
1.52          using f g sets unfolding G_def by (auto intro!: add_mono)
1.53        also have "\<dots> = \<nu> A"
1.54 @@ -388,9 +388,9 @@
1.55    qed
1.56    from choice[OF this] obtain gs where "\<And>i. gs i \<in> G" "\<And>n. integral\<^isup>P M (gs n) = ys n" by auto
1.57    hence y_eq: "?y = (SUP i. integral\<^isup>P M (gs i))" using ys by auto
1.58 -  let "?g i x" = "Max ((\<lambda>n. gs n x) ` {..i})"
1.59 +  let ?g = "\<lambda>i x. Max ((\<lambda>n. gs n x) ` {..i})"
1.60    def f \<equiv> "\<lambda>x. SUP i. ?g i x"
1.61 -  let "?F A x" = "f x * indicator A x"
1.62 +  let ?F = "\<lambda>A x. f x * indicator A x"
1.63    have gs_not_empty: "\<And>i x. (\<lambda>n. gs n x) ` {..i} \<noteq> {}" by auto
1.64    { fix i have "?g i \<in> G"
1.65      proof (induct i)
1.66 @@ -420,7 +420,7 @@
1.67    have "\<And>x. 0 \<le> f x"
1.68      unfolding f_def using `\<And>i. gs i \<in> G`
1.69      by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
1.70 -  let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
1.71 +  let ?t = "\<lambda>A. \<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
1.72    let ?M = "M\<lparr> measure := ?t\<rparr>"
1.73    interpret M: sigma_algebra ?M
1.74      by (intro sigma_algebra_cong) auto
1.75 @@ -522,7 +522,7 @@
1.76          using M'.finite_measure b finite_measure M.positive_measure[OF B(1)]
1.77          by (cases rule: ereal2_cases[of "?t B" "b * \<mu> B"]) auto }
1.78      note bM_le_t = this
1.79 -    let "?f0 x" = "f x + b * indicator A0 x"
1.80 +    let ?f0 = "\<lambda>x. f x + b * indicator A0 x"
1.81      { fix A assume A: "A \<in> sets M"
1.82        hence "A \<inter> A0 \<in> sets M" using `A0 \<in> sets M` by auto
1.83        have "(\<integral>\<^isup>+x. ?f0 x  * indicator A x \<partial>M) =
1.84 @@ -550,8 +550,7 @@
1.85          by (cases "\<integral>\<^isup>+x. ?F A x \<partial>M", cases "\<nu> A") auto
1.86        finally have "(\<integral>\<^isup>+x. ?f0 x * indicator A x \<partial>M) \<le> \<nu> A" . }
1.87      hence "?f0 \<in> G" using `A0 \<in> sets M` b `f \<in> G` unfolding G_def
1.88 -      by (auto intro!: borel_measurable_indicator borel_measurable_ereal_add
1.90 +      by (auto intro!: ereal_add_nonneg_nonneg)
1.91      have real: "?t (space M) \<noteq> \<infinity>" "?t A0 \<noteq> \<infinity>"
1.92        "b * \<mu> (space M) \<noteq> \<infinity>" "b * \<mu> A0 \<noteq> \<infinity>"
1.93        using `A0 \<in> sets M` b
1.94 @@ -633,7 +632,7 @@
1.95    have "{} \<in> ?Q" using v.empty_measure by auto
1.96    then have Q_not_empty: "?Q \<noteq> {}" by blast
1.97    have "?a \<le> \<mu> (space M)" using sets_into_space
1.98 -    by (auto intro!: SUP_least measure_mono top)
1.99 +    by (auto intro!: SUP_least measure_mono)
1.100    then have "?a \<noteq> \<infinity>" using finite_measure_of_space
1.101      by auto
1.102    from SUPR_countable_SUPR[OF Q_not_empty, of \<mu>]
1.103 @@ -643,7 +642,7 @@
1.104    from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = \<mu> (Q' i)" "\<And>i. Q' i \<in> ?Q"
1.105      by auto
1.106    then have a_Lim: "?a = (SUP i::nat. \<mu> (Q' i))" using a by simp
1.107 -  let "?O n" = "\<Union>i\<le>n. Q' i"
1.108 +  let ?O = "\<lambda>n. \<Union>i\<le>n. Q' i"
1.109    have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
1.110    proof (rule continuity_from_below[of ?O])
1.111      show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
1.112 @@ -675,7 +674,7 @@
1.113          using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
1.114      qed
1.115    qed
1.116 -  let "?O_0" = "(\<Union>i. ?O i)"
1.117 +  let ?O_0 = "(\<Union>i. ?O i)"
1.118    have "?O_0 \<in> sets M" using Q' by auto
1.119    def Q \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> Q' 0 | Suc n \<Rightarrow> ?O (Suc n) - ?O n"
1.120    { fix i have "Q i \<in> sets M" unfolding Q_def using Q'[of 0] by (cases i) (auto intro: O_sets) }
1.121 @@ -710,10 +709,9 @@
1.122              fix i have "?O i \<union> A \<in> ?Q"
1.123              proof (safe del: notI)
1.124                show "?O i \<union> A \<in> sets M" using O_sets A by auto
1.125 -              from O_in_G[of i]
1.126 -              moreover have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
1.127 +              from O_in_G[of i] have "\<nu> (?O i \<union> A) \<le> \<nu> (?O i) + \<nu> A"
1.128                  using v.measure_subadditive[of "?O i" A] A O_sets by auto
1.129 -              ultimately show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
1.130 +              with O_in_G[of i] show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
1.131                  using `\<nu> A \<noteq> \<infinity>` by auto
1.132              qed
1.133              then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule SUP_upper)
1.134 @@ -800,7 +798,7 @@
1.135      and f: "\<And>A i. A \<in> sets M \<Longrightarrow>
1.136        \<nu> (Q i \<inter> A) = (\<integral>\<^isup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M)"
1.137      by auto
1.138 -  let "?f x" = "(\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x"
1.139 +  let ?f = "\<lambda>x. (\<Sum>i. f i x * indicator (Q i) x) + \<infinity> * indicator Q0 x"
1.140    show ?thesis
1.141    proof (safe intro!: bexI[of _ ?f])
1.142      show "?f \<in> borel_measurable M" using Q0 borel Q_sets
1.143 @@ -850,7 +848,7 @@
1.144      nn: "\<And>x. 0 \<le> h x" and
1.145      pos: "\<And>x. x \<in> space M \<Longrightarrow> 0 < h x" and
1.146      "\<And>x. x \<in> space M \<Longrightarrow> h x < \<infinity>" by auto
1.147 -  let "?T A" = "(\<integral>\<^isup>+x. h x * indicator A x \<partial>M)"
1.148 +  let ?T = "\<lambda>A. (\<integral>\<^isup>+x. h x * indicator A x \<partial>M)"
1.149    let ?MT = "M\<lparr> measure := ?T \<rparr>"
1.150    interpret T: finite_measure ?MT
1.151      where "space ?MT = space M" and "sets ?MT = sets M" and "measure ?MT = ?T"
1.152 @@ -872,7 +870,7 @@
1.153    show ?thesis
1.154    proof (safe intro!: bexI[of _ "\<lambda>x. h x * f x"])
1.155      show "(\<lambda>x. h x * f x) \<in> borel_measurable M"
1.156 -      using borel f_borel by (auto intro: borel_measurable_ereal_times)
1.157 +      using borel f_borel by auto
1.158      show "\<And>x. 0 \<le> h x * f x" using nn f_borel by auto
1.159      fix A assume "A \<in> sets M"
1.160      then show "\<nu> A = (\<integral>\<^isup>+x. h x * f x * indicator A x \<partial>M)"
1.161 @@ -933,8 +931,8 @@
1.162      (is "\<And>A. A \<in> sets M \<Longrightarrow> ?P f A = ?P f' A")
1.163    shows "AE x. f x = f' x"
1.164  proof -
1.165 -  let "?\<nu> A" = "?P f A" and "?\<nu>' A" = "?P f' A"
1.166 -  let "?f A x" = "f x * indicator A x" and "?f' A x" = "f' x * indicator A x"
1.167 +  let ?\<nu> = "\<lambda>A. ?P f A" and ?\<nu>' = "\<lambda>A. ?P f' A"
1.168 +  let ?f = "\<lambda>A x. f x * indicator A x" and ?f' = "\<lambda>A x. f' x * indicator A x"
1.169    interpret M: measure_space "M\<lparr> measure := ?\<nu>\<rparr>"
1.170      using borel(1) pos(1) by (rule measure_space_density) simp
1.171    have ac: "absolutely_continuous ?\<nu>"
1.172 @@ -957,7 +955,7 @@
1.173    proof (rule AE_I')
1.174      { fix f :: "'a \<Rightarrow> ereal" assume borel: "f \<in> borel_measurable M"
1.175          and eq: "\<And>A. A \<in> sets M \<Longrightarrow> ?\<nu> A = (\<integral>\<^isup>+x. f x * indicator A x \<partial>M)"
1.176 -      let "?A i" = "Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
1.177 +      let ?A = "\<lambda>i. Q0 \<inter> {x \<in> space M. f x < (i::nat)}"
1.178        have "(\<Union>i. ?A i) \<in> null_sets"
1.179        proof (rule null_sets_UN)
1.180          fix i ::nat have "?A i \<in> sets M"
1.181 @@ -1079,7 +1077,7 @@
1.182      apply (rule_tac Int)
1.183      by (cases i) (auto intro: measurable_sets[OF f(1)]) }
1.184    note A_in_sets = this
1.185 -  let "?A n" = "case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
1.186 +  let ?A = "\<lambda>n. case prod_decode n of (i,j) \<Rightarrow> A i \<inter> Q j"
1.187    show "sigma_finite_measure ?N"
1.188    proof (default, intro exI conjI subsetI allI)
1.189      fix x assume "x \<in> range ?A"
```