Глава 4. Теоремы сходимости: монотонная и мажорированная

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

Предел под интегралом

Главы 6.1–6.3 построили меру и интеграл Лебега как процессы. Настоящая глава ставит вопрос, ради которого интеграл Лебега и был создан: когда предел можно вносить под интеграл — когда

$$\int \underset{n}{\lim }{f}_n=\underset{n}{\lim }\int f_n.$$

Это обмен двух пределов, и он не автоматичен: интеграл сам есть предел (процесс накопления), и переставить его с пределом последовательности $f_n$ можно лишь при условиях. Два классических условия дают две теоремы — монотонной сходимости (Беппо Леви) и мажорированной сходимости (Лебег); их и разбирает глава, вместе с леммой Фату, которая обе подпирает.

Где прячется бесконечность — и что доказано

Перестановка двух пределов — ровно то место, где в классическом анализе прячется неконструктивность: то завершённая мера, то <<существующая>> мажоранта, добываемая неявно. ToS вытаскивает обе на свет. Держим три уровня строгости. Доказано: монотонная сходимость — растущая ограниченная последовательность интегралов сходится (цена — L3); редукция мажорированной сходимости — её движок и мажоранта-конверт доказаны без аксиом, а сходимость интегралов следует из сходимости невязок; лемма Фату на процессном уровне. Остаётся честной границей: сам шаг <<поточечная сходимость плюс мажоранта влечёт сходимость невязок к нулю>> — тот самый шаг Фату над завершённой мерой — берётся как явная гипотеза-вход, а не доказывается внутри системы.¹

E/R/R-каркас главы

Зададим каркас в порождающем порядке Rules $\to$ Roles $\to$ Elements; полный разбор — в § «Разбор в порождающем порядке». Глава вводит систему теорем сходимости.

Rules (Правила, $\leftrightarrow$ L5). Правило обмена $\int \lim =\lim \int$ при условиях, расщеплённое на: <<монотонно-ограниченное сходится>> (цена L3); движок (разность интегралов не больше интеграла модуля разности); конверт (доминирование); сжатие невязки.

Roles (Роли, $\leftrightarrow$ L4). <<Интеграл предела>> — роль-предел процесса интегралов; мажоранта $g$ — роль-конверт (явный параметр); невязка $\int |f_n-f|$ — роль-индикатор близости.

Elements (Элементы, $\leftrightarrow$ L1$+$P4). Значения $\int f_n$, значения мажоранты $g$, невязки $\int |f_n-f|$; завершённый предел-функция и завершённая мера (полный Фату) — вне элементов.

Монотонная сходимость (Беппо Леви)

Пусть функции растут поточечно, $f_0\le f_1\le f_2\le \dots$, и равномерно ограничены. Тогда их интегралы тоже растут (интеграл монотонен) и ограничены сверху — а растущая ограниченная последовательность сходится. Это и есть монотонная сходимость: $\int f_n$ возрастает к пределу, и предел этот существует как процесс.

Доказательство процессно и опирается на единственный классический шаг — монотонный ограниченный процесс есть процесс Коши, — который стоит на Законе Исключённого Третьего.²

Доказуемое ядро монотонной сходимости — теорема: процесс интегралов растущей ограниченной последовательности сходится. <<Интеграл предела>> $\int {\lim }_n{f}_n$ есть роль-предел этого процесса; завершённая предельная функция как объект не нужна.

Цена — L3 — это именно цена леммы monotone_bounded_Cauchy: перехода от монотонности и ограниченности к Cauchy-поведению процесса (та же зависимость, что у счётной аддитивности в Главе 6.1). Это честная и единственная цена монотонной сходимости; никакой завершённой меры или Аксиомы Выбора она не требует.

Доменно-явная мажоранта

