Theory HOL-Probability.Weak_Convergence

(*  Title:     HOL/Probability/Weak_Convergence.thy
    Authors:   Jeremy Avigad (CMU), Johannes Hölzl (TUM)
*)

section ‹Weak Convergence of Functions and Distributions›

text ‹Properties of weak convergence of functions and measures, including the portmanteau theorem.›

theory Weak_Convergence
  imports Distribution_Functions
begin

section ‹Weak Convergence of Functions›

definition
  weak_conv :: "(nat  (real  real))  (real  real)  bool"
where
  "weak_conv F_seq F  x. isCont F x  (λn. F_seq n x)  F x"

section ‹Weak Convergence of Distributions›

definition
  weak_conv_m :: "(nat  real measure)  real measure  bool"
where
  "weak_conv_m M_seq M  weak_conv (λn. cdf (M_seq n)) (cdf M)"

section ‹Skorohod's theorem›

locale right_continuous_mono =
  fixes f :: "real  real" and a b :: real
  assumes cont: "x. continuous (at_right x) f"
  assumes mono: "mono f"
  assumes bot: "(f  a) at_bot"
  assumes top: "(f  b) at_top"
begin

abbreviation I :: "real  real" where
  "I ω  Inf {x. ω  f x}"

lemma pseudoinverse: assumes "a < ω" "ω < b" shows "ω  f x  I ω  x"
proof
  let ?F = "{x. ω  f x}"
  obtain y where "f y < ω"
    by (metis eventually_happens' trivial_limit_at_bot_linorder order_tendstoD(2) bot a < ω)
  with mono have bdd: "bdd_below ?F"
    by (auto intro!: bdd_belowI[of _ y] elim: mono_invE[OF _ less_le_trans])

  have ne: "?F  {}"
    using order_tendstoD(1)[OF top ω < b]
    by (auto dest!: eventually_happens'[OF trivial_limit_at_top_linorder] intro: less_imp_le)

  show "ω  f x  I ω  x"
    by (auto intro!: cInf_lower bdd)

  { assume *: "I ω  x"
    have "ω  (INF s{x. ω  f x}. f s)"
      by (rule cINF_greatest[OF ne]) auto
    also have " = f (I ω)"
      using continuous_at_Inf_mono[OF mono cont ne bdd] ..
    also have "  f x"
      using * by (rule monoD[OF mono f])
    finally show "ω  f x" . }
qed

lemma pseudoinverse': "ω{a<..<b}. x. ω  f x  I ω  x"
  by (intro ballI allI impI pseudoinverse) auto

lemma mono_I: "mono_on {a <..< b} I"
  unfolding mono_on_def by (metis order.trans order.refl pseudoinverse')

end

locale cdf_distribution = real_distribution
begin

abbreviation "C  cdf M"

sublocale right_continuous_mono C 0 1
  by standard
     (auto intro: cdf_nondecreasing cdf_is_right_cont cdf_lim_at_top_prob cdf_lim_at_bot monoI)

lemma measurable_C[measurable]: "C  borel_measurable borel"
  by (intro borel_measurable_mono mono)

lemma measurable_CI[measurable]: "I  borel_measurable (restrict_space borel {0<..<1})"
  by (intro borel_measurable_mono_on_fnc mono_I)

lemma emeasure_distr_I: "emeasure (distr (restrict_space lborel {0<..<1::real}) borel I) UNIV = 1"
  by (simp add: emeasure_distr space_restrict_space emeasure_restrict_space )

lemma distr_I_eq_M: "distr (restrict_space lborel {0<..<1::real}) borel I = M" (is "?I = _")
proof (intro cdf_unique ext)
  let  = "restrict_space lborel {0<..<1}::real measure"
  interpret Ω: prob_space 
    by (auto simp add: emeasure_restrict_space space_restrict_space intro!: prob_spaceI)
  show "real_distribution ?I"
    by auto

  fix x
  have "cdf ?I x = measure lborel {ω{0<..<1}. ω  C x}"
    by (subst cdf_def)
       (auto simp: pseudoinverse[symmetric] measure_distr space_restrict_space measure_restrict_space
             intro!: arg_cong2[where f="measure"])
  also have " = measure lborel {0 <..< C x}"
    using cdf_bounded_prob[of x] AE_lborel_singleton[of "C x"]
    by (auto intro!: arg_cong[where f=enn2real] emeasure_eq_AE simp: measure_def)
  also have " = C x"
    by (simp add: cdf_nonneg)
  finally show "cdf (distr  borel I) x = C x" .
qed standard

end

context
  fixes μ :: "nat  real measure"
    and M :: "real measure"
  assumes μ: "n. real_distribution (μ n)"
  assumes M: "real_distribution M"
  assumes μ_to_M: "weak_conv_m μ M"
begin

(* state using obtains? *)
theorem Skorohod:
 " (Ω :: real measure) (Y_seq :: nat  real  real) (Y :: real  real).
    prob_space Ω 
    (n. Y_seq n  measurable Ω borel) 
    (n. distr Ω borel (Y_seq n) = μ n) 
    Y  measurable Ω lborel 
    distr Ω borel Y = M 
    (x  space Ω. (λn. Y_seq n x)  Y x)"
proof -
  interpret μ: cdf_distribution "μ n" for n
    unfolding cdf_distribution_def by (rule μ)
  interpret M: cdf_distribution M
    unfolding cdf_distribution_def by (rule M)

  have conv: "measure M {x} = 0  (λn. μ.C n x)  M.C x" for x
    using μ_to_M M.isCont_cdf by (auto simp: weak_conv_m_def weak_conv_def)

  let  = "restrict_space lborel {0<..<1} :: real measure"
  have "prob_space "
    by (auto simp: space_restrict_space emeasure_restrict_space intro!: prob_spaceI)
  interpret Ω: prob_space 
    by fact

  have Y_distr: "distr  borel M.I = M"
    by (rule M.distr_I_eq_M)

  have Y_cts_cnv: "(λn. μ.I n ω)  M.I ω"
    if ω: "ω  {0<..<1}" "isCont M.I ω" for ω :: real
  proof (intro limsup_le_liminf_real)
    show "liminf (λn. μ.I n ω)  M.I ω"
      unfolding le_Liminf_iff
    proof safe
      fix B :: ereal assume B: "B < M.I ω"
      then show "F n in sequentially. B < μ.I n ω"
      proof (cases B)
        case (real r)
        with B have r: "r < M.I ω"
          by simp
        then obtain x where x: "r < x" "x < M.I ω" "measure M {x} = 0"
          using open_minus_countable[OF M.countable_support, of "{r<..<M.I ω}"] by auto
        then have Fx_less: "M.C x < ω"
          using M.pseudoinverse' ω not_less by blast

        have "F n in sequentially. μ.C n x < ω"
          using order_tendstoD(2)[OF conv[OF x(3)] Fx_less] .
        then have "F n in sequentially. x < μ.I n ω"
          by eventually_elim (insert ω μ.pseudoinverse[symmetric], simp add: not_le[symmetric])
        then show ?thesis
          by eventually_elim (insert x(1), simp add: real)
      qed auto
    qed

    have *: "limsup (λn. μ.I n ω)  M.I ω'"
      if ω': "0 < ω'" "ω' < 1" "ω < ω'" for ω' :: real
    proof (rule dense_ge_bounded)
      fix B' assume "ereal (M.I ω') < B'" "B' < ereal (M.I ω' + 1)"
      then obtain B where "M.I ω' < B" and [simp]: "B' = ereal B"
        by (cases B') auto
      then obtain y where y: "M.I ω' < y" "y < B" "measure M {y} = 0"
        using open_minus_countable[OF M.countable_support, of "{M.I ω'<..<B}"] by auto
      then have "ω'  M.C (M.I ω')"
        using M.pseudoinverse' ω' by (metis greaterThanLessThan_iff order_refl)
      also have "...  M.C y"
        using M.mono y unfolding mono_def by auto
      finally have Fy_gt: "ω < M.C y"
        using ω'(3) by simp

      have "F n in sequentially. ω  μ.C n y"
        using order_tendstoD(1)[OF conv[OF y(3)] Fy_gt] by eventually_elim (rule less_imp_le)
      then have 2: "F n in sequentially. μ.I n ω  ereal y"
        by simp (subst μ.pseudoinverse'[rule_format, OF ω(1), symmetric])
      then show "limsup (λn. μ.I n ω)  B'"
        using y < B
        by (intro Limsup_bounded[rotated]) (auto intro: le_less_trans elim: eventually_mono)
    qed simp

    have **: "(M.I  ereal (M.I ω)) (at_right ω)"
      using ω(2) by (auto intro: tendsto_within_subset simp: continuous_at)
    show "limsup (λn. μ.I n ω)  M.I ω"
      using ω
      by (intro tendsto_lowerbound[OF **])
         (auto intro!: exI[of _ 1] * simp: eventually_at_right[of _ 1])
  qed

  let ?D = "{ω{0<..<1}. ¬ isCont M.I ω}"
  have D_countable: "countable ?D"
    using mono_on_ctble_discont[OF M.mono_I] by (simp add: at_within_open[of _ "{0 <..< 1}"] cong: conj_cong)
  hence D: "emeasure  ?D = 0"
    using emeasure_lborel_countable[OF D_countable]
    by (subst emeasure_restrict_space) auto

  define Y' where "Y' ω = (if ω  ?D then 0 else M.I ω)" for ω
  have Y'_AE: "AE ω in . Y' ω = M.I ω"
    by (rule AE_I [OF _ D]) (auto simp: space_restrict_space sets_restrict_space_iff Y'_def)

  define Y_seq' where "Y_seq' n ω = (if ω  ?D then 0 else μ.I n ω)" for n ω
  have Y_seq'_AE: "n. AE ω in . Y_seq' n ω = μ.I n ω"
    by (rule AE_I [OF _ D]) (auto simp: space_restrict_space sets_restrict_space_iff Y_seq'_def)

  have Y'_cnv: "ω{0<..<1}. (λn. Y_seq' n ω)  Y' ω"
    by (auto simp: Y'_def Y_seq'_def Y_cts_cnv)

  have [simp]: "Y_seq' n  borel_measurable " for n
    by (rule measurable_discrete_difference[of "μ.I n" _ _ ?D])
       (insert μ.measurable_CI[of n] D_countable, auto simp: sets_restrict_space Y_seq'_def)
  moreover have "distr  borel (Y_seq' n) = μ n" for n
    using μ.distr_I_eq_M [of n] Y_seq'_AE [of n]
    by (subst distr_cong_AE[where f = "Y_seq' n" and g = "μ.I n"], auto)
  moreover have [simp]: "Y'  borel_measurable "
    by (rule measurable_discrete_difference[of M.I _ _ ?D])
       (insert M.measurable_CI D_countable, auto simp: sets_restrict_space Y'_def)
  moreover have "distr  borel Y' = M"
    using M.distr_I_eq_M Y'_AE
    by (subst distr_cong_AE[where f = Y' and g = M.I], auto)
  ultimately have "prob_space   (n. Y_seq' n  borel_measurable ) 
    (n. distr  borel (Y_seq' n) = μ n)  Y'  measurable  lborel  distr  borel Y' = M 
    (xspace . (λn. Y_seq' n x)  Y' x)"
    using Y'_cnv prob_space  by (auto simp: space_restrict_space)
  thus ?thesis by metis
qed

text ‹
  The Portmanteau theorem, that is, the equivalence of various definitions of weak convergence.
›

theorem weak_conv_imp_bdd_ae_continuous_conv:
  fixes
    f :: "real  'a::{banach, second_countable_topology}"
  assumes
    discont_null: "M ({x. ¬ isCont f x}) = 0" and
    f_bdd: "x. norm (f x)  B" and
    [measurable]: "f  borel_measurable borel"
  shows
    "(λ n. integralL (μ n) f)  integralL M f"
proof -
  have "0  B"
    using norm_ge_zero f_bdd by (rule order_trans)
  note Skorohod
  then obtain Omega Y_seq Y where
    ps_Omega [simp]: "prob_space Omega" and
    Y_seq_measurable [measurable]: "n. Y_seq n  borel_measurable Omega" and
    distr_Y_seq: "n. distr Omega borel (Y_seq n) = μ n" and
    Y_measurable [measurable]: "Y  borel_measurable Omega" and
    distr_Y: "distr Omega borel Y = M" and
    YnY: "x :: real. x  space Omega  (λn. Y_seq n x)  Y x"  by force
  interpret prob_space Omega by fact
  have *: "emeasure Omega (Y -` {x. ¬ isCont f x}  space Omega) = 0"
    by (subst emeasure_distr [symmetric, where N=borel]) (auto simp: distr_Y discont_null)
  have *: "AE x in Omega. (λn. f (Y_seq n x))  f (Y x)"
    by (rule AE_I [OF _ *]) (auto intro: isCont_tendsto_compose YnY)
  show ?thesis
    by (auto intro!: integral_dominated_convergence[where w="λx. B"]
             simp: f_bdd * integral_distr distr_Y_seq [symmetric] distr_Y [symmetric])
qed

theorem weak_conv_imp_integral_bdd_continuous_conv:
  fixes f :: "real  'a::{banach, second_countable_topology}"
  assumes
    "x. isCont f x" and
    "x. norm (f x)  B"
  shows
    "(λ n. integralL (μ n) f)  integralL M f"
  using assms
  by (intro weak_conv_imp_bdd_ae_continuous_conv)
     (auto intro!: borel_measurable_continuous_onI continuous_at_imp_continuous_on)

theorem weak_conv_imp_continuity_set_conv:
  fixes f :: "real  real"
  assumes [measurable]: "A  sets borel" and "M (frontier A) = 0"
  shows "(λn. measure (μ n) A)  measure M A"
proof -
  interpret M: real_distribution M by fact
  interpret μ: real_distribution "μ n" for n by fact

  have "(λn. (x. indicator A x μ n) :: real)  (x. indicator A x M)"
    by (intro weak_conv_imp_bdd_ae_continuous_conv[where B=1])
       (auto intro: assms simp: isCont_indicator)
  then show ?thesis
    by simp
qed

end

definition
  cts_step :: "real  real  real  real"
where
  "cts_step a b x  if x  a then 1 else if x  b then 0 else (b - x) / (b - a)"

lemma cts_step_uniformly_continuous:
  assumes [arith]: "a < b"
  shows "uniformly_continuous_on UNIV (cts_step a b)"
  unfolding uniformly_continuous_on_def
proof clarsimp
  fix e :: real assume [arith]: "0 < e"
  let ?d = "min (e * (b - a)) (b - a)"
  have "?d > 0"
    by (auto simp add: field_simps)
  moreover have "dist x' x < ?d  dist (cts_step a b x') (cts_step a b x) < e" for x x'
    by (auto simp: dist_real_def divide_simps cts_step_def)
  ultimately show "d > 0. x x'. dist x' x < d  dist (cts_step a b x') (cts_step a b x) < e"
    by blast
qed

lemma (in real_distribution) integrable_cts_step: "a < b  integrable M (cts_step a b)"
  by (rule integrable_const_bound [of _ 1]) (auto simp: cts_step_def[abs_def])

lemma (in real_distribution) cdf_cts_step:
  assumes [arith]: "x < y"
  shows "cdf M x  integralL M (cts_step x y)" and "integralL M (cts_step x y)  cdf M y"
proof -
  have "cdf M x = integralL M (indicator {..x})"
    by (simp add: cdf_def)
  also have "  expectation (cts_step x y)"
    by (intro integral_mono integrable_cts_step)
       (auto simp: cts_step_def less_top[symmetric] split: split_indicator)
  finally show "cdf M x  expectation (cts_step x y)" .
next
  have "expectation (cts_step x y)  integralL M (indicator {..y})"
    by (intro integral_mono integrable_cts_step)
       (auto simp: cts_step_def less_top[symmetric] split: split_indicator)
  also have " = cdf M y"
    by (simp add: cdf_def)
  finally show "expectation (cts_step x y)  cdf M y" .
qed

context
  fixes M_seq :: "nat  real measure"
    and M :: "real measure"
  assumes distr_M_seq [simp]: "n. real_distribution (M_seq n)"
  assumes distr_M [simp]: "real_distribution M"
begin

theorem continuity_set_conv_imp_weak_conv:
  fixes f :: "real  real"
  assumes *: "A. A  sets borel  M (frontier A) = 0  (λ n. (measure (M_seq n) A))  measure M A"
  shows "weak_conv_m M_seq M"
proof -
  interpret real_distribution M by simp
  show ?thesis
    by (auto intro!: * simp: frontier_real_atMost isCont_cdf emeasure_eq_measure weak_conv_m_def weak_conv_def cdf_def2)
qed

theorem integral_cts_step_conv_imp_weak_conv:
  assumes integral_conv: "x y. x < y  (λn. integralL (M_seq n) (cts_step x y))  integralL M (cts_step x y)"
  shows "weak_conv_m M_seq M"
  unfolding weak_conv_m_def weak_conv_def
proof (clarsimp)
  interpret real_distribution M by (rule distr_M)
  fix x assume "isCont (cdf M) x"
  hence left_cont: "continuous (at_left x) (cdf M)"
    unfolding continuous_at_split ..
  { fix y :: real assume [arith]: "x < y"
    have "limsup (λn. cdf (M_seq n) x)  limsup (λn. integralL (M_seq n) (cts_step x y))"
      by (auto intro!: Limsup_mono always_eventually real_distribution.cdf_cts_step)
    also have " = integralL M (cts_step x y)"
      by (intro lim_imp_Limsup) (auto intro: integral_conv)
    also have "  cdf M y"
      by (simp add: cdf_cts_step)
    finally have "limsup (λn. cdf (M_seq n) x)  cdf M y" .
  } note * = this
  { fix y :: real assume [arith]: "x > y"
    have "cdf M y  ereal (integralL M (cts_step y x))"
      by (simp add: cdf_cts_step)
    also have " = liminf (λn. integralL (M_seq n) (cts_step y x))"
      by (intro lim_imp_Liminf[symmetric]) (auto intro: integral_conv)
    also have "  liminf (λn. cdf (M_seq n) x)"
      by (auto intro!: Liminf_mono always_eventually real_distribution.cdf_cts_step)
    finally have "liminf (λn. cdf (M_seq n) x)  cdf M y" .
  } note ** = this

  have "limsup (λn. cdf (M_seq n) x)  cdf M x"
  proof (rule tendsto_lowerbound)
    show "F i in at_right x. limsup (λxa. ereal (cdf (M_seq xa) x))  ereal (cdf M i)"
      by (subst eventually_at_right[of _ "x + 1"]) (auto simp: * intro: exI [of _ "x+1"])
  qed (insert cdf_is_right_cont, auto simp: continuous_within)
  moreover have "cdf M x  liminf (λn. cdf (M_seq n) x)"
  proof (rule tendsto_upperbound)
    show "F i in at_left x. ereal (cdf M i)  liminf (λxa. ereal (cdf (M_seq xa) x))"
      by (subst eventually_at_left[of "x - 1"]) (auto simp: ** intro: exI [of _ "x-1"])
  qed (insert left_cont, auto simp: continuous_within)
  ultimately show "(λn. cdf (M_seq n) x)  cdf M x"
    by (elim limsup_le_liminf_real)
qed

theorem integral_bdd_continuous_conv_imp_weak_conv:
  assumes
    "f. (x. isCont f x)  (x. abs (f x)  1)  (λn. integralL (M_seq n) f::real)  integralL M f"
  shows
    "weak_conv_m M_seq M"
  apply (rule integral_cts_step_conv_imp_weak_conv [OF assms])
  apply (rule continuous_on_interior)
  apply (rule uniformly_continuous_imp_continuous)
  apply (rule cts_step_uniformly_continuous)
  apply (auto simp: cts_step_def)
  done

end

end