--- 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.
--- 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.
--- 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
--- 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
--- 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")
--- 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]:
--- 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 =
--- 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
--- 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)
--- 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)
--- /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
--- /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
--- /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
--- /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
--- 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"
--- 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"
--- /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
--- 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
--- 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
-
--- 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))"
--- 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"
--- 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
--- 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)"
--- 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)
--- /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
--- /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
--- 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>
--- 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)"
--- 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)
--- 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"