diff -r f17602cbf76a -r 1d066f6ab25d src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Thu Apr 14 12:17:44 2016 +0200
+++ b/src/HOL/Probability/Levy.thy	Thu Apr 14 15:48:11 2016 +0200
@@ -25,17 +25,17 @@
   have 1: "cmod (?F t - (b - a)) \<le> a^2 / 2 * abs t + b^2 / 2 * abs t" if "t \<noteq> 0" for t
   proof -
     have "cmod (?F t - (b - a)) = cmod (
-        (iexp (-(t * a)) - (1 + ii * -(t * a))) / (ii * t) - 
-        (iexp (-(t * b)) - (1 + ii * -(t * b))) / (ii * t))"  
+        (iexp (-(t * a)) - (1 + ii * -(t * a))) / (ii * t) -
+        (iexp (-(t * b)) - (1 + ii * -(t * b))) / (ii * t))"
            (is "_ = cmod (?one / (ii * t) - ?two / (ii * t))")
       using `t \<noteq> 0` by (intro arg_cong[where f=norm]) (simp add: field_simps)
-    also have "\<dots> \<le> cmod (?one / (ii * t)) + cmod (?two / (ii * t))" 
+    also have "\<dots> \<le> cmod (?one / (ii * t)) + cmod (?two / (ii * t))"
       by (rule norm_triangle_ineq4)
     also have "cmod (?one / (ii * t)) = cmod ?one / abs t"
       by (simp add: norm_divide norm_mult)
     also have "cmod (?two / (ii * t)) = cmod ?two / abs t"
-      by (simp add: norm_divide norm_mult)      
-    also have "cmod ?one / abs t + cmod ?two / abs t \<le> 
+      by (simp add: norm_divide norm_mult)
+    also have "cmod ?one / abs t + cmod ?two / abs t \<le>
         ((- (a * t))^2 / 2) / abs t + ((- (b * t))^2 / 2) / abs t"
       apply (rule add_mono)
       apply (rule divide_right_mono)
@@ -71,7 +71,7 @@
     using iexp_approx1 [of "t * (b - a)" 0]
     by (intro divide_right_mono) (auto simp add: field_simps eval_nat_numeral)
   also have "\<dots> = b - a"
-    using assms by (auto simp add: abs_mult) 
+    using assms by (auto simp add: abs_mult)
   finally show ?thesis .
 qed
 
@@ -109,7 +109,7 @@
       also have "\<dots> + ?t = (CLBINT t=(0::real)..T. ?f (-t) x + ?f t x)"
         using 1
         by (intro interval_lebesgue_integral_add(2) [symmetric] interval_integrable_mirror[THEN iffD2]) simp_all
-      also have "\<dots> = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) -  
+      also have "\<dots> = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) -
           (iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (ii * t))"
         using `T \<ge> 0` by (intro interval_integral_cong) (auto simp add: divide_simps)
       also have "\<dots> = (CLBINT t=(0::real)..T. complex_of_real(
@@ -120,7 +120,7 @@
         unfolding minus_diff_eq[symmetric, of "y * x" "y * a" for y a] sin_minus cos_minus
         apply (simp add: field_simps power2_eq_square)
         done
-      also have "\<dots> = complex_of_real (LBINT t=(0::real)..T. 
+      also have "\<dots> = complex_of_real (LBINT t=(0::real)..T.
           2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t))"
         by (rule interval_lebesgue_integral_of_real)
       also have "\<dots> = complex_of_real (2 * (sgn (x - a) * Si (T * abs (x - a)) -
@@ -133,7 +133,7 @@
       finally have "(CLBINT t. ?f' (t, x)) =
           2 * (sgn (x - a) * Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))" .
     } note main_eq = this
-    have "(CLBINT t=-T..T. ?F t * \<phi> t) = 
+    have "(CLBINT t=-T..T. ?F t * \<phi> t) =
       (CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))"
       using `T \<ge> 0` unfolding \<phi>_def char_def interval_lebesgue_integral_def
       by (auto split: split_indicator intro!: integral_cong)
@@ -142,24 +142,26 @@
     also have "\<dots> = (CLINT x | M. (CLBINT t. ?f' (t, x)))"
     proof (intro P.Fubini_integral [symmetric] integrableI_bounded_set [where B="b - a"])
       show "emeasure (lborel \<Otimes>\<^sub>M M) ({- T<..<T} \<times> space M) < \<infinity>"
