src/HOL/Probability/Radon_Nikodym.thy
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.89 -                       borel_measurable_ereal_times ereal_add_nonneg_nonneg)
    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"