Глава 3. Непрерывность

От топологии к непрерывности

Что построили предыдущие главы

Часть V строит анализ процессов слой за слоем. Глава 5.1 дала расстояние: метрику на рациональных числах, открытые шары, расстояние как процесс. Глава 5.2 дала топологию: открытые и замкнутые множества, отделимость, компактность, равномерные покрытия. Накоплено всё, что нужно для следующего шага, — и шаг этот называется непрерывность.

Непрерывная функция — это функция, уважающая близость. Если два аргумента близки, близки и значения; малое возмущение входа даёт малое возмущение выхода. Метрика дала смысл слову <<близки>>; топология дала окрестности; теперь можно спросить, какие функции переводят близкое в близкое.

И — сразу же — две главные теоремы, которые непрерывность делает возможными. Теорема о промежуточном значении: непрерывная функция, меняющая знак, где-то обращается в нуль. Теорема об экстремуме: непрерывная функция на отрезке достигает максимума. Это две опоры классического анализа, и обе — предмет настоящей главы.

Два лица непрерывности

С непрерывностью над $Q$ нужно с самого начала условиться о различии, без которого вся глава звучала бы неточно. Непрерывность бывает двух видов, и над рациональными числами они не совпадают.

Поточечная непрерывность смотрит на каждую точку по отдельности. Функция $f$ непрерывна в точке $x$ , если для всякой требуемой точности $ε$ найдётся своя окрестность $δ$ , в которой значения не отходят от $f (x)$ дальше $ε$ . Размер $δ$ может зависеть от точки $x$ : в одних местах функция может быть полога, в других крута.

Равномерная непрерывность требует большего. Она требует, чтобы $δ$ можно было выбрать одну на весь отрезок — общую для всех точек сразу. Не <<у каждой точки своя окрестность>>, а <<есть единый масштаб, на котором функция всюду ведёт себя смирно>>.

{ Над действительными числами есть классическая теорема — теорема Кантора–Гейне, — которая говорит: на отрезке (на компакте) эти два вида непрерывности совпадают. Поточечно непрерывная функция на $[a, b]$ автоматически равномерно непрерывна. Над $Q$ это не так. И причина та же, что рушила Гейне–Бореля в § 2.5, — неполнота $Q$ . Рациональный отрезок дыряв, и поточечной непрерывности не хватает, чтобы стянуть все локальные $δ$ в одну глобальную. }

Из этого следует ключевой факт о строении главы. Обе главные теоремы — о промежуточном значении и об экстремуме — формализованы с гипотезой равномерной непрерывности, не поточечной. Не потому, что формализация слаба, а потому, что над $Q$ равномерность — это именно то, что нужно, и его приходится требовать явно, раз Кантора–Гейне не действует.

О статусе аксиом: техническое и онтологическое

Как и в Главе 5.2, условимся о словах заранее — иначе теоремы этой главы прозвучат тревожнее, чем следует.

Доказательства теоремы о промежуточном значении и теоремы об экстремуме используют аксиому classic — объект из файла ToS_Axioms.v. Но classic — не чужеродный костыль и не уступка нестрогости. Это техническая Rocq-аксиома, реализующая онтологический закон логики ToS: закон исключённого третьего, $L 3$ , в той форме, в какой его принимает Rocq.

Различие принципиально. В чисто конструктивной математике появление classic было бы признанием слабости. В ToS это не так: $L 3$ — закон логики ToS, принятый на уровне самой системы (Часть I). Когда доказательство <<использует classic>>, оно не отступает от строгости — оно явно учитывает, что опирается на закон логики ToS. Поэтому всякий раз, когда глава отмечает обращение к $L 3$ , это честный учёт уровня, а не сигнал тревоги. Далее по главе — сквозная отсылка <<по уговору § 3.1>>.

Замысел главы

Глава идёт от понятия к теоремам. Сначала — непрерывность как таковая: её топологическое лицо (§ 3.2) и центральный для главы разговор о равномерной непрерывности и границе $Q$ (§ 3.3). Затем — первая большая теорема: о промежуточном значении, через бисекцию (§ 3.4), и на трёх уровнях типизации (§ 3.5). Затем — вторая: об экстремуме, через измельчение сетки (§ 3.6), в двух версиях формализации (§ 3.7). И наконец — равномерный предел непрерывных функций и итог главы (§ 3.8).

Опорных файлов девять, все сверены с репозиторием дословно. Топологический слой непрерывности — без аксиом; теоремы о промежуточном значении и об экстремуме — с явно учтённым $L 3$ .

Непрерывность: топологическое лицо

Определение через $δ$ {delta}- $ε$ {epsilon}

Начнём с простейшего лица непрерывности — поточечного. Непрерывность функции в точке ToS определяет так: функция $f$ непрерывна в точке $x$ , если всякую требуемую точность значения можно обеспечить достаточной точностью аргумента. Формально — для любого $ε$ найдётся радиус $δ$ такой, что всякий аргумент $y$ ближе $δ$ к $x$ даёт значение $f (y)$ ближе $ε$ к $f (x)$ . Функция непрерывна, если непрерывна в каждой точке. Это классическое $δ$ - $ε$ определение, перенесённое на рациональный уровень: аргумент, точка, радиусы — рациональные. В Rocq оно записано в файле Topology.v, с которым глава познакомилась ещё в § 2.2:

Definition continuous_at (f : Q -> Q) (x : Q) : Prop :=
  forall eps, eps > 0 -> exists delta, delta > 0 /\
    forall y, Qabs (y - x) < delta -> Qabs (f y - f x) < eps.
 
Definition continuous (f : Q -> Q) : Prop :=
  forall x, continuous_at f x.

Для работы с приращением удобна вторая, родственная форма того же понятия — непрерывность на интервале. Она спрашивает о поведении $f$ на отрезке $[a, b]$ и измеряет изменение через приращение $h$ : малое $h$ даёт малое изменение $f (x + h) - f (x)$ . В репозитории эта форма записана в UniformConvergence.v:

Definition continuous_on (f : Q -> Q) (a b : Q) : Prop :=
  forall x : Q, a <= x -> x <= b ->
    forall eps : Q, 0 < eps ->
      exists delta : Q, 0 < delta /\
        forall h : Q, Qabs h < delta ->
          a <= x + h -> x + h <= b ->
          Qabs (f (x + h) - f x) < eps.

continuous_on f a b — та же поточечная непрерывность, ограниченная отрезком и записанная через приращение. Это — главная интервальная форма определения непрерывности среди опорных файлов главы; именно она удобна для теорем о равномерных пределах, к которым глава придёт в § 3.8.

Алгебра непрерывных функций

Непрерывность — свойство устойчивое: оно переживает основные операции над функциями, и потому из немногих простейших непрерывных функций можно построить богатый класс. Проследим это построение; каждый его шаг подтверждён доказанной леммой Topology.v.

{ Простейшие функции непрерывны. Тождество $x \mapsto x$ непрерывно — малое изменение аргумента есть в точности малое изменение значения (лемма identity_continuous). Постоянная функция непрерывна тривиально — значение не меняется вовсе (constant_continuous). Сдвиг $x \mapsto x + c$ непрерывен (add_const_continuous). Это отправные кирпичи. }

{ Операции сохраняют непрерывность. Сумма двух непрерывных в точке функций непрерывна в этой точке (continuous_at_sum); отрицание непрерывной непрерывно (continuous_at_neg); композиция непрерывных непрерывна (continuous_at_comp). Каждая из этих лемм Topology.v замыкает класс непрерывных функций относительно ещё одной операции. }

