Глава 5. Интеграл

Интеграл как процесс накопления

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

Часть V строит анализ слой за слоем. Глава 5.1 ввела расстояние, 5.2 — топологию и компактность, 5.3 — непрерывность, 5.4 — производную: division-free критерий $o(h)$, производную-процесс deriv_process и сеточную теорему о среднем через walk-точки. Интеграл — следующий слой, и он двойственен производной: там мы измеряли скорость изменения, здесь измеряем накопленную величину — площадь под графиком.

Связь с предыдущей главой прямая и техническая. Риманова сумма, которой строится интеграл, определена на тех же walk-точках, что и теорема о среднем § 5.4: сетка $x,x+s,x+2s,\dots$ задаёт узлы, в которых берутся значения функции. То есть глава об интеграле встаёт прямо на сетке, построенной главой о производной. А равномерная дифференцируемость udiff_on из § 5.4 окажется именно тем условием, при котором суммы производной сходятся к приращению функции.

Площадь и предел как проблема

Классически интеграл — предел Римановых сумм при измельчении разбиения:

$${\int }_a^{b}f=\underset{\text{разбиение}\to 0}{\lim }\sum _{i}f(x_i)\Delta x_i.$$

Как и с производной, стоит точно понять, что здесь составляет трудность, а что нет.

Не составляет трудности конечная Риманова сумма. Если сетка фиксирована — скажем, $n$ равных отрезков, — то ${\sum }_{i}f(x_i)\Delta x_i$ есть конечная сумма произведений рациональных чисел, то есть рациональное число, вычисляемое точно. Никакого предела для неё не нужно.

Трудность — в пределе. Во-первых, $\lim$ при измельчении — завершённый объект, а завершённых пределов под $P4$ нет. Во-вторых, <<разбиение как угодно мелкое>> отсылает к потенциальной бесконечности уровней измельчения. Нужна формулировка, в которой предел сумм не стоит на месте первичного определения — ровно как с производной, где предел частного не был первичным.

Конечная Риманова сумма на сетке

Первый слой интеграла — конечная сумма. На равномерной сетке walk-точек с шагом step левая Риманова сумма определяется рекурсией по числу узлов:

Fixpoint riemann_sum (f : Q -> Q) (a step : Q) (n : nat) : Q :=
  match n with
  | O => 0
  | S n' => f (walk_point a step n') * step + riemann_sum f a step n'
  end.

То есть $‘rieman{n}_{s}um‘fa‘step‘n={\sum }_{k=0}^{n-1}f(‘wal{k}_{p}oint‘a‘step‘k)\cdot ‘step‘$ — сумма площадей $n$ прямоугольников высоты $f$ в узле и ширины step. На каждом фиксированном $n$ это рациональное число, точное, без всякого приближения.

{ Отметим уровень типа (предохранитель Части V): $f:Q\to Q$, а сумма есть рациональное число. И сразу — предупреждение об именах (предохранитель C4). В репозитории есть три разных определения с именем riemann_sum: это, основное, из RiemannIntegration.v (левая сумма по walk_point); отдельное riemann_sum_01 на отрезке $[0,1]$ в ProcessIntegration.v; и ещё одно, демонстрационное, в ProcessAnalysis.v. Имена совпадают, определения различны; ниже под riemann_sum мы всегда понимаем первое, а к остальным двум обратимся отдельно в § 5.7, всякий раз называя файл.}

Интеграл-процесс: integral_process{Интеграл-процесс: integral_process}

Второй слой — процесс. Чтобы получить интеграл, конечную сумму надо измельчать. Зафиксируем последовательность всё более мелких сеток: на уровне $n$ берём $n+1$ подынтервалов с шагом

$$‘integra{l}_{s}tep‘abn=\frac{b-a}{n+1}$$

и считаем Риманову сумму на этой сетке. Получаем процесс — на уровне $n$ рациональное число:

Definition integral_step (a b : Q) (n : nat) : Q :=
  (b - a) / inject_Z (Z.of_nat (S n)).
 
Definition integral_process (f : Q -> Q) (a b : Q) : RealProcess :=
  fun n => riemann_sum f a (integral_step a b n) (S n).

Под $P4$ интеграл мыслится не как предел этого процесса, а как сам процесс рациональных приближений площади — ровно как в § 5.4 производная была процессом приближений наклона. Шаг положителен при $a<b$ (integral_step_pos), а измельчение работает: integral_step_vanishes утверждает, что для всякого $\delta >0$ найдётся уровень $N$ с шагом меньше $\delta$ (через архимедову лемму nat_above_Q из § 5.4). Тип процесса — RealProcess, то есть $N\to Q$.