Прежде чем перейти к мажорированной сходимости, вернёмся к методу, заявленному в Главе 6.1: мажоранта есть явный параметр, а не существующий по умолчанию объект. Классическая формулировка начинается словами <<пусть существует интегрируемая $g$, такая что $|f_n|\le g$…>>, и в классическом доказательстве эта $g$ часто задаётся как существующая оболочка класса функций или как следствие предыдущей теоремы — а не предъявляется как данные. В ToS $g$ — данная функция, предъявленная гипотезой; доминирование — отношение, берущее $g$ явным аргументом.³

Где классика молча выбирает контролирующую функцию из завершённой совокупности, ToS требует её построить и показать.

Именно явность мажоранты делает мажорированную сходимость конструктивной без Аксиомы Выбора: имея $g$ на руках, остаётся чисто конечная арифметика оценок, к которой мы и переходим.

Мажорированная сходимость как редукция

Теорема Лебега о мажорированной сходимости утверждает: если $f_n\to f$ поточечно и $|f_n|\le g$ с интегрируемой $g$, то $\int f_n\to \int f$. ToS разлагает её на три звена, и первые два доказаны без аксиом.

Движок — неравенство

$$|\int f_n-\int f|\le \int |f_n-f|.$$

Разность интегралов не превосходит интеграла модуля разности; это линейность плюс неравенство треугольника для конечных сумм, доказанные точно.⁴

Конверт — доминирование загоняет невязку под мажоранту:

$$|f_n-f|\le 2g⟹\int |f_n-f|\le \int 2g.$$

Это монотонность интеграла, применённая к доменно-явной мажоранте.⁵

Сжатие — если интеграл невязки стремится к нулю, то по движку и $|\int f_n-\int f|\to 0$, то есть $\int f_n\to \int f$.⁶

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

И здесь — честная граница. Шаг <<поточечная сходимость $f_n\to f$ при мажоранте $g$ влечёт $\int |f_n-f|\to 0$>> — это и есть содержательная сердцевина теоремы Лебега (классически она доказывается через лемму Фату над завершённой мерой). ToS берёт её как явную гипотезу-вход, а не доказывает внутри системы: именно тут жила бы завершённая мера, и именно её мы не актуализируем (P4). Что доказано — это редукция: вся арифметическая машина обмена (движок и конверт) собрана конструктивно, и остаётся ровно один инфинитарный шаг, честно вынесенный наружу.

Лемма Фату на процессном уровне

Лемму Фату — что интеграл нижнего предела не превосходит нижнего предела интегралов — ToS удерживает на процессном уровне: для неотрицательных функций нижняя огибающая последовательности интегралов неотрицательна, а при доминировании ограничена.⁷ Это конечно-процессное ядро Фату: на каждой стадии $n$ величины определены и удовлетворяют нужным неравенствам.

Полная лемма Фату над завершённой мерой — та, через которую классически и доказывается шаг <<невязки $\to 0$>> из § «Мажорированная сходимость как редукция», — остаётся за границей P4: она требует сформулированного нижнего предела и меры на уровне завершённого ($L^1$/мера) пространства — слой, который в текущей главе не актуализируется. Процессное ядро доказано; завершённый объект не актуализируется. Это та же линия честности, что и всюду в Части VI.

E/R/R-разбор: обмен пределов как Правило

Разбор в порождающем порядке

Каркас задан в начале главы (§ «E/R/R-каркас главы»); здесь разворачиваем его с таблицей и проверкой корректности. Разберём систему теорем сходимости в терминах E/R/R, продолжая разборы Глав 6.1–6.3. Оговорка об уровне прежняя. Ведём разбор в порождающем порядке Rules $\to$ Roles $\to$ Elements.

Rules (Правила, $\leftrightarrow$ L5). В основании — правило обмена $\int \lim =\lim \int$ при условиях. Оно расщеплено на: <<монотонно-ограниченное сходится>> (монотонная сходимость, цена L3); движок — разность интегралов не больше интеграла модуля разности; конверт — доминирование загоняет невязку под мажоранту; сжатие невязки (формулы — в § «Мажорированная сходимость как редукция»). Универсальный слой — L1–L5 (в частности, L3 для монотонного предела) и P4, выносящий шаг Фату за границу.

