# HG changeset patch
# User hoelzl
# Date 1452079133 -3600
# Node ID 7582b39f51ed7999db08cff12b4971889ee3b2dc
# Parent  614ef6d7a6b635c1573e7041ec42619be9bc481f
add the proof of the central limit theorem

diff -r 614ef6d7a6b6 -r 7582b39f51ed CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Jan 06 13:04:31 2016 +0100
+++ b/CONTRIBUTORS	Wed Jan 06 12:18:53 2016 +0100
@@ -6,6 +6,10 @@
 Contributions to Isabelle2016
 -----------------------------
 
+* Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM
+  Proof of the central limit theorem: includes weak convergence, characteristic
+  functions, and Levy's uniqueness and continuity theorem.
+
 * Winter 2015: Manuel Eberl, TUM
   The radius of convergence of power series and various summability tests.
   Harmonic numbers and the Euler-Mascheroni constant.
diff -r 614ef6d7a6b6 -r 7582b39f51ed NEWS
--- a/NEWS	Wed Jan 06 13:04:31 2016 +0100
+++ b/NEWS	Wed Jan 06 12:18:53 2016 +0100
@@ -660,6 +660,9 @@
 Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
 properties.
 
+* Probability: The central limit theorem based on Levy's uniqueness and
+continuity theorems, weak convergence, and characterisitc functions.
+
 * Data_Structures: new and growing session of standard data structures.
 
 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -159,4 +159,21 @@
   thus ?thesis by auto
 qed
 
+lemma open_minus_countable:
+  fixes S A :: "real set" assumes "countable A" "S \<noteq> {}" "open S"
+  shows "\<exists>x\<in>S. x \<notin> A"
+proof -
+  obtain x where "x \<in> S"
+    using \<open>S \<noteq> {}\<close> by auto
+  then obtain e where "0 < e" "{y. dist y x < e} \<subseteq> S"
+    using \<open>open S\<close> by (auto simp: open_dist subset_eq)
+  moreover have "{y. dist y x < e} = {x - e <..< x + e}"
+    by (auto simp: dist_real_def)
+  ultimately have "uncountable (S - A)"
+    using uncountable_open_interval[of "x - e" "x + e"] \<open>countable A\<close>
+    by (intro uncountable_minus_countable) (auto dest: countable_subset)
+  then show ?thesis
+    unfolding uncountable_def by auto
+qed
+
 end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -1882,6 +1882,18 @@
     by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
 
+lemma ereal_Inf':
+  assumes *: "bdd_below A" "A \<noteq> {}"
+  shows "ereal (Inf A) = (INF a:A. ereal a)"
+proof (rule ereal_Inf)
+  from * obtain l u where "\<And>x. x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A"
+    by (auto simp: bdd_below_def)
+  then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u"
+    by (auto intro!: INF_greatest INF_lower)
+  then show "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
+    by auto
+qed
+
 lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
   using ereal_Inf[of "f`A"] by auto
 
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -1851,6 +1851,16 @@
     "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
   by (meson closed_in_limpt closed_subset closedin_closed_trans)
 
+lemma bdd_below_closure:
+  fixes A :: "real set"
+  assumes "bdd_below A"
+  shows "bdd_below (closure A)"
+proof -
+  from assms obtain m where "\<And>x. x \<in> A \<Longrightarrow> m \<le> x" unfolding bdd_below_def by auto
+  hence "A \<subseteq> {m..}" by auto
+  hence "closure A \<subseteq> {m..}" using closed_real_atLeast by (rule closure_minimal)
+  thus ?thesis unfolding bdd_below_def by auto
+qed
 
 subsection\<open>Connected components, considered as a connectedness relation or a set\<close>
 
@@ -2649,6 +2659,17 @@
   shows "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> closed S \<Longrightarrow> Inf S \<in> S"
   by (metis closure_contains_Inf closure_closed assms)
 
+lemma closed_subset_contains_Inf:
+  fixes A C :: "real set"
+  shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> Inf A \<in> C"
+  by (metis closure_contains_Inf closure_minimal subset_eq)
+
+lemma atLeastAtMost_subset_contains_Inf:
+  fixes A :: "real set" and a b :: real 
+  shows "A \<noteq> {} \<Longrightarrow> a \<le> b \<Longrightarrow> A \<subseteq> {a..b} \<Longrightarrow> Inf A \<in> {a..b}"
+  by (rule closed_subset_contains_Inf) 
+     (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a])
+
 lemma not_trivial_limit_within_ball:
   "\<not> trivial_limit (at x within S) \<longleftrightarrow> (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"
   (is "?lhs \<longleftrightarrow> ?rhs")
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Parity.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -321,7 +321,10 @@
     with \<open>a \<le> b\<close> show ?thesis using power_mono by auto
   qed
 qed
- 
+
+lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))"
+  by auto
+
 text \<open>Simplify, when the exponent is a numeral\<close>
 
 lemma zero_le_power_eq_numeral [simp]:
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Power.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -755,7 +755,6 @@
   "(x - y)\<^sup>2 = (y - x)\<^sup>2"
   by (simp add: algebra_simps power2_eq_square)
 
-
 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
 
 lemmas zero_compare_simps =
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Binary_Product_Measure.thy
--- a/src/HOL/Probability/Binary_Product_Measure.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -1012,7 +1012,7 @@
     also have "\<dots> = (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV)"
       by(rule nn_integral_cong)(force split: split_indicator intro: rev_image_eqI simp add: C')
     also have "\<dots> = (\<integral>\<^sup>+ x'. (\<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV) * indicator {x} x' \<partial>count_space UNIV)"
-      by(simp add: one_ereal_def[symmetric] nn_integral_nonneg nn_integral_cmult_indicator)
+      by(simp add: one_ereal_def[symmetric] nn_integral_nonneg max_def)
     also have "\<dots> \<le> (\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' (x, y) \<partial>count_space UNIV \<partial>count_space UNIV)"
       by(rule nn_integral_mono)(simp split: split_indicator add: nn_integral_nonneg)
     also have "\<dots> \<le> ?lhs" using **
@@ -1024,7 +1024,7 @@
     have "\<infinity> = \<integral>\<^sup>+ x. ereal (1 / Suc n) * indicator C' x \<partial>count_space UNIV"
       using C'_def False by(simp add: nn_integral_cmult)
     also have "\<dots> = \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C' x * indicator {SOME y. (x, y) \<in> C} y \<partial>count_space UNIV \<partial>count_space UNIV"
-      by(auto simp add: one_ereal_def[symmetric] nn_integral_cmult_indicator intro: nn_integral_cong)
+      by(auto simp add: one_ereal_def[symmetric] max_def intro: nn_integral_cong)
     also have "\<dots> \<le> \<integral>\<^sup>+ x. \<integral>\<^sup>+ y. ereal (1 / Suc n) * indicator C (x, y) \<partial>count_space UNIV \<partial>count_space UNIV"
       by(intro nn_integral_mono)(auto simp add: C'_def split: split_indicator intro: someI)
     also have "\<dots> \<le> ?lhs" using C
@@ -1121,4 +1121,4 @@
     by (auto simp: space_pair_measure M.emeasure_pair_measure_Times)
 qed
 
-end
\ No newline at end of file
+end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -1042,10 +1042,14 @@
     integral\<^sup>L M (\<lambda>x. f x - g x) = integral\<^sup>L M f - integral\<^sup>L M g"
   by (intro has_bochner_integral_integral_eq has_bochner_integral_diff has_bochner_integral_integrable)
 
-lemma integral_setsum[simp]: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow>
+lemma integral_setsum: "(\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)) \<Longrightarrow>
   integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
   by (intro has_bochner_integral_integral_eq has_bochner_integral_setsum has_bochner_integral_integrable)
 
+lemma integral_setsum'[simp]: "(\<And>i. i \<in> I =simp=> integrable M (f i)) \<Longrightarrow>
+  integral\<^sup>L M (\<lambda>x. \<Sum>i\<in>I. f i x) = (\<Sum>i\<in>I. integral\<^sup>L M (f i))"
+  unfolding simp_implies_def by (rule integral_setsum)
+
 lemma integral_bounded_linear: "bounded_linear T \<Longrightarrow> integrable M f \<Longrightarrow>
     integral\<^sup>L M (\<lambda>x. T (f x)) = T (integral\<^sup>L M f)"
   by (metis has_bochner_integral_bounded_linear has_bochner_integral_integrable has_bochner_integral_integral_eq)
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -22,6 +22,272 @@
     by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)  
 qed
 
+definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
+
+lemma mono_onI:
+  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A"
+  unfolding mono_on_def by simp
+
+lemma mono_onD:
+  "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
+  unfolding mono_on_def by simp
+
+lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
+  unfolding mono_def mono_on_def by auto
+
+lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
+  unfolding mono_on_def by auto
+
+definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s"
+
+lemma strict_mono_onI:
+  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A"
+  unfolding strict_mono_on_def by simp
+
+lemma strict_mono_onD:
+  "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
+  unfolding strict_mono_on_def by simp
+
+lemma mono_on_greaterD:
+  assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
+  shows "x > y"
+proof (rule ccontr)
+  assume "\<not>x > y"
+  hence "x \<le> y" by (simp add: not_less)
+  from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
+  with assms(4) show False by simp
+qed
+
+lemma strict_mono_inv:
+  fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
+  assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
+  shows "strict_mono g"
+proof
+  fix x y :: 'b assume "x < y"
+  from \<open>surj f\<close> obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
+  with \<open>x < y\<close> and \<open>strict_mono f\<close> have "x' < y'" by (simp add: strict_mono_less)
+  with inv show "g x < g y" by simp
+qed
+
+lemma strict_mono_on_imp_inj_on:
+  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
+  shows "inj_on f A"
+proof (rule inj_onI)
+  fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
+  thus "x = y"
+    by (cases x y rule: linorder_cases)
+       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 
+qed
+
+lemma strict_mono_on_leD:
+  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
+  shows "f x \<le> f y"
+proof (insert le_less_linear[of y x], elim disjE)
+  assume "x < y"
+  with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
+  thus ?thesis by (rule less_imp_le)
+qed (insert assms, simp)
+
+lemma strict_mono_on_eqD:
+  fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
+  assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
+  shows "y = x"
+  using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
+
+lemma mono_on_imp_deriv_nonneg:
+  assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
+  assumes "x \<in> interior A"
+  shows "D \<ge> 0"
+proof (rule tendsto_le_const)
+  let ?A' = "(\<lambda>y. y - x) ` interior A"
+  from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)"
+      by (simp add: field_has_derivative_at has_field_derivative_def)
+  from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset)
+
+  show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
+  proof (subst eventually_at_topological, intro exI conjI ballI impI)
+    have "open (interior A)" by simp
+    hence "open (op + (-x) ` interior A)" by (rule open_translation)
+    also have "(op + (-x) ` interior A) = ?A'" by auto
+    finally show "open ?A'" .
+  next
+    from \<open>x \<in> interior A\<close> show "0 \<in> ?A'" by auto
+  next
+    fix h assume "h \<in> ?A'"
+    hence "x + h \<in> interior A" by auto
+    with mono' and \<open>x \<in> interior A\<close> show "(f (x + h) - f x) / h \<ge> 0"
+      by (cases h rule: linorder_cases[of _ 0])
+         (simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps)
+  qed
+qed simp
+
+lemma strict_mono_on_imp_mono_on: 
+  "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
+  by (rule mono_onI, rule strict_mono_on_leD)
+
+lemma mono_on_ctble_discont:
+  fixes f :: "real \<Rightarrow> real"
+  fixes A :: "real set"
+  assumes "mono_on f A"
+  shows "countable {a\<in>A. \<not> continuous (at a within A) f}"
+proof -
+  have mono: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+    using `mono_on f A` by (simp add: mono_on_def)
+  have "\<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}. \<exists>q :: nat \<times> rat.
+      (fst q = 0 \<and> of_rat (snd q) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd q))) \<or>
+      (fst q = 1 \<and> of_rat (snd q) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> f x > of_rat (snd q)))"
+  proof (clarsimp simp del: One_nat_def)
+    fix a assume "a \<in> A" assume "\<not> continuous (at a within A) f"
+    thus "\<exists>q1 q2.
+            q1 = 0 \<and> real_of_rat q2 < f a \<and> (\<forall>x\<in>A. x < a \<longrightarrow> f x < real_of_rat q2) \<or>
+            q1 = 1 \<and> f a < real_of_rat q2 \<and> (\<forall>x\<in>A. a < x \<longrightarrow> real_of_rat q2 < f x)"
+    proof (auto simp add: continuous_within order_tendsto_iff eventually_at)
+      fix l assume "l < f a"
+      then obtain q2 where q2: "l < of_rat q2" "of_rat q2 < f a"
+        using of_rat_dense by blast
+      assume * [rule_format]: "\<forall>d>0. \<exists>x\<in>A. x \<noteq> a \<and> dist x a < d \<and> \<not> l < f x"
+      from q2 have "real_of_rat q2 < f a \<and> (\<forall>x\<in>A. x < a \<longrightarrow> f x < real_of_rat q2)"
+      proof auto
+        fix x assume "x \<in> A" "x < a"
+        with q2 *[of "a - x"] show "f x < real_of_rat q2"
+          apply (auto simp add: dist_real_def not_less)
+          apply (subgoal_tac "f x \<le> f xa")
+          by (auto intro: mono)
+      qed 
+      thus ?thesis by auto
+    next
+      fix u assume "u > f a"
+      then obtain q2 where q2: "f a < of_rat q2" "of_rat q2 < u"
+        using of_rat_dense by blast
+      assume *[rule_format]: "\<forall>d>0. \<exists>x\<in>A. x \<noteq> a \<and> dist x a < d \<and> \<not> u > f x"
+      from q2 have "real_of_rat q2 > f a \<and> (\<forall>x\<in>A. x > a \<longrightarrow> f x > real_of_rat q2)"
+      proof auto
+        fix x assume "x \<in> A" "x > a"
+        with q2 *[of "x - a"] show "f x > real_of_rat q2"
+          apply (auto simp add: dist_real_def)
+          apply (subgoal_tac "f x \<ge> f xa")
+          by (auto intro: mono)
+      qed 
+      thus ?thesis by auto
+    qed
+  qed
+  hence "\<exists>g :: real \<Rightarrow> nat \<times> rat . \<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}. 
+      (fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
+      (fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> f x > of_rat (snd (g a))))"
+    by (rule bchoice)
+  then guess g ..
+  hence g: "\<And>a x. a \<in> A \<Longrightarrow> \<not> continuous (at a within A) f \<Longrightarrow> x \<in> A \<Longrightarrow>
+      (fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
+      (fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (x > a \<longrightarrow> f x > of_rat (snd (g a))))"
+    by auto
+  have "inj_on g {a\<in>A. \<not> continuous (at a within A) f}"
+  proof (auto simp add: inj_on_def)
+    fix w z
+    assume 1: "w \<in> A" and 2: "\<not> continuous (at w within A) f" and
+           3: "z \<in> A" and 4: "\<not> continuous (at z within A) f" and
+           5: "g w = g z"
+    from g [OF 1 2 3] g [OF 3 4 1] 5 
+    show "w = z" by auto
+  qed
+  thus ?thesis 
+    by (rule countableI') 
+qed
+
+lemma mono_on_ctble_discont_open:
+  fixes f :: "real \<Rightarrow> real"
+  fixes A :: "real set"
+  assumes "open A" "mono_on f A"
+  shows "countable {a\<in>A. \<not>isCont f a}"
+proof -
+  have "{a\<in>A. \<not>isCont f a} = {a\<in>A. \<not>(continuous (at a within A) f)}"
+    by (auto simp add: continuous_within_open [OF _ `open A`])
+  thus ?thesis
+    apply (elim ssubst)
+    by (rule mono_on_ctble_discont, rule assms)
+qed
+
+lemma mono_ctble_discont:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "mono f"
+  shows "countable {a. \<not> isCont f a}"
+using assms mono_on_ctble_discont [of f UNIV] unfolding mono_on_def mono_def by auto
+
+lemma has_real_derivative_imp_continuous_on:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
+  shows "continuous_on A f"
+  apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
+  apply (intro ballI Deriv.differentiableI)
+  apply (rule has_field_derivative_subset[OF assms])
+  apply simp_all
+  done
+
+lemma closure_contains_Sup:
+  fixes S :: "real set"
+  assumes "S \<noteq> {}" "bdd_above S"
+  shows "Sup S \<in> closure S"
+proof-
+  have "Inf (uminus ` S) \<in> closure (uminus ` S)" 
+      using assms by (intro closure_contains_Inf) auto
+  also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
+  also have "closure (uminus ` S) = uminus ` closure S"
+      by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
+  finally show ?thesis by auto
+qed
+
+lemma closed_contains_Sup:
+  fixes S :: "real set"
+  shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
+  by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
+
+lemma deriv_nonneg_imp_mono:
+  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes ab: "a \<le> b"
+  shows "g a \<le> g b"
+proof (cases "a < b")
+  assume "a < b"
+  from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
+  from MVT2[OF \<open>a < b\<close> this] and deriv 
+    obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
+  from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
+  with g_ab show ?thesis by simp
+qed (insert ab, simp)
+
+lemma continuous_interval_vimage_Int:
+  assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
+  assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}"
+  obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d"
+proof-
+    let ?A = "{a..b} \<inter> g -` {c..d}"
+    from IVT'[of g a c b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) 
+         obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto
+    from IVT'[of g a d b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) 
+         obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto
+    hence [simp]: "?A \<noteq> {}" by blast
+
+    def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A"
+    have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def
+        by (intro subsetI) (auto intro: cInf_lower cSup_upper)
+    moreover from assms have "closed ?A" 
+        using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
+    hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def
+        by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
+    hence "{c'..d'} \<subseteq> ?A" using assms 
+        by (intro subsetI)
+           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] 
+                 intro!: mono)
+    moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
+    moreover have "g c' \<le> c" "g d' \<ge> d"
+      apply (insert c'' d'' c'd'_in_set)
+      apply (subst c''(2)[symmetric])
+      apply (auto simp: c'_def intro!: mono cInf_lower c'') []
+      apply (subst d''(2)[symmetric])
+      apply (auto simp: d'_def intro!: mono cSup_upper d'') []
+      done
+    with c'd'_in_set have "g c' = c" "g d' = d" by auto
+    ultimately show ?thesis using that by blast
+qed
+
 subsection \<open>Generic Borel spaces\<close>
 
 definition borel :: "'a::topological_space measure" where
@@ -49,6 +315,10 @@
 lemma sets_borel: "sets borel = sigma_sets UNIV {S. open S}"
   unfolding borel_def by (rule sets_measure_of) simp
 
+lemma measurable_sets_borel:
+    "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
+  by (drule (1) measurable_sets) simp
+
 lemma pred_Collect_borel[measurable (raw)]: "Measurable.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
   unfolding borel_def pred_def by auto
 
@@ -888,6 +1158,28 @@
     by (subst borel_measurable_iff_halfspace_le) auto
 qed auto
 
+lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
+  assumes "A \<in> sets borel" 
+  assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
+          un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
+  shows "P (A::real set)"
+proof-
+  let ?G = "range (\<lambda>(a,b). {a..b::real})"
+  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" 
+      using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
+  thus ?thesis
+  proof (induction rule: sigma_sets_induct_disjoint) 
+    case (union f)
+      from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
+      with union show ?case by (auto intro: un)
+  next
+    case (basic A)
+    then obtain a b where "A = {a .. b}" by auto
+    then show ?case
+      by (cases "a \<le> b") (auto intro: int empty)
+  qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
+qed
+
 subsection "Borel measurable operators"
 
 lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
@@ -1467,6 +1759,11 @@
     by simp
 qed
 
+lemma isCont_borel_pred[measurable]:
+  fixes f :: "'b::metric_space \<Rightarrow> 'a::metric_space"
+  shows "Measurable.pred borel (isCont f)"
+  unfolding pred_def by (simp add: isCont_borel)
+
 lemma is_real_interval:
   assumes S: "is_interval S"
   shows "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or> S = {a<..} \<or> S = {a..} \<or>
@@ -1485,16 +1782,21 @@
     by auto
 qed
 
+lemma borel_measurable_mono_on_fnc:
+  fixes f :: "real \<Rightarrow> real" and A :: "real set"
+  assumes "mono_on f A"
+  shows "f \<in> borel_measurable (restrict_space borel A)"
+  apply (rule measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]])
+  apply (auto intro!: image_eqI[where x="{x}" for x] simp: sets_restrict_space)
+  apply (auto simp add: sets_restrict_restrict_space continuous_on_eq_continuous_within
+              cong: measurable_cong_sets 
+              intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset)
+  done
+
 lemma borel_measurable_mono:
   fixes f :: "real \<Rightarrow> real"
