isabelle: src/HOL/Probability/Distribution_Functions.thy@3b6a3632e754 (annotated)

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

author	hoelzl
	Fri, 30 Sep 2016 15:35:32 +0200
changeset 63970	3b6a3632e754
parent 63464	9d4dbb7a548a
child 63992	3aa9837d05c7
permissions	-rw-r--r--