Сложив отправные кирпичи с этими операциями, получаем сразу многое: сложением, отрицанием, сдвигом и композицией из тождества и постоянных строится богатый класс непрерывных функций. Полное утверждение — что непрерывны все многочлены — требует ещё одного звена: леммы о сохранении непрерывности при умножении. Среди лемм Topology.v, на которые глава здесь опирается (continuous_at_sum, continuous_at_neg, continuous_at_comp и отправные identity_ continuous, constant_continuous), такого звена нет; замыкание относительно умножения — стандартное расширение алгебры непрерывных функций, и глава оставляет его именно расширением, не приписывая Topology.v большего, чем там доказано. Важно другое: фундамент — устойчивый, замкнутый относительно основных операций класс непрерывных функций — заложен, и на него можно опираться.

Прообраз открытого открыт

У непрерывности есть и второе лицо — чисто топологическое, без $δ$ и $ε$ , на одних открытых множествах. И его ToS не постулирует отдельно, а выводит из $δ$ - $ε$ определения — показывая, что два описания непрерывности суть одно.

Рассуждение таково. Пусть $f$ непрерывна и $S$ — открытое множество. Возьмём точку $x$ , чей образ $f (x)$ лежит в $S$ . Раз $S$ открыто, вокруг $f (x)$ есть запас свободного пространства — шар радиуса $ε$ , целиком лежащий в $S$ . Раз $f$ непрерывна в $x$ , этому $ε$ отвечает $δ$ : всякий аргумент ближе $δ$ к $x$ даёт значение ближе $ε$ к $f (x)$ , — то есть значение, всё ещё попадающее в $S$ . Значит, весь $δ$ -шар вокруг $x$ переходит под $f$ в $S$ : у точки $x$ есть запас свободного пространства в прообразе. А это и значит, что прообраз $S$ открыт. Так из $δ$ - $ε$ непрерывности выводится топологическая:

Theorem continuous_preserves_open_preimage : forall f S,
  continuous f -> is_open S ->
  is_open (fun x => S (f x)).

Это утверждение — доказанная в Topology.v теорема, подтверждающая проведённый вывод: прообраз открытого множества под непрерывной функцией открыт. В классической топологии им часто определяют непрерывность: непрерывная функция — та, что не разрывает открытость при взятии прообраза. ToS получает это определение не как постулат, а как следствие $δ$ - $ε$ определения — два лица непрерывности оказываются согласованы.

Здесь видна и прямая связь с Главой 5.2. Открытое множество, бывшее там центральным понятием топологии, становится теперь пробным камнем непрерывности: непрерывная функция — ровно та, что уважает топологическую структуру, построенную предыдущей главой.

И заметим, на чём всё это стоит. Топологическое лицо непрерывности — $δ$ - $ε$ определение, алгебра непрерывных функций, вывод теоремы о прообразе — получено конструктивно, без обращения к законам логики; Topology.v, как отмечалось ещё в § 2.2, не использует ни одной аксиомы. Аксиомы понадобятся дальше — когда глава перейдёт к двум большим теоремам анализа.

Разбор E/R/R: непрерывность как система

Непрерывность — система, и к ней приложима методология E/R/R (Часть I). Разбор разворачивает разметку, уже стоящую в заголовке опорного файла, где непрерывность названа прямо: правило — непрерывность есть конституция: прообраз открытого открыт.¹ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе — та же, что в Главах 5.1–5.2: непрерывность здесь — свойство функций $Q \to Q$ , не отображений фактор-классов; <<система>> — содержательная онтологическая интерпретация, не объект System $L$ .

Rules — правила (закон $L 5$ ). Сама непрерывность есть конституция — в двух равносильных формах: локальной ( $δ$ - $ε$ ) и топологической (<<прообраз открытого открыт>>); § 3.2.3 показал, что это одно правило, записанное дважды. К нему примыкает конкретный слой — замыкание класса непрерывных функций относительно суммы, отрицания, сдвига и композиции (§ 3.2.2); всё это конструктивно, без аксиом. Но над $Q$ у правил непрерывности есть вынужденное усиление: поточечной формы недостаточно для теорем анализа, ибо Кантора–Гейне над $Q$ неверна (§ 3.3.2). Поэтому в правила входит требование равномерности, а конструктивным мостом к ней служит липшицевость (§ 3.3.3). Это — Rule-уровневое следствие неполноты $Q$ , объясняющее, почему обе большие теоремы несут равномерную непрерывность в гипотезе. Наконец, у каждой теоремы — своё правило-конструкция: бисекция (знак в середине $\to$ выбор половины) и измельчение сетки.

Roles — значимость позиций (закон $L 4$ ). Функция играет роль отображения — перевода входа в выход; непрерывность наделяет её одной из качественных позиций: непрерывна в точке, равномерно непрерывна, липшицева — режимы, в которых функция уважает близость с разной силой. В двух больших теоремах роль иная: искомый объект — корень или максимизатор — играет роль Cauchy-процесса в $[a, b]$ , сходящегося к перемене знака или к супремуму.² Здесь же — тонкое ролевое различение § 3.6.3: у максимума роль значения (процесс супремума, Коши) первична, а роль позиции (argmax) производна и хрупка.

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — сами функции $Q \to Q$ и точки $Q$ , на которых они определены. В процессах двух теорем носители конечны на каждом шаге: середины вложенных отрезков (бисекция) и узлы сетки (экстремум) — всякий кадр обозрим, в духе $P 4$ ; завершённый <<корень>> или <<точка максимума>> могут быть иррациональны и как готовый элемент не существуют — актуальны лишь конечные приближения.

Сведём разбор в таблицу.

Компонент	Что фиксирует	E/R/R
функции $Q \to Q$ , точки	носители	Element
отображение; режимы: непрерывна / равномерно / липшицева	роли-позиции	Role
непрерывность ( $δ$ - $ε$ $\equiv$ прообраз открытого открыт)	конституция	Rule (конструкт.)
замыкание по сумме, композиции, сдвигу	алгебра	Rule (конструкт.)
равномерность как требование (Кантор–Гейне над $Q$ неверна)	усиление правила	Rule (неполнота, $L 3$ )
бисекция, измельчение сетки	конструкции теорем	Rule
законы $L 1$ – $L 5$	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: функции суть элементы, режимы непрерывности — роли, критерий непрерывности — правило. Самореференции нет: критерий квантифицирует по аргументам и стоит над значениями функции — по $L 5$ операция выше операндов. Непрерывность хорошо сформирована.

Разбор проясняет две тонкости, к которым глава придёт дальше. Три уровня теоремы о промежуточном значении (§ 3.5) — это, по $P 3$ , три интенсионально различных представления одного корня: три ответа на вопрос <<что есть корень>>, согласованных по содержанию, но разных по типу. А argmax теоремы об экстремуме (§ 3.7) — это $L 5$ -выделенная роль-позиция: порядок $L 5$ делает выбор максимизатора однозначным там, где значений-претендентов несколько. И тот же разбор задаёт образец Части V: каждое аналитическое понятие читается как система со своей E/R/R-структурой.

Равномерная непрерывность и граница $Q$ {Равномерная непрерывность и граница Q}

Определение равномерной непрерывности

§ 3.2 дало поточечную непрерывность. Теперь нужно её усиление — понятие, на котором будет стоять вся вторая половина главы.

Поточечная непрерывность позволяет $δ$ зависеть от точки: у каждого $x$ — своя окрестность. Для двух больших теорем анализа этого мало; им нужен единый масштаб — одна $δ$ , годная сразу для всего отрезка. Это требование и выделяет равномерную непрерывность: функция равномерно непрерывна на $[a, b]$ , если для всякой требуемой точности $ε$ можно указать одну $δ$ такую, что любая пара аргументов отрезка, отстоящих меньше чем на $δ$ , даёт значения, отстоящие меньше чем на $ε$ . В Rocq это записано так:

Definition uniformly_continuous_on (f : Q -> Q) (a b : Q) : Prop :=
  forall eps : Q, eps > 0 -> exists delta : Q, delta > 0 /\
    forall x y : Q, a <= x <= b -> a <= y <= b ->
      Qabs (x - y) < delta -> Qabs (f x - f y) < eps.

Всё различие с поточечной непрерывностью § 3.2 — в порядке кванторов. Там $δ$ стояла внутри квантора по точке: <<для каждой точки — своя $δ$ >>. Здесь $δ$ вынесена наружу, перед квантором по $x$ и $y$ : одна $δ$ на весь отрезок. Перестановка двух кванторов — и получается принципиально иное, более сильное свойство: единый масштаб, на котором функция ведёт себя смирно всюду на $[a, b]$ сразу.

{ Об этом понятии нужно сказать одно честное слово — о его статусе в нашем построении. Канонический головной файл теории непрерывности теперь есть — analysis/Continuity.v: в нём сведены воедино определения continuous_on, uniformly_continuous_on и Lipschitz_on (для $f : Q \to Q$ на отрезке $[a, b]$ ), доказан мост lipschitz_uniform (липшицевость влечёт равномерную непрерывность) и переход uniformly_continuous_pointwise, а с ними элементарная алгебра (константа, тождество, сумма) — всё без аксиом. Честная оговорка, однако, двоякая. Во-первых, миграция: существующие большие теоремы — IVT_ERR.v, EVT_ERR.v, EVT_idx.v, HeineBorelComplete.v — пока не переведены на этот головной файл: каждая по-прежнему несёт своё локальное, дословно повторяющееся определение uniformly_continuous_on, и сведение их к канону отложено (чтобы не вызывать каскад правок в уже доказанном). Во-вторых, обратного перехода — от поточечной непрерывности к равномерной — в каноне нет, и это не упущение: над $Q$ он неверен (теорема Кантора–Гейне, к которой глава переходит ниже). Так что головной файл задаёт канон и Липшицев путь к равномерности, но единой теорией, на которую опираются все теоремы главы, он станет лишь после миграции. }

Кантора–Гейне над Q неверна

Теперь — центральный для главы факт. И подать его надо так же прямо, как в § 2.5 был подан провал Гейне–Бореля.

Над $Q$ поточечная непрерывность на отрезке не влечёт равномерную. Классическая теорема Кантора–Гейне над $Q$ неверна.

Классическая теорема Кантора–Гейне утверждает: функция, поточечно непрерывная на замкнутом ограниченном отрезке, на нём автоматически равномерно непрерывна. Над действительными числами это так. Над рациональными — нет.

Корень — тот же, что и у провала Гейне–Бореля в § 2.5: неполнота $Q$ . Классическое доказательство Кантора–Гейне опирается на компактность отрезка в полном смысле: из любого покрытия локальными $δ$ -окрестностями извлекается конечное подпокрытие, и минимум конечного набора $δ$ даёт искомую глобальную $δ$ . Над $Q$ этот ход не проходит. Рациональный отрезок не компактен в классическом смысле (§ 2.5): покрытие может <<утекать>> в иррациональный зазор, и локальные $δ$ , мельчая к зазору, не дают положительного минимума. Поточечная непрерывность остаётся — а стянуть её в равномерную нечем.

Это не дефект формализации. Это математический факт о $Q$ , прямое продолжение того, что Глава 5.2 установила о компактности. Рациональная прямая дырява, и дыры мешают равномерности так же, как мешали конечному подпокрытию.

У этого факта есть простое, вполне осязаемое лицо — конкретный пример. Возьмём функцию

f (x) = \frac{1}{x ^{2} - 2}

на рациональном отрезке $[1, 2] \cap Q$ . Для всякого рационального $x$ знаменатель $x^{2} - 2$ отличен от нуля — $2$ иррационально, рациональный квадрат двойке не равен, — поэтому функция определена и поточечно непрерывна в каждой точке отрезка. Но равномерно непрерывной она не является. Рациональные точки могут подходить к иррациональному разрезу $2$ сколь угодно близко, и у самого разреза значения $f$ растут неограниченно. Никакой единой $δ$ , годной на всём рациональном отрезке сразу, для такой функции нет: чем ближе к $2$ , тем мельче приходится брать окрестность. Это и есть конкретное лицо неполноты $Q$ — локальная непрерывность есть в каждой точке, а глобальной равномерности нет, потому что отрезок дыряв и функция пользуется дырой.³

Конструктивная замена: липшицевость

Если мост <<непрерывность $\Rightarrow$ равномерность>> над $Q$ обрушен, нужен другой путь к равномерной непрерывности — такой, который над $Q$ держит, не опираясь на полноту. Такой путь ToS и прокладывает, и ведёт он через липшицевость.

Функция липшицева с константой $L$ , если расстояние между значениями не превосходит $L$ , помноженного на расстояние между аргументами: $∣ f (x) - f (y) ∣ \leq L ∣ x - y ∣$ . Из этого свойства равномерная непрерывность следует прямым счётом. В самом деле: задано $ε$ ; возьмём $δ = ε / L$ (при $L > 0$ ); тогда для всякой пары аргументов ближе $δ$ имеем $∣ f (x) - f (y) ∣ \leq L ∣ x - y ∣ < L \cdot ε / L = ε$ . Одна $δ$ , годная сразу для всего отрезка, не подобрана наугад, а вычислена по $ε$ и $L$ . Вырожденный случай $L = 0$ — постоянная функция — ещё проще: годится любая $δ$ . Этот вывод формализован в HeineBorelComplete.v (с этим файлом глава встречалась в § 2.6) теоремой:

Theorem lipschitz_uniform_cont : forall f a b L,
  Lipschitz_on f a b L ->
  uniformly_continuous_on f a b.

Вот в чём смысл этой замены. Над $R$ путь к равномерной непрерывности шёл так: непрерывность $\Rightarrow$ (по Кантору–Гейне) равномерность. Над $Q$ первая стрелка сломана. Но есть обходной путь: липшицевость $\Rightarrow$ равномерность, — и этот путь конструктивен, он не зависит от полноты. Там, где классика пользуется недоказуемой над $Q$ импликацией, ToS пользуется доказуемой: липшицевость — проверяемое, вычислимое свойство, и из него равномерная непрерывность следует прямым счётом.

{ И вокруг этого моста — та же алгебра, что в § 3.2 окружала поточечную непрерывность. Сумма, масштабирование и композиция равномерно непрерывных функций снова равномерно непрерывны, тождество и постоянная равномерно непрерывны: класс равномерно непрерывных функций так же замкнут и богат, как класс непрерывных. Эти замыкания подтверждены в HeineBorelComplete.v леммами uniform_cont_sum, uniform_cont_scale, uniform_cont_composition. }

Почему теоремы анализа требуют равномерной непрерывности

Теперь видно, почему обе главные теоремы главы — о промежуточном значении (§ 3.4) и об экстремуме (§ 3.6) — формализованы с гипотезой именно равномерной непрерывности.

Это прямое следствие § 3.3.2. Над $R$ можно было бы записать эти теоремы с гипотезой поточечной непрерывности — а равномерность получить попутно, из Кантора–Гейне. Над $Q$ так нельзя: Кантора–Гейне не действует. Значит, равномерность, которая в доказательствах реально нужна (нужен единый $δ$ , чтобы оценки работали по всему отрезку сразу), приходится требовать явно — внести в гипотезу теоремы. В терминах разбора § 3.2.4 это усиление правила: над $Q$ конституция непрерывности требует равномерной формы.

