#import "../conf.typ": *

= Теорема Больцано-Вейерштрасса и критерий Коши сходимости числовой последовательности
== Теорема Больцано-Вейерштрасса

#definition[
  Пусть имеется правило, которое каждому натуральному числу $n$ ставит в
  соответствие некоторое $x_n$ из множества $G$. Тогда *последовательностью*
  называется множество всевозможных упорядоченных пар $(n, x_n), n in NN$.
]

#definition[
  Последовательность $seq(x)$ называется *ограниченной сверху (снизу)*, если
  #eq[
    $exists M (m): x_n <= M$ ($x_n >= M$) $forall n in NN$.
  ]
]

#definition[
  Последовательность $seq(x)$ называется *ограниченной*, если она ограничена и
  сверху, и снизу.
]

#definition[
  Последовательность называется *строго возрастающей (убывающей)*, если
  #eq[
    $forall n in NN : x_n < x_(n + 1)$ ($x_n > x_(n + 1)$).
  ]
]

#definition[
  Последовательность $seq(idx: k, y)$ называется *подпоследовательностью*
  последовательности $seq(x)$, если
  #eq[
    $forall k in NN : exists n = n_k : y_k = x_n_k$,
  ]
  где последовательность $seq(idx: k, n)$ - строго возрастающая. Эта последовательность
  обозначается $seq(idx: k, x_n)$.
]

#definition[
  Последовательность отрезков ${[a_n, b_n]}_(n = 1)^oo$ называется
  *последовательностью вложенных отрезков*, если
  #eq[
    $forall n in NN : [a_n, b_n] supset [a_(n + 1), b_(n + 1)]$.
  ]
]

#theorem(
  "Принцип Кантора вложенных отрезков",
)[
  Всякая последовательность вложенных отрезков ${[a_n, b_n]}_(n = 1)^oo$ имеет
  непустое пересечение, то есть
  #eq[
    $sect.big_(n = 1)^oo [a_n, b_n] != emptyset$
  ]
]

#definition[
  Число $x_0$ называется *пределом последовательности* $seq(x)$, если
  #eq[
    $forall epsilon > 0 : exists N_epsilon in NN : forall n >= N_epsilon : |x_n - x_0| < epsilon$.
  ]
]

#theorem("Больцано-Вейерштрасса")[
  Из каждой ограниченной последовательности можно выделить сходящуюся
  подпоследовательность.
]

#proof[
  Пусть $seq(x)$ -- рассматриваемая ограниченная последовательность, то есть
  #eq[
    $exists a_1, b_1 in RR: forall n in NN : space a_1 <= x_n <= b_1$
  ]
  Заметим, что один из отрезков $[a_1, (a_1 + b_1) / 2], [(a_1 + b_1) / 2, b_1]$ содержит
  бесконечно много элементов последовательности.

  Пусть $[a_2, b_2]$ -- тот из отрезков, который содержит бесконечно много
  элементов.

  Продолжая данный трюк счётное количество раз, получим последовательность
  вложенных отрезков ${[a_n, b_n]}_(n = 1)^oo$. Также заметим, что данные отрезки
  стягиваются:
  #eq[
    $0 < b_n - a_n = (b_1 - a_1) / 2^n$
  ]

  Тогда по принципу Кантора:
  #eq[
    $sect.big_(n = 1)^oo [a_n, b_n] = {c}$
  ]
  Осталось построить подпоследовательность, будем брать $x_n_k in [a_k, b_k]$,
  причём так, чтобы $n_k > n_(k - 1)$. Очевидно, $n_1 = 1$. Существование предела
  также очевидно:
  #eq[
    $0 <= abs(c - x_n_k) <= b_k - a_k = (b_1 - a_1) / 2^k ->_(k -> oo) 0$
  ]
]

== <NAME>
#definition[
  Последовательность $seq(x)$ называется *фундаментальной*, если
  #eq[
    $forall epsilon > 0 : exists N in NN : forall n > N : forall p in NN : space abs(x_(n + p) - x_n) < epsilon$
  ]
]

#theorem("Критерий Коши сходимости числовой последовательности")[
  Числовая последовательность сходится $<=>$ она фундаментальна.
]

#proof[
  $=>$ По определению предела:
  #eq[
    $exists l in RR : forall epsilon > 0 : exists N in NN : forall n > N : space abs(x_n - l) < epsilon / 2$
  ]
  Тогда по неравенству треугольника в условиях предела:
  #eq[
    $abs(x_(n + p) - x_n) = abs(x_(n + p) - l + l - x_n) <= abs(x_(n + p) - l) + abs(x_n - l) < epsilon$
  ]

  $arrow.l.double$ Вначале докажем, что из фундаментальности следует
  ограниченность:
  #eq[
    $epsilon := 1 : exists N in NN : forall n > N : forall p in NN : space abs(x_(n + p) - x_n) < 1$
  ]
  Тогда заметим, что
  #eq[
    $forall n in NN : min(x_1, ..., x_N, x_(N + 1) + 1) <= x_n <= max(x_1, ..., x_N, x_(N + 1) + 1)$
  ]
  Тогда из ограниченной последовательности $seq(x)$ по теореме
  Больцано-Вейерштрасса достанем сходящуюся подпоследовательность:
  #eq[
    $exists seq(idx: k, x_n) : exists l : forall epsilon > 0 : exists K(epsilon) in NN : forall k > K(epsilon) : space abs(x_n_k - l) < epsilon / 2$
  ]
  Также по определению фундаментальности:
  #eq[
    $forall epsilon > 0 : exists N(epsilon) in NN : forall n > N(epsilon) : forall p in NN : space abs(x_(n + p) - x_n) < epsilon$
  ]
  Объединим эти два условия и получим требуемое:
  #eq[
    $forall epsilon > 0 : exists N_0 = max(N(epsilon), n_(K(epsilon) + 1)) : forall n &> N_0 : \
    abs(x_n - l) = abs(x_n - x_n_(K(epsilon) + 1) + x_n_(K(epsilon) + 1) - l)        &<= abs(x_n - x_n_(K(epsilon) + 1)) + abs(x_n_(K(epsilon) + 1) - l) < epsilon$
  ]
]
