(* Title: HOL/Probability/Levy.thy Authors: Jeremy Avigad (CMU)
*)
section \<open>The Levy inversion theorem, and the Levy continuity theorem.\<close>
theory Levy imports Characteristic_Functions Helly_Selection Sinc_Integral begin
subsection \<open>The Levy inversion theorem\<close>
(* Actually, this is not needed for us -- but it is useful for other purposes. (See Billingsley.) *) lemma Levy_Inversion_aux1: fixes a b :: real assumes"a \ b" shows"((\t. (iexp (-(t * a)) - iexp (-(t * b))) / (\ * t)) \ b - a) (at 0)"
(is"(?F \ _) (at _)") proof - have 1: "cmod (?F t - (b - a)) \ a^2 / 2 * abs t + b^2 / 2 * abs t" if "t \ 0" for t proof - have"cmod (?F t - (b - a)) = cmod (
(iexp (-(t * a)) - (1 + \<i> * -(t * a))) / (\<i> * t) -
(iexp (-(t * b)) - (1 + \<i> * -(t * b))) / (\<i> * t))"
(is"_ = cmod (?one / (\ * t) - ?two / (\ * t))") using\<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps) alsohave"\ \ cmod (?one / (\ * t)) + cmod (?two / (\ * t))" by (rule norm_triangle_ineq4) alsohave"cmod (?one / (\ * t)) = cmod ?one / abs t" by (simp add: norm_divide norm_mult) alsohave"cmod (?two / (\ * t)) = cmod ?two / abs t" by (simp add: norm_divide norm_mult) alsohave"cmod ?one / abs t + cmod ?two / abs t \
((- (a * t))^2 / 2) / abs t + ((- (b * t))^2 / 2) / abs t" using iexp_approx1 [of "-(t * _)" 1] by (intro add_mono divide_right_mono abs_ge_zero) (auto simp: field_simps eval_nat_numeral) alsohave"\ = a^2 / 2 * abs t + b^2 / 2 * abs t" using\<open>t \<noteq> 0\<close> apply (case_tac "t \<ge> 0", simp add: field_simps power2_eq_square) using\<open>t \<noteq> 0\<close> by (subst (1 2) abs_of_neg, auto simp add: field_simps power2_eq_square) finallyshow"cmod (?F t - (b - a)) \ a^2 / 2 * abs t + b^2 / 2 * abs t" . qed show ?thesis apply (rule LIM_zero_cancel) apply (rule tendsto_norm_zero_cancel) apply (rule real_LIM_sandwich_zero [OF _ _ 1]) apply (auto intro!: tendsto_eq_intros) done qed
lemma Levy_Inversion_aux2: fixes a b t :: real assumes"a \ b" and "t \ 0" shows"cmod ((iexp (t * b) - iexp (t * a)) / (\ * t)) \ b - a" (is "?F \ _") proof - have"?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (\ * t))" using\<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps exp_diff exp_minus) alsohave"\ = cmod (iexp (t * (b - a)) - 1) / abs t" unfolding norm_divide norm_mult norm_exp_i_times using\<open>t \<noteq> 0\<close> by (simp add: complex_eq_iff norm_mult) alsohave"\ \ abs (t * (b - a)) / abs t" using iexp_approx1 [of "t * (b - a)" 0] by (intro divide_right_mono) (auto simp add: field_simps eval_nat_numeral) alsohave"\ = b - a" using assms by (auto simp add: abs_mult) finallyshow ?thesis . qed
(* TODO: refactor! *) theorem (in real_distribution) Levy_Inversion: fixes a b :: real assumes"a \ b" defines"\ \ measure M" and "\ \ char M" assumes"\ {a} = 0" and "\ {b} = 0" shows"(\T. 1 / (2 * pi) * (CLBINT t=-T..T. (iexp (-(t * a)) - iexp (-(t * b))) / (\ * t) * \ t)) \<longlonglongrightarrow> \<mu> {a<..b}"
(is"(\T. 1 / (2 * pi) * (CLBINT t=-T..T. ?F t * \ t)) \ of_real (\ {a<..b})") proof - interpret P: pair_sigma_finite lborel M .. from bounded_Si obtain B where Bprop: "\T. abs (Si T) \ B" by auto from Bprop [of 0] have [simp]: "B \ 0" by auto let ?f = "\t x :: real. (iexp (t * (x - a)) - iexp(t * (x - b))) / (\ * t)"
{ fix T :: real assume"T \ 0" let ?f' = "\(t, x). indicator {-T<..R ?f t x"
{ fix x have int: "interval_lebesgue_integrable lborel (ereal 0) (ereal T) (\t. 2 * (sin (t * (x-w)) / t))" for w using integrable_sinc' interval_lebesgue_integrable_mult_right by blast have 1: "complex_interval_lebesgue_integrable lborel u v (\t. ?f t x)" for u v :: real using Levy_Inversion_aux2[of "x - b""x - a"] apply (simp add: interval_lebesgue_integrable_def set_integrable_def del: times_divide_eq_left) apply (intro integrableI_bounded_set_indicator[where B="b - a"] conjI impI) apply (auto intro!: AE_I [of _ _ "{0}"] simp: assms) done have"(CLBINT t. ?f' (t, x)) = (CLBINT t=-T..T. ?f t x)" using\<open>T \<ge> 0\<close> by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def) alsohave"\ = (CLBINT t=-T..(0 :: real). ?f t x) + (CLBINT t=(0 :: real)..T. ?f t x)"
(is"_ = _ + ?t") using 1 by (intro interval_integral_sum[symmetric]) (simp add: min_absorb1 max_absorb2 \<open>T \<ge> 0\<close>) alsohave"(CLBINT t=-T..(0 :: real). ?f t x) = (CLBINT t=(0::real)..T. ?f (-t) x)" by (subst interval_integral_reflect) auto alsohave"\ + ?t = (CLBINT t=(0::real)..T. ?f (-t) x + ?f t x)" using 1 by (intro interval_lebesgue_integral_add(2) [symmetric] interval_integrable_mirror[THEN iffD2]) simp_all alsohave"\ = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) -
(iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (\<i> * t))" using\<open>T \<ge> 0\<close> by (intro interval_integral_cong) (auto simp add: field_split_simps) alsohave"\ = (CLBINT t=(0::real)..T. complex_of_real(
2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t)))" using\<open>T \<ge> 0\<close> by (intro interval_integral_cong) (simp add: divide_simps Im_divide Re_divide Im_exp Re_exp complex_eq_iff) alsohave"\ = complex_of_real (LBINT t=(0::real)..T.
2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t))" by (rule interval_lebesgue_integral_of_real) alsohave"\ = complex_of_real ((LBINT t=ereal 0..ereal T. 2 * (sin (t * (x - a)) / t)) -
(LBINT t=ereal 0..ereal T. 2 * (sin (t * (x - b)) / t)))" unfolding interval_lebesgue_integral_diff using int by auto alsohave"\ = complex_of_real (2 * (sgn (x - a) * Si (T * abs (x - a)) -
sgn (x - b) * Si (T * abs (x - b))))" unfolding interval_lebesgue_integral_mult_right by (simp add: zero_ereal_def[symmetric] LBINT_I0c_sin_scale_divide[OF \<open>T \<ge> 0\<close>]) finallyhave"(CLBINT t. ?f' (t, x)) =
2 * (sgn (x - a) * Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))" .
} note main_eq = this have"(CLBINT t=-T..T. ?F t * \ t) =
(CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))" using\<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def set_lebesgue_integral_def by (auto split: split_indicator intro!: Bochner_Integration.integral_cong) alsohave"\ = (CLBINT t. (CLINT x | M. ?f' (t, x)))" by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator) alsohave"\ = (CLINT x | M. (CLBINT t. ?f' (t, x)))" proof (intro P.Fubini_integral [symmetric] integrableI_bounded_set [where B="b - a"]) show"emeasure (lborel \\<^sub>M M) ({- T<.. space M) < \" using\<open>T \<ge> 0\<close> by (subst emeasure_pair_measure_Times)
(auto simp: ennreal_mult_less_top not_less top_unique) show"AE x\{- T<.. space M in lborel \\<^sub>M M. cmod (case x of (t, x) \ ?f' (t, x)) \ b - a" using Levy_Inversion_aux2[of "x - b""x - a"for x] \<open>a \<le> b\<close> by (intro AE_I [of _ _ "{0} \ UNIV"]) (force simp: emeasure_pair_measure_Times)+ qed (auto split: split_indicator split_indicator_asm) alsohave"\ = (CLINT x | M. (complex_of_real (2 * (sgn (x - a) *
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))))" using main_eq by (intro Bochner_Integration.integral_cong, auto) alsohave"\ = complex_of_real (LINT x | M. (2 * (sgn (x - a) *
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))" by (rule integral_complex_of_real) finallyhave"(CLBINT t=-T..T. ?F t * \ t) =
complex_of_real (LINT x | M. (2 * (sgn (x - a) *
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))" .
} note main_eq2 = this
have"(\T :: nat. LINT x | M. (2 * (sgn (x - a) *
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow>
(LINT x | M. 2 * pi * indicator {a<..b} x)" proof (rule integral_dominated_convergence [where w="\x. 4 * B"]) show"integrable M (\x. 4 * B)" by (rule integrable_const_bound [of _ "4 * B"]) auto next let ?S = "\n::nat. \x. sgn (x - a) * Si (n * \x - a\) - sgn (x - b) * Si (n * \x - b\)"
{ fix n x have"norm (?S n x) \ norm (sgn (x - a) * Si (n * \x - a\)) + norm (sgn (x - b) * Si (n * \x - b\))" by (rule norm_triangle_ineq4) alsohave"\ \ B + B" using Bprop by (intro add_mono) (auto simp: abs_mult abs_sgn_eq) finallyhave"norm (2 * ?S n x) \ 4 * B" by simp } thenshow"\n. AE x in M. norm (2 * ?S n x) \ 4 * B" by auto have"AE x in M. x \ a" "AE x in M. x \ b" 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) thenshow"AE x in M. (\n. 2 * ?S n x) \ 2 * pi * indicator {a<..b} x" proof eventually_elim fix x assume x: "x \ a" "x \ b" thenhave"(\n. 2 * (sgn (x - a) * Si (\x - a\ * n) - sgn (x - b) * Si (\x - b\ * n))) \<longlonglongrightarrow> 2 * (sgn (x - a) * (pi / 2) - sgn (x - b) * (pi / 2))" by (intro tendsto_intros filterlim_compose[OF Si_at_top]
filterlim_tendsto_pos_mult_at_top[OF tendsto_const] filterlim_real_sequentially)
auto alsohave"(\n. 2 * (sgn (x - a) * Si (\x - a\ * n) - sgn (x - b) * Si (\x - b\ * n))) = (\n. 2 * ?S n x)" by (auto simp: ac_simps) alsohave"2 * (sgn (x - a) * (pi / 2) - sgn (x - b) * (pi / 2)) = 2 * pi * indicator {a<..b} x" using x \<open>a \<le> b\<close> by (auto split: split_indicator) finallyshow"(\n. 2 * ?S n x) \ 2 * pi * indicator {a<..b} x" . qed qed simp_all alsohave"(LINT x | M. 2 * pi * indicator {a<..b} x) = 2 * pi * \ {a<..b}" by (simp add: \<mu>_def) finallyhave"(\T. LINT x | M. (2 * (sgn (x - a) *
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow>
2 * pi * \<mu> {a<..b}" . with main_eq2 show ?thesis by (auto intro!: tendsto_eq_intros) qed
have"cdf M1 = cdf M2" proof (rule ext) fix x let ?D = "\x. \cdf M1 x - cdf M2 x\"
{ fix\<epsilon> :: real assume"\ > 0" have"(?D \ 0) at_bot" using M1.cdf_lim_at_bot M2.cdf_lim_at_bot by (intro tendsto_eq_intros) auto thenhave"eventually (\y. ?D y < \ / 2 \ y \ x) at_bot" using\<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot abs_idempotent) thenobtain M where"\y. y \ M \ ?D y < \ / 2" "M \ x" unfolding eventually_at_bot_linorder by auto with open_minus_countable[OF count, of "{..< M}"] obtain a where "measure M1 {a} = 0""measure M2 {a} = 0""a < M""a \ x" and 1: "?D a < \ / 2" by auto
have"(?D \ ?D x) (at_right x)" using M1.cdf_is_right_cont [of x] M2.cdf_is_right_cont [of x] by (intro tendsto_intros) (auto simp add: continuous_within) thenhave"eventually (\y. \?D y - ?D x\ < \ / 2) (at_right x)" using\<open>\<epsilon> > 0\<close> by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less) thenobtain N where"N > x""\y. x < y \ y < N \ \?D y - ?D x\ < \ / 2" by (auto simp add: eventually_at_right[OF less_add_one]) with open_minus_countable[OF count, of "{x <..< N}"] obtain b where"x < b""b < N" "measure M1 {b} = 0""measure M2 {b} = 0"and 2: "\?D b - ?D x\ < \ / 2" by (auto simp: abs_minus_commute) from\<open>a \<le> x\<close> \<open>x < b\<close> have "a < b" "a \<le> b" by auto
from\<open>char M1 = char M2\<close>
M1.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M1 {a} = 0\<close> \<open>measure M1 {b} = 0\<close>]
M2.Levy_Inversion [OF \<open>a \<le> b\<close> \<open>measure M2 {a} = 0\<close> \<open>measure M2 {b} = 0\<close>] have"complex_of_real (measure M1 {a<..b}) = complex_of_real (measure M2 {a<..b})" by (intro LIMSEQ_unique) auto thenhave"?D a = ?D b" 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 thenhave"?D x = \(?D b - ?D x) - ?D a\" by simp alsohave"\ \ \?D b - ?D x\ + \?D a\" by (rule abs_triangle_ineq4) alsohave"\ \ \ / 2 + \ / 2" using 1 2 by (intro add_mono) auto finallyhave"?D x \ \" by simp } thenshow"cdf M1 x = cdf M2 x" by (metis abs_le_zero_iff dense_ge eq_iff_diff_eq_0) qed thus ?thesis by (rule cdf_unique [OF \<open>real_distribution M1\<close> \<open>real_distribution M2\<close>]) qed
subsection \<open>The Levy continuity theorem\<close>
theorem levy_continuity1: fixes M :: "nat \ real measure" and M' :: "real measure" assumes"\n. real_distribution (M n)" "real_distribution M'" "weak_conv_m M M'" shows"(\n. char (M n) t) \ char M' t" unfolding char_def using assms by (rule weak_conv_imp_integral_bdd_continuous_conv) auto
theorem levy_continuity: fixes M :: "nat \ real measure" and M' :: "real measure" assumes real_distr_M : "\n. real_distribution (M n)" and real_distr_M': "real_distribution M'" and char_conv: "\t. (\n. char (M n) t) \ char M' t" shows"weak_conv_m M M'" proof - interpret Mn: real_distribution "M n"for n by fact interpret M': real_distribution M'by fact
have *: "\u x. u > 0 \ x \ 0 \ (CLBINT t:{-u..u}. 1 - iexp (t * x)) =
2 * (u - sin (u * x) / x)" proof - fix u :: real and x :: real assume"u > 0"and"x \ 0" hence"(CLBINT t:{-u..u}. 1 - iexp (t * x)) = (CLBINT t=-u..u. 1 - iexp (t * x))" by (subst interval_integral_Icc, auto) alsohave"\ = (CLBINT t=-u..ereal 0. 1 - iexp (t * x)) + (CLBINT t= ereal 0..u. 1 - iexp (t * x))" using\<open>u > 0\<close> by (subst interval_integral_sum; force simp add: interval_integrable_isCont) alsohave"\ = (CLBINT t=ereal 0..u. 1 - iexp (t * -x)) + (CLBINT t=ereal 0..u. 1 - iexp (t * x))" by (subst interval_integral_reflect, auto) alsohave"... = CLBINT xa=ereal 0..ereal u. 1 - iexp (xa * - x) + (1 - iexp (xa * x))" by (subst interval_lebesgue_integral_add (2) [symmetric]) (auto simp: interval_integrable_isCont) alsohave"\ = (LBINT t=ereal 0..u. 2 - 2 * cos (t * x))" unfolding exp_Euler cos_of_real by (simp flip: interval_lebesgue_integral_of_real) alsohave"\ = 2 * u - 2 * sin (u * x) / x" by (subst interval_lebesgue_integral_diff)
(auto intro!: interval_integrable_isCont
simp: interval_lebesgue_integral_of_real integral_cos [OF \<open>x \<noteq> 0\<close>] mult.commute[of _ x]) finallyshow"(CLBINT t:{-u..u}. 1 - iexp (t * x)) = 2 * (u - sin (u * x) / x)" by (simp add: field_simps) qed have main_bound: "\u n. u > 0 \ Re (CLBINT t:{-u..u}. 1 - char (M n) t) \
u * measure (M n) {x. abs x \<ge> 2 / u}" proof - fix u :: real and n assume"u > 0" interpret P: pair_sigma_finite "M n" lborel .. (* TODO: put this in the real_distribution locale as a simp rule? *) have Mn1 [simp]: "measure (M n) UNIV = 1"by (metis Mn.prob_space Mn.space_eq_univ) (* TODO: make this automatic somehow? *) have Mn2 [simp]: "\x. complex_integrable (M n) (\t. exp (\ * complex_of_real (x * t)))" by (rule Mn.integrable_const_bound [where B = 1], auto) have Mn3: "set_integrable (M n \\<^sub>M lborel) (UNIV \ {- u..u}) (\a. 1 - exp (\ * complex_of_real (snd a * fst a)))" using\<open>0 < u\<close> unfolding set_integrable_def by (intro integrableI_bounded_set_indicator [where B="2"])
(auto simp: lborel.emeasure_pair_measure_Times ennreal_mult_less_top not_less top_unique
split: split_indicator
intro!: order_trans [OF norm_triangle_ineq4]) have"(CLBINT t:{-u..u}. 1 - char (M n) t) =
(CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))" unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult) alsohave"\ = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))" unfolding set_lebesgue_integral_def by (rule Bochner_Integration.integral_cong) (auto split: split_indicator) alsohave"\ = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))" using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta' set_integrable_def set_lebesgue_integral_def) alsohave"\ = (CLINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))" using\<open>u > 0\<close> by (intro Bochner_Integration.integral_cong, auto simp add: * simp del: of_real_mult) alsohave"\ = (LINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))" by (rule integral_complex_of_real) finallyhave"Re (CLBINT t:{-u..u}. 1 - char (M n) t) =
(LINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))" by simp alsohave"\ \ (LINT x : {x. abs x \ 2 / u} | M n. u)" proof - have"complex_integrable (M n) (\x. CLBINT t:{-u..u}. 1 - iexp (snd (x, t) * fst (x, t)))" using Mn3 unfolding set_integrable_def set_lebesgue_integral_def by (intro P.integrable_fst) (simp add: indicator_times split_beta') hence"complex_integrable (M n) (\x. if x = 0 then 0 else 2 * (u - sin (u * x) / x))" using\<open>u > 0\<close> unfolding set_integrable_def by (subst Bochner_Integration.integrable_cong) (auto simp add: * simp del: of_real_mult) hence **: "integrable (M n) (\x. if x = 0 then 0 else 2 * (u - sin (u * x) / x))" unfolding complex_of_real_integrable_eq . have"2 * sin x \ x" if "2 \ x" for x :: real by (rule order_trans[OF _ \<open>2 \<le> x\<close>]) auto moreoverhave"x \ 2 * sin x" if "x \ - 2" for x :: real by (rule order_trans[OF \<open>x \<le> - 2\<close>]) auto moreoverhave"x < 0 \ x \ sin x" for x :: real using sin_x_le_x[of "-x"] by simp ultimatelyshow ?thesis using\<open>u > 0\<close> unfolding set_lebesgue_integral_def by (intro integral_mono [OF _ **])
(auto simp: divide_simps sin_x_le_x mult.commute[of u] mult_neg_pos top_unique less_top[symmetric]
split: split_indicator) qed also (xtrans) have"(LINT x : {x. abs x \ 2 / u} | M n. u) = u * measure (M n) {x. abs x \ 2 / u}" unfolding set_lebesgue_integral_def by (simp add: Mn.emeasure_eq_measure) finallyshow"Re (CLBINT t:{-u..u}. 1 - char (M n) t) \ u * measure (M n) {x. abs x \ 2 / u}" . qed
have tight_aux: "\\. \ > 0 \ \a b. a < b \ (\n. 1 - \ < measure (M n) {a<..b})" proof - fix\<epsilon> :: real assume"\ > 0" with M'.isCont_char [of 0] obtain d where d0: "d>0"and"\x'. dist x' 0 < d \ dist (char M' x') (char M' 0) < \/4" unfolding continuous_at_eps_delta by (metis \<open>0 < \<epsilon>\<close> divide_pos_pos zero_less_numeral) thenhave d1: "\t. abs t < d \ cmod (char M' t - 1) < \ / 4" by (simp add: M'.char_zero dist_norm) have 1: "\x. cmod (1 - char M' x) \ 2" by (rule order_trans [OF norm_triangle_ineq4], auto simp add: M'.cmod_char_le_1) thenhave 2: "\u v. complex_set_integrable lborel {u..v} (\x. 1 - char M' x)" unfolding set_integrable_def by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq) have 3: "\u v. integrable lborel (\x. indicat_real {u..v} x *\<^sub>R cmod (1 - char M' x))" by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
continuous_intros ballI M'.isCont_char continuous_intros) have"cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \ (LBINT t:{-d/2..d/2}. cmod (1 - char M' t))" unfolding set_lebesgue_integral_def using integral_norm_bound[of _ "\x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp alsohave 4: "\ \ (LBINT t:{-d/2..d/2}. \ / 4)" unfolding set_lebesgue_integral_def proof (rule integral_mono [OF 3])
show"indicat_real {- d / 2..d / 2} x *\<^sub>R cmod (1 - char M' x) \<le> indicat_real {- d / 2..d / 2} x *\<^sub>R (\<epsilon> / 4)" if"x \ space lborel" for x proof (cases "x \ {-d/2..d/2}") case True show ?thesis using d0 d1 that True [simplified] by (smt (verit, best) field_sum_of_halves minus_diff_eq norm_minus_cancel indicator_pos_le scaleR_left_mono) qed auto qed (simp add: emeasure_lborel_Icc_eq) alsofrom d0 4 have"\ = d * \ / 4" unfolding set_lebesgue_integral_def by simp finallyhave bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \ d * \ / 4" . have"cmod (1 - char (M n) x) \ 2" for n x by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1) thenhave"(\n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \ (CLBINT t:{-d/2..d/2}. 1 - char M' t)" unfolding set_lebesgue_integral_def apply (intro integral_dominated_convergence[where w="\x. indicator {-d/2..d/2} x *\<^sub>R 2"]) apply (auto intro!: char_conv tendsto_intros
simp: emeasure_lborel_Icc_eq
split: split_indicator) done hence"eventually (\n. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \ / 4) sequentially" using d0 \<open>\<epsilon> > 0\<close> apply (subst (asm) tendsto_iff) by (subst (asm) dist_complex_def, drule spec, erule mp, auto) hence"\N. \n \ N. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \ / 4" by (simp add: eventually_sequentially) thenobtain N where"\n\N. cmod ((CLBINT t:{- d / 2..d / 2}. 1 - char (M n) t) -
(CLBINT t:{- d / 2..d / 2}. 1 - char M' t)) < d * \ / 4" .. hence N: "\n. n \ N \ cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \ / 4" by auto
{ fix n assume"n \ N" have"cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) =
cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - (CLBINT t:{-d/2..d/2}. 1 - char M' t)
+ (CLBINT t:{-d/2..d/2}. 1 - char M' t))" by simp alsohave"\ \ cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) + cmod(CLBINT t:{-d/2..d/2}. 1 - char M' t)" by (rule norm_triangle_ineq) alsohave"\ < d * \ / 4 + d * \ / 4" by (rule add_less_le_mono [OF N [OF \<open>n \<ge> N\<close>] bound]) alsohave"\ = d * \ / 2" by auto finallyhave"cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) < d * \ / 2" . hence"d * \ / 2 > Re (CLBINT t:{-d/2..d/2}. 1 - char (M n) t)" by (rule order_le_less_trans [OF complex_Re_le_cmod]) hence"d * \ / 2 > Re (CLBINT t:{-(d/2)..d/2}. 1 - char (M n) t)" (is "_ > ?lhs") by simp alsohave"?lhs \ (d / 2) * measure (M n) {x. abs x \ 2 / (d / 2)}" using d0 by (intro main_bound, simp) finally (xtrans) have"d * \ / 2 > (d / 2) * measure (M n) {x. abs x \ 2 / (d / 2)}" . with d0 \<open>\<epsilon> > 0\<close> have "\<epsilon> > measure (M n) {x. abs x \<ge> 2 / (d / 2)}" by (simp add: field_simps) hence"\ > 1 - measure (M n) (UNIV - {x. abs x \ 2 / (d / 2)})" apply (subst Mn.borel_UNIV [symmetric]) by (subst Mn.prob_compl, auto) alsohave"UNIV - {x. abs x \ 2 / (d / 2)} = {x. -(4 / d) < x \ x < (4 / d)}" using d0 by (simp add: set_eq_iff divide_simps abs_if) (smt (verit, best) mult_less_0_iff) finallyhave"measure (M n) {x. -(4 / d) < x \ x < (4 / d)} > 1 - \" by auto
} note 6 = this
{ fix n :: nat have *: "(UN (k :: nat). {- real k<..real k}) = UNIV" by (auto, metis leI le_less_trans less_imp_le minus_less_iff reals_Archimedean2) have"(\k. measure (M n) {- real k<..real k}) \
measure (M n) (UN (k :: nat). {- real k<..real k})" by (rule Mn.finite_Lim_measure_incseq, auto simp add: incseq_def) hence"(\k. measure (M n) {- real k<..real k}) \ 1" using Mn.prob_space unfolding * Mn.borel_UNIV by simp hence"eventually (\k. measure (M n) {- real k<..real k} > 1 - \) sequentially" using\<open>\<epsilon> > 0\<close> order_tendstoD by fastforce
} note 7 = this
{ fix n :: nat have"eventually (\k. \m < n. measure (M m) {- real k<..real k} > 1 - \) sequentially"
(is"?P n") proof (induct n) case (Suc n) with 7[of n] show ?case by eventually_elim (auto simp add: less_Suc_eq) qed simp
} note 8 = this from 8 [of N] have"\K :: nat. \k \ K. \m <
Sigma_Algebra.measure (M m) {- real k<..real k}" by (auto simp add: eventually_sequentially) hence"\K :: nat. \m < Sigma_Algebra.measure (M m) {- real K<..real K}" by auto thenobtain K :: nat where "\m < Sigma_Algebra.measure (M m) {- real K<..real K}" .. hence K: "\m. m < N \ 1 - \ < Sigma_Algebra.measure (M m) {- real K<..real K}" by auto let ?K' = "max K (4 / d)" have"1 - \ < measure (M n) {- max (real K) (4 / d)<..max (real K) (4 / d)}" for n proof (cases "n < N") case True thenshow ?thesis by (force intro: order_less_le_trans [OF K Mn.finite_measure_mono]) next case False thenshow ?thesis by (force intro: order_less_le_trans [OF 6 Mn.finite_measure_mono]) qed thenhave"-?K' < ?K' \ (\n. 1 - \ < measure (M n) {-?K'<..?K'})" using d0 by (simp add: less_max_iff_disj minus_less_iff) thus"\a b. a < b \ (\n. 1 - \ < measure (M n) {a<..b})" by (intro exI) qed have tight: "tight M" by (auto simp: tight_def intro: assms tight_aux) show ?thesis proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight]) fix s \<nu> assume s: "strict_mono (s :: nat \ nat)" assume nu: "weak_conv_m (M \ s) \" assume *: "real_distribution \" have 2: "\n. real_distribution ((M \ s) n)" unfolding comp_def by (rule assms) have 3: "\t. (\n. char ((M \ s) n) t) \ char \ t" by (intro levy_continuity1 [OF 2 * nu]) have 4: "\t. (\n. char ((M \ s) n) t) = ((\n. char (M n) t) \ s)" by (rule ext, simp) have 5: "\t. (\n. char ((M \ s) n) t) \ char M' t" by (subst 4, rule LIMSEQ_subseq_LIMSEQ [OF _ s], rule assms) hence"char \ = char M'" by (intro ext, intro LIMSEQ_unique [OF 3 5]) hence"\ = M'" by (rule Levy_uniqueness [OF * \real_distribution M'\]) thus"weak_conv_m (M \ s) M'" by (elim subst) (rule nu) qed qed
end
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
