isabelle: src/HOL/Probability/Distribution_Functions.thy@0909deb8059b (annotated)

62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	1	(*
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	2	Title : Distribution_Functions.thy
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	3	Authors : Jeremy Avigad and Luke Serafin
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	4	*)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	5
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	6	section \<open>Distribution Functions\<close>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	7
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	8	text \<open>
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	9	Shows that the cumulative distribution function (cdf) of a distribution (a measure on the reals) is
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	10	nondecreasing and right continuous, which tends to 0 and 1 in either direction.
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	11
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	12	Conversely, every such function is the cdf of a unique distribution. This direction defines the
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	13	measure in the obvious way on half-open intervals, and then applies the Caratheodory extension
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	14	theorem.
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	15	\<close>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	16
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	17	(* TODO: the locales "finite_borel_measure" and "real_distribution" are defined here, but maybe they
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	18	should be somewhere else. *)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	19
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	20	theory Distribution_Functions
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	21	imports Probability_Measure "~~/src/HOL/Library/ContNotDenum"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	22	begin
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	23
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	24	lemma UN_Ioc_eq_UNIV: "(\<Union>n. { -real n <.. real n}) = UNIV"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	25	by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	26	(metis le_less_trans minus_minus neg_less_iff_less not_le real_arch_simple
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	27	of_nat_0_le_iff reals_Archimedean2)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	28
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 63092 diff changeset	29	subsection \<open>Properties of cdf's\<close>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	30
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	31	definition
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	32	cdf :: "real measure \<Rightarrow> real \<Rightarrow> real"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	33	where
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	34	"cdf M \<equiv> \<lambda>x. measure M {..x}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	35
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	36	lemma cdf_def2: "cdf M x = measure M {..x}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	37	by (simp add: cdf_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	38
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	39	locale finite_borel_measure = finite_measure M for M :: "real measure" +
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	40	assumes M_super_borel: "sets borel \<subseteq> sets M"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	41	begin
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	42
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	43	lemma sets_M[intro]: "a \<in> sets borel \<Longrightarrow> a \<in> sets M"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	44	using M_super_borel by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	45
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	46	lemma cdf_diff_eq:
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	47	assumes "x < y"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	48	shows "cdf M y - cdf M x = measure M {x<..y}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	49	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	50	from assms have *: "{..x} \<union> {x<..y} = {..y}" by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	51	have "measure M {..y} = measure M {..x} + measure M {x<..y}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	52	by (subst finite_measure_Union [symmetric], auto simp add: *)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	53	thus ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	54	unfolding cdf_def by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	55	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	56
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	57	lemma cdf_nondecreasing: "x \<le> y \<Longrightarrow> cdf M x \<le> cdf M y"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	58	unfolding cdf_def by (auto intro!: finite_measure_mono)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	59
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	60	lemma borel_UNIV: "space M = UNIV"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	61	by (metis in_mono sets.sets_into_space space_in_borel top_le M_super_borel)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	62
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	63	lemma cdf_nonneg: "cdf M x \<ge> 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	64	unfolding cdf_def by (rule measure_nonneg)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	65
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	66	lemma cdf_bounded: "cdf M x \<le> measure M (space M)"
63092 a949b2a5f51d eliminated use of empty "assms"; wenzelm parents: 62975 diff changeset	67	unfolding cdf_def by (intro bounded_measure)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	68
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	69	lemma cdf_lim_infty:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	70	"((\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> measure M (space M))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	71	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	72	have "(\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> measure M (\<Union> i::nat. {..real i})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	73	unfolding cdf_def by (rule finite_Lim_measure_incseq) (auto simp: incseq_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	74	also have "(\<Union> i::nat. {..real i}) = space M"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	75	by (auto simp: borel_UNIV intro: real_arch_simple)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	76	finally show ?thesis .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	77	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	78
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	79	lemma cdf_lim_at_top: "(cdf M \<longlongrightarrow> measure M (space M)) at_top"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	80	by (rule tendsto_at_topI_sequentially_real)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	81	(simp_all add: mono_def cdf_nondecreasing cdf_lim_infty)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	82
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	83	lemma cdf_lim_neg_infty: "((\<lambda>i. cdf M (- real i)) \<longlonglongrightarrow> 0)"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	84	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	85	have "(\<lambda>i. cdf M (- real i)) \<longlonglongrightarrow> measure M (\<Inter> i::nat. {.. - real i })"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	86	unfolding cdf_def by (rule finite_Lim_measure_decseq) (auto simp: decseq_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	87	also have "(\<Inter> i::nat. {..- real i}) = {}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	88	by auto (metis leD le_minus_iff reals_Archimedean2)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	89	finally show ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	90	by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	91	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	92
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	93	lemma cdf_lim_at_bot: "(cdf M \<longlongrightarrow> 0) at_bot"
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	94	proof -
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	95	have *: "((\<lambda>x :: real. - cdf M (- x)) \<longlongrightarrow> 0) at_top"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	96	by (intro tendsto_at_topI_sequentially_real monoI)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	97	(auto simp: cdf_nondecreasing cdf_lim_neg_infty tendsto_minus_cancel_left[symmetric])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	98	from filterlim_compose [OF *, OF filterlim_uminus_at_top_at_bot]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	99	show ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	100	unfolding tendsto_minus_cancel_left[symmetric] by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	101	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	102
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	103	lemma cdf_is_right_cont: "continuous (at_right a) (cdf M)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	104	unfolding continuous_within
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	105	proof (rule tendsto_at_right_sequentially[where b="a + 1"])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	106	fix f :: "nat \<Rightarrow> real" and x assume f: "decseq f" "f \<longlonglongrightarrow> a"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	107	then have "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> measure M (\<Inter>i. {.. f i})"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 63092 diff changeset	108	using \<open>decseq f\<close> unfolding cdf_def
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	109	by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	110	also have "(\<Inter>i. {.. f i}) = {.. a}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	111	using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	112	finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	113	by (simp add: cdf_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	114	qed simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	115
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	116	lemma cdf_at_left: "(cdf M \<longlongrightarrow> measure M {..<a}) (at_left a)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	117	proof (rule tendsto_at_left_sequentially[of "a - 1"])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	118	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"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	119	then have "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> measure M (\<Union>i. {.. f i})"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 63092 diff changeset	120	using \<open>incseq f\<close> unfolding cdf_def
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	121	by (intro finite_Lim_measure_incseq) (auto simp: incseq_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	122	also have "(\<Union>i. {.. f i}) = {..<a}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	123	by (auto dest!: order_tendstoD(1)[OF f(2)] eventually_happens'[OF sequentially_bot]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	124	intro: less_imp_le le_less_trans f(3))
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	125	finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> measure M {..<a}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	126	by (simp add: cdf_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	127	qed auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	128
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	129	lemma isCont_cdf: "isCont (cdf M) x \<longleftrightarrow> measure M {x} = 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	130	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	131	have "isCont (cdf M) x \<longleftrightarrow> cdf M x = measure M {..<x}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	132	by (auto simp: continuous_at_split cdf_is_right_cont continuous_within[where s="{..< _}"]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	133	cdf_at_left tendsto_unique[OF _ cdf_at_left])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	134	also have "cdf M x = measure M {..<x} \<longleftrightarrow> measure M {x} = 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	135	unfolding cdf_def ivl_disj_un(2)[symmetric]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	136	by (subst finite_measure_Union) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	137	finally show ?thesis .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	138	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	139
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	140	lemma countable_atoms: "countable {x. measure M {x} > 0}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	141	using countable_support unfolding zero_less_measure_iff .
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	142
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	143	end
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	144
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	145	locale real_distribution = prob_space M for M :: "real measure" +
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	146	assumes events_eq_borel [simp, measurable_cong]: "sets M = sets borel" and space_eq_univ [simp]: "space M = UNIV"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	147	begin
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	148
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	149	sublocale finite_borel_measure M
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	150	by standard auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	151
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	152	lemma cdf_bounded_prob: "\<And>x. cdf M x \<le> 1"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	153	by (subst prob_space [symmetric], rule cdf_bounded)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	154
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	155	lemma cdf_lim_infty_prob: "(\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> 1"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	156	by (subst prob_space [symmetric], rule cdf_lim_infty)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	157
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	158	lemma cdf_lim_at_top_prob: "(cdf M \<longlongrightarrow> 1) at_top"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	159	by (subst prob_space [symmetric], rule cdf_lim_at_top)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	160
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	161	lemma measurable_finite_borel [simp]:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	162	"f \<in> borel_measurable borel \<Longrightarrow> f \<in> borel_measurable M"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	163	by (rule borel_measurable_subalgebra[where N=borel]) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	164
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	165	end
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	166
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	167	lemma (in prob_space) real_distribution_distr [intro, simp]:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	168	"random_variable borel X \<Longrightarrow> real_distribution (distr M borel X)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	169	unfolding real_distribution_def real_distribution_axioms_def by (auto intro!: prob_space_distr)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	170
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 63092 diff changeset	171	subsection \<open>uniqueness\<close>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	172
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	173	lemma (in real_distribution) emeasure_Ioc:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	174	assumes "a \<le> b" shows "emeasure M {a <.. b} = cdf M b - cdf M a"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	175	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	176	have "{a <.. b} = {..b} - {..a}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	177	by auto
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 63092 diff changeset	178	with \<open>a \<le> b\<close> show ?thesis
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	179	by (simp add: emeasure_eq_measure finite_measure_Diff cdf_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	180	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	181
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	182	lemma cdf_unique:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	183	fixes M1 M2
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	184	assumes "real_distribution M1" and "real_distribution M2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	185	assumes "cdf M1 = cdf M2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	186	shows "M1 = M2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	187	proof (rule measure_eqI_generator_eq[where \<Omega>=UNIV])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	188	fix X assume "X \<in> range (\<lambda>(a, b). {a<..b::real})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	189	then obtain a b where Xeq: "X = {a<..b}" by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	190	then show "emeasure M1 X = emeasure M2 X"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	191	by (cases "a \<le> b")
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	192	(simp_all add: assms(1,2)[THEN real_distribution.emeasure_Ioc] assms(3))
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	193	next
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	194	show "(\<Union>i. {- real (i::nat)<..real i}) = UNIV"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	195	by (rule UN_Ioc_eq_UNIV)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	196	qed (auto simp: real_distribution.emeasure_Ioc[OF assms(1)]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	197	assms(1,2)[THEN real_distribution.events_eq_borel] borel_sigma_sets_Ioc
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	198	Int_stable_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	199
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	200	lemma real_distribution_interval_measure:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	201	fixes F :: "real \<Rightarrow> real"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	202	assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y" and
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	203	right_cont_F : "\<And>a. continuous (at_right a) F" and
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	204	lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot" and
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	205	lim_F_at_top : "(F \<longlongrightarrow> 1) at_top"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	206	shows "real_distribution (interval_measure F)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	207	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	208	let ?F = "interval_measure F"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	209	interpret prob_space ?F
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	210	proof
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	211	have "ennreal (1 - 0) = (SUP i::nat. ennreal (F (real i) - F (- real i)))"
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	212	by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	213	lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	214	lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	215	filterlim_uminus_at_top[THEN iffD1])
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	216	(auto simp: incseq_def nondecF intro!: diff_mono)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	217	also have "\<dots> = (SUP i::nat. emeasure ?F {- real i<..real i})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	218	by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	219	also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	220	by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	221	also have "(\<Union>i. {- real (i::nat)<..real i}) = space ?F"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	222	by (simp add: UN_Ioc_eq_UNIV)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	223	finally show "emeasure ?F (space ?F) = 1"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	224	by (simp add: one_ereal_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	225	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	226	show ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	227	proof qed simp_all
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	228	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	229
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	230	lemma cdf_interval_measure:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	231	fixes F :: "real \<Rightarrow> real"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	232	assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y" and
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	233	right_cont_F : "\<And>a. continuous (at_right a) F" and
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	234	lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot" and
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	235	lim_F_at_top : "(F \<longlongrightarrow> 1) at_top"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	236	shows "cdf (interval_measure F) = F"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	237	unfolding cdf_def
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	238	proof (intro ext)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	239	interpret real_distribution "interval_measure F"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	240	by (rule real_distribution_interval_measure) fact+
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	241	fix x
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	242	have "F x - 0 = measure (interval_measure F) (\<Union>i::nat. {-real i <.. x})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	243	proof (intro LIMSEQ_unique[OF _ finite_Lim_measure_incseq])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	244	have "(\<lambda>i. F x - F (- real i)) \<longlonglongrightarrow> F x - 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	245	by (intro tendsto_intros lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	246	filterlim_uminus_at_top[THEN iffD1])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	247	then show "(\<lambda>i. measure (interval_measure F) {- real i<..x}) \<longlonglongrightarrow> F x - 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	248	apply (rule filterlim_cong[OF refl refl, THEN iffD1, rotated])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	249	apply (rule eventually_sequentiallyI[where c="nat (ceiling (- x))"])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	250	apply (simp add: measure_interval_measure_Ioc right_cont_F nondecF)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	251	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	252	qed (auto simp: incseq_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	253	also have "(\<Union>i::nat. {-real i <.. x}) = {..x}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	254	by auto (metis minus_minus neg_less_iff_less reals_Archimedean2)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	255	finally show "measure (interval_measure F) {..x} = F x"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	256	by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	257	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	258
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	259	end

author	wenzelm
	Thu, 26 May 2016 17:51:22 +0200
changeset 63167	0909deb8059b
parent 63092	a949b2a5f51d
child 63329	6b26c378ab35
permissions	-rw-r--r--