author hoelzl Tue, 05 Jul 2016 20:29:58 +0200 changeset 63393 c22928719e19 parent 63392 786074d8d61b child 63397 a528d24826c5
Probability: simplified Levy's uniqueness theorem
```--- 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)"
-    from M2.cdf_is_right_cont [of x] have "(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)"
+    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"
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```