isabelle: src/HOL/Probability/Levy.thy@c72fd8f1fceb (annotated)

63329 6b26c378ab35 Probability: tuned headers; cleanup Radon_Nikodym hoelzl parents: 63167 diff changeset	1	(* Title: HOL/Probability/Levy.thy
6b26c378ab35 Probability: tuned headers; cleanup Radon_Nikodym hoelzl parents: 63167 diff changeset	2	Authors: Jeremy Avigad (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>The Levy inversion theorem, and the Levy continuity theorem.\<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	theory Levy
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	8	imports Characteristic_Functions Helly_Selection Sinc_Integral
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	9	begin
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	10
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	11	subsection \<open>The Levy inversion theorem\<close>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	12
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	13	(* Actually, this is not needed for us -- but it is useful for other purposes. (See Billingsley.) *)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	14	lemma Levy_Inversion_aux1:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	15	fixes a b :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	16	assumes "a \<le> b"
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	17	shows "((\<lambda>t. (iexp (-(t * a)) - iexp (-(t * b))) / (\<i> * t)) \<longlongrightarrow> b - a) (at 0)"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	18	(is "(?F \<longlongrightarrow> _) (at _)")
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	19	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	20	have 1: "cmod (?F t - (b - a)) \<le> a^2 / 2 * abs t + b^2 / 2 * abs t" if "t \<noteq> 0" for t
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	21	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	22	have "cmod (?F t - (b - a)) = cmod (
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	23	(iexp (-(t * a)) - (1 + \<i> * -(t * a))) / (\<i> * t) -
58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	24	(iexp (-(t * b)) - (1 + \<i> * -(t * b))) / (\<i> * t))"
58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	25	(is "_ = cmod (?one / (\<i> * t) - ?two / (\<i> * t))")
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	26	using \<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps)
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	27	also have "\<dots> \<le> cmod (?one / (\<i> * t)) + cmod (?two / (\<i> * t))"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	28	by (rule norm_triangle_ineq4)
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	29	also have "cmod (?one / (\<i> * t)) = cmod ?one / abs t"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	30	by (simp add: norm_divide norm_mult)
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	31	also have "cmod (?two / (\<i> * t)) = cmod ?two / abs t"
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	32	by (simp add: norm_divide norm_mult)
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	33	also have "cmod ?one / abs t + cmod ?two / abs t \<le>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	34	((- (a * t))^2 / 2) / abs t + ((- (b * t))^2 / 2) / abs t"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	35	apply (rule add_mono)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	36	apply (rule divide_right_mono)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	37	using iexp_approx1 [of "-(t * a)" 1] apply (simp add: field_simps eval_nat_numeral)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	38	apply force
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	39	apply (rule divide_right_mono)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	40	using iexp_approx1 [of "-(t * b)" 1] apply (simp add: field_simps eval_nat_numeral)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	41	by force
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	42	also have "\<dots> = a^2 / 2 * abs t + b^2 / 2 * abs t"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	43	using \<open>t \<noteq> 0\<close> apply (case_tac "t \<ge> 0", simp add: field_simps power2_eq_square)
0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	44	using \<open>t \<noteq> 0\<close> by (subst (1 2) abs_of_neg, auto simp add: field_simps power2_eq_square)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	45	finally show "cmod (?F t - (b - a)) \<le> a^2 / 2 * abs t + b^2 / 2 * abs t" .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	46	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	47	show ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	48	apply (rule LIM_zero_cancel)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	49	apply (rule tendsto_norm_zero_cancel)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	50	apply (rule real_LIM_sandwich_zero [OF _ _ 1])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	51	apply (auto intro!: tendsto_eq_intros)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	52	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	53	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	54
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	55	lemma Levy_Inversion_aux2:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	56	fixes a b t :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	57	assumes "a \<le> b" and "t \<noteq> 0"
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	58	shows "cmod ((iexp (t * b) - iexp (t * a)) / (\<i> * t)) \<le> b - a" (is "?F \<le> _")
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	59	proof -
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	60	have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (\<i> * t))"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	61	using \<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps exp_diff exp_minus)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	62	also have "\<dots> = cmod (iexp (t * (b - a)) - 1) / abs t"
65064 a4abec71279a Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands paulson <lp15@cam.ac.uk> parents: 64284 diff changeset	63	unfolding norm_divide norm_mult norm_exp_i_times using \<open>t \<noteq> 0\<close>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	64	by (simp add: complex_eq_iff norm_mult)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	65	also have "\<dots> \<le> abs (t * (b - a)) / abs t"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	66	using iexp_approx1 [of "t * (b - a)" 0]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	67	by (intro divide_right_mono) (auto simp add: field_simps eval_nat_numeral)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	68	also have "\<dots> = b - a"
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	69	using assms by (auto simp add: abs_mult)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	70	finally show ?thesis .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	71	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	72
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	73	(* TODO: refactor! *)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	74	theorem (in real_distribution) Levy_Inversion:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	75	fixes a b :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	76	assumes "a \<le> b"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	77	defines "\<mu> \<equiv> measure M" and "\<phi> \<equiv> char M"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	78	assumes "\<mu> {a} = 0" and "\<mu> {b} = 0"
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	79	shows "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. (iexp (-(t * a)) - iexp (-(t * b))) / (\<i> * t) * \<phi> t))
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	80	\<longlonglongrightarrow> \<mu> {a<..b}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	81	(is "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. ?F t * \<phi> t)) \<longlonglongrightarrow> of_real (\<mu> {a<..b})")
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	82	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	83	interpret P: pair_sigma_finite lborel M ..
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	84	from bounded_Si obtain B where Bprop: "\<And>T. abs (Si T) \<le> B" by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	85	from Bprop [of 0] have [simp]: "B \<ge> 0" by auto
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	86	let ?f = "\<lambda>t x :: real. (iexp (t * (x - a)) - iexp(t * (x - b))) / (\<i> * t)"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	87	{ fix T :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	88	assume "T \<ge> 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	89	let ?f' = "\<lambda>(t, x). indicator {-T<..<T} t *\<^sub>R ?f t x"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	90	{ fix x
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	91	have 1: "complex_interval_lebesgue_integrable lborel u v (\<lambda>t. ?f t x)" for u v :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	92	using Levy_Inversion_aux2[of "x - b" "x - a"]
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	93	apply (simp add: interval_lebesgue_integrable_def set_integrable_def del: times_divide_eq_left)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	94	apply (intro integrableI_bounded_set_indicator[where B="b - a"] conjI impI)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	95	apply (auto intro!: AE_I [of _ _ "{0}"] simp: assms)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	96	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	97	have "(CLBINT t. ?f' (t, x)) = (CLBINT t=-T..T. ?f t x)"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	98	using \<open>T \<ge> 0\<close> by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	99	also have "\<dots> = (CLBINT t=-T..(0 :: real). ?f t x) + (CLBINT t=(0 :: real)..T. ?f t x)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	100	(is "_ = _ + ?t")
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	101	using 1 by (intro interval_integral_sum[symmetric]) (simp add: min_absorb1 max_absorb2 \<open>T \<ge> 0\<close>)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	102	also have "(CLBINT t=-T..(0 :: real). ?f t x) = (CLBINT t=(0::real)..T. ?f (-t) x)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	103	by (subst interval_integral_reflect) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	104	also have "\<dots> + ?t = (CLBINT t=(0::real)..T. ?f (-t) x + ?f t x)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	105	using 1
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	106	by (intro interval_lebesgue_integral_add(2) [symmetric] interval_integrable_mirror[THEN iffD2]) simp_all
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	107	also have "\<dots> = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) -
63589 58aab4745e85 more symbols; wenzelm parents: 63540 diff changeset	108	(iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (\<i> * t))"
70817 dd675800469d dedicated fact collections for algebraic simplification rules potentially splitting goals haftmann parents: 67977 diff changeset	109	using \<open>T \<ge> 0\<close> by (intro interval_integral_cong) (auto simp add: field_split_simps)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	110	also have "\<dots> = (CLBINT t=(0::real)..T. complex_of_real(
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	111	2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t)))"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	112	using \<open>T \<ge> 0\<close>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	113	apply (intro interval_integral_cong)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	114	apply (simp add: field_simps cis.ctr Im_divide Re_divide Im_exp Re_exp complex_eq_iff)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	115	unfolding minus_diff_eq[symmetric, of "y * x" "y * a" for y a] sin_minus cos_minus
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	116	apply (simp add: field_simps power2_eq_square)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	117	done
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	118	also have "\<dots> = complex_of_real (LBINT t=(0::real)..T.
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	119	2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	120	by (rule interval_lebesgue_integral_of_real)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	121	also have "\<dots> = complex_of_real (2 * (sgn (x - a) * Si (T * abs (x - a)) -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	122	sgn (x - b) * Si (T * abs (x - b))))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	123	apply (subst interval_lebesgue_integral_diff)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	124	apply (rule interval_lebesgue_integrable_mult_right, rule integrable_sinc')+
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	125	apply (subst interval_lebesgue_integral_mult_right)+
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	126	apply (simp add: zero_ereal_def[symmetric] LBINT_I0c_sin_scale_divide[OF \<open>T \<ge> 0\<close>])
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	127	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	128	finally have "(CLBINT t. ?f' (t, x)) =
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	129	2 * (sgn (x - a) * Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))" .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	130	} note main_eq = this
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	131	have "(CLBINT t=-T..T. ?F t * \<phi> t) =
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	132	(CLBINT t. (CLINT x \| M. ?F t * iexp (t * x) * indicator {-T<..<T} t))"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	133	using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def set_lebesgue_integral_def
63886 685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel hoelzl parents: 63589 diff changeset	134	by (auto split: split_indicator intro!: Bochner_Integration.integral_cong)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	135	also have "\<dots> = (CLBINT t. (CLINT x \| M. ?f' (t, x)))"
63886 685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel hoelzl parents: 63589 diff changeset	136	by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	137	also have "\<dots> = (CLINT x \| M. (CLBINT t. ?f' (t, x)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	138	proof (intro P.Fubini_integral [symmetric] integrableI_bounded_set [where B="b - a"])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	139	show "emeasure (lborel \<Otimes>\<^sub>M M) ({- T<..<T} \<times> space M) < \<infinity>"
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	140	using \<open>T \<ge> 0\<close>
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	141	by (subst emeasure_pair_measure_Times)
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	142	(auto simp: ennreal_mult_less_top not_less top_unique)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	143	show "AE x\<in>{- T<..<T} \<times> space M in lborel \<Otimes>\<^sub>M M. cmod (case x of (t, x) \<Rightarrow> ?f' (t, x)) \<le> b - a"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	144	using Levy_Inversion_aux2[of "x - b" "x - a" for x] \<open>a \<le> b\<close>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	145	by (intro AE_I [of _ _ "{0} \<times> UNIV"]) (force simp: emeasure_pair_measure_Times)+
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	146	qed (auto split: split_indicator split_indicator_asm)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	147	also have "\<dots> = (CLINT x \| M. (complex_of_real (2 * (sgn (x - a) *
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	148	Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))))"
63886 685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel hoelzl parents: 63589 diff changeset	149	using main_eq by (intro Bochner_Integration.integral_cong, auto)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	150	also have "\<dots> = complex_of_real (LINT x \| M. (2 * (sgn (x - a) *
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	151	Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	152	by (rule integral_complex_of_real)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	153	finally have "(CLBINT t=-T..T. ?F t * \<phi> t) =
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	154	complex_of_real (LINT x \| M. (2 * (sgn (x - a) *
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	155	Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))" .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	156	} note main_eq2 = this
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: 62397 diff changeset	158	have "(\<lambda>T :: nat. LINT x \| M. (2 * (sgn (x - a) *
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	159	Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	160	(LINT x \| M. 2 * pi * indicator {a<..b} x)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	161	proof (rule integral_dominated_convergence [where w="\<lambda>x. 4 * B"])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	162	show "integrable M (\<lambda>x. 4 * B)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	163	by (rule integrable_const_bound [of _ "4 * B"]) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	164	next
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	165	let ?S = "\<lambda>n::nat. \<lambda>x. sgn (x - a) * Si (n * \<bar>x - a\<bar>) - sgn (x - b) * Si (n * \<bar>x - b\<bar>)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	166	{ fix n x
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	167	have "norm (?S n x) \<le> norm (sgn (x - a) * Si (n * \<bar>x - a\<bar>)) + norm (sgn (x - b) * Si (n * \<bar>x - b\<bar>))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	168	by (rule norm_triangle_ineq4)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	169	also have "\<dots> \<le> B + B"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	170	using Bprop by (intro add_mono) (auto simp: abs_mult abs_sgn_eq)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	171	finally have "norm (2 * ?S n x) \<le> 4 * B"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	172	by simp }
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	173	then show "\<And>n. AE x in M. norm (2 * ?S n x) \<le> 4 * B"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	174	by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	175	have "AE x in M. x \<noteq> a" "AE x in M. x \<noteq> b"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	176	using prob_eq_0[of "{a}"] prob_eq_0[of "{b}"] \<open>\<mu> {a} = 0\<close> \<open>\<mu> {b} = 0\<close> by (auto simp: \<mu>_def)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	177	then show "AE x in M. (\<lambda>n. 2 * ?S n x) \<longlonglongrightarrow> 2 * pi * indicator {a<..b} x"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	178	proof eventually_elim
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	179	fix x assume x: "x \<noteq> a" "x \<noteq> b"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	180	then have "(\<lambda>n. 2 * (sgn (x - a) * Si (\<bar>x - a\<bar> * n) - sgn (x - b) * Si (\<bar>x - b\<bar> * n)))
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	181	\<longlonglongrightarrow> 2 * (sgn (x - a) * (pi / 2) - sgn (x - b) * (pi / 2))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	182	by (intro tendsto_intros filterlim_compose[OF Si_at_top]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	183	filterlim_tendsto_pos_mult_at_top[OF tendsto_const] filterlim_real_sequentially)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	184	auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	185	also have "(\<lambda>n. 2 * (sgn (x - a) * Si (\<bar>x - a\<bar> * n) - sgn (x - b) * Si (\<bar>x - b\<bar> * n))) = (\<lambda>n. 2 * ?S n x)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	186	by (auto simp: ac_simps)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	187	also have "2 * (sgn (x - a) * (pi / 2) - sgn (x - b) * (pi / 2)) = 2 * pi * indicator {a<..b} x"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	188	using x \<open>a \<le> b\<close> by (auto split: split_indicator)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	189	finally show "(\<lambda>n. 2 * ?S n x) \<longlonglongrightarrow> 2 * pi * indicator {a<..b} x" .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	190	qed
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	191	qed simp_all
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	192	also have "(LINT x \| M. 2 * pi * indicator {a<..b} x) = 2 * pi * \<mu> {a<..b}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	193	by (simp add: \<mu>_def)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	194	finally have "(\<lambda>T. LINT x \| M. (2 * (sgn (x - a) *
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	195	Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	196	2 * pi * \<mu> {a<..b}" .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	197	with main_eq2 show ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	198	by (auto intro!: tendsto_eq_intros)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	199	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	200
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	201	theorem Levy_uniqueness:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	202	fixes M1 M2 :: "real measure"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	203	assumes "real_distribution M1" "real_distribution M2" and
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	204	"char M1 = char M2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	205	shows "M1 = M2"
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	interpret M1: real_distribution M1 by (rule assms)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	208	interpret M2: real_distribution M2 by (rule assms)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	209	have "countable ({x. measure M1 {x} \<noteq> 0} \<union> {x. measure M2 {x} \<noteq> 0})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	210	by (intro countable_Un M2.countable_support M1.countable_support)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	211	then have count: "countable {x. measure M1 {x} \<noteq> 0 \<or> measure M2 {x} \<noteq> 0}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	212	by (simp add: Un_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	213
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	214	have "cdf M1 = cdf M2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	215	proof (rule ext)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	216	fix x
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	217	let ?D = "\<lambda>x. \<bar>cdf M1 x - cdf M2 x\<bar>"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	218
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	219	{ fix \<epsilon> :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	220	assume "\<epsilon> > 0"
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	221	have "(?D \<longlongrightarrow> 0) at_bot"
67682 00c436488398 tuned proofs -- prefer explicit names for facts from 'interpret'; wenzelm parents: 66447 diff changeset	222	using M1.cdf_lim_at_bot M2.cdf_lim_at_bot by (intro tendsto_eq_intros) auto
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	223	then have "eventually (\<lambda>y. ?D y < \<epsilon> / 2 \<and> y \<le> x) at_bot"
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	224	using \<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot abs_idempotent)
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	225	then obtain M where "\<And>y. y \<le> M \<Longrightarrow> ?D y < \<epsilon> / 2" "M \<le> x"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	226	unfolding eventually_at_bot_linorder by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	227	with open_minus_countable[OF count, of "{..< M}"] obtain a where
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	228	"measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \<le> x" and 1: "?D a < \<epsilon> / 2"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	229	by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	230
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	231	have "(?D \<longlongrightarrow> ?D x) (at_right x)"
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	232	using M1.cdf_is_right_cont [of x] M2.cdf_is_right_cont [of x]
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	233	by (intro tendsto_intros) (auto simp add: continuous_within)
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	234	then have "eventually (\<lambda>y. \<bar>?D y - ?D x\<bar> < \<epsilon> / 2) (at_right x)"
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	235	using \<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less)
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	236	then obtain N where "N > x" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>?D y - ?D x\<bar> < \<epsilon> / 2"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	237	by (auto simp add: eventually_at_right[OF less_add_one])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	238	with open_minus_countable[OF count, of "{x <..< N}"] obtain b where "x < b" "b < N"
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	239	"measure M1 {b} = 0" "measure M2 {b} = 0" and 2: "\<bar>?D b - ?D x\<bar> < \<epsilon> / 2"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	240	by (auto simp: abs_minus_commute)
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	241	from \<open>a \<le> x\<close> \<open>x < b\<close> have "a < b" "a \<le> b" by auto
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	242
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	243	from \<open>char M1 = char M2\<close>
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	244	M1.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M1 {a} = 0\<close> \<open>measure M1 {b} = 0\<close>]
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	245	M2.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M2 {a} = 0\<close> \<open>measure M2 {b} = 0\<close>]
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	246	have "complex_of_real (measure M1 {a<..b}) = complex_of_real (measure M2 {a<..b})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	247	by (intro LIMSEQ_unique) auto
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	248	then have "?D a = ?D b"
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	249	unfolding of_real_eq_iff M1.cdf_diff_eq [OF \<open>a < b\<close>, symmetric] M2.cdf_diff_eq [OF \<open>a < b\<close>, symmetric] by simp
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	250	then have "?D x = \<bar>(?D b - ?D x) - ?D a\<bar>"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	251	by simp
63393 c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	252	also have "\<dots> \<le> \<bar>?D b - ?D x\<bar> + \<bar>?D a\<bar>"
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	253	by (rule abs_triangle_ineq4)
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	254	also have "\<dots> \<le> \<epsilon> / 2 + \<epsilon> / 2"
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	255	using 1 2 by (intro add_mono) auto
c22928719e19 Probability: simplified Levy's uniqueness theorem hoelzl parents: 63329 diff changeset	256	finally have "?D x \<le> \<epsilon>" by simp }
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	257	then show "cdf M1 x = cdf M2 x"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	258	by (metis abs_le_zero_iff dense_ge eq_iff_diff_eq_0)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	259	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	260	thus ?thesis
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	261	by (rule cdf_unique [OF \<open>real_distribution M1\<close> \<open>real_distribution M2\<close>])
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	262	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	263
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	264
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	265	subsection \<open>The Levy continuity theorem\<close>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	266
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	267	theorem levy_continuity1:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	268	fixes M :: "nat \<Rightarrow> real measure" and M' :: "real measure"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	269	assumes "\<And>n. real_distribution (M n)" "real_distribution M'" "weak_conv_m M M'"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	270	shows "(\<lambda>n. char (M n) t) \<longlonglongrightarrow> char M' t"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	271	unfolding char_def using assms by (rule weak_conv_imp_integral_bdd_continuous_conv) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	272
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	273	theorem levy_continuity:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	274	fixes M :: "nat \<Rightarrow> real measure" and M' :: "real measure"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	275	assumes real_distr_M : "\<And>n. real_distribution (M n)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	276	and real_distr_M': "real_distribution M'"
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	277	and char_conv: "\<And>t. (\<lambda>n. char (M n) t) \<longlonglongrightarrow> char M' t"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	278	shows "weak_conv_m M M'"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	279	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	280	interpret Mn: real_distribution "M n" for n by fact
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	281	interpret M': real_distribution M' by fact
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	282
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	283	have : "\<And>u x. u > 0 \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (CLBINT t:{-u..u}. 1 - iexp (t x)) =
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	284	2 * (u - sin (u * x) / x)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	285	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	286	fix u :: real and x :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	287	assume "u > 0" and "x \<noteq> 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	288	hence "(CLBINT t:{-u..u}. 1 - iexp (t * x)) = (CLBINT t=-u..u. 1 - iexp (t * x))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	289	by (subst interval_integral_Icc, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	290	also have "\<dots> = (CLBINT t=-u..0. 1 - iexp (t * x)) + (CLBINT t=0..u. 1 - iexp (t * x))"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	291	using \<open>u > 0\<close>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	292	apply (subst interval_integral_sum)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	293	apply (simp add: min_absorb1 min_absorb2 max_absorb1 max_absorb2)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	294	apply (rule interval_integrable_isCont)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	295	apply auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	296	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	297	also have "\<dots> = (CLBINT t=ereal 0..u. 1 - iexp (t * -x)) + (CLBINT t=ereal 0..u. 1 - iexp (t * x))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	298	apply (subgoal_tac "0 = ereal 0", erule ssubst)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	299	by (subst interval_integral_reflect, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	300	also have "\<dots> = (LBINT t=ereal 0..u. 2 - 2 * cos (t * x))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	301	apply (subst interval_lebesgue_integral_add (2) [symmetric])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	302	apply ((rule interval_integrable_isCont, auto)+) [2]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	303	unfolding exp_Euler cos_of_real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	304	apply (simp add: of_real_mult interval_lebesgue_integral_of_real[symmetric])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	305	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	306	also have "\<dots> = 2 * u - 2 * sin (u * x) / x"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	307	by (subst interval_lebesgue_integral_diff)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	308	(auto intro!: interval_integrable_isCont
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	309	simp: interval_lebesgue_integral_of_real integral_cos [OF \<open>x \<noteq> 0\<close>] mult.commute[of _ x])
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	310	finally show "(CLBINT t:{-u..u}. 1 - iexp (t * x)) = 2 * (u - sin (u * x) / x)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	311	by (simp add: field_simps)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	312	qed
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	313	have main_bound: "\<And>u n. u > 0 \<Longrightarrow> Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	314	u * measure (M n) {x. abs x \<ge> 2 / u}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	315	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	316	fix u :: real and n
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	317	assume "u > 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	318	interpret P: pair_sigma_finite "M n" lborel ..
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	319	(* TODO: put this in the real_distribution locale as a simp rule? *)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	320	have Mn1 [simp]: "measure (M n) UNIV = 1" by (metis Mn.prob_space Mn.space_eq_univ)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	321	(* TODO: make this automatic somehow? *)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	322	have Mn2 [simp]: "\<And>x. complex_integrable (M n) (\<lambda>t. exp (\<i> * complex_of_real (x * t)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	323	by (rule Mn.integrable_const_bound [where B = 1], auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	324	have Mn3: "set_integrable (M n \<Otimes>\<^sub>M lborel) (UNIV \<times> {- u..u}) (\<lambda>a. 1 - exp (\<i> * complex_of_real (snd a * fst a)))"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	325	using \<open>0 < u\<close>
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	326	unfolding set_integrable_def
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	327	by (intro integrableI_bounded_set_indicator [where B="2"])
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	328	(auto simp: lborel.emeasure_pair_measure_Times ennreal_mult_less_top not_less top_unique
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	329	split: split_indicator
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	330	intro!: order_trans [OF norm_triangle_ineq4])
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	331	have "(CLBINT t:{-u..u}. 1 - char (M n) t) =
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	332	(CLBINT t:{-u..u}. (CLINT x \| M n. 1 - iexp (t * x)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	333	unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	334	also have "\<dots> = (CLBINT t. (CLINT x \| M n. indicator {-u..u} t \<^sub>R (1 - iexp (t x))))"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	335	unfolding set_lebesgue_integral_def
63886 685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel hoelzl parents: 63589 diff changeset	336	by (rule Bochner_Integration.integral_cong) (auto split: split_indicator)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	337	also have "\<dots> = (CLINT x \| M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	338	using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta' set_integrable_def set_lebesgue_integral_def)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	339	also have "\<dots> = (CLINT x \| M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))"
63886 685fb01256af move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel hoelzl parents: 63589 diff changeset	340	using \<open>u > 0\<close> by (intro Bochner_Integration.integral_cong, auto simp add: * simp del: of_real_mult)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	341	also have "\<dots> = (LINT x \| M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	342	by (rule integral_complex_of_real)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	343	finally have "Re (CLBINT t:{-u..u}. 1 - char (M n) t) =
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	344	(LINT x \| M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))" by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	345	also have "\<dots> \<ge> (LINT x : {x. abs x \<ge> 2 / u} \| M n. u)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	346	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	347	have "complex_integrable (M n) (\<lambda>x. CLBINT t:{-u..u}. 1 - iexp (snd (x, t) * fst (x, t)))"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	348	using Mn3 unfolding set_integrable_def set_lebesgue_integral_def
557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	349	by (intro P.integrable_fst) (simp add: indicator_times split_beta')
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	350	hence "complex_integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u - sin (u * x) / x))"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	351	using \<open>u > 0\<close>
557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	352	unfolding set_integrable_def
557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	353	by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	354	hence *: "integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 (u - sin (u * x) / x))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	355	unfolding complex_of_real_integrable_eq .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	356	have "2 * sin x \<le> x" if "2 \<le> x" for x :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	357	by (rule order_trans[OF _ \<open>2 \<le> x\<close>]) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	358	moreover have "x \<le> 2 * sin x" if "x \<le> - 2" for x :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	359	by (rule order_trans[OF \<open>x \<le> - 2\<close>]) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	360	moreover have "x < 0 \<Longrightarrow> x \<le> sin x" for x :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	361	using sin_x_le_x[of "-x"] by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	362	ultimately show ?thesis
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	363	using \<open>u > 0\<close> unfolding set_lebesgue_integral_def
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	364	by (intro integral_mono [OF _ **])
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	365	(auto simp: divide_simps sin_x_le_x mult.commute[of u] mult_neg_pos top_unique less_top[symmetric]
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	366	split: split_indicator)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	367	qed
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	368	also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} \| M n. u) = u * measure (M n) {x. abs x \<ge> 2 / u}"
557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	369	unfolding set_lebesgue_integral_def
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	370	by (simp add: Mn.emeasure_eq_measure)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	371	finally show "Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge> u * measure (M n) {x. abs x \<ge> 2 / u}" .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	372	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	373
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	374	have tight_aux: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> \<exists>a b. a < b \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {a<..b})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	375	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	376	fix \<epsilon> :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	377	assume "\<epsilon> > 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	378	note M'.isCont_char [of 0]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	379	hence "\<exists>d>0. \<forall>t. abs t < d \<longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	380	apply (subst (asm) continuous_at_eps_delta)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	381	apply (drule_tac x = "\<epsilon> / 4" in spec)
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	382	using \<open>\<epsilon> > 0\<close> by (auto simp add: dist_real_def dist_complex_def M'.char_zero)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	383	then obtain d where "d > 0 \<and> (\<forall>t. (abs t < d \<longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4))" ..
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	384	hence d0: "d > 0" and d1: "\<And>t. abs t < d \<Longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4" by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	385	have 1: "\<And>x. cmod (1 - char M' x) \<le> 2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	386	by (rule order_trans [OF norm_triangle_ineq4], auto simp add: M'.cmod_char_le_1)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	387	then have 2: "\<And>u v. complex_set_integrable lborel {u..v} (\<lambda>x. 1 - char M' x)"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	388	unfolding set_integrable_def
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	389	by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq)
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	390	have 3: "\<And>u v. integrable lborel (\<lambda>x. indicat_real {u..v} x *\<^sub>R cmod (1 - char M' x))"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	391	by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	392	continuous_intros ballI M'.isCont_char continuous_intros)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	393	have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	394	unfolding set_lebesgue_integral_def
64283 979cdfdf7a79 HOL-Probability: move conditional expectation from AFP/Ergodic_Theory hoelzl parents: 63886 diff changeset	395	using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp
63540 f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	396	also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	397	unfolding set_lebesgue_integral_def
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	398	apply (rule integral_mono [OF 3])
63540 f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	399	apply (simp add: emeasure_lborel_Icc_eq)
f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	400	apply (case_tac "x \<in> {-d/2..d/2}")
f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	401	apply auto
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	402	apply (subst norm_minus_commute)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	403	apply (rule less_imp_le)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	404	apply (rule d1 [simplified])
63540 f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	405	using d0 apply auto
f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	406	done
f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	407	also from d0 4 have "\<dots> = d * \<epsilon> / 4"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	408	unfolding set_lebesgue_integral_def by simp
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	409	finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" .
63540 f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	410	have "cmod (1 - char (M n) x) \<le> 2" for n x
f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	411	by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
f8652d0534fa tuned proofs -- avoid unstructured calculation; wenzelm parents: 63393 diff changeset	412	then have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
67977 557ea2740125 Probability builds with new definitions paulson <lp15@cam.ac.uk> parents: 67682 diff changeset	413	unfolding set_lebesgue_integral_def
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	414	apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"])
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	415	apply (auto intro!: char_conv tendsto_intros
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	416	simp: emeasure_lborel_Icc_eq
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	417	split: split_indicator)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	418	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	419	hence "eventually (\<lambda>n. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	420	(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4) sequentially"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	421	using d0 \<open>\<epsilon> > 0\<close> apply (subst (asm) tendsto_iff)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	422	by (subst (asm) dist_complex_def, drule spec, erule mp, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	423	hence "\<exists>N. \<forall>n \<ge> N. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	424	(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by (simp add: eventually_sequentially)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	425	then guess N ..
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	426	hence N: "\<And>n. n \<ge> N \<Longrightarrow> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	427	(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	428	{ fix n
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	429	assume "n \<ge> N"
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	430	have "cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) =
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	431	cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - (CLBINT t:{-d/2..d/2}. 1 - char M' t)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	432	+ (CLBINT t:{-d/2..d/2}. 1 - char M' t))" by simp
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	433	also have "\<dots> \<le> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	434	(CLBINT t:{-d/2..d/2}. 1 - char M' t)) + cmod(CLBINT t:{-d/2..d/2}. 1 - char M' t)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	435	by (rule norm_triangle_ineq)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	436	also have "\<dots> < d * \<epsilon> / 4 + d * \<epsilon> / 4"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	437	by (rule add_less_le_mono [OF N [OF \<open>n \<ge> N\<close>] bound])
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	438	also have "\<dots> = d * \<epsilon> / 2" by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	439	finally have "cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) < d * \<epsilon> / 2" .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	440	hence "d * \<epsilon> / 2 > Re (CLBINT t:{-d/2..d/2}. 1 - char (M n) t)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	441	by (rule order_le_less_trans [OF complex_Re_le_cmod])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	442	hence "d * \<epsilon> / 2 > Re (CLBINT t:{-(d/2)..d/2}. 1 - char (M n) t)" (is "_ > ?lhs") by simp
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	443	also have "?lhs \<ge> (d / 2) * measure (M n) {x. abs x \<ge> 2 / (d / 2)}"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	444	using d0 by (intro main_bound, simp)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	445	finally (xtrans) have "d * \<epsilon> / 2 > (d / 2) * measure (M n) {x. abs x \<ge> 2 / (d / 2)}" .
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	446	with d0 \<open>\<epsilon> > 0\<close> have "\<epsilon> > measure (M n) {x. abs x \<ge> 2 / (d / 2)}" by (simp add: field_simps)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	447	hence "\<epsilon> > 1 - measure (M n) (UNIV - {x. abs x \<ge> 2 / (d / 2)})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	448	apply (subst Mn.borel_UNIV [symmetric])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	449	by (subst Mn.prob_compl, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	450	also have "UNIV - {x. abs x \<ge> 2 / (d / 2)} = {x. -(4 / d) < x \<and> x < (4 / d)}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	451	using d0 apply (auto simp add: field_simps)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	452	(* very annoying -- this should be automatic *)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	453	apply (case_tac "x \<ge> 0", auto simp add: field_simps)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	454	apply (subgoal_tac "0 \<le> x * d", arith, rule mult_nonneg_nonneg, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	455	apply (case_tac "x \<ge> 0", auto simp add: field_simps)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	456	apply (subgoal_tac "x * d \<le> 0", arith)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	457	apply (rule mult_nonpos_nonneg, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	458	by (case_tac "x \<ge> 0", auto simp add: field_simps)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	459	finally have "measure (M n) {x. -(4 / d) < x \<and> x < (4 / d)} > 1 - \<epsilon>"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	460	by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	461	} note 6 = this
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	462	{ fix n :: nat
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	463	have *: "(UN (k :: nat). {- real k<..real k}) = UNIV"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	464	by (auto, metis leI le_less_trans less_imp_le minus_less_iff reals_Archimedean2)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	465	have "(\<lambda>k. measure (M n) {- real k<..real k}) \<longlonglongrightarrow>
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	466	measure (M n) (UN (k :: nat). {- real k<..real k})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	467	by (rule Mn.finite_Lim_measure_incseq, auto simp add: incseq_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	468	hence "(\<lambda>k. measure (M n) {- real k<..real k}) \<longlonglongrightarrow> 1"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	469	using Mn.prob_space unfolding * Mn.borel_UNIV by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	470	hence "eventually (\<lambda>k. measure (M n) {- real k<..real k} > 1 - \<epsilon>) sequentially"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	471	apply (elim order_tendstoD (1))
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	472	using \<open>\<epsilon> > 0\<close> by auto
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	473	} note 7 = this
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	474	{ fix n :: nat
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	475	have "eventually (\<lambda>k. \<forall>m < n. measure (M m) {- real k<..real k} > 1 - \<epsilon>) sequentially"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	476	(is "?P n")
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	477	proof (induct n)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	478	case (Suc n) with 7[of n] show ?case
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	479	by eventually_elim (auto simp add: less_Suc_eq)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	480	qed simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	481	} note 8 = this
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	482	from 8 [of N] have "\<exists>K :: nat. \<forall>k \<ge> K. \<forall>m<N. 1 - \<epsilon> <
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	483	Sigma_Algebra.measure (M m) {- real k<..real k}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	484	by (auto simp add: eventually_sequentially)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	485	hence "\<exists>K :: nat. \<forall>m<N. 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}" by auto
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	486	then obtain K :: nat where
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	487	"\<forall>m<N. 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}" ..
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	488	hence K: "\<And>m. m < N \<Longrightarrow> 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	489	by auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	490	let ?K' = "max K (4 / d)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	491	have "-?K' < ?K' \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {-?K'<..?K'})"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	492	using d0 apply auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	493	apply (rule max.strict_coboundedI2, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	494	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	495	fix n
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	496	show " 1 - \<epsilon> < measure (M n) {- max (real K) (4 / d)<..max (real K) (4 / d)}"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	497	apply (case_tac "n < N")
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	498	apply (rule order_less_le_trans)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	499	apply (erule K)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	500	apply (rule Mn.finite_measure_mono, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	501	apply (rule order_less_le_trans)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	502	apply (rule 6, erule leI)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	503	by (rule Mn.finite_measure_mono, auto)
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	504	qed
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	505	thus "\<exists>a b. a < b \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {a<..b})" by (intro exI)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	506	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	507	have tight: "tight M"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	508	by (auto simp: tight_def intro: assms tight_aux)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	509	show ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	510	proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	511	fix s \<nu>
66447 a1f5c5c26fa6 Replaced subseq with strict_mono eberlm <eberlm@in.tum.de> parents: 65064 diff changeset	512	assume s: "strict_mono (s :: nat \<Rightarrow> nat)"
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	513	assume nu: "weak_conv_m (M \<circ> s) \<nu>"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	514	assume *: "real_distribution \<nu>"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	515	have 2: "\<And>n. real_distribution ((M \<circ> s) n)" unfolding comp_def by (rule assms)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	516	have 3: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char \<nu> t" by (intro levy_continuity1 [OF 2 * nu])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	517	have 4: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) = ((\<lambda>n. char (M n) t) \<circ> s)" by (rule ext, simp)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	518	have 5: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char M' t"
62397 5ae24f33d343 Substantial new material for multivariate analysis. Also removal of some duplicates. paulson <lp15@cam.ac.uk> parents: 62083 diff changeset	519	by (subst 4, rule LIMSEQ_subseq_LIMSEQ [OF _ s], rule assms)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	520	hence "char \<nu> = char M'" by (intro ext, intro LIMSEQ_unique [OF 3 5])
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62975 diff changeset	521	hence "\<nu> = M'" by (rule Levy_uniqueness [OF * \<open>real_distribution M'\<close>])
62975 1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	522	thus "weak_conv_m (M \<circ> s) M'"
1d066f6ab25d Probability: move emeasure and nn_integral from ereal to ennreal hoelzl parents: 62397 diff changeset	523	by (elim subst) (rule nu)
62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	524	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	525	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	526
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	527	end

author	nipkow
	Thu, 01 Apr 2021 07:35:03 +0200
changeset 73527	c72fd8f1fceb
parent 70817	dd675800469d
child 74362	0135a0c77b64
permissions	-rw-r--r--