Глава 3. Пикар–Линделёф: оператор-сжатие на пространстве функций

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

Гарантия сходимости

Глава 8.1 установила, что решение задачи Коши есть процесс приближений; Глава 8.2 предъявила простейший такой процесс — ломаную Эйлера — и вычислила его на эталонных уравнениях. Но один вопрос остался открытым: почему процесс приближений сходится? Ломаная Эйлера — это последовательность рациональных стадий; что гарантирует, что они сближаются, а не разбегаются? Настоящая глава даёт гарантию, и она — центральный результат Части VIII.

Гарантию даёт теорема Пикара–Линделёфа в её процессном прочтении. Её классическая форма звучит так: оператор Пикара

$$\Phi (y)(t)=y_0+{\int }_{t_0}^{t}f(s,y(s))ds$$

есть сжатие на пространстве функций $y(\cdot )$, а у сжатия по банаховой схеме есть единственная неподвижная точка — решение. Здесь существенно слово пространство функций: $\Phi$ действует не на число, а на целую функцию-кандидат, и сжимает расстояние между функциями. Именно эта формулировка — сжатие на функциях — и есть подлинная теорема Пикара–Линделёфа.

Что эта глава утверждает — и что нет

Честная оговорка о том, что здесь новое. Предыдущий слой формализации тома доказывал сжатие для скалярной итерации Эйлера–Пикара — отображения $y\mapsto y_0+f(y)h$ одного рационального значения в другое, с коэффициентом $Lh$.¹ Это важный, но не тот же результат: подлинная теорема требует сжатия оператора $\Phi$ на целых функциях $t\mapsto y(t)$, а не на отдельных значениях. Настоящая глава предъявляет именно функция-space теорему — и она доказана.²

Ключ, делающий бесконечномерную теорему конечной над ℚ: пространство функций на сетке $[0,T]$ — это $Q^{N+1}$, набор значений в $N+1$ узлах. Расстояние между двумя функциями-кандидатами — равномерная оценка их рассогласования по узлам (sup-метрика). Над таким конечным пространством сжатие, геометрический зазор и единственность — точные алгебраические факты без единой аксиомы.

Чего глава не делает: геометрический зазор итератов доказан алгебраически, но его чтение как $\epsilon$-Коши-сходимости (<<для всякого $\epsilon$ найдётся номер>>) использует затухание $(LT{)}^n\to 0$, а завершённая функция-предел — ещё один роль-предел; эти два шага наследуют закон исключённого третьего (L3) и в этой главе не актуализируются.³ И глобальное во времени продолжение решения — отдельная граница (§ «Локальное существование и его граница»).

Три уровня строгости. Первый — сжатие оператора Пикара на грид-функциях, геометрический зазор итератов и единственность решения на сетке: доказаны над ℚ без аксиом. Второй — процессные чтения: пространство функций как $Q^{N+1}$, решение как роль-предел Коши-процесса итераций, существование как геометрическое сближение. Третий — завершённый предел и глобальное решение — роль-пределы и L3-слой.

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

Каркас в порождающем порядке Rules $\to$ Roles $\to$ Elements; полный разбор — в § «Разбор в порождающем порядке». Опираемся на авторскую E/R/R-шапку файла ProcessPicardOperator.v.⁴ Глава вводит систему оператора Пикара как сжатия.

Rules (Правила, $\leftrightarrow$ L5). Оператор Пикара на сетке $\Phi (y{)}_k=y_0+h{\sum }_{j<k}f(t_j,y_j)$; при липшицевости $f$ он есть сжатие в sup-метрике с коэффициентом $L\cdot T$ (где $T=Nh$ — длина интервала); итераты ${\Phi }^n$ имеют геометрический зазор $(LT{)}^n$; при $LT<1$ неподвижная точка единственна.

Roles (Роли, $\leftrightarrow$ L4). Оператор $\Phi$ — роль-отображение функций; равномерная оценка по узлам — роль-метрика; итерат ${\Phi }^n$ — роль-приближение; неподвижная точка — роль-решение; условие $LT<1$ — роль-режим (где процесс сжимается).

