Глава 2. Исчисление функций-процессов

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

Глава 16.1 дала носитель: функция реифицирована как коэффициент-процесс $‘FPS‘=N\to Q$, и по нему прошла граница Element/role-limit (многочлен против неполиномиального ряда). Но носитель без операций инертен. Чтобы реифицированные функции жили — складывались, умножались, дифференцировались, — на коэффициент-процессах нужно исчисление.

Эта глава его строит. По свёртке Коши формальные степенные ряды несут кольцевую структуру: умножение коммутативно, ассоциативно и с единицей (коммутативный моноид), сложение и масштаб поточечны, а формальная производная согласована с умножением правилами Лейбница и степени. И у всего этого исчисления есть одна общая черта, ради которой стоит затевать реификацию: каждая операция здесь — конечная арифметика коэффициентов. Ни одного предела, ни одного $\epsilon$-$\delta$. Сумма, произведение, производная функции-процесса вычисляются за конечное число шагов из конечного числа коэффициентов. Исчисление целиком лежит на Element-стороне — и оттого 0-аксиомно.

Порядок главы. Сперва — поточечные сложение и масштаб и не-поточечное умножение, свёртка Коши (§ 16.2.2). Затем — кольцевые законы: коммутативность, ассоциативность, единица (§ 16.2.3). Затем — формальная производная и наблюдение, что у функции-процесса она есть Element-операция, а не предел (§ 16.2.4). Затем — правила Лейбница и степени (§ 16.2.5). И наконец — разбор E/R/R с переходом к композиции и цепному правилу (§ 16.2.6), на которых Глава 16.3 соберёт формальное сердце тождества $e^{-\ln (1-x)}=1/(1-x)$.

Сложение, масштаб и свёртка

Две операции на коэффициент-процессах поточечны и потому тривиально Element. Сложение складывает коэффициенты, масштаб умножает их на константу:

$$(a+b{)}_n=a_n+b_n,(c\cdot a{)}_n=c{a}_n.$$

Каждая стадия $n$ — одно рациональное сложение или умножение.¹

Умножение функций не поточечно. Коэффициент произведения $f\cdot g$ есть свёртка Коши — конечная сумма всех произведений коэффициентов, индексы которых дают $n$:

$$(f\cdot g{)}_n=\sum _{i+j=n}{f}_i{g}_j=\sum _{i=0}^n{f}_i{g}_{n-i}.$$

Это не произвол, а единственный закон, при котором коэффициент-процессы перемножаются как функции: ровно так перемножаются ряды $\left({\sum }_i{a}_i{x}^i\right)\left({\sum }_j{b}_j{x}^j\right)$. И — ключевое для P4 — каждый $(f\cdot g{)}_n$ есть конечная сумма: индексов $i+j=n$ при данном $n$ конечно много. Умножение функций-процессов — роль-свёртка: правило, собирающее из двух коэффициент-процессов третий, и собирающее за конечное число шагов.²

Definition fps_mul (f g : FPS) : FPS := conv f g.   (* (f*g)_n = sum_{i+j=n} f_i*g_j *)

Кольцевая структура: коммутативность, ассоциативность, единица

Свёртка наделяет коэффициент-процессы структурой коммутативного кольца с единицей — и каждый кольцевой закон проверяется на коэффициентах.

Коммутативность: $f\cdot g=g\cdot f$. На уровне коэффициентов это симметрия суммы ${\sum }_{i+j=n}{f}_i{g}_j$ относительно перестановки $i\leftrightarrow j$.³

Единица: ряд $‘fp{s}_{o}ne‘=(1,0,0,\dots )$ (коэффициент $1$ при $x^0$, дальше нули) есть нейтральный элемент: $‘fp{s}_{o}ne‘\cdot f=f$.⁴

Ассоциативность: $(f\cdot g)\cdot h=f\cdot (g\cdot h)$ — самый содержательный закон. Обе стороны равны одной тройной сумме Коши ${\sum }_{i+j+k=n}{f}_i{g}_j{h}_k$; чтобы свести к ней левую и правую группировки, нужно перегруппировать треугольник индексов $\{(i,j):j\le i\le n\}$ по столбцу. Этот треугольный Fubini-своп конечных сумм пришлось доказать отдельно — в прежней библиотеке его не было; на нём ассоциативность и стоит.⁵