И это, по логике всей Части V, — не слабость, а точность. Теорема, честно записанная над $Q$ , обязана нести в условии ровно то, на чём стоит её доказательство. Гипотеза uniformly_continuous_on в формулировках IVT и EVT — не лишняя предосторожность, а точное указание уровня: вот при каком условии теорема над $Q$ верна. Когда в § 3.4 и § 3.6 глава будет читать сигнатуры главных теорем, эта гипотеза будет стоять там не случайно — она поставлена туда неполнотой $Q$ .

Теорема о промежуточном значении: бисекция

Замысел теоремы

Первая большая теорема главы — теорема о промежуточном значении. Классическая формулировка проста и наглядна: если непрерывная функция $f$ на концах отрезка имеет значения разных знаков — $f (a) < 0$ и $f (b) > 0$ , — то где-то между $a$ и $b$ она обращается в нуль. Непрерывная функция не может перескочить через нуль, не коснувшись его.

Классика говорит: существует точка $c$ с $f (c) = 0$ . ToS, по $P 4$ , говорит иначе. Завершённой точки $c$ может и не быть — корень способен оказаться иррациональным, а иррационального числа в $Q$ нет. Поэтому ToS строит не точку, а процесс: алгоритм, который шаг за шагом всё точнее локализует, где функция переходит через нуль. Корень — это сам процесс, не его недостижимый предел. Как именно мы строим этот процесс — предмет следующего подраздела; построенная конструкция целиком формализована в файле IVT_ERR.v (424 строки, двадцать три доказанные теоремы, ни одного незакрытого места).

Алгоритм бисекции

Процесс, локализующий корень, мы строим бисекцией — делением пополам. Идея проста. Перемена знака заперта внутри отрезка $[a, b]$ ; поделим отрезок надвое и посмотрим, в какой половине заперта она теперь. Знак функции в середине отрезка — решает: если в середине $f$ отрицательна, перемена знака ушла в правую половину, если неотрицательна — в левую. Берём ту половину, где перемена знака осталась, и повторяем. Отрезок ужимается вдвое за шаг, а перемена знака на его концах не теряется.

Чтобы это формализовать, опишем состояние процесса — пару концов текущего отрезка — и шаг, переводящий состояние в состояние:

Record BisectionState := mkBisection { bis_left : Q; bis_right : Q }.
 
Definition bisection_step (f : ContinuousFunction) (s : BisectionState)
  : BisectionState :=
  let mid := (bis_left s + bis_right s) / 2 in
  if Qlt_le_dec (f mid) 0
  then mkBisection mid (bis_right s)
  else mkBisection (bis_left s) mid.

Так IVT_ERR.v записывает один шаг бисекции. mid — середина; Qlt_le_dec проверяет знак $f$ в ней; в зависимости от знака новым состоянием становится правая половина $[mid, right]$ или левая $[left, mid]$ — ровно та половина, где перемена знака сохранилась.

Существенно здесь одно — Qlt_le_dec. Это решающая процедура: для рациональных чисел вопрос << $f (mid) < 0$ или $f (mid) \geq 0$ ?>> решается вычислением, за конечное время, без всякого обращения к закону исключённого третьего. Выбор половины здесь конструктивен — и этим бисекция IVT отличается от бисекции Больцано–Вейерштрасса (§ 2.7), где выбор населённой половины не вычислялся и требовал $L 3$ .

Шаг бисекции построен; теперь надо повторять его и собирать результат в процесс. Применив шаг $n$ раз к начальному отрезку $[a, b]$ и взяв середину получившегося отрезка, мы получаем $n$ -е приближение корня. Последовательность этих середин и есть искомый процесс — локализатор корня. В IVT_ERR.v итерация шага и сам процесс записаны так (bisection_iter применяет шаг $n$ раз, bisection_process выдаёт середину):

Definition bisection_process (f : ContinuousFunction) (a b : Q)
  : RealProcess :=
  fun n => let s := bisection_iter f (mkBisection a b) n in
           (bis_left s + bis_right s) / 2.

На шаге $n$ процесс выдаёт середину $n$ -го вложенного отрезка — рациональное приближение корня тем точнее, чем больше $n$ .

Ширина и свойство Коши

Чтобы последовательность середин была осмысленным приближением корня, вложенные отрезки должны стягиваться к точке — иначе <<приближение>> ни к чему не приближается. Убедимся, что они стягиваются, и установим, что процесс середин — процесс Коши.

Каждый шаг бисекции делит отрезок ровно пополам; значит, после $n$ шагов ширина отрезка есть в точности $(b - a) / 2^{n}$ . Это устанавливает лемма bisection_width. Дальше работает архимедовость $Q$ : величина $(b - a) / 2^{n}$ становится меньше любой наперёд заданной за конечное число шагов. А раз отрезки вложены и ширина их стремится к нулю, середины сближаются: для всякой точности найдётся шаг, после которого все середины лежат теснее требуемого, — то есть процесс середин есть процесс Коши. Этот вывод подтверждён в IVT_ERR.v леммами bisection_shrinks и bisection_is_Cauchy. Процесс бисекции — полноценный Cauchy-процесс в смысле Главы 5.1; темп его сходимости — $1/2$ за шаг.

Слабый инвариант знака

Чтобы бисекция работала, на концах каждого вложенного отрезка должна сохраняться перемена знака. Спросим точно: какой инвариант мы можем здесь доказать?

Естественно было бы ждать строгого инварианта: на концах каждого отрезка $f (left) < 0$ и $f (right) > 0$ . Но строгий инвариант над $Q$ недоказуем — и вот почему. Середина отрезка — рациональное число; $f$ — функция $Q \to Q$ . Вполне может случиться, что $f (mid)$ окажется точно равно нулю: для рациональной функции это не исключение, а возможный случай. Если такое произошло, на новом конце отрезка $f$ обращается в нуль ровно — и строгое неравенство там нарушено.

{ Значит, доказуемый инвариант — слабый: $f (left) \leq 0$ и $f (right) \geq 0$ , с нестрогими неравенствами. И этого вполне достаточно. Если в какой-то середине $f$ обратилась точно в нуль — тем лучше, корень найден буквально; а если нет — слабый инвариант продолжает зажимать перемену знака между концами. Именно слабый инвариант — то, что нужно теории, и именно его IVT_ERR.v и доказывает, под именем bisection_preserves_signs_weak; слово weak в имени стоит не случайно. Слабая формулировка — не небрежность, а точный учёт того, что над $Q$ функция может попасть в нуль ровно. }

Главная теорема

Все части собраны: бисекция строит вложенные отрезки, ширина их стремится к нулю, процесс середин есть Коши, слабый инвариант удерживает перемену знака. Собрав их, получаем теорему о промежуточном значении — в IVT_ERR.v она записана так:

Theorem IVT_process : forall (f : ContinuousFunction) (a b : Q),
  a < b -> uniformly_continuous_on f a b ->
  f a < 0 -> f b > 0 ->
  exists c : RealProcess, is_Cauchy c /\ in_interval a b c /\
    equiv (apply_to_process f c) (fun _ => 0).

Прочтём её внимательно — здесь сразу две точки точности.

Первое — гипотеза. В условии стоит uniformly_continuous_on, равномерная непрерывность, не поточечная. Это ровно то, о чём говорил § 3.3.4: над $Q$ Кантора–Гейне не действует, и равномерность — то, что реально нужно доказательству (единый $δ$ , чтобы оценка $∣ f (mid) - f (left) ∣$ работала на любом шаге), — внесена в гипотезу явно.

Второе — заключение. Теорема даёт не <<точку $c$ с $f (c) = 0$ >>, а процесс $c$ — Cauchy-процесс, лежащий в $[a, b]$ , — для которого equiv (apply_to_process f c) (fun _ => 0). Это значит: процесс значений $f (c)$ эквивалентен нулевому процессу. Не << $f (c)$ равно нулю буквально>>, а <<процесс $f (c)$ сколь угодно близок к нулю>>. Разница принципиальна и снова идёт от $P 4$ : буквальный корень над $Q$ может не существовать (он иррационален), но процесс, чьи значения под $f$ неотличимо приближаются к нулю, существует и построен — это сама бисекция.

