Глава 6. Основная теорема анализа

Основная теорема как процессная связь

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

Часть V строила анализ слой за слоем: расстояние, топология, непрерывность, производная, интеграл. Две последние главы дали два процесса. Глава 5.4 построила производную как процесс разностных отношений deriv_process и сеточную теорему о среднем через walk-точки. Глава 5.5 построила интеграл как процесс накопления Римановых сумм integral_process. Настоящая глава — та, где эти два процесса смыкаются. Основная теорема анализа связывает дифференцирование и интегрирование: интеграл производной восстанавливает приращение функции.

Связь готовилась заранее. Телескопическая сумма telescope_collapse, сворачивающая сумму приращений в разность концов, введена в § 5.5.1; сеточная форма теоремы ftc_grid названа в § 5.5.2 как мост. Здесь они становятся предметом, а не вспомогательным средством.

Классическая теорема и почему её нельзя взять прямо

Классическая основная теорема анализа двухчастна. Первая часть: если $F(x)={\int }_a^{x}f$, то $F^{\prime }=f$ — интегрирование с переменным верхним пределом обратно дифференцированию. Вторая часть: ${\int }_a^b{f}^{\prime }=f(b)-f(a)$ — интеграл производной равен приращению.

Перенести это в ToS прямо мешает не логика, а устройство текущего слоя. Классическую теорему нельзя просто импортировать как готовое утверждение о вещественной прямой: в текущем слое нет первичного завершённого $R$, нет функции-интеграла $F(x)={\int }_a^{x}f$ с переменным верхним пределом на фактор-классах, а сам интеграл представлен процессом Римановых сумм (§ 5.5). Поэтому классическую формулу приходится восстанавливать как сеточно-процессную связь, а не как равенство завершённых пределов. Это honest-граница, и мы называем её в самом начале главы: ниже строится не полная классическая двухчастная теорема, а её сеточная форма плюс точные частные случаи.

Сеточная форма: ftc_grid{ftc_grid}

{ Содержательное ядро главы — теорема ftc_grid из RiemannIntegration.v. Если функция $f$ равномерно дифференцируема на $[a,b]$ с производной $f^{\prime }$ (условие udiff_on из § 5.4), то для всякого $\epsilon >0$ найдётся уровень $N$, при котором Риманова сумма производной на сетке из $N+1$ подынтервалов приближает приращение:

$$|‘rieman{n}_{s}um‘f^{\prime }a‘step‘(N+1)-(f(y_{N+1})-f(a)\left)\right|\le \epsilon \cdot (b-a),$$

где $y_{N+1}=‘wal{k}_{p}oint‘a‘step‘(N+1)$ и $N+1$ соответствует S N в коде. Предельного деления на $h$ здесь нет: производная входит через division-free критерий udiff_on (§ 5.4). Сама сетка, конечно, использует безопасное рациональное деление при выборе шага $(b-a)/(SN)$ — знаменатель ненулевой, и это законное конечное деление, не запрещённый предельный переход. Форма сеточная. Доказательство собирается из двух лемм § 5.5.1: telescope_collapse отождествляет сумму приращений с разностью концов, а rs_tele_error_bound оценивает расстояние между Римановой суммой $f^{\prime }$ и этим телескопом. Именно здесь лежит доказательная сила всей главы.}

Стоит сразу назвать одну точность (Qeq-гигиена). Теорема сравнивает Риманову сумму с $f(y_{N+1})-f(a)$, где $y_{N+1}$ — последняя walk-точка, а не буквально с $f(b)-f(a)$. Лемма walk_endpoint_qeq даёт, что $y_{N+1}$ равна $b$ в смысле отношения Qeq; но чтобы перенести это под $f$ и прочесть $f(y_{N+1})$ как $f(b)$, функция $f$ должна уважать Qeq (быть Proper). Для произвольной $f:Q\to Q$ это требует отдельной оговорки. Ниже, читая ftc_grid как <<сумма $f^{\prime }$ приближает $f(b)-f(a)$>>, мы держим эту тонкость в уме.

Процессная обёртка: ftc_error_process{Процессная обёртка: ftc_error_process}

Над сеточной оценкой надстраивается процессный слой — файл ProcessFTC.v. Он определяет ошибку основной теоремы как процесс:

