Глава 5. Аналитический мост eval и теорема Таннери: замыкание уравнения логарифма

Замысел главы: что мы соединяем

К этой главе у нас два готовых, но ещё не соединённых куска. Из Главы 16.3 — формальное сердце $e^{-\ln (1-x)}=1/(1-x)$: равенство формальных рядов, на коэффициентах, 0-аксиомное. Из Главы 16.4 — ${\exp }_R$, вещественная экспонента процесса, с теоремой сложения и инъективностью. Один кусок — тождество о коэффициентах; другой — оператор над числами-процессами. Эта глава их сводит и достигает цели всей Части XVI: настоящего функционального уравнения логарифма над числами-процессами,

$$L(x)+L(y)\sim L(x\oplus y),x\oplus y:=x+y-xy,$$

где $L(x)=-\ln (1-x)$ — логарифм-процесс, а $\sim$ — равенство чисел-процессов.

Мост держится на двух новых инструментах. Первый — гомоморфизм вычисления $\mathrm{eval}$: формальный ряд, оценённый в точке, становится числом-процессом, и эта оценка уважает всю алгебру Главы 16.2. Второй — теорема Таннери: аналитическая лицензия переставить предел с бесконечной суммой. Без неё диагональ ${\exp }_R$ и одношаговое суммирование ряда не склеить.

Ярус, как и в Главе 16.4, — аналитический, на L3. Но ядро здесь на удивление чистое: сама теорема Таннери, затухание $n{z}^n\to 0$, конечная перестановка Фубини и аддитивность $\mathrm{eval}$ — аксиомо-свободны; L3 входит лишь в финальную сборку равенств.

Мост вычисления: $\mathrm{eval}${eval} как гомоморфизм

Формальный ряд — это коэффициент-процесс (Глава 16.1). Зафиксируем точку $x$, $0\le x<1$. Частичные суммы $\sum a_n{x}^n$ образуют Коши-процесс — значение ряда в точке:

$$\mathrm{eval}ax:=\mathrm{serie}{\mathrm{s}}_{\mathrm{l}}\mathrm{imit}\left({\sum }_n{a}_n{x}^n\right).$$

Это вычисление — гомоморфизм из формального исчисления Главы 16.2 в числа-процессы:

$$\mathrm{eval}(a+b)x\sim \mathrm{eval}ax+\mathrm{eval}bx,\mathrm{eval}(a\cdot b)x\sim \mathrm{eval}ax\cdot \mathrm{eval}bx,\mathrm{eval}(a^k)x\sim (\mathrm{eval}ax{)}^k,$$

где слева $\cdot$ — свёртка рядов, справа — произведение процессов. И оно отождествляет именные ряды с их классическими значениями:

$$\mathrm{eval}‘ex{p}_{f}ps‘t\sim \exp (t),\mathrm{eval}‘log1m_{f}ps‘x\sim L(x).$$

Здесь $L$ — всюду в главе положительный логарифм-процесс $L(x)=-\ln (1-x)={\sum }_{n\ge 1}{x}^n/n$; соответственно log1m_fps читается как ряд для $-\ln (1-x)$, а не для $\ln (1-x)$. То есть $\mathrm{eval}$ играет роль функтора <<формальное $\to$ аналитическое>> (в категориальном чтении; в самой формализации это гомоморфизм оценки, без отдельного categorical-слоя): он переносит коэффициентную алгебру Главы 16.2 в равенства чисел и закрепляет двух героев — экспоненту и логарифм — за их аналитическим смыслом.¹

Формальное сердце, оценённое

Формальное сердце Главы 16.3 было равенством рядов $E\circ L=‘geom‘$. Применим $\mathrm{eval}$ в точке $x$:

$$\mathrm{eval}(‘ex{p}_{f}ps‘\circ ‘log1m_{f}ps‘)x\sim \frac{1}{1-x}.$$

Тождество, жившее на коэффициентах, теперь держится как равенство чисел-процессов — в каждой точке $0\le x<1$. Под капотом оценка композиции требует конечной перестановки Фубини — на стадии $n$ поменять порядок суммирования в $\mathrm{eval}(f\circ g)$, — которая законна при $g(0)=0$ и сама аксиомо-свободна. Так мост переносит формальное сердце на ту сторону — конечной ценой.²

Теорема Таннери: аналитический клей

Остаётся зазор. ${\exp }_R(L(x))$ — по построению Главы 16.4 — это диагональ: ${\exp }_R(P)={\mathrm{diag}}_n\exp (P_n)$, экспонента берётся от рациональных приближений процесса $P=L(x)$, а потом диагонализируется. Значение же $\mathrm{eval}(E\circ L)x$ — это один ряд, просуммированный сразу. Чтобы доказать их равенство, надо переставить два предельных перехода: диагональ по $n$ (приближение $L(x)$) и бесконечную сумму по ряду экспоненты. Наивная перестановка предела и бесконечной суммы незаконна. Лицензию даёт теорема Таннери.