-        using \<open>T \<ge> 0\<close> by (subst emeasure_pair_measure_Times) auto
+        using \<open>T \<ge> 0\<close>
+        by (subst emeasure_pair_measure_Times)
+           (auto simp: ennreal_mult_less_top not_less top_unique)
       show "AE x\<in>{- T<..<T} \<times> space M in lborel \<Otimes>\<^sub>M M. cmod (case x of (t, x) \<Rightarrow> ?f' (t, x)) \<le> b - a"
         using Levy_Inversion_aux2[of "x - b" "x - a" for x] `a \<le> b`
         by (intro AE_I [of _ _ "{0} \<times> UNIV"]) (force simp: emeasure_pair_measure_Times)+
     qed (auto split: split_indicator split_indicator_asm)
-    also have "\<dots> = (CLINT x | M. (complex_of_real (2 * (sgn (x - a) * 
+    also have "\<dots> = (CLINT x | M. (complex_of_real (2 * (sgn (x - a) *
          Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))))"
        using main_eq by (intro integral_cong, auto)
-    also have "\<dots> = complex_of_real (LINT x | M. (2 * (sgn (x - a) * 
+    also have "\<dots> = complex_of_real (LINT x | M. (2 * (sgn (x - a) *
          Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))"
        by (rule integral_complex_of_real)
-    finally have "(CLBINT t=-T..T. ?F t * \<phi> t) = 
-        complex_of_real (LINT x | M. (2 * (sgn (x - a) * 
+    finally have "(CLBINT t=-T..T. ?F t * \<phi> t) =
+        complex_of_real (LINT x | M. (2 * (sgn (x - a) *
          Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))" .
   } note main_eq2 = this
 
-  have "(\<lambda>T :: nat. LINT x | M. (2 * (sgn (x - a) * 
-         Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow> 
+  have "(\<lambda>T :: nat. LINT x | M. (2 * (sgn (x - a) *
+         Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow>
        (LINT x | M. 2 * pi * indicator {a<..b} x)"
   proof (rule integral_dominated_convergence [where w="\<lambda>x. 4 * B"])
     show "integrable M (\<lambda>x. 4 * B)"
@@ -191,11 +193,11 @@
         using x `a \<le> b` by (auto split: split_indicator)
       finally show "(\<lambda>n. 2 * ?S n x) \<longlonglongrightarrow> 2 * pi * indicator {a<..b} x" .
     qed
-  qed simp_all 
+  qed simp_all
   also have "(LINT x | M. 2 * pi * indicator {a<..b} x) = 2 * pi * \<mu> {a<..b}"
     by (simp add: \<mu>_def)
-  finally have "(\<lambda>T. LINT x | M. (2 * (sgn (x - a) * 
-         Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow> 
+  finally have "(\<lambda>T. LINT x | M. (2 * (sgn (x - a) *
+         Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow>
        2 * pi * \<mu> {a<..b}" .
   with main_eq2 show ?thesis
     by (auto intro!: tendsto_eq_intros)
@@ -233,7 +235,7 @@
         "measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \<le> x" "\<bar>cdf M1 a\<bar> < \<epsilon> / 4" "\<bar>cdf M2 a\<bar> < \<epsilon> / 4"
         by auto
 
-      from `\<epsilon> > 0` `(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)` `(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)` 
+      from `\<epsilon> > 0` `(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)` `(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)`
       have "eventually (\<lambda>y. \<bar>cdf M1 y - cdf M1 x\<bar> < \<epsilon> / 4 \<and> \<bar>cdf M2 y - cdf M2 x\<bar> < \<epsilon> / 4 \<and> x < y) (at_right x)"
         by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less)
       then obtain N where "N > x" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>cdf M1 y - cdf M1 x\<bar> < \<epsilon> / 4"
@@ -269,9 +271,9 @@
         by (intro add_mono less_imp_le \<open>\<bar>cdf M2 x - cdf M2 b\<bar> < \<epsilon> / 4\<close> \<open>\<bar>cdf M2 a\<bar> < \<epsilon> / 4\<close>)
       finally have 2: "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) \<le> \<epsilon> / 2" by simp
 
-      have "abs (cdf M1 x - cdf M2 x) = abs ((cdf M1 x - (cdf M1 b - cdf M1 a)) - 
+      have "abs (cdf M1 x - cdf M2 x) = abs ((cdf M1 x - (cdf M1 b - cdf M1 a)) -
           (cdf M2 x - (cdf M2 b - cdf M2 a)))" by (subst *, simp)
-      also have "\<dots> \<le> abs (cdf M1 x - (cdf M1 b - cdf M1 a)) + 
+      also have "\<dots> \<le> abs (cdf M1 x - (cdf M1 b - cdf M1 a)) +
           abs (cdf M2 x - (cdf M2 b - cdf M2 a))" by (rule abs_triangle_ineq4)
       also have "\<dots> \<le> \<epsilon> / 2 + \<epsilon> / 2" by (rule add_mono [OF 1 2])
       finally have "abs (cdf M1 x - cdf M2 x) \<le> \<epsilon>" by simp }