Здесь нужен тот же предохранитель, что и для производной-про-цес-са в § 5.4. Процесс integral_process $fab$ определён для любой функции $f:Q\to Q$ — но само его существование ещё не делает $f$ интегрируемой. integral_process — это канонический кандидат, представитель интеграла; его аналитическая законность требует, чтобы процесс сумм сходился (обладал свойством Коши). Для констант это видно сразу (§ 5.2.1); для более широких классов функций свойство Коши собирается из сеточных оценок и grid-формы основной теоремы (§ 5.5). Теорема integral_is_process_construction, предъявляющая процесс сумм как конструкцию, — это не теорема интегрируемости, и выдавать одно за другое не следует.

Разбор E/R/R: интеграл как система

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

Rules — правила (закон $L5$). Конституция интеграла — накопление: Риманова сумма на walk-сетке (§ 5.1.3) плюс измельчение (integral_process, § 5.1.4). К ней примыкает конкретный слой — линейность (§ 5.3), монотонность и неотрицательность (мотив M4, § 5.4): именно эти порядковые правила делают интеграл фундаментом меры. Законность процесса как интеграла даёт ещё одно правило-условие — интегрируемость как свойство Коши процесса сумм (через grid-FTC, § 5.5). Честная граница: отдельного предиката интегрируемости в ядре нет, свойство Коши собирается из сеточных оценок для конкретного класса функций (§ 5.5.3).

Roles — значимость позиций (закон $L4$). Центральная роль — накопленная величина, площадь под графиком, которую интегрирование присваивает функции на отрезке. Вычислительную сторону роли несёт процесс Римановых сумм — Cauchy-процесс, сходящийся к значению интеграла (так роль и названа в заголовке файла). В точной step-линии та же роль выступает как интегрирование и $L^1$-норма (§ 5.2.3). По $L4$ роль обоснована: площадь структурно задана суммой значений с весами-ширинами, а не извне.

Elements — носители (закон $L1$ и принцип $P4$). Элементы — подынтегральные функции $Q\to Q$ и частичные Римановы суммы $‘RS{‘}_n$ (а в step-линии — записи Step). По $L1$ каждая сумма тождественна себе. По $P4$ носители конечны на каждом уровне: $‘RS{‘}_n$ — конечная сумма рациональных, точная и обозримая; завершённого предела сумм нет, интеграл актуален как процесс накопления.

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

Компонент	Что фиксирует	E/R/R
функции $Q\to Q$; суммы $‘RS{‘}_n$; Step-записи	носители	Element
площадь; процесс, сходящийся к значению интеграла	роли	Role
Риманова сумма на сетке $+$ измельчение	конституция-накопление	Rule (конструкт.)
линейность, монотонность, неотрицательность (M4)	порядковые правила	Rule (конструкт.)
интегрируемость $=$ свойство Коши (grid-FTC)	условие законности	Rule
законы $L1$–$L5$	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: функции и суммы суть элементы, площадь — роль, накопление и порядковые законы — правила. Самореференции нет: сумма работает над значениями функции и стоит выше них — по $L5$ операция выше операндов. Две конструкции — точная step-линия и процесс Римановых сумм — не спорят, а суть два согласованных представления одной роли-интеграла (§ 5.2.5). Интеграл хорошо сформирован.

Разбор проясняет место интеграла в Части V. Он двойствен производной (§ 5.4): у обеих систем один ролевой узор — процесс, сходящийся к значению (наклон там, площадь здесь), — и дуальные правила (дифференцирование против накопления); основная теорема (глава 5.6) свяжет два процесса в один. Мотив M4 — неотрицательность — это то правило, которым интеграл становится положительным функционалом, фундаментом меры (Часть VI). А две конструкции, точная и процессная, суть два интенсиональных представления одного интеграла — та же кратность представлений ($P3$), что у трёх уровней теоремы о промежуточном значении в Главе 5.3. И тот же разбор задаёт образец Части V: каждое аналитическое понятие читается как система со своей E/R/R-структурой.

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

Дальше глава движется так. § 5.2 — интеграл простых функций: константа, ширина сетки, точные step-функции. § 5.3 — линейность. § 5.4 — монотонность и неотрицательность (мотив M4). § 5.5 — оценки и сходимость: интегрируемость как свойство Коши процесса сумм. § 5.6 — граница главы: что интеграл готовит для основной теоремы анализа (telescope, grid-FTC как мост, краткий обзор правил, которые развернёт глава 5.6). § 5.7 — вычислительные примеры. § 5.8 — итог.

