# HG changeset patch
# User hoelzl
# Date 1467743398 -7200
# Node ID c22928719e198a58fd796f6b0aee6262119d9ed4
# Parent  786074d8d61bd13eedaedad7b0c782a1641cafc2
Probability: simplified Levy's uniqueness theorem

diff -r 786074d8d61b -r c22928719e19 src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Tue Jul 05 18:00:21 2016 +0200
+++ b/src/HOL/Probability/Levy.thy	Tue Jul 05 20:29:58 2016 +0200
@@ -219,64 +219,46 @@
   have "cdf M1 = cdf M2"
   proof (rule ext)
     fix x
-    from M1.cdf_is_right_cont [of x] have "(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)"
-      by (simp add: continuous_within)
-    from M2.cdf_is_right_cont [of x] have "(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)"
-      by (simp add: continuous_within)
+    let ?D = "\<lambda>x. \<bar>cdf M1 x - cdf M2 x\<bar>"
 
     { fix \<epsilon> :: real
       assume "\<epsilon> > 0"
-      from \<open>\<epsilon> > 0\<close> \<open>(cdf M1 \<longlongrightarrow> 0) at_bot\<close> \<open>(cdf M2 \<longlongrightarrow> 0) at_bot\<close>
-      have "eventually (\<lambda>y. \<bar>cdf M1 y\<bar> < \<epsilon> / 4 \<and> \<bar>cdf M2 y\<bar> < \<epsilon> / 4 \<and> y \<le> x) at_bot"
-        by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot)
-      then obtain M where "\<And>y. y \<le> M \<Longrightarrow> \<bar>cdf M1 y\<bar> < \<epsilon> / 4" "\<And>y. y \<le> M \<Longrightarrow> \<bar>cdf M2 y\<bar> < \<epsilon> / 4" "M \<le> x"
+      have "(?D \<longlongrightarrow> 0) at_bot"
+        using \<open>(cdf M1 \<longlongrightarrow> 0) at_bot\<close> \<open>(cdf M2 \<longlongrightarrow> 0) at_bot\<close> by (intro tendsto_eq_intros) auto
+      then have "eventually (\<lambda>y. ?D y < \<epsilon> / 2 \<and> y \<le> x) at_bot"
+        using \<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot abs_idempotent)
+      then obtain M where "\<And>y. y \<le> M \<Longrightarrow> ?D y < \<epsilon> / 2" "M \<le> x"
         unfolding eventually_at_bot_linorder by auto
       with open_minus_countable[OF count, of "{..< M}"] obtain a where
-        "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"
+        "measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \<le> x" and 1: "?D a < \<epsilon> / 2"
         by auto
 
-      from \<open>\<epsilon> > 0\<close> \<open>(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)\<close> \<open>(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)\<close>
-      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"
-        "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>cdf M2 y - cdf M2 x\<bar> < \<epsilon> / 4" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> x < y"
+      have "(?D \<longlongrightarrow> ?D x) (at_right x)"
+        using M1.cdf_is_right_cont [of x] M2.cdf_is_right_cont [of x]
+        by (intro tendsto_intros) (auto simp add: continuous_within)
+      then have "eventually (\<lambda>y. \<bar>?D y - ?D x\<bar> < \<epsilon> / 2) (at_right x)"
+        using \<open>\<epsilon> > 0\<close> 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>?D y - ?D x\<bar> < \<epsilon> / 2"
         by (auto simp add: eventually_at_right[OF less_add_one])
       with open_minus_countable[OF count, of "{x <..< N}"] obtain b where "x < b" "b < N"
-          "measure M1 {b} = 0" "measure M2 {b} = 0" "\<bar>cdf M2 x - cdf M2 b\<bar> < \<epsilon> / 4" "\<bar>cdf M1 x - cdf M1 b\<bar> < \<epsilon> / 4"
+          "measure M1 {b} = 0" "measure M2 {b} = 0" and 2: "\<bar>?D b - ?D x\<bar> < \<epsilon> / 2"
         by (auto simp: abs_minus_commute)
       from \<open>a \<le> x\<close> \<open>x < b\<close> have "a < b" "a \<le> b" by auto
 
       from \<open>char M1 = char M2\<close>
-        M1.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M1 {a} = 0\<close>  \<open>measure M1 {b} = 0\<close>]
+        M1.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M1 {a} = 0\<close> \<open>measure M1 {b} = 0\<close>]
         M2.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M2 {a} = 0\<close> \<open>measure M2 {b} = 0\<close>]
       have "complex_of_real (measure M1 {a<..b}) = complex_of_real (measure M2 {a<..b})"
         by (intro LIMSEQ_unique) auto
-      then have "measure M1 {a<..b} = measure M2 {a<..b}" by auto
-      then have *: "cdf M1 b - cdf M1 a = cdf M2 b - cdf M2 a"
-        unfolding M1.cdf_diff_eq [OF \<open>a < b\<close>] M2.cdf_diff_eq [OF \<open>a < b\<close>] .
-
-      have "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) = abs (cdf M1 x - cdf M1 b + cdf M1 a)"
+      then have "?D a = ?D b"
+        unfolding of_real_eq_iff M1.cdf_diff_eq [OF \<open>a < b\<close>, symmetric] M2.cdf_diff_eq [OF \<open>a < b\<close>, symmetric] by simp
+      then have "?D x = \<bar>(?D b - ?D x) - ?D a\<bar>"
         by simp
-      also have "\<dots> \<le> abs (cdf M1 x - cdf M1 b) + abs (cdf M1 a)"
-        by (rule abs_triangle_ineq)
-      also have "\<dots> \<le> \<epsilon> / 4 + \<epsilon> / 4"
-        by (intro add_mono less_imp_le \<open>\<bar>cdf M1 a\<bar> < \<epsilon> / 4\<close> \<open>\<bar>cdf M1 x - cdf M1 b\<bar> < \<epsilon> / 4\<close>)
-      finally have 1: "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) \<le> \<epsilon> / 2" by simp
-
-      have "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) = abs (cdf M2 x - cdf M2 b + cdf M2 a)"
-        by simp
-      also have "\<dots> \<le> abs (cdf M2 x - cdf M2 b) + abs (cdf M2 a)"
-        by (rule abs_triangle_ineq)
-      also have "\<dots> \<le> \<epsilon> / 4 + \<epsilon> / 4"
-        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)) -
-          (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)) +
-          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 }
+      also have "\<dots> \<le> \<bar>?D b - ?D x\<bar> + \<bar>?D a\<bar>"
+        by (rule abs_triangle_ineq4)
+      also have "\<dots> \<le> \<epsilon> / 2 + \<epsilon> / 2"
+        using 1 2 by (intro add_mono) auto
+      finally have "?D x \<le> \<epsilon>" by simp }
     then show "cdf M1 x = cdf M2 x"
       by (metis abs_le_zero_iff dense_ge eq_iff_diff_eq_0)
   qed