@@ -295,13 +297,13 @@
   fixes M :: "nat \<Rightarrow> real measure" and M' :: "real measure"
   assumes real_distr_M : "\<And>n. real_distribution (M n)"
     and real_distr_M': "real_distribution M'"
-    and char_conv: "\<And>t. (\<lambda>n. char (M n) t) \<longlonglongrightarrow> char M' t" 
+    and char_conv: "\<And>t. (\<lambda>n. char (M n) t) \<longlonglongrightarrow> char M' t"
   shows "weak_conv_m M M'"
 proof -
   interpret Mn: real_distribution "M n" for n by fact
   interpret M': real_distribution M' by fact
 
-  have *: "\<And>u x. u > 0 \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (CLBINT t:{-u..u}. 1 - iexp (t * x)) = 
+  have *: "\<And>u x. u > 0 \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (CLBINT t:{-u..u}. 1 - iexp (t * x)) =
       2 * (u  - sin (u * x) / x)"
   proof -
     fix u :: real and x :: real
@@ -331,7 +333,7 @@
     finally show "(CLBINT t:{-u..u}. 1 - iexp (t * x)) = 2 * (u  - sin (u * x) / x)"
       by (simp add: field_simps)
   qed
-  have main_bound: "\<And>u n. u > 0 \<Longrightarrow> Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge> 
+  have main_bound: "\<And>u n. u > 0 \<Longrightarrow> Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge>
     u * measure (M n) {x. abs x \<ge> 2 / u}"
   proof -
     fix u :: real and n
@@ -345,9 +347,10 @@
     have Mn3: "set_integrable (M n \<Otimes>\<^sub>M lborel) (UNIV \<times> {- u..u}) (\<lambda>a. 1 - exp (\<i> * complex_of_real (snd a * fst a)))"
       using `0 < u`
       by (intro integrableI_bounded_set_indicator [where B="2"])
-         (auto simp: lborel.emeasure_pair_measure_Times split: split_indicator
+         (auto simp: lborel.emeasure_pair_measure_Times ennreal_mult_less_top not_less top_unique
+               split: split_indicator
                intro!: order_trans [OF norm_triangle_ineq4])
-    have "(CLBINT t:{-u..u}. 1 - char (M n) t) = 
+    have "(CLBINT t:{-u..u}. 1 - char (M n) t) =
         (CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))"
       unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult)
     also have "\<dots> = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))"
@@ -358,7 +361,7 @@
       using `u > 0` by (intro integral_cong, auto simp add: * simp del: of_real_mult)
     also have "\<dots> = (LINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
       by (rule integral_complex_of_real)
-    finally have "Re (CLBINT t:{-u..u}. 1 - char (M n) t) = 
+    finally have "Re (CLBINT t:{-u..u}. 1 - char (M n) t) =
        (LINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))" by simp
     also have "\<dots> \<ge> (LINT x : {x. abs x \<ge> 2 / u} | M n. u)"
     proof -
@@ -377,9 +380,10 @@
       ultimately show ?thesis
         using `u > 0`
         by (intro integral_mono [OF _ **])
-           (auto simp: divide_simps sin_x_le_x mult.commute[of u] mult_neg_pos split: split_indicator)
+           (auto simp: divide_simps sin_x_le_x mult.commute[of u] mult_neg_pos top_unique less_top[symmetric]
+                 split: split_indicator)
     qed
-    also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) = 
+    also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) =
         u * measure (M n) {x. abs x \<ge> 2 / u}"
       by (simp add: Mn.emeasure_eq_measure)
     finally show "Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge> u * measure (M n) {x. abs x \<ge> 2 / u}" .
@@ -423,7 +427,7 @@
     have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
       using bd1
       apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"])