Вместе эти законы означают: по свёртке формальные ряды образуют коммутативный моноид с единицей $‘fp{s}_{o}ne‘$, а с поточечными сложением и масштабом — кольцевую структуру над $Q$. Машинно подтверждены именно мультипликативные законы свёртки (коммутативность, ассоциативность, единица) и их согласование с производной (ниже); дистрибутивность свёртки над поточечным сложением и законы аддитивной группы рутинны и отдельными леммами не выделены.⁶ Реифицированные функции получили алгебру. Первый её нетривиальный факт уже встречался в Главе 16.1: определяющее уравнение геометрической $(1-x)\cdot \frac{1}{1-x}=1$ — это в точности утверждение, что $‘geo{m}_{f}ps‘$ есть обратный к $(1-x)$ в этом кольце. То, что в Главе 16.1 было первым свидетельством <<функция-процесс работает>>, теперь видно как равенство в кольце функций-процессов.

Формальная производная: дифференцирование без предела

Производная на коэффициент-процессе задаётся одним правилом: коэффициент при $x^n$ у $f^{\prime }$ есть $(n+1)c_{n+1}$ — сдвиг индекса на единицу и умножение на номер:

$$(f^{\prime }{)}_n=(n+1)c_{n+1},\text{ибо}\frac{d}{dx}\sum _n{c}_n{x}^n=\sum _n(n+1)c_{n+1}{x}^n.$$

Definition fps_deriv (f : FPS) : FPS := fun n => inject_Z (Z.of_nat (S n)) * f (S n).

И здесь — наблюдение, ради которого реификация и затевалась. Классически производная есть предел разностного отношения — объект role-limit-стороны, $\epsilon$-$\delta$, бесконечный процесс приближения. Но у функции, реифицированной как коэффициент-процесс, производная — это конечная арифметика: сдвиг последовательности на один шаг и умножение $n$-го члена на $(n+1)$. Ни предела, ни анализа. Дифференцирование функции-процесса есть Element-операция: оно считается, а не пределяется. То, что классически живёт на role-limit-стороне, на реифицированной функции переходит на Element-сторону — ровно как умножение свелось к конечной свёртке.

И реифицированные базовые функции удовлетворяют своим определяющим тождествам на уровне коэффициентов — в формальном смысле, как равенства коэффициент-процессов, без всякой сходимости. Формальная экспонента есть неподвижная точка формальной производной: $(e^x{)}^{\prime }=e^x$, потому что $(n+1)\cdot \frac{1}{(n+1)!}=\frac{1}{n!}$. А ряд $-\ln (1-x)$ — это и есть $‘log1m_{f}ps‘$ (с коэффициентами $c_0=0$, $c_{k+1}=1/(k+1)$) — даёт геометрическую: $(-\ln (1-x){)}^{\prime }=\frac{1}{1-x}$, потому что $(n+1)\cdot \frac{1}{n+1}=1$ — постоянный коэффициент геометрической. Оба тождества — не предельные переходы, а конечные равенства коэффициентов.⁷

Правило Лейбница и правило степени

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

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

На уровне коэффициентов это равенство свёрток, и доказывается оно конволюционной рекуррентностью — факториальной формой тождества Вандермонда, без всяких биномиальных коэффициентов.⁸

Из Лейбница индукцией получается правило степени. Степень ряда определяется обычной рекурсией — $g^0=‘fp{s}_{o}ne‘$, $g^{k+1}=g\cdot g^k$, — и для неё

$$(g^{k+1}{)}^{\prime }=(k+1)g^k{g}^{\prime }.$$

Доказательство — индукция по $k$ поверх правила Лейбница, с одним применением ассоциативности ($g\cdot (g^k\cdot g^{\prime })=(g\cdot g^k)\cdot g^{\prime }=g^{k+1}\cdot g^{\prime }$) и коммутативности, чтобы собрать слагаемые. Кольцо § 16.2.3 здесь работает в полную силу.⁹

Эти два правила — последний кусок исчисления перед композицией. Имея производную, Лейбница и степень, Глава 16.3 построит цепное правило $(f\circ g{)}^{\prime }=(f^{\prime }\circ g)\cdot g^{\prime }$ — и через него получит формальное сердце $e^{-\ln (1-x)}=1/(1-x)$.

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