{ Опорных файлов два якоря: RiemannIntegration.v — ядро конечных Римановых сумм, и ProcessIntegral.v — процесс из этих сумм. Дополнительные слои: StepIntegral.v (точный интеграл кусочно-постоянных) и демонстрационные файлы примеров; IntegralApplications.v с правилами интеграла мы лишь назовём в § 5.6, оставив разбор главе 5.6. Оговорку о статусе аксиом — с важным случаем ProcessArithmetic.v, где заголовок расходится с фактом, — глава даёт в § 5.8.}

Интеграл простых функций

Интеграл константы

Проверим определение на простейшем случае — постоянной функции. Формально лемма integral_process_const утверждает эквивалентность процессов:

$$‘integra{l}_{p}rocess‘({\lambda }_{.}c)ab\sim ‘cons{t}_{p}rocess‘(c\cdot (b-a)),$$

то есть процесс интеграла константы $c$ эквивалентен постоянному процессу со значением $c\cdot (b-a)$. Стоит назвать точно: результат выражен через эквивалентность процессов (process_equiv), хотя доказательство показывает даже поточечно нулевой зазор на каждом уровне. В самом деле, на уровне $n$ Риманова сумма константы есть $c\cdot (n+1)\cdot ‘step‘$ (по riemann_sum_const), а произведение $(n+1)\cdot ‘step‘$ равно в точности $b-a$ (по grid_width_eq); поэтому разность с $c\cdot (b-a)$ равна нулю при каждом $n$, а не только в пределе.

Содержательно это привычная площадь под горизонталью: высота $c$ на ширину $b-a$, точно и сразу. И это единственный класс, где интегрируемость в смысле § 5.1.4 видна немедленно — без всяких сеточных оценок: процесс уже постоянен.

Ширина сетки

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

$$‘rieman{n}_{s}um‘({\lambda }_{.}1)a‘step‘n=n\cdot ‘step‘$$

(лемма riemann_sum_width), а на сетке из $n+1$ подынтервалов с шагом $(b-a)/(n+1)$ это даёт $b-a$ ровно (grid_width_eq). То есть суммарная ширина сетки точно равна длине отрезка независимо от уровня измельчения. Это <<нормировка>>, на которой потом держатся все оценки § 5.4 и § 5.5: сколько бы прямоугольников мы ни взяли, их общая ширина одна и та же.

Точный интеграл кусочно-постоянных: step-функции

Есть и совсем другая конструкция интеграла, не требующая ни сетки, ни измельчения, — интеграл кусочно-постоянных функций. Она живёт в файле StepIntegral.v. Step-функция — это конечная сумма $f={\sum }_i{c}_i\cdot {\chi }_{[a_i,b_i]}$; в коде её элемент задаётся записью с полем-значением и двумя концами:

Record Step := mkStep {
  step_val : Q;
  step_left : Q;
  step_right : Q;
  step_valid : step_left <= step_right
}.
 
Definition step_integral (s : Step) : Q :=
  step_val s * (step_right s - step_left s).

Интеграл step-функции step_fun_integral — сумма ${\sum }_i{c}_i(b_i-a_i)$ по конечному списку ступеней. Это точное рациональное число, без всякого предела и измельчения: конечная сумма по конечному списку. Примеры из файла прямые: интеграл константы $c$ на отрезке есть $c$ (integral_constant); интеграл индикатора ${\chi }_{[0,1/2]}$ есть $1/2$; интеграл функции <<$2$ на $[0,1/2]$ и $3$ на $[1/2,1]$>> есть $5/2$ (integral_two_step).

Назовём роль точно (предохранители C1 и C4). Это точная конструкция, не процесс и не сеточный предел; и она использует свою запись Step, отдельную от Римановых сумм, — параллельная линия. Шапка файла называет её <<P4-совместимой теорией меры: интегрирование первично, мера производна>> и <<фундаментом меры Бишопа–Ченга>>. Говорить об этом стоит как о мосте, не как о построенной мере: step-функции — фундамент будущей меры, интегрирование кусочно-постоянных уже построено, но сама общая мера и $L^1$-пополнение — предмет следующих частей. Здесь мы лишь отмечаем точную линию и не смешиваем её с процессом.

Две конструкции интеграла

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

Связь между ними проста и поучительна. Риманова сумма на уровне $n$ — это в точности интеграл step-функции, аппроксимирующей $f$ на сетке: каждый прямоугольник суммы есть ступенька постоянной высоты. То есть процесс integral_process есть последовательность точных интегралов step-приближений функции $f$, всё более частых. Точная линия и процессная линия — не соперники, а две стороны одного: на каждом уровне процесс есть точный step-интеграл, а сам интеграл $f$ — процесс этих точных значений. В разборе § 5.1.5 это два представления одной роли-интеграла: точное (step) и процессное (Римановы суммы).