Elements (Элементы, $\leftrightarrow$ L1$+$P4). Грид-функции $y:\{0,\dots ,N\}\to Q$, их значения $y_k$, конечные суммы ${\sum }_{j<k}$, индекс узла $k\le N$. Под P4 завершённая функция-предел — вне элементов: актуальны конечные грид-функции и итераты.

Оператор Пикара и пространство функций над сеткой

Интегральная форма задачи Коши (Глава 8.1) задаёт оператор, перерабатывающий функцию-кандидат $y(\cdot )$ в новую функцию:

$$\Phi (y)(t)=y_0+{\int }_{t_0}^{t}f(s,y(s))ds.$$

На рациональной сетке $t_k=kh$ интеграл становится процессом накопления Части V — левой суммой по узлам, а оператор — конечной формулой:

$$\Phi (y{)}_k=y_0+h\sum _{j<k}f(t_j,y_j).$$

Здесь $y=(y_0,y_1,\dots ,y_N)$ — грид-функция, набор значений в узлах, а $\Phi (y)$ — такая же грид-функция.⁵ Так классически бесконечномерное пространство функций $C([0,T])$ оборачивается конечным пространством $Q^{N+1}$ — значениями в $N+1$ узлах.

Расстояние между двумя кандидатами $y$ и $z$ — их максимальное рассогласование по узлам, sup-метрика:

$$\text{supnorm}y-z=\underset{k\le N}{\max }|y_k-z_k|.$$

На конечной сетке этот максимум — просто наибольшее из $N+1$ рациональных чисел, без всякого предела.

Оператор Пикара $\Phi$ — роль-отображение: он перерабатывает всю функцию-кандидата целиком, а не отдельное значение. <<Пространство функций>>, на котором он действует, — роль-арена, и над ℚ на сетке она конечна: $Q^{N+1}$. Решение — та функция, которую $\Phi$ оставляет на месте.

Оператор Пикара есть сжатие

Центральная теорема главы: при липшицевости правой части оператор Пикара есть сжатие в sup-метрике с коэффициентом $L\cdot T$. Развёрнуто: для любых двух грид-функций $y,z$, рассогласованных не более чем на $D$ во всех узлах, образы $\Phi (y),\Phi (z)$ рассогласованы не более чем на $(L\cdot T)D$:

$$(\forall k\le N:|y_k-z_k|\le D)⟹\forall k\le N:|\Phi (y{)}_k-\Phi (z{)}_k|\le (L\cdot T)D.$$

Механизм прозрачен. Разность образов есть просуммированная разность наклонов:

$$\Phi (y{)}_k-\Phi (z{)}_k=h\sum _{j<k}[f(t_j,y_j)-f(t_j,z_j)].$$

Каждое слагаемое липшицево: $|f(t_j,y_j)-f(t_j,z_j)|\le L|y_j-z_j|\le LD$. Слагаемых — ровно $k$, а поскольку $k\le N$, их не больше $N$; поэтому сумма по модулю не превосходит $N\cdot LD$, а умножение на шаг даёт

$$|\Phi (y{)}_k-\Phi (z{)}_k|\le h\cdot N\cdot LD=(L\cdot Nh)D=(L\cdot T)D.$$

Это и есть сжатие с коэффициентом $L\cdot T$.⁶ Сжатие в собственном смысле — когда коэффициент меньше единицы: $L\cdot T<1$, то есть интервал достаточно короток ($T<1/L$).

Сравним со скалярным слоем. Скалярная итерация Эйлера–Пикара сжимала расстояние между числами с коэффициентом $Lh$ (шаг); здесь сжимается расстояние между функциями с коэффициентом $LT$ (вся длина интервала). Первое — про один шаг, второе — про весь оператор на пространстве кандидатов. Подлинная теорема Пикара–Линделёфа — именно вторая, и её процессное ядро — сжатие на пространстве грид-функций — теперь доказано, конечно и над ℚ.