Сформулируем. Пусть двойная последовательность $a(k,n)\ge 0$ мажорируется почленно суммируемой мажорантой $a(k,n)\le M(k)$ (с сходящейся ${\sum }_{k}M(k)$) и при каждом фиксированном $k$ столбец $a(k,n)\to 0$ при $n\to \infty$. Тогда диагональная частичная сумма стремится к нулю:

$$\sum _{k<n}a(k,n)\underset{n\to \infty }{\to }0.$$

Мы пользуемся именно этой специализированной хвостовой формой Таннери — занулением диагональной ошибки, — а не общим переходом ${\lim }_n{\sum }_k={\sum }_k{\lim }_n$: для нашей перестановки её достаточно. Две детали делают её нужным и притом честным инструментом:

• Мажоранту здесь поставляет затухание $n{z}^n\to 0$: $k$-й блок ограничен ${\sigma }^k$ при суммируемом $\sigma <1$ — ровно $M(k)$ Таннери.
• Теорема Таннери в нашей системе аксиомо-свободна — <>, — и таковы же затухание $n{z}^n\to 0$ и конечный Фубини. Аналитический клей, лицензирующий перестановку, вполне конструктивен; L3 несут лишь обрамляющие конструкции вещественных равенств (series_limit, ${\exp }_R$).

Итог — ключевая лемма-стык:

$${\exp }_R(L(z))\sim \mathrm{eval}(E\circ L)z.$$

Диагональная экспонента логарифма-процесса равна одношаговой оценке формальной композиции.³

Ключ, мультипликативный замок и замыкание

Сцепим стык с оценённым сердцем:

$${\exp }_R(L(z))\sim \mathrm{eval}(E\circ L)z\sim \frac{1}{1-z}.$$

Это ключ: вещественная экспонента логарифма-процесса есть геометрический процесс, представляющий $1/(1-z)$. Формальное сердце Главы 16.3, поднятое экспонентой Главы 16.4 и мостом Главы 16.5, становится утверждением о настоящих вещественных числах.

У геометрического процесса своя групповая арифметика:

• он обратен к $(1-z)$: $(1-z)\cdot \frac{1}{1-z}\sim 1$;
• произведения умножаются по закону дополнительных множителей,

$$\frac{1}{1-x}\cdot \frac{1}{1-y}\sim \frac{1}{1-(x\oplus y)},x\oplus y=x+y-xy.$$

Странный аргумент $x\oplus y$ — не случайность: это ровно то, что заставляет дополнения перемножаться, $(1-x)(1-y)=1-(x\oplus y)$. Отсюда же и область: при $0\le x<1$ и $0\le y<1$ имеем $1-(x\oplus y)=(1-x)(1-y)>0$, так что $0\le x\oplus y<1$ — и $L(x\oplus y)$ определён (ровно гипотезы, на которых стоит формализованное уравнение).

Теперь всё на месте, чтобы замкнуть уравнение. Прочтём цепочку:

$${\exp }_R(L(x)+L(y))\sim {\exp }_R(L(x))\cdot {\exp }_R(L(y))\sim \frac{1}{1-x}\cdot \frac{1}{1-y}\sim \frac{1}{1-(x\oplus y)}\sim {\exp }_R(L(x\oplus y)),$$

где первый шаг — теорема сложения Главы 16.4, средние — ключ и закон $\oplus$, последний — ключ наоборот. Оба конца суть ${\exp }_R$ от чего-то; по инъективности ${\exp }_R$ (Глава 16.4)

$$L(x)+L(y)\sim L(x\oplus y),\text{то есть}L(x)+L(y)\sim L(x+y-xy).$$

Это и есть ln_mul_closed. Утверждение, которое система прежде несла лишь как горизонт — выписанное как Prop, намеренно не подделанное через Admitted, — теперь доказанная теорема.⁴

Разбор E/R/R, ярус и что глава достигла

компонент главы	роль в системе	слой E/R/R
частичные суммы $\mathrm{eval}$, конечные свёртки и блоки на стадии $n$	носители, конечны	Element (P4)
$\mathrm{eval}$ — гомоморфизм оценки	мост формальное $\to$ аналит.\ (функтор.\ чтение)	Role
ключ и замыкание $L(x)+L(y)\sim L(x\oplus y)$	аддитивность $L$ над $\oplus$	Role
Таннери, $n{z}^n\to 0$, конечный Фубини	аксиомо-свободные оценки	Rule (0 акс.)
геом.\ групповой закон, ключ, инъективность ${\exp }_R$	процесс-оценки	Rule (L3)

Elements. На каждой стадии $n$ — конечные рациональные частичные суммы $\mathrm{eval}$, конечные перестановки Фубини, конечные блоки Таннери. Element-сторона цела.

Roles. $\mathrm{eval}$ — роль гомоморфизма оценки (формальное $\to$ аналитическое); Таннери — роль лицензии перестановки; ${\exp }_R$ и $L$ — вещественная экспонента и логарифм-процесс; функциональное уравнение — роль аддитивности $L$ над мультипликативным $\oplus$.

Rules. Затухание $n{z}^n\to 0$, геометрический групповой закон, ключ, инъективность — правила, по которым процесс-оценки собираются в замкнутое уравнение.

Диагностика P4 и ярус. Всё движение — настоящий вещественный анализ над $Q$-процессами; его аналитическое замыкание опирается на L3, как помечено начиная с Главы 16.4. Но аналитическое ядро необычно чисто — разделение проверено машинно (Print Assumptions):

аксиомо-свободно (0 акс., <>)	только L3 (Classical_Prop.classic)
tannery, n_times_pow_limit, eval_compose_swap, eval_add	eval_mul, eval_exp, eval_log1m, eval_pow, eval_compose_exp_log1m_geom, geom_inv, geom_mul, ln_mul_from_key, boss, exp_R_ln_proc_is_geom, ln_mul_closed

То есть теорема Таннери, затухание $n{z}^n\to 0$, конечный Фубини и аддитивность $\mathrm{eval}$ не зависят ни от одной аксиомы; L3 входит лишь в сборку вещественных равенств.

Что нового. Герои — Мертенс, Таннери, функциональное уравнение логарифма — классический анализ. Ново — (а) $\mathrm{eval}$ как явный гомоморфизм, переносящий формальные тождества в равенства чисел-процессов; (б) конструктивное, аксиомо-свободное прочтение Таннери и кормящего его затухания; (в) замыкание уравнения, которое система несла как открытый горизонт (не Admitted) — теперь теорема; (г) структурное прочтение $x+y-xy$ как закона, перемножающего дополнения. Уровень — новое обрамление и сборка классического анализа над процессами.

Что глава достигла. Число $\to$ функция: функция есть процесс (16.1); исчисление таких процессов (16.2); композиция и формальное сердце (16.3); вещественная экспонента процесса (16.4); и теперь — аналитический мост, замыкающий настоящее функциональное уравнение (16.5). Лестница в одной ступени от вершины: Глава 16.6 прочтёт всю лестницу реификации число $\to$ функция $\to$ функционал, где сам $\mathrm{eval}$ — отображение, берущее функцию и возвращающее число, — и есть первый функционал.

---

---

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

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

Footnotes

1. src/FPSEval.v (32 Qed, 0 Admitted): eval_add — аксиомо-свободна; eval_mul, eval_pow, eval_exp ($\mathrm{eval}‘ex{p}_{f}ps‘t\sim ‘ex{p}_{l}imit‘t$), eval_log1m ($\mathrm{eval}‘log1m_{f}ps‘x\sim ‘l{n}_{p}roc‘x$) — без новых аксиом, только L3. Машинно проверено. ↩

2. src/FPSEval.v: eval_compose_exp_log1m_geom ($\mathrm{eval}(E\circ L)x\sim ‘geometri{c}_{l}imit‘x$) — без новых аксиом, только L3; её опора eval_compose_swap (конечный Фубини при $g(0)=0$) — аксиомо-свободна. ↩

3. src/Tannery.v (4 Qed, 0 Admitted): tannery — аксиомо-свободна. src/PolyTimesGeom.v (2 Qed): n_times_pow_limit ($n{z}^n\to 0$) — аксиомо-свободна. Стык boss (src/LnMulClosed.v) — без новых аксиом, только L3. Машинно проверено. ↩

4. src/LnMulReduction.v (6 Qed, 0 Admitted): geom_inv, geom_mul (закон $\oplus$), ln_mul_from_key (<<ключ $\Rightarrow$ уравнение>>). src/LnMulClosed.v (11 Qed, 0 Admitted): exp_R_ln_proc_is_geom (ключ), ln_mul_closed (замыкание). Без новых аксиом, только L3. Сама формулировка-Prop ln_mul_functional_equation живёт в src/Log2FunctionalEq.v (7 Qed, 0 Admitted) как горизонт — здесь он снят. Машинно проверено. ↩