(* Title: HOL/Probability/Weak_Convergence.thy
Authors: Jeremy Avigad (CMU), Johannes Hölzl (TUM)
*)
section \<open>Weak Convergence of Functions and Distributions\<close>
text \<open>Properties of weak convergence of functions and measures, including the portmanteau theorem.\<close>
theory Weak_Convergence
imports Distribution_Functions
begin
section \<open>Weak Convergence of Functions\<close>
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 \<open>Weak Convergence of Distributions\<close>
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 \<open>Skorohod's theorem\<close>
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 \<open>\<omega> < b\<close>]
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 \<open>mono f\<close>])
finally show "\ \ f x" . }
qed
lemma pseudoinverse': "\\\{a<..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 ?\<Omega> = "restrict_space lborel {0<..<1}::real measure"
interpret \<Omega>: prob_space ?\<Omega>
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 \<mu> :: "nat \<Rightarrow> real measure"
and M :: "real measure"
assumes \<mu>: "\<And>n. real_distribution (\<mu> n)"
assumes M: "real_distribution M"
assumes \<mu>_to_M: "weak_conv_m \<mu> M"
begin
(* state using obtains? *)
theorem Skorohod:
"\ (\ :: real measure) (Y_seq :: nat \ real \ real) (Y :: real \ real).
prob_space \<Omega> \<and>
(\<forall>n. Y_seq n \<in> measurable \<Omega> borel) \<and>
(\<forall>n. distr \<Omega> borel (Y_seq n) = \<mu> n) \<and>
Y \<in> measurable \<Omega> lborel \<and>
distr \<Omega> borel Y = M \<and>
(\<forall>x \<in> space \<Omega>. (\<lambda>n. Y_seq n x) \<longlonglongrightarrow> Y x)"
proof -
interpret \<mu>: cdf_distribution "\<mu> n" for n
unfolding cdf_distribution_def by (rule \<mu>)
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 \<mu>_to_M M.isCont_cdf by (auto simp: weak_conv_m_def weak_conv_def)
let ?\<Omega> = "restrict_space lborel {0<..<1} :: real measure"
have "prob_space ?\"
by (auto simp: space_restrict_space emeasure_restrict_space intro!: prob_spaceI)
interpret \<Omega>: prob_space ?\<Omega>
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 \<omega>: "\<omega> \<in> {0<..<1}" "isCont M.I \<omega>" for \<omega> :: 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 "\\<^sub>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<..}"] by auto
then have Fx_less: "M.C x < \"
using M.pseudoinverse' \ not_less by blast
have "\\<^sub>F n in sequentially. \.C n x < \"
using order_tendstoD(2)[OF conv[OF x(3)] Fx_less] .
then have "\\<^sub>F n in sequentially. x < \.I n \"
by eventually_elim (insert \<omega> \<mu>.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 \<omega>': "0 < \<omega>'" "\<omega>' < 1" "\<omega> < \<omega>'" for \<omega>' :: 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 \'<..
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 \<omega>'(3) by simp
have "\\<^sub>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: "\\<^sub>F n in sequentially. \.I n \ \ ereal y"
by simp (subst \<mu>.pseudoinverse'[rule_format, OF \<omega>(1), symmetric])
then show "limsup (\n. \.I n \) \ B'"
using \<open>y < B\<close>
by (intro Limsup_bounded[rotated]) (auto intro: le_less_trans elim: eventually_mono)
qed simp
have **: "(M.I \ ereal (M.I \)) (at_right \)"
using \<omega>(2) by (auto intro: tendsto_within_subset simp: continuous_at)
show "limsup (\n. \.I n \) \ M.I \"
using \<omega>
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' \<omega> = (if \<omega> \<in> ?D then 0 else M.I \<omega>)" for \<omega>
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 \<omega> = (if \<omega> \<in> ?D then 0 else \<mu>.I n \<omega>)" for n \<omega>
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 \<mu>.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 \<mu>.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 ?\) \
(\<forall>n. distr ?\<Omega> borel (Y_seq' n) = \<mu> n) \<and> Y' \<in> measurable ?\<Omega> lborel \<and> distr ?\<Omega> borel Y' = M \<and>
(\<forall>x\<in>space ?\<Omega>. (\<lambda>n. Y_seq' n x) \<longlonglongrightarrow> Y' x)"
using Y'_cnv \prob_space ?\\ by (auto simp: space_restrict_space)
thus ?thesis by metis
qed
text \<open>
The Portmanteau theorem, that is, the equivalence of various definitions of weak convergence.
\<close>
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\<^sup>L (\ n) f) \ integral\<^sup>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\<^sup>L (\ n) f) \ integral\<^sup>L 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 \<mu>: real_distribution "\<mu> 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\<^sup>L M (cts_step x y)" and "integral\<^sup>L M (cts_step x y) \ cdf M y"
proof -
have "cdf M x = integral\<^sup>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\<^sup>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_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. integral\<^sup>L (M_seq n) (cts_step x y)) \ integral\<^sup>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\<^sup>L (M_seq n) (cts_step x y))"
by (auto intro!: Limsup_mono always_eventually real_distribution.cdf_cts_step)
also have "\ = integral\<^sup>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\<^sup>L M (cts_step y x))"
by (simp add: cdf_cts_step)
also have "\ = liminf (\n. integral\<^sup>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 "\\<^sub>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 "\\<^sub>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\<^sup>L (M_seq n) f::real) \ integral\<^sup>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
¤ Dauer der Verarbeitung: 0.8 Sekunden
(vorverarbeitet)
¤
|
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.
|
