Theory Levy

theory Levy
imports Characteristic_Functions Helly_Selection Sinc_Integral
(*  Title:     HOL/Probability/Levy.thy
    Authors:   Jeremy Avigad (CMU)
*)

section ‹The Levy inversion theorem, and the Levy continuity theorem.›

theory Levy
  imports Characteristic_Functions Helly_Selection Sinc_Integral
begin

subsection ‹The Levy inversion theorem›

(* 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 ‹t ≠ 0› 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"
      apply (rule add_mono)
      apply (rule divide_right_mono)
      using iexp_approx1 [of "-(t * a)" 1] apply (simp add: field_simps eval_nat_numeral)
      apply force
      apply (rule divide_right_mono)
      using iexp_approx1 [of "-(t * b)" 1] apply (simp add: field_simps eval_nat_numeral)
      by force
    also have "… = a^2 / 2 * abs t + b^2 / 2 * abs t"
      using ‹t ≠ 0› apply (case_tac "t ≥ 0", simp add: field_simps power2_eq_square)
      using ‹t ≠ 0› 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 ‹t ≠ 0› 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 ‹t ≠ 0›
    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))
    ⇢ μ {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<..<T} t *R ?f t x"
    { fix x
      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 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 ‹T ≥ 0› by (simp add: interval_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 ‹T ≥ 0›)
      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 ‹T ≥ 0› by (intro interval_integral_cong) (auto simp add: divide_simps)
      also have "… = (CLBINT t=(0::real)..T. complex_of_real(
          2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t)))"
        using ‹T ≥ 0›
        apply (intro interval_integral_cong)
        apply (simp add: field_simps cis.ctr Im_divide Re_divide Im_exp Re_exp complex_eq_iff)
        unfolding minus_diff_eq[symmetric, of "y * x" "y * a" for y a] sin_minus cos_minus
        apply (simp add: field_simps power2_eq_square)
        done
      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 (2 * (sgn (x - a) * Si (T * abs (x - a)) -
          sgn (x - b) * Si (T * abs (x - b))))"
        apply (subst interval_lebesgue_integral_diff)
        apply (rule interval_lebesgue_integrable_mult_right, rule integrable_sinc')+
        apply (subst interval_lebesgue_integral_mult_right)+
        apply (simp add: zero_ereal_def[symmetric] LBINT_I0c_sin_scale_divide[OF ‹T ≥ 0›])
        done
      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 ‹T ≥ 0› unfolding φ_def char_def interval_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 ⨂M M) ({- T<..<T} × space M) < ∞"
        using ‹T ≥ 0›
        by (subst emeasure_pair_measure_Times)
           (auto simp: ennreal_mult_less_top not_less top_unique)
      show "AE x∈{- T<..<T} × space M in lborel ⨂M M. cmod (case x of (t, x) ⇒ ?f' (t, x)) ≤ b - a"
        using Levy_Inversion_aux2[of "x - b" "x - a" for x] ‹a ≤ b›
        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))))) ⇢
       (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}"] ‹μ {a} = 0› ‹μ {b} = 0› by (auto simp: μ_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)))
          ⇢ 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 ‹a ≤ b› 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: μ_def)
  finally have "(λT. LINT x | M. (2 * (sgn (x - a) *
         Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) ⇢
       2 * pi * μ {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 ε :: real
      assume "ε > 0"
      have "(?D ⤏ 0) at_bot"
        using ‹(cdf M1 ⤏ 0) at_bot› ‹(cdf M2 ⤏ 0) at_bot› by (intro tendsto_eq_intros) auto
      then have "eventually (λy. ?D y < ε / 2 ∧ y ≤ x) at_bot"
        using ‹ε > 0› 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 ‹ε > 0› 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 ‹a ≤ x› ‹x < b› have "a < b" "a ≤ b" by auto

      from ‹char M1 = char M2›
        M1.Levy_Inversion [OF ‹a ≤ b› ‹measure M1 {a} = 0› ‹measure M1 {b} = 0›]
        M2.Levy_Inversion [OF ‹a ≤ b› ‹measure M2 {a} = 0› ‹measure M2 {b} = 0›]
      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 ‹a < b›, symmetric] M2.cdf_diff_eq [OF ‹a < b›, 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 ‹real_distribution M1› ‹real_distribution M2›])
qed


