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

63992 3aa9837d05c7 updated headers; wenzelm parents: 63970 diff changeset	1	(* Title: HOL/Probability/Distribution_Functions.thy
63329 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" +
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	39	assumes M_is_borel: "sets M = sets borel"
62083 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"
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	43	using M_is_borel by auto
62083 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"
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	60	by (metis in_mono sets.sets_into_space space_in_borel top_le M_is_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}"
68532 f8b98d31ad45 Incorporating new/strengthened proofs from Library and AFP entries paulson <lp15@cam.ac.uk> parents: 64321 diff changeset	110	using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
62083 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" +
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	145	assumes events_eq_borel [simp, measurable_cong]: "sets M = sets borel"
62083 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
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	148	lemma finite_borel_measure_M: "finite_borel_measure M"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	149	by standard auto
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	150
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	151	sublocale finite_borel_measure M
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	152	by (rule finite_borel_measure_M)
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	153
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	154	lemma space_eq_univ [simp]: "space M = UNIV"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	155	using events_eq_borel[THEN sets_eq_imp_space_eq] by simp
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	156
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	157	lemma cdf_bounded_prob: "\<And>x. cdf M x \<le> 1"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	158	by (subst prob_space [symmetric], rule cdf_bounded)
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 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	161	by (subst prob_space [symmetric], rule cdf_lim_infty)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	162
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62083 diff changeset	163	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	164	by (subst prob_space [symmetric], rule cdf_lim_at_top)
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 measurable_finite_borel [simp]:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	167	"f \<in> borel_measurable borel \<Longrightarrow> f \<in> borel_measurable M"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	168	by (rule borel_measurable_subalgebra[where N=borel]) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	169
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	170	end
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 prob_space) real_distribution_distr [intro, simp]:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	173	"random_variable borel X \<Longrightarrow> real_distribution (distr M borel X)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	174	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	175
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	176	subsection \<open>Uniqueness\<close>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	177
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	178	lemma (in finite_borel_measure) emeasure_Ioc:
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	179	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	180	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	181	have "{a <.. b} = {..b} - {..a}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	182	by auto
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	183	moreover have "{..x} \<in> sets M" for x
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	184	using atMost_borel[of x] M_is_borel by auto
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	185	moreover note \<open>a \<le> b\<close>
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	186	ultimately show ?thesis
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	187	by (simp add: emeasure_eq_measure finite_measure_Diff cdf_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	188	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	189
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	190	lemma cdf_unique':
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	191	fixes M1 M2
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	192	assumes "finite_borel_measure M1" and "finite_borel_measure M2"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	193	assumes "cdf M1 = cdf M2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	194	shows "M1 = M2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	195	proof (rule measure_eqI_generator_eq[where \<Omega>=UNIV])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	196	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	197	then obtain a b where Xeq: "X = {a<..b}" by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	198	then show "emeasure M1 X = emeasure M2 X"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	199	by (cases "a \<le> b")
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	200	(simp_all add: assms(1,2)[THEN finite_borel_measure.emeasure_Ioc] assms(3))
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	201	next
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	202	show "(\<Union>i. {- real (i::nat)<..real i}) = UNIV"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	203	by (rule UN_Ioc_eq_UNIV)
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	204	qed (auto simp: finite_borel_measure.emeasure_Ioc[OF assms(1)]
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	205	assms(1,2)[THEN finite_borel_measure.M_is_borel] borel_sigma_sets_Ioc
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	206	Int_stable_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	207
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	208	lemma cdf_unique:
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	209	"real_distribution M1 \<Longrightarrow> real_distribution M2 \<Longrightarrow> cdf M1 = cdf M2 \<Longrightarrow> M1 = M2"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	210	using cdf_unique'[of M1 M2] by (simp add: real_distribution.finite_borel_measure_M)
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	211
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	212	lemma
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	213	fixes F :: "real \<Rightarrow> real"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	214	assumes nondecF : "\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	215	and right_cont_F : "\<And>a. continuous (at_right a) F"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	216	and lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	217	and lim_F_at_top : "(F \<longlongrightarrow> m) at_top"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	218	and m: "0 \<le> m"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	219	shows interval_measure_UNIV: "emeasure (interval_measure F) UNIV = m"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	220	and finite_borel_measure_interval_measure: "finite_borel_measure (interval_measure F)"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	221	proof -
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	222	let ?F = "interval_measure F"
69260 0a9688695a1b removed relics of ASCII syntax for indexed big operators haftmann parents: 68532 diff changeset	223	{ have "ennreal (m - 0) = (SUP i. ennreal (F (real i) - F (- real i)))"
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	224	by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	225	lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	226	lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	227	filterlim_uminus_at_top[THEN iffD1])
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	228	(auto simp: incseq_def nondecF intro!: diff_mono)
69260 0a9688695a1b removed relics of ASCII syntax for indexed big operators haftmann parents: 68532 diff changeset	229	also have "\<dots> = (SUP i. emeasure ?F {- real i<..real i})"
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	230	by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	231	also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	232	by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	233	also have "(\<Union>i. {- real (i::nat)<..real i}) = space ?F"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	234	by (simp add: UN_Ioc_eq_UNIV)
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	235	finally have "emeasure ?F (space ?F) = m"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	236	by simp }
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	237	note * = this
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	238	then show "emeasure (interval_measure F) UNIV = m"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	239	by simp
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	240
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	241	interpret finite_measure ?F
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	242	proof
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	243	show "emeasure ?F (space ?F) \<noteq> \<infinity>"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	244	using * by simp
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	245	qed
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	246	show "finite_borel_measure (interval_measure F)"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	247	proof qed simp_all
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	248	qed
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	249
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	250	lemma real_distribution_interval_measure:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	251	fixes F :: "real \<Rightarrow> real"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	252	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	253	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	254	lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot" and
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	255	lim_F_at_top : "(F \<longlongrightarrow> 1) at_top"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	256	shows "real_distribution (interval_measure F)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	257	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	258	let ?F = "interval_measure F"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	259	interpret prob_space ?F
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	260	proof qed (use interval_measure_UNIV[OF assms] in simp)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	261	show ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	262	proof qed simp_all
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	263	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	264
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	265	lemma
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	266	fixes F :: "real \<Rightarrow> real"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	267	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	268	right_cont_F : "\<And>a. continuous (at_right a) F" and
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	269	lim_F_at_bot : "(F \<longlongrightarrow> 0) at_bot"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	270	shows emeasure_interval_measure_Iic: "emeasure (interval_measure F) {.. x} = F x"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	271	and measure_interval_measure_Iic: "measure (interval_measure F) {.. x} = F x"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	272	unfolding cdf_def
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	273	proof -
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	274	have F_nonneg[simp]: "0 \<le> F y" for y
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	275	using lim_F_at_bot by (rule tendsto_upperbound) (auto simp: eventually_at_bot_linorder nondecF intro!: exI[of _ y])
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	276
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	277	have "emeasure (interval_measure F) (\<Union>i::nat. {-real i <.. x}) = F x - ennreal 0"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	278	proof (intro LIMSEQ_unique[OF Lim_emeasure_incseq])
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	279	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	280	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	281	filterlim_uminus_at_top[THEN iffD1])
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	282	from tendsto_ennrealI[OF this]
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	283	show "(\<lambda>i. emeasure (interval_measure F) {- real i<..x}) \<longlonglongrightarrow> F x - ennreal 0"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	284	apply (rule filterlim_cong[THEN iffD1, rotated 3])
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	285	apply simp
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	286	apply simp
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	287	apply (rule eventually_sequentiallyI[where c="nat (ceiling (- x))"])
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	288	apply (simp add: emeasure_interval_measure_Ioc right_cont_F nondecF)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	289	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	290	qed (auto simp: incseq_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	291	also have "(\<Union>i::nat. {-real i <.. x}) = {..x}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	292	by auto (metis minus_minus neg_less_iff_less reals_Archimedean2)
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	293	finally show "emeasure (interval_measure F) {..x} = F x"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	294	by simp
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	295	then show "measure (interval_measure F) {..x} = F x"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	296	by (simp add: measure_def)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	297	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	298
64321 95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	299	lemma cdf_interval_measure:
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	300	"(\<And> x y. x \<le> y \<Longrightarrow> F x \<le> F y) \<Longrightarrow> (\<And>a. continuous (at_right a) F) \<Longrightarrow> (F \<longlongrightarrow> 0) at_bot \<Longrightarrow> cdf (interval_measure F) = F"
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	301	by (simp add: cdf_def fun_eq_iff measure_interval_measure_Iic)
95be866e49fc HOL-Probability: generalize theorems about cumulative distribution function hoelzl parents: 63992 diff changeset	302
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	303	end

author	wenzelm
	Sun, 03 Sep 2023 16:44:07 +0200
changeset 78639	ca56952b7322
parent 69260	0a9688695a1b
permissions	-rw-r--r--