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