-  assumes "mono f"
-  shows "f \<in> borel_measurable borel"
-proof (subst borel_measurable_iff_ge, auto simp add:)
-  fix a :: real
-  have "is_interval {w. a \<le> f w}"
-    unfolding is_interval_1 using assms by (auto dest: monoD intro: order.trans)
-  thus "{w. a \<le> f w} \<in> sets borel" using real_interval_borel_measurable by auto  
-qed
+  shows "mono f \<Longrightarrow> f \<in> borel_measurable borel"
+  using borel_measurable_mono_on_fnc[of f UNIV] by (simp add: mono_def mono_on_def)
 
 no_notation
   eucl_less (infix "<e" 50)
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Central_Limit_Theorem.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Central_Limit_Theorem.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -0,0 +1,117 @@
+(*  Theory: Central_Limit_Theorem.thy
+    Authors: Jeremy Avigad, Luke Serafin
+*)
+
+section \<open>The Central Limit Theorem\<close>
+
+theory Central_Limit_Theorem
+  imports Levy
+begin
+
+theorem (in prob_space) central_limit_theorem:
+  fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> real"
+    and \<mu> :: "real measure"
+    and \<sigma> :: real
+    and S :: "nat \<Rightarrow> 'a \<Rightarrow> real"
+  assumes X_indep: "indep_vars (\<lambda>i. borel) X UNIV"
+    and X_integrable: "\<And>n. integrable M (X n)"
+    and X_mean_0: "\<And>n. expectation (X n) = 0"
+    and \<sigma>_pos: "\<sigma> > 0"
+    and X_square_integrable: "\<And>n. integrable M (\<lambda>x. (X n x)\<^sup>2)"
+    and X_variance: "\<And>n. variance (X n) = \<sigma>\<^sup>2"
+    and X_distrib: "\<And>n. distr M borel (X n) = \<mu>"
+  defines "S n \<equiv> \<lambda>x. \<Sum>i<n. X i x"
+  shows "weak_conv_m (\<lambda>n. distr M borel (\<lambda>x. S n x / sqrt (n * \<sigma>\<^sup>2))) std_normal_distribution"
+proof -
+  let ?S' = "\<lambda>n x. S n x / sqrt (real n * \<sigma>\<^sup>2)"
+  def \<phi> \<equiv> "\<lambda>n. char (distr M borel (?S' n))"
+  def \<psi> \<equiv> "\<lambda>n t. char \<mu> (t / sqrt (\<sigma>\<^sup>2 * n))"
+
+  have X_rv [simp, measurable]: "\<And>n. random_variable borel (X n)"
+    using X_indep unfolding indep_vars_def2 by simp
+  interpret \<mu>: real_distribution \<mu>
+    by (subst X_distrib [symmetric, of 0], rule real_distribution_distr, simp)
+
+  (* these are equivalent to the hypotheses on X, given X_distr *)
+  have \<mu>_integrable [simp]: "integrable \<mu> (\<lambda>x. x)"
+    and \<mu>_mean_integrable [simp]: "\<mu>.expectation (\<lambda>x. x) = 0"
+    and \<mu>_square_integrable [simp]: "integrable \<mu> (\<lambda>x. x^2)"
+    and \<mu>_variance [simp]: "\<mu>.expectation (\<lambda>x. x^2) = \<sigma>\<^sup>2"
+    using assms by (simp_all add: X_distrib [symmetric, of 0] integrable_distr_eq integral_distr)
+
+  have main: "\<forall>\<^sub>F n in sequentially.
+      cmod (\<phi> n t - (1 + (-(t^2) / 2) / n)^n) \<le>
+      t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>t / sqrt (\<sigma>\<^sup>2 * n)\<bar> * \<bar>x\<bar> ^ 3))" for t
+  proof (rule eventually_sequentiallyI)
+    fix n :: nat
+    assume "n \<ge> nat (ceiling (t^2 / 4))"
+    hence n: "n \<ge> t^2 / 4" by (subst nat_ceiling_le_eq [symmetric])
+    let ?t = "t / sqrt (\<sigma>\<^sup>2 * n)"
+
+    def \<psi>' \<equiv> "\<lambda>n i. char (distr M borel (\<lambda>x. X i x / sqrt (\<sigma>\<^sup>2 * n)))"
+    have *: "\<And>n i t. \<psi>' n i t = \<psi> n t"
+      unfolding \<psi>_def \<psi>'_def char_def
+      by (subst X_distrib [symmetric]) (auto simp: integral_distr)
+
+    have "\<phi> n t = char (distr M borel (\<lambda>x. \<Sum>i<n. X i x / sqrt (\<sigma>\<^sup>2 * real n))) t"
+      by (auto simp: \<phi>_def S_def setsum_divide_distrib ac_simps)
+    also have "\<dots> = (\<Prod> i < n. \<psi>' n i t)"
+      unfolding \<psi>'_def
+      apply (rule char_distr_setsum)
+      apply (rule indep_vars_compose2[where X=X])
+      apply (rule indep_vars_subset)
+      apply (rule X_indep)
+      apply auto
+      done
+    also have "\<dots> = (\<psi> n t)^n"
+      by (auto simp add: * setprod_constant)
+    finally have \<phi>_eq: "\<phi> n t =(\<psi> n t)^n" .
+
+    have "norm (\<psi> n t - (1 - ?t^2 * \<sigma>\<^sup>2 / 2)) \<le> ?t\<^sup>2 / 6 * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3))"
+      unfolding \<psi>_def by (rule \<mu>.char_approx3, auto)
+    also have "?t^2 * \<sigma>\<^sup>2 = t^2 / n"
+      using \<sigma>_pos by (simp add: power_divide)
+    also have "t^2 / n / 2 = (t^2 / 2) / n"
+      by simp
+    finally have **: "norm (\<psi> n t - (1 + (-(t^2) / 2) / n)) \<le> 
+      ?t\<^sup>2 / 6 * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3))" by simp
+
+    have "norm (\<phi> n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \<le> 
+         n * norm (\<psi> n t - (complex_of_real (1 + (-(t^2) / 2) / n)))"
+      using n
+      by (auto intro!: norm_power_diff \<mu>.cmod_char_le_1 abs_leI
+               simp del: of_real_diff simp: of_real_diff[symmetric] divide_le_eq \<phi>_eq \<psi>_def)
+    also have "\<dots> \<le> n * (?t\<^sup>2 / 6 * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
+      by (rule mult_left_mono [OF **], simp)
+    also have "\<dots> = (t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))" 
+      using \<sigma>_pos by (simp add: field_simps min_absorb2)
+    finally show "norm (\<phi> n t - (1 + (-(t^2) / 2) / n)^n) \<le> 
+        (t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))" 
+      by simp
+  qed
+
+  show ?thesis
+  proof (rule levy_continuity)
+    fix t
+    let ?t = "\<lambda>n. t / sqrt (\<sigma>\<^sup>2 * n)"
+    have "\<And>x. (\<lambda>n. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3 / \<bar>sqrt (\<sigma>\<^sup>2 * real n)\<bar>)) \<longlonglongrightarrow> 0"
+      using \<sigma>_pos 
+      by (auto simp: real_sqrt_mult min_absorb2
+               intro!: tendsto_min[THEN tendsto_eq_rhs] sqrt_at_top[THEN filterlim_compose]
+                       filterlim_tendsto_pos_mult_at_top filterlim_at_top_imp_at_infinity
+                       tendsto_divide_0 filterlim_real_sequentially)
+    then have "(\<lambda>n. LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t n\<bar> * \<bar>x\<bar> ^ 3)) \<longlonglongrightarrow> (LINT x|\<mu>. 0)"
+      by (intro integral_dominated_convergence [where w = "\<lambda>x. 6 * x^2"]) auto
+    then have *: "(\<lambda>n. t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t n\<bar> * \<bar>x\<bar> ^ 3))) \<longlonglongrightarrow> 0"
+      by (simp only: integral_zero tendsto_mult_right_zero)
+
+    have "(\<lambda>n. complex_of_real ((1 + (-(t^2) / 2) / n)^n)) \<longlonglongrightarrow> complex_of_real (exp (-(t^2) / 2))"
+      by (rule isCont_tendsto_compose [OF _ tendsto_exp_limit_sequentially]) auto
+    then have "(\<lambda>n. \<phi> n t) \<longlonglongrightarrow> complex_of_real (exp (-(t^2) / 2))"
+      by (rule Lim_transform) (rule Lim_null_comparison [OF main *])
+    then show "(\<lambda>n. char (distr M borel (?S' n)) t) \<longlonglongrightarrow> char std_normal_distribution t"
+      by (simp add: \<phi>_def char_std_normal_distribution)
+  qed (auto intro!: real_dist_normal_dist simp: S_def)
+qed
+
+end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Characteristic_Functions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -0,0 +1,554 @@
+(*
+  Theory: Characteristic_Functions.thy
+  Authors: Jeremy Avigad, Luke Serafin
+*)
+
+section \<open>Characteristic Functions\<close>
+
+theory Characteristic_Functions
+  imports Weak_Convergence Interval_Integral Independent_Family Distributions
+begin
+
+lemma mult_min_right: "a \<ge> 0 \<Longrightarrow> (a :: real) * min b c = min (a * b) (a * c)"
+  by (metis min.absorb_iff2 min_def mult_left_mono)
+
+lemma sequentially_even_odd:
+  assumes E: "eventually (\<lambda>n. P (2 * n)) sequentially" and O: "eventually (\<lambda>n. P (2 * n + 1)) sequentially"
+  shows "eventually P sequentially"
+proof -
+  from E obtain n_e where [intro]: "\<And>n. n \<ge> n_e \<Longrightarrow> P (2 * n)"
+    by (auto simp: eventually_sequentially)
+  moreover
+  from O obtain n_o where [intro]: "\<And>n. n \<ge> n_o \<Longrightarrow> P (Suc (2 * n))"
+    by (auto simp: eventually_sequentially)
+  show ?thesis
+    unfolding eventually_sequentially
+  proof (intro exI allI impI)
+    fix n assume "max (2 * n_e) (2 * n_o + 1) \<le> n" then show "P n"
+      by (cases "even n") (auto elim!: evenE oddE )
+  qed
+qed
+
+lemma limseq_even_odd: 
+  assumes "(\<lambda>n. f (2 * n)) \<longlonglongrightarrow> (l :: 'a :: topological_space)"
+      and "(\<lambda>n. f (2 * n + 1)) \<longlonglongrightarrow> l"
+  shows "f \<longlonglongrightarrow> l"
+  using assms by (auto simp: filterlim_iff intro: sequentially_even_odd)
+
+subsection \<open>Application of the FTC: integrating $e^ix$\<close>
+
+abbreviation iexp :: "real \<Rightarrow> complex" where
+  "iexp \<equiv> (\<lambda>x. exp (\<i> * complex_of_real x))"
+
+lemma isCont_iexp [simp]: "isCont iexp x"
+  by (intro continuous_intros)
+
+lemma has_vector_derivative_iexp[derivative_intros]:
+  "(iexp has_vector_derivative \<i> * iexp x) (at x within s)"
+  by (auto intro!: derivative_eq_intros simp: Re_exp Im_exp has_vector_derivative_complex_iff)
+
+lemma interval_integral_iexp:
+  fixes a b :: real
+  shows "(CLBINT x=a..b. iexp x) = ii * iexp a - ii * iexp b"
+  by (subst interval_integral_FTC_finite [where F = "\<lambda>x. -ii * iexp x"])
+     (auto intro!: derivative_eq_intros continuous_intros)
+
+subsection \<open>The Characteristic Function of a Real Measure.\<close>
+
+definition
+  char :: "real measure \<Rightarrow> real \<Rightarrow> complex"
+where
+  "char M t = CLINT x|M. iexp (t * x)"
+
+lemma (in real_distribution) char_zero: "char M 0 = 1"
+  unfolding char_def by (simp del: space_eq_univ add: prob_space)
+
+lemma (in prob_space) integrable_iexp: 
+  assumes f: "f \<in> borel_measurable M" "\<And>x. Im (f x) = 0"
+  shows "integrable M (\<lambda>x. exp (ii * (f x)))"
+proof (intro integrable_const_bound [of _ 1])
+  from f have "\<And>x. of_real (Re (f x)) = f x"
+    by (simp add: complex_eq_iff)
+  then show "AE x in M. cmod (exp (\<i> * f x)) \<le> 1"
+    using norm_exp_ii_times[of "Re (f x)" for x] by simp
+qed (insert f, simp)
+
+lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1"
+proof -
+  have "norm (char M t) \<le> (\<integral>x. norm (iexp (t * x)) \<partial>M)"
+    unfolding char_def by (intro integral_norm_bound integrable_iexp) auto
+  also have "\<dots> \<le> 1"
+    by (simp del: of_real_mult)
+  finally show ?thesis .
+qed
+
+lemma (in real_distribution) isCont_char: "isCont (char M) t"
+  unfolding continuous_at_sequentially
+proof safe
+  fix X assume X: "X \<longlonglongrightarrow> t"
+  show "(char M \<circ> X) \<longlonglongrightarrow> char M t"
+    unfolding comp_def char_def
+    by (rule integral_dominated_convergence[where w="\<lambda>_. 1"]) (auto intro!: tendsto_intros X)
+qed
+
+lemma (in real_distribution) char_measurable [measurable]: "char M \<in> borel_measurable borel"
+  by (auto intro!: borel_measurable_continuous_on1 continuous_at_imp_continuous_on isCont_char)
+
+subsection \<open>Independence\<close>
+
+(* the automation can probably be improved *)  
+lemma (in prob_space) char_distr_sum:
+  fixes X1 X2 :: "'a \<Rightarrow> real" and t :: real
+  assumes "indep_var borel X1 borel X2"
+  shows "char (distr M borel (\<lambda>\<omega>. X1 \<omega> + X2 \<omega>)) t =
+    char (distr M borel X1) t * char (distr M borel X2) t"
+proof -
+  from assms have [measurable]: "random_variable borel X1" by (elim indep_var_rv1)
+  from assms have [measurable]: "random_variable borel X2" by (elim indep_var_rv2)
+
+  have "char (distr M borel (\<lambda>\<omega>. X1 \<omega> + X2 \<omega>)) t = (CLINT x|M. iexp (t * (X1 x + X2 x)))"
+    by (simp add: char_def integral_distr)
+  also have "\<dots> = (CLINT x|M. iexp (t * (X1 x)) * iexp (t * (X2 x))) "
+    by (simp add: field_simps exp_add)
+  also have "\<dots> = (CLINT x|M. iexp (t * (X1 x))) * (CLINT x|M. iexp (t * (X2 x)))"
+    by (intro indep_var_lebesgue_integral indep_var_compose[unfolded comp_def, OF assms])
+       (auto intro!: integrable_iexp)
+  also have "\<dots> = char (distr M borel X1) t * char (distr M borel X2) t"
+    by (simp add: char_def integral_distr)
+  finally show ?thesis .
+qed
+
+lemma (in prob_space) char_distr_setsum:
+  "indep_vars (\<lambda>i. borel) X A \<Longrightarrow>
+    char (distr M borel (\<lambda>\<omega>. \<Sum>i\<in>A. X i \<omega>)) t = (\<Prod>i\<in>A. char (distr M borel (X i)) t)"
+proof (induct A rule: infinite_finite_induct)
+  case (insert x F) with indep_vars_subset[of "\<lambda>_. borel" X "insert x F" F] show ?case
+    by (auto simp add: char_distr_sum indep_vars_setsum)
+qed (simp_all add: char_def integral_distr prob_space del: distr_const)
+
+subsection \<open>Approximations to $e^{ix}$\<close>
+
+text \<open>Proofs from Billingsley, page 343.\<close>
+
+lemma CLBINT_I0c_power_mirror_iexp:
+  fixes x :: real and n :: nat
+  defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
+  shows "(CLBINT s=0..x. f s n * iexp s) =
+    x^Suc n / Suc n + (ii / Suc n) * (CLBINT s=0..x. f s (Suc n) * iexp s)"
+proof -
+  have 1:
+    "((\<lambda>s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s)
+      has_vector_derivative complex_of_real((x - s)^n) * iexp s + (ii * iexp s) * complex_of_real(-((x - s) ^ (Suc n) / (Suc n))))
+      (at s within A)" for s A
+    by (intro derivative_eq_intros) auto
+
+  let ?F = "\<lambda>s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s"
+  have "x^(Suc n) / (Suc n) = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * -(f s (Suc n) / (Suc n))))" (is "?LHS = ?RHS")
+  proof -
+    have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * 
+      complex_of_real(-((x - s) ^ (Suc n) / (Suc n)))))"
+      by (cases "0 \<le> x") (auto intro!: simp: f_def[abs_def])
+    also have "... = ?F x - ?F 0"
+      unfolding zero_ereal_def using 1
+      by (intro interval_integral_FTC_finite)
+         (auto simp: f_def add_nonneg_eq_0_iff complex_eq_iff 
+               intro!: continuous_at_imp_continuous_on continuous_intros)
+    finally show ?thesis
+      by auto
+  qed
+  show ?thesis
+    unfolding \<open>?LHS = ?RHS\<close> f_def interval_lebesgue_integral_mult_right [symmetric]
+    by (subst interval_lebesgue_integral_add(2) [symmetric])
+       (auto intro!: interval_integrable_isCont continuous_intros simp: zero_ereal_def complex_eq_iff)
+qed
+
+lemma iexp_eq1:
+  fixes x :: real
+  defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
+  shows "iexp x =
+    (\<Sum>k \<le> n. (ii * x)^k / (fact k)) + ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (f s n) * (iexp s))" (is "?P n")
+proof (induction n)
+  show "?P 0"
+    by (auto simp add: field_simps interval_integral_iexp f_def zero_ereal_def)
+next
+  fix n assume ih: "?P n"
+  have **: "\<And>a b :: real. a = -b \<longleftrightarrow> a + b = 0"
+    by linarith
+  have *: "of_nat n * of_nat (fact n) \<noteq> - (of_nat (fact n)::complex)"
+    unfolding of_nat_mult[symmetric]
+    by (simp add: complex_eq_iff ** of_nat_add[symmetric] del: of_nat_mult of_nat_fact of_nat_add)
+  show "?P (Suc n)"
+    unfolding setsum_atMost_Suc ih f_def CLBINT_I0c_power_mirror_iexp[of _ n]
+    by (simp add: divide_simps add_eq_0_iff *) (simp add: field_simps)
+qed
+
+lemma iexp_eq2:
+  fixes x :: real
+  defines "f s m \<equiv> complex_of_real ((x - s) ^ m)" 
+  shows "iexp x = (\<Sum>k\<le>Suc n. (ii*x)^k/fact k) + ii^Suc n/fact n * (CLBINT s=0..x. f s n*(iexp s - 1))"
+proof -
+  have isCont_f: "isCont (\<lambda>s. f s n) x" for n x
+    by (auto simp: f_def)
+  let ?F = "\<lambda>s. complex_of_real (-((x - s) ^ (Suc n) / real (Suc n)))"
+  have calc1: "(CLBINT s=0..x. f s n * (iexp s - 1)) =
+    (CLBINT s=0..x. f s n * iexp s) - (CLBINT s=0..x. f s n)"
+    unfolding zero_ereal_def
+    by (subst interval_lebesgue_integral_diff(2) [symmetric])
+       (simp_all add: interval_integrable_isCont isCont_f field_simps)
+
+  have calc2: "(CLBINT s=0..x. f s n) = x^Suc n / Suc n"
+    unfolding zero_ereal_def
+  proof (subst interval_integral_FTC_finite [where a = 0 and b = x and f = "\<lambda>s. f s n" and F = ?F])
+    show "(?F has_vector_derivative f y n) (at y within {min 0 x..max 0 x})" for y
+      unfolding f_def
+      by (intro has_vector_derivative_of_real)
+         (auto intro!: derivative_eq_intros simp del: power_Suc simp add: add_nonneg_eq_0_iff)
+  qed (auto intro: continuous_at_imp_continuous_on isCont_f)
+
+  have calc3: "ii ^ (Suc (Suc n)) / (fact (Suc n)) = (ii ^ (Suc n) / (fact n)) * (ii / (Suc n))"
+    by (simp add: field_simps)
+
+  show ?thesis
+    unfolding iexp_eq1 [where n = "Suc n" and x=x] calc1 calc2 calc3 unfolding f_def
+    by (subst CLBINT_I0c_power_mirror_iexp [where n = n]) auto
+qed
+
+lemma abs_LBINT_I0c_abs_power_diff:
+  "\<bar>LBINT s=0..x. \<bar>(x - s)^n\<bar>\<bar> = \<bar>x ^ (Suc n) / (Suc n)\<bar>"
+proof -
+ have "\<bar>LBINT s=0..x. \<bar>(x - s)^n\<bar>\<bar> = \<bar>LBINT s=0..x. (x - s)^n\<bar>"
+  proof cases
+    assume "0 \<le> x \<or> even n"
+    then have "(LBINT s=0..x. \<bar>(x - s)^n\<bar>) = LBINT s=0..x. (x - s)^n"
+      by (auto simp add: zero_ereal_def power_even_abs power_abs min_absorb1 max_absorb2
+               intro!: interval_integral_cong)
+    then show ?thesis by simp
+  next
+    assume "\<not> (0 \<le> x \<or> even n)" 
+    then have "(LBINT s=0..x. \<bar>(x - s)^n\<bar>) = LBINT s=0..x. -((x - s)^n)"
+      by (auto simp add: zero_ereal_def power_abs min_absorb1 max_absorb2
+                         ereal_min[symmetric] ereal_max[symmetric] power_minus_odd[symmetric]
+               simp del: ereal_min ereal_max intro!: interval_integral_cong)
+    also have "\<dots> = - (LBINT s=0..x. (x - s)^n)"
+      by (subst interval_lebesgue_integral_uminus, rule refl)
+    finally show ?thesis by simp
+  qed
+  also have "LBINT s=0..x. (x - s)^n = x^Suc n / Suc n"
+  proof -
+    let ?F = "\<lambda>t. - ((x - t)^(Suc n) / Suc n)"
+    have "LBINT s=0..x. (x - s)^n = ?F x - ?F 0"
+      unfolding zero_ereal_def
+      by (intro interval_integral_FTC_finite continuous_at_imp_continuous_on
+                has_field_derivative_iff_has_vector_derivative[THEN iffD1])
+         (auto simp del: power_Suc intro!: derivative_eq_intros simp add: add_nonneg_eq_0_iff)
+    also have "\<dots> = x ^ (Suc n) / (Suc n)" by simp
+    finally show ?thesis .
+  qed
+  finally show ?thesis .
+qed
+
+lemma iexp_approx1: "cmod (iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k)) \<le> \<bar>x\<bar>^(Suc n) / fact (Suc n)"
+proof -
+  have "iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k) =
+      ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s))" (is "?t1 = ?t2")
+    by (subst iexp_eq1 [of _ n], simp add: field_simps)
+  then have "cmod (?t1) = cmod (?t2)"
+    by simp
+  also have "\<dots> =  (1 / of_nat (fact n)) * cmod (CLBINT s=0..x. (x - s)^n * (iexp s))"
+    by (simp add: norm_mult norm_divide norm_power)
+  also have "\<dots> \<le> (1 / of_nat (fact n)) * \<bar>LBINT s=0..x. cmod ((x - s)^n * (iexp s))\<bar>"
+    by (intro mult_left_mono interval_integral_norm2)
+       (auto simp: zero_ereal_def intro: interval_integrable_isCont)
+  also have "\<dots> \<le> (1 / of_nat (fact n)) * \<bar>LBINT s=0..x. \<bar>(x - s)^n\<bar>\<bar>"
+    by (simp add: norm_mult del: of_real_diff of_real_power)
+  also have "\<dots> \<le> (1 / of_nat (fact n)) * \<bar>x ^ (Suc n) / (Suc n)\<bar>"
+    by (simp add: abs_LBINT_I0c_abs_power_diff)
+  also have "1 / real_of_nat (fact n::nat) * \<bar>x ^ Suc n / real (Suc n)\<bar> =
+      \<bar>x\<bar> ^ Suc n / fact (Suc n)"
+    by (simp add: abs_mult power_abs)
+  finally show ?thesis .
+qed
+
+lemma iexp_approx2: "cmod (iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k)) \<le> 2 * \<bar>x\<bar>^n / fact n"
+proof (induction n) -- \<open>really cases\<close>
+  case (Suc n)
+  have *: "\<And>a b. interval_lebesgue_integrable lborel a b f \<Longrightarrow> interval_lebesgue_integrable lborel a b g \<Longrightarrow>
+      \<bar>LBINT s=a..b. f s\<bar> \<le> \<bar>LBINT s=a..b. g s\<bar>"
+    if f: "\<And>s. 0 \<le> f s" and g: "\<And>s. f s \<le> g s" for f g :: "_ \<Rightarrow> real"
+    using order_trans[OF f g] f g unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def
+    by (auto simp: integral_nonneg_AE[OF AE_I2] intro!: integral_mono mult_mono)
+
+  have "iexp x - (\<Sum>k \<le> Suc n. (ii * x)^k / fact k) =
+      ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s - 1))" (is "?t1 = ?t2")
+    unfolding iexp_eq2 [of x n] by (simp add: field_simps)
+  then have "cmod (?t1) = cmod (?t2)"
+    by simp
+  also have "\<dots> =  (1 / (fact n)) * cmod (CLBINT s=0..x. (x - s)^n * (iexp s - 1))"
+    by (simp add: norm_mult norm_divide norm_power)
+  also have "\<dots> \<le> (1 / (fact n)) * \<bar>LBINT s=0..x. cmod ((x - s)^n * (iexp s - 1))\<bar>"
+    by (intro mult_left_mono interval_integral_norm2)
+       (auto intro!: interval_integrable_isCont simp: zero_ereal_def)
+  also have "\<dots> = (1 / (fact n)) * \<bar>LBINT s=0..x. abs ((x - s)^n) * cmod((iexp s - 1))\<bar>"
+    by (simp add: norm_mult del: of_real_diff of_real_power)
+  also have "\<dots> \<le> (1 / (fact n)) * \<bar>LBINT s=0..x. abs ((x - s)^n) * 2\<bar>"
+    by (intro mult_left_mono * order_trans [OF norm_triangle_ineq4])
+       (auto simp: mult_ac zero_ereal_def intro!: interval_integrable_isCont)
+  also have "\<dots> = (2 / (fact n)) * \<bar>x ^ (Suc n) / (Suc n)\<bar>"
+   by (simp add: abs_LBINT_I0c_abs_power_diff abs_mult)
+  also have "2 / fact n * \<bar>x ^ Suc n / real (Suc n)\<bar> = 2 * \<bar>x\<bar> ^ Suc n / (fact (Suc n))"
+    by (simp add: abs_mult power_abs)
+  finally show ?case .
+qed (insert norm_triangle_ineq4[of "iexp x" 1], simp)
+
+lemma (in real_distribution) char_approx1:
+  assumes integrable_moments: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. x^k)"
+  shows "cmod (char M t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le>
+    (2*\<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>x\<bar>^n)" (is "cmod (char M t - ?t1) \<le> _")
+proof -
+  have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
+    by (intro integrable_const_bound) auto
+  
+  def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
+  have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
+    unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
+  
+  have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k
+    unfolding c_def integral_mult_right_zero integral_complex_of_real by simp
+  then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
+    by (simp add: integ_c)
+  also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
+    unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
+  also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
+    by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
+  also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
+  proof (rule integral_mono)
+    show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
+      by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
+    show "integrable M (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
+      unfolding power_abs[symmetric]
+      by (intro integrable_mult_right integrable_abs integrable_moments) simp
+    show "cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)) \<le> 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n" for x
+      using iexp_approx2[of "t * x" n] by (auto simp add: abs_mult field_simps c_def)
+  qed
+  finally show ?thesis
+    unfolding integral_mult_right_zero .
+qed
+
+lemma (in real_distribution) char_approx2:
+  assumes integrable_moments: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. x ^ k)"
+  shows "cmod (char M t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le>
+    (\<bar>t\<bar>^n / fact (Suc n)) * expectation (\<lambda>x. min (2 * \<bar>x\<bar>^n * Suc n) (\<bar>t\<bar> * \<bar>x\<bar>^Suc n))"
+    (is "cmod (char M t - ?t1) \<le> _")
+proof -
+  have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
+    by (intro integrable_const_bound) auto
+  
+  def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
+  have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
+    unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
+
+  have *: "min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^Suc n / fact (Suc n)) =
+      \<bar>t\<bar>^n / fact (Suc n) * min (2 * \<bar>x\<bar>^n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar>^(Suc n))" for x
+    apply (subst mult_min_right)
+    apply simp
+    apply (rule arg_cong2[where f=min])
+    apply (simp_all add: field_simps abs_mult del: fact_Suc)
+    apply (simp_all add: field_simps)
+    done
+  
+  have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k
+    unfolding c_def integral_mult_right_zero integral_complex_of_real by simp
+  then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
+    by (simp add: integ_c)
+  also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
+    unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
+  also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
+    by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
+  also have "\<dots> \<le> expectation (\<lambda>x. min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^(Suc n) / fact (Suc n)))"
+    (is "_ \<le> expectation ?f")
+  proof (rule integral_mono)
+    show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
+      by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
+    show "integrable M ?f"
+      by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"])
+         (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
+    show "cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)) \<le> ?f x" for x
+      using iexp_approx1[of "t * x" n] iexp_approx2[of "t * x" n]
+      by (auto simp add: abs_mult field_simps c_def intro!: min.boundedI)
+  qed
+  also have "\<dots> = (\<bar>t\<bar>^n / fact (Suc n)) * expectation (\<lambda>x. min (2 * \<bar>x\<bar>^n * Suc n) (\<bar>t\<bar> * \<bar>x\<bar>^Suc n))"
+    unfolding *
+  proof (rule integral_mult_right)
+    show "integrable M (\<lambda>x. min (2 * \<bar>x\<bar> ^ n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar> ^ Suc n))"
+      by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"])
+         (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
+  qed
+  finally show ?thesis
+    unfolding integral_mult_right_zero .
+qed
+
+lemma (in real_distribution) char_approx3:
+  fixes t
+  assumes
+    integrable_1: "integrable M (\<lambda>x. x)" and
+    integral_1: "expectation (\<lambda>x. x) = 0" and
+    integrable_2: "integrable M (\<lambda>x. x^2)" and
+    integral_2: "variance (\<lambda>x. x) = \<sigma>2"
+  shows "cmod (char M t - (1 - t^2 * \<sigma>2 / 2)) \<le>
+    (t^2 / 6) * expectation (\<lambda>x. min (6 * x^2) (abs t * (abs x)^3) )"
+proof -
+  note real_distribution.char_approx2 [of M 2 t, simplified]
+  have [simp]: "prob UNIV = 1" by (metis prob_space space_eq_univ)
+  from integral_2 have [simp]: "expectation (\<lambda>x. x * x) = \<sigma>2" 
+    by (simp add: integral_1 numeral_eq_Suc)
+  have 1: "k \<le> 2 \<Longrightarrow> integrable M (\<lambda>x. x^k)" for k 
+    using assms by (auto simp: eval_nat_numeral le_Suc_eq)
+  note char_approx1
+  note 2 = char_approx1 [of 2 t, OF 1, simplified]
+  have "cmod (char M t - (\<Sum>k\<le>2. (\<i> * t) ^ k * (expectation (\<lambda>x. x ^ k)) / (fact k))) \<le>
+      t\<^sup>2 * expectation (\<lambda>x. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3)) / fact (3::nat)"
+    using char_approx2 [of 2 t, OF 1] by simp
+  also have "(\<Sum>k\<le>2. (\<i> * t) ^ k * expectation (\<lambda>x. x ^ k) / (fact k)) = 1 - t^2 * \<sigma>2 / 2"
+    by (simp add: complex_eq_iff numeral_eq_Suc integral_1 Re_divide Im_divide)
+  also have "fact 3 = 6" by (simp add: eval_nat_numeral)
+  also have "t\<^sup>2 * expectation (\<lambda>x. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3)) / 6 =
+     t\<^sup>2 / 6 * expectation (\<lambda>x. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3))" by (simp add: field_simps)
+  finally show ?thesis .
+qed
+
+text \<open>
+  This is a more familiar textbook formulation in terms of random variables, but 
+  we will use the previous version for the CLT.
+\<close>
+
+lemma (in prob_space) char_approx3':
+  fixes \<mu> :: "real measure" and X
+  assumes rv_X [simp]: "random_variable borel X"
+    and [simp]: "integrable M X" "integrable M (\<lambda>x. (X x)^2)" "expectation X = 0"
+    and var_X: "variance X = \<sigma>2"
+    and \<mu>_def: "\<mu> = distr M borel X"
+  shows "cmod (char \<mu> t - (1 - t^2 * \<sigma>2 / 2)) \<le>
+    (t^2 / 6) * expectation (\<lambda>x. min (6 * (X x)^2) (\<bar>t\<bar> * \<bar>X x\<bar>^3))"
+  using var_X unfolding \<mu>_def
+  apply (subst integral_distr [symmetric, OF rv_X], simp)
+  apply (intro real_distribution.char_approx3)
+  apply (auto simp add: integrable_distr_eq integral_distr)
+  done
+
+text \<open>
+  this is the formulation in the book -- in terms of a random variable *with* the distribution,
+  rather the distribution itself. I don't know which is more useful, though in principal we can
+  go back and forth between them.
+\<close>
+
+lemma (in prob_space) char_approx1':
+  fixes \<mu> :: "real measure" and X
+  assumes integrable_moments : "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. X x ^ k)"
+    and rv_X[measurable]: "random_variable borel X"
+    and \<mu>_distr : "distr M borel X = \<mu>"
+  shows "cmod (char \<mu> t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. (X x)^k))) \<le>
+    (2 * \<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>X x\<bar>^n)"
+  unfolding \<mu>_distr[symmetric]
+  apply (subst (1 2) integral_distr [symmetric, OF rv_X], simp, simp)
+  apply (intro real_distribution.char_approx1[of "distr M borel X" n t] real_distribution_distr rv_X)
+  apply (auto simp: integrable_distr_eq integrable_moments)
+  done
+
+subsection \<open>Calculation of the Characteristic Function of the Standard Distribution\<close>
+
+abbreviation
+  "std_normal_distribution \<equiv> density lborel std_normal_density"
+
+(* TODO: should this be an instance statement? *)
+lemma real_dist_normal_dist: "real_distribution std_normal_distribution"
+  using prob_space_normal_density by (auto simp: real_distribution_def real_distribution_axioms_def)
+
+lemma std_normal_distribution_even_moments:
+  fixes k :: nat
+  shows "(LINT x|std_normal_distribution. x^(2 * k)) = fact (2 * k) / (2^k * fact k)"
+    and "integrable std_normal_distribution (\<lambda>x. x^(2 * k))"
+  using integral_std_normal_moment_even[of k]
+  by (subst integral_density)
+     (auto simp: normal_density_nonneg integrable_density
+           intro: integrable.intros std_normal_moment_even)
+
+lemma integrable_std_normal_distribution_moment: "integrable std_normal_distribution (\<lambda>x. x^k)"
+  by (auto simp: normal_density_nonneg integrable_std_normal_moment integrable_density)
+
+lemma integral_std_normal_distribution_moment_odd:
+  "odd k \<Longrightarrow> integral\<^sup>L std_normal_distribution (\<lambda>x. x^k) = 0"
+  using integral_std_normal_moment_odd[of "(k - 1) div 2"]
+  by (auto simp: integral_density normal_density_nonneg elim: oddE)
+
+lemma std_normal_distribution_even_moments_abs:
+  fixes k :: nat
+  shows "(LINT x|std_normal_distribution. \<bar>x\<bar>^(2 * k)) = fact (2 * k) / (2^k * fact k)"
+  using integral_std_normal_moment_even[of k]
+  by (subst integral_density) (auto simp: normal_density_nonneg power_even_abs)
+
+lemma std_normal_distribution_odd_moments_abs:
+  fixes k :: nat
+  shows "(LINT x|std_normal_distribution. \<bar>x\<bar>^(2 * k + 1)) = sqrt (2 / pi) * 2 ^ k * fact k"
+  using integral_std_normal_moment_abs_odd[of k]
+  by (subst integral_density) (auto simp: normal_density_nonneg)
+
+theorem char_std_normal_distribution:
+  "char std_normal_distribution = (\<lambda>t. complex_of_real (exp (- (t^2) / 2)))"
+proof (intro ext LIMSEQ_unique)
+  fix t :: real
+  let ?f' = "\<lambda>k. (ii * t)^k / fact k * (LINT x | std_normal_distribution. x^k)"
+  let ?f = "\<lambda>n. (\<Sum>k \<le> n. ?f' k)"
+  show "?f \<longlonglongrightarrow> exp (-(t^2) / 2)"
+  proof (rule limseq_even_odd)
+    have "(\<i> * complex_of_real t) ^ (2 * a) / (2 ^ a * fact a) = (- ((complex_of_real t)\<^sup>2 / 2)) ^ a / fact a" for a
+      by (subst power_mult) (simp add: field_simps uminus_power_if power_mult)
+    then have *: "?f (2 * n) = complex_of_real (\<Sum>k < Suc n. (1 / fact k) * (- (t^2) / 2)^k)" for n :: nat
+      unfolding of_real_setsum
+      by (intro setsum.reindex_bij_witness_not_neutral[symmetric, where
+           i="\<lambda>n. n div 2" and j="\<lambda>n. 2 * n" and T'="{i. i \<le> 2 * n \<and> odd i}" and S'="{}"])
+         (auto simp: integral_std_normal_distribution_moment_odd std_normal_distribution_even_moments)
+    show "(\<lambda>n. ?f (2 * n)) \<longlonglongrightarrow> exp (-(t^2) / 2)"
+      unfolding * using exp_converges[where 'a=real]
+      by (intro tendsto_of_real LIMSEQ_Suc) (auto simp: inverse_eq_divide sums_def [symmetric])
+    have **: "?f (2 * n + 1) = ?f (2 * n)" for n
+    proof -
+      have "?f (2 * n + 1) = ?f (2 * n) + ?f' (2 * n + 1)"
+        by simp
+      also have "?f' (2 * n + 1) = 0"
+        by (subst integral_std_normal_distribution_moment_odd) simp_all
+      finally show "?f (2 * n + 1) = ?f (2 * n)"
+        by simp
+    qed
+    show "(\<lambda>n. ?f (2 * n + 1)) \<longlonglongrightarrow> exp (-(t^2) / 2)"
+      unfolding ** by fact
+  qed
+
+  have **: "(\<lambda>n. x ^ n / fact n) \<longlonglongrightarrow> 0" for x :: real
+    using summable_LIMSEQ_zero [OF summable_exp] by (auto simp add: inverse_eq_divide)
+
+  let ?F = "\<lambda>n. 2 * \<bar>t\<bar> ^ n / fact n * (LINT x|std_normal_distribution. \<bar>x\<bar> ^ n)"
+
+  show "?f \<longlonglongrightarrow> char std_normal_distribution t"
+  proof (rule metric_tendsto_imp_tendsto[OF limseq_even_odd])
+    show "(\<lambda>n. ?F (2 * n)) \<longlonglongrightarrow> 0"
+    proof (rule Lim_transform_eventually)
+      show "\<forall>\<^sub>F n in sequentially. 2 * ((t^2 / 2)^n / fact n) = ?F (2 * n)"
+        unfolding std_normal_distribution_even_moments_abs by (simp add: power_mult power_divide)
+    qed (intro tendsto_mult_right_zero **)
+
+    have *: "?F (2 * n + 1) = (2 * \<bar>t\<bar> * sqrt (2 / pi)) * ((2 * t^2)^n * fact n / fact (2 * n + 1))" for n
+      unfolding std_normal_distribution_odd_moments_abs
+      by (simp add: field_simps power_mult[symmetric] power_even_abs)
+    have "norm ((2 * t\<^sup>2) ^ n * fact n / fact (2 * n + 1)) \<le> (2 * t\<^sup>2) ^ n / fact n" for n
+      using mult_mono[OF _ square_fact_le_2_fact, of 1 "1 + 2 * real n" n]
+      by (auto simp add: divide_simps intro!: mult_left_mono)
+    then show "(\<lambda>n. ?F (2 * n + 1)) \<longlonglongrightarrow> 0"
+      unfolding * by (intro tendsto_mult_right_zero Lim_null_comparison [OF _ ** [of "2 * t\<^sup>2"]]) auto
+
+    show "\<forall>\<^sub>F n in sequentially. dist (?f n) (char std_normal_distribution t) \<le> dist (?F n) 0"
+      using real_distribution.char_approx1[OF real_dist_normal_dist integrable_std_normal_distribution_moment]
+      by (auto simp: dist_norm integral_nonneg_AE norm_minus_commute)
+  qed
+qed
+
+end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Distribution_Functions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Distribution_Functions.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -0,0 +1,259 @@
+(*
+  Title    : Distribution_Functions.thy
+  Authors  : Jeremy Avigad and Luke Serafin
+*)
+
+section \<open>Distribution Functions\<close>
+
+text \<open>
+Shows that the cumulative distribution function (cdf) of a distribution (a measure on the reals) is 
+nondecreasing and right continuous, which tends to 0 and 1 in either direction.
+
+Conversely, every such function is the cdf of a unique distribution. This direction defines the 
+measure in the obvious way on half-open intervals, and then applies the Caratheodory extension 
+theorem.
+\<close>
+
+(* TODO: the locales "finite_borel_measure" and "real_distribution" are defined here, but maybe they
+ should be somewhere else. *)
+
+theory Distribution_Functions
+  imports Probability_Measure "~~/src/HOL/Library/ContNotDenum"
+begin
+
+lemma UN_Ioc_eq_UNIV: "(\<Union>n. { -real n <.. real n}) = UNIV"
+  by auto
+     (metis le_less_trans minus_minus neg_less_iff_less not_le real_arch_simple
+            of_nat_0_le_iff reals_Archimedean2)
+
+subsection {* Properties of cdf's *}
+
+definition
+  cdf :: "real measure \<Rightarrow> real \<Rightarrow> real"
+where
+  "cdf M \<equiv> \<lambda>x. measure M {..x}"
+
+lemma cdf_def2: "cdf M x = measure M {..x}"
+  by (simp add: cdf_def)
+
+locale finite_borel_measure = finite_measure M for M :: "real measure" +
+  assumes M_super_borel: "sets borel \<subseteq> sets M"
+begin
+
+lemma sets_M[intro]: "a \<in> sets borel \<Longrightarrow> a \<in> sets M"
+  using M_super_borel by auto
+
+lemma cdf_diff_eq: 
+  assumes "x < y"
+  shows "cdf M y - cdf M x = measure M {x<..y}"
+proof -
+  from assms have *: "{..x} \<union> {x<..y} = {..y}" by auto
+  have "measure M {..y} = measure M {..x} + measure M {x<..y}"
+    by (subst finite_measure_Union [symmetric], auto simp add: *)
+  thus ?thesis
+    unfolding cdf_def by auto
+qed
+
+lemma cdf_nondecreasing: "x \<le> y \<Longrightarrow> cdf M x \<le> cdf M y"
+  unfolding cdf_def by (auto intro!: finite_measure_mono)
+
+lemma borel_UNIV: "space M = UNIV"
+ by (metis in_mono sets.sets_into_space space_in_borel top_le M_super_borel)
+ 
+lemma cdf_nonneg: "cdf M x \<ge> 0"
+  unfolding cdf_def by (rule measure_nonneg)
+
+lemma cdf_bounded: "cdf M x \<le> measure M (space M)"
+  unfolding cdf_def using assms by (intro bounded_measure)
+
+lemma cdf_lim_infty:
+  "((\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> measure M (space M))"
+proof -
+  have "(\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> measure M (\<Union> i::nat. {..real i})"
+    unfolding cdf_def by (rule finite_Lim_measure_incseq) (auto simp: incseq_def)
+  also have "(\<Union> i::nat. {..real i}) = space M"
+    by (auto simp: borel_UNIV intro: real_arch_simple)
+  finally show ?thesis .
+qed
+
+lemma cdf_lim_at_top: "(cdf M \<longlongrightarrow> measure M (space M)) at_top" 
+  by (rule tendsto_at_topI_sequentially_real)
+     (simp_all add: mono_def cdf_nondecreasing cdf_lim_infty)
+
+lemma cdf_lim_neg_infty: "((\<lambda>i. cdf M (- real i)) \<longlonglongrightarrow> 0)" 
+proof -
+  have "(\<lambda>i. cdf M (- real i)) \<longlonglongrightarrow> measure M (\<Inter> i::nat. {.. - real i })"
+    unfolding cdf_def by (rule finite_Lim_measure_decseq) (auto simp: decseq_def)
+  also have "(\<Inter> i::nat. {..- real i}) = {}"
+    by auto (metis leD le_minus_iff reals_Archimedean2)
+  finally show ?thesis
+    by simp
+qed
+
+lemma cdf_lim_at_bot: "(cdf M \<longlongrightarrow> 0) at_bot"
+proof - 
+  have *: "((\<lambda>x :: real. - cdf M (- x)) \<longlongrightarrow> 0) at_top"
+    by (intro tendsto_at_topI_sequentially_real monoI)
+       (auto simp: cdf_nondecreasing cdf_lim_neg_infty tendsto_minus_cancel_left[symmetric])
+  from filterlim_compose [OF *, OF filterlim_uminus_at_top_at_bot]
+  show ?thesis
+    unfolding tendsto_minus_cancel_left[symmetric] by simp
+qed
+
+lemma cdf_is_right_cont: "continuous (at_right a) (cdf M)"
+  unfolding continuous_within
+proof (rule tendsto_at_right_sequentially[where b="a + 1"])
+  fix f :: "nat \<Rightarrow> real" and x assume f: "decseq f" "f \<longlonglongrightarrow> a"
+  then have "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> measure M (\<Inter>i. {.. f i})"
+    using `decseq f` unfolding cdf_def 
+    by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
+  also have "(\<Inter>i. {.. f i}) = {.. a}"
+    using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
+  finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
+    by (simp add: cdf_def)
+qed simp
+
+lemma cdf_at_left: "(cdf M \<longlongrightarrow> measure M {..<a}) (at_left a)"
+proof (rule tendsto_at_left_sequentially[of "a - 1"])
+  fix f :: "nat \<Rightarrow> real" and x assume f: "incseq f" "f \<longlonglongrightarrow> a" "\<And>x. f x < a" "\<And>x. a - 1 < f x"
+  then have "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> measure M (\<Union>i. {.. f i})"
+    using `incseq f` unfolding cdf_def 
+    by (intro finite_Lim_measure_incseq) (auto simp: incseq_def)
+  also have "(\<Union>i. {.. f i}) = {..<a}"
+    by (auto dest!: order_tendstoD(1)[OF f(2)] eventually_happens'[OF sequentially_bot]
+             intro: less_imp_le le_less_trans f(3))
+  finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> measure M {..<a}"
+    by (simp add: cdf_def)
+qed auto
+
+lemma isCont_cdf: "isCont (cdf M) x \<longleftrightarrow> measure M {x} = 0"
+proof -
+  have "isCont (cdf M) x \<longleftrightarrow> cdf M x = measure M {..<x}"
+    by (auto simp: continuous_at_split cdf_is_right_cont continuous_within[where s="{..< _}"]
+                   cdf_at_left tendsto_unique[OF _ cdf_at_left])
+  also have "cdf M x = measure M {..<x} \<longleftrightarrow> measure M {x} = 0"
+    unfolding cdf_def ivl_disj_un(2)[symmetric]
+    by (subst finite_measure_Union) auto
+  finally show ?thesis .
+qed
+
+lemma countable_atoms: "countable {x. measure M {x} > 0}"
+  using countable_support unfolding zero_less_measure_iff .
+    
+end
+
+locale real_distribution = prob_space M for M :: "real measure" +
+  assumes events_eq_borel [simp, measurable_cong]: "sets M = sets borel" and space_eq_univ [simp]: "space M = UNIV"
+begin
+
+sublocale finite_borel_measure M
+  by standard auto
+
+lemma cdf_bounded_prob: "\<And>x. cdf M x \<le> 1"
+  by (subst prob_space [symmetric], rule cdf_bounded)
+
+lemma cdf_lim_infty_prob: "(\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> 1"
+  by (subst prob_space [symmetric], rule cdf_lim_infty)
+
+lemma cdf_lim_at_top_prob: "(cdf M \<longlongrightarrow> 1) at_top" 
+  by (subst prob_space [symmetric], rule cdf_lim_at_top)
+
+lemma measurable_finite_borel [simp]:
+  "f \<in> borel_measurable borel \<Longrightarrow> f \<in> borel_measurable M"
+  by (rule borel_measurable_subalgebra[where N=borel]) auto
+
+end
+
+lemma (in prob_space) real_distribution_distr [intro, simp]:
+  "random_variable borel X \<Longrightarrow> real_distribution (distr M borel X)"
+  unfolding real_distribution_def real_distribution_axioms_def by (auto intro!: prob_space_distr)
+
+subsection {* uniqueness *}
+
+lemma (in real_distribution) emeasure_Ioc:
+  assumes "a \<le> b" shows "emeasure M {a <.. b} = cdf M b - cdf M a"
+proof -
+  have "{a <.. b} = {..b} - {..a}"
+    by auto
+  with `a \<le> b` show ?thesis
+    by (simp add: emeasure_eq_measure finite_measure_Diff cdf_def)
+qed
+
+lemma cdf_unique:
+  fixes M1 M2
+  assumes "real_distribution M1" and "real_distribution M2"
+  assumes "cdf M1 = cdf M2"
+  shows "M1 = M2"
+proof (rule measure_eqI_generator_eq[where \<Omega>=UNIV])
+  fix X assume "X \<in> range (\<lambda>(a, b). {a<..b::real})"
+  then obtain a b where Xeq: "X = {a<..b}" by auto
+  then show "emeasure M1 X = emeasure M2 X"
+    by (cases "a \<le> b")
+       (simp_all add: assms(1,2)[THEN real_distribution.emeasure_Ioc] assms(3))
+next
+  show "(\<Union>i. {- real (i::nat)<..real i}) = UNIV"
+    by (rule UN_Ioc_eq_UNIV)
+qed (auto simp: real_distribution.emeasure_Ioc[OF assms(1)]
+  assms(1,2)[THEN real_distribution.events_eq_borel] borel_sigma_sets_Ioc
+  Int_stable_def)
+
+lemma real_distribution_interval_measure:
+  fixes F :: "real \<Rightarrow> real"
+  assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y" and
+    right_cont_F : "\<And>a. continuous (at_right a) F" and 
+    lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot" and
+    lim_F_at_top : "(F \<longlongrightarrow> 1) at_top"
+  shows "real_distribution (interval_measure F)"
+proof -
+  let ?F = "interval_measure F"
+  interpret prob_space ?F
+  proof
+    have "ereal (1 - 0) = (SUP i::nat. ereal (F (real i) - F (- real i)))"
+      by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] lim_ereal[THEN iffD2] tendsto_intros
+         lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
+         lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
+         filterlim_uminus_at_top[THEN iffD1])
+         (auto simp: incseq_def intro!: diff_mono nondecF)
+    also have "\<dots> = (SUP i::nat. emeasure ?F {- real i<..real i})"
+      by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
+    also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
+      by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
+    also have "(\<Union>i. {- real (i::nat)<..real i}) = space ?F"
+      by (simp add: UN_Ioc_eq_UNIV)
+    finally show "emeasure ?F (space ?F) = 1"
+      by (simp add: one_ereal_def)
+  qed
+  show ?thesis
+    proof qed simp_all
+qed
+
+lemma cdf_interval_measure:
+  fixes F :: "real \<Rightarrow> real"
+  assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y" and
+    right_cont_F : "\<And>a. continuous (at_right a) F" and 
+    lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot" and
+    lim_F_at_top : "(F \<longlongrightarrow> 1) at_top"
+  shows "cdf (interval_measure F) = F"
+  unfolding cdf_def
+proof (intro ext)
+  interpret real_distribution "interval_measure F"
+    by (rule real_distribution_interval_measure) fact+
+  fix x
+  have "F x - 0 = measure (interval_measure F) (\<Union>i::nat. {-real i <.. x})"
+  proof (intro LIMSEQ_unique[OF _ finite_Lim_measure_incseq])
+    have "(\<lambda>i. F x - F (- real i)) \<longlonglongrightarrow> F x - 0"
+      by (intro tendsto_intros lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
+                filterlim_uminus_at_top[THEN iffD1])
+    then show "(\<lambda>i. measure (interval_measure F) {- real i<..x}) \<longlonglongrightarrow> F x - 0"
+      apply (rule filterlim_cong[OF refl refl, THEN iffD1, rotated])
+      apply (rule eventually_sequentiallyI[where c="nat (ceiling (- x))"])
+      apply (simp add: measure_interval_measure_Ioc right_cont_F nondecF)
+      done
+  qed (auto simp: incseq_def)
+  also have "(\<Union>i::nat. {-real i <.. x}) = {..x}"
+    by auto (metis minus_minus neg_less_iff_less reals_Archimedean2)
+  finally show "measure (interval_measure F) {..x} = F x"
+    by simp
+qed
+
+end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Helly_Selection.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Helly_Selection.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -0,0 +1,297 @@
+(*
+  Theory: Helly_Selection.thy
+  Authors: Jeremy Avigad, Luke Serafin
+*)
+
+section \<open>Helly's selection theorem\<close>
+
+text \<open>The set of bounded, monotone, right continuous functions is sequentially compact\<close>
+
+theory Helly_Selection
+  imports "~~/src/HOL/Library/Diagonal_Subsequence" Weak_Convergence
+begin
+
+lemma minus_one_less: "x - 1 < (x::real)"
+  by simp
+
+theorem Helly_selection:
+  fixes f :: "nat \<Rightarrow> real \<Rightarrow> real"
+  assumes rcont: "\<And>n x. continuous (at_right x) (f n)"
+  assumes mono: "\<And>n. mono (f n)"
+  assumes bdd: "\<And>n x. \<bar>f n x\<bar> \<le> M"
+  shows "\<exists>s. subseq s \<and> (\<exists>F. (\<forall>x. continuous (at_right x) F) \<and> mono F \<and> (\<forall>x. \<bar>F x\<bar> \<le> M) \<and>
+    (\<forall>x. continuous (at x) F \<longrightarrow> (\<lambda>n. f (s n) x) \<longlonglongrightarrow> F x))"
+proof -
+  obtain m :: "real \<Rightarrow> nat" where "bij_betw m \<rat> UNIV"
+    using countable_rat Rats_infinite by (erule countableE_infinite)
+  then obtain r :: "nat \<Rightarrow> real" where bij: "bij_betw r UNIV \<rat>"
+    using bij_betw_inv by blast
+
+  have dense_r: "\<And>x y. x < y \<Longrightarrow> \<exists>n. x < r n \<and> r n < y"
+    by (metis Rats_dense_in_real bij f_the_inv_into_f bij_betw_def)
+
+  let ?P = "\<lambda>n. \<lambda>s. convergent (\<lambda>k. f (s k) (r n))"
+  interpret nat: subseqs ?P
+  proof (unfold convergent_def, unfold subseqs_def, auto)
+    fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "subseq s"
+    have "bounded {-M..M}"
+      using bounded_closed_interval by auto
+    moreover have "\<And>k. f (s k) (r n) \<in> {-M..M}" 
+      using bdd by (simp add: abs_le_iff minus_le_iff)
+    ultimately have "\<exists>l s'. subseq s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
+      using compact_Icc compact_imp_seq_compact seq_compactE by metis
+    thus "\<exists>s'. subseq s' \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)"
+      by (auto simp: comp_def)
+  qed
+  def d \<equiv> "nat.diagseq"
+  have subseq: "subseq d"
+    unfolding d_def using nat.subseq_diagseq by auto
+  have rat_cnv: "?P n d" for n
+  proof -
+    have Pn_seqseq: "?P n (nat.seqseq (Suc n))"
+      by (rule nat.seqseq_holds)
+    have 1: "(\<lambda>k. f ((nat.seqseq (Suc n) \<circ> (\<lambda>k. nat.fold_reduce (Suc n) k
+      (Suc n + k))) k) (r n)) = (\<lambda>k. f (nat.seqseq (Suc n) k) (r n)) \<circ>
+      (\<lambda>k. nat.fold_reduce (Suc n) k (Suc n + k))"
+      by auto
+    have 2: "?P n (d \<circ> (op + (Suc n)))"
+      unfolding d_def nat.diagseq_seqseq 1
+      by (intro convergent_subseq_convergent Pn_seqseq nat.subseq_diagonal_rest)
+    then obtain L where 3: "(\<lambda>na. f (d (na + Suc n)) (r n)) \<longlonglongrightarrow> L"
+      by (auto simp: add.commute dest: convergentD)
+    then have "(\<lambda>k. f (d k) (r n)) \<longlonglongrightarrow> L"
+      by (rule LIMSEQ_offset)
+    then show ?thesis
+      by (auto simp: convergent_def)
+  qed
+  let ?f = "\<lambda>n. \<lambda>k. f (d k) (r n)"
+  have lim_f: "?f n \<longlonglongrightarrow> lim (?f n)" for n
+    using rat_cnv convergent_LIMSEQ_iff by auto
+  have lim_bdd: "lim (?f n) \<in> {-M..M}" for n
+  proof -
+    have "closed {-M..M}" using closed_real_atLeastAtMost by auto
+    hence "(\<forall>i. ?f n i \<in> {-M..M}) \<and> ?f n \<longlonglongrightarrow> lim (?f n) \<longrightarrow> lim (?f n) \<in> {-M..M}"
+      unfolding closed_sequential_limits by (drule_tac x = "\<lambda>k. f (d k) (r n)" in spec) blast
+    moreover have "\<forall>i. ?f n i \<in> {-M..M}"
+      using bdd by (simp add: abs_le_iff minus_le_iff)
+    ultimately show "lim (?f n) \<in> {-M..M}"
+      using lim_f by auto
+  qed
+  then have limset_bdd: "\<And>x. {lim (?f n) |n. x < r n} \<subseteq> {-M..M}"
+    by auto
+  then have bdd_below: "bdd_below {lim (?f n) |n. x < r n}" for x
+    by (metis (mono_tags) bdd_below_Icc bdd_below_mono)
+  have r_unbdd: "\<exists>n. x < r n" for x
+    using dense_r[OF less_add_one, of x] by auto
+  then have nonempty: "{lim (?f n) |n. x < r n} \<noteq> {}" for x
+    by auto
+
+  def F \<equiv> "\<lambda>x. Inf {lim (?f n) |n. x < r n}"
+  have F_eq: "ereal (F x) = (INF n:{n. x < r n}. ereal (lim (?f n)))" for x
+    unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image)
+  have mono_F: "mono F"
+    using nonempty by (auto intro!: cInf_superset_mono simp: F_def bdd_below mono_def)
+  moreover have "\<And>x. continuous (at_right x) F"
+    unfolding continuous_within order_tendsto_iff eventually_at_right[OF less_add_one]
+  proof safe
+    show "F x < u \<Longrightarrow> \<exists>b>x. \<forall>y>x. y < b \<longrightarrow> F y < u" for x u
+      unfolding F_def cInf_less_iff[OF nonempty bdd_below] by auto
+  next
+    show "\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> l < F y" if l: "l < F x" for x l
+      using less_le_trans[OF l mono_F[THEN monoD, of x]] by (auto intro: less_add_one)
+  qed
+  moreover
+  { fix x
+    have "F x \<in> {-M..M}"
+      unfolding F_def using limset_bdd bdd_below r_unbdd by (intro closed_subset_contains_Inf) auto
+    then have "\<bar>F x\<bar> \<le> M" by auto }
+  moreover have "(\<lambda>n. f (d n) x) \<longlonglongrightarrow> F x" if cts: "continuous (at x) F" for x
+  proof (rule limsup_le_liminf_real)
+    show "limsup (\<lambda>n. f (d n) x) \<le> F x"
+    proof (rule tendsto_le_const)
+      show "(F \<longlongrightarrow> ereal (F x)) (at_right x)"
+        using cts unfolding continuous_at_split by (auto simp: continuous_within)
+      show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>n. f (d n) x) \<le> F i"
+        unfolding eventually_at_right[OF less_add_one]
+      proof (rule, rule, rule less_add_one, safe)
+        fix y assume y: "x < y"
+        with dense_r obtain N where "x < r N" "r N < y" by auto
+        have *: "y < r n' \<Longrightarrow> lim (?f N) \<le> lim (?f n')" for n'
+          using \<open>r N < y\<close> by (intro LIMSEQ_le[OF lim_f lim_f]) (auto intro!: mono[THEN monoD])
+        have "limsup (\<lambda>n. f (d n) x) \<le> limsup (?f N)"
+          using \<open>x < r N\<close> by (auto intro!: Limsup_mono always_eventually mono[THEN monoD])
+        also have "\<dots> = lim (\<lambda>n. ereal (?f N n))"
+          using rat_cnv[of N] by (force intro!: convergent_limsup_cl simp: convergent_def)
+        also have "\<dots> \<le> F y"
+          by (auto intro!: INF_greatest * simp: convergent_real_imp_convergent_ereal rat_cnv F_eq)
+        finally show "limsup (\<lambda>n. f (d n) x) \<le> F y" .
+      qed
+    qed simp
+    show "F x \<le> liminf (\<lambda>n. f (d n) x)"
+    proof (rule tendsto_ge_const)
+      show "(F \<longlongrightarrow> ereal (F x)) (at_left x)"
+        using cts unfolding continuous_at_split by (auto simp: continuous_within)
+      show "\<forall>\<^sub>F i in at_left x. F i \<le> liminf (\<lambda>n. f (d n) x)"
+        unfolding eventually_at_left[OF minus_one_less]
+      proof (rule, rule, rule minus_one_less, safe)
+        fix y assume y: "y < x"
+        with dense_r obtain N where "y < r N" "r N < x" by auto
+        have "F y \<le> liminf (?f N)"
+          using \<open>y < r N\<close> by (auto simp: F_eq convergent_real_imp_convergent_ereal
+            rat_cnv convergent_liminf_cl intro!: INF_lower2)
+        also have "\<dots> \<le> liminf (\<lambda>n. f (d n) x)"
+          using \<open>r N < x\<close> by (auto intro!: Liminf_mono monoD[OF mono] always_eventually)
+        finally show "F y \<le> liminf (\<lambda>n. f (d n) x)" .
+      qed
+    qed simp
+  qed
+  ultimately show ?thesis using subseq by auto
+qed
+
+(** Weak convergence corollaries to Helly's theorem. **)
+
+definition
+  tight :: "(nat \<Rightarrow> real measure) \<Rightarrow> bool"
+where
+  "tight \<mu> \<equiv> (\<forall>n. real_distribution (\<mu> n)) \<and> (\<forall>(\<epsilon>::real)>0. \<exists>a b::real. a < b \<and> (\<forall>n. measure (\<mu> n) {a<..b} > 1 - \<epsilon>))"
+
+(* Can strengthen to equivalence. *)
+theorem tight_imp_convergent_subsubsequence:
+  assumes \<mu>: "tight \<mu>" "subseq s"
+  shows "\<exists>r M. subseq r \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M"
+proof -
+  def f \<equiv> "\<lambda>k. cdf (\<mu> (s k))"
+  interpret \<mu>: real_distribution "\<mu> k" for k
+    using \<mu> unfolding tight_def by auto
+
+  have rcont: "\<And>x. continuous (at_right x) (f k)"
+    and mono: "mono (f k)"
+    and top: "(f k \<longlongrightarrow> 1) at_top"
+    and bot: "(f k \<longlongrightarrow> 0) at_bot" for k
+    unfolding f_def mono_def
+    using \<mu>.cdf_nondecreasing \<mu>.cdf_is_right_cont \<mu>.cdf_lim_at_top_prob \<mu>.cdf_lim_at_bot by auto
+  have bdd: "\<bar>f k x\<bar> \<le> 1" for k x
+    by (auto simp add: abs_le_iff minus_le_iff f_def \<mu>.cdf_nonneg \<mu>.cdf_bounded_prob)
+
+  from Helly_selection[OF rcont mono bdd, of "\<lambda>x. x"] obtain r F
+    where F: "subseq r" "\<And>x. continuous (at_right x) F" "mono F" "\<And>x. \<bar>F x\<bar> \<le> 1"
+    and lim_F: "\<And>x. continuous (at x) F \<Longrightarrow> (\<lambda>n. f (r n) x) \<longlonglongrightarrow> F x"
+    by blast
+
+  have "0 \<le> f n x" for n x
+    unfolding f_def by (rule \<mu>.cdf_nonneg)
+  have F_nonneg: "0 \<le> F x" for x
+  proof -
+    obtain y where "y < x" "isCont F y"
+      using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{..< x}"] by auto
+    then have "0 \<le> F y"
+      by (intro LIMSEQ_le_const[OF lim_F]) (auto simp: f_def \<mu>.cdf_nonneg)
+    also have "\<dots> \<le> F x"
+      using \<open>y < x\<close> by (auto intro!: monoD[OF \<open>mono F\<close>])
+    finally show "0 \<le> F x" .
+  qed
+
+  have Fab: "\<exists>a b. (\<forall>x\<ge>b. F x \<ge> 1 - \<epsilon>) \<and> (\<forall>x\<le>a. F x \<le> \<epsilon>)" if \<epsilon>: "0 < \<epsilon>" for \<epsilon>
+  proof auto
+    obtain a' b' where a'b': "a' < b'" "\<And>k. measure (\<mu> k) {a'<..b'} > 1 - \<epsilon>"
+      using \<epsilon> \<mu> by (auto simp: tight_def)
+    obtain a where a: "a < a'" "isCont F a"
+      using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{..< a'}"] by auto
+    obtain b where b: "b' < b" "isCont F b"
+      using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{b' <..}"] by auto
+    have "a < b"
+      using a b a'b' by simp
+
+    let ?\<mu> = "\<lambda>k. measure (\<mu> (s (r k)))"
+    have ab: "?\<mu> k {a<..b} > 1 - \<epsilon>" for k
+    proof -
+      have "?\<mu> k {a'<..b'} \<le> ?\<mu> k {a<..b}"
+        using a b by (intro \<mu>.finite_measure_mono) auto
+      then show ?thesis
+        using a'b'(2) by (metis less_eq_real_def less_trans)
+    qed
+
+    have "(\<lambda>k. ?\<mu> k {..b}) \<longlonglongrightarrow> F b"
+      using b(2) lim_F unfolding f_def cdf_def o_def by auto
+    then have "1 - \<epsilon> \<le> F b"
+    proof (rule tendsto_le_const[OF sequentially_bot], intro always_eventually allI)
+      fix k
+      have "1 - \<epsilon> < ?\<mu> k {a<..b}"
+        using ab by auto
+      also have "\<dots> \<le> ?\<mu> k {..b}"
+        by (auto intro!: \<mu>.finite_measure_mono)
+      finally show "1 - \<epsilon> \<le> ?\<mu> k {..b}"
+        by (rule less_imp_le)
+    qed
+    then show "\<exists>b. \<forall>x\<ge>b. 1 - \<epsilon> \<le> F x"
+      using F unfolding mono_def by (metis order.trans)
+
+    have "(\<lambda>k. ?\<mu> k {..a}) \<longlonglongrightarrow> F a"
+      using a(2) lim_F unfolding f_def cdf_def o_def by auto
+    then have Fa: "F a \<le> \<epsilon>"
+    proof (rule tendsto_ge_const[OF sequentially_bot], intro always_eventually allI)
+      fix k
+      have "?\<mu> k {..a} + ?\<mu> k {a<..b} \<le> 1"
+        by (subst \<mu>.finite_measure_Union[symmetric]) auto
+      then show "?\<mu> k {..a} \<le> \<epsilon>"
+        using ab[of k] by simp
+    qed
+    then show "\<exists>a. \<forall>x\<le>a. F x \<le> \<epsilon>"
+      using F unfolding mono_def by (metis order.trans)
+  qed
+
+  have "(F \<longlongrightarrow> 1) at_top"
+  proof (rule order_tendstoI)
+    show "1 < y \<Longrightarrow> \<forall>\<^sub>F x in at_top. F x < y" for y
+      using \<open>\<And>x. \<bar>F x\<bar> \<le> 1\<close> \<open>\<And>x. 0 \<le> F x\<close> by (auto intro: le_less_trans always_eventually)
+    fix y :: real assume "y < 1"
+    then obtain z where "y < z" "z < 1"
+      using dense[of y 1] by auto
+    with Fab[of "1 - z"] show "\<forall>\<^sub>F x in at_top. y < F x"
+      by (auto simp: eventually_at_top_linorder intro: less_le_trans)
+  qed
+  moreover
+  have "(F \<longlongrightarrow> 0) at_bot"
+  proof (rule order_tendstoI)
+    show "y < 0 \<Longrightarrow> \<forall>\<^sub>F x in at_bot. y < F x" for y
+      using \<open>\<And>x. 0 \<le> F x\<close> by (auto intro: less_le_trans always_eventually)
+    fix y :: real assume "0 < y"
+    then obtain z where "0 < z" "z < y"
+      using dense[of 0 y] by auto
+    with Fab[of z] show "\<forall>\<^sub>F x in at_bot. F x < y"
+      by (auto simp: eventually_at_bot_linorder intro: le_less_trans)
+  qed
+  ultimately have M: "real_distribution (interval_measure F)" "cdf (interval_measure F) = F"
+    using F by (auto intro!: real_distribution_interval_measure cdf_interval_measure simp: mono_def)
+  with lim_F lim_subseq M have "weak_conv_m (\<mu> \<circ> s \<circ> r) (interval_measure F)"
+    by (auto simp: weak_conv_def weak_conv_m_def f_def comp_def)
+  then show "\<exists>r M. subseq r \<and> (real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M)"
+    using F M by auto
+qed
+
+corollary tight_subseq_weak_converge:
+  fixes \<mu> :: "nat \<Rightarrow> real measure" and M :: "real measure"
+  assumes "\<And>n. real_distribution (\<mu> n)" "real_distribution M" and tight: "tight \<mu>" and
+    subseq: "\<And>s \<nu>. subseq s \<Longrightarrow> real_distribution \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) M"
+  shows "weak_conv_m \<mu> M"
+proof (rule ccontr)
+  def f \<equiv> "\<lambda>n. cdf (\<mu> n)" and F \<equiv> "cdf M"
+
+  assume "\<not> weak_conv_m \<mu> M"
+  then obtain x where x: "isCont F x" "\<not> (\<lambda>n. f n x) \<longlonglongrightarrow> F x"
+    by (auto simp: weak_conv_m_def weak_conv_def f_def F_def)
+  then obtain \<epsilon> where "\<epsilon> > 0" and "infinite {n. \<not> dist (f n x) (F x) < \<epsilon>}"
+    by (auto simp: tendsto_iff not_eventually INFM_iff_infinite cofinite_eq_sequentially[symmetric])
+  then obtain s where s: "\<And>n. \<not> dist (f (s n) x) (F x) < \<epsilon>" and "subseq s"
+    using enumerate_in_set enumerate_mono by (fastforce simp: subseq_def)
+  then obtain r \<nu> where r: "subseq r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>"
+    using tight_imp_convergent_subsubsequence[OF tight] by blast
+  then have "weak_conv_m (\<mu> \<circ> (s \<circ> r)) M"
+    using \<open>subseq s\<close> r by (intro subseq subseq_o) (auto simp: comp_assoc)
+  then have "(\<lambda>n. f (s (r n)) x) \<longlonglongrightarrow> F x"
+    using x by (auto simp: weak_conv_m_def weak_conv_def F_def f_def)
+  then show False
+    using s \<open>\<epsilon> > 0\<close> by (auto dest: tendstoD)
+qed
+
+end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Interval_Integral.thy
--- a/src/HOL/Probability/Interval_Integral.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -190,6 +190,19 @@
     interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g"
   by (auto intro: set_lebesgue_integral_cong_AE simp: interval_lebesgue_integral_def)
 
+lemma interval_integrable_mirror:
+  shows "interval_lebesgue_integrable lborel a b (\<lambda>x. f (-x)) \<longleftrightarrow>
+    interval_lebesgue_integrable lborel (-b) (-a) f"
+proof -
+  have *: "indicator (einterval a b) (- x) = (indicator (einterval (-b) (-a)) x :: real)"
+    for a b :: ereal and x :: real
+    by (cases a b rule: ereal2_cases) (auto simp: einterval_def split: split_indicator)
+  show ?thesis
+    unfolding interval_lebesgue_integrable_def
+    using lborel_integrable_real_affine_iff[symmetric, of "-1" "\<lambda>x. indicator (einterval _ _) x *\<^sub>R f x" 0]
+    by (simp add: *)
+qed
+
 lemma interval_lebesgue_integral_add [intro, simp]: 
   fixes M a b f 
   assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g"
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -12,243 +12,6 @@
 imports Interval_Integral
 begin
 
-lemma measurable_sets_borel:
-    "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
-  by (drule (1) measurable_sets) simp
-
-lemma nn_integral_indicator_singleton[simp]:
-  assumes [measurable]: "{y} \<in> sets M"
-  shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
-proof-
-  have "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f y) * indicator {y} x \<partial>M)"
-    by (subst nn_integral_max_0[symmetric]) (auto intro!: nn_integral_cong split: split_indicator)
-  then show ?thesis
-    by (simp add: nn_integral_cmult)
-qed
-
-lemma nn_integral_set_ereal:
-  "(\<integral>\<^sup>+x. ereal (f x) * indicator A x \<partial>M) = (\<integral>\<^sup>+x. ereal (f x * indicator A x) \<partial>M)"
-  by (rule nn_integral_cong) (simp split: split_indicator)
-
-lemma nn_integral_indicator_singleton'[simp]:
-  assumes [measurable]: "{y} \<in> sets M"
-  shows "(\<integral>\<^sup>+x. ereal (f x * indicator {y} x) \<partial>M) = max 0 (f y) * emeasure M {y}"
-  by (subst nn_integral_set_ereal[symmetric]) simp
-
-lemma set_borel_measurable_sets:
-  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
-  assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
-  shows "f -` B \<inter> X \<in> sets M"
-proof -
-  have "f \<in> borel_measurable (restrict_space M X)"
-    using assms by (subst borel_measurable_restrict_space_iff) auto
-  then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
-    by (rule measurable_sets) fact
-  with \<open>X \<in> sets M\<close> show ?thesis
-    by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
-qed
-
-lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
-  assumes "A \<in> sets borel" 
-  assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
-          un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
-  shows "P (A::real set)"
-proof-
-  let ?G = "range (\<lambda>(a,b). {a..b::real})"
-  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" 
-      using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
-  thus ?thesis
-  proof (induction rule: sigma_sets_induct_disjoint) 
-    case (union f)
-      from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
-      with union show ?case by (auto intro: un)
-  next
-    case (basic A)
-    then obtain a b where "A = {a .. b}" by auto
-    then show ?case
-      by (cases "a \<le> b") (auto intro: int empty)
-  qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
-qed
-
-definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
-
-lemma mono_onI:
-  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A"
-  unfolding mono_on_def by simp
-
-lemma mono_onD:
-  "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
-  unfolding mono_on_def by simp
-
-lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
-  unfolding mono_def mono_on_def by auto
-
-lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
-  unfolding mono_on_def by auto
-
-definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s"
-
-lemma strict_mono_onI:
-  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A"
-  unfolding strict_mono_on_def by simp
-
-lemma strict_mono_onD:
-  "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
-  unfolding strict_mono_on_def by simp
-
-lemma mono_on_greaterD:
-  assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
-  shows "x > y"
-proof (rule ccontr)
-  assume "\<not>x > y"
-  hence "x \<le> y" by (simp add: not_less)
-  from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
-  with assms(4) show False by simp
-qed
-
-lemma strict_mono_inv:
-  fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
-  assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
-  shows "strict_mono g"
-proof
-  fix x y :: 'b assume "x < y"
-  from \<open>surj f\<close> obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
-  with \<open>x < y\<close> and \<open>strict_mono f\<close> have "x' < y'" by (simp add: strict_mono_less)
-  with inv show "g x < g y" by simp
-qed
-
-lemma strict_mono_on_imp_inj_on:
-  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
-  shows "inj_on f A"
-proof (rule inj_onI)
-  fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
-  thus "x = y"
-    by (cases x y rule: linorder_cases)
-       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 
-qed
-
-lemma strict_mono_on_leD:
-  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
-  shows "f x \<le> f y"
-proof (insert le_less_linear[of y x], elim disjE)
-  assume "x < y"
-  with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
-  thus ?thesis by (rule less_imp_le)
-qed (insert assms, simp)
-
-lemma strict_mono_on_eqD:
-  fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
-  assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
-  shows "y = x"
-  using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
-
-lemma mono_on_imp_deriv_nonneg:
-  assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
-  assumes "x \<in> interior A"
-  shows "D \<ge> 0"
-proof (rule tendsto_le_const)
-  let ?A' = "(\<lambda>y. y - x) ` interior A"
-  from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)"
-      by (simp add: field_has_derivative_at has_field_derivative_def)
-  from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset)
-
-  show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
-  proof (subst eventually_at_topological, intro exI conjI ballI impI)
-    have "open (interior A)" by simp
-    hence "open (op + (-x) ` interior A)" by (rule open_translation)
-    also have "(op + (-x) ` interior A) = ?A'" by auto
-    finally show "open ?A'" .
-  next
-    from \<open>x \<in> interior A\<close> show "0 \<in> ?A'" by auto
-  next
-    fix h assume "h \<in> ?A'"
-    hence "x + h \<in> interior A" by auto
-    with mono' and \<open>x \<in> interior A\<close> show "(f (x + h) - f x) / h \<ge> 0"
-      by (cases h rule: linorder_cases[of _ 0])
-         (simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps)
-  qed
-qed simp
-
-lemma strict_mono_on_imp_mono_on: 
-  "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
-  by (rule mono_onI, rule strict_mono_on_leD)
-
-lemma has_real_derivative_imp_continuous_on:
-  assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
-  shows "continuous_on A f"
-  apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
-  apply (intro ballI Deriv.differentiableI)
-  apply (rule has_field_derivative_subset[OF assms])
-  apply simp_all
-  done
-
-lemma closure_contains_Sup:
-  fixes S :: "real set"
-  assumes "S \<noteq> {}" "bdd_above S"
-  shows "Sup S \<in> closure S"
-proof-
-  have "Inf (uminus ` S) \<in> closure (uminus ` S)" 
-      using assms by (intro closure_contains_Inf) auto
-  also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
-  also have "closure (uminus ` S) = uminus ` closure S"
-      by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
-  finally show ?thesis by auto
-qed
-
-lemma closed_contains_Sup:
-  fixes S :: "real set"
-  shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
-  by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
-
-lemma deriv_nonneg_imp_mono:
-  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
-  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
-  assumes ab: "a \<le> b"
-  shows "g a \<le> g b"
-proof (cases "a < b")
-  assume "a < b"
-  from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
-  from MVT2[OF \<open>a < b\<close> this] and deriv 
-    obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
-  from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
-  with g_ab show ?thesis by simp
-qed (insert ab, simp)
-
-lemma continuous_interval_vimage_Int:
-  assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
-  assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}"
-  obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d"
-proof-
-    let ?A = "{a..b} \<inter> g -` {c..d}"
-    from IVT'[of g a c b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) 
-         obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto
-    from IVT'[of g a d b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) 
-         obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto
-    hence [simp]: "?A \<noteq> {}" by blast
-
-    def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A"
-    have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def
-        by (intro subsetI) (auto intro: cInf_lower cSup_upper)
-    moreover from assms have "closed ?A" 
-        using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
-    hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def
-        by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
-    hence "{c'..d'} \<subseteq> ?A" using assms 
-        by (intro subsetI)
-           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] 
-                 intro!: mono)
-    moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
-    moreover have "g c' \<le> c" "g d' \<ge> d"
-      apply (insert c'' d'' c'd'_in_set)
-      apply (subst c''(2)[symmetric])
-      apply (auto simp: c'_def intro!: mono cInf_lower c'') []
-      apply (subst d''(2)[symmetric])
-      apply (auto simp: d'_def intro!: mono cSup_upper d'') []
-      done
-    with c'd'_in_set have "g c' = c" "g d' = d" by auto
-    ultimately show ?thesis using that by blast
-qed
-
 lemma nn_integral_substitution_aux:
   fixes f :: "real \<Rightarrow> ereal"
   assumes Mf: "f \<in> borel_measurable borel"
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Levy.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Levy.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -0,0 +1,539 @@
+(*  Theory: Levy.thy
+    Author: Jeremy Avigad
+*)
+
+section \<open>The Levy inversion theorem, and the Levy continuity theorem.\<close>
+
+theory Levy
+  imports Characteristic_Functions Helly_Selection Sinc_Integral
+begin
+
+lemma LIM_zero_cancel:
+  fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
+  shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F"
+unfolding tendsto_iff dist_norm by simp
+
+subsection \<open>The Levy inversion theorem\<close>
+
+(* Actually, this is not needed for us -- but it is useful for other purposes. (See Billingsley.) *)
+lemma Levy_Inversion_aux1:
+  fixes a b :: real
+  assumes "a \<le> b"
+  shows "((\<lambda>t. (iexp (-(t * a)) - iexp (-(t * b))) / (ii * t)) \<longlongrightarrow> b - a) (at 0)"
+    (is "(?F \<longlongrightarrow> _) (at _)")
+proof -
+  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))"  
+           (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))" 
+      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> 
+        ((- (a * t))^2 / 2) / abs t + ((- (b * t))^2 / 2) / abs t"
+      apply (rule add_mono)
+      apply (rule divide_right_mono)
+      using iexp_approx1 [of "-(t * a)" 1] apply (simp add: field_simps eval_nat_numeral)
+      apply force
+      apply (rule divide_right_mono)
+      using iexp_approx1 [of "-(t * b)" 1] apply (simp add: field_simps eval_nat_numeral)
+      by force
+    also have "\<dots> = a^2 / 2 * abs t + b^2 / 2 * abs t"
+      using `t \<noteq> 0` apply (case_tac "t \<ge> 0", simp add: field_simps power2_eq_square)
+      using `t \<noteq> 0` by (subst (1 2) abs_of_neg, auto simp add: field_simps power2_eq_square)
+    finally show "cmod (?F t - (b - a)) \<le> a^2 / 2 * abs t + b^2 / 2 * abs t" .
+  qed
+  show ?thesis
+    apply (rule LIM_zero_cancel)
+    apply (rule tendsto_norm_zero_cancel)
+    apply (rule real_LIM_sandwich_zero [OF _ _ 1])
+    apply (auto intro!: tendsto_eq_intros)
+    done
+qed
+
+lemma Levy_Inversion_aux2:
+  fixes a b t :: real
+  assumes "a \<le> b" and "t \<noteq> 0"
+  shows "cmod ((iexp (t * b) - iexp (t * a)) / (ii * t)) \<le> b - a" (is "?F \<le> _")
+proof -
+  have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (ii * t))"
+    using `t \<noteq> 0` by (intro arg_cong[where f=norm]) (simp add: field_simps exp_diff exp_minus)
+  also have "\<dots> = cmod (iexp (t * (b - a)) - 1) / abs t"
+    unfolding norm_divide norm_mult norm_exp_ii_times using `t \<noteq> 0`
+    by (simp add: complex_eq_iff norm_mult)
+  also have "\<dots> \<le> abs (t * (b - a)) / abs t"
+    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) 
+  finally show ?thesis .
+qed
+
+(* TODO: refactor! *)
+theorem (in real_distribution) Levy_Inversion:
+  fixes a b :: real
+  assumes "a \<le> b"
+  defines "\<mu> \<equiv> measure M" and "\<phi> \<equiv> char M"
+  assumes "\<mu> {a} = 0" and "\<mu> {b} = 0"
+  shows "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. (iexp (-(t * a)) - iexp (-(t * b))) / (ii * t) * \<phi> t))
+    \<longlonglongrightarrow> \<mu> {a<..b}"
+    (is "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. ?F t * \<phi> t)) \<longlonglongrightarrow> of_real (\<mu> {a<..b})")
+proof -
+  interpret P: pair_sigma_finite lborel M ..
+  from bounded_Si obtain B where Bprop: "\<And>T. abs (Si T) \<le> B" by auto
+  from Bprop [of 0] have [simp]: "B \<ge> 0" by auto
+  let ?f = "\<lambda>t x :: real. (iexp (t * (x - a)) - iexp(t * (x - b))) / (ii * t)"
+  { fix T :: real
+    assume "T \<ge> 0"
+    let ?f' = "\<lambda>(t, x). indicator {-T<..<T} t *\<^sub>R ?f t x"
+    { fix x
+      have 1: "complex_interval_lebesgue_integrable lborel u v (\<lambda>t. ?f t x)" for u v :: real
+        using Levy_Inversion_aux2[of "x - b" "x - a"]
+        apply (simp add: interval_lebesgue_integrable_def del: times_divide_eq_left)
+        apply (intro integrableI_bounded_set_indicator[where B="b - a"] conjI impI)
+        apply (auto intro!: AE_I [of _ _ "{0}"] simp: assms)
+        done
+      have "(CLBINT t. ?f' (t, x)) = (CLBINT t=-T..T. ?f t x)"
+        using `T \<ge> 0` by (simp add: interval_lebesgue_integral_def)
+      also have "\<dots> = (CLBINT t=-T..(0 :: real). ?f t x) + (CLBINT t=(0 :: real)..T. ?f t x)"
+          (is "_ = _ + ?t")
+        using 1 by (intro interval_integral_sum[symmetric]) (simp add: min_absorb1 max_absorb2 \<open>T \<ge> 0\<close>)
+      also have "(CLBINT t=-T..(0 :: real). ?f t x) = (CLBINT t=(0::real)..T. ?f (-t) x)"
+        by (subst interval_integral_reflect) auto
+      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)))) -  
+          (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(
+          2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t)))"
+        using `T \<ge> 0`
+        apply (intro interval_integral_cong)
+        apply (simp add: field_simps cis.ctr Im_divide Re_divide Im_exp Re_exp complex_eq_iff)
+        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. 
+          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)) -
+          sgn (x - b) * Si (T * abs (x - b))))"
+        apply (subst interval_lebesgue_integral_diff)
+        apply (rule interval_lebesgue_integrable_mult_right, rule integrable_sinc')+
+        apply (subst interval_lebesgue_integral_mult_right)+
+        apply (simp add: zero_ereal_def[symmetric] LBINT_I0c_sin_scale_divide[OF `T \<ge> 0`])
+        done
+      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) = 
+      (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)
+    also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))"
+      by (auto intro!: integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
+    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
+      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) * 
+         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) * 
+         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) * 
+         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> 
+       (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)"
+      by (rule integrable_const_bound [of _ "4 * B"]) auto
+  next
+    let ?S = "\<lambda>n::nat. \<lambda>x. sgn (x - a) * Si (n * \<bar>x - a\<bar>) - sgn (x - b) * Si (n * \<bar>x - b\<bar>)"
+    { fix n x
+      have "norm (?S n x) \<le> norm (sgn (x - a) * Si (n * \<bar>x - a\<bar>)) + norm (sgn (x - b) * Si (n * \<bar>x - b\<bar>))"
+        by (rule norm_triangle_ineq4)
+      also have "\<dots> \<le> B + B"
+        using Bprop by (intro add_mono) (auto simp: abs_mult abs_sgn_eq)
+      finally have "norm (2 * ?S n x) \<le> 4 * B"
+        by simp }
+    then show "\<And>n. AE x in M. norm (2 * ?S n x) \<le> 4 * B"
+      by auto
+    have "AE x in M. x \<noteq> a" "AE x in M. x \<noteq> b"
+      using prob_eq_0[of "{a}"] prob_eq_0[of "{b}"] `\<mu> {a} = 0` `\<mu> {b} = 0` by (auto simp: \<mu>_def)
+    then show "AE x in M. (\<lambda>n. 2 * ?S n x) \<longlonglongrightarrow> 2 * pi * indicator {a<..b} x"
+    proof eventually_elim
+      fix x assume x: "x \<noteq> a" "x \<noteq> b"
+      then have "(\<lambda>n. 2 * (sgn (x - a) * Si (\<bar>x - a\<bar> * n) - sgn (x - b) * Si (\<bar>x - b\<bar> * n)))
+          \<longlonglongrightarrow> 2 * (sgn (x - a) * (pi / 2) - sgn (x - b) * (pi / 2))"
+        by (intro tendsto_intros filterlim_compose[OF Si_at_top]
+            filterlim_tendsto_pos_mult_at_top[OF tendsto_const] filterlim_real_sequentially)
+           auto
+      also have "(\<lambda>n. 2 * (sgn (x - a) * Si (\<bar>x - a\<bar> * n) - sgn (x - b) * Si (\<bar>x - b\<bar> * n))) = (\<lambda>n. 2 * ?S n x)"
+        by (auto simp: ac_simps)
+      also have "2 * (sgn (x - a) * (pi / 2) - sgn (x - b) * (pi / 2)) = 2 * pi * indicator {a<..b} x"
+        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 
+  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> 
+       2 * pi * \<mu> {a<..b}" .
+  with main_eq2 show ?thesis
+    by (auto intro!: tendsto_eq_intros)
+qed
+
+theorem Levy_uniqueness:
+  fixes M1 M2 :: "real measure"
+  assumes "real_distribution M1" "real_distribution M2" and
+    "char M1 = char M2"
+  shows "M1 = M2"
+proof -
+  interpret M1: real_distribution M1 by (rule assms)
+  interpret M2: real_distribution M2 by (rule assms)
+  have "countable ({x. measure M1 {x} \<noteq> 0} \<union> {x. measure M2 {x} \<noteq> 0})"
+    by (intro countable_Un M2.countable_support M1.countable_support)
+  then have count: "countable {x. measure M1 {x} \<noteq> 0 \<or> measure M2 {x} \<noteq> 0}"
+    by (simp add: Un_def)
+
+  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)
+
+    { fix \<epsilon> :: real
+      assume "\<epsilon> > 0"
+      from `\<epsilon> > 0` `(cdf M1 \<longlongrightarrow> 0) at_bot` `(cdf M2 \<longlongrightarrow> 0) at_bot`
+      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"
+        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"
+        by auto
+
+      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"
+        "\<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"
+        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"
+        by (auto simp: abs_minus_commute)
+      from `a \<le> x` `x < b` have "a < b" "a \<le> b" by auto
+
+      from `char M1 = char M2`
+        M1.Levy_Inversion [OF `a \<le> b` `measure M1 {a} = 0`  `measure M1 {b} = 0`]
+        M2.Levy_Inversion [OF `a \<le> b` `measure M2 {a} = 0` `measure M2 {b} = 0`]
+      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 `a < b`] M2.cdf_diff_eq [OF `a < b`] .
+
+      have "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) = abs (cdf M1 x - cdf M1 b + cdf M1 a)"
+        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 }
+    then show "cdf M1 x = cdf M2 x"
+      by (metis abs_le_zero_iff dense_ge eq_iff_diff_eq_0)
+  qed
+  thus ?thesis
+    by (rule cdf_unique [OF `real_distribution M1` `real_distribution M2`])
+qed
+
+
+subsection \<open>The Levy continuity theorem\<close>
+
+theorem levy_continuity1:
+  fixes M :: "nat \<Rightarrow> real measure" and M' :: "real measure"
+  assumes "\<And>n. real_distribution (M n)" "real_distribution M'" "weak_conv_m M M'"
+  shows "(\<lambda>n. char (M n) t) \<longlonglongrightarrow> char M' t"
+  unfolding char_def using assms by (rule weak_conv_imp_integral_bdd_continuous_conv) auto
+
+theorem levy_continuity:
+  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" 
+  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)) = 
+      2 * (u  - sin (u * x) / x)"
+  proof -
+    fix u :: real and x :: real
+    assume "u > 0" and "x \<noteq> 0"
+    hence "(CLBINT t:{-u..u}. 1 - iexp (t * x)) = (CLBINT t=-u..u. 1 - iexp (t * x))"
+      by (subst interval_integral_Icc, auto)
+    also have "\<dots> = (CLBINT t=-u..0. 1 - iexp (t * x)) + (CLBINT t=0..u. 1 - iexp (t * x))"
+      using `u > 0`
+      apply (subst interval_integral_sum)
+      apply (simp add: min_absorb1 min_absorb2 max_absorb1 max_absorb2)
+      apply (rule interval_integrable_isCont)
+      apply auto
+      done
+    also have "\<dots> = (CLBINT t=ereal 0..u. 1 - iexp (t * -x)) + (CLBINT t=ereal 0..u. 1 - iexp (t * x))"
+      apply (subgoal_tac "0 = ereal 0", erule ssubst)
+      by (subst interval_integral_reflect, auto)
+    also have "\<dots> = (LBINT t=ereal 0..u. 2 - 2 * cos (t * x))"
+      apply (subst interval_lebesgue_integral_add (2) [symmetric])
+      apply ((rule interval_integrable_isCont, auto)+) [2]
+      unfolding exp_Euler cos_of_real
+      apply (simp add: of_real_mult interval_lebesgue_integral_of_real[symmetric])
+      done
+    also have "\<dots> = 2 * u - 2 * sin (u * x) / x"
+      by (subst interval_lebesgue_integral_diff)
+         (auto intro!: interval_integrable_isCont
+               simp: interval_lebesgue_integral_of_real integral_cos [OF `x \<noteq> 0`] mult.commute[of _ x])
+    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> 
+    u * measure (M n) {x. abs x \<ge> 2 / u}"
+  proof -
+    fix u :: real and n
+    assume "u > 0"
+    interpret P: pair_sigma_finite "M n" lborel ..
+    (* TODO: put this in the real_distribution locale as a simp rule? *)
+    have Mn1 [simp]: "measure (M n) UNIV = 1" by (metis Mn.prob_space Mn.space_eq_univ)
+    (* TODO: make this automatic somehow? *)
+    have Mn2 [simp]: "\<And>x. complex_integrable (M n) (\<lambda>t. exp (\<i> * complex_of_real (x * t)))"
+      by (rule Mn.integrable_const_bound [where B = 1], auto)
+    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
+               intro!: order_trans [OF norm_triangle_ineq4])
+    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))))"
+      by (rule integral_cong) (auto split: split_indicator)
+    also have "\<dots> = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))"
+      using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta')
+    also have "\<dots> = (CLINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
+      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) = 
+       (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 -
+      have "complex_integrable (M n) (\<lambda>x. CLBINT t:{-u..u}. 1 - iexp (snd (x, t) * fst (x, t)))"
+        using Mn3 by (intro P.integrable_fst) (simp add: indicator_times split_beta')
+      hence "complex_integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
+        using `u > 0` by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
+      hence **: "integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
+        unfolding complex_of_real_integrable_eq .
+      have "2 * sin x \<le> x" if "2 \<le> x" for x :: real
+        by (rule order_trans[OF _ \<open>2 \<le> x\<close>]) auto
+      moreover have "x \<le> 2 * sin x" if "x \<le> - 2" for x :: real
+        by (rule order_trans[OF \<open>x \<le> - 2\<close>]) auto
+      moreover have "x < 0 \<Longrightarrow> x \<le> sin x" for x :: real
+        using sin_x_le_x[of "-x"] by simp
+      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)
+    qed
+    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}" .
+  qed
+
+  have tight_aux: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> \<exists>a b. a < b \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {a<..b})"
+  proof -
+    fix \<epsilon> :: real
+    assume "\<epsilon> > 0"
+    note M'.isCont_char [of 0]
+    hence "\<exists>d>0. \<forall>t. abs t < d \<longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4"
+      apply (subst (asm) continuous_at_eps_delta)
+      apply (drule_tac x = "\<epsilon> / 4" in spec)
+      using `\<epsilon> > 0` by (auto simp add: dist_real_def dist_complex_def M'.char_zero)
+    then obtain d where "d > 0 \<and> (\<forall>t. (abs t < d \<longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4))" ..
+    hence d0: "d > 0" and d1: "\<And>t. abs t < d \<Longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4" by auto
+    have 1: "\<And>x. cmod (1 - char M' x) \<le> 2"
+      by (rule order_trans [OF norm_triangle_ineq4], auto simp add: M'.cmod_char_le_1)
+    then have 2: "\<And>u v. complex_set_integrable lborel {u..v} (\<lambda>x. 1 - char M' x)"
+      by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq)
+    have 3: "\<And>u v. set_integrable lborel {u..v} (\<lambda>x. cmod (1 - char M' x))"
+      by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
+                continuous_intros ballI M'.isCont_char continuous_intros)
+    have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
+      using integral_norm_bound[OF 2] by simp
+    also have "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
+      apply (rule integral_mono [OF 3])
+      apply (simp add: emeasure_lborel_Icc_eq)
+      apply (case_tac "x \<in> {-d/2..d/2}", auto)
+      apply (subst norm_minus_commute)
+      apply (rule less_imp_le)
+      apply (rule d1 [simplified])
+      using d0 by auto
+    also with d0 have "\<dots> = d * \<epsilon> / 4"
+      by simp
+    finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" .
+    { fix n x
+      have "cmod (1 - char (M n) x) \<le> 2"
+        by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
+    } note bd1 = this
+    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 
+                  simp: emeasure_lborel_Icc_eq
+                  split: split_indicator)
+      done
+    hence "eventually (\<lambda>n. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
+        (CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4) sequentially"
+      using d0 `\<epsilon> > 0` apply (subst (asm) tendsto_iff)
+      by (subst (asm) dist_complex_def, drule spec, erule mp, auto)
+    hence "\<exists>N. \<forall>n \<ge> N. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
+        (CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by (simp add: eventually_sequentially)
+    then guess N ..
+    hence N: "\<And>n. n \<ge> N \<Longrightarrow> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
+        (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) = 
+        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) - 
+          (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" 
+        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)}" 
+        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)
+      hence "\<epsilon> > 1 - measure (M n) (UNIV - {x. abs x \<ge> 2 / (d / 2)})"
+        apply (subst Mn.borel_UNIV [symmetric])
+        by (subst Mn.prob_compl, auto)
+      also have "UNIV - {x. abs x \<ge> 2 / (d / 2)} = {x. -(4 / d) < x \<and> x < (4 / d)}"
+        using d0 apply (auto simp add: field_simps)
+        (* very annoying -- this should be automatic *)
+        apply (case_tac "x \<ge> 0", auto simp add: field_simps)
+        apply (subgoal_tac "0 \<le> x * d", arith, rule mult_nonneg_nonneg, auto)
+        apply (case_tac "x \<ge> 0", auto simp add: field_simps)
+        apply (subgoal_tac "x * d \<le> 0", arith)
+        apply (rule mult_nonpos_nonneg, auto)
+        by (case_tac "x \<ge> 0", auto simp add: field_simps)
+      finally have "measure (M n) {x. -(4 / d) < x \<and> x < (4 / d)} > 1 - \<epsilon>"
+        by auto
+    } note 6 = this
+    { 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> 
+          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"
+        using Mn.prob_space unfolding * Mn.borel_UNIV by simp
+      hence "eventually (\<lambda>k. measure (M n) {- real k<..real k} > 1 - \<epsilon>) sequentially"
+        apply (elim order_tendstoD (1))
+        using `\<epsilon> > 0` by auto
+    } note 7 = this
+    { fix n :: nat
+      have "eventually (\<lambda>k. \<forall>m < n. measure (M m) {- real k<..real k} > 1 - \<epsilon>) sequentially"
+        (is "?P n")
+      proof (induct n)
+        case (Suc n) with 7[of n] show ?case
+          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> < 
+        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 
+      "\<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
+    let ?K' = "max K (4 / d)"
+    have "-?K' < ?K' \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {-?K'<..?K'})"
+      using d0 apply auto
+      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)}"      
+        apply (case_tac "n < N")
+        apply (rule order_less_le_trans)
+        apply (erule K)
+        apply (rule Mn.finite_measure_mono, auto)
+        apply (rule order_less_le_trans)
+        apply (rule 6, erule leI)
+        by (rule Mn.finite_measure_mono, auto)
+    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"
+    by (auto simp: tight_def intro: assms tight_aux)
+  show ?thesis
+  proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight])
+    fix s \<nu>
+    assume s: "subseq s"
+    assume nu: "weak_conv_m (M \<circ> s) \<nu>"
+    assume *: "real_distribution \<nu>"
+    have 2: "\<And>n. real_distribution ((M \<circ> s) n)" unfolding comp_def by (rule assms)
+    have 3: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char \<nu> t" by (intro levy_continuity1 [OF 2 * nu])
+    have 4: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) = ((\<lambda>n. char (M n) t) \<circ> s)" by (rule ext, simp)
+    have 5: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char M' t"
+      by (subst 4, rule lim_subseq [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'" 
+      apply (elim subst)
+      by (rule nu)  
+  qed
+qed
+
+end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -1186,6 +1186,25 @@
   finally show ?thesis .
 qed
 
+lemma nn_integral_indicator_singleton[simp]:
+  assumes [measurable]: "{y} \<in> sets M"
+  shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
+proof-
+  have "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f y) * indicator {y} x \<partial>M)"
+    by (subst nn_integral_max_0[symmetric]) (auto intro!: nn_integral_cong split: split_indicator)
+  then show ?thesis
+    by (simp add: nn_integral_cmult)
+qed
+
+lemma nn_integral_set_ereal:
+  "(\<integral>\<^sup>+x. ereal (f x) * indicator A x \<partial>M) = (\<integral>\<^sup>+x. ereal (f x * indicator A x) \<partial>M)"
+  by (rule nn_integral_cong) (simp split: split_indicator)
+
+lemma nn_integral_indicator_singleton'[simp]:
+  assumes [measurable]: "{y} \<in> sets M"
+  shows "(\<integral>\<^sup>+x. ereal (f x * indicator {y} x) \<partial>M) = max 0 (f y) * emeasure M {y}"
+  by (subst nn_integral_set_ereal[symmetric]) (simp add: nn_integral_indicator_singleton)
+
 lemma nn_integral_add:
   assumes f: "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x"
   and g: "g \<in> borel_measurable M" "AE x in M. 0 \<le> g x"
@@ -1854,7 +1873,7 @@
     by (subst nn_integral_setsum)
        (simp_all add: AE_count_space ereal_zero_le_0_iff less_imp_le)
   also have "\<dots> = (\<Sum>a|a\<in>A \<and> 0 < f a. f a)"
-    by (auto intro!: setsum.cong simp: nn_integral_cmult_indicator one_ereal_def[symmetric])
+    by (auto intro!: setsum.cong simp: one_ereal_def[symmetric] max_def)
   finally show ?thesis by (simp add: nn_integral_max_0)
 qed
 
@@ -1890,7 +1909,7 @@
   from f have "(\<integral>\<^sup>+x. f x * indicator A x \<partial>M) = (\<integral>\<^sup>+x. (\<Sum>a\<in>A. f a * indicator {a} x) \<partial>M)"
     by (intro nn_integral_cong) (auto simp: indicator_def if_distrib[where f="\<lambda>a. x * a" for x] setsum.If_cases)
   also have "\<dots> = (\<Sum>a\<in>A. f a * emeasure M {a})"
-    using nn by (subst nn_integral_setsum) (auto simp: nn_integral_cmult_indicator)
+    using nn by (subst nn_integral_setsum) (auto simp: max_def)
   finally show ?thesis .
 qed
 
@@ -1912,7 +1931,7 @@
   also have "\<dots> = (\<Sum>j. (\<integral>\<^sup>+i. f j * indicator {j} i \<partial>count_space UNIV))"
     by (rule nn_integral_suminf) (auto simp: nonneg)
   also have "\<dots> = (\<Sum>j. f j)"
-    by (simp add: nonneg nn_integral_cmult_indicator one_ereal_def[symmetric])
+    by (simp add: nonneg one_ereal_def[symmetric] max_def)
   finally show ?thesis .
 qed
 
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Probability.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -7,12 +7,10 @@
   Discrete_Topology
   Complete_Measure
   Projective_Limit
-  Independent_Family
-  Distributions
   Probability_Mass_Function
   Stream_Space
   Embed_Measure
+  Central_Limit_Theorem
 begin
 
 end
-
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -32,48 +32,6 @@
 lemma ereal_divide': "b \<noteq> 0 \<Longrightarrow> ereal (a / b) = ereal a / ereal b"
   using ereal_divide[of a b] by simp
 
-lemma (in finite_measure) countable_support:
-  "countable {x. measure M {x} \<noteq> 0}"
-proof cases
-  assume "measure M (space M) = 0"
-  with bounded_measure measure_le_0_iff have "{x. measure M {x} \<noteq> 0} = {}"
-    by auto
-  then show ?thesis
-    by simp
-next
-  let ?M = "measure M (space M)" and ?m = "\<lambda>x. measure M {x}"
-  assume "?M \<noteq> 0"
-  then have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. ?M / Suc n < ?m x})"
-    using reals_Archimedean[of "?m x / ?M" for x]
-    by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff)
-  have **: "\<And>n. finite {x. ?M / Suc n < ?m x}"
-  proof (rule ccontr)
-    fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
-    then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
-      by (metis infinite_arbitrarily_large)
-    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
-      by auto
-    { fix x assume "x \<in> X"
-      from \<open>?M \<noteq> 0\<close> *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
-      then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
-    note singleton_sets = this
-    have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
-      using \<open>?M \<noteq> 0\<close>
-      by (simp add: \<open>card X = Suc (Suc n)\<close> of_nat_Suc field_simps less_le measure_nonneg)
-    also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
-      by (rule setsum_mono) fact
-    also have "\<dots> = measure M (\<Union>x\<in>X. {x})"
-      using singleton_sets \<open>finite X\<close>
-      by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def)
-    finally have "?M < measure M (\<Union>x\<in>X. {x})" .
-    moreover have "measure M (\<Union>x\<in>X. {x}) \<le> ?M"
-      using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto
-    ultimately show False by simp
-  qed
-  show ?thesis
-    unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
-qed
-
 lemma (in finite_measure) AE_support_countable:
   assumes [simp]: "sets M = UNIV"
   shows "(AE x in M. measure M {x} \<noteq> 0) \<longleftrightarrow> (\<exists>S. countable S \<and> (AE x in M. x \<in> S))"
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -9,6 +9,48 @@
   imports Lebesgue_Measure Radon_Nikodym
 begin
 