И — по уговору § 3.1 — об основании. Доказательство опирается на архимедовость $Q$ и через неё — на classic, аксиому, приходящую в файл из Archimedean_ERR. По уговору: classic — техническая Rocq-реализация $L 3$ . Обращение к ней — явный учёт уровня. Сам выбор половины, отметим, конструктивен (Qlt_le_dec); $L 3$ нужен не для выбора, а в архимедовой части рассуждения.

IVT на трёх уровнях

Один факт, три высоты типизации

Теорема о промежуточном значении формализована в ToS трижды — не из повторения, а потому, что один и тот же математический факт можно записать на разной высоте типизации. Три файла — IVT_ERR.v, ProcessIVT.v, IVT_CauchyReal.v — дают три уровня. § 3.4 разобрал нижний; теперь — два верхних.

Уровень процесса

На первом уровне корень был RealProcess — функцией $N \to Q$ , голой последовательностью рациональных чисел, к которой свойство Коши приложено отдельной леммой. Поднять результат на уровень процессов в смысле ProcessCore — того аппарата, на котором стоит вся Часть V, — значит переписать теорему в его языке. Это и делает второй уровень.

{ Основная работа здесь — навести мосты совместимости. Загвоздка техническая: свойство Коши определяется двумя чуть разными способами. Archimedean_ERR, откуда пришла бисекция, формулирует его через условие $(m > N)$ ; ProcessCore формулирует через $(N \leq m)$ . Условия равносильны — с точностью до сдвига $N$ на единицу, — но формально это разные предикаты, и прежде чем переносить теорему, надо их равносильность доказать. Доказав её, мы и получаем мосты: cauchy_compat (свойства Коши совпадают), interval_compat (совпадают определения <<лежать в $[a, b]$ >>), equiv_compat (совпадают определения эквивалентности процессов). По этим мостам теорема о промежуточном значении переписывается в типах ProcessCore как process_IVT, а ivt_convergence_rate фиксирует темп — $1/2$ . Всё это — содержание файла ProcessIVT.v (175 строк). }

Новых математических трудностей на этом уровне нет: бисекция и её сходимость уже доказаны, здесь — лишь аккуратная стыковка теоремы с языком процессов ToS. И своих аксиом этот уровень не вносит: classic он наследует от IVT_ERR, ничего к нему не добавляя.

Уровень типа: корень как CauchySeq

Третий уровень — IVT_CauchyReal.v (382 строки) — делает шаг тоньше. На первых двух уровнях корень был последовательностью, а свойство Коши — отдельным утверждением о ней. Здесь корень предъявляется как объект типа CauchySeq — типа, в который Коши-свойство встроено. Носить с собой доказательство свойства Коши отдельно больше не нужно: оно стало частью самого объекта.

Theorem ivt_cauchy_real :
  forall (f : ContinuousFunction) (a b : Q),
    a < b -> uniformly_continuous_on f a b ->
    f a < 0 -> f b > 0 ->
    exists c : CauchySeq,
      (forall n : nat, a <= cs_seq c n /\ cs_seq c n <= b) /\
      (forall eps : Q, 0 < eps ->
        exists N : nat, forall n : nat,
          (N <= n)%nat -> Qabs (f (cs_seq c n)) < eps).

Корень — c : CauchySeq: не <<последовательность, про которую доказано, что она Коши>>, а объект, чья типовая принадлежность уже несёт доказательство свойства Коши.

Существенная для этого уровня лемма — continuous_compose_cauchy. Она утверждает: если $f$ равномерно непрерывна, а $c$ — Cauchy-последовательность в $[a, b]$ , то и композиция $f \circ c$ — снова Cauchy. Равномерная непрерывность сохраняет свойство Коши. И здесь опять видно, зачем нужна именно равномерная непрерывность, а не поточечная: общий $δ$ позволяет из близости членов $c$ заключить близость членов $f \circ c$ единообразно, не подбирая $δ$ заново под каждую точку. Главная теорема ivt_cauchy_real и её следствие ivt_cauchy_real_equiv (которое выражает результат через cauchy_equiv с постоянным нулём) стоят на этой лемме.

Зачем три уровня

Стоит сказать, зачем один факт записан трижды. Дело не в избыточности, а в интенсиональной точности — в принципе $P 3$ .

{ Три уровня — это три ответа на вопрос <<что есть корень>>. На уровне IVT_ERR — голая последовательность плюс отдельная справка о её свойстве Коши. На уровне ProcessIVT — процесс в смысле ProcessCore, встроенный в общий аппарат Части V. На уровне IVT_CauchyReal — объект, в типе которого свойство Коши уже записано. Математическое содержание — бисекция, сходящаяся к перемене знака — одно. Но как объект задан, что он есть интенсионально — меняется от уровня к уровню. По $P 3$ это и значит, что перед нами три разных, хотя и согласованных, представления одного факта. ToS строит лестницу типизации, и теорема о промежуточном значении прописана на каждой её ступени. В терминах разбора § 3.2.4 это три роли-представления одного корня — разные по типу, согласованные по содержанию ( $P 3$ ). }

Теорема об экстремуме: сетка

Замысел теоремы

Вторая большая теорема главы — теорема об экстремуме. Классическая формулировка: непрерывная функция на замкнутом отрезке достигает на нём своего максимума — есть точка $x^{*}$ , в которой $f (x^{*})$ не меньше всех остальных значений.

И снова ToS читает <<достигает>> по $P 4$ . Завершённой точки максимума может не быть — $x^{*}$ способна оказаться иррациональной. Поэтому максимум строится как процесс: последовательность всё более подробных приближений. Но здесь, в отличие от теоремы о промежуточном значении, процессов оказывается два, и они ведут себя по-разному. Это — узловая точность раздела, и к ней § 3.6.3 вернётся отдельно.

Опорные файлы EVT — три: EVT_ERR.v как историческая argmax-версия, EVT_idx.v как текущая рекомендуемая index-версия, и process-обёртка ProcessEVT.v. В § 3.6 мы объясним общую конструкцию — сетку и процесс значений; в § 3.7 разберём, почему текущей основной версией является именно EVT_idx.v.

Сетка

Инструмент теоремы об экстремуме — не бисекция, а сетка. Бисекция годилась для корня: знак функции в середине указывал, какую половину взять. Для максимума такого указателя нет — максимум может прятаться где угодно на отрезке. Поэтому максимум мы ищем иначе: расставляем на отрезке конечный равномерный набор пробных точек, вычисляем $f$ во всех узлах, берём наибольшее — и затем измельчаем сетку, добавляя узлы. Чем гуще сетка, тем точнее наибольшее значение по узлам приближает истинный максимум.

Узел сетки строится прямой формулой: $k$ -й из $n + 1$ равноотстоящих узлов отрезка $[a, b]$ есть $a + \frac{k}{n} (b - a)$ . В Rocq это записано так:

Definition grid_point (a b : Q) (n k : nat) : Q :=
  a + (inject_Z (Z.of_nat k)) * (b - a) / (inject_Z (Z.of_nat n)).

При $k = 0$ это $a$ , при $k = n$ — $b$ , между — равномерные узлы; grid_list собирает их в конечный список. Измельчение — это рост $n$ : на шаге $n$ сетка тем гуще, чем $n$ больше.

И здесь стоит отметить $P 4$ в работе. Процесс поиска максимума разворачивается бесконечно — но всякий его кадр — конечный, обозримый список узлов, на котором $f$ вычисляется конечным числом операций. Никакой завершённой бесконечности; на каждом шаге — актуально конечная сетка.