компонент главы	роль в системе	слой E/R/R
коэффициенты $c_n\in Q$, конечные суммы ${\sum }_{i+j=n}$	носители и счёт	Element (P4)
умножение $=$ свёртка Коши	роль-свёртка	Role
производная $=$ сдвиг $+$ умножение на $(n+1)$	роль-операция	Role
свёртка: коммут.{/}ассоц.{/}единица (моноид)	алгебра носителя	Rule (конструктивно)
Лейбниц и степень	согласование производной с кольцом	Rule (конструктивно)

Elements. Всё, чем оперирует глава, — рациональные коэффициенты и конечные суммы по индексам $i+j=n$. Каждая стадия конечно-актуальна; ни одного завершённо-бесконечного объекта.

Roles. Умножение играет роль свёртки, производная — роль сдвига с весом. Это операции над функцией-процессом, превращающие носитель в живую алгебру с дифференцированием.

Rules. Кольцевые законы (коммутативность, ассоциативность, единица) и правила исчисления (Лейбниц, степень) суть правила согласования. Каждое — равенство коэффициентов, проверяемое конечным счётом; ассоциативность опёрта на треугольный Fubini-своп, которого в библиотеке не было.

Диагностика P4. Всё исчисление функций-процессов — конечная арифметика коэффициентов: сумма, свёртка, сдвиг-с-весом. Здесь нет ни одного предела. Поэтому, в отличие от классического анализа, где умножение рядов и дифференцирование тянут за собой сходимость, формальное исчисление целиком на Element-стороне и 0-аксиомно. Резкая формулировка: на реифицированной функции дифференцирование — это счёт, а не предел. И здесь точная грань P4: бесконечность относится к целому объекту-ряду (role-limit), а не к отдельной коэффициентной операции — каждый коэффициент суммы, свёртки и производной вычисляется конечным правилом. Целый ряд может быть role-limit, но всякий коэффициентный шаг остаётся Element.

Что нового. Кольцевая структура формальных рядов (коммутативный моноид свёртки и поточечное сложение), формальная производная, правила Лейбница и степени — классическая алгебра. Ново здесь обрамление: исчисление построено на коэффициент-процессе (функция-как-процесс из § 16.1), и каждая операция прочитана как конечно-актуальная Element-операция; плюс конструктивная деталь — ассоциативность свёртки через треугольный Fubini-своп. Уровень — новое обрамление, при честном 0-аксиомном построении всего исчисления.¹⁰

Что глава готовит. У нас есть кольцо функций-процессов и производная с правилами Лейбница и степени. На них Глава 16.3 строит композицию рядов (корректную при $g(0)=0$) и цепное правило, а через них — формальное сердце $e^{-\ln (1-x)}=1/(1-x)$: тождество обратной функции, ставшее проверяемой процесс-рекуррентностью на коэффициентах.

---

---

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

Навигация: ← Глава 1. Граница финитизации на уровне функций · Глава 3. Композиция, цепное правило и формальное сердце E∘ L →

Footnotes

1. src/FormalPowerSeries.v (37 Qed, 0 Admitted, 0 аксиом): fps_add, fps_neg, fps_sub, fps_scale — все поточечны по коэффициентам. ↩

2. Там же: fps_mul := conv — умножение FPS есть свёртка Коши conv. Машинно проверено, 0 аксиом. ↩

3. src/FormalPowerSeries.v: conv_comm (переиндексация $i\mapsto n-i$). Машинно проверено, 0 аксиом. ↩

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

5. Там же: conv_assoc через partial_sum_triangle_swap (перегруппировка треугольной двойной суммы). Машинно проверено, 0 аксиом. ↩

6. Там же: fps_mul_comm, fps_mul_assoc, fps_mul_one_l, fps_mul_one_r — мультипликативные законы свёртки (коммутативный моноид над conv). Машинно проверено, 0 аксиом. ↩

7. src/FormalPowerSeries.v: exp_fps_deriv ($‘fp{s}_{d}eriv‘‘ex{p}_{f}ps‘=‘ex{p}_{f}ps‘$) и log1m_deriv ($‘fp{s}_{d}eriv‘‘log1m_{f}ps‘=‘geo{m}_{f}ps‘$). Машинно проверено, 0 аксиом. ↩

8. src/FormalPowerSeries.v: fps_deriv_mul — правило Лейбница на коэффициентах. Машинно проверено, 0 аксиом. ↩

9. Там же: fps_pow (степень ряда), fps_pow_deriv и fps_pow_deriv_eq — правило степени. Машинно проверено, 0 аксиом. ↩

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