Оговоримся о статусе этой связи (honest-замечание). В репозитории она изложена как математическое чтение, а не как доказанная лемма: отдельной теоремы, отождествляющей riemann_sum со step_fun_integral специально построенной step-функции, в опорных файлах главы нет, и StepIntegral.v с RiemannIntegration.v существуют как две параллельные линии (одна над списками Step, другая над walk_point-сет-ка-ми). Такая лемма была бы естественным будущим мостом между ними. К сходимости процесса сумм мы вернёмся в § 5.5.

Линейность интеграла

Аддитивность и скаляр

Первое содержательное свойство интеграла — линейность. На уровне конечной Римановой суммы это два тождества, верных на каждой сетке. Сумма функций даёт сумму сумм:

$$‘rieman{n}_{s}um‘(\lambda x.fx+gx)a‘step‘n=‘rieman{n}_{s}um‘fa‘step‘n+‘rieman{n}_{s}um‘ga‘step‘n$$

(лемма riemann_sum_add); скалярное кратное выносится: $‘rieman{n}_{s}um‘(\lambda x.c\cdot fx)=c\cdot ‘rieman{n}_{s}um‘f$ (лемма riemann_sum_scale). Оба доказываются короткой индукцией по числу узлов: на каждом шаге работает кольцевое тождество для рациональных чисел.

На уровне процесса эти тождества поднимаются дословно: integral_process_add и integral_process_scale дают аддитивность и однородность поточечно на каждом уровне, а integral_linearity_process соединяет их в одно: $\int (c\cdot f+g)=c\cdot \int f+\int g$. Предохранитель C1: на конечной сумме это точное тождество, на процессе — поточечное равенство на каждом уровне. Содержательно интеграл линеен по той же причине, по которой линейна сумма: Риманова сумма есть линейная комбинация значений функции с весами-ширинами.

Разность

{ Разность выводится из суммы и скаляра, а не доказывается заново. Лемма riemann_sum_negate_fn даёт $‘RS‘(-f)=-‘RS‘(f)$, а riemann_sum_sub — $‘RS‘(f-g)=‘RS‘(f)-‘RS‘(g)$. Обе получаются переписыванием через riemann_sum_ext — лемму об экстенсиональности: если $f$ и $g$ совпадают в узлах сетки, их Римановы суммы равны. Это та же экономия средств, что с правилом разности производной в § 5.4: каждое следующее тождество встаёт поверх уже доказанных. Предохранитель C4 об источниках: riemann_sum_sub и riemann_sum_negate_fn относятся к FTC-слою репозитория — файлу analysis/FTC.v; лемма об экстенсиональности riemann_sum_ext живёт в IntegralApplications.v. Для главы важно содержательно: разность выводится из аддитивности и масштабирования, а не доказывается заново.}

Что значит линейность интеграла

Линейность — не случайность, а отражение того, что Риманова сумма есть линейная комбинация значений подынтегральной функции. И она двойственна линейности производной из § 5.4: дифференцирование переводило линейные операции над функциями в линейные операции над наклонами, интегрирование — в линейные операции над площадями. Обе операции анализа линейны, и основная теорема (глава 5.6) свяжет их в одно. Пока же это первый мост вперёд: то, что интеграл и производная ведут себя одинаково по отношению к сложению и скаляру, — не совпадение, а признак их грядущего родства. В терминах § 5.1.5 это E/R/R-двойственность: интеграл и производная делят ролевой узор (процесс, сходящийся к значению) при дуальных правилах.

Монотонность и неотрицательность

Монотонность

{ Интеграл сохраняет порядок. Лемма riemann_sum_monotone утверждает: если $f\le g$ во всех узлах сетки и шаг неотрицателен, то $‘rieman{n}_{s}um‘f\le ‘rieman{n}_{s}um‘g$. На уровне процесса это integral_monotone: из $f\le g$ на сетке следует $‘integra{l}_{p}rocess‘f\le ‘integra{l}_{p}rocess‘g$ поточечно. Доказательство — индукция по числу узлов: на каждом шаге $f(x_k)\cdot ‘step‘\le g(x_k)\cdot ‘step‘$, поскольку множитель step неотрицателен. Предохранитель C1: на конечной сумме — точное неравенство, на процессе — поточечное. Содержательно: большая подынтегральная функция накрывает большую площадь.}

Неотрицательность: мотив M4