Значение против позиции

Теперь — узловая точность всего раздела. На сетке у максимума два аспекта, и над $Q$ они ведут себя по-разному.

Значение максимума — max_on_grid, наибольшее из значений $f$ по узлам сетки. Позиция максимума — argmax, тот узел, на котором это наибольшее значение достигается. С измельчением сетки оба, казалось бы, должны сходиться. Но это не так.

{ Процесс значений — sup_process — сходится. Файл доказывает sup_process_is_Cauchy: последовательность наибольших значений по всё более густым сеткам есть процесс Коши. }

Процесс позиций — argmax_process — сходиться не обязан. И EVT_ERR.v прямо это оговаривает в комментарии. Представим постоянную функцию: $f (x) = 1$ всюду. Тогда наибольшее значение достигается в каждом узле сетки. Без фиксированного правила выбора <<позиция максимума>> здесь вообще не определена однозначно: при разных допустимых выборах она может скакать от узла к узлу при каждом измельчении. Процесс значений при этом безупречно сходится — он попросту постоянен и равен единице.

Index-версия (§ 3.7) как раз вводит такое правило — $L 5$ -порядок позиций, — чтобы сделать позицию на каждом шаге детерминированной. Но и детерминированности мало: даже с однозначно выбираемой позицией процесс argmax_process над $Q$ Cauchy быть не обязан. Максимум может приближаться к иррациональной точке, и тогда процесс рациональных приближений позиции к Cauchy-процессу не сводится; или позиция может перескакивать с одной стороны на другую при измельчении сетки. Процесс значений от всех этих бед свободен.

Вывод, который глава должна сформулировать прямо: теорема об экстремуме над $Q$ доказывает сходимость процесса значений, не процесса позиций. По $P 4$ это и есть верное прочтение <<максимума>>: фундаментален процесс значения супремума; позиция — производное, более хрупкое понятие, требующее дополнительной структуры (изоляции максимума), которой в общем случае нет. В терминах разбора § 3.2.4 перед нами расщепление роли: значение и позиция — две роли максимума, и над $Q$ Коши-устойчива лишь первая.

Главная теорема

Собрав сетку, процесс наибольших значений и его свойства, мы получаем теорему об экстремуме. В EVT_ERR.v она записана так:

Theorem EVT_complete : forall f a b,
  a < b -> uniformly_continuous_on f a b ->
  exists (M : RealProcess) (c : RealProcess),
    is_Cauchy M /\
    (forall n, a <= c n <= b) /\
    (forall n, apply_f f c n == M n) /\
    (forall x, a <= x <= b -> process_le (fun _ => f x) M).

Теорема даёт два процесса: $M$ — процесс значений супремума, и $c$ — процесс приближённых максимизаторов. Утверждается: $M$ есть процесс Коши; $c$ лежит в $[a, b]$ ; на каждом шаге $f (c)$ совпадает с $M$ ; и $M$ мажорирует $f$ — значение $f$ в любой точке отрезка не превосходит $M$ (с точностью до процессного $\leq$ ). Гипотеза — снова uniformly_continuous_on, равномерная непрерывность, по причине из § 3.3.4.

{ И здесь честность требует отметить, чего в этой формулировке нет — по сравнению с тем, что хотелось бы доказать. Глядя на § 3.6.3, естественно ждать в заключении и Коши-свойства для процесса позиций $c$ . Его там нет, и в такой общей формулировке оно стоять не должно: задача максимизации сама по себе Коши-свойства процесса позиций не гарантирует. При плато или нескольких равноценных максимумах выбор позиции требует дополнительного правила; без него позиционный процесс может оказаться скачущим. Поэтому формулировку пришлось ослабить — оставить Коши-свойство только за процессом значений $M$ . Именно это — сходимость $M$ и его мажорирующее свойство — и есть честное содержание теоремы об экстремуме над $Q$ ; и именно так EVT_complete в репозитории и сформулирована (комментарий файла отмечает это ослабление прямо). Глава не выдаёт EVT_complete за полную классическую теорему: это её отремонтированная, ослабленная — и потому верная — форма. }

EVT: argmax-версия, index-версия, обёртка

Две версии главного файла

Теорема об экстремуме формализована в репозитории дважды, и об этих двух формализациях нужно сказать прямо — потому что одна из них наткнулась на затруднение, а другая его обошла.

{ Первая формализация — EVT_ERR.v, argmax-версия. Сегодня это историческая версия: в её шапке стоит пометка <<DEPRECATED: Use EVT_idx.v instead>>, и к использованию рекомендована не она. След того затруднения, ради которого версию сменили, виден и внутри файла: одна лемма — max_list_attained — обрывается командой Abort; доказать её в задуманном виде не удалось, и в дело пошёл обходной вариант max_list_attained_classical. Мы не прячем этот Abort — он и есть свидетельство того, что argmax-версия упёрлась в стену. }

Вторая формализация — EVT_idx.v — эту стену обходит, и она же сегодня рекомендуемая, основная. Чтобы понять, почему понадобилась смена версии, разберём, в чём состояло затруднение и в чём — его решение.

Index-based решение

Затруднение argmax-версии — тонкое, но показательное. Оно в различии двух равенств рациональных чисел. Есть равенство по значению, Qeq: числа $1/2$ и $2/4$ равны как рациональные. И есть равенство буквальное, лейбницево: $1/2$ и $2/4$ — разные выражения, разные представления. Узел сетки grid_point a b n 0 равен $a$ по значению (Qeq), но не буквально — это разные термы. Argmax-версия, выбирая максимум по значениям, всё время спотыкалась об этот разрыв: доказательства о том, что максимум достигается, вязли в согласовании Qeq с лейбницевым равенством.

EVT_idx.v обходит это затруднение переключением внимания — и приём стоит того, чтобы назвать его прямо: вместо значения наилучшего узла argmax возвращает его номер, индекс в списке. Не <<какое значение наибольшее>>, а <<на каком месте оно стоит>>. В Rocq это записано так:

Definition argmax_idx (f : Q -> Q) (l : list Q) (default : Q) : nat :=
  match l with
  | [] => O
  | x :: xs => find_max_idx_acc f xs 1%nat O (f x)
  end.

find_max_idx_acc — аккумуляторный обход списка, возвращающий индекс наилучшего узла; max_on_grid определяется тогда как $f$ от узла, стоящего на этом индексе. Выигрыш немедленный. Лемма <<максимум на сетке достигается>> — max_on_grid_attained — в index-версии становится тривиальной: она доказывается одним словом reflexivity. Достижение максимума здесь определительно — максимум по построению есть $f$ от узла на найденном индексе, — и согласовывать Qeq с лейбницевым равенством больше негде. Индексы — натуральные числа, с равенством у них никаких тонкостей нет. Так переключение с значения на позицию снимает затруднение, в которое упёрлась argmax-версия.

L5 и статус argmax

С переходом к индексам проясняется и более глубокий вопрос — что вообще такое <<позиция максимума>>, когда максимум достигается не в одной точке. Разберём его; ответ опирается на закон логики ToS, и тот же ответ зафиксирован в комментарии EVT_idx.v.

Представим плато: на сетке несколько узлов дают одно и то же наибольшее значение, $f (x_{1}) = f (x_{2}) = f (x_{3}) = M$ . Какой из них — <>? Наивный ответ: <<надо разрешить ничью>>, доопределить выбор каким-то внешним правилом. Точнее — иначе. Здесь работает $L 5$ , закон порядка ToS. $L 5$ конституирует порядок позиций; и <> мы определяем через этот порядок — как выделенную $L 5$ -позицию, достигающую максимума: позицию, отобранную фиксированным порядком обхода сетки. На плато роль <> назначается $L 5$ не как <<разрешение ничьей>> внешним правилом, а потому, что сам $L 5$ задаёт порядок, в котором узлы рассматриваются. Ничьей нет: порядок $L 5$ выделяет позицию, а вполне-упорядоченность натуральных индексов делает выбор однозначным. Никакой внешней информации не добавляется — структура берётся из самого закона порядка.