Roles (Роли, $\leftrightarrow$ L4). <<Интеграл предела>> $\int {\lim }_n{f}_n$ — роль-предел процесса интегралов. Мажоранта $g$ — роль-конверт, вынуждающая обмен: явный параметр, а не объект <<по существованию>> (методология предъявления данных). <<Невязка $\int |f_n-f|$>> — роль-индикатор близости, чьё стремление к нулю и есть честная гипотеза-вход.

Elements (Элементы, $\leftrightarrow$ L1$+$P4). Носители конечны на каждой стадии: значения интегралов $\int f_n$, значения мажоранты $g$, невязки $\int |f_n-f|$. Завершённый предел-функция и завершённая мера, через которую идёт полный Фату, — к элементам не принадлежат.

Компонент	Что фиксирует	E/R/R
обмен $\int \lim =\lim \int$; движок; конверт; <<монотонно-огранич. сходится>>	КАК организован перенос предела под интеграл	Rules ($L5$)
интеграл предела; мажоранта-конверт; невязка	ЗАЧЕМ значимы носители: роли обмена	Roles ($L4$)
$\int f_n$; значения $g$; $\int	f_n-f	$

Что даёт разбор

{ Разбор показывает, где в обмене пределов прячется бесконечность и как ToS с ней обходится. Монотонная сходимость честно платит L3 за единственный шаг <<монотонно-ограниченное сходится>>. Мажорированная сходимость редуцирована: её арифметическая машина (движок и конверт) доказана без аксиом, а единственный инфинитарный шаг — стремление невязки к нулю, классически идущее через завершённую меру и Фату, — вынесен в явную гипотезу. Мажоранта при этом не <<существует>>, а предъявляется (L4, P4). Это и есть способ ToS делать теоремы сходимости конструктивными: не прятать инфинитарный шаг в завершённый объект, а назвать его и поставить на границу.}

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

---

---

Часть: Часть VI. Меры и интегрирование · Том: «Математика»

Навигация: ← Глава 3. Измеримые функции и интеграл Лебега · Глава 5. L^1 и L^2: пространства как процессы, полнота как конструируемость →

Footnotes

1. Опорные файлы — ProcessMCT.v, ProcessDCT.v, ProcessFatou.v (каталог src/process/ Rocq-репозитория ToS). Имена лемм — в сносках ниже. ↩

2. Утверждение process_mct: для поточечно растущей и равномерно ограниченной последовательности интегрируемых функций последовательность их интегралов есть процесс Коши — is_Cauchy. Опирается на riemann_sum_monotone (поточечное $f\le g$ влечёт $\int f\le \int g$) и monotone_bounded_Cauchy. Цена — classic (L3); новых аксиом нет. В коде утверждение доказано для самодостаточного рационального интеграла-суммы $\int f=w{\sum }_{i}f(x_i)$; перенос на $L^1$-интегральный слой — содержательное чтение той же схемы (она использует лишь монотонность и ограниченность интегрального процесса), а не отдельная теорема этой главы. ↩

3. Предикат dominated в ProcessFatou.v: $\forall kx,|f_k(x)|\le g(x)$, где $g$ — параметр. Это прямое P4-чтение (методология предъявления данных, а не аксиома, используемая файлом): существование $\to$ предъявление. ↩

4. dct_diff_bound в ProcessDCT.v (0 аксиом): опирается на аддитивность сумм и покомпонентное неравенство треугольника q_sum_abs_le. ↩

5. dct_dom_bound в ProcessDCT.v (0 аксиом). ↩

6. process_dct в ProcessDCT.v (0 аксиом): из сходимости невязок $\int |f_n-f|\to 0$ следует сходимость интегралов. Пакет process_dct_dominated объединяет конверт и сжатие. ↩

7. process_fatou_nonneg и process_fatou_bounded в ProcessFatou.v (0 аксиом); dominated_integral_bound — оценка разности интегралов через мажоранту. ↩