Definition ftc_error (f f' : Q -> Q) (a b : Q) (n : nat) : Q :=
  Qabs (integral_process f' a b n - (f b - f a)).
 
Definition ftc_error_process (f f' : Q -> Q) (a b : Q) : RealProcess :=
  fun n => integral_process f' a b n - (f b - f a).

На уровне $n$ это разность между Римановой суммой производной и приращением функции; ftc_error — её модуль. Теорема ftc_is_process_construction предъявляет этот процесс ошибки как конструкцию (E/R/R-форма).

Назовём статус честно (предохранители C1 и C4). Это процессная обёртка: определения ProcessFTC.v записывают ошибку основной теоремы в процессной форме, но сами по себе не доказывают, что эта ошибка убывает или образует процесс Коши. Содержательную оценку даёт ftc_grid из RiemannIntegration.v, а не ProcessFTC.v. Более того: хотя шапка ProcessFTC.v называет ftc_grid среди своих <<правил>>, в доказательствах самого файла ftc_grid не вызывается — файл строит процессную запись, а доказательная работа остаётся за RiemannIntegration.v. Мы это разводим прямо, чтобы не выдать обёртку за источник теоремы.

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

Основная теорема — не новая отдельная система, а связь двух уже разобранных: производной (Глава 5.4) и интеграла (Глава 5.5). Но и у этой связи есть E/R/R-устройство, и заголовки опорных файлов задают его прямо. FTC.v размечает объекты: $f$ — подынтегральное, $f^{\prime }$ — производная, $K$ — липшицева граница; правило — уравнение FTC (конституция), липшицева оценка (ограничение). ProcessFTC.v размечает процессы: элементы — производный и интегральный процессы; роль — мост между дифференцированием и интегрированием; правило — ftc_grid.¹ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе — та же, что в Главах 5.1–5.5: речь о функциях $Q\to Q$, не о фактор-классах; и теорема здесь — в сеточной форме, не классическая двухчастная (§ 6.1.2).

Rules — правила (закон $L5$). Конституция — само уравнение основной теоремы: интеграл производной восстанавливает приращение функции; в текущем слое оно записано сеточно (ftc_grid, § 6.2.3). К конституции примыкают условие равномерной дифференцируемости (udiff_on) и липшицева оценка как ограничение, контролирующее остаток (§ 6.3); доказательная опора — телескоп (§ 6.2.1). Честная граница: это сеточная, приближённая форма, точная лишь для аффинных функций (§ 6.3.2), — так что конституция здесь процессная, семейство оценок, а не одно завершённое равенство.

Roles — значимость позиций (закон $L4$). На уровне объектов теорема раздаёт роли: $f$ играет роль подынтегрального, $f^{\prime }$ — производной, $K$ — липшицевой границы (так размечает FTC.v). А на уровне процессов центральная роль самой теоремы одна — быть мостом между процессом-производной (§ 5.4) и процессом-интегралом (§ 5.5). По $L4$ эти роли обоснованы уравнением FTC: именно оно делает $f^{\prime }$ <<тем, что интегрируют, чтобы вернуть $f$>>.

Elements — носители (закон $L1$ и принцип $P4$). Элементы — функции, их производные и интегралы (Римановы суммы), а на процессном уровне — сами производный и интегральный процессы, связанные теоремой. По $L1$ каждый сохраняет тождество. По $P4$ оба суть процессы приближений, не завершённые пределы — и связь между ними тоже процессная: семейство сеточных оценок, уточняющихся с измельчением.

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

Компонент	Что фиксирует	E/R/R
функции, производные, интегралы; производный и интегральный процессы	носители	Element
$f\to$ подынтегральное, $f^{\prime }\to$ производная, $K\to$ граница; теорема как мост	роли	Role
уравнение FTC (ftc_grid, сеточное)	конституция	Rule
равномерная дифференцируемость, липшицева оценка	условие / ограничение	Rule
телескоп	доказательная опора	Rule
законы $L1$–$L5$	универсальный слой	Rule (универс.)

Хорошая сформированность. Основная теорема связывает две уже хорошо сформированные системы — производную и интеграл — без смешения категорий: $f$ остаётся элементом-подынтегральным, $f^{\prime }$ — его ролью-производной, уравнение FTC — правилом. Самореференции нет. Одно честное уточнение: громкая теорема derivative_integral_duality (§ 6.7.1) сама по себе скромна — настоящая связь держится не на ней, а на паре мостов (ftc_grid и deriv_process_converges), и именно эта пара хорошо сформирована.

Разбор замыкает E/R/R-нить Части V. Основная теорема — это правило, связывающее две двойственные системы: производную (процесс наклона, § 5.4) и интеграл (процесс площади, § 5.5). У обеих один ролевой узор — процесс, сходящийся к значению, — и FTC соединяет их так, что одно действие восстанавливается другим. Под $P4$ сама связь — процесс, а не завершённое тождество. Так аналитический слой Части V — метрика, топология, непрерывность, производная, интеграл — собирается в единое целое, и каждое его звено прочитано как система со своей E/R/R-структурой.

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

Дальше глава движется так. § 6.2 — сеточная теорема и телескоп (содержательное доказательство). § 6.3 — точные и регулярные случаи: аффинная функция точно, равномерно дифференцируемая приближённо. § 6.4 — следствия: оценка приращения, монотонность, разность. § 6.5 — правило произведения и интегрирование по частям (здесь, наконец, полный разбор приложений). § 6.6 — единственность первообразной и аффинная замена переменной. § 6.7 — двойственность производной и интеграла как процессов и мост к слабым производным. § 6.8 — итог.

Опорные файлы распределены так. Содержательные якоря — RiemannIntegration.v (ftc_grid, телескоп) и FTC.v (липшицевость, монотонность, аффинная подстановка). Приложения — IntegralApplications.v (правило произведения, интегрирование по частям, единственность первообразной). ProcessFTC.v — процессная обёртка. Оговорку о статусе аксиом глава даёт в § 6.8.

Сеточная теорема и телескоп

Телескоп: сумма приращений есть разность концов

{ Доказательство сеточной основной теоремы держится на телескопической сумме. Определим её как сумму приращений функции по последовательным узлам walk-сетки: $‘tel{e}_{s}um‘fa‘step‘n={\sum }_{k=0}^{n-1}[f(y_{k+1})-f(y_k)]$, где $y_k=‘wal{k}_{p}oint‘a‘step‘k$. Лемма telescope_collapse сворачивает её точно:

$$‘tel{e}_{s}um‘fa‘step‘n=f(y_n)-f(a).$$

Промежуточные значения сокращаются попарно, остаётся разность концов. Это конструктивное зерно основной теоремы: накопление приращений функции по сетке равно её полному изменению от $a$ до $y_n$. Совпадение лейбницево-точное, поскольку узлы заданы рекурсивной walk_point из § 5.4, а не замкнутой формулой — та же honest-деталь, что разбиралась в главе о производной.}

Оценка ошибки телескопа: rs_tele_error_bound{Оценка ошибки телескопа}

Второй кирпич связывает телескоп функции с Римановой суммой её производной. Лемма rs_tele_error_bound: при равномерной дифференцируемости udiff_on $f{f}^{\prime }ab$ для всякого $\epsilon >0$ найдётся уровень $N$, при котором

$$|‘rieman{n}_{s}um‘f^{\prime }a‘step‘(N+1)-‘tel{e}_{s}um‘fa‘step‘(N+1)|\le \epsilon \cdot (b-a).$$

Идея доказательства — внутренняя индукция по числу шагов сетки. На одном шаге Риманово слагаемое $f^{\prime }(y_k)\cdot ‘step‘$ отличается от приращения $f(y_{k+1})-f(y_k)$ ровно на ошибку линейного приближения производной, а та по равномерной дифференцируемости меньше $\epsilon \cdot ‘step‘$ (одношаговая оценка $|f(x+h)-f(x)-f^{\prime }(x)h|<\epsilon |h|$). Суммируя $k$ шагов, накапливаем $k\cdot \epsilon \cdot ‘step‘$; при $k=N+1$, где $(N+1)\cdot ‘step‘=b-a$, это даёт $\epsilon \cdot (b-a)$. Полный код — большая индукция; здесь важна схема: равномерность даёт оценку одного шага, сложение шагов — общую.

Сеточная теорема как итог

{ Сложив два кирпича, получаем ftc_grid. Телескоп равен разности концов (telescope_collapse), а Риманова сумма производной близка к телескопу (rs_tele_error_bound); значит, Риманова сумма производной близка к разности концов:

$$|‘rieman{n}_{s}um‘f^{\prime }a‘step‘(N+1)-(f(y_{N+1})-f(a)\left)\right|\le \epsilon \cdot (b-a).$$

Это центральная теорема § 6.2. Назовём её статус честно (предохранитель C1): форма division-free, сеточная, приближённая — это не точное равенство ${\int }_a^b{f}^{\prime }=f(b)-f(a)$. Там, где классический анализ ставит знак равенства, здесь стоит $\le \epsilon \cdot (b-a)$ при достаточно мелкой сетке.}

И снова Qeq-точность из § 6.1.3: в правой части стоит $f(y_{N+1})$, а не $f(b)$. Лемма walk_endpoint_qeq даёт $y_{N+1}=b$ в смысле Qeq; чтение $f(y_{N+1})$ как $f(b)$ корректно, когда $f$ уважает Qeq. Прозовое <<сумма $f^{\prime }$ приближает $f(b)-f(a)$>> держит эту оговорку в уме.

Почему это уже основная теорема

Может показаться, что <<приближённая>> теорема слабее классической. Но под $P4$ это не так. ftc_grid содержит всю суть основной теоремы: интеграл производной восстанавливает приращение функции. <<Приближённость>> здесь — не дефект, а сама природа объекта: завершённого предела не берётся, и процесс приближений есть теорема. Это та же интонация, что в § 5.4 с мостом deriv_process_converges: там процесс разностных отношений сходился к наклону, здесь процесс Римановых сумм производной сходится к приращению. Две главы — производная и интеграл — смыкаются, и смыкание тоже процессное. Двойственность дифференцирования и интегрирования (к ней вернётся § 6.7) живёт именно в этой паре мостов. В терминах разбора § 6.1.5 основная теорема и есть то правило, что связывает две двойственные системы — производную и интеграл.

Точные и регулярные случаи

Нулевая производная

Простейший случай основной теоремы — нулевая производная. Лемма ftc_zero_deriv утверждает: $‘integra{l}_{p}rocess‘({\lambda }_{.}0)abn=0$ поточечно на каждом уровне $n$. Интеграл нулевой производной есть нуль — точно, без приближения, доказывается прямой индукцией по числу узлов. Это согласуется с основной теоремой: если $f$ постоянна, то $f^{\prime }=0$, приращение $f(b)-f(a)=0$, и интеграл производной тоже нуль. Предохранитель C1: здесь результат точный, процесс тождественно нулевой.

Константная производная: точная теорема для аффинной функции

{ Следующий случай — постоянная производная, то есть аффинная функция. Лемма ftc_error_const — единственный нетривиальный содержательный факт файла ProcessFTC.v: для $f(x)=c\cdot x$ с производной $f^{\prime }=c$ процесс ошибки основной теоремы эквивалентен постоянному процессу нуль,

$$‘ft{c}_{e}rro{r}_{p}rocess‘(\lambda x.cx)({\lambda }_{.}c)ab\sim ‘cons{t}_{p}rocess‘0.$$

То есть ${\int }_a^{b}c=c(b-a)=f(b)-f(a)$ точно: ошибка тождественно нулевая на каждом уровне. Это точный процессный случай основной теоремы.}

{ Здесь нужно развести два близких результата (предохранитель C1). Точен именно ftc_error_const — процессный нуль для $f(x)=cx$. Лемма же ftc_affine из RiemannIntegration.v оформляет тот же аффинный сюжет в сеточной $\epsilon$-форме через ftc_grid (вида <<существует $N$, при котором ошибка $\le \epsilon (b-a)$>>), а не как отдельное точное равенство на каждом уровне. Ставить их в один ряд как <<точные>> было бы неверно: ftc_error_const точен, ftc_affine — $\epsilon$-оценка. (Третий родственник, ftc_const_deriv, переэкспортирует integral_process_const из § 5.5.) Содержательно: для прямой линии площадь под производной в точности равна приращению, и тот же факт виден в сеточной форме.}

Равномерно дифференцируемые: сеточная оценка

Для общих равномерно дифференцируемых функций основная теорема уже не точна, а сеточна: ftc_grid даёт ошибку $\le \epsilon (b-a)$, но не нуль. Граница между точным и приближённым проходит ровно по линейности. Аффинные функции — точно, потому что их приращение линейно по шагу и Риманова сумма ловит его без остатка. Нелинейные — приближённо, потому что появляется остаток высшего порядка (тот же сюжет, что с квадратом в § 5.4: ошибка линейного приближения была $h^2$). Чем мельче сетка, тем меньше этот остаток.

{ Сама сеточная оценка ftc_grid стоит на равномерной дифференцируемости (udiff_on), телескопе (telescope_collapse) и оценке rs_tele_error_bound — в дополнительной регулярности она не нуждается. Однако FTC.v надстраивает над ней регулярностный слой: леммы вроде udiff_implies_bounded (оценка значений функции через производную) и lipschitz_bounded (ограниченность липшицевой функции) помогают контролировать классы функций, на которых сеточные рассуждения применяются устойчиво, — это полезно для приложений § 6.4–6.5, а не для самой центральной оценки.}

Неотрицательность интеграла производной

Последний случай связывает основную теорему с порядком. Лемма ftc_nonneg_integral (RiemannIntegration.v): при $f^{\prime }\ge 0$ Риманова сумма производной неотрицательна с точностью до сеточной ошибки. Содержательно: неотрицательная производная даёт неубывающее приращение — если функция нигде не убывает по скорости, её значение не падает. Это сеточная FTC-форма мотива M4 из § 5.5 и мост к монотонности § 6.4: знак производной управляет ростом приращения.

Следствия основной теоремы

Оценка приращения

Первое следствие — оценка приращения через производную. Лемма ftc_increment_bound (FTC.v) есть по сути та же bounded_deriv_bounded_increment из теоремы о среднем § 5.4 §4.6: ограниченная производная даёт ограниченное приращение функции. Предохранитель C4: это та же лемма, что и в главе о производной, здесь прочитанная в контексте основной теоремы. Связь прямая — сеточная теорема о среднем была одной из предтеч ftc_grid, и оценка приращения переносится без изменений.

Монотонность из знака производной

{ Второе следствие — монотонность. Лемма ftc_monotone: при $f^{\prime }\ge 0$ функция растёт на сетке (приращение неотрицательно); ftc_strict_monotone (то же, что pos_deriv_increases из § 5.4) даёт строгий рост при производной, отделённой от нуля. Основная теорема превращает локальное свойство <<производная положительна>> в глобальное <<функция растёт>>: знак производной управляет ростом накопленного приращения. Это сеточные результаты, как и всё в § 6.2–6.4.}

Разность и линейность приращений

Третье следствие — линейность. Лемма ftc_difference даёт приращение разности функций, ftc_sum_rule (она же ftc_linearity) и ftc_scale_rule (через udiff_scale) — приращения суммы и скалярного кратного. Основная теорема уважает линейные операции: приращение суммы есть сумма приращений, в полном согласии с линейностью интеграла § 5.5.3 и производной § 5.4.2. Это не новость, а проявление того, что обе операции анализа линейны, и связь между ними линейность сохраняет.

Абсолютная оценка

Четвёртое следствие — абсолютная оценка. Лемма ftc_absolute_value_bound (FTC.v): при $|f^{\prime }|\le M$ Риманова сумма производной не превосходит $M\cdot (b-a)$ по модулю. Это FTC-форма оценки § 5.4.4, теперь применённая к производной. Она понадобится в § 6.5: в правиле произведения и интегрировании по частям множители придётся ограничивать, и эта лемма даёт нужный контроль.

Правило произведения и интегрирование по частям

Правило произведения для равномерной дифференцируемости

{ Главное нелинейное приложение основной теоремы — правило произведения, лемма udiff_product из IntegralApplications.v. Если $f$ и $g$ равномерно дифференцируемы на отрезке с ограниченными значениями и производными, то их произведение $f\cdot g$ равномерно дифференцируемо с производной

$$(f\cdot g{)}^{\prime }=f^{\prime }g+f{g}^{\prime }.$$

Доказательство приведём идеей в три шага. Во-первых, product_decomp раскладывает приращение произведения на три слагаемых — по образцу разложения из правила производной § 5.4 §4.4.2. Во-вторых, каждое слагаемое оценивается долей $\epsilon /3$. В-третьих, множители контролируются ограничениями $M_f,M_g,M_{f^{\prime }},M_{g^{\prime }}$ на значения и производные. Сумма трёх оценок по $\epsilon /3$ даёт требуемое. Это полная теорема (предохранитель C1), прямая равномерная версия правила произведения производной — но на отрезке, как нужно для интегрирования. Частный случай — udiff_square: производная квадрата $(f^2{)}^{\prime }=2f{f}^{\prime }$.}

Основная теорема для произведения

Применив ftc_grid к производной произведения, получаем лемму ftc_product: Риманова сумма выражения $f^{\prime }g+f{g}^{\prime }$ приближает приращение произведения $fg$. Это прямое следствие правила произведения и сеточной теоремы: коль скоро $(fg{)}^{\prime }=f^{\prime }g+f{g}^{\prime }$, интеграл правой части восстанавливает приращение $fg$. Лемма — мост к интегрированию по частям.

Интегрирование по частям

{ Перегруппировав ftc_product, получаем интегрирование по частям — лемму integration_by_parts. В сеточной форме она утверждает: Риманова сумма $f^{\prime }g$ приближает граничный член $fg$ минус Риманова сумма $f{g}^{\prime }$,

$$|‘RS‘(f^{\prime }g)-(f(\text{конец})g(\text{конец})-f(a)g(a))+‘RS‘(f{g}^{\prime })|\le \epsilon \cdot (b-a).$$

Доказательство — ftc_product плюс линейность Римановых сумм (riemann_sum_add, riemann_sum_sub). Предохранитель C1: это $\epsilon$-grid-форма, не точное равенство. Частные случаи: ibp_self даёт $2\int f^{\prime }f\approx f(\text{конец}{)}^2-f(a{)}^2$, а ibp_identity — формулу с тождественным множителем, $\int g\approx xg{|}_a^b-\int x{g}^{\prime }$.}

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

Геометрический и операционный смысл интегрирования по частям стоит назвать прямо. Формула перераспределяет производную между множителями: производную можно перенести с одной функции на другую — ценой граничного члена $fg{|}_a^b$. Это прямое следствие правила произведения, проинтегрированного по отрезку: раз приращение произведения распадается на два вклада $f^{\prime }g$ и $f{g}^{\prime }$, то, зная приращение произведения и один из интегралов, восстанавливаем другой. Перенос производости с множителя на множитель — ровно тот приём, который в анализе функций многих переменных станет определением слабой производной; к этому мосту глава вернётся в § 6.7.

Единственность первообразной и замена переменной

Единственность первообразной

{ Ещё одно классическое следствие — единственность первообразной. Лемма antiderivative_unique из IntegralApplications.v: если функции $f$ и $g$ имеют на $[a,b]$ одну и ту же производную $h$, то их приращения совпадают (с точностью до сеточной ошибки $\epsilon (b-a)$). Доказательство опирается на udiff_sub: разность $f-g$ имеет нулевую производную, а тогда ftc_grid с нулевой производной даёт малое приращение разности. Содержательно это сеточная форма утверждения <<первообразная определена с точностью до константы>>: две первообразные одной функции отличаются на нечто с нулевой производной, то есть почти постоянное. Прямая параллель с zero_deriv_near_constant из § 5.4 §4.7: нулевая производная влечёт почти-постоянство.}

Замена переменной: только аффинный случай

Замена переменной формализована лишь частично, и это надо назвать честно (предохранители C1 и C4). Общего цепного правила в ядре нет, как уже отмечалось в § 5.4 и § 5.5. Есть только аффинный случай: udiff_chain_affine (FTC.v) — цепное правило для внутренней функции $g=c\cdot x+d$ при $c>0$, и udiff_chain_affine_neg при $c<0$. На них построена аффинная замена переменной в интеграле ftc_u_substitution_affine. То есть подстановка $u=g(x)$ доказана лишь для линейной $g$; общая замена с произвольной гладкой $g$ не формализована. Граница очерчена конкретно.

Липшицевость и равномерная непрерывность

{ Регулярность, на которой стоят FTC-оценки, образует иерархию, но называть её надо аккуратно. Строгий мост есть один: lipschitz_uniform_cont (FTC.v) доказывает, что липшицева функция равномерно непрерывна. Понятия Lipschitz_on и uniformly_continuous_on определены здесь же.}

{ Дальше следует быть осторожным. Отдельной теоремы вида << udiff_on $\Rightarrow$ Lipschitz_on >> в стандартной форме файл не содержит, и подавать иерархию как готовую цепочку не стоит. Что есть точно: lipschitz_bounded — ограниченность функции, если она уже липшицева; udiff_implies_bounded — оценка значений через слой теоремы о среднем. Для равномерно дифференцируемых функций есть сеточные и MVT-оценки приращений (например, bounded_deriv_bounded_increment из § 5.4 и родственные), но это не одна простая теорема <<равномерно дифференцируема, значит липшицева>>. Связь с § 5.3, где липшицевость вводилась как условие, и с § 5.4, где из ограниченной производной выводились MVT-оценки приращений, близкие к липшицевым, держится именно на этих конкретных леммах, а не на единой импликации.}

Двойственность производной и интеграла. Мост к слабым производным

Производная и интеграл как двойственные процессы

В ProcessFTC.v двойственность производной и интеграла заявлена теоремой с громким именем derivative_integral_duality. Назовём её содержание честно (предохранитель C1). Теорема утверждает для $a<b$ две вещи: во-первых, существует процесс, и при has_derivative $fx(f^{\prime }x)$ производная-процесс есть Коши (через deriv_process_cauchy); во-вторых, существует integral_process $f^{\prime }ab$.

Имя <<двойственность>> звучит сильнее, чем формальное содержание. В коде первый процесс proc_d — фиктивный (буквально ${\lambda }_{.}0$, с авторским комментарием <>); реальное содержание — переэкспорт deriv_process_cauchy из § 5.4 плюс тривиальное существование integral_process. Это не доказательство двойственности $d/dx$ и $\int$ как операций; это утверждение, что оба процесса существуют и производная-процесс есть Коши при наличии производной. Назвать следует именно так — конъюнкция существований, а не теорема дуальности.

В каком смысле двойственность реальна

Сказанное не означает, что двойственности нет — означает лишь, что она держится не на теореме с громким именем, а на двух отдельных мостах, доказанных по-настоящему. Первый мост — ftc_grid этой главы: интеграл производной восстанавливает приращение функции. Второй — deriv_process_converges из § 5.4: производная-процесс сходится к наклону. Вместе они и составляют содержательную двойственность дифференцирования и интегрирования: одно действие восстанавливается другим, на уровне процессов. Честно развести стоит так: громкое имя derivative_integral_duality само по себе скромно, а настоящая двойственность — в паре ftc_grid и deriv_process_converges.

Интервальное разбиение

Лемма ftc_interval_split (ProcessFTC.v) утверждает, что для $a<m<b$ существуют процессы на $[a,m]$ и $[m,b]$, поточечно равные integral_process. Назовём её статус прямо (предохранитель C1): это не аддитивность интеграла по интервалу ${\int }_a^b={\int }_a^m+{\int }_m^b$. Доказательство — предъявление двух процессов и reflexivity; лемма утверждает лишь существование под-процессов на подотрезках, но не равенство интеграла их сумме. Полная аддитивность по интервалу потребовала бы отдельной теоремы, которой в опорных файлах нет. Это честная граница, и имя леммы не следует читать как больше, чем она доказывает.

Мост к слабым производным

Интегрирование по частям § 6.5 открывает дверь в анализ, выходящий за пределы этой главы, — и стоит назвать эту дверь, ясно пометив, что сама она здесь не строится. Формула ИБП переносит производную с одной функции на другую ценой граничного члена. Если граничный член обнулить (взять пробные функции, исчезающие на концах), получится чистый перенос: $\int f^{\prime }\phi =-\int f{\phi }^{\prime }$. Это равенство и берут за определение слабой (обобщённой) производной — производной, заданной не поточечно, а через действие на пробные функции. Слабые производные — входная точка пространств Соболева и современной теории уравнений в частных производных.

Подчеркнём предельно ясно: в опорных файлах этой главы слабых производных и пространств Соболева нет. Интегрирование по частям показывает лишь формальный паттерн, который для них нужен — перенос производности с граничным членом. Сами эти понятия — мотивационная программа будущих частей тома, а не доказанное содержание FTC.v или IntegralApplications.v. Мы называем направление, не приписывая репозиторию того, чего в нём пока нет. В терминах разбора § 6.1.5 интегрирование по частям — правило (Rule), переносящее производность; оно лишь намечает паттерн слабых производных, не строя их.

Что построено и что готовится. Итог главы

Итог в трёх столбцах

Соберём сделанное в режиме инфраструктуры.

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

• сеточная основная теорема ftc_grid (Риманова сумма $f^{\prime }$ приближает приращение $f$ при udiff_on) — содержательное ядро; телескоп и rs_tele_error_bound;
• точный процессный случай для аффинной функции (ftc_error_const); нулевая производная (ftc_zero_deriv); аффинная $\epsilon$-форма (ftc_affine);
• процессная обёртка ftc_error_process, ftc_is_process_construction;
• следствия: оценка приращения, монотонность, разность, абсолютная оценка;
• правило произведения udiff_product, интегрирование по частям integration_by_parts, ibp_self и ibp_identity, единственность первообразной antiderivative_unique;
• аффинная замена переменной ftc_u_substitution_affine;
• липшицевость влечёт равномерную непрерывность (lipschitz_uniform_cont).

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

• классическая двухчастная теорема ($F(x)={\int }_a^{x}f$, $F^{\prime }=f$) в общем виде — доказана сеточная форма плюс точный аффинный случай; двухчастная формулировка — содержательное чтение, не теорема;
• основная теорема для функций на классах RealPoint — здесь только $Q$-функции (предохранитель C2);
• общее цепное правило и общая замена переменной — только аффинный случай;
• аддитивность интеграла по интервалу как теорема (ftc_interval_split — лишь существование под-процессов);
• слабые производные и пространства Соболева — мотивационная программа будущих частей, не содержание опорных файлов.

Готовит дальше:

• Фубини (глава 5.7): 2D step-функции, перестановка двойного процесса;
• слабые производные и Соболев — через интегрирование по частям;
• меру (Часть VI): на фундаменте step-интеграла § 5.5.

Что осталось бы для классической двухчастной теоремы

Глава доказала сеточную форму; назовём конкретно, чего не хватает до классической двухчастной теоремы — так же, как § 5.8 называла недостающее для интеграла на классах. Понадобилось бы, во-первых, определить функцию-интеграл с переменным верхним пределом $F(x)={\int }_a^{x}f$ как процесс и доказать первую часть теоремы $F^{\prime }=f$ — в опорных файлах этого нет. Во-вторых, точное равенство (а не сеточная оценка) потребовало бы перехода к фактор-классам RealPoint и доказательства корректности относительно эквивалентности. Заголовок здесь — <<классическая двухчастная>>, а не <<полная>>: для своей сеточно-процессной задачи глава полна, недостающее — именно классическая надстройка.

Оговорка о статусе аксиом

{ Предохранитель Части V требует точности об аксиомах. Ядра — RiemannIntegration.v, FTC.v, IntegralApplications.v — в шапках заявляют << none >> или << 0 axioms >>; ProcessFTC.v — << 8 Qed, 0 axioms >>. Но некоторые из этих файлов импортируют слои, где встречается классическая логика: например, EVT_idx.v с локальным classic или ProcessArithmetic.v, где classic используется в monotone_bounded_Cauchy. Сами Differentiation.v и MeanValueTheorem.v в шапках заявляют отсутствие аксиом. Огульно говорить <<все тянут classic>> не следует: импорт сам по себе не означает, что каждая лемма зависит от classic — статус конкретной теоремы устанавливается только командой Print Assumptions для неё самой.}

Print Assumptions выписан в финале RiemannIntegration.v (для ftc_grid и других) и FTC.v (для lipschitz_uniform_cont, ftc_u_substitution_affine и других); у ProcessFTC.v и IntegralApplications.v финального блока нет — для нужной теоремы его запускают отдельно. И honest-факты для полноты картины: ftc_grid назван в шапке ProcessFTC.v среди правил, но в доказательствах файла не вызывается; теорема derivative_integral_duality содержит фиктивный процесс; ftc_interval_split не есть аддитивность; многие леммы ProcessFTC.v — переэкспорты уже доказанного.

Итог главы

Глава связала производную и интеграл — два процесса, построенные в § 5.4 и § 5.5. Главный поворот в том, чем оказалась сама связь. Под $P4$ основная теорема анализа — не одна завершённая предельная идентичность ${\int }_a^b{f}^{\prime }=f(b)-f(a)$, а процессная связь: семейство приближений, в котором на каждом уровне сетки Риманова сумма производной приближает приращение функции, а точность растёт с измельчением. Содержательное ядро — division-free сеточная оценка ftc_grid; для аффинных функций связь точна, для общих равномерно дифференцируемых функций — сеточно-приближённа, и приближение контролируется именно оценкой ftc_grid. Главная осторожность: это не полная классическая двухчастная теорема, громкие имена названы честно, а слабые производные оставлены будущим частям как программа.

Построено: сеточная основная теорема ftc_grid через телескоп; точный аффинный случай; следствия (монотонность, оценки приращения); правило произведения, интегрирование по частям, единственность первообразной; аффинная замена переменной.

На чём стоит: на телескопе и равномерной дифференцируемости § 5.4–5.5, на сеточной онтологии $P4$, в которой связь производной и интеграла — не завершённое равенство, а процесс приближений; настоящая двойственность держится на паре мостов ftc_grid и deriv_process_converges.

Дальше: Фубини для 2D step-функций (глава 5.7); слабые производные и Соболев через интегрирование по частям; общая мера на фундаменте step-интеграла (Часть VI).

---

---

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

Навигация: ← Глава 5. Интеграл · Глава 7. Теорема Фубини на процессах →

Footnotes

1. E/R/R-разметка в шапках файлов FTC.v (объекты) и ProcessFTC.v (процессы); здесь разворачивается по образцу Части I. ↩