Уточним, что значит <<выделенная>> — и при чтении кода здесь стоит быть внимательным. В аккумуляторе find_max_idx_acc сравнение узлов идёт через Qle_bool, и обновление наилучшего индекса происходит при равенстве значений. Если сетка перечисляется слева направо, выделенной окажется одна позиция; если список реализует обратный порядок или иначе обновляет при равенстве — другая. Важно поэтому не <<левая первой>> само по себе — важно отсутствие произвольного внешнего выбора: <> детерминирован порядком $L 5$ , каким бы конкретно порядком перечисления узлов этот $L 5$ -приоритет ни был реализован. Index-версия как раз и делает выбор детерминированным; для полной прозрачности следует лишь держать в виду, какой порядок обхода сетки этот приоритет воплощает.

Итог секции EVT_STRONG файла — теорема EVT_strong_process: процесс значений супремума есть Коши, процесс позиций лежит в $[a, b]$ , и на каждом шаге значение супремума совпадает с $f$ от позиции. То же честное содержание, что и в EVT_complete (§ 3.6.4): сходимость доказана для процесса значений; о процессе позиций комментарий EVT_idx.v прямо повторяет — над $Q$ он Коши быть не обязан, его предел может оказаться иррациональным.

Process-обёртка

{ Третий файл — ProcessEVT.v (133 строки) — играет ту же роль, что ProcessIVT.v для теоремы о промежуточном значении: тонкая обёртка, переносящая результат на язык процессов ProcessCore. Мосты Cauchy-совместимости (evt_cauchy_ compat), sup_process_cauchy, process_EVT; evt_convergence_rate фиксирует темп — $1/2$ . }

Здесь важна одна оговорка о согласованности. ProcessEVT.v оборачивает именно слой EVT_ERR.v — он импортирует историческую argmax-версию, а не новую index-версию EVT_idx.v. Поэтому ProcessEVT.v следует читать как process-адаптацию исторической формулировки теоремы об экстремуме. А для вопроса о достижении максимума на сетке и для разрешения затруднения <<Qeq против лейбницева равенства>> главным файлом остаётся EVT_idx.v.

И — последняя для раздела точность, по уговору § 3.1. Файл EVT_idx.v устроен в отношении аксиом с особенностью: он импортирует ToS_Axioms и при этом ещё раз объявляет Axiom classic локально, внутри самого файла. Содержательно это тот же $L 3$ — закон исключённого третьего: по замыслу обе classic — одна и та же техническая Rocq-реализация закона логики ToS. Но технически файл объявляет $L 3$ отдельной локальной аксиомой — и при чтении Print Assumptions эту зависимость следует учитывать именно как локальное объявление, а не автоматически как тот же самый объект из ToS_Axioms.v. Глава отмечает это как особенность файла; на статус доказательства это не влияет — по уговору § 3.1 обращение к $L 3$ есть явный учёт уровня.

Равномерный предел, связь и итог главы

Равномерный предел непрерывных функций

Остаётся последний сюжет главы — и он отвечает на естественный вопрос: сохраняется ли непрерывность при предельном переходе? Если последовательность непрерывных функций к чему-то сходится, будет ли предел непрерывен?

Ответ зависит от вида сходимости — и здесь придётся, как уже было с непрерывностью в § 3.3, различить поточечное и равномерное. Сходимость последовательности функций $f_{n}$ к функции $f$ бывает поточечной: в каждой точке $x$ по отдельности значения $f_{n} (x)$ сходятся к $f (x)$ . И бывает равномерной: номер $N$ , после которого $f_{n}$ уже неотличимо близка к $f$ , един для всего отрезка сразу. Равномерную сходимость на $[a, b]$ записывают так:

Definition uniform_converges (fn : fun_seq) (f : Q -> Q) (a b : Q)
  : Prop :=
  forall eps : Q, 0 < eps ->
    exists N : nat, forall n : nat,
      (N <= n)%nat -> forall x : Q, a <= x -> x <= b ->
        Qabs (fn n x - f x) < eps.

И здесь — та же перестановка кванторов, что отличала равномерную непрерывность от поточечной (§ 3.3). При равномерной сходимости номер $N$ вынесен наружу, перед квантором по точке: после шага $N$ все функции $f_{n}$ отстоят от $f$ ближе $ε$ сразу во всех точках. Этого — и только этого — хватает, чтобы непрерывность пережила предельный переход:

Theorem uniform_limit_continuous_on :
  forall (fn : fun_seq) (f : Q -> Q) (a b : Q),
    uniform_converges fn f a b ->
    (forall n : nat, continuous_on (fn n) a b) ->
    continuous_on f a b.

Равномерный предел непрерывных функций непрерывен. Если все $f_{n}$ непрерывны на $[a, b]$ и сходятся к $f$ равномерно, то и $f$ непрерывна. Доказательство — классический приём << $ε /3$ >>: расстояние $∣ f (x + h) - f (x) ∣$ разбивается на три части — от $f$ к близкому $f_{n}$ , от $f_{n} (x + h)$ к $f_{n} (x)$ по непрерывности $f_{n}$ , и обратно от $f_{n}$ к $f$ , — и каждая делается меньше $ε /3$ . Это полноценная содержательная теорема о непрерывности, и она завершает понятийную линию главы: непрерывность не только определена и снабжена двумя большими теоремами, но и устойчива относительно равномерного предельного перехода.

Одна честная оговорка о границах. Файл UniformConvergence.v — шире этой одной теоремы: в нём есть и обмен предела с интегралом, и обмен с производной, и теорема Дини. Но эти сюжеты опираются на интегрирование и дифференцирование — на аппарат, который Часть V строит позже. Глава 5.3 берёт из UniformConvergence.v только то, что относится собственно к непрерывности, — определение continuous_on и теорему о равномерном пределе. Обмен предела с интегралом и производной — материал одной из последующих глав Части V.

{ И — по уговору § 3.1 — слово об аксиомном статусе. Шапка файла UniformConvergence.v объявляет, что файл в целом импортирует классический слой — classic приходит в него через смежные результаты о монотонной сходимости и дифференцировании. Само доказательство uniform_limit_continuous_on имеет стандартный $ε /3$ -вид. Однако без отдельной проверки Print Assumptions именно этой теоремы глава не утверждает её аксиомной чистоты — по правилу аудита, заведённому ещё в Главе 4.6: аксиомный статус устанавливается по Print Assumptions конкретной теоремы, а не приписывается ей от заголовка файла. Поэтому глава использует uniform_limit_continuous_on как рабочий результат о равномерных пределах, а суждение о его аксиомной чистоте оставляет этой проверке. }

Смежная заготовка: отображения процессов

{ Стоит, чтобы карта была полной, упомянуть ещё один файл — ProcessContinuity.v. Имя обещает теорию непрерывности, но содержание иное, и честнее сказать это прямо. Файл маленький (36 строк) и говорит не о непрерывности функций $Q \to Q$ , а об отображениях процессов — отображениях $‘ R e a l P r ocess ‘ \to ‘ R e a l P r ocess ‘$ . Он вводит process_map_lipschitz (липшицевость такого отображения) и process_contraction (сжатие) — понятия, относящиеся к будущей линии неподвижных точек, а не к настоящей главе. Его теорема с громким именем continuity_foundation — как и одноимённые <> из Главы 5.1 — честно есть лишь конъюнкция двух тривиальных лемм (тождественное отображение липшицево с константой $1$ , постоянное — с константой $0$ ). К теории непрерывности функций ProcessContinuity.v прямого отношения не имеет; глава называет это прямо. }

