Глава 3. Композиция, цепное правило и формальное сердце E∘ L

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

Глава 16.2 дала исчисление: коэффициент-процессы перемножаются свёрткой и дифференцируются формально, с правилами Лейбница и степени. Остался последний инструмент анализа — композиция, $f\circ g$, и её цепное правило. С ними часть достигает своей вершины.

Вершина эта — конкретное тождество:

$$e^{-\ln (1-x)}=\frac{1}{1-x}.$$

Оно говорит, что экспонента и $-\ln (1-x)$ взаимно гасят друг друга до геометрической. И именно это тождество было препятствием всей программе <<функция — процесс>>. Пока функция оставалась внешним отображением, тождество обратности высказывалось о функции как о целом, поперёк всей области, — и поточечная, процессная машинерия его <<не видела>>. Это было диагностировано как второпорядковая граница финитизации: не стена, а недостроенный объект — функция, ещё не ставшая процессом.

Эта глава снимает препятствие. Реифицировав функцию коэффициент-процессом (Глава 16.1) и построив на нём исчисление (Глава 16.2), мы превращаем тождество обратности в коэффициентную процесс-рекуррентность: все коэффициенты ряда $e^{-\ln (1-x)}$ оказываются равны единице — то есть это геометрическая, — и проверяется это конечной индукцией, 0-аксиомно. Препятствие было не стеной, а объектом, ждавшим реификации.

Порядок главы: композиция рядов и почему условие $g(0)=0$ делает её конечной (§ 16.3.2); цепное правило (§ 16.3.3); структурное сердце — единственность решения ОДУ геометрической (§ 16.3.4); и сборка — формальное сердце $e^{-\ln (1-x)}=1/(1-x)$ (§ 16.3.5). Завершает — разбор E/R/R и честная граница: это сердце формальное (на коэффициентах); аналитический мост к равенству чисел-процессов строит Глава 16.5, опираясь на процессную экспоненту Главы 16.4 (§ 16.3.6).

Композиция рядов

Подставить один ряд в другой — значит вычислить $f(g(x))$ покоэффициентно. Если $f={\sum }_k{f}_k{y}^k$, то $f(g(x))={\sum }_k{f}_{k}g(x{)}^k$, и коэффициент при $x^n$ собирается из всех степеней $g^k$ (с соглашением $g^0=‘fp{s}_{o}ne‘$ — единичный ряд):

$$(f\circ g{)}_n=\sum _{k=0}^n{f}_k(g^k{)}_n.$$

Definition fps_compose (f g : FPS) : FPS :=
  fun n => partial_sum (fun k => f k * fps_pow g k n) n.

Здесь есть тонкость, и ToS разрешает её конечностью. Бесконечная подстановка ${\sum }_k{f}_k{g}^k$ угрожала бы бесконечной суммой на каждом коэффициенте. Но при условии $g(0)=0$ — у $g$ нет свободного члена — степень $g^k$ имеет порядок не ниже $k$: первые $k$ её коэффициентов нулевые.¹ Значит при $k>n$ слагаемое $f_k(g^k{)}_n$ зануляется, и сумма по $k$ усекается до $k\le n$: каждый $(f\circ g{)}_n$ — конечная сумма. Условие $g(0)=0$ — не техническое ограничение, а ровно то, что делает композицию корректной операцией над коэффициент-процессами: подстановка ряда без свободного члена считается за конечное число шагов. И в нуле композиция ведёт себя как положено: $(f\circ g)(0)=f(0)$.²

Цепное правило

Композиция согласована с формальной производной обычным цепным правилом — при том же условии $g(0)=0$:

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

³

На уровне коэффициентов это равенство свёрток, и доказывается оно тем же геометрическим приёмом, что ассоциативность из § 16.2.3: двойную сумму по треугольнику $(i,k)$ удаётся переписать квадратом и поменять порядок суммирования, а зануление высоких степеней ($(g^k{)}_i=0$ при $k>i$) обрезает лишнее. Этот квадрат-треугольник-своп с занулением — ядро цепного правила.⁴ Классическое цепное правило, обычно выводимое через пределы разностных отношений, здесь — конечное тождество коэффициентов.

Структурное сердце: ОДУ геометрической

Прежде чем собрать тождество, нужен один структурный факт — о том, что геометрическая функция однозначно определяется простым дифференциальным уравнением.

Сам ряд geom удовлетворяет уравнению $‘geom{‘}^{\prime }=‘geom‘\cdot ‘geom‘$ — то есть $h^{\prime }=h\cdot ‘geom‘$ при $h=‘geom‘$ (эквивалентно $(1-x)h^{\prime }=h$).⁵ И — это ключ — никакая другая функция-процесс с условием $h(0)=1$ уравнению $h^{\prime }=h\cdot ‘geom‘$ не удовлетворяет:

$$h^{\prime }=h\cdot ‘geom‘\text{и}h(0)=1⟹h=‘geom‘.$$

⁶

Почему единственность так прозрачна на коэффициентах. Поскольку geom есть ряд из одних единиц, свёртка с ней есть просто частичная сумма: $(h\cdot ‘geom‘{)}_n={\sum }_{i\le n}{h}_i$.⁷ Поэтому уравнение $h^{\prime }=h\cdot ‘geom‘$ на коэффициентах есть рекуррентность

$$(n+1)h_{n+1}=\sum _{i=0}^n{h}_i.$$

С начальным условием $h_0=1$ она разматывается однозначно: $h_1=h_0=1$; $2h_2=h_0+h_1=2$, то есть $h_2=1$; и индукцией — если $h_0,\dots ,h_n$ все единицы, то ${\sum }_{i\le n}{h}_i=n+1$, и значит $(n+1)h_{n+1}=n+1$, откуда $h_{n+1}=1$. Все коэффициенты равны единице — это и есть geom. Дифференциальное уравнение пришпиливает геометрическую как свою единственную нормированную функцию-процесс, и делает это конечной индукцией.

Формальное сердце: $e^{-\ln (1-x)}=1/(1-x)${e^(-ln(1-x)) = 1/(1-x)}

Теперь собираем вершину. Рассмотрим композицию $h:=\exp \circ (-\ln (1-x))$ — то есть подстановку ряда $-\ln (1-x)$ в экспоненту. (Здесь $‘log1m_{f}ps‘$ обозначает именно ряд $-\ln (1-x)={\sum }_{n\ge 1}{x}^n/n$ — положительный логарифмический ряд, а не $\ln (1-x)$; знак выбран так, что производная есть $+‘geom‘$.) Подстановка корректна: у $-\ln (1-x)$ нет свободного члена, $(-\ln (1-x))(0)=0$, так что § 16.3.2 применимо.

Покажем, что $h$ удовлетворяет тому самому ОДУ. По цепному правилу (§ 16.3.3):

$$h^{\prime }=({\exp }^{\prime }\circ (-\ln (1-x)))\cdot (-\ln (1-x){)}^{\prime }.$$

Но обе производные известны из § 16.2.4: экспонента есть собственная производная, ${\exp }^{\prime }=\exp$; а производная $-\ln (1-x)$ есть геометрическая, $(-\ln (1-x){)}^{\prime }=‘geom‘$. Подставляя:

$$h^{\prime }=(\exp \circ (-\ln (1-x)))\cdot ‘geom‘=h\cdot ‘geom‘.$$

И начальное условие: $h(0)=\exp ((-\ln (1-x))(0))=\exp (0)=1$. Итак, $h^{\prime }=h\cdot ‘geom‘$ и $h(0)=1$ — а по структурному сердцу § 16.3.4 такое $h$ единственно и равно geom. Значит

$$\boxed{e^{-\ln (1-x)}=\frac{1}{1-x}}$$

на уровне коэффициент-процессов: все коэффициенты формального ряда $e^{-\ln (1-x)}$ равны единице, то есть это геометрическая.⁸

Вот в чём смысл этого результата для нашей программы. Тождество обратности — то самое, что сопротивлялось, пока функция была внешним отображением, — стало конечной процесс-рекуррентностью $c_n=1$ и доказано машинной индукцией без единой аксиомы. Препятствие растворилось: оно было не стеной, а функцией, ещё не ставшей процессом. Реификация дала ей бытие процесса — и тождество, прежде невидимое, стало проверяемым.

Разбор E/R/R и что глава готовит

компонент главы	роль в системе	слой E/R/R
коэффициенты и усечённые суммы ${\sum }_{k\le n}$	носители и счёт	Element (P4)
композиция $=$ подстановка ряда	роль-подстановка	Role
ОДУ $h^{\prime }=h\cdot ‘geom‘$, $h(0)=1$	роль-ограничение, пришпиливает geom	Rule
цепное правило, единственность ОДУ, сердце $c_n=1$	процесс-рекуррентности	Rule (конструктивно)

Elements. Композиция при $g(0)=0$ есть конечная усечённая сумма ${\sum }_{k\le n}{f}_k(g^k{)}_n$; рекуррентность сердца $(n+1)h_{n+1}={\sum }_{i\le n}{h}_i$ — конечный шаг. Всё считается за конечное число операций над коэффициентами.

Roles. Композиция играет роль подстановки одного ряда в другой; дифференциальное уравнение играет роль ограничения, единственным решением которого (при $h(0)=1$) оказывается геометрическая.

Rules. Цепное правило, единственность решения ОДУ и само сердце $e^{-\ln (1-x)}=1/(1-x)$ — это равенства коэффициентных процессов, проверяемые конечной индукцией.

Диагностика P4. До реификации тождество обратности было второпорядковым утверждением о функции как о целом — поперёк всей области, и потому невидимым поточечной, процессной машинерии. Реифицировав функцию коэффициент-процессом, мы превращаем его в семейство первопорядковых равенств коэффициентов — рекуррентность $c_n=1$, конечную на каждом шаге (Element). Граница финитизации функций здесь пересечена на формальном коэффициентном уровне; аналитический перенос к числам-процессам остаётся задачей следующих глав.

Что нового и честная граница. Композиция рядов, цепное правило, единственность решения ОДУ и тождество $e^{-\ln (1-x)}=1/(1-x)$ — классическая математика формальных рядов. Ново обрамление: препятствие, прежде стоявшее перед программой <<функция — процесс>>, прочитано как недостроенный объект и снято реификацией, а вся цепочка до конкретного тождества обратной функции проверена машинно, без аксиом.⁹ Честная граница: это сердце — формальное, на уровне коэффициентов. Что вычисленный ряд $e^{-\ln (1-x)}$ равен геометрической как число-процесс в каждой точке $|x|<1$ — отдельное, аналитическое утверждение; его строит Глава 16.5 через мост вычисления, и для него нужна процессная экспонента вещественного аргумента.

Что глава готовит. Формальное сердце получено на коэффициентах. Чтобы перенести его в равенство чисел-процессов, нужна экспонента, умеющая брать в аргумент не рациональное число, а целый процесс — вещественную ${\exp }_R$. Её строит Глава 16.4: из теоремы Мертенса о произведении рядов — к теореме сложения, гомоморфизму групп $(Q,+)\to (R^{+},\times )$ и инъективности.

---

---

Часть: Часть XVI. Функция как процесс · Том: «Математика»

Навигация: ← Глава 2. Исчисление функций-процессов · Глава 4. Процессная экспонента exp_ℝ →

Footnotes

1. src/FormalPowerSeries.v (37 Qed, 0 Admitted, 0 аксиом): fps_pow_low_order — если $g(0)=0$, то $(g^k{)}_i=0$ при $i<k$. Машинно проверено, 0 аксиом. ↩

2. Там же: fps_compose_zero. Машинно проверено, 0 аксиом. ↩

3. src/FormalPowerSeries.v: fps_chain_rule (при $g(0)=0$). Машинно проверено, 0 аксиом. ↩

4. Там же: conv_compose_swap — база цепного правила (partial_sum_swap $+$ fps_pow_low_order). Машинно проверено, 0 аксиом. ↩

5. src/FormalPowerSeries.v: geom_satisfies_ode — $‘fp{s}_{d}eriv‘‘geom‘=‘fp{s}_{m}ul‘‘geom‘‘geom‘$. Машинно проверено, 0 аксиом. ↩

6. Там же: ode_geom_unique. Машинно проверено, 0 аксиом. ↩

7. Там же: conv_ones — $‘conv‘a‘geom‘n=‘partia{l}_{s}um‘an$. ↩

8. src/FormalPowerSeries.v: compose_exp_log1m_is_geom — $‘fp{s}_{c}ompose‘‘ex{p}_{f}ps‘‘log1m_{f}ps‘=‘geo{m}_{f}ps‘$. Машинно проверено, 0 аксиом. ↩

9. Весь материал главы — из src/FormalPowerSeries.v (37 Qed, 0 Admitted, 0 аксиом; Print Assumptions = «Closed under the global context» для ключевых лемм, включая compose_exp_log1m_is_geom). ↩