Сжатие — роль-правило: оно говорит, что применение оператора сближает любые две функции-кандидата в фиксированное число раз. Коэффициент $L\cdot T$ — роль-темп этого сближения; условие $LT<1$ — роль-режим, в котором процесс итераций гарантированно сходится.

Следствия: геометрический зазор и единственность

Итераты сближаются геометрически

Из сжатия следует, что последовательные итерации оператора сближаются геометрически. Запустим процесс с постоянной функции $y^{(0)}\equiv y_0$ и будем применять $\Phi$; тогда зазор между соседними итерациями убывает как степень коэффициента:

$$\text{supnorm}{\Phi }^{n+1}-{\Phi }^n\le (L\cdot T{)}^n\text{supnorm}{\Phi }^1-{\Phi }^0.$$

При $LT<1$ степени $(LT{)}^n$ убывают, и зазоры стягиваются — это и есть Коши-содержание процесса: итерации в конце концов сближаются сколь угодно тесно.⁷ Подчеркнём честно: геометрический зазор доказан без аксиом; переход от него к самой Коши-сходимости в форме <<для всякого $\epsilon$ найдётся номер>> и к завершённому пределу использует затухание $(LT{)}^n\to 0$, наследующее L3.

Решение единственно — без аксиом

Сжатие даёт и единственность, причём — что примечательно — конструктивно, без закона исключённого третьего. Пусть $y$ и $z$ — две неподвижные точки оператора на сетке ($\Phi (y)=y$ и $\Phi (z)=z$ во всех узлах). Возьмём их максимальное рассогласование $D^{\ast }={\max }_{k\le N}|y_k-z_k|$ — наибольшее из $N+1$ рациональных чисел. Поскольку обе функции неподвижны, сжатие даёт для каждого узла

$$|y_k-z_k|=|\Phi (y{)}_k-\Phi (z{)}_k|\le (L\cdot T)D^{\ast },$$

а значит и максимум подчиняется той же оценке: $D^{\ast }\le (L\cdot T)D^{\ast }$. При $LT<1$ это возможно лишь при $D^{\ast }=0$ — то есть $y$ и $z$ совпадают во всех узлах.⁸ Существенно, что максимум берётся по конечной сетке: это рациональное число, а не предел, и потому единственность не требует L3 — в отличие от существования завершённого предела.

Единственность — роль-жёсткость: у сжатия не может быть двух разных неподвижных точек. Доказанная конструктивно через конечный максимум, она показывает, что роль-решение определено однозначно ещё до того, как мы спросим о его завершённом пределе. Существование (Коши-зазор) и единственность — две стороны одного сжатия.

Локальное существование и его граница

Теорема главы — локальная. Коэффициент сжатия есть $L\cdot T$, и режим гарантированной сходимости — $L\cdot T<1$, то есть интервал короче $1/L$. На таком интервале процесс итераций Пикара — Коши (геометрический зазор), а решение единственно. Это локальное существование и единственность: на достаточно коротком отрезке.

Классически отсюда строят глобальное решение: дойдя до конца интервала, берут полученное значение за новое начальное условие и продолжают на следующий отрезок, и так далее. Это продолжение (continuation). Но глобальная картина — продолжение на всё время, анализ возможного обращения решения в бесконечность за конечное время (blow-up), максимальный интервал существования — в нашей формализации не доказана. Это честная P4-граница: завершённое решение на неограниченном интервале — роль-предел, а теорема о продолжении — направление, а не построенный результат.

Локальность — не дефект, а точное содержание над ℚ: гарантия касается режима $LT<1$. Глобальное решение — роль-предел процесса продолжений, к которому ведёт повторное применение локальной теоремы; как завершённый объект на всём времени оно не строится.

E/R/R-разбор: оператор Пикара как Роль-сжатие

Постановка