Что построено и что готовится

Итог главы — тремя списками, по дисциплине honest-режима Части V.

Построено и проверено.

{ Топологическое лицо непрерывности над $Q$ — $δ$ - $ε$ определение (continuous_at, continuous, continuous_on), алгебра непрерывных функций, прообраз открытого открыт; конструктивно, без аксиом (Topology.v).}
Равномерная непрерывность и конструктивный мост к ней — lipschitz_uniform_cont (липшицевость влечёт равномерную непрерывность), с алгеброй равномерно непрерывных функций.
Теорема о промежуточном значении на трёх уровнях — $ε$ -версия (IVT_process), процессная обёртка (process_IVT), типовой апгрейд до CauchySeq (ivt_cauchy_real); корень — бисекционный Cauchy-процесс.
Теорема об экстремуме в двух версиях: историческая argmax-версия EVT_complete сохранена, но помечена как deprecated; текущая рекомендуемая index-based версия — EVT_strong_process. В обеих процесс значений супремума — Коши.
Равномерный предел непрерывных функций непрерывен (uniform_limit_continuous_on).

На чём это стоит.

Топологическое лицо непрерывности — на чистой конструкции, без аксиом (Topology.v).
Теоремы о промежуточном значении и об экстремуме — на $L 3$ : classic приходит в IVT_ERR через архимедовость, в EVT_ERR и EVT_idx — напрямую. Это не изъян, а явный учёт уровня: classic — техническая Rocq-реализация закона исключённого третьего ToS.

Не построено в этой главе.

{ Теорема Кантора–Гейне над $Q$ — поточечная непрерывность на отрезке не влечёт равномерную; это математический факт, а не пробел, и причина — неполнота $Q$ .}
Сходимость процесса позиций максимума: над $Q$ argmax_process не обязан быть Коши — доказана сходимость лишь процесса значений.
{ Миграция теорем на головной файл: канонический головной файл теории непрерывности построен (analysis/Continuity.v: канон continuous_on, uniformly_continuous_on, Lipschitz_on и Липшицев мост), но существующие теоремы (IVT, EVT, HeineBorelComplete) на него ещё не переведены — каждая несёт своё локальное определение.}
Непрерывность функций на фактор-классах RealPoint — материал главы живёт на уровне функций $Q \to Q$ .

{

Готовит дальше. Равномерная непрерывность и липшицевость — рабочий аппарат для следующей главы Части V, о производной; теоремы о промежуточном значении и об экстремуме — инструменты, на которые обопрётся дифференциальное исчисление; обмен равномерного предела с интегралом и производной (остальная часть Uniform\- Convergence.v) — материал одной из последующих глав. }

Итог главы

Глава 5.3 прошла непрерывность от $δ$ - $ε$ определения до двух больших теорем анализа. Её главный урок — о двух лицах непрерывности. Над $Q$ поточечная и равномерная непрерывность не совпадают: теорема Кантора–Гейне, склеивающая их над $R$ , над $Q$ неверна — та же неполнота, что рушила Гейне–Бореля. Поэтому обе главные теоремы — о промежуточном значении и об экстремуме — честно несут в гипотезе именно равномерную непрерывность, и обе строят не классическую <<точку>>, а процесс: бисекцию, сходящуюся к перемене знака, и измельчающуюся сетку, чьи значения супремума образуют процесс Коши.

{Итог главы — в трёх частях. Первое: что построено. Топологическое лицо непрерывности над $Q$ — определение, алгебра непрерывных функций, теорема о прообразе — построено конструктивно, без аксиом, в рамках файла Topology.v. Равномерная непрерывность снабжена конструктивным мостом — липшицевость влечёт равномерную непрерывность — взамен недоказуемой над $Q$ теоремы Кантора–Гейне. Теорема о промежуточном значении доказана на трёх уровнях типизации, теорема об экстремуме — в двух версиях; равномерный предел непрерывных функций непрерывен.}

{Второе: на чём это стоит. Топологическое лицо непрерывности — на чистой конструкции. Теоремы о промежуточном значении и об экстремуме — на $L 3$ , законе исключённого третьего ToS. Техническая Rocq-аксиома classic — это реализация $L 3$ ; обращение к ней есть явный учёт уровня доказательства, а не отступление от строгости.}

{Третье: что остаётся открытым. Теорема Кантора–Гейне над $Q$ неверна — это математический факт. Процесс позиций максимума над $Q$ не обязан быть Коши — доказана сходимость лишь процесса значений. Канонический головной файл теории непрерывности построен (analysis/Continuity.v), но миграция на него существующих теорем (IVT, EVT) пока отложена. Глава дала непрерывность и две её теоремы; производная, что встанет на этом основании, — предмет следующей главы Части V.}

Часть: Часть V. Топология и анализ процессов · Том: «Математика»

Понятия: Логика · Формализация

Навигация: ← Глава 2. Топология и компактность · Глава 4. Производная →

E/R/R-разметка в шапке файла Topology.v; здесь разворачивается по образцу Части I. ↩
Эта ролевая разметка — из шапок ProcessIVT.v и ProcessEVT.v. ↩
Этот пример теперь и формально проверен. Для $f (x) = 1/ (x^{2} - 2)$ на $[1, 2] \cap Q$ машинно установлены обе стороны границы: поточечная непрерывность во всякой точке отрезка (cantor_heine_continuous) и отсутствие равномерной непрерывности (cantor_heine_not_uniform), — вместе они и означают, что теорема Кантора–Гейне над $Q$ неверна (cantor_heine_fails_Q). Подходящие к $2$ точки — это рациональные приближения по рекуррентности Пелля $x_{k} = p_{k} / q_{k}$ с точной ошибкой $∣ x_{k}^{2} - 2∣ = 1/ q_{k}^{2}$ , на которых $∣ f (x_{k}) ∣ = q_{k}^{2} \to \infty$ . Машинно проверено, 11 Qed, 0 аксиом. ↩

Путь Мудрости

Проводник

Глава 3. Непрерывность

От топологии к непрерывности

Что построили предыдущие главы

Два лица непрерывности

О статусе аксиом: техническое и онтологическое

Замысел главы

Непрерывность: топологическое лицо

Определение через δ{delta}-ε{epsilon}

Алгебра непрерывных функций

Прообраз открытого открыт

Разбор E/R/R: непрерывность как система

Равномерная непрерывность и граница Q{Равномерная непрерывность и граница Q}

Определение равномерной непрерывности

Кантора–Гейне над Q неверна

Конструктивная замена: липшицевость

Почему теоремы анализа требуют равномерной непрерывности

Теорема о промежуточном значении: бисекция

Замысел теоремы

Алгоритм бисекции

Ширина и свойство Коши

Слабый инвариант знака

Главная теорема

IVT на трёх уровнях

Один факт, три высоты типизации

Уровень процесса

Уровень типа: корень как CauchySeq

Зачем три уровня

Теорема об экстремуме: сетка

Замысел теоремы

Сетка

Значение против позиции

Главная теорема

EVT: argmax-версия, index-версия, обёртка

Две версии главного файла

Index-based решение

L5 и статус argmax

Process-обёртка

Равномерный предел, связь и итог главы

Равномерный предел непрерывных функций

Смежная заготовка: отображения процессов

Что построено и что готовится

Итог главы

Footnotes

Вид графа

Оглавление

Обратные ссылки

Определение через $δ$ {delta}- $ε$ {epsilon}

Равномерная непрерывность и граница $Q$ {Равномерная непрерывность и граница Q}