+lemma (in finite_measure) countable_support:
+  "countable {x. measure M {x} \<noteq> 0}"
+proof cases
+  assume "measure M (space M) = 0"
+  with bounded_measure measure_le_0_iff have "{x. measure M {x} \<noteq> 0} = {}"
+    by auto
+  then show ?thesis
+    by simp
+next
+  let ?M = "measure M (space M)" and ?m = "\<lambda>x. measure M {x}"
+  assume "?M \<noteq> 0"
+  then have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. ?M / Suc n < ?m x})"
+    using reals_Archimedean[of "?m x / ?M" for x]
+    by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff)
+  have **: "\<And>n. finite {x. ?M / Suc n < ?m x}"
+  proof (rule ccontr)
+    fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
+    then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
+      by (metis infinite_arbitrarily_large)
+    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
+      by auto
+    { fix x assume "x \<in> X"
+      from \<open>?M \<noteq> 0\<close> *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
+      then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
+    note singleton_sets = this
+    have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
+      using \<open>?M \<noteq> 0\<close>
+      by (simp add: \<open>card X = Suc (Suc n)\<close> of_nat_Suc field_simps less_le measure_nonneg)
+    also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
+      by (rule setsum_mono) fact
+    also have "\<dots> = measure M (\<Union>x\<in>X. {x})"
+      using singleton_sets \<open>finite X\<close>
+      by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def)
+    finally have "?M < measure M (\<Union>x\<in>X. {x})" .
+    moreover have "measure M (\<Union>x\<in>X. {x}) \<le> ?M"
+      using singleton_sets[THEN sets.sets_into_space] by (intro finite_measure_mono) auto
+    ultimately show False by simp
+  qed
+  show ?thesis
+    unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
+qed
+
 locale prob_space = finite_measure +
   assumes emeasure_space_1: "emeasure M (space M) = 1"
 
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Radon_Nikodym.thy
--- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -1295,7 +1295,7 @@
   have "density M (RN_deriv M N) {x} = (\<integral>\<^sup>+w. RN_deriv M N x * indicator {x} w \<partial>M)"
     by (auto simp: indicator_def emeasure_density intro!: nn_integral_cong)
   with x density_RN_deriv[OF ac] RN_deriv_nonneg[of M N] show ?thesis