Разберём построенную систему — оператор Пикара как сжатие — в терминах E/R/R, читая авторскую E/R/R-шапку файла ProcessPicardOperator.v.⁹ Это онтологическое осмысление и чтение шапки, а не приписывание коду новых утверждений. Как и прежде, аббревиатура задаёт эпистемический порядок (Elements $\to$ Roles $\to$ Rules); разбор ведём в порождающем, Rules $\to$ Roles $\to$ Elements.

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

Rules (Правила, $\leftrightarrow$ L5). В основании — оператор Пикара $\Phi (y{)}_k=y_0+h{\sum }_{j<k}f(t_j,y_j)$, перерабатывающий грид-функцию в грид-функцию. Над ним — правило сжатия: при липшицевости $f$ оператор сближает любые два кандидата в sup-метрике с коэффициентом $L\cdot T$. Из сжатия следуют геометрический зазор итератов $(LT{)}^n$ (Коши-содержание) и единственность неподвижной точки. Универсальный слой включает L3 там, где мы хотим прочитать геометрический зазор как $\epsilon$-сходимость и завершённый предел; само конечное сжатие и единственность как алгебраические факты его не требуют. Конкретный слой — формула оператора и условие $LT<1$.

Roles (Роли, $\leftrightarrow$ L4). Правила задают роли. Оператор $\Phi$ — роль-отображение функций. Равномерная оценка по узлам ($\text{supnorm}\cdot$) — роль-метрика на пространстве кандидатов. Итерат ${\Phi }^n$ — роль-приближение. Условие $LT<1$ — роль-режим (где сжатие работает). Неподвижная точка — роль-решение, а её завершённый предел — роль-предел: то, к чему стягивается Коши-процесс, не актуализируемое как функция-объект.

Elements (Элементы, $\leftrightarrow$ L1$+$P4). Носители конечны: грид-функции $y:\{0,\dots ,N\}\to Q$, их значения $y_k\in Q$, конечные суммы ${\sum }_{j<k}$, индекс узла $k\le N$, коэффициент $L\cdot T\in Q$. Под P4 <<пространство всех функций>> и завершённый предел не суть элементы: арена на сетке есть конечное $Q^{N+1}$, актуальны грид-функции и итераты.

Компонент	Что фиксирует	E/R/R
оператор $\Phi (y{)}_k=y_0+h\sum f$; сжатие rate $LT$; зазор $(LT{)}^n$; единственность	КАК оператор сжимает и почему процесс сходится	Rules ($L5$)
$\Phi$ роль-оператор; sup-метрика; итерат ${\Phi }^n$; режим $LT<1$; решение/предел	ЗАЧЕМ значимы носители: роли в сжатии	Roles ($L4$)
грид-функции $y_k\in Q$; суммы ${\sum }_{j<k}$; узел $k\le N$; $LT\in Q$	ЧТО есть на каждой стадии (конечно, P4)	Elements ($L1$, P4)

Проверка сформированности и что даёт разбор

{ Система сформирована корректно: каждый компонент попадает ровно в одну E/R/R-категорию, и нет самоотнесения (P1). Существенно, чего здесь нет: оператор Пикара не берёт своей ареной <<пространство всех функций>> как завершённый бесконечномерный объект. Арена на сетке — конечное $Q^{N+1}$, метрика — максимум по конечному набору узлов, а единственность доказывается через этот конечный максимум без предельного перехода. Именно эта конечность арены отделяет доказанное (сжатие, зазор, единственность — 0 аксиом) от границы (завершённый предел — L3-слой).}

Что даёт разбор. Он переводит центральный результат на язык структуры: оператор Пикара — это Роль-отображение функций, сжатие — Правило сближения, неподвижная точка — Роль-решение, а грид-функции и их значения — Элементы (конечные на каждой стадии). Брать <<пространство функций>> как завершённый бесконечномерный объект или <<решение>> как готовую функцию-предел значит ставить роль-арену или роль-предел на место Элемента — то же смешение категорий, что <<точка как объект>> вместо класса (Глава 4.3) или <<ряд как завершённая сумма>> вместо семейства усечений (Глава 7.1). Процессное ядро теоремы Пикара–Линделёфа здесь есть, и оно конечно: сжатие на $Q^{N+1}$, геометрическое сближение итератов и единственность неподвижной точки на сетке. Переход к завершённой функции-решению остаётся роль-пределом.