-      apply (auto intro!: char_conv tendsto_intros 
+      apply (auto intro!: char_conv tendsto_intros
                   simp: emeasure_lborel_Icc_eq
                   split: split_indicator)
       done
@@ -438,20 +442,20 @@
         (CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by auto
     { fix n
       assume "n \<ge> N"
-      have "cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) = 
+      have "cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) =
         cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - (CLBINT t:{-d/2..d/2}. 1 - char M' t)
           + (CLBINT t:{-d/2..d/2}. 1 - char M' t))" by simp
-      also have "\<dots> \<le> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - 
+      also have "\<dots> \<le> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
           (CLBINT t:{-d/2..d/2}. 1 - char M' t)) + cmod(CLBINT t:{-d/2..d/2}. 1 - char M' t)"
         by (rule norm_triangle_ineq)
-      also have "\<dots> < d * \<epsilon> / 4 + d * \<epsilon> / 4" 
+      also have "\<dots> < d * \<epsilon> / 4 + d * \<epsilon> / 4"
         by (rule add_less_le_mono [OF N [OF `n \<ge> N`] bound])
       also have "\<dots> = d * \<epsilon> / 2" by auto
       finally have "cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) < d * \<epsilon> / 2" .
       hence "d * \<epsilon> / 2 > Re (CLBINT t:{-d/2..d/2}. 1 - char (M n) t)"
         by (rule order_le_less_trans [OF complex_Re_le_cmod])
       hence "d * \<epsilon> / 2 > Re (CLBINT t:{-(d/2)..d/2}. 1 - char (M n) t)" (is "_ > ?lhs") by simp
-      also have "?lhs \<ge> (d / 2) * measure (M n) {x. abs x \<ge> 2 / (d / 2)}" 
+      also have "?lhs \<ge> (d / 2) * measure (M n) {x. abs x \<ge> 2 / (d / 2)}"
         using d0 by (intro main_bound, simp)
       finally (xtrans) have "d * \<epsilon> / 2 > (d / 2) * measure (M n) {x. abs x \<ge> 2 / (d / 2)}" .
       with d0 `\<epsilon> > 0` have "\<epsilon> > measure (M n) {x. abs x \<ge> 2 / (d / 2)}" by (simp add: field_simps)
@@ -473,7 +477,7 @@
     { fix n :: nat
       have *: "(UN (k :: nat). {- real k<..real k}) = UNIV"
         by (auto, metis leI le_less_trans less_imp_le minus_less_iff reals_Archimedean2)
-      have "(\<lambda>k. measure (M n) {- real k<..real k}) \<longlonglongrightarrow> 
+      have "(\<lambda>k. measure (M n) {- real k<..real k}) \<longlonglongrightarrow>
           measure (M n) (UN (k :: nat). {- real k<..real k})"
         by (rule Mn.finite_Lim_measure_incseq, auto simp add: incseq_def)
       hence "(\<lambda>k. measure (M n) {- real k<..real k}) \<longlonglongrightarrow> 1"
@@ -490,11 +494,11 @@
           by eventually_elim (auto simp add: less_Suc_eq)
       qed simp
     } note 8 = this
-    from 8 [of N] have "\<exists>K :: nat. \<forall>k \<ge> K. \<forall>m<N. 1 - \<epsilon> < 
+    from 8 [of N] have "\<exists>K :: nat. \<forall>k \<ge> K. \<forall>m<N. 1 - \<epsilon> <
         Sigma_Algebra.measure (M m) {- real k<..real k}"
       by (auto simp add: eventually_sequentially)
     hence "\<exists>K :: nat. \<forall>m<N. 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}" by auto
-    then obtain K :: nat where 
+    then obtain K :: nat where
       "\<forall>m<N. 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}" ..
     hence K: "\<And>m. m < N \<Longrightarrow> 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}"
       by auto
@@ -504,7 +508,7 @@
       apply (rule max.strict_coboundedI2, auto)
     proof -
       fix n
-      show " 1 - \<epsilon> < measure (M n) {- max (real K) (4 / d)<..max (real K) (4 / d)}"      
+      show " 1 - \<epsilon> < measure (M n) {- max (real K) (4 / d)<..max (real K) (4 / d)}"
         apply (case_tac "n < N")
         apply (rule order_less_le_trans)
         apply (erule K)
@@ -512,7 +516,7 @@
         apply (rule order_less_le_trans)
         apply (rule 6, erule leI)
         by (rule Mn.finite_measure_mono, auto)
-    qed 
+    qed
     thus "\<exists>a b. a < b \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {a<..b})" by (intro exI)
   qed
   have tight: "tight M"
@@ -530,8 +534,8 @@
       by (subst 4, rule LIMSEQ_subseq_LIMSEQ [OF _ s], rule assms)
     hence "char \<nu> = char M'" by (intro ext, intro LIMSEQ_unique [OF 3 5])
     hence "\<nu> = M'" by (rule Levy_uniqueness [OF * `real_distribution M'`])
-    thus "weak_conv_m (M \<circ> s) M'" 
-      by (elim subst) (rule nu)  
+    thus "weak_conv_m (M \<circ> s) M'"
+      by (elim subst) (rule nu)
   qed
 qed