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