(* Title: HOL/Probability/Helly_Selection.thy
Authors: Jeremy Avigad (CMU), Luke Serafin (CMU)
Authors: Johannes Hölzl, TU München
*)
section \<open>Helly's selection theorem\<close>
text \<open>The set of bounded, monotone, right continuous functions is sequentially compact\<close>
theory Helly_Selection
imports "HOL-Library.Diagonal_Subsequence" Weak_Convergence
begin
lemma minus_one_less: "x - 1 < (x::real)"
by simp
theorem Helly_selection:
fixes f :: "nat \ real \ real"
assumes rcont: "\n x. continuous (at_right x) (f n)"
assumes mono: "\n. mono (f n)"
assumes bdd: "\n x. \f n x\ \ M"
shows "\s. strict_mono (s::nat \ nat) \ (\F. (\x. continuous (at_right x) F) \ mono F \ (\x. \F x\ \ M) \
(\<forall>x. continuous (at x) F \<longrightarrow> (\<lambda>n. f (s n) x) \<longlonglongrightarrow> F x))"
proof -
obtain m :: "real \ nat" where "bij_betw m \ UNIV"
using countable_rat Rats_infinite by (erule countableE_infinite)
then obtain r :: "nat \ real" where bij: "bij_betw r UNIV \"
using bij_betw_inv by blast
have dense_r: "\x y. x < y \ \n. x < r n \ r n < y"
by (metis Rats_dense_in_real bij f_the_inv_into_f bij_betw_def)
let ?P = "\n. \s. convergent (\k. f (s k) (r n))"
interpret nat: subseqs ?P
proof (unfold convergent_def, unfold subseqs_def, auto)
fix n :: nat and s :: "nat \ nat" assume s: "strict_mono s"
have "bounded {-M..M}"
using bounded_closed_interval by auto
moreover have "\k. f (s k) (r n) \ {-M..M}"
using bdd by (simp add: abs_le_iff minus_le_iff)
ultimately have "\l s'. strict_mono s' \ ((\k. f (s k) (r n)) \ s') \ l"
using compact_Icc compact_imp_seq_compact seq_compactE by metis
thus "\s'. strict_mono (s'::nat\nat) \ (\l. (\k. f (s (s' k)) (r n)) \ l)"
by (auto simp: comp_def)
qed
define d where "d = nat.diagseq"
have subseq: "strict_mono d"
unfolding d_def using nat.subseq_diagseq by auto
have rat_cnv: "?P n d" for n
proof -
have Pn_seqseq: "?P n (nat.seqseq (Suc n))"
by (rule nat.seqseq_holds)
have 1: "(\k. f ((nat.seqseq (Suc n) \ (\k. nat.fold_reduce (Suc n) k
(Suc n + k))) k) (r n)) = (\<lambda>k. f (nat.seqseq (Suc n) k) (r n)) \<circ>
(\<lambda>k. nat.fold_reduce (Suc n) k (Suc n + k))"
by auto
have 2: "?P n (d \ ((+) (Suc n)))"
unfolding d_def nat.diagseq_seqseq 1
by (intro convergent_subseq_convergent Pn_seqseq nat.subseq_diagonal_rest)
then obtain L where 3: "(\na. f (d (na + Suc n)) (r n)) \ L"
by (auto simp: add.commute dest: convergentD)
then have "(\k. f (d k) (r n)) \ L"
by (rule LIMSEQ_offset)
then show ?thesis
by (auto simp: convergent_def)
qed
let ?f = "\n. \k. f (d k) (r n)"
have lim_f: "?f n \ lim (?f n)" for n
using rat_cnv convergent_LIMSEQ_iff by auto
have lim_bdd: "lim (?f n) \ {-M..M}" for n
proof -
have "closed {-M..M}" using closed_real_atLeastAtMost by auto
hence "(\i. ?f n i \ {-M..M}) \ ?f n \ lim (?f n) \ lim (?f n) \ {-M..M}"
unfolding closed_sequential_limits by (drule_tac x = "\k. f (d k) (r n)" in spec) blast
moreover have "\i. ?f n i \ {-M..M}"
using bdd by (simp add: abs_le_iff minus_le_iff)
ultimately show "lim (?f n) \ {-M..M}"
using lim_f by auto
qed
then have limset_bdd: "\x. {lim (?f n) |n. x < r n} \ {-M..M}"
by auto
then have bdd_below: "bdd_below {lim (?f n) |n. x < r n}" for x
by (metis (mono_tags) bdd_below_Icc bdd_below_mono)
have r_unbdd: "\n. x < r n" for x
using dense_r[OF less_add_one, of x] by auto
then have nonempty: "{lim (?f n) |n. x < r n} \ {}" for x
by auto
define F where "F x = Inf {lim (?f n) |n. x < r n}" for x
have F_eq: "ereal (F x) = (INF n\{n. x < r n}. ereal (lim (?f n)))" for x
unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image image_comp)
have mono_F: "mono F"
using nonempty by (auto intro!: cInf_superset_mono simp: F_def bdd_below mono_def)
moreover have "\x. continuous (at_right x) F"
unfolding continuous_within order_tendsto_iff eventually_at_right[OF less_add_one]
proof safe
show "F x < u \ \b>x. \y>x. y < b \ F y < u" for x u
unfolding F_def cInf_less_iff[OF nonempty bdd_below] by auto
next
show "\b>x. \y>x. y < b \ l < F y" if l: "l < F x" for x l
using less_le_trans[OF l mono_F[THEN monoD, of x]] by (auto intro: less_add_one)
qed
moreover
{ fix x
have "F x \ {-M..M}"
unfolding F_def using limset_bdd bdd_below r_unbdd by (intro closed_subset_contains_Inf) auto
then have "\F x\ \ M" by auto }
moreover have "(\n. f (d n) x) \ F x" if cts: "continuous (at x) F" for x
proof (rule limsup_le_liminf_real)
show "limsup (\n. f (d n) x) \ F x"
proof (rule tendsto_lowerbound)
show "(F \ ereal (F x)) (at_right x)"
using cts unfolding continuous_at_split by (auto simp: continuous_within)
show "\\<^sub>F i in at_right x. limsup (\n. f (d n) x) \ F i"
unfolding eventually_at_right[OF less_add_one]
proof (rule, rule, rule less_add_one, safe)
fix y assume y: "x < y"
with dense_r obtain N where "x < r N" "r N < y" by auto
have *: "y < r n' \ lim (?f N) \ lim (?f n')" for n'
using \<open>r N < y\<close> by (intro LIMSEQ_le[OF lim_f lim_f]) (auto intro!: mono[THEN monoD])
have "limsup (\n. f (d n) x) \ limsup (?f N)"
using \<open>x < r N\<close> by (auto intro!: Limsup_mono always_eventually mono[THEN monoD])
also have "\ = lim (\n. ereal (?f N n))"
using rat_cnv[of N] by (force intro!: convergent_limsup_cl simp: convergent_def)
also have "\ \ F y"
by (auto intro!: INF_greatest * simp: convergent_real_imp_convergent_ereal rat_cnv F_eq)
finally show "limsup (\n. f (d n) x) \ F y" .
qed
qed simp
show "F x \ liminf (\n. f (d n) x)"
proof (rule tendsto_upperbound)
show "(F \ ereal (F x)) (at_left x)"
using cts unfolding continuous_at_split by (auto simp: continuous_within)
show "\\<^sub>F i in at_left x. F i \ liminf (\n. f (d n) x)"
unfolding eventually_at_left[OF minus_one_less]
proof (rule, rule, rule minus_one_less, safe)
fix y assume y: "y < x"
with dense_r obtain N where "y < r N" "r N < x" by auto
have "F y \ liminf (?f N)"
using \<open>y < r N\<close> by (auto simp: F_eq convergent_real_imp_convergent_ereal
rat_cnv convergent_liminf_cl intro!: INF_lower2)
also have "\ \ liminf (\n. f (d n) x)"
using \<open>r N < x\<close> by (auto intro!: Liminf_mono monoD[OF mono] always_eventually)
finally show "F y \ liminf (\n. f (d n) x)" .
qed
qed simp
qed
ultimately show ?thesis using subseq by auto
qed
(** Weak convergence corollaries to Helly's theorem. **)
definition
tight :: "(nat \ real measure) \ bool"
where
"tight \ \ (\n. real_distribution (\ n)) \ (\(\::real)>0. \a b::real. a < b \ (\n. measure (\ n) {a<..b} > 1 - \))"
(* Can strengthen to equivalence. *)
theorem tight_imp_convergent_subsubsequence:
assumes \<mu>: "tight \<mu>" "strict_mono s"
shows "\r M. strict_mono (r :: nat \ nat) \ real_distribution M \ weak_conv_m (\ \ s \ r) M"
proof -
define f where "f k = cdf (\ (s k))" for k
interpret \<mu>: real_distribution "\<mu> k" for k
using \<mu> unfolding tight_def by auto
have rcont: "\x. continuous (at_right x) (f k)"
and mono: "mono (f k)"
and top: "(f k \ 1) at_top"
and bot: "(f k \ 0) at_bot" for k
unfolding f_def mono_def
using \<mu>.cdf_nondecreasing \<mu>.cdf_is_right_cont \<mu>.cdf_lim_at_top_prob \<mu>.cdf_lim_at_bot by auto
have bdd: "\f k x\ \ 1" for k x
by (auto simp add: abs_le_iff minus_le_iff f_def \<mu>.cdf_nonneg \<mu>.cdf_bounded_prob)
from Helly_selection[OF rcont mono bdd, of "\x. x"] obtain r F
where F: "strict_mono r" "\x. continuous (at_right x) F" "mono F" "\x. \F x\ \ 1"
and lim_F: "\x. continuous (at x) F \ (\n. f (r n) x) \ F x"
by blast
have "0 \ f n x" for n x
unfolding f_def by (rule \<mu>.cdf_nonneg)
have F_nonneg: "0 \ F x" for x
proof -
obtain y where "y < x" "isCont F y"
using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{..< x}"] by auto
then have "0 \ F y"
by (intro LIMSEQ_le_const[OF lim_F]) (auto simp: f_def \<mu>.cdf_nonneg)
also have "\ \ F x"
using \<open>y < x\<close> by (auto intro!: monoD[OF \<open>mono F\<close>])
finally show "0 \ F x" .
qed
have Fab: "\a b. (\x\b. F x \ 1 - \) \ (\x\a. F x \ \)" if \: "0 < \" for \
proof auto
obtain a' b' where a'b': "a' < b'" "\k. measure (\ k) {a'<..b'} > 1 - \"
using \<epsilon> \<mu> by (auto simp: tight_def)
obtain a where a: "a < a'" "isCont F a"
using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{..< a'}"] by auto
obtain b where b: "b' < b" "isCont F b"
using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{b' <..}"] by auto
have "a < b"
using a b a'b' by simp
let ?\<mu> = "\<lambda>k. measure (\<mu> (s (r k)))"
have ab: "?\ k {a<..b} > 1 - \" for k
proof -
have "?\ k {a'<..b'} \ ?\ k {a<..b}"
using a b by (intro \<mu>.finite_measure_mono) auto
then show ?thesis
using a'b'(2) by (metis less_eq_real_def less_trans)
qed
have "(\k. ?\ k {..b}) \ F b"
using b(2) lim_F unfolding f_def cdf_def o_def by auto
then have "1 - \ \ F b"
proof (rule tendsto_lowerbound, intro always_eventually allI)
fix k
have "1 - \ < ?\ k {a<..b}"
using ab by auto
also have "\ \ ?\ k {..b}"
by (auto intro!: \<mu>.finite_measure_mono)
finally show "1 - \ \ ?\ k {..b}"
by (rule less_imp_le)
qed (rule sequentially_bot)
then show "\b. \x\b. 1 - \ \ F x"
using F unfolding mono_def by (metis order.trans)
have "(\k. ?\ k {..a}) \ F a"
using a(2) lim_F unfolding f_def cdf_def o_def by auto
then have Fa: "F a \ \"
proof (rule tendsto_upperbound, intro always_eventually allI)
fix k
have "?\ k {..a} + ?\ k {a<..b} \ 1"
by (subst \<mu>.finite_measure_Union[symmetric]) auto
then show "?\ k {..a} \ \"
using ab[of k] by simp
qed (rule sequentially_bot)
then show "\a. \x\a. F x \ \"
using F unfolding mono_def by (metis order.trans)
qed
have "(F \ 1) at_top"
proof (rule order_tendstoI)
show "1 < y \ \\<^sub>F x in at_top. F x < y" for y
using \<open>\<And>x. \<bar>F x\<bar> \<le> 1\<close> \<open>\<And>x. 0 \<le> F x\<close> by (auto intro: le_less_trans always_eventually)
fix y :: real assume "y < 1"
then obtain z where "y < z" "z < 1"
using dense[of y 1] by auto
with Fab[of "1 - z"] show "\\<^sub>F x in at_top. y < F x"
by (auto simp: eventually_at_top_linorder intro: less_le_trans)
qed
moreover
have "(F \ 0) at_bot"
proof (rule order_tendstoI)
show "y < 0 \ \\<^sub>F x in at_bot. y < F x" for y
using \<open>\<And>x. 0 \<le> F x\<close> by (auto intro: less_le_trans always_eventually)
fix y :: real assume "0 < y"
then obtain z where "0 < z" "z < y"
using dense[of 0 y] by auto
with Fab[of z] show "\\<^sub>F x in at_bot. F x < y"
by (auto simp: eventually_at_bot_linorder intro: le_less_trans)
qed
ultimately have M: "real_distribution (interval_measure F)" "cdf (interval_measure F) = F"
using F by (auto intro!: real_distribution_interval_measure cdf_interval_measure simp: mono_def)
with lim_F LIMSEQ_subseq_LIMSEQ M have "weak_conv_m (\ \ s \ r) (interval_measure F)"
by (auto simp: weak_conv_def weak_conv_m_def f_def comp_def)
then show "\r M. strict_mono (r :: nat \ nat) \ (real_distribution M \ weak_conv_m (\ \ s \ r) M)"
using F M by auto
qed
corollary tight_subseq_weak_converge:
fixes \<mu> :: "nat \<Rightarrow> real measure" and M :: "real measure"
assumes "\n. real_distribution (\ n)" "real_distribution M" and tight: "tight \" and
subseq: "\s \. strict_mono s \ real_distribution \ \ weak_conv_m (\ \ s) \ \ weak_conv_m (\ \ s) M"
shows "weak_conv_m \ M"
proof (rule ccontr)
define f where "f n = cdf (\ n)" for n
define F where "F = cdf M"
assume "\ weak_conv_m \ M"
then obtain x where x: "isCont F x" "\ (\n. f n x) \ F x"
by (auto simp: weak_conv_m_def weak_conv_def f_def F_def)
then obtain \<epsilon> where "\<epsilon> > 0" and "infinite {n. \<not> dist (f n x) (F x) < \<epsilon>}"
by (auto simp: tendsto_iff not_eventually INFM_iff_infinite cofinite_eq_sequentially[symmetric])
then obtain s :: "nat \ nat" where s: "\n. \ dist (f (s n) x) (F x) < \" and "strict_mono s"
using enumerate_in_set enumerate_mono by (fastforce simp: strict_mono_def)
then obtain r \<nu> where r: "strict_mono r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>"
using tight_imp_convergent_subsubsequence[OF tight] by blast
then have "weak_conv_m (\ \ (s \ r)) M"
using \<open>strict_mono s\<close> r by (intro subseq strict_mono_o) (auto simp: comp_assoc)
then have "(\n. f (s (r n)) x) \ F x"
using x by (auto simp: weak_conv_m_def weak_conv_def F_def f_def)
then show False
using s \<open>\<epsilon> > 0\<close> by (auto dest: tendstoD)
qed
end
¤ Dauer der Verarbeitung: 0.17 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.
|
