Quelle Levy.thy Sprache: Isabelle

(* 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 + \ * -(t * a))) / (\ * t) -
 (iexp (-(t * b)) - (1 + \ * -(t * b))) / (\ * t))"
 (is "_ = cmod (?one / (\ * t) - ?two / (\ * t))")
 using \<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps)
 also have "\ \ cmod (?one / (\ * t)) + cmod (?two / (\ * t))"
 by (rule norm_triangle_ineq4)
 also have "cmod (?one / (\ * t)) = cmod ?one / abs t"
 by (simp add: norm_divide norm_mult)
 also have "cmod (?two / (\ * t)) = cmod ?two / abs t"
 by (simp add: norm_divide norm_mult)
 also have "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)
 also have "\ = 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)
 finally show "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)
 also have "\ = 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)
 also have "\ \ 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)
 also have "\ = b - a"
 using assms by (auto simp add: abs_mult)
 finally show ?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)
 also have "\ = (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>)
 also have "(CLBINT t=-T..(0 :: real). ?f t x) = (CLBINT t=(0::real)..T. ?f (-t) x)"
 by (subst interval_integral_reflect) auto
 also have "\ + ?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
 also have "\ = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) -
 (iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (\ * t))"
 using \<open>T \<ge> 0\<close> by (intro interval_integral_cong) (auto simp add: field_split_simps)
 also have "\ = (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)
 also have "\ = 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)
 also have "\ = 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
 also have "\ = 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>])
 finally have "(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)
 also have "\ = (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)
 also have "\ = (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)
 also have "\ = (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)
 also have "\ = 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)
 finally have "(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)
 also have "\ \ B + B"
 using Bprop by (intro add_mono) (auto simp: abs_mult abs_sgn_eq)
 finally have "norm (2 * ?S n x) \ 4 * B"
 by simp }
 then show "\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)
 then show "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"
 then have "(\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
 also have "(\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)
 also have "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)
 finally show "(\n. 2 * ?S n x) \ 2 * pi * indicator {a<..b} x" .
 qed
 qed simp_all
 also have "(LINT x | M. 2 * pi * indicator {a<..b} x) = 2 * pi * \ {a<..b}"
 by (simp add: \<mu>_def)
 finally have "(\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

theorem Levy_uniqueness:
 fixes M1 M2 :: "real measure"
 assumes "real_distribution M1" "real_distribution M2" and
 "char M1 = char M2"
 shows "M1 = M2"
proof -
 interpret M1: real_distribution M1 by (rule assms)
 interpret M2: real_distribution M2 by (rule assms)
 have "countable ({x. measure M1 {x} \ 0} \ {x. measure M2 {x} \ 0})"
 by (intro countable_Un M2.countable_support M1.countable_support)
 then have count: "countable {x. measure M1 {x} \ 0 \ measure M2 {x} \ 0}"
 by (simp add: Un_def)

 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
 then have "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)
 then obtain 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)
 then have "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)
 then obtain 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
 then have "?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
 then have "?D x = \(?D b - ?D x) - ?D a\"
 by simp
 also have "\ \ \?D b - ?D x\ + \?D a\"
 by (rule abs_triangle_ineq4)
 also have "\ \ \ / 2 + \ / 2"
 using 1 2 by (intro add_mono) auto
 finally have "?D x \ \" by simp }
 then show "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)
 also have "\ = (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)
 also have "\ = (CLBINT t=ereal 0..u. 1 - iexp (t * -x)) + (CLBINT t=ereal 0..u. 1 - iexp (t * x))"
 by (subst interval_integral_reflect, auto)
 also have "... = 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)
 also have "\ = (LBINT t=ereal 0..u. 2 - 2 * cos (t * x))"
 unfolding exp_Euler cos_of_real by (simp flip: interval_lebesgue_integral_of_real)
 also have "\ = 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])
 finally show "(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)
 also have "\ = (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)
 also have "\ = (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)
 also have "\ = (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)
 also have "\ = (LINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))"
 by (rule integral_complex_of_real)
 finally have "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
 also have "\ \ (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
 moreover have "x \ 2 * sin x" if "x \ - 2" for x :: real
 by (rule order_trans[OF \<open>x \<le> - 2\<close>]) auto
 moreover have "x < 0 \ x \ sin x" for x :: real
 using sin_x_le_x[of "-x"] by simp
 ultimately show ?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)
 finally show "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 :: 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)
 then have 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)
 then have 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
 also have 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)
 also from d0 4 have "\ = d * \ / 4"
 unfolding set_lebesgue_integral_def by simp
 finally have 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)
 then have "(\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)
 then obtain 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
 also have "\ \ 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)
 also have "\ < d * \ / 4 + d * \ / 4"
 by (rule add_less_le_mono [OF N [OF \<open>n \<ge> N\<close>] bound])
 also have "\ = d * \ / 2" by auto
 finally have "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
 also have "?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)
 also have "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)
 finally have "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
 then obtain 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
 then show ?thesis
 by (force intro: order_less_le_trans [OF K Mn.finite_measure_mono])
 next
 case False
 then show ?thesis
 by (force intro: order_less_le_trans [OF 6 Mn.finite_measure_mono])
 qed
 then have "-?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

quality98%

¤ Dauer der Verarbeitung: 0.38 Sekunden ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.