Quelle Helly_Selection.thy Sprache: Isabelle

(*  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

quality99%

¤ Dauer der Verarbeitung: 0.16 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.