(* 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 I {a <..< b}" 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 ∧ (∀x∈space ?Ω. (λ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. integral⇧^{L}(μ n) f) ⇢ integral⇧^{L}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. integral⇧^{L}(μ n) f) ⇢ integral⇧^{L}M f" using assms by (intro weak_conv_imp_bdd_ae_continuous_conv) (auto intro!: borel_measurable_continuous_on1 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 ≤ integral⇧^{L}M (cts_step x y)" and "integral⇧^{L}M (cts_step x y) ≤ cdf M y" proof - have "cdf M x = integral⇧^{L}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) ≤ integral⇧^{L}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_Iic 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. integral⇧^{L}(M_seq n) (cts_step x y)) ⇢ integral⇧^{L}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. integral⇧^{L}(M_seq n) (cts_step x y))" by (auto intro!: Limsup_mono always_eventually real_distribution.cdf_cts_step) also have "… = integral⇧^{L}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 (integral⇧^{L}M (cts_step y x))" by (simp add: cdf_cts_step) also have "… = liminf (λn. integral⇧^{L}(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. integral⇧^{L}(M_seq n) f::real) ⇢ integral⇧^{L}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