Имея гарантию сходимости, следующая глава обращается к устойчивости: как расходятся решения с разными начальными данными, как контролирует это расхождение неравенство Гронуолла и в каком смысле классический множитель $e^{Lt}$ — роль-предел процесса роста, а не предзаданная экспонента.

---

---

Часть: Часть VIII. Обыкновенные дифференциальные уравнения · Том: «Математика»

Навигация: ← Глава 2. Метод Эйлера: решение на сетке · Глава 4. Устойчивость, единственность, неравенство Гронуолла →

Footnotes

1. euler_picard_contraction в ProcessPicard.v: сжатие отображения $Q\to Q$ с коэффициентом $Lh$ при $Lh<1$. Это скалярная итерация: сжимается расстояние между числами, а не между функциями. ↩

2. Опорный файл — ProcessPicardOperator.v (Rocq-репозиторий ToS): оператор Пикара на грид-функциях, теорема о сжатии в sup-метрике (picard_op_contraction), геометрический зазор итератов (picard_iter_gap) и единственность решения на сетке (picard_unique). Ключевые теоремы — 0 аксиом (Print Assumptions: <>). ↩

3. Обёртка <<итераты сходятся к пределу>> идёт через iterate_is_cauchy / Qpow_vanish в FixedPoint.v, наследующие classic. Сжатие, зазор и единственность — 0 аксиом; предел — L3-слой. ↩

4. Шапка размечает прямо: Rules — $\Phi (y{)}_k=y_0+h{\sum }_{j<k}f(t_j,y_j)$, Липшиц $\Rightarrow$ $\Phi$ сжатие, rate $L\cdot T$; Roles — $\Phi$ роль-оператор, равномерная оценка роль-метрика; Elements — грид-функции, значения $y_k$, конечные суммы. ↩

5. picard_sum $=‘q_{s}um‘(\lambda j.f(t_j,y_j))k$ и picard_op$(y{)}_k=y_0+h\cdot ‘picar{d}_{s}um‘yk$ в ProcessPicardOperator.v; узлы $t_j=‘tgrid‘j=j\cdot h$, длина $T=‘Tlen‘=N\cdot h$. ↩

6. picard_diff_bound (оценка разности сумм Пикара индукцией по $k$) и picard_op_contraction (сжатие с коэффициентом $L\cdot ‘Tlen‘$) в ProcessPicardOperator.v, 0 аксиом. Коэффициент $L\cdot T=L\cdot Nh$. ↩

7. picard_iter_gap в ProcessPicardOperator.v: $\text{supnorm}{\Phi }^{n+1}-{\Phi }^n\le (L\cdot T{)}^n{C}_0$, где $C_0$ — оценка первого зазора; доказано индукцией по $n$ через теорему о сжатии. 0 аксиом. ↩

8. picard_unique в ProcessPicardOperator.v: единственность неподвижной точки на сетке. Максимум по конечной сетке реализован как gmax — наибольшее из $N+1$ рациональных значений; отсюда $D^{\ast }\le (LT)D^{\ast }$ и $LT<1$ дают $D^{\ast }=0$ без обращения к пределу. 0 аксиом. ↩

9. Шапка файла ведёт разбор прямо: Rules — $\Phi (y{)}_k=y_0+h{\sum }_{j<k}f(t_j,y_j)$, Липшиц $\Rightarrow$ сжатие rate $L\cdot T$, итераты с зазором $(LT{)}^n$, единственность неподвижной точки; Roles — $\Phi$ роль-оператор, равномерная оценка роль-метрика, ${\Phi }^n$ роль-приближение, неподвижная точка роль-решение; Elements — грид-функции, значения $y_k$, конечные суммы, $k\le N$. ↩