(* Title: HOL/Probability/Helly_Selection.thy Authors: Jeremy Avigad (CMU), Luke Serafin (CMU) Authors: Johannes Hölzl, TU München *) section ‹Helly's selection theorem› text ‹The set of bounded, monotone, right continuous functions is sequentially compact› 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) ∧ (∀x. continuous (at x) F ⟶ (λn. f (s n) x) ⇢ 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)) = (λk. f (nat.seqseq (Suc n) k) (r n)) ∘ (λk. nat.fold_reduce (Suc n) k (Suc n + k))" by auto have 2: "?P n (d ∘ (op + (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) 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 "∀⇩_{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 ‹r N < y› 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 ‹x < r N› 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 "∀⇩_{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 ‹y < r N› 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 ‹r N < x› 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 μ: "tight μ" "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 μ: real_distribution "μ k" for k using μ 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 μ.cdf_nondecreasing μ.cdf_is_right_cont μ.cdf_lim_at_top_prob μ.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 μ.cdf_nonneg μ.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 μ.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 ‹mono F›], of "{..< x}"] by auto then have "0 ≤ F y" by (intro LIMSEQ_le_const[OF lim_F]) (auto simp: f_def μ.cdf_nonneg) also have "… ≤ F x" using ‹y < x› by (auto intro!: monoD[OF ‹mono F›]) 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 ε μ by (auto simp: tight_def) obtain a where a: "a < a'" "isCont F a" using open_minus_countable[OF mono_ctble_discont[OF ‹mono F›], of "{..< a'}"] by auto obtain b where b: "b' < b" "isCont F b" using open_minus_countable[OF mono_ctble_discont[OF ‹mono F›], of "{b' <..}"] by auto have "a < b" using a b a'b' by simp let ?μ = "λk. measure (μ (s (r k)))" have ab: "?μ k {a<..b} > 1 - ε" for k proof - have "?μ k {a'<..b'} ≤ ?μ k {a<..b}" using a b by (intro μ.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!: μ.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 μ.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 ⟹ ∀⇩_{F}x in at_top. F x < y" for y using ‹⋀x. ¦F x¦ ≤ 1› ‹⋀x. 0 ≤ F x› 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 "∀⇩_{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 ⟹ ∀⇩_{F}x in at_bot. y < F x" for y using ‹⋀x. 0 ≤ F x› 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 "∀⇩_{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 μ :: "nat ⇒ 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 ε where "ε > 0" and "infinite {n. ¬ dist (f n x) (F x) < ε}" 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 ν where r: "strict_mono r" "real_distribution ν" "weak_conv_m (μ ∘ s ∘ r) ν" using tight_imp_convergent_subsubsequence[OF tight] by blast then have "weak_conv_m (μ ∘ (s ∘ r)) M" using ‹strict_mono s› 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 ‹ε > 0› by (auto dest: tendstoD) qed end