{ Частный случай монотонности — ключевой мотив всей Части V. Лемма riemann_sum_nonneg: если $f\ge 0$ во всех узлах сетки и шаг неотрицателен, то $‘rieman{n}_{s}um‘f\ge 0$. Это четвёртый сквозной мотив Части V (M4): интеграл от неотрицательной функции неотрицателен. Он следует из монотонности с $g=f$, $f=0$ либо доказывается прямой индукцией.}

Содержательно мотив прост: площадь под неотрицательным графиком неотрицательна. Но именно он — основа того, что интеграл задаёт меру: положительный линейный функционал, переводящий неотрицательные функции в неотрицательные числа. Это мост к Части VI, где из интеграла кусочно-постоянных вырастет общая мера. M4 здесь — не техническая деталь, а тот порядковый закон, ради которого интеграл вообще годится в фундамент меры. В разборе § 5.1.5 M4 — то правило (Rule), которым интеграл есть положительный функционал.

Неотрицательность нормы step-функций

Тот же мотив M4 проявляется и в точной step-линии. $L^1$-норма step-функции определена как интеграл её модуля, $\Vert f{\Vert }_1=I(|f|)$, и лемма norm_nonneg утверждает $\Vert f{\Vert }_1\ge 0$. Вместе со step_integral_nonneg (интеграл неотрицательной ступени неотрицателен) это показывает: закон M4 един для обеих линий — и процессно-сеточной (riemann_sum_nonneg), и точной step-линии (norm_nonneg). Один и тот же порядковый закон интеграла проявляется дважды, на двух разных конструкциях, — что и подобает фундаментальному свойству.

Оценки сверху и снизу

Порядок даёт и количественные оценки. Лемма riemann_sum_abs_bound: если $|f|\le M$ в узлах, то $|‘rieman{n}_{s}um‘fa‘step‘n|\le M\cdot n\cdot ‘step‘$. Лемма riemann_sum_global_bound: при $\mathrm{lo}\le f\le \mathrm{hi}$ в узлах сумма из $n$ слагаемых зажата между $\mathrm{lo}\cdot n\cdot ‘step‘$ и $\mathrm{hi}\cdot n\cdot ‘step‘$. Это оценки произвольной конечной суммы с $n$ подынтервалами. В интегральном процессе на уровне $n$ число подынтервалов равно $Sn$ (то есть $n+1$), и нормировка такова: $(Sn)\cdot ‘integra{l}_{s}tep‘abn=b-a$ (grid_width_eq). Подставив, получаем для конечной суммы процесса $‘RS{‘}_n$:

$$|‘RS{‘}_n(f)|\le M\cdot (b-a),\mathrm{lo}\cdot (b-a)\le ‘RS{‘}_n(f)\le \mathrm{hi}\cdot (b-a).$$

Формулировать их стоит именно так — как оценки конечной суммы $‘RS{‘}_n$, теоремы о конкретном уровне, а не о предельном интеграле. Как оценки интеграла — $|\int f|\le M\cdot (b-a)$ и так далее — они читаются после того, как процесс сумм принят интегральным представителем со смыслом Коши (§ 5.1.4, § 5.5). Предохранитель C1: оценки на конечной сумме точны и безусловны; интегральное чтение вторично и условно. Эти оценки готовят оценку сходимости § 5.5.

Сходимость: интегрируемость как свойство Коши

Телескоп и связь с производной

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

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

Сумма приращений по узлам равна полному приращению от $a$ до конца сетки — и это совпадение лейбницево-точное, потому что узлы заданы рекурсивной walk_point из § 5.4, а не формулой $a+ks$ (та же honest-деталь, что разбиралась в главе о производной).}

Связь с производной даёт лемма rs_tele_error_bound: если $f$ равномерно дифференцируема на $[a,b]$ с производной $f^{\prime }$ (udiff_on из § 5.4), то разница между Римановой суммой $f^{\prime }$ и телескопической суммой $f$ мала — найдётся уровень $N$, при котором она не превосходит $\epsilon \cdot (b-a)$. Предохранитель C1: это оценка с выбором уровня, $\epsilon$-grid-форма. Доказательство — внутренняя индукция по числу шагов сетки, на каждом шаге работает граница из равномерной дифференцируемости.

grid-FTC: Риманова сумма производной приближает приращение{grid-FTC: Риманова сумма производной приближает приращение}

Соединив телескоп с его свёрткой, получаем сеточную форму основной теоремы анализа — лемму ftc_grid. Если $f$ равномерно дифференцируема на $[a,b]$ с производной $f^{\prime }$, то для всякого $\epsilon >0$ найдётся уровень $N$, при котором

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