subsection ‹The Levy continuity theorem›

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..0. 1 - iexp (t * x)) + (CLBINT t=0..u. 1 - iexp (t * x))"
      using ‹u > 0›
      apply (subst interval_integral_sum)
      apply (simp add: min_absorb1 min_absorb2 max_absorb1 max_absorb2)
      apply (rule interval_integrable_isCont)
      apply auto
      done
    also have "… = (CLBINT t=ereal 0..u. 1 - iexp (t * -x)) + (CLBINT t=ereal 0..u. 1 - iexp (t * x))"
      apply (subgoal_tac "0 = ereal 0", erule ssubst)
      by (subst interval_integral_reflect, auto)
    also have "… = (LBINT t=ereal 0..u. 2 - 2 * cos (t * x))"
      apply (subst interval_lebesgue_integral_add (2) [symmetric])
      apply ((rule interval_integrable_isCont, auto)+) [2]
      unfolding exp_Euler cos_of_real
      apply (simp add: of_real_mult interval_lebesgue_integral_of_real[symmetric])
      done
    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 ‹x ≠ 0›] 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 ≥ 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 ⨂M lborel) (UNIV × {- u..u}) (λa. 1 - exp (𝗂 * complex_of_real (snd a * fst a)))"
      using ‹0 < u›
      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 *R (1 - iexp (t * x))))"
      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')
    also have "… = (CLINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
      using ‹u > 0› 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 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 ‹u > 0› by (subst 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 _ ‹2 ≤ x›]) auto
      moreover have "x ≤ 2 * sin x" if "x ≤ - 2" for x :: real
        by (rule order_trans[OF ‹x ≤ - 2›]) auto
      moreover have "x < 0 ⟹ x ≤ sin x" for x :: real
        using sin_x_le_x[of "-x"] by simp
      ultimately show ?thesis
        using ‹u > 0›
        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}"
      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 < b ∧ (∀n. 1 - ε < measure (M n) {a<..b})"
  proof -
    fix ε :: real
    assume "ε > 0"
    note M'.isCont_char [of 0]
    hence "∃d>0. ∀t. abs t < d ⟶ cmod (char M' t - 1) < ε / 4"
      apply (subst (asm) continuous_at_eps_delta)
      apply (drule_tac x = "ε / 4" in spec)
      using ‹ε > 0› by (auto simp add: dist_real_def dist_complex_def M'.char_zero)
    then obtain d where "d > 0 ∧ (∀t. (abs t < d ⟶ cmod (char M' t - 1) < ε / 4))" ..
    hence d0: "d > 0" and d1: "⋀t. abs t < d ⟹ cmod (char M' t - 1) < ε / 4" by auto
    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)"
      by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq)
    have 3: "⋀u v. set_integrable lborel {u..v} (λx. 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)"
      using integral_norm_bound[of _ "λx. indicator {u..v} x *R (1 - char M' x)" for u v] by simp
    also have 4: "… ≤ LBINT t:{-d/2..d/2}. ε / 4"
      apply (rule integral_mono [OF 3])
       apply (simp add: emeasure_lborel_Icc_eq)
      apply (case_tac "x ∈ {-d/2..d/2}")
       apply auto
      apply (subst norm_minus_commute)
      apply (rule less_imp_le)
      apply (rule d1 [simplified])
      using d0 apply auto
      done
    also from d0 4 have "… = d * ε / 4"
      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)"
      apply (intro integral_dominated_convergence[where w="λx. indicator {-d/2..d/2} x *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 ‹ε > 0› 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 guess N ..
    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 ‹n ≥ N›] 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 ‹ε > 0› have "ε > measure (M n) {x. abs x ≥ 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 apply (auto simp add: field_simps)
        (* very annoying -- this should be automatic *)
        apply (case_tac "x ≥ 0", auto simp add: field_simps)
        apply (subgoal_tac "0 ≤ x * d", arith, rule mult_nonneg_nonneg, auto)
        apply (case_tac "x ≥ 0", auto simp add: field_simps)
        apply (subgoal_tac "x * d ≤ 0", arith)
        apply (rule mult_nonpos_nonneg, auto)
        by (case_tac "x ≥ 0", auto simp add: field_simps)
      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"
        apply (elim order_tendstoD (1))
        using ‹ε > 0› by auto
    } 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<N. 1 - ε <
        Sigma_Algebra.measure (M m) {- real k<..real k}"
      by (auto simp add: eventually_sequentially)
    hence "∃K :: nat. ∀m<N. 1 - ε < Sigma_Algebra.measure (M m) {- real K<..real K}" by auto
    then obtain K :: nat where
      "∀m<N. 1 - ε < 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 "-?K' < ?K' ∧ (∀n. 1 - ε < measure (M n) {-?K'<..?K'})"
      using d0 apply auto
      apply (rule max.strict_coboundedI2, auto)
    proof -
      fix n
      show " 1 - ε < measure (M n) {- max (real K) (4 / d)<..max (real K) (4 / d)}"
        apply (case_tac "n < N")
        apply (rule order_less_le_trans)
        apply (erule K)
        apply (rule Mn.finite_measure_mono, auto)
        apply (rule order_less_le_trans)
        apply (rule 6, erule leI)
        by (rule Mn.finite_measure_mono, auto)
    qed
    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 ν
    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