Глава 7. Теорема Фубини на процессах

Зачем главе Фубини

Где стоит глава

Часть V прошла одномерный анализ на процессах: метрику (Глава 5.1), топологию и компактность (5.2), непрерывность (5.3), производную как процесс уточнения наклона (5.4), интеграл как процесс накопления (5.5) и основную теорему анализа, связавшую их (5.6). Одномерная картина замкнута. Остаётся шаг в многомерное интегрирование — и первый его закон есть теорема Фубини: связь двойного интеграла с повторными одномерными.

Что именно эта глава доказывает — и что нет

Здесь нужна честность с самого начала, ибо предмет обманчив. Формально в этой главе доказан не процесс измельчающихся двумерных разбиений, а конечный ступенчатый уровень: списки прямоугольных вкладов с точной рациональной арифметикой. В опорном файле нет ни типа RealProcess, ни функции nat $\to$ ℚ, ни последовательности мельчающихся 2D-сеток — есть конечный список прямоугольников и конечные суммы их вкладов.¹

Но именно этот скромный уровень показывает первый закон порядка наблюдения — что итог не зависит от того, в каком порядке сложены вклады, — и показывает, где этот закон из тривиального становится трудным. <<Двойной интеграл как процесс по 2D-разбиениям>> останется в этой главе философской рамкой и программой, а не доказанным объектом; доказан конечный прототип, который этот процесс в будущем должен поднять к пределу.

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

Глава идёт так. Сперва — конечный двойной интеграл по прямоугольным вкладам (§ 7.2) и доказанная на нём теорема Фубини для ступенчатых функций (§ 7.3), с конкретными вычислениями. Затем — методологическая вершина: почему перестановка пределов нетривиальна и что её легитимизирует (§ 7.4). Затем — честная граница: непрерывный случай как программа, не теорема, с названными кирпичами (§ 7.5). Затем — обобщения и применения как перспектива (§ 7.6), разбор E/R/R (§ 7.7) и итог главы и всей Части V (§ 7.8).

Конечный двойной интеграл по прямоугольным вкладам

От одномерного к двумерному

Одномерный интеграл ступенчатой функции (Глава 5.5) есть сумма вкладов $c_i\cdot (b_i-a_i)$ — значение на куске, умноженное на длину куска. Двумерный аналог берёт значение на прямоугольнике и умножает на его площадь: $c\cdot (x_2-x_1)\cdot (y_2-y_1)$. Это и есть носитель настоящей главы.

Прямоугольник и его интеграл

Прямоугольный вклад ToS записывает типом Rectangle: постоянное рациональное значение на рациональном прямоугольнике, с условием корректности границ.

Record Rectangle := mkRect {
  rect_val : Q;
  rect_x1 : Q;  rect_x2 : Q;
  rect_y1 : Q;  rect_y2 : Q;
  rect_x_valid : rect_x1 <= rect_x2;
  rect_y_valid : rect_y1 <= rect_y2 }.
 
Definition rect_integral (r : Rectangle) : Q :=
  rect_val r * (rect_x2 r - rect_x1 r) * (rect_y2 r - rect_y1 r).

Двумерная ступенчатая функция — конечный список таких прямоугольников, StepFun2D := list Rectangle, а её двойной интеграл integral_2d — сумма вкладов rect_integral по списку. Вся арифметика — точная, в ℚ; никаких пределов на этом уровне нет.

Оговорка: список вкладов, а не разбиение

{ Здесь нужна точность, иначе скромный объект прозвучит сильнее, чем он есть. StepFun2D — это не обязательно разбиение области и не обязательно непересекающийся набор прямоугольников; это формальная конечная сумма прямоугольных вкладов. Файл не строит теории покрытий области, не требует, чтобы прямоугольники замощали $[a,b]\times [c,d]$ без щелей и наложений; он определяет сумму вкладов и доказывает её свойства. Это достаточно, чтобы увидеть закон порядка, но это не общий двойной интеграл произвольной функции.}

Фубини для ступенчатых функций: что доказано

Один прямоугольник: порядок не важен

Повторный интеграл по одному прямоугольнику можно взять в двух порядках: сперва по $x$, потом по $y$ — или наоборот. ToS записывает оба и доказывает их равенство.

Definition iterated_xy (r : Rectangle) : Q :=
  rect_val r * (rect_x2 r - rect_x1 r) * (rect_y2 r - rect_y1 r).
Definition iterated_yx (r : Rectangle) : Q :=
  rect_val r * (rect_y2 r - rect_y1 r) * (rect_x2 r - rect_x1 r).
 
Lemma fubini_rectangle : forall r : Rectangle,
  iterated_xy r == iterated_yx r.
Proof. intros r. unfold iterated_xy, iterated_yx. ring. Qed.

Доказательство — одно слово ring: равенство есть в точности коммутативность умножения, $c\cdot \Delta x\cdot \Delta y=c\cdot \Delta y\cdot \Delta x$. И обе повторные величины равны двойному интегралу прямоугольника (iterated_eq_double, iterated_yx_eq_double).

Список прямоугольников: индукция

{ Для конечного списка вкладов теорема Фубини доказывается индукцией по списку: на пустом — тождество, на шаге — равенство для головного прямоугольника (fubini_rectangle) плюс предположение индукции.}

Theorem fubini_step : forall f : StepFun2D,
  iterated_xy_list f == iterated_yx_list f.
Proof.
  intros f. induction f as [| r rest IH].
  - simpl. ring.
  - simpl. rewrite fubini_rectangle. rewrite IH. ring.
Qed.

{ И оба повторных интеграла списка равны двойному (iterated_xy_eq_2d, iterated_yx_eq_2d): порядок сложения вкладов и порядок интегрирования внутри вклада — оба безразличны.}

Конкретные вычисления

{ В духе Части V — не только построение, но и работающее вычисление. Возьмём $f=3$ на $[0,1]\times [0,2]$: двойной интеграл есть $3\cdot 1\cdot 2=6$, и оба порядка дают одно (example_rect_integral, example_fubini_concrete). Для двух прямоугольников — $f=2$ на $[0,1]\times [0,1]$ и $f=3$ на $[1,2]\times [0,1]$ — двойной интеграл есть $2+3=5$ (example_two_rects). Всё это Rocq проверяет точной рациональной арифметикой: в этих примерах доказательства сводятся к ring или прямому применению fubini_rectangle — процессный анализ здесь не абстракция, а счёт.}

Тривиально на ступени, трудно на пределе

На ступенчатом уровне теорема Фубини тривиальна: она есть коммутативность умножения, доказываемая одним ring. Весь содержательный вес теоремы лежит не здесь, а на уровне предела — там, где конечный список вкладов должен смениться процессом измельчающихся разбиений. Доказанное fubini_step — конечный прототип закона порядка; настоящая Фубини начинается за ним.

Почему перестановка пределов нетривиальна

Двойной предел

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

В общем случае пределы переставлять нельзя

А смена порядка двух пределов — операция деликатная и в общем случае неверная. Величины ${\lim }_n{\lim }_m{a}_{nm}$ и ${\lim }_m{\lim }_n{a}_{nm}$ могут давать разные значения, а то и не существовать вовсе. Это известный факт анализа, и теорема Фубини есть в точности утверждение, что для подынтегральной функции здесь перестановка законна. Без обоснования это утверждение неверно: существуют функции, для которых повторные интегралы в разных порядках дают разные числа.

Стоит сказать точно, что прячет привычное классическое изложение, когда подаёт Фубини как технический результат. Прячет оно не столько один акт выбора, сколько условия, при которых менять порядок пределов разрешено: полноту $L^1$, интегрируемость подынтегральной функции, доминированную сходимость, машинерию Фубини–Тонелли. В конструктивном чтении именно эти места требуют явных процессов и модулей сходимости, а не молчаливого перехода к пределу.

Что легитимизирует перестановку: равномерность

Что же делает перестановку законной для непрерывной функции на компактном прямоугольнике? Равномерная непрерывность (Глава 5.3). Когда $f(x,y)$ непрерывна на компакте $[a,b]\times [c,d]$, её модуль непрерывности $\omega (\epsilon )$ не зависит ни от $x$, ни от $y$. Значит, скорость сходимости римановых сумм оценивается одной общей функцией $\epsilon \mapsto \delta (\epsilon )$ для всех точек прямоугольника — и уточнение разбиения по $x$ и по $y$ можно синхронизировать: для любой точности $\epsilon$ одновременно подобрать достаточно мелкую сетку по обеим координатам. Эта одновременность и есть то, что делает двойной предел корректным.

Три условия

Итак, перестановка пределов в Фубини на компактном прямоугольнике опирается на три условия:

Условие	Что даёт
непрерывность $f$	локальные модули непрерывности в каждой точке
компактность области (Гейне–Борель, 5.2)	равномерность — единый модуль на всём прямоугольнике
архимедовость ℚ\ (3.4)	согласование уровней разбиения по двум координатам одним $N$

Без любого из трёх теорема в общей форме ломается: для разрывных функций или на некомпактных областях есть классические контрпримеры, где повторные интегралы расходятся. С тремя условиями появляется каркас будущего обоснования: они дают синхронизацию сеток и контроль приближений. Но — и это предмет следующего раздела — само доказательство перестановки двух предельных процессов требует $L^1$-слоя и доминированной сходимости и в репозитории ещё не собрано в машинную теорему.

Непрерывный случай: программа, не теорема

Каркас, а не доказательство

Три условия § 7.4 — верный и стандартный путь к непрерывной Фубини. Но сами по себе они теорему не доказывают: они дают инженерный каркас для построения синхронизированных двумерных сеток. Перестановка двух предельных процессов требует, сверх этого каркаса, отдельного слоя — приближения непрерывной функции ступенчатыми и контроля сходимости интегралов (тип доминированной сходимости). Этот слой здесь не собран. Единой машинной теоремы <<Фубини для непрерывных>> в репозитории нет.²

Кирпичи — и чем именно они являются

{ Кирпичи для будущего непрерывного случая в репозитории есть, и важно назвать каждый точно, не приписывая ему чужой силы. }

Точный ступенчатый интеграл. Файл StepIntegral.v (20 Qed, 0 аксиом) даёт точный интеграл ступенчатых функций над ℚ — основание подхода Бишопа–Ченга, на котором всё остальное есть $L^1$-пополнение. Это будущий носитель аппроксимации; сама теорема о приближении непрерывной функции ступенчатыми в этой главе не доказана.

Скелет доминированной сходимости. Файл DominatedConvergence.v (20 Qed, 0 аксиом) даёт основания ступенчатого уровня: доминирование, $L^1$-сходимость, сходимость интегралов, скелет теоремы о доминированной сходимости. Файл сам честно отмечает, что на ступенчатом уровне эта теорема почти тривиальна, а глубокое содержание возникает при переходе к $L^1$-пополнению. Это ещё не та доминированная сходимость, что доказывает непрерывную Фубини.

Компактность — с ограничением ℚ. Файл HeineBorelComplete.v (22 Qed, 0 аксиом) даёт тотальную ограниченность ℚ-интервалов и равномерную непрерывность из липшицевости, плюс теорию $\epsilon$-сетей. Но он же прямо отмечает: полный Гейне–Борель и переход <<непрерывность $\Rightarrow$ равномерность>> в общем виде над ℚ не доступны в текущем слое — используются лишь липшицев частный случай или допущение о числе Лебега. Это honest-граница самого инструмента компактности.

Что остаётся фронтиром

Итак, непрерывная Фубини есть программа, не теорема: каркас трёх условий верен, кирпичи названы, но все они — ступенчатого уровня, а решающий шаг ($L^1$-пополнение и доминированная сходимость на нём, с аккуратным обходом ℚ-ограничения на равномерность) остаётся фронтиром процессного анализа. В рабочей карте формализации (см. итог тома) эта задача стоит явным пунктом.

Обобщения и применения

Ниже — не результаты текущего файла, а направления, для которых ступенчатая Фубини есть первый конечный прототип.

n-мерное обобщение. Фубини обобщается на интегралы в $n$-мерных областях; конструктивный путь — индукция по размерности, сводящая $n$-мерный интеграл к одномерному шаг за шагом. В коде этого обобщения нет — оно намечено как программа.

Применения. На непрерывную Фубини, когда она будет собрана, опираются: вычисление объёмов многомерных тел; сведение многомерных уравнений (в частности УЧП) к одномерным; преобразования Лапласа и Фурье (Часть VII); построение меры произведения (Часть VI). Всё это — перспектива, лежащая за настоящей главой, а не её следствия.

Разбор E/R/R: Фубини-перестановка как система

Закрепим доказанное разбором E/R/R (Часть I); шапка опорного файла даёт разметку прямо. Ведём в онтологическом порядке Rules $\to$ Roles $\to$ Elements.

Rules — конституция: порядок интегрирования не влияет на итог (fubini_step); на ступенчатом уровне это коммутативность умножения. Roles — значимые позиции: двойной интеграл, повторный интеграл, обмен порядка. Elements — носители: прямоугольники и конечные списки прямоугольных вкладов; по $P4$ всякий такой список конечен, интеграл вычисляется точно.

Хорошая сформированность и диагностика. Разметка однозначна: прямоугольники — элементы, интегралы и обмен — роли, закон порядка — правило. И здесь разбор оборачивается диагностикой, важной для всей главы: на конечном ступенчатом уровне правило перестановки доказано (коммутативность); на уровне предела оно становится трудной теоремой. Смешать два уровня — принять доказанное на ступени за доказанное на пределе — и есть конструктивная ловушка, в которую попадает наивное чтение Фубини. Классическое изложение прячет здесь не <<выбор вообще>>, а условия перестановки пределов (§ 7.4); честная разметка эти условия выносит наружу.

Итог главы. Итог Части V. Переход к Части VI

Итог главы

Глава прошла теорему Фубини на той честной глубине, на какой она сегодня формализована. Доказан — точно и без аксиом — ступенчатый случай: двойной интеграл конечного списка прямоугольных вкладов не зависит от порядка интегрирования (fubini_step). Показано, что на этом уровне теорема тривиальна, а её настоящий вес — в перестановке пределов: для непрерывного случая равномерная непрерывность на компакте даёт каркас синхронизации сеток, а полное обоснование требует $L^1$-слоя и доминированной сходимости. И честно очерчено, что непрерывный случай остаётся программой: каркас трёх условий верен, кирпичи названы, но $L^1$-слой не собран.

Итог Части V

Настоящей главой Часть V замыкается. Сожмём её путь. Метрика оказалась процессом разностей (5.1). Топология и компактность — режимами рассмотрения семейств процессов: компактность взята через конструктивные и условно-классические формы — $\epsilon$-сети, uniform-вариант Гейне–Бореля и Cauchy-версию Больцано–Вейерштрасса, с явной маркировкой $L3$/$L4$ там, где она нужна (5.2). Непрерывность — с $\epsilon$-версиями теорем о промежуточном значении и экстремуме (5.3). Производная — процессом уточнения наклона (5.4). Интеграл — процессом накопления (5.5). Основная теорема анализа связала производную и интеграл (5.6). И Фубини — открыла дверь в многомерное, показав на конечном прототипе закон порядка и назвав, где начинается его глубина (5.7). Сквозная нить выдержана: аналитический объект строится как процесс — где-то как настоящий процесс приближения, где-то (Фубини) как конечный step-прототип будущего процессного предела.

Переход к Части VI

Дальше — мера и интегрирование по Лебегу. Ступенчатый интеграл, служивший здесь носителем, есть основание меры в подходе Бишопа–Ченга; $L^1$-пополнение, оставленное фронтиром в § 7.5, и есть предмет Части VI. ToS построит там интегрирование без внешней сет-теоретической аксиомы выбора, с явной локальной маркировкой $L3$ и $L4$ там, где они понадобятся, — и тогда непрерывная Фубини, программа этой главы, получит своё полное доказательство.

{ Итог — в трёх частях. Первое: что доказано. Теорема Фубини для конечных списков прямоугольных вкладов: двойной интеграл не зависит от порядка интегрирования (fubini_step) — точно, без аксиом, как коммутативность умножения. Второе: на чём это стоит и чего здесь нет. Доказан ступенчатый прототип; непрерывный случай — программа на трёх условиях (равномерная непрерывность, компактность, архимедовость) с названными кирпичами (StepIntegral, DominatedConvergence, HeineBorelComplete), но без собранного $L^1$-слоя. Третье: куда ведёт. Перестановка пределов — не тривиальность, а сердце многомерного анализа; ступенчатая Фубини есть её конечный прототип, а полное доказательство ждёт меры Части VI. Этим Часть V завершается: весь базовый анализ получил процессно-совместимую инфраструктуру — часть результатов уже дана как процессы, часть как конечные step-прототипы будущих процессных пределов, — и сила каждого шага честно размечена.}

---

---

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

Понятия: Формализация

Навигация: ← Глава 6. Основная теорема анализа · Глава 1. Мера как процесс приписывания — Часть VI →

Footnotes

1. Опорный файл — FubiniProcess.v Rocq-репозитория ToS (каталог src/analysis/), 20 доказанных утверждений, 0 Admitted, 0 аксиом. Имена, приводимые ниже, — из него. ↩

2. В предварительном плане главы доказательство непрерывного случая было ошибочно отнесено к несуществующему файлу Fubini.v; фактический файл — FubiniProcess.v — доказывает ступенчатый случай. Здесь это исправлено. ↩