{ Здесь $N+1$ соответствует S N в коде. Содержательно: сумма значений производной по сетке приближает полное приращение функции. Доказательство прямое — rs_tele_error_bound оценивает расстояние от телескопа, а telescope_collapse отождествляет телескоп с приращением $f(y_{N+1})-f(a)$.}

Назовём статус честно (предохранитель C1). Это не классическое равенство ${\int }_a^b{f}^{\prime }=f(b)-f(a)$. Это его сеточная, приближённая форма: при достаточно мелкой сетке сумма производной сколь угодно близка к приращению. Развёрнутая основная теорема анализа — её точная сеточно-процессная формулировка и следствия — предмет главы 5.6; здесь ftc_grid выступает как мост, показывающий, что измельчение действительно сближает сумму с приращением.

Интегрируемость как свойство Коши процесса{Интегрируемость как свойство Коши процесса}

Теперь можно сказать, что значит <<функция интегрируема>> в процессном смысле. Это значит, что процесс integral_process есть процесс Коши: его значения на разных уровнях сближаются при измельчении сетки. Тогда процесс-кандидат из § 5.1.4 становится законным интегралом — сходящимся процессом с устойчивым значением. Для некоторых достаточно регулярных классов это поведение уже поддержано сеточными оценками. В частности, ftc_grid контролирует Римановы суммы производной равномерно дифференцируемой функции через приращение самой функции (§ 5.5.2). Более общее утверждение — о Коши-сходимости integral_process для всех липшицевых или всех непрерывных функций — потребовало бы отдельной теоремы, которой в опорных файлах нет.

Здесь нужен терминологический предохранитель. Слово <<интегрируемость>> мы употребляем как процессное чтение инфраструктуры, а не как уже введённый в репозитории предикат. В ядре нет отдельного предиката is_riemann_integrable с доказанными общими свойствами, и нет единой теоремы <<процесс integral_process есть Коши для всех непрерывных функций>>. Есть сеточные оценки для конкретных классов, из которых свойство Коши собирается для конкретной функции. Такой предикат можно было бы ввести позже как обобщение текущей инфраструктуры — но читателю не следует искать в коде центральный предикат интегрируемости: его там нет, и это честная граница. (Здесь же в дело входит ProcessArithmetic.v с сохранением свойства Коши под операциями — и его оговорка о classic, к которой § 5.8.3 ещё вернётся.)

Измельчение без завершённой бесконечности

Остаётся последний кирпич — что измельчение действительно достигает любой точности. Лемма integral_step_vanishes: для всякого $\delta >0$ найдётся уровень $N$, на котором шаг сетки меньше $\delta$. Опирается она на архимедово свойство — именно на лемму nat_above_Q из процессного слоя производной (§ 5.4). Близкая архимедова лемма q_archimedean есть в ProcessArithmetic.v, но это другой технический маршрут (монотонные ограниченные процессы), и integral_step_vanishes её не использует. За конечное число делений шаг становится как угодно мал.

{ Это та же интонация, что в § 5.1 (шкала процессов сколь угодно мелка) и § 5.4 (walk_step_small). Под $P4$ <<измельчение до бесконечности>> — это процесс, а не завершённая бесконечность: каждый уровень конечен, на каждом сетка имеет конечное число узлов, а предел как отдельный объект не берётся. Интеграл не ждёт <<бесконечно мелкого разбиения>> — он есть процесс всё более мелких конечных разбиений.}

Граница главы: что интеграл готовит для FTC

Телескопическая сумма как мост к производной

Эта глава строит интеграл и его базовые свойства; развёрнутая основная теорема анализа и её следствия — предмет следующей главы. Здесь мы лишь очерчиваем границу: что уже готово и что развернётся дальше.

Конструктивное зерно будущей теоремы уже в руках — это телескоп § 5.5.1. Лемма telescope_collapse сворачивает сумму приращений функции по узлам сетки в разность концов, $f(y_n)-f(a)$. Это и есть мысль основной теоремы в зародыше: накопление приращений функции равно её полному изменению. Интеграл производной и приращение функции связаны телескопом — осталось превратить эту связь в теорему, что и сделает глава 5.6.

grid-FTC как предварительная форма

Второй готовый кирпич — ftc_grid из § 5.5.2. Подчеркнём его статус ещё раз: это предварительная, сеточная форма основной теоремы — неравенство $|‘RS‘(f^{\prime })-(f(\text{конец})-f(a))|\le \epsilon \cdot (b-a)$, а не точное равенство $\int f^{\prime }=f(b)-f(a)$. Предохранитель C1: $\epsilon$-grid-форма. Глава 5.5 не доказывает развёрнутую теорему и её следствия — она лишь доводит до сеточного моста, на котором следующая глава построит точную связь.

Какие правила развернёт следующая глава

Назовём — именно назовём, не разбирая, — что глава 5.6 построит поверх grid-FTC. Файл IntegralApplications.v содержит правило произведения для интеграла (udiff_product, с тем же $\epsilon /3$-разложением product_decomp, что и правило произведения производной в § 5.4), интегрирование по частям (integration_by_parts и его частный случай ibp_self) и единственность первообразной (antiderivative_unique: две функции с одной производной имеют равные приращения — сеточная параллель тому, что нулевая производная означает почти-постоянство, § 5.4). Все эти теоремы сверены и существуют в репозитории — но их естественное место — глава об основной теореме анализа. Здесь достаточно отметить, что инфраструктура для них готова: grid-FTC, линейность сумм и равномерная дифференцируемость уже на месте.

Почему общая замена переменной пока не построена

{ Одну границу стоит назвать особо — замену переменной. Общего цепного правила в ядре нет, как уже отмечалось в § 5.4. Есть только аффинный случай: udiff_chain_affine для внутренней функции $g=c\cdot x+d$, и на нём аффинная замена в интеграле (ftc_u_substitution_affine). То есть подстановка формализована лишь для линейной замены переменной; общая замена $u=g(x)$ с произвольной гладкой $g$ — нет. Это честная граница, очерченная конкретно: глава 5.6 развернёт правила интеграла в доказанных пределах, не приписывая теории большего, чем в ней есть.}

Вычислительные примеры

Интеграл на отрезке [0,1]: процесс в числах

Процессный интеграл хорош тем, что на каждом уровне даёт конкретное рациональное число, которое можно вычислить. Файл ProcessIntegration.v делает это явно на отрезке $[0,1]$: своя сумма riemann_sum_01 с $K+1$ узлами и интеграл process_integral_01 $fK$ на уровне $K$. Примеры доказаны прямым вычислением (vm_compute): интеграл единицы ${\int }_0^{1}1$ равен $1$ на уровнях $K=0,1,2$; интеграл нуля равен нулю; интеграл двойки равен $2$. На каждом уровне — точное рациональное значение, машинно-проверяемое.

{ Предохранитель C4: это своё riemann_sum_01 на $[0,1]$, отдельное от основного riemann_sum по walk_point из § 5.1.3. Файл демонстрационный; мы используем его как иллюстрацию <<интеграл считается>>, не как основную теорию.}

Исчисление как процесс: демонстрация

Ещё дальше идёт файл ProcessAnalysis.v — развёрнутая демонстрация <<исчисления как процесса над $Q$>> без всякого $\epsilon$-$\delta$, на одних рациональных вычислениях. Производная квадрата там — процесс process_derivative $f_{s}quare$, равный $2x+1/(K+1)$; в точке $x=1$ он даёт $3,5/2,21/10,201/100$ на уровнях $K=0,1,9,99$ — видно, как значения приближаются к $2$. Интеграл ${\int }_0^{1}1$ равен $1$ на каждом уровне. Итоговая process_analysis_foundation собирает эти примеры в одно утверждение.

Здесь предохранитель C4 особенно важен. Файл ProcessAnalysis.v содержит свои process_derivative, riemann_sum и process_integral — определения, отличные от тех, что в ProcessDerivative.v и RiemannIntegration.v, хотя имена совпадают. Это самостоятельный демонстрационный файл; его process_integral не следует путать с основным интегралом главы. Мы цитируем его как наглядную иллюстрацию, не как якорь теории.

Что показывают примеры

Примеры подтверждают главный тезис главы наглядно. Интеграл и производная под $P4$ — процессы, и каждый уровень такого процесса есть точное рациональное вычисление, проверяемое машиной, без обращения к завершённой бесконечности. Значения приближаются к классическим — $2$ для производной квадрата в единице, $1$ для ${\int }_0^{1}1$, — но само приближение и есть объект: процесс, а не его предел. Где классический анализ говорит <<предел равен двум>>, теория систем говорит <<процесс $3,5/2,21/10,201/100,\dots$>> — и этого достаточно, потому что под $P4$ число представляется таким процессом, а точечное число в строгом смысле читается как класс эквивалентных процессов (как уточнялось в Главах IV.3–IV.4).

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

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

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

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

• интеграл как процесс накопления integral_process (шаг $(b-a)/(n+1)$); конечная Риманова сумма riemann_sum на walk-сетке; integral_is_process_construction;
• точный интеграл step-функций step_fun_integral — фундамент будущей меры;
• линейность (сложение, скаляр, разность) — на конечной сумме и на процессе;
• монотонность; неотрицательность — мотив M4 (riemann_sum_nonneg, norm_nonneg);
• оценки сумм (abs_bound, global_bound); телескоп (telescope_collapse); сеточный мост grid-FTC (ftc_grid);
• вычислительные примеры (${\int }_0^1$ на разных уровнях).

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

• более развитая формулировка основной теоремы анализа ${\int }_a^b{f}^{\prime }=f(b)-f(a)$ и её следствия — здесь доказана только сеточная форма ftc_grid; дальнейшее — глава 5.6 (которая, судя по опорным файлам, тоже работает в сеточном walk-point-каркасе, а не выходит сразу на точное равенство на классах);
• правило произведения, интегрирование по частям, единственность первообразной как развёрнутые теоремы — они существуют в IntegralApplications.v, но их место — глава 5.6;
• интеграл функции на классах RealPoint — здесь только $Q$-функции (предохранитель C2);
• общая замена переменной — формализован лишь аффинный случай;
• интеграл Лебега и общая мера — step-функции лишь фундамент (Часть VI);
• несобственный интеграл как процесс расширения области — естественное будущее расширение, не предмет этой главы.

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

• основную теорему анализа (глава 5.6): развёрнутую сеточно-процессную связь производной и интеграла через ftc_grid, udiff_product, ИБП;
• Фубини (глава 5.7): 2D step-функции;
• меру (Часть VI): step-функции как $L^1$-фундамент Бишопа–Ченга.

Что осталось бы для интеграла на классах

Глава честно ограничилась функциями $Q\to Q$. Назовём конкретно, какого шага не хватает до интеграла на фактор-классах RealPoint — так же, как § 4.8 называла недостающее звено для производной. Понадобилось бы, во-первых, доказать корректность integral_process относительно эквивалентности процессов — что интеграл не меняется при замене подынтегральной функции эквивалентной; во-вторых, поднять определение с $Q$-функций на функции фактор-классов. В опорных файлах этого нет — честная граница, очерченная конкретно.

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

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

Особый случай заслуживает прямого упоминания. Файл ProcessArithmetic.v заявляет в шапке << AXIOMS: none >>, но импортирует Stdlib.Classical и использует classic в доказательстве monotone_bounded_Cauchy — заголовок прямо расходится с фактом. А главный якорь ProcessIntegral.v импортирует ProcessArithmetic.v. Точная — и не огульная — формула такова: сам факт импорта ещё не означает, что каждая интегральная теорема зависит от classic (многие могут не зависеть), но заголовок файла << 0 axioms >> не является достаточным аудитом — статус конкретной теоремы устанавливается только командой Print Assumptions для неё самой. Это сильнейший довод за сквозное правило C3. Не следует делать огульного утверждения ни в одну сторону.

{ Print Assumptions выписан в финале RiemannIntegration.v для ftc_grid, udiff_add, ftc_comparison. У файлов без такого финального блока статус конкретной теоремы при необходимости проверяется отдельно. Реально конструктивны (импортируют только Rocq-stdlib или ProcessCore, без классического слоя): StepIntegral.v, ProcessIntegration.v, ProcessAnalysis.v — StepIntegral.v к тому же короток и заявляет << 20 Qed, 0 Admitted, 0 axioms >>. И ещё один honest-факт для полноты: имя riemann_sum носят три разных определения в трёх файлах.}

Итог главы

Глава построила интеграл — аналитический слой, двойственный производной § 5.4. Главный поворот в том, как устроено само понятие. Интеграл — это процесс накопления Римановых сумм, а не завершённый предел: конечная сумма на каждом уровне точна и рациональна, а процесс собирает измельчение сетки. Сам процесс существует для любой $Q$-функции и служит представителем интеграла; его законность как интеграла даёт сходимость — свойство Коши, которое для конкретных регулярных классов функций собирается из сеточных оценок. Главная осторожность: grid-FTC — сеточная форма; развёрнутая связь производной и интеграла будет предметом главы 5.6; step-функции — фундамент меры, не сама мера.

Построено: интеграл-процесс integral_process и конечная Риманова сумма; точный интеграл step-функций; линейность, монотонность, неотрицательность (M4); оценки, телескоп и сеточный мост grid-FTC; вычислительные примеры.

На чём стоит: на walk-точках и равномерной дифференцируемости § 5.4, на архимедовом свойстве как топливе измельчения, на процессной онтологии $P4$, в которой интеграл — не завершённый предел сумм, а процесс их накопления.

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

---

---

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

Навигация: ← Глава 4. Производная · Глава 6. Основная теорема анализа →

Footnotes

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