1(* Title: HOL/Probability/Helly_Selection.thy 2 Authors: Jeremy Avigad (CMU), Luke Serafin (CMU) 3 Authors: Johannes H��lzl, TU M��nchen 4*) 5 6section \<open>Helly's selection theorem\<close> 7 8text \<open>The set of bounded, monotone, right continuous functions is sequentially compact\<close> 9 10theory Helly_Selection 11 imports "HOL-Library.Diagonal_Subsequence" Weak_Convergence 12begin 13 14lemma minus_one_less: "x - 1 < (x::real)" 15 by simp 16 17theorem Helly_selection: 18 fixes f :: "nat \<Rightarrow> real \<Rightarrow> real" 19 assumes rcont: "\<And>n x. continuous (at_right x) (f n)" 20 assumes mono: "\<And>n. mono (f n)" 21 assumes bdd: "\<And>n x. \<bar>f n x\<bar> \<le> M" 22 shows "\<exists>s. strict_mono (s::nat \<Rightarrow> nat) \<and> (\<exists>F. (\<forall>x. continuous (at_right x) F) \<and> mono F \<and> (\<forall>x. \<bar>F x\<bar> \<le> M) \<and> 23 (\<forall>x. continuous (at x) F \<longrightarrow> (\<lambda>n. f (s n) x) \<longlonglongrightarrow> F x))" 24proof - 25 obtain m :: "real \<Rightarrow> nat" where "bij_betw m \<rat> UNIV" 26 using countable_rat Rats_infinite by (erule countableE_infinite) 27 then obtain r :: "nat \<Rightarrow> real" where bij: "bij_betw r UNIV \<rat>" 28 using bij_betw_inv by blast 29 30 have dense_r: "\<And>x y. x < y \<Longrightarrow> \<exists>n. x < r n \<and> r n < y" 31 by (metis Rats_dense_in_real bij f_the_inv_into_f bij_betw_def) 32 33 let ?P = "\<lambda>n. \<lambda>s. convergent (\<lambda>k. f (s k) (r n))" 34 interpret nat: subseqs ?P 35 proof (unfold convergent_def, unfold subseqs_def, auto) 36 fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "strict_mono s" 37 have "bounded {-M..M}" 38 using bounded_closed_interval by auto 39 moreover have "\<And>k. f (s k) (r n) \<in> {-M..M}" 40 using bdd by (simp add: abs_le_iff minus_le_iff) 41 ultimately have "\<exists>l s'. strict_mono s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l" 42 using compact_Icc compact_imp_seq_compact seq_compactE by metis 43 thus "\<exists>s'. strict_mono (s'::nat\<Rightarrow>nat) \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)" 44 by (auto simp: comp_def) 45 qed 46 define d where "d = nat.diagseq" 47 have subseq: "strict_mono d" 48 unfolding d_def using nat.subseq_diagseq by auto 49 have rat_cnv: "?P n d" for n 50 proof - 51 have Pn_seqseq: "?P n (nat.seqseq (Suc n))" 52 by (rule nat.seqseq_holds) 53 have 1: "(\<lambda>k. f ((nat.seqseq (Suc n) \<circ> (\<lambda>k. nat.fold_reduce (Suc n) k 54 (Suc n + k))) k) (r n)) = (\<lambda>k. f (nat.seqseq (Suc n) k) (r n)) \<circ> 55 (\<lambda>k. nat.fold_reduce (Suc n) k (Suc n + k))" 56 by auto 57 have 2: "?P n (d \<circ> ((+) (Suc n)))" 58 unfolding d_def nat.diagseq_seqseq 1 59 by (intro convergent_subseq_convergent Pn_seqseq nat.subseq_diagonal_rest) 60 then obtain L where 3: "(\<lambda>na. f (d (na + Suc n)) (r n)) \<longlonglongrightarrow> L" 61 by (auto simp: add.commute dest: convergentD) 62 then have "(\<lambda>k. f (d k) (r n)) \<longlonglongrightarrow> L" 63 by (rule LIMSEQ_offset) 64 then show ?thesis 65 by (auto simp: convergent_def) 66 qed 67 let ?f = "\<lambda>n. \<lambda>k. f (d k) (r n)" 68 have lim_f: "?f n \<longlonglongrightarrow> lim (?f n)" for n 69 using rat_cnv convergent_LIMSEQ_iff by auto 70 have lim_bdd: "lim (?f n) \<in> {-M..M}" for n 71 proof - 72 have "closed {-M..M}" using closed_real_atLeastAtMost by auto 73 hence "(\<forall>i. ?f n i \<in> {-M..M}) \<and> ?f n \<longlonglongrightarrow> lim (?f n) \<longrightarrow> lim (?f n) \<in> {-M..M}" 74 unfolding closed_sequential_limits by (drule_tac x = "\<lambda>k. f (d k) (r n)" in spec) blast 75 moreover have "\<forall>i. ?f n i \<in> {-M..M}" 76 using bdd by (simp add: abs_le_iff minus_le_iff) 77 ultimately show "lim (?f n) \<in> {-M..M}" 78 using lim_f by auto 79 qed 80 then have limset_bdd: "\<And>x. {lim (?f n) |n. x < r n} \<subseteq> {-M..M}" 81 by auto 82 then have bdd_below: "bdd_below {lim (?f n) |n. x < r n}" for x 83 by (metis (mono_tags) bdd_below_Icc bdd_below_mono) 84 have r_unbdd: "\<exists>n. x < r n" for x 85 using dense_r[OF less_add_one, of x] by auto 86 then have nonempty: "{lim (?f n) |n. x < r n} \<noteq> {}" for x 87 by auto 88 89 define F where "F x = Inf {lim (?f n) |n. x < r n}" for x 90 have F_eq: "ereal (F x) = (INF n\<in>{n. x < r n}. ereal (lim (?f n)))" for x 91 unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image image_comp) 92 have mono_F: "mono F" 93 using nonempty by (auto intro!: cInf_superset_mono simp: F_def bdd_below mono_def) 94 moreover have "\<And>x. continuous (at_right x) F" 95 unfolding continuous_within order_tendsto_iff eventually_at_right[OF less_add_one] 96 proof safe 97 show "F x < u \<Longrightarrow> \<exists>b>x. \<forall>y>x. y < b \<longrightarrow> F y < u" for x u 98 unfolding F_def cInf_less_iff[OF nonempty bdd_below] by auto 99 next 100 show "\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> l < F y" if l: "l < F x" for x l 101 using less_le_trans[OF l mono_F[THEN monoD, of x]] by (auto intro: less_add_one) 102 qed 103 moreover 104 { fix x 105 have "F x \<in> {-M..M}" 106 unfolding F_def using limset_bdd bdd_below r_unbdd by (intro closed_subset_contains_Inf) auto 107 then have "\<bar>F x\<bar> \<le> M" by auto } 108 moreover have "(\<lambda>n. f (d n) x) \<longlonglongrightarrow> F x" if cts: "continuous (at x) F" for x 109 proof (rule limsup_le_liminf_real) 110 show "limsup (\<lambda>n. f (d n) x) \<le> F x" 111 proof (rule tendsto_lowerbound) 112 show "(F \<longlongrightarrow> ereal (F x)) (at_right x)" 113 using cts unfolding continuous_at_split by (auto simp: continuous_within) 114 show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>n. f (d n) x) \<le> F i" 115 unfolding eventually_at_right[OF less_add_one] 116 proof (rule, rule, rule less_add_one, safe) 117 fix y assume y: "x < y" 118 with dense_r obtain N where "x < r N" "r N < y" by auto 119 have *: "y < r n' \<Longrightarrow> lim (?f N) \<le> lim (?f n')" for n' 120 using \<open>r N < y\<close> by (intro LIMSEQ_le[OF lim_f lim_f]) (auto intro!: mono[THEN monoD]) 121 have "limsup (\<lambda>n. f (d n) x) \<le> limsup (?f N)" 122 using \<open>x < r N\<close> by (auto intro!: Limsup_mono always_eventually mono[THEN monoD]) 123 also have "\<dots> = lim (\<lambda>n. ereal (?f N n))" 124 using rat_cnv[of N] by (force intro!: convergent_limsup_cl simp: convergent_def) 125 also have "\<dots> \<le> F y" 126 by (auto intro!: INF_greatest * simp: convergent_real_imp_convergent_ereal rat_cnv F_eq) 127 finally show "limsup (\<lambda>n. f (d n) x) \<le> F y" . 128 qed 129 qed simp 130 show "F x \<le> liminf (\<lambda>n. f (d n) x)" 131 proof (rule tendsto_upperbound) 132 show "(F \<longlongrightarrow> ereal (F x)) (at_left x)" 133 using cts unfolding continuous_at_split by (auto simp: continuous_within) 134 show "\<forall>\<^sub>F i in at_left x. F i \<le> liminf (\<lambda>n. f (d n) x)" 135 unfolding eventually_at_left[OF minus_one_less] 136 proof (rule, rule, rule minus_one_less, safe) 137 fix y assume y: "y < x" 138 with dense_r obtain N where "y < r N" "r N < x" by auto 139 have "F y \<le> liminf (?f N)" 140 using \<open>y < r N\<close> by (auto simp: F_eq convergent_real_imp_convergent_ereal 141 rat_cnv convergent_liminf_cl intro!: INF_lower2) 142 also have "\<dots> \<le> liminf (\<lambda>n. f (d n) x)" 143 using \<open>r N < x\<close> by (auto intro!: Liminf_mono monoD[OF mono] always_eventually) 144 finally show "F y \<le> liminf (\<lambda>n. f (d n) x)" . 145 qed 146 qed simp 147 qed 148 ultimately show ?thesis using subseq by auto 149qed 150 151(** Weak convergence corollaries to Helly's theorem. **) 152 153definition 154 tight :: "(nat \<Rightarrow> real measure) \<Rightarrow> bool" 155where 156 "tight \<mu> \<equiv> (\<forall>n. real_distribution (\<mu> n)) \<and> (\<forall>(\<epsilon>::real)>0. \<exists>a b::real. a < b \<and> (\<forall>n. measure (\<mu> n) {a<..b} > 1 - \<epsilon>))" 157 158(* Can strengthen to equivalence. *) 159theorem tight_imp_convergent_subsubsequence: 160 assumes \<mu>: "tight \<mu>" "strict_mono s" 161 shows "\<exists>r M. strict_mono (r :: nat \<Rightarrow> nat) \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M" 162proof - 163 define f where "f k = cdf (\<mu> (s k))" for k 164 interpret \<mu>: real_distribution "\<mu> k" for k 165 using \<mu> unfolding tight_def by auto 166 167 have rcont: "\<And>x. continuous (at_right x) (f k)" 168 and mono: "mono (f k)" 169 and top: "(f k \<longlongrightarrow> 1) at_top" 170 and bot: "(f k \<longlongrightarrow> 0) at_bot" for k 171 unfolding f_def mono_def 172 using \<mu>.cdf_nondecreasing \<mu>.cdf_is_right_cont \<mu>.cdf_lim_at_top_prob \<mu>.cdf_lim_at_bot by auto 173 have bdd: "\<bar>f k x\<bar> \<le> 1" for k x 174 by (auto simp add: abs_le_iff minus_le_iff f_def \<mu>.cdf_nonneg \<mu>.cdf_bounded_prob) 175 176 from Helly_selection[OF rcont mono bdd, of "\<lambda>x. x"] obtain r F 177 where F: "strict_mono r" "\<And>x. continuous (at_right x) F" "mono F" "\<And>x. \<bar>F x\<bar> \<le> 1" 178 and lim_F: "\<And>x. continuous (at x) F \<Longrightarrow> (\<lambda>n. f (r n) x) \<longlonglongrightarrow> F x" 179 by blast 180 181 have "0 \<le> f n x" for n x 182 unfolding f_def by (rule \<mu>.cdf_nonneg) 183 have F_nonneg: "0 \<le> F x" for x 184 proof - 185 obtain y where "y < x" "isCont F y" 186 using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{..< x}"] by auto 187 then have "0 \<le> F y" 188 by (intro LIMSEQ_le_const[OF lim_F]) (auto simp: f_def \<mu>.cdf_nonneg) 189 also have "\<dots> \<le> F x" 190 using \<open>y < x\<close> by (auto intro!: monoD[OF \<open>mono F\<close>]) 191 finally show "0 \<le> F x" . 192 qed 193 194 have Fab: "\<exists>a b. (\<forall>x\<ge>b. F x \<ge> 1 - \<epsilon>) \<and> (\<forall>x\<le>a. F x \<le> \<epsilon>)" if \<epsilon>: "0 < \<epsilon>" for \<epsilon> 195 proof auto 196 obtain a' b' where a'b': "a' < b'" "\<And>k. measure (\<mu> k) {a'<..b'} > 1 - \<epsilon>" 197 using \<epsilon> \<mu> by (auto simp: tight_def) 198 obtain a where a: "a < a'" "isCont F a" 199 using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{..< a'}"] by auto 200 obtain b where b: "b' < b" "isCont F b" 201 using open_minus_countable[OF mono_ctble_discont[OF \<open>mono F\<close>], of "{b' <..}"] by auto 202 have "a < b" 203 using a b a'b' by simp 204 205 let ?\<mu> = "\<lambda>k. measure (\<mu> (s (r k)))" 206 have ab: "?\<mu> k {a<..b} > 1 - \<epsilon>" for k 207 proof - 208 have "?\<mu> k {a'<..b'} \<le> ?\<mu> k {a<..b}" 209 using a b by (intro \<mu>.finite_measure_mono) auto 210 then show ?thesis 211 using a'b'(2) by (metis less_eq_real_def less_trans) 212 qed 213 214 have "(\<lambda>k. ?\<mu> k {..b}) \<longlonglongrightarrow> F b" 215 using b(2) lim_F unfolding f_def cdf_def o_def by auto 216 then have "1 - \<epsilon> \<le> F b" 217 proof (rule tendsto_lowerbound, intro always_eventually allI) 218 fix k 219 have "1 - \<epsilon> < ?\<mu> k {a<..b}" 220 using ab by auto 221 also have "\<dots> \<le> ?\<mu> k {..b}" 222 by (auto intro!: \<mu>.finite_measure_mono) 223 finally show "1 - \<epsilon> \<le> ?\<mu> k {..b}" 224 by (rule less_imp_le) 225 qed (rule sequentially_bot) 226 then show "\<exists>b. \<forall>x\<ge>b. 1 - \<epsilon> \<le> F x" 227 using F unfolding mono_def by (metis order.trans) 228 229 have "(\<lambda>k. ?\<mu> k {..a}) \<longlonglongrightarrow> F a" 230 using a(2) lim_F unfolding f_def cdf_def o_def by auto 231 then have Fa: "F a \<le> \<epsilon>" 232 proof (rule tendsto_upperbound, intro always_eventually allI) 233 fix k 234 have "?\<mu> k {..a} + ?\<mu> k {a<..b} \<le> 1" 235 by (subst \<mu>.finite_measure_Union[symmetric]) auto 236 then show "?\<mu> k {..a} \<le> \<epsilon>" 237 using ab[of k] by simp 238 qed (rule sequentially_bot) 239 then show "\<exists>a. \<forall>x\<le>a. F x \<le> \<epsilon>" 240 using F unfolding mono_def by (metis order.trans) 241 qed 242 243 have "(F \<longlongrightarrow> 1) at_top" 244 proof (rule order_tendstoI) 245 show "1 < y \<Longrightarrow> \<forall>\<^sub>F x in at_top. F x < y" for y 246 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) 247 fix y :: real assume "y < 1" 248 then obtain z where "y < z" "z < 1" 249 using dense[of y 1] by auto 250 with Fab[of "1 - z"] show "\<forall>\<^sub>F x in at_top. y < F x" 251 by (auto simp: eventually_at_top_linorder intro: less_le_trans) 252 qed 253 moreover 254 have "(F \<longlongrightarrow> 0) at_bot" 255 proof (rule order_tendstoI) 256 show "y < 0 \<Longrightarrow> \<forall>\<^sub>F x in at_bot. y < F x" for y 257 using \<open>\<And>x. 0 \<le> F x\<close> by (auto intro: less_le_trans always_eventually) 258 fix y :: real assume "0 < y" 259 then obtain z where "0 < z" "z < y" 260 using dense[of 0 y] by auto 261 with Fab[of z] show "\<forall>\<^sub>F x in at_bot. F x < y" 262 by (auto simp: eventually_at_bot_linorder intro: le_less_trans) 263 qed 264 ultimately have M: "real_distribution (interval_measure F)" "cdf (interval_measure F) = F" 265 using F by (auto intro!: real_distribution_interval_measure cdf_interval_measure simp: mono_def) 266 with lim_F LIMSEQ_subseq_LIMSEQ M have "weak_conv_m (\<mu> \<circ> s \<circ> r) (interval_measure F)" 267 by (auto simp: weak_conv_def weak_conv_m_def f_def comp_def) 268 then show "\<exists>r M. strict_mono (r :: nat \<Rightarrow> nat) \<and> (real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M)" 269 using F M by auto 270qed 271 272corollary tight_subseq_weak_converge: 273 fixes \<mu> :: "nat \<Rightarrow> real measure" and M :: "real measure" 274 assumes "\<And>n. real_distribution (\<mu> n)" "real_distribution M" and tight: "tight \<mu>" and 275 subseq: "\<And>s \<nu>. strict_mono s \<Longrightarrow> real_distribution \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) M" 276 shows "weak_conv_m \<mu> M" 277proof (rule ccontr) 278 define f where "f n = cdf (\<mu> n)" for n 279 define F where "F = cdf M" 280 281 assume "\<not> weak_conv_m \<mu> M" 282 then obtain x where x: "isCont F x" "\<not> (\<lambda>n. f n x) \<longlonglongrightarrow> F x" 283 by (auto simp: weak_conv_m_def weak_conv_def f_def F_def) 284 then obtain \<epsilon> where "\<epsilon> > 0" and "infinite {n. \<not> dist (f n x) (F x) < \<epsilon>}" 285 by (auto simp: tendsto_iff not_eventually INFM_iff_infinite cofinite_eq_sequentially[symmetric]) 286 then obtain s :: "nat \<Rightarrow> nat" where s: "\<And>n. \<not> dist (f (s n) x) (F x) < \<epsilon>" and "strict_mono s" 287 using enumerate_in_set enumerate_mono by (fastforce simp: strict_mono_def) 288 then obtain r \<nu> where r: "strict_mono r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>" 289 using tight_imp_convergent_subsubsequence[OF tight] by blast 290 then have "weak_conv_m (\<mu> \<circ> (s \<circ> r)) M" 291 using \<open>strict_mono s\<close> r by (intro subseq strict_mono_o) (auto simp: comp_assoc) 292 then have "(\<lambda>n. f (s (r n)) x) \<longlonglongrightarrow> F x" 293 using x by (auto simp: weak_conv_m_def weak_conv_def F_def f_def) 294 then show False 295 using s \<open>\<epsilon> > 0\<close> by (auto dest: tendstoD) 296qed 297 298end 299