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

= Теорема о промежуточных значениях непрерывной функции

#theorem(
  "Больцано-Коши о промежуточных значениях",
)[
  Пусть $f$ непрерывна на $[a, b]$. Тогда
  #eq[
    $forall x_1, x_2 in [a, b] : c := f(x_1) < d := f(x_2) : space forall e in (c, d) : exists gamma in [a, b] : f(gamma) = e$
  ]
]

#proof[
  Рассмотрим частный случай $c < e = 0 < d$.

  Построим последовательность отрезков ${[a_n, b_n]}_(n = 1)^oo$, где $[a_1, b_1] = {x_1, x_2}$ (мы
  не знаем в каком порядке идут иксы).

  Заметим, что $f(a_1) dot f(b_1) < 0$.

  Рассмотрим $f((a_1 + b_1) / 2)$. Какие могут быть случаи?
  - Если $f((a_1 + b_1) / 2) = 0$, то мы победили и останавливаемся.
  - Если $f((a_1 + b_1) / 2) > 0$, то $a_2 := a_1, b_2 := (a_1 + b_1) / 2$.
  - Если $f((a_1 + b_1) / 2) < 0$, то $a_2 := (a_1 + b_1) / 2, b_2 := b_1$.
  Либо после конечного числа шагов мы найдём требуемую точку, либо построим
  последовательность стягивающихся отрезков:

  #eq[
    $\
    b_n - a_n = abs(x_2 - x_1) / 2^(n - 1) \ $
  ]
  Тогда по принципу Кантора ${gamma} = sect.big_(n = 1)^oo [a_n, b_n]$, причём
  #eq[
    $lim_(n -> oo)a_n = lim_(n -> oo) b_n = gamma in [a, b]$
  ]
  Тогда в силу непрерывности $f$:
  #eq[
    $f(gamma) = lim_(n -> oo) f(a_n) = lim_(n -> oo) f(b_n)$
  ]
  Заметим, что после каждой итерации алгоритма изначальное свойство сохраняется:
  #eq[
    $f(a_n) dot f(b_n) < 0$
  ]
  Совершив предельный переход в неравенстве, получим
  #eq[
    $f^2(gamma) <= 0$
  ]
  Из чего следует $f(gamma) = 0$.

  В общем случае рассматривается вспомогательная функция $F(x) = f(x) - e$.
]