-    by (auto simp: nn_integral_cmult_indicator)
+    by (auto simp: max_def)
 qed
 
 end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Set_Integral.thy
--- a/src/HOL/Probability/Set_Integral.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Set_Integral.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -69,6 +69,19 @@
   by (auto simp add: indicator_def)
 *)
 
+lemma set_borel_measurable_sets:
+  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
+  assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
+  shows "f -` B \<inter> X \<in> sets M"
+proof -
+  have "f \<in> borel_measurable (restrict_space M X)"
+    using assms by (subst borel_measurable_restrict_space_iff) auto
+  then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
+    by (rule measurable_sets) fact
+  with \<open>X \<in> sets M\<close> show ?thesis
+    by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
+qed
+
 lemma set_lebesgue_integral_cong:
   assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
   shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -2206,6 +2206,10 @@
     by simp
 qed
 
+lemma restrict_space_sets_cong:
+  "A = B \<Longrightarrow> sets M = sets N \<Longrightarrow> sets (restrict_space M A) = sets (restrict_space N B)"
+  by (auto simp: sets_restrict_space)
+
 lemma sets_restrict_space_count_space :
   "sets (restrict_space (count_space A) B) = sets (count_space (A \<inter> B))"
 by(auto simp add: sets_restrict_space)
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Sinc_Integral.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Sinc_Integral.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -0,0 +1,403 @@
+(*
+  Theory: Sinc_Integral.thy
+  Authors: Jeremy Avigad, Luke Serafin, Johannes Hölzl 
+*)
+
+section \<open>Integral of sinc\<close>
+
+theory Sinc_Integral
+  imports Distributions
+begin
+
+subsection \<open>Various preparatory integrals\<close>
+
+text \<open> Naming convention
+The theorem name consists of the following parts:
+  \<^item> Kind of integral: @{text has_bochner_integral} / @{text integrable} / @{text LBINT}
+  \<^item> Interval: Interval (0 / infinity / open / closed) (infinity / open / closed) 
+  \<^item> Name of the occurring constants: power, exp, m (for minus), scale, sin, $\ldots$
+\<close>
+
+lemma has_bochner_integral_I0i_power_exp_m':
+  "has_bochner_integral lborel (\<lambda>x. x^k * exp (-x) * indicator {0 ..} x::real) (fact k)"
+  using nn_intergal_power_times_exp_Ici[of k]
+  by (intro has_bochner_integral_nn_integral)
+     (auto simp: ereal_indicator[symmetric] split: split_indicator)
+
+lemma has_bochner_integral_I0i_power_exp_m:
+  "has_bochner_integral lborel (\<lambda>x. x^k * exp (-x) * indicator {0 <..} x::real) (fact k)"
+  using AE_lborel_singleton[of 0]
+  by (intro has_bochner_integral_cong_AE[THEN iffD1, OF _ _ _ has_bochner_integral_I0i_power_exp_m'])
+     (auto split: split_indicator)
+
+lemma integrable_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> set_integrable lborel {0 <..} (\<lambda>x. exp (-(x * u)))" 
+  using lborel_integrable_real_affine_iff[of u "\<lambda>x. indicator {0 <..} x *\<^sub>R exp (- x)" 0]
+        has_bochner_integral_I0i_power_exp_m[of 0]
+  by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros)
+
+lemma LBINT_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> LBINT x=0..\<infinity>. exp (-(x * u)) = 1 / u" 
+  using lborel_integral_real_affine[of u "\<lambda>x. indicator {0<..} x *\<^sub>R exp (- x)" 0]
+        has_bochner_integral_I0i_power_exp_m[of 0]
+  by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty field_simps
+           dest!: has_bochner_integral_integral_eq)
+
+lemma LBINT_I0c_exp_mscale_sin:
+  "LBINT x=0..t. exp (-(u * x)) * sin x =
+    (1 / (1 + u^2)) * (1 - exp (-(u * t)) * (u * sin t + cos t))" (is "_ = ?F t")
+  unfolding zero_ereal_def
+proof (subst interval_integral_FTC_finite)
+  show "(?F has_vector_derivative exp (- (u * x)) * sin x) (at x within {min 0 t..max 0 t})" for x
+    by (auto intro!: derivative_eq_intros
+             simp: has_field_derivative_iff_has_vector_derivative[symmetric] power2_eq_square)
+       (simp_all add: field_simps add_nonneg_eq_0_iff)
+qed (auto intro: continuous_at_imp_continuous_on)
+
+lemma LBINT_I0i_exp_mscale_sin:
+  assumes "0 < x"
+  shows "LBINT u=0..\<infinity>. \<bar>exp (-u * x) * sin x\<bar> = \<bar>sin x\<bar> / x" 
+proof (subst interval_integral_FTC_nonneg)
+  let ?F = "\<lambda>u. 1 / x * (1 - exp (- u * x)) * \<bar>sin x\<bar>"
+  show "\<And>t. (?F has_real_derivative \<bar>exp (- t * x) * sin x\<bar>) (at t)"
+    using \<open>0 < x\<close> by (auto intro!: derivative_eq_intros simp: abs_mult)
+  show "((?F \<circ> real_of_ereal) \<longlongrightarrow> 0) (at_right 0)"
+    using \<open>0 < x\<close> by (auto simp: zero_ereal_def ereal_tendsto_simps intro!: tendsto_eq_intros)
+  have *: "((\<lambda>t. exp (- t * x)) \<longlongrightarrow> 0) at_top"
+    using \<open>0 < x\<close>
+    by (auto intro!: exp_at_bot[THEN filterlim_compose] filterlim_tendsto_pos_mult_at_top filterlim_ident
+             simp: filterlim_uminus_at_bot mult.commute[of _ x])
+  show "((?F \<circ> real_of_ereal) \<longlongrightarrow> \<bar>sin x\<bar> / x) (at_left \<infinity>)"
+    using \<open>0 < x\<close> unfolding ereal_tendsto_simps
+    by (intro filterlim_compose[OF _ *]) (auto intro!: tendsto_eq_intros filterlim_ident)
+qed auto
+
+lemma
+  shows integrable_inverse_1_plus_square:
+      "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))"
+  and LBINT_inverse_1_plus_square:
+      "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi"
+proof -
+  have 1: "- (pi / 2) < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> (tan has_real_derivative 1 + (tan x)\<^sup>2) (at x)" for x
+    using cos_gt_zero_pi[of x] by (subst tan_sec) (auto intro!: DERIV_tan simp: power_inverse)
+  have 2: "- (pi / 2) < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> isCont (\<lambda>x. 1 + (tan x)\<^sup>2) x" for x
+    using cos_gt_zero_pi[of x] by auto
+  show "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi"
+    by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
+       (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
+             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
+  show "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))"
+    by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
+       (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
+             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
+qed
+
+lemma 
+  shows integrable_I0i_1_div_plus_square:
+    "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))"
+  and LBINT_I0i_1_div_plus_square:
+    "LBINT x=0..\<infinity>. 1 / (1 + x^2) = pi / 2"
+proof -
+  have 1: "0 < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> (tan has_real_derivative 1 + (tan x)\<^sup>2) (at x)" for x
+    using cos_gt_zero_pi[of x] by (subst tan_sec) (auto intro!: DERIV_tan simp: power_inverse)
+  have 2: "0 < x \<Longrightarrow> x * 2 < pi \<Longrightarrow> isCont (\<lambda>x. 1 + (tan x)\<^sup>2) x" for x
+    using cos_gt_zero_pi[of x] by auto
+  show "LBINT x=0..\<infinity>. 1 / (1 + x^2) = pi / 2"
+    by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
+       (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
+             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
+  show "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))"
+    unfolding interval_lebesgue_integrable_def 
+    by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
+       (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
+             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
+qed
+
+section \<open>The sinc function, and the sine integral (Si)\<close>
+
+abbreviation sinc :: "real \<Rightarrow> real" where
+  "sinc \<equiv> (\<lambda>x. if x = 0 then 1 else sin x / x)"
+
+lemma sinc_at_0: "((\<lambda>x. sin x / x::real) \<longlongrightarrow> 1) (at 0)"
+  using DERIV_sin [of 0] by (auto simp add: has_field_derivative_def field_has_derivative_at)
+
+lemma isCont_sinc: "isCont sinc x"
+proof cases
+  assume "x = 0" then show ?thesis
+    using LIM_equal [where g = "\<lambda>x. sin x / x" and a=0 and f=sinc and l=1]
+    by (auto simp: isCont_def sinc_at_0)
+next
+  assume "x \<noteq> 0" show ?thesis
+    by (rule continuous_transform_at [where d = "abs x" and f = "\<lambda>x. sin x / x"])
+       (auto simp add: dist_real_def \<open>x \<noteq> 0\<close>)
+qed
+
+lemma continuous_on_sinc[continuous_intros]:
+  "continuous_on S f \<Longrightarrow> continuous_on S (\<lambda>x. sinc (f x))"
+  using continuous_on_compose[of S f sinc, OF _ continuous_at_imp_continuous_on]
+  by (auto simp: isCont_sinc)
+
+lemma borel_measurable_sinc[measurable]: "sinc \<in> borel_measurable borel"
+  by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_sinc)
+
+lemma sinc_AE: "AE x in lborel. sin x / x = sinc x"
+  by (rule AE_I [where N = "{0}"], auto)
+
+definition Si :: "real \<Rightarrow> real" where "Si t \<equiv> LBINT x=0..t. sin x / x"
+
+lemma sinc_neg [simp]: "sinc (- x) = sinc x"
+  by auto
+
+(* TODO: Determine whether this can reasonably be eliminated by redefining Si. *)
+lemma Si_alt_def : "Si t = LBINT x=0..t. sinc x"
+proof cases
+  assume "0 \<le> t" then show ?thesis
+    using AE_lborel_singleton[of 0]
+    by (auto simp: Si_def intro!: interval_lebesgue_integral_cong_AE)
+next
+  assume "\<not> 0 \<le> t" then show ?thesis
+    unfolding Si_def using AE_lborel_singleton[of 0]
+    by (subst (1 2) interval_integral_endpoints_reverse)
+       (auto simp: Si_def intro!: interval_lebesgue_integral_cong_AE)
+qed
+
+lemma Si_neg: 
+  assumes "T \<ge> 0" shows "Si (- T) = - Si T"
+proof -
+  have "LBINT x=ereal 0..T. -1 *\<^sub>R sinc (- x) = LBINT y= ereal (- 0)..ereal (- T). sinc y"
+    by (rule interval_integral_substitution_finite [OF assms])
+       (auto intro: derivative_intros continuous_at_imp_continuous_on isCont_sinc)
+  also have "(LBINT x=ereal 0..T. -1 *\<^sub>R sinc (- x)) = -(LBINT x=ereal 0..T. sinc x)"
+    by (subst sinc_neg) (simp_all add: interval_lebesgue_integral_uminus)
+  finally have *: "-(LBINT x=ereal 0..T. sinc x) = LBINT y= ereal 0..ereal (- T). sinc y"
+    by simp
+  show ?thesis
+    using assms unfolding Si_alt_def
+    by (subst zero_ereal_def)+ (auto simp add: * [symmetric])
+qed
+
+lemma integrable_sinc':
+  "interval_lebesgue_integrable lborel (ereal 0) (ereal T) (\<lambda>t. sin (t * \<theta>) / t)"
+proof -
+  have *: "interval_lebesgue_integrable lborel (ereal 0) (ereal T) (\<lambda>t. \<theta> * sinc (t * \<theta>))"
+    by (intro interval_lebesgue_integrable_mult_right interval_integrable_isCont continuous_within_compose3 [OF isCont_sinc])
+       auto
+  show ?thesis
+    by (rule interval_lebesgue_integrable_cong_AE[THEN iffD1, OF _ _ _ *])
+       (insert AE_lborel_singleton[of 0], auto)
+qed
+
+(* TODO: need a better version of FTC2 *)
+lemma DERIV_Si: "(Si has_real_derivative sinc x) (at x)"
+proof -
+  have "(at x within {min 0 (x - 1)..max 0 (x + 1)}) = at x"
+    by (intro at_within_interior) auto
+  moreover have "min 0 (x - 1) \<le> x" "x \<le> max 0 (x + 1)"
+    by auto
+  ultimately show ?thesis
+    using interval_integral_FTC2[of "min 0 (x - 1)" 0 "max 0 (x + 1)" sinc x]
+    by (auto simp: continuous_at_imp_continuous_on isCont_sinc Si_alt_def[abs_def] zero_ereal_def
+                   has_field_derivative_iff_has_vector_derivative
+             split del: split_if)
+qed
+
+lemma isCont_Si: "isCont Si x"
+  using DERIV_Si by (rule DERIV_isCont)
+
+lemma borel_measurable_Si[measurable]: "Si \<in> borel_measurable borel"
+  by (auto intro: isCont_Si continuous_at_imp_continuous_on borel_measurable_continuous_on1)
+
+lemma Si_at_top_LBINT:
+  "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top"
+proof -
+  let ?F = "\<lambda>x t. exp (- (x * t)) * (x * sin t + cos t) / (1 + x\<^sup>2) :: real"
+  have int: "set_integrable lborel {0<..} (\<lambda>x. exp (- x) * (x + 1) :: real)"
+    unfolding distrib_left
+    using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
+    by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps)
+
+  have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top"
+  proof (rule integral_dominated_convergence_at_top[OF _ _ int], simp_all del: abs_divide split: split_indicator)
+    have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real
+      by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
+         (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
+    then have **: "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
+        by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right
+                 intro!:  mult_mono)
+  
+    show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
+      using eventually_ge_at_top[of "1::real"] ** by (auto elim: eventually_mono)
+    show "AE x in lborel. 0 < x \<longrightarrow> (?F x \<longlongrightarrow> 0) at_top"
+    proof (intro always_eventually impI allI)
+      fix x :: real assume "0 < x"
+      show "((\<lambda>t. exp (- (x * t)) * (x * sin t + cos t) / (1 + x\<^sup>2)) \<longlongrightarrow> 0) at_top"
+      proof (rule Lim_null_comparison)
+        show "\<forall>\<^sub>F t in at_top. norm (?F x t) \<le> exp (- (x * t)) * (x + 1)"
+          using eventually_ge_at_top[of "1::real"] * \<open>0 < x\<close>
+          by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right
+                   intro!: mult_mono elim: eventually_mono)
+        show "((\<lambda>t. exp (- (x * t)) * (x + 1)) \<longlongrightarrow> 0) at_top"
+          by (auto simp: filterlim_uminus_at_top [symmetric]
+                   intro!: filterlim_tendsto_pos_mult_at_top[OF tendsto_const] \<open>0<x\<close> filterlim_ident
+                           tendsto_mult_left_zero filterlim_compose[OF exp_at_bot])
+      qed
+    qed
+  qed
+  then show "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top"
+    by (simp add: interval_lebesgue_integral_0_infty)
+qed
+
+lemma Si_at_top_integrable:
+  assumes "t \<ge> 0"
+  shows "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. exp (- (x * t)) * (x * sin t + cos t) / (1 + x\<^sup>2))"
+  using \<open>0 \<le> t\<close> unfolding le_less
+proof
+  assume "0 = t" then show ?thesis
+    using integrable_I0i_1_div_plus_square by simp
+next
+  assume [arith]: "0 < t"
+  have *: "0 \<le> a \<Longrightarrow> 0 < x \<Longrightarrow> a / (1 + x\<^sup>2) \<le> a" for a x :: real
+    using zero_le_power2[of x, arith] using divide_left_mono[of 1 "1+x\<^sup>2" a] by auto
+  have "set_integrable lborel {0<..} (\<lambda>x. (exp (- x) * x) * (sin t/t) + exp (- x) * cos t)"
+    using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
+    by (intro set_integral_add set_integrable_mult_left)
+       (auto dest!: integrable.intros simp: ac_simps)
+  from lborel_integrable_real_affine[OF this, of t 0]
+  show ?thesis
+    unfolding interval_lebesgue_integral_0_infty
+    by (rule integrable_bound) (auto simp: field_simps * split: split_indicator)
+qed
+
+lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top"
+proof -
+  have "\<forall>\<^sub>F t in at_top. pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t"
+    using eventually_ge_at_top[of 0]
+  proof eventually_elim
+    fix t :: real assume "t \<ge> 0"
+    have "Si t = LBINT x=0..t. sin x * (LBINT u=0..\<infinity>. exp (-(u * x)))"
+      unfolding Si_def using `0 \<le> t`
+      by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale)
+    also have "\<dots> = LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x)))"
+      using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac)
+    also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
+      by (subst interval_integral_Ioi) (simp_all add: indicator_times ac_simps)
+    also have "\<dots> = LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
+    proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable)
+      show "(\<lambda>(x, y). indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x))))
+          \<in> borel_measurable (lborel \<Otimes>\<^sub>M lborel)" (is "?f \<in> borel_measurable _")
+        by measurable
+
+      have "AE x in lborel. indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
+        using AE_lborel_singleton[of 0] AE_lborel_singleton[of t]
+      proof eventually_elim
+        fix x :: real assume x: "x \<noteq> 0" "x \<noteq> t"
+        have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> = 
+            LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x"
+          by (intro integral_cong) (auto split: split_indicator simp: abs_mult)
+        also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>.  exp (- (y * x)))"
+          by (cases "x > 0")                                       
+             (auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
+        also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (1 / x)"
+          by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale)
+        also have "\<dots> = indicator {0..t} x *\<^sub>R \<bar>sinc x\<bar>"
+          using x by (simp add: field_simps split: split_indicator)
+        finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
+          by simp
+      qed
+      moreover have "set_integrable lborel {0 .. t} (\<lambda>x. abs (sinc x))"
+        by (auto intro!: borel_integrable_compact continuous_intros simp del: real_scaleR_def)
+      ultimately show "integrable lborel (\<lambda>x. LBINT y. norm (?f (x, y)))"
+        by (rule integrable_cong_AE_imp[rotated 2]) simp
+  
+      have "0 < x \<Longrightarrow> set_integrable lborel {0<..} (\<lambda>y. sin x * exp (- (y * x)))" for x :: real
+          by (intro set_integrable_mult_right integrable_I0i_exp_mscale)
+      then show "AE x in lborel. integrable lborel (\<lambda>y. ?f (x, y))"
+        by (intro AE_I2) (auto simp: indicator_times split: split_indicator)
+    qed
+    also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
+      using \<open>0\<le>t\<close>
+      by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
+               split: split_indicator intro!: integral_cong)
+    also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
+      by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
+    also have "... = pi / 2 - (LBINT u=0..\<infinity>. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))"
+      using Si_at_top_integrable[OF \<open>0\<le>t\<close>] by (simp add: integrable_I0i_1_div_plus_square LBINT_I0i_1_div_plus_square)
+    finally show "pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t" ..
+  qed
+  then show ?thesis
+    by (rule Lim_transform_eventually)
+       (auto intro!: tendsto_eq_intros Si_at_top_LBINT)
+qed
+
+subsection \<open>The final theorems: boundedness and scalability\<close>
+
+lemma bounded_Si: "\<exists>B. \<forall>T. \<bar>Si T\<bar> \<le> B"
+proof -
+  have *: "0 \<le> y \<Longrightarrow> dist x y < z \<Longrightarrow> abs x \<le> y + z" for x y z :: real
+    by (simp add: dist_real_def)
+
+  have "eventually (\<lambda>T. dist (Si T) (pi / 2) < 1) at_top"
+    using Si_at_top by (elim tendstoD) simp
+  then have "eventually (\<lambda>T. 0 \<le> T \<and> \<bar>Si T\<bar> \<le> pi / 2 + 1) at_top"
+    using eventually_ge_at_top[of 0] by eventually_elim (insert *[of "pi/2" "Si _" 1], auto)
+  then have "\<exists>T. 0 \<le> T \<and> (\<forall>t \<ge> T. \<bar>Si t\<bar> \<le> pi / 2 + 1)"
+    by (auto simp add: eventually_at_top_linorder)
+  then obtain T where T: "0 \<le> T" "\<And>t. t \<ge> T \<Longrightarrow> \<bar>Si t\<bar> \<le> pi / 2 + 1"
+    by auto
+  moreover have "t \<le> - T \<Longrightarrow> \<bar>Si t\<bar> \<le> pi / 2 + 1" for t
+    using T(1) T(2)[of "-t"] Si_neg[of "- t"] by simp
+  moreover have "\<exists>M. \<forall>t. -T \<le> t \<and> t \<le> T \<longrightarrow> \<bar>Si t\<bar> \<le> M"
+    by (rule isCont_bounded) (auto intro!: isCont_Si continuous_intros \<open>0 \<le> T\<close>)
+  then obtain M where M: "\<And>t. -T \<le> t \<and> t \<le> T \<Longrightarrow> \<bar>Si t\<bar> \<le> M"
+    by auto
+  ultimately show ?thesis
+    by (intro exI[of _ "max M (pi/2 + 1)"]) (meson le_max_iff_disj linorder_not_le order_le_less)
+qed    
+
+lemma LBINT_I0c_sin_scale_divide:
+  assumes "T \<ge> 0"
+  shows "LBINT t=0..T. sin (t * \<theta>) / t = sgn \<theta> * Si (T * \<bar>\<theta>\<bar>)"
+proof -
+  { assume "0 < \<theta>"
+    have "(LBINT t=ereal 0..T. sin (t * \<theta>) / t) = (LBINT t=ereal 0..T. \<theta> *\<^sub>R sinc (t * \<theta>))"
+      by (rule interval_integral_discrete_difference[of "{0}"]) auto
+    also have "\<dots> = (LBINT t=ereal (0 * \<theta>)..T * \<theta>. sinc t)"
+      apply (rule interval_integral_substitution_finite [OF assms])
+      apply (subst mult.commute, rule DERIV_subset)
+      by (auto intro!: derivative_intros continuous_at_imp_continuous_on isCont_sinc)
+    also have "\<dots> = (LBINT t=ereal (0 * \<theta>)..T * \<theta>. sin t / t)"
+      by (rule interval_integral_discrete_difference[of "{0}"]) auto
+    finally have "(LBINT t=ereal 0..T. sin (t * \<theta>) / t) = (LBINT t=ereal 0..T * \<theta>. sin t / t)"
+      by simp
+    hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
+        LBINT x. indicator {0<..<T * \<theta>} x * sin x / x"
+      using assms `0 < \<theta>` unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def 
+        by (auto simp: ac_simps)
+  } note aux1 = this
+  { assume "0 > \<theta>"
+    have [simp]: "integrable lborel (\<lambda>x. sin (x * \<theta>) * indicator {0<..<T} x / x)"
+      using integrable_sinc' [of T \<theta>] assms 
+      by (simp add: interval_lebesgue_integrable_def ac_simps)
+    have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T. -\<theta> *\<^sub>R sinc (t * -\<theta>))"
+      by (rule interval_integral_discrete_difference[of "{0}"]) auto
+    also have "\<dots> = (LBINT t=ereal (0 * -\<theta>)..T * -\<theta>. sinc t)"
+      apply (rule interval_integral_substitution_finite [OF assms])
+      apply (subst mult.commute, rule DERIV_subset)
+      by (auto intro!: derivative_intros continuous_at_imp_continuous_on isCont_sinc)
+    also have "\<dots> = (LBINT t=ereal (0 * -\<theta>)..T * -\<theta>. sin t / t)"
+      by (rule interval_integral_discrete_difference[of "{0}"]) auto
+    finally have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T * -\<theta>. sin t / t)"
+      by simp
+    hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
+       - (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)"
+      using assms `0 > \<theta>` unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
+        by (auto simp add: field_simps mult_le_0_iff split: split_if_asm)
+  } note aux2 = this
+  show ?thesis
+    using assms unfolding Si_def interval_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
+    apply auto
+    apply (erule aux1)
+    apply (rule aux2)
+    apply auto
+    done
+qed
+
+end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Probability/Weak_Convergence.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Weak_Convergence.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -0,0 +1,420 @@
+(*
+  Theory: Weak_Convergence.thy
+  Authors: Jeremy Avigad, Luke Serafin
+*)
+
+section \<open>Weak Convergence of Functions and Distributions\<close>
+
+text \<open>Properties of weak convergence of functions and measures, including the portmanteau theorem.\<close>
+
+theory Weak_Convergence
+  imports Distribution_Functions
+begin
+
+section \<open>Weak Convergence of Functions\<close>
+
+definition
+  weak_conv :: "(nat \<Rightarrow> (real \<Rightarrow> real)) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
+where
+  "weak_conv F_seq F \<equiv> \<forall>x. isCont F x \<longrightarrow> (\<lambda>n. F_seq n x) \<longlonglongrightarrow> F x"
+
+section \<open>Weak Convergence of Distributions\<close>
+
+definition
+  weak_conv_m :: "(nat \<Rightarrow> real measure) \<Rightarrow> real measure \<Rightarrow> bool"
+where
+  "weak_conv_m M_seq M \<equiv> weak_conv (\<lambda>n. cdf (M_seq n)) (cdf M)"
+
+section \<open>Skorohod's theorem\<close>
+
+locale right_continuous_mono = 
+  fixes f :: "real \<Rightarrow> real" and a b :: real
+  assumes cont: "\<And>x. continuous (at_right x) f"
+  assumes mono: "mono f"
+  assumes bot: "(f \<longlongrightarrow> a) at_bot" 
+  assumes top: "(f \<longlongrightarrow> b) at_top"
+begin
+
+abbreviation I :: "real \<Rightarrow> real" where
+  "I \<omega> \<equiv> Inf {x. \<omega> \<le> f x}"
+
+lemma pseudoinverse: assumes "a < \<omega>" "\<omega> < b" shows "\<omega> \<le> f x \<longleftrightarrow> I \<omega> \<le> x"
+proof
+  let ?F = "{x. \<omega> \<le> f x}"
+  obtain y where "f y < \<omega>"
+    by (metis eventually_happens' trivial_limit_at_bot_linorder order_tendstoD(2) bot \<open>a < \<omega>\<close>)
+  with mono have bdd: "bdd_below ?F"
+    by (auto intro!: bdd_belowI[of _ y] elim: mono_invE[OF _ less_le_trans])
+
+  have ne: "?F \<noteq> {}"
+    using order_tendstoD(1)[OF top \<open>\<omega> < b\<close>] 
+    by (auto dest!: eventually_happens'[OF trivial_limit_at_top_linorder] intro: less_imp_le)
+
+  show "\<omega> \<le> f x \<Longrightarrow> I \<omega> \<le> x"
+    by (auto intro!: cInf_lower bdd)
+
+  { assume *: "I \<omega> \<le> x"
+    have "\<omega> \<le> (INF s:{x. \<omega> \<le> f x}. f s)"
+      by (rule cINF_greatest[OF ne]) auto
+    also have "\<dots> = f (I \<omega>)"
+      using continuous_at_Inf_mono[OF mono cont ne bdd] ..
+    also have "\<dots> \<le> f x"
+      using * by (rule monoD[OF \<open>mono f\<close>])
+    finally show "\<omega> \<le> f x" . }
+qed
+
+lemma pseudoinverse': "\<forall>\<omega>\<in>{a<..<b}. \<forall>x. \<omega> \<le> f x \<longleftrightarrow> I \<omega> \<le> x"
+  by (intro ballI allI impI pseudoinverse) auto
+
+lemma mono_I: "mono_on I {a <..< b}"
+  unfolding mono_on_def by (metis order.trans order.refl pseudoinverse')
+
+end
+
+locale cdf_distribution = real_distribution
+begin
+
+abbreviation "C \<equiv> cdf M"
+
+sublocale right_continuous_mono C 0 1
+  by standard
+     (auto intro: cdf_nondecreasing cdf_is_right_cont cdf_lim_at_top_prob cdf_lim_at_bot monoI)
+
+lemma measurable_C[measurable]: "C \<in> borel_measurable borel"
+  by (intro borel_measurable_mono mono)
+
+lemma measurable_CI[measurable]: "I \<in> borel_measurable (restrict_space borel {0<..<1})"
+  by (intro borel_measurable_mono_on_fnc mono_I)
+
+lemma emeasure_distr_I: "emeasure (distr (restrict_space lborel {0<..<1::real}) borel I) UNIV = 1"
+  by (simp add: emeasure_distr space_restrict_space emeasure_restrict_space )
+
+lemma distr_I_eq_M: "distr (restrict_space lborel {0<..<1::real}) borel I = M" (is "?I = _")
+proof (intro cdf_unique ext)
+  let ?\<Omega> = "restrict_space lborel {0<..<1}::real measure"
+  interpret \<Omega>: prob_space ?\<Omega>
+    by (auto simp add: emeasure_restrict_space space_restrict_space intro!: prob_spaceI)
+  show "real_distribution ?I"
+    by auto
+
+  fix x
+  have "cdf ?I x = measure lborel {\<omega>\<in>{0<..<1}. \<omega> \<le> C x}"
+    by (subst cdf_def)
+       (auto simp: pseudoinverse[symmetric] measure_distr space_restrict_space measure_restrict_space
+             intro!: arg_cong2[where f="measure"])
+  also have "\<dots> = measure lborel {0 <..< C x}"
+    using cdf_bounded_prob[of x] AE_lborel_singleton[of "C x"]
+    by (auto intro!: arg_cong[where f=real_of_ereal] emeasure_eq_AE simp: measure_def)
+  also have "\<dots> = C x"
+    by (simp add: cdf_nonneg)
+  finally show "cdf (distr ?\<Omega> borel I) x = C x" .
+qed standard
+
+end
+
+context
+  fixes \<mu> :: "nat \<Rightarrow> real measure"
+    and M :: "real measure"
+  assumes \<mu>: "\<And>n. real_distribution (\<mu> n)" 
+  assumes M: "real_distribution M"
+  assumes \<mu>_to_M: "weak_conv_m \<mu> M"
+begin  
+
+(* state using obtains? *)
+theorem Skorohod:
+ "\<exists> (\<Omega> :: real measure) (Y_seq :: nat \<Rightarrow> real \<Rightarrow> real) (Y :: real \<Rightarrow> real). 
+    prob_space \<Omega> \<and>
+    (\<forall>n. Y_seq n \<in> measurable \<Omega> borel) \<and>
+    (\<forall>n. distr \<Omega> borel (Y_seq n) = \<mu> n) \<and>
+    Y \<in> measurable \<Omega> lborel \<and>
+    distr \<Omega> borel Y = M \<and>
+    (\<forall>x \<in> space \<Omega>. (\<lambda>n. Y_seq n x) \<longlonglongrightarrow> Y x)"
+proof -
+  interpret \<mu>: cdf_distribution "\<mu> n" for n
+    unfolding cdf_distribution_def by (rule \<mu>)
+  interpret M: cdf_distribution M
+    unfolding cdf_distribution_def by (rule M)
+
+  have conv: "measure M {x} = 0 \<Longrightarrow> (\<lambda>n. \<mu>.C n x) \<longlonglongrightarrow> M.C x" for x
+    using \<mu>_to_M M.isCont_cdf by (auto simp: weak_conv_m_def weak_conv_def)
+
+  let ?\<Omega> = "restrict_space lborel {0<..<1} :: real measure"
+  have "prob_space ?\<Omega>"
+    by (auto simp: space_restrict_space emeasure_restrict_space intro!: prob_spaceI)
+  interpret \<Omega>: prob_space ?\<Omega>
+    by fact
+
+  have Y_distr: "distr ?\<Omega> borel M.I = M"
+    by (rule M.distr_I_eq_M)
+
+  have Y_cts_cnv: "(\<lambda>n. \<mu>.I n \<omega>) \<longlonglongrightarrow> M.I \<omega>" 
+    if \<omega>: "\<omega> \<in> {0<..<1}" "isCont M.I \<omega>" for \<omega> :: real
+  proof (intro limsup_le_liminf_real)
+    show "liminf (\<lambda>n. \<mu>.I n \<omega>) \<ge> M.I \<omega>"
+      unfolding le_Liminf_iff
+    proof safe
+      fix B :: ereal assume B: "B < M.I \<omega>"
+      then show "\<forall>\<^sub>F n in sequentially. B < \<mu>.I n \<omega>"
+      proof (cases B)
+        case (real r)
+        with B have r: "r < M.I \<omega>"
+          by simp
+        then obtain x where x: "r < x" "x < M.I \<omega>" "measure M {x} = 0"
+          using open_minus_countable[OF M.countable_support, of "{r<..<M.I \<omega>}"] by auto
+        then have Fx_less: "M.C x < \<omega>"
+          using M.pseudoinverse' \<omega> not_less by blast
+
+        have "\<forall>\<^sub>F n in sequentially. \<mu>.C n x < \<omega>"
+          using order_tendstoD(2)[OF conv[OF x(3)] Fx_less] .
+        then have "\<forall>\<^sub>F n in sequentially. x < \<mu>.I n \<omega>"
+          by eventually_elim (insert \<omega> \<mu>.pseudoinverse[symmetric], simp add: not_le[symmetric])
+        then show ?thesis
+          by eventually_elim (insert x(1), simp add: real)
+      qed auto
+    qed
+
+    have *: "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> M.I \<omega>'"
+      if \<omega>': "0 < \<omega>'" "\<omega>' < 1" "\<omega> < \<omega>'" for \<omega>' :: real
+    proof (rule dense_ge_bounded)
+      fix B' assume "ereal (M.I \<omega>') < B'" "B' < ereal (M.I \<omega>' + 1)"
+      then obtain B where "M.I \<omega>' < B" and [simp]: "B' = ereal B"
+        by (cases B') auto
+      then obtain y where y: "M.I \<omega>' < y" "y < B" "measure M {y} = 0"
+        using open_minus_countable[OF M.countable_support, of "{M.I \<omega>'<..<B}"] by auto
+      then have "\<omega>' \<le> M.C (M.I \<omega>')"
+        using M.pseudoinverse' \<omega>' by (metis greaterThanLessThan_iff order_refl)
+      also have "... \<le> M.C y"
+        using M.mono y unfolding mono_def by auto
+      finally have Fy_gt: "\<omega> < M.C y"
+        using \<omega>'(3) by simp
+
+      have "\<forall>\<^sub>F n in sequentially. \<omega> \<le> \<mu>.C n y"
+        using order_tendstoD(1)[OF conv[OF y(3)] Fy_gt] by eventually_elim (rule less_imp_le)
+      then have 2: "\<forall>\<^sub>F n in sequentially. \<mu>.I n \<omega> \<le> ereal y"
+        by simp (subst \<mu>.pseudoinverse'[rule_format, OF \<omega>(1), symmetric])
+      then show "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> B'"
+        using \<open>y < B\<close>
+        by (intro Limsup_bounded[rotated]) (auto intro: le_less_trans elim: eventually_mono)
+    qed simp
+    
+    have **: "(M.I \<longlongrightarrow> ereal (M.I \<omega>)) (at_right \<omega>)"
+      using \<omega>(2) by (auto intro: tendsto_within_subset simp: continuous_at)
+    show "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> M.I \<omega>"
+      using \<omega>
+      by (intro tendsto_le_const[OF trivial_limit_at_right_real **])
+         (auto intro!: exI[of _ 1] * simp: eventually_at_right[of _ 1])
+  qed
+
+  let ?D = "{\<omega>\<in>{0<..<1}. \<not> isCont M.I \<omega>}"
+  have D_countable: "countable ?D"
+    using mono_on_ctble_discont[OF M.mono_I] by (simp add: at_within_open[of _ "{0 <..< 1}"] cong: conj_cong)
+  hence D: "emeasure ?\<Omega> ?D = 0"
+    using emeasure_lborel_countable[OF D_countable]
+    by (subst emeasure_restrict_space) auto
+
+  def Y' \<equiv> "\<lambda>\<omega>. if \<omega> \<in> ?D then 0 else M.I \<omega>"
+  have Y'_AE: "AE \<omega> in ?\<Omega>. Y' \<omega> = M.I \<omega>"
+    by (rule AE_I [OF _ D]) (auto simp: space_restrict_space sets_restrict_space_iff Y'_def)
+
+  def Y_seq' \<equiv> "\<lambda>n \<omega>. if \<omega> \<in> ?D then 0 else \<mu>.I n \<omega>"
+  have Y_seq'_AE: "\<And>n. AE \<omega> in ?\<Omega>. Y_seq' n \<omega> = \<mu>.I n \<omega>"
+    by (rule AE_I [OF _ D]) (auto simp: space_restrict_space sets_restrict_space_iff Y_seq'_def)
+
+  have Y'_cnv: "\<forall>\<omega>\<in>{0<..<1}. (\<lambda>n. Y_seq' n \<omega>) \<longlonglongrightarrow> Y' \<omega>"
+    by (auto simp: Y'_def Y_seq'_def Y_cts_cnv)
+
+  have [simp]: "Y_seq' n \<in> borel_measurable ?\<Omega>" for n
+    by (rule measurable_discrete_difference[of "\<mu>.I n" _ _ ?D])
+       (insert \<mu>.measurable_CI[of n] D_countable, auto simp: sets_restrict_space Y_seq'_def)
+  moreover have "distr ?\<Omega> borel (Y_seq' n) = \<mu> n" for n
+    using \<mu>.distr_I_eq_M [of n] Y_seq'_AE [of n]
+    by (subst distr_cong_AE[where f = "Y_seq' n" and g = "\<mu>.I n"], auto)
+  moreover have [simp]: "Y' \<in> borel_measurable ?\<Omega>"
+    by (rule measurable_discrete_difference[of M.I _ _ ?D])
+       (insert M.measurable_CI D_countable, auto simp: sets_restrict_space Y'_def)
+  moreover have "distr ?\<Omega> borel Y' = M"
+    using M.distr_I_eq_M Y'_AE
+    by (subst distr_cong_AE[where f = Y' and g = M.I], auto)
+  ultimately have "prob_space ?\<Omega> \<and> (\<forall>n. Y_seq' n \<in> borel_measurable ?\<Omega>) \<and>
+    (\<forall>n. distr ?\<Omega> borel (Y_seq' n) = \<mu> n) \<and> Y' \<in> measurable ?\<Omega> lborel \<and> distr ?\<Omega> borel Y' = M \<and>
+    (\<forall>x\<in>space ?\<Omega>. (\<lambda>n. Y_seq' n x) \<longlonglongrightarrow> Y' x)"
+    using Y'_cnv \<open>prob_space ?\<Omega>\<close> by (auto simp: space_restrict_space)
+  thus ?thesis by metis
+qed
+
+text \<open>
+  The Portmanteau theorem, that is, the equivalence of various definitions of weak convergence.
+\<close>
+
+theorem weak_conv_imp_bdd_ae_continuous_conv:
+  fixes 
+    f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  assumes 
+    discont_null: "M ({x. \<not> isCont f x}) = 0" and
+    f_bdd: "\<And>x. norm (f x) \<le> B" and
+    [measurable]: "f \<in> borel_measurable borel"
+  shows 
+    "(\<lambda> n. integral\<^sup>L (\<mu> n) f) \<longlonglongrightarrow> integral\<^sup>L M f"
+proof -
+  have "0 \<le> B"
+    using norm_ge_zero f_bdd by (rule order_trans)
+  note Skorohod
+  then obtain Omega Y_seq Y where
+    ps_Omega [simp]: "prob_space Omega" and
+    Y_seq_measurable [measurable]: "\<And>n. Y_seq n \<in> borel_measurable Omega" and
+    distr_Y_seq: "\<And>n. distr Omega borel (Y_seq n) = \<mu> n" and
+    Y_measurable [measurable]: "Y \<in> borel_measurable Omega" and
+    distr_Y: "distr Omega borel Y = M" and
+    YnY: "\<And>x :: real. x \<in> space Omega \<Longrightarrow> (\<lambda>n. Y_seq n x) \<longlonglongrightarrow> Y x"  by force
+  interpret prob_space Omega by fact
+  have *: "emeasure Omega (Y -` {x. \<not> isCont f x} \<inter> space Omega) = 0"
+    by (subst emeasure_distr [symmetric, where N=borel]) (auto simp: distr_Y discont_null)
+  have *: "AE x in Omega. (\<lambda>n. f (Y_seq n x)) \<longlonglongrightarrow> f (Y x)"
+    by (rule AE_I [OF _ *]) (auto intro: isCont_tendsto_compose YnY)
+  show ?thesis
+    by (auto intro!: integral_dominated_convergence[where w="\<lambda>x. B"]
+             simp: f_bdd * integral_distr distr_Y_seq [symmetric] distr_Y [symmetric])
+qed
+
+theorem weak_conv_imp_integral_bdd_continuous_conv:
+  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  assumes 
+    "\<And>x. isCont f x" and
+    "\<And>x. norm (f x) \<le> B"
+  shows 
+    "(\<lambda> n. integral\<^sup>L (\<mu> n) f) \<longlonglongrightarrow> integral\<^sup>L M f"
+  using assms
+  by (intro weak_conv_imp_bdd_ae_continuous_conv)
+     (auto intro!: borel_measurable_continuous_on1 continuous_at_imp_continuous_on)
+
+theorem weak_conv_imp_continuity_set_conv:
+  fixes f :: "real \<Rightarrow> real"
+  assumes [measurable]: "A \<in> sets borel" and "M (frontier A) = 0"
+  shows "(\<lambda>n. measure (\<mu> n) A) \<longlonglongrightarrow> measure M A"
+proof -
+  interpret M: real_distribution M by fact
+  interpret \<mu>: real_distribution "\<mu> n" for n by fact
+  
+  have "(\<lambda>n. (\<integral>x. indicator A x \<partial>\<mu> n) :: real) \<longlonglongrightarrow> (\<integral>x. indicator A x \<partial>M)"
+    by (intro weak_conv_imp_bdd_ae_continuous_conv[where B=1])
+       (auto intro: assms simp: isCont_indicator)
+  then show ?thesis
+    by simp
+qed
+
+end
+
+definition
+  cts_step :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
+where
+  "cts_step a b x \<equiv> if x \<le> a then 1 else if x \<ge> b then 0 else (b - x) / (b - a)"
+
+lemma cts_step_uniformly_continuous:
+  assumes [arith]: "a < b"
+  shows "uniformly_continuous_on UNIV (cts_step a b)"
+  unfolding uniformly_continuous_on_def
+proof clarsimp
+  fix e :: real assume [arith]: "0 < e"
+  let ?d = "min (e * (b - a)) (b - a)"
+  have "?d > 0"
+    by (auto simp add: field_simps)
+  moreover have "dist x' x < ?d \<Longrightarrow> dist (cts_step a b x') (cts_step a b x) < e" for x x'
+    by (auto simp: dist_real_def divide_simps cts_step_def)
+  ultimately show "\<exists>d > 0. \<forall>x x'. dist x' x < d \<longrightarrow> dist (cts_step a b x') (cts_step a b x) < e"
+    by blast
+qed
+
+lemma (in real_distribution) integrable_cts_step: "a < b \<Longrightarrow> integrable M (cts_step a b)"
+  by (rule integrable_const_bound [of _ 1]) (auto simp: cts_step_def[abs_def])
+
+lemma (in real_distribution) cdf_cts_step:
+  assumes [arith]: "x < y"
+  shows "cdf M x \<le> integral\<^sup>L M (cts_step x y)" and "integral\<^sup>L M (cts_step x y) \<le> cdf M y"
+proof -
+  have "cdf M x = integral\<^sup>L M (indicator {..x})"
+    by (simp add: cdf_def)
+  also have "\<dots> \<le> expectation (cts_step x y)"
+    by (intro integral_mono integrable_cts_step) (auto simp: cts_step_def split: split_indicator)
+  finally show "cdf M x \<le> expectation (cts_step x y)" .
+next
+  have "expectation (cts_step x y) \<le> integral\<^sup>L M (indicator {..y})"
+    by (intro integral_mono integrable_cts_step) (auto simp: cts_step_def split: split_indicator)
+  also have "\<dots> = cdf M y"
+    by (simp add: cdf_def)
+  finally show "expectation (cts_step x y) \<le> cdf M y" .
+qed
+
+context
+  fixes M_seq :: "nat \<Rightarrow> real measure"
+    and M :: "real measure"
+  assumes distr_M_seq [simp]: "\<And>n. real_distribution (M_seq n)" 
+  assumes distr_M [simp]: "real_distribution M"
+begin  
+
+theorem continuity_set_conv_imp_weak_conv:
+  fixes f :: "real \<Rightarrow> real"
+  assumes *: "\<And>A. A \<in> sets borel \<Longrightarrow> M (frontier A) = 0 \<Longrightarrow> (\<lambda> n. (measure (M_seq n) A)) \<longlonglongrightarrow> measure M A"
+  shows "weak_conv_m M_seq M"
+proof -
+  interpret real_distribution M by simp
+  show ?thesis
+    by (auto intro!: * simp: frontier_real_Iic isCont_cdf emeasure_eq_measure weak_conv_m_def weak_conv_def cdf_def2)
+qed
+
+theorem integral_cts_step_conv_imp_weak_conv:
+  assumes integral_conv: "\<And>x y. x < y \<Longrightarrow> (\<lambda>n. integral\<^sup>L (M_seq n) (cts_step x y)) \<longlonglongrightarrow> integral\<^sup>L M (cts_step x y)"
+  shows "weak_conv_m M_seq M"
+  unfolding weak_conv_m_def weak_conv_def 
+proof (clarsimp)
+  interpret real_distribution M by (rule distr_M) 
+  fix x assume "isCont (cdf M) x"
+  hence left_cont: "continuous (at_left x) (cdf M)"
+    unfolding continuous_at_split ..
+  { fix y :: real assume [arith]: "x < y"
+    have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> limsup (\<lambda>n. integral\<^sup>L (M_seq n) (cts_step x y))"
+      by (auto intro!: Limsup_mono always_eventually real_distribution.cdf_cts_step)
+    also have "\<dots> = integral\<^sup>L M (cts_step x y)"
+      by (intro lim_imp_Limsup) (auto intro: integral_conv)
+    also have "\<dots> \<le> cdf M y"
+      by (simp add: cdf_cts_step)
+    finally have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> cdf M y" .
+  } note * = this
+  { fix y :: real assume [arith]: "x > y"
+    have "cdf M y \<le> ereal (integral\<^sup>L M (cts_step y x))"
+      by (simp add: cdf_cts_step)
+    also have "\<dots> = liminf (\<lambda>n. integral\<^sup>L (M_seq n) (cts_step y x))"
+      by (intro lim_imp_Liminf[symmetric]) (auto intro: integral_conv)
+    also have "\<dots> \<le> liminf (\<lambda>n. cdf (M_seq n) x)"
+      by (auto intro!: Liminf_mono always_eventually real_distribution.cdf_cts_step)
+    finally have "liminf (\<lambda>n. cdf (M_seq n) x) \<ge> cdf M y" .
+  } note ** = this
+
+  have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> cdf M x"
+  proof (rule tendsto_le_const)
+    show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>xa. ereal (cdf (M_seq xa) x)) \<le> ereal (cdf M i)"
+      by (subst eventually_at_right[of _ "x + 1"]) (auto simp: * intro: exI [of _ "x+1"])
+  qed (insert cdf_is_right_cont, auto simp: continuous_within)
+  moreover have "cdf M x \<le> liminf (\<lambda>n. cdf (M_seq n) x)"
+  proof (rule tendsto_ge_const)
+    show "\<forall>\<^sub>F i in at_left x. ereal (cdf M i) \<le> liminf (\<lambda>xa. ereal (cdf (M_seq xa) x))"
+      by (subst eventually_at_left[of "x - 1"]) (auto simp: ** intro: exI [of _ "x-1"])
+  qed (insert left_cont, auto simp: continuous_within)
+  ultimately show "(\<lambda>n. cdf (M_seq n) x) \<longlonglongrightarrow> cdf M x"
+    by (elim limsup_le_liminf_real) 
+qed
+
+theorem integral_bdd_continuous_conv_imp_weak_conv:
+  assumes 
+    "\<And>f. (\<And>x. isCont f x) \<Longrightarrow> (\<And>x. abs (f x) \<le> 1) \<Longrightarrow> (\<lambda>n. integral\<^sup>L (M_seq n) f::real) \<longlonglongrightarrow> integral\<^sup>L M f"
+  shows 
+    "weak_conv_m M_seq M"
+  apply (rule integral_cts_step_conv_imp_weak_conv [OF assms])
+  apply (rule continuous_on_interior)
+  apply (rule uniformly_continuous_imp_continuous)
+  apply (rule cts_step_uniformly_continuous)
+  apply (auto simp: cts_step_def)
+  done
+
+end
+
+end
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Real.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -1583,7 +1583,6 @@
   "\<lceil>numeral x ^ n\<rceil> = numeral x ^ n"
   by (metis ceiling_of_int of_int_numeral of_int_power)
 
-
 subsection \<open>Implementation of rational real numbers\<close>
 
 text \<open>Formal constructor\<close>
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Set.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -989,6 +989,9 @@
 lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
   by blast
 
+lemma setcompr_eq_image: "{f x |x. P x} = f ` {x. P x}"
+  by auto
+
 lemma ball_imageD:
   assumes "\<forall>x\<in>f ` A. P x"
   shows "\<forall>x\<in>A. P (f x)"
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -453,6 +453,9 @@
   "x < y \<Longrightarrow> eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
   unfolding at_right_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)
 
+lemma eventually_at_right_less: "\<forall>\<^sub>F y in at_right (x::'a::{linorder_topology, no_top}). x < y"
+  using gt_ex[of x] eventually_at_right[of x] by auto
+
 lemma trivial_limit_at_right_top: "at_right (top::_::{order_top, linorder_topology}) = bot"
   unfolding filter_eq_iff eventually_at_topological by auto
 
@@ -1610,6 +1613,9 @@
 lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
   by (simp add: continuous_on_def continuous_at at_within_open[of _ s])
 
+lemma continuous_within_open: "a \<in> A \<Longrightarrow> open A \<Longrightarrow> continuous (at a within A) f \<longleftrightarrow> isCont f a"
+  by (simp add: at_within_open_NO_MATCH)
+
 lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
   by (auto intro: continuous_at_imp_continuous_at_within simp: continuous_on_eq_continuous_within)
 
diff -r 614ef6d7a6b6 -r 7582b39f51ed src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Transcendental.thy	Wed Jan 06 12:18:53 2016 +0100
@@ -10,6 +10,25 @@
 imports Binomial Series Deriv NthRoot
 begin
 
+text \<open>A fact theorem on reals.\<close>
+
+lemma square_fact_le_2_fact: 
+  shows "fact n * fact n \<le> (fact (2 * n) :: real)"
+proof (induct n)
+  case 0 then show ?case by simp
+next
+  case (Suc n)
+  have "(fact (Suc n)) * (fact (Suc n)) = of_nat (Suc n) * of_nat (Suc n) * (fact n * fact n :: real)"
+    by (simp add: field_simps)
+  also have "\<dots> \<le> of_nat (Suc n) * of_nat (Suc n) * fact (2 * n)"
+    by (rule mult_left_mono [OF Suc]) simp
+  also have "\<dots> \<le> of_nat (Suc (Suc (2 * n))) * of_nat (Suc (2 * n)) * fact (2 * n)"
+    by (rule mult_right_mono)+ (auto simp: field_simps)
+  also have "\<dots> = fact (2 * Suc n)" by (simp add: field_simps)
+  finally show ?case .
+qed
+
+
 lemma of_int_leD: 
   fixes x :: "'a :: linordered_idom"
   shows "\<bar>of_int n\<bar> \<le> x \<Longrightarrow> n=0 \<or> x\<ge>1"