Глава 4. Производная

Зачем производная без деления

Что построили предыдущие главы

Часть V строит анализ слой за слоем. Глава 5.1 ввела расстояние и показала, что между процессами оно само есть процесс. Глава 5.2 построила топологию: открытые шары, окрестности, компактность. Глава 5.3 определила непрерывность — через $δ$ - $ε$ , доказала теорему о промежуточном значении бисекцией и теорему об экстремуме сеткой. К этому моменту у нас есть аппарат, которым можно сказать: функция непрерывна — её значения не делают скачков.

Производная — следующий слой. Она отвечает не на вопрос <<делает ли функция скачки>>, а на вопрос <<с какой скоростью она меняется>>. От непрерывности к гладкости: от того, что приращение мало при малом шаге, к тому, что приращение линейно по шагу с точностью до поправки высшего порядка. Непрерывность уже дала нам $δ$ - $ε$ -язык; производная надстраивается прямо над ним, и потому глава многократно будет ссылаться на § 5.3.

Деление и предел как проблема

Классическое определение производной выглядит так:

f^{'} (x) = h \to 0 lim \frac{f ( x + h ) - f ( x )}{h} .

Прежде чем переносить его в ToS, стоит точно понять, что здесь составляет трудность, а что — нет.

Не составляет трудности деление на ненулевой рациональный шаг. Если $h$ — конкретное ненулевое рациональное число, то $(f (x + h) - f (x)) / h$ — совершенно законное рациональное выражение; ничего проблемного в нём нет, и ниже в этой главе мы будем таким делением свободно пользоваться.

Трудность — в другом, и она двойная. Во-первых, классическое определение делает первичным объектом предел отношения при $h \to 0$ . Но $h$ при этом пробегает значения, стремящиеся к нулю, а на нуль делить нельзя; чтобы предел был определён, нужно рассматривать частное на всё более мелких шагах и переходить к пределу. Во-вторых, сам этот предел — завершённый объект << $lim$ >>, а завершённых пределов под $P 4$ нет: <<действительное>> в ToS само есть процесс. Нужна формулировка, в которой предел частного при $h = 0$ не стоит на месте первичного определения.

Division-free критерий: $o (h)$ {Division-free критерий: o(h)}

Первый слой производной в ToS — это критерий: правило, отвечающее на вопрос <<какое число $L$ является производной функции $f$ в точке $x$ >>. И формулируем мы этот критерий без деления.

Идея проста. Сказать <<наклон $f$ в точке $x$ равен $L$ >> — значит сказать, что приращение $f (x + h) - f (x)$ хорошо приближается линейным выражением $L \cdot h$ . Насколько хорошо? Так, что ошибка приближения мала по порядку $h$ : меньше любой наперёд заданной доли от $∣ h ∣$ . Запишем это:

\forall ε > 0 \exists δ > 0 \forall h : 0 < ∣ h ∣ < δ ⟹ f (x + h) - f (x) - L \cdot h < ε \cdot ∣ h ∣.

Деления здесь нет. Есть оценка вида $o (h)$ — ошибка линейного приближения убывает быстрее, чем сам шаг. В Rocq это определение носит имя has_derivative и записано в файле Differentiation.v:

Definition has_derivative (f : Q -> Q) (x L : Q) : Prop :=
  forall eps : Q, 0 < eps ->
    exists delta : Q, 0 < delta /\
      forall h : Q, 0 < Qabs h -> Qabs h < delta ->
        Qabs (f (x + h) - f x - L * h) < eps * Qabs h.

Прочтём внимательно. $L \cdot h$ — линейное приближение приращения. Разность $f (x + h) - f (x) - L \cdot h$ — ошибка этого приближения. Критерий требует, чтобы ошибка была меньше $ε \cdot ∣ h ∣$ — то есть сколь угодно малой долей шага — коль скоро шаг достаточно мал. Предел тут присутствует не как завершённый объект, а как $ε$ - $δ$ -квантор — ровно тот же приём, которым в § 5.3 определялась $δ$ - $ε$ -непрерывность. Критерий говорит, какое $L$ есть производная, не делая предел частного первичным.

Отметим точно уровень типа (предохранитель Части V). Здесь $f : Q \to Q$ — функция, переводящая рациональное число в рациональное. Это не процесс и не функция на фактор-классах RealPoint; глава работает с рационально-значными функциями рационального аргумента, и это honest-ограничение названо сразу.

Ещё одна деталь требует слова. Шаг $h$ берётся ненулевым: условие записано как $0 < ∣ h ∣ < δ$ . Главная причина — содержательная: производная проверяет поведение функции при малых ненулевых сдвигах, то есть в проколотой окрестности точки $x$ . Нулевой шаг неинформативен: при $h = 0$ оценка обращается в $0 < 0$ слева и истинна тривиально, локального содержания она не несёт. В коде ненулевость $h$ вдобавок помогает обойти технические тонкости рационального представления и отношения Qeq — но это вторичный мотив, а не основной. Тот же приём применялся к continuous_at в § 5.3; это сознательная деталь, не недосмотр.

Производная-процесс: `deriv_process` и мост{Производная-процесс: deriv_process и мост}

Критерий § 4.1.3 говорит, какое число $L$ является производной. Но сам он $L$ не вычисляет: это предикат, проверка, а не построение. Для вычислительной стороны нужен второй слой — производная как процесс.

Идея процессного слоя прямо отвечает онтологии $P 4$ . Вместо того чтобы говорить о пределе при $h \to 0$ , мы фиксируем конкретную убывающую последовательность ненулевых шагов

h_{n} = \frac{1}{n + 1} (n = 0, 1, 2, \dots)

и на каждом шаге считаем обычное разностное отношение. Получаем процесс: на уровне $n$ — рациональное число $(f (x + h_{n}) - f (x)) / h_{n}$ . Под $P 4$ производная — не завершённый предел этого процесса, а сам процесс пошаговых рациональных приближений наклона. В файле ProcessDerivative.v это записано так:

Definition deriv_step (n : nat) : Q :=
  1 / inject_Z (Z.of_nat (S n)).
 
Definition deriv_process (f : Q -> Q) (x : Q) : RealProcess :=
  fun n =>
    let h := deriv_step n in
    (f (x + h) - f x) / h.

{ Здесь деление есть — но это деление на $h_{n}$ , а $h_{n}$ заведомо положительно: лемма deriv_step_pos устанавливает $0 < h_{n}$ для всякого $n$ . Это законное деление на ненулевой рациональный шаг, а не запретный предел при $h = 0$ . На простейших функциях процесс ведёт себя ожидаемо: deriv_process_const показывает, что для константы он эквивалентен постоянному процессу $0$ , а deriv_process_id — что для тождества $w \mapsto w$ он эквивалентен постоянному процессу $1$ .}

{ Два слоя — критерий и процесс — связывает мост: теорема deriv_process_converges. Она утверждает: если $L$ есть производная $f$ в точке $x$ в смысле критерия has_derivative, то процесс разностных отношений эквивалентен постоянному процессу $L$ :

‘ ha s_{d} er i v a t i v e ‘ f x L ⟹ ‘ d er i v_{p} r ocess ‘ f x \sim ‘ co n s t_{p} r ocess ‘ L .

Содержательно мост говорит: division-free критерий и вычислительный процесс согласованы — число $L$ , удовлетворяющее критерию, есть в точности то, к чему сходится процесс разностных отношений. Доказательство прямое: критерий даёт $δ$ , лемма deriv_step_vanishes находит уровень $N$ , начиная с которого $h_{n} < δ$ , и тогда $(f (x + h) - f (x)) / h - L = ∣ f (x + h) - f (x) - L h ∣/∣ h ∣ < ε$ . Из моста немедленно следуют ещё два факта: deriv_process_cauchy (процесс разностных отношений есть процесс Коши) и derivative_is_process_construction (производная предъявляется как Коши-процесс, эквивалентный постоянному $L$ — E/R/R-форма результата).}

Стоит развести три статуса, чтобы дальше не путать (предохранитель Части V). has_derivative — это критерий, предикат. deriv_process — это процесс, конструкция. deriv_process_converges — это теорема-мост между ними. Три разные вещи, и глава всякий раз будет указывать, о которой речь.

И здесь же — важная оговорка о том, чем deriv_process не является. Сам по себе процесс разностных отношений — это кандидат на производную, а не полное определение дифференцируемости. Он берёт одну фиксированную последовательность положительных шагов $h_{n} = 1/ (n + 1)$ — то есть, по сути, это правосторонний процесс разностных отношений. Поэтому его сходимость сама по себе не заменяет двусторонний критерий has_derivative, который проверяет все малые ненулевые $h$ , в обе стороны. Классический контрпример — функция $∣ x ∣$ в нуле: правосторонние разностные отношения сходятся к $1$ , но двусторонней производной нет (к этому примеру глава вернётся в § 4.3.3). Полный смысл производной задаёт именно has_derivative; теорема deriv_process_converges утверждает лишь одно направление — если производная существует в division-free смысле, то выбранный процесс разностных отношений к ней сходится. Определять дифференцируемость как << процесс deriv_process есть процесс Коши >> было бы ошибкой.

Про статус аксиом: ProcessDerivative.v в шапке заявляет << 0 axioms, 16 Qed >>; он импортирует ProcessCore, ProcessArithmetic и Differentiation. К сквозной оговорке о том, что заголовок файла не заменяет аудита конкретной теоремы, глава вернётся в § 4.8.

Разбор E/R/R: производная как система

Производная — система, и к ней приложима методология E/R/R (Часть I). Разбор разворачивает разметку из заголовка опорного файла, где она дана прямо: элементы — разностные отношения; роль — Cauchy-процесс, сходящийся к наклону; правило — условие has_derivative.¹ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе — та же, что в Главах 5.1–5.3: речь о функциях $Q \to Q$ , не об отображениях фактор-классов; <<система>> — содержательная онтологическая интерпретация, не объект System $L$ .

Rules — правила (закон $L 5$ ). Конституция производной — division-free критерий $o (h)$ (has_derivative, § 4.1.3): ошибка линейного приближения меньше $ε \cdot ∣ h ∣$ . Это правило говорит, какое число есть наклон, не делая предел частного первичным. К конституции примыкает конкретный слой — правила дифференцирования (линейность § 4.2, произведение и степень § 4.4), мост между критерием и процессом (§ 4.1.4) и единственность наклона (§ 4.5.1). Над $Q$ у правил есть усиление: для теоремы о среднем нужна не поточечная, а равномерная дифференцируемость (udiff_on, § 4.6) — та же перестановка кванторов, что отличала равномерную непрерывность в § 5.3.

Roles — значимость позиций (закон $L 4$ ). Центральная роль — наклон: коэффициент линейного приближения, который дифференцирование присваивает функции в точке. По $L 4$ эта роль структурно обоснована: критерий $o (h)$ выделяет наклон однозначно (единственность, § 4.5.1). Вычислительную сторону роли несёт процесс разностных отношений — Cauchy-процесс, сходящийся к наклону (так роль и названа в заголовке файла). Сама функция при этом получает одну из качественных позиций: дифференцируема, равномерно дифференцируема.

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — функции $Q \to Q$ , а в процессе — разностные отношения $q (n) = (f (x + h_{n}) - f (x)) / h_{n}$ при $h_{n} = 1/ (n + 1)$ . По $L 1$ наклон, если существует, тождественен себе (единствен). По $P 4$ носители процесса конечны на каждом шаге — рациональные разностные отношения, обозримые на любом уровне; завершённого <<предела при $h \to 0$ >> нет, производная актуальна как процесс приближений наклона.

Сведём разбор в таблицу.

Компонент	Что фиксирует	E/R/R
функции $Q \to Q$ ; разностные отношения $q (n)$	носители	Element
наклон $L$ ; процесс, сходящийся к наклону	роли	Role
$o (h)$ -критерий `has_derivative`	конституция (division-free)	Rule (конструкт.)
линейность, произведение, степень	правила дифференцирования	Rule (конструкт.)
мост критерий–процесс; единственность наклона	согласование	Rule
равномерная дифференцируемость (`udiff`)	усиление для среднего	Rule
законы $L 1$ – $L 5$	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: функции и разностные отношения суть элементы, наклон — роль, критерий $o (h)$ — правило. Производная как роль определена корректно: критерий выделяет наклон единственным (§ 4.5.1) — это $L 1$ для роли. Самореференции нет: критерий квантифицирует по шагам $h$ и стоит над значениями функции — по $L 5$ операция выше операндов. Производная хорошо сформирована.

Разбор проясняет устройство главы. Два слоя — критерий и процесс — это различение правила и носителя: $o (h)$ -критерий (Rule) говорит, что есть наклон, а процесс разностных отношений (Element-конструкция) его приближает; мост § 4.1.4 их связывает. Отсюда и предостережение § 4.1.4 о функции $∣ x ∣$ : односторонний процесс — лишь кандидат-носитель, а определяет производную именно двусторонний критерий-правило. А липшицевость § 4.7.3 показывает, как Rules производной порождают то, что в § 5.3 приходилось требовать для непрерывности. И тот же разбор задаёт образец Части V: каждое аналитическое понятие читается как система со своей E/R/R-структурой.

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

Дальше глава движется так. § 4.2 — базовые правила дифференцирования: производная константы, тождества, линейность. § 4.3 — связь с § 5.3: дифференцируемость влечёт непрерывность. § 4.4 — произведение и степень, главные нелинейные правила. § 4.5 — единственность производной и приложение к оптимизации: теорема Ферма. § 4.6 — теорема о среднем через <<walk-точки>>. § 4.7 — следствия теоремы о среднем: монотонность, липшицевость. § 4.8 — итог.

{ Опорных файлов три. Differentiation.v — division-free критерий и правила. ProcessDerivative.v — производная как процесс и мост к критерию. MeanValueTheorem.v — сеточная теорема о среднем и её следствия. Все три в своих шапках заявляют статус << AXIOMS: none >>; точную оговорку о том, что этот заголовок означает и чего не означает, глава даёт в § 4.8.}

Базовые правила дифференцирования

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

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

Первая лемма — экстенсиональность по функции. Если две функции $f$ и $g$ поточечно равны, то есть $f w = g w$ для всякого $w$ , то производная одной есть производная другой. В Differentiation.v это has_derivative_ext: из forall w, f w == g w и has_derivative f x L следует has_derivative g x L. Доказательство очевидно — разность $g (x + h) - g (x) - L h$ поточечно равна $f (x + h) - f (x) - L h$ , и оценка переносится без изменений.

Вторая лемма — экстенсиональность по значению производной. Если $L = L^{'}$ как рациональные числа (в смысле Qeq), то $L^{'}$ есть производная всякий раз, когда $L$ есть производная. Это has_derivative_eq. Вместе обе леммы означают: понятие <<производная>> корректно определено — оно не различает поточечно равные функции и не различает Qeq-равные значения. Дальше мы этим пользуемся не оговариваясь.

Простейшие случаи: константа и тождество

Два простейших правила задают базу для всего остального.

Производная константы есть нуль. Если $f$ — постоянная функция $w \mapsto c$ , то её производная в любой точке равна $0$ . В коде это deriv_const. Доказательство тривиально: ошибка линейного приближения здесь

c - c - 0 \cdot h = 0,

то есть тождественно нулевая, и неравенство $0 < ε \cdot ∣ h ∣$ выполнено при любом положительном $ε$ и ненулевом $h$ . Содержательно: постоянная функция не меняется, её скорость изменения — нуль.

Производная тождества есть единица. Для функции $w \mapsto w$ производная в любой точке равна $1$ — это deriv_id. Ошибка приближения опять тождественно нулевая:

(x + h) - x - 1 \cdot h = 0.

Содержательно: тождественная функция меняется с той же скоростью, с какой меняется аргумент. Эти два правила — deriv_const и deriv_id — послужат базой индукции в § 4.4.3, где из них вырастет степенное правило.

Линейность производной

Дифференцирование — линейная операция. Это означает четыре правила, собранные в SECTION 2 файла Differentiation.v.

Производная скалярного кратного: $(c \cdot f)^{'} = c \cdot f^{'}$ . Если $L$ есть производная $f$ , то $c \cdot L$ есть производная функции $w \mapsto c \cdot f (w)$ — это deriv_scale. Производная противоположной функции: $(- f)^{'} = - f^{'}$ — это deriv_neg. Производная суммы: $(f + g)^{'} = f^{'} + g^{'}$ — это deriv_sum. Производная разности: $(f - g)^{'} = f^{'} - g^{'}$ — это deriv_sub.

Приём доказательства суммы стоит назвать, он типичен для всей главы. Ошибка линейного приближения суммы раскладывается на две ошибки:

(f (x + h) + g (x + h)) - (f (x) + g (x)) - (L_{f} + L_{g}) h = (f (x + h) - f (x) - L_{f} h) + (g (x + h) - g (x) - L_{g} h) .

Каждое слагаемое мало по своей производной; чтобы их сумма уложилась в $ε \cdot ∣ h ∣$ , для каждого берётся оценка с $ε /2$ , и неравенство треугольника для модуля собирает результат. Этот приём дробления $ε$ на части — общий для всех правил, где приращение распадается на сумму.

Отметим экономию средств. Правило разности deriv_sub не доказывается заново: оно выводится из deriv_sum и deriv_neg через экстенсиональные леммы § 4.2.1 — разность $f - g$ переписывается как сумма $f + (- g)$ , и результат переносится. Каждое следующее правило встаёт поверх уже доказанных, а не строится с нуля.

Линейность переносится и в процессный слой. Файл ProcessDerivative.v поднимает сумму и скалярное кратное в процессную форму: deriv_sum_process утверждает, что процесс разностных отношений суммы $f + g$ эквивалентен постоянному процессу $L_{f} + L_{g}$ , а deriv_scale_process — что процесс для $c \cdot f$ эквивалентен постоянному процессу $c \cdot L$ . Оба доказываются единообразно и коротко: применяется мост deriv_process_converges, а затем соответствующее правило deriv_sum или deriv_scale из Differentiation.v. То есть процессные правила — надстройка над правилами-критериями через мост § 4.1.4, а не отдельные доказательства.

Что значит линейность для теории

Линейность производной — не случайное совпадение, а отражение устройства самого определения. В критерии has_derivative приближающее выражение — это $L \cdot h$ , и оно линейно по $h$ . Дифференцирование сопоставляет функции её линейное приближение; и коль скоро приближение линейно, линейные операции над функциями переходят в линейные операции над приближениями. Сумма функций даёт сумму наклонов, скалярное кратное — кратный наклон.

Стоит, однако, заранее предупредить: на этом линейность кончается. Произведение двух функций линейным правилом не описывается — наклон произведения не есть произведение наклонов. Почему так и каким правилом произведение всё же описывается — предмет § 4.4.

Дифференцируемость влечёт непрерывность

Гладкое — это непрерывное

Глава 5.3 ввела непрерывность; настоящий раздел связывает её с производной. Утверждение простое: если функция дифференцируема в точке, то она в этой точке непрерывна. В Differentiation.v это deriv_implies_continuous: из has_derivative f x L следует continuous_at f x, где continuous_at — определение непрерывности из § 5.3.

Содержательно связь очевидна. Если приращение $f (x + h) - f (x)$ приближается линейным $L \cdot h$ с ошибкой порядка $o (h)$ , то само приращение мало при малом шаге: оно не больше суммы линейной части $∣ L ∣ \cdot ∣ h ∣$ и малой ошибки. И то и другое стремится к нулю вместе с $h$ — значит, $f$ не делает скачка в точке $x$ .

Доказательство уточняет, как именно выбрать $δ$ для непрерывности. Берётся $δ$ как минимум двух величин: $δ$ , доставленного критерием производной при $ε = 1$ , и числа $ε / (∣ L ∣ + 1)$ . На таком шаге ошибка приближения меньше $∣ h ∣$ , а линейная часть — меньше $∣ L ∣ \cdot ∣ h ∣$ ; сумма не превосходит $(∣ L ∣ + 1) \cdot ∣ h ∣$ , что по выбору $δ$ меньше $ε$ . Полный код приводить не будем — важна идея: $δ$ непрерывности собирается из $δ$ производной и поправки на величину наклона.

Ограниченность вблизи точки

Из непрерывности извлекается ещё один технический факт, который понадобится в § 4.4. Лемма continuous_bounded_near утверждает: непрерывная в точке $x$ функция ограничена в некоторой проколотой окрестности $x$ — существуют число $M$ и радиус $δ > 0$ , такие что $∣ f (x + h) ∣ \leq M$ при $0 < ∣ h ∣ < δ$ .

Доказательство короткое: непрерывность при $ε = 1$ даёт $δ$ , на котором $∣ f (x + h) - f (x) ∣ < 1$ ; тогда $∣ f (x + h) ∣ \leq ∣ f (x) ∣ + 1$ , и за $M$ берётся $∣ f (x) ∣ + 1$ . Сам по себе факт скромный, но в § 4.4.2 он окажется существенным: в доказательстве правила произведения множитель $g (x + h)$ нужно будет чем-то ограничить, и ограничит его именно эта лемма. Роль её названа заранее, чтобы появление continuous_bounded_near в § 4.4 не выглядело неожиданным.

Иерархия: гладкое $\subset$ непрерывное{Иерархия: гладкое в непрерывном}

Итог раздела — одна строчка иерархии: дифференцируемость строго сильнее непрерывности. Всякая дифференцируемая функция непрерывна — это deriv_implies_continuous. Обратное неверно. Стандартный пример — функция $∣ x ∣$ в нуле: она непрерывна, но не дифференцируема, поскольку слева приращение ведёт себя с наклоном $- 1$ , а справа — с наклоном $+ 1$ , и единого линейного приближения нет. Над $Q$ этот пример работает так же, как над $R$ .

Подаём $∣ x ∣$ именно как стандартную интуицию, а не как отдельную Rocq-теорему: леммы вида << $∣ x ∣$ не дифференцируема в нуле >> в Differentiation.v нет, и приписывать репозиторию её не следует. Этот же пример наглядно показывает, почему процесс deriv_process из § 4.1.4 — с одними лишь положительными шагами — не может быть самостоятельным определением производной: у $∣ x ∣$ в нуле правые разностные отношения сходятся к $1$ , и процесс deriv_process был бы процессом Коши, тогда как двусторонней производной нет. Полное определение даёт только двусторонний критерий has_derivative. Содержательный итог таков: глава поднялась на ступень — от непрерывности § 5.3 к гладкости. Дальше эта ступень несёт правила дифференцирования.

Произведение и степень

Квадрат: прямой счёт

Прежде чем браться за общее правило произведения, полезна разминка — производная квадрата. Утверждение: для функции $w \mapsto w \cdot w$ производная в точке $x$ равна $2 x$ . В коде это deriv_square.

Доказательство — прямой алгебраический счёт. Ошибка линейного приближения здесь

(x + h) \cdot (x + h) - x \cdot x - 2 x \cdot h = h \cdot h,

то есть ровно $h^{2}$ . Остаётся заметить, что $∣ h \cdot h ∣ = ∣ h ∣ \cdot ∣ h ∣ < ε \cdot ∣ h ∣$ , коль скоро $∣ h ∣ < ε$ — для чего за $δ$ достаточно взять сам $ε$ . Содержательно важно вот что: ошибка приближения квадрата — это в точности квадратичный остаток $h^{2}$ , и именно он уходит в $o (h)$ . Этот сюжет — <<нелинейность даёт квадратичный остаток>> — повторится в общем правиле произведения.

Правило произведения

{ Главное нелинейное правило: производная произведения. Если $f$ имеет производную $L_{f}$ , а $g$ — производную $L_{g}$ , то функция $w \mapsto f (w) \cdot g (w)$ имеет производную

L_{f} \cdot g (x) + f (x) \cdot L_{g} .

В Differentiation.v это deriv_product — самое длинное доказательство файла (SECTION 4, около ста пятидесяти строк). Приводить его целиком не будем; назовём идею.}

Идея — алгебраическое разложение ошибки приближения на три слагаемых:

f (x + h) g (x + h) - f (x) g (x) - (L_{f} g (x) + f (x) L_{g}) h = T_{1} (f (x + h) - f (x) - L_{f} h) g (x + h) + T_{2} L_{f} h (g (x + h) - g (x)) = + T_{3} f (x) (g (x + h) - g (x) - L_{g} h) .

Каждое из трёх слагаемых оценивается величиной $(ε /3) \cdot ∣ h ∣$ — отсюда дробление $ε$ на три части. Слагаемое $T_{1}$ содержит ошибку приближения $f$ , помноженную на $g (x + h)$ ; чтобы оценить его, множитель $g (x + h)$ нужно ограничить — и здесь работает лемма continuous_bounded_near из § 4.3.2, заранее для этого приготовленная. Слагаемое $T_{2}$ оценивается через непрерывность $g$ (разность $g (x + h) - g (x)$ мала). Слагаемое $T_{3}$ — через производную $g$ (ошибка её приближения мала по порядку $h$ ). Сумма трёх оценок по $(ε /3) \cdot ∣ h ∣$ и неравенство треугольника дают требуемое.

{ Это полная теорема, не сеточная и не приближённая версия (предохранитель Части V). У правила есть и процессная форма: deriv_product_process в ProcessDerivative.v утверждает, что процесс разностных отношений произведения эквивалентен постоянному процессу $L_{f} g (x) + f (x) L_{g}$ . Доказана она, как и процессные правила § 4.2.3, через мост deriv_process_converges и саму deriv_product — снова надстройка, а не отдельное доказательство.}

Степенное правило индукцией

Из правила произведения вырастает степенное правило: для всякого натурального $n$ производная функции $w \mapsto w^{n + 1}$ в точке $x$ равна $(n + 1) \cdot x^{n}$ . В коде это deriv_power_succ.

Доказательство — индукция по $n$ . База: при $n = 0$ речь о производной $w \mapsto w^{1}$ , то есть тождества, и правило даёт $1 \cdot x^{0} = 1$ — это deriv_id из § 4.2.2. Шаг: степень $w^{n + 2}$ записывается как произведение $w \cdot w^{n + 1}$ , к нему применяется правило произведения — множитель $w$ даёт наклон $1$ , множитель $w^{n + 1}$ — наклон $(n + 1) x^{n}$ по предположению индукции, — и алгебра сводит результат к $(n + 2) \cdot x^{n + 1}$ .

Степень рационального числа — это Qpow, рекурсивная функция; она построена не здесь, а раньше по цепочке зависимостей — в файле SeriesConvergence.v. То есть возведение в степень глава получает готовым. Содержательно deriv_power_succ — бесконечное семейство правил, по одному на каждое $n$ , свёрнутое индукцией в одну теорему.

Почему произведение ломает линейность

Стоит вернуться к предупреждению из § 4.2.4. Производная произведения не есть произведение производных: правило даёт $L_{f} g (x) + f (x) L_{g}$ , а не $L_{f} \cdot L_{g}$ . Произведение нелинейно по самой своей природе, и дифференцирование это наследует.

Видно это и алгебраически. Перемножая два линейных приближения — $f (x) + L_{f} h$ и $g (x) + L_{g} h$ , — получаем

f (x) g (x) + (L_{f} g (x) + f (x) L_{g}) h + L_{f} L_{g} h^{2} .

Линейная по $h$ часть — ровно $L_{f} g (x) + f (x) L_{g}$ , наклон из правила произведения. А член $L_{f} L_{g} h^{2}$ — квадратичный остаток, и именно он уходит в $o (h)$ . Это тот же сюжет, что в § 4.4.1, где ошибка квадрата оказалась равной $h^{2}$ : всякий раз, как приближение первого порядка взаимодействует с самим собой через умножение, появляется остаток порядка $h^{2}$ , и определение $o (h)$ ровно для того и устроено, чтобы такой остаток поглощать.

Единственность и теорема Ферма

Производная единственна

Критерий has_derivative проверяет, является ли данное число $L$ производной. Но не может ли критерию удовлетворять сразу несколько разных чисел? Лемма deriv_unique отвечает: нет. Если и $L$ , и $L^{'}$ суть производные $f$ в точке $x$ , то $L = L^{'}$ (в смысле Qeq).

{ Доказательство — от противного. Пусть $L \neq = L^{'}$ ; тогда $∣ L - L^{'} ∣ > 0$ , и можно взять $ε = ∣ L - L^{'} ∣/4$ . Оба критерия — для $L$ и для $L^{'}$ — доставляют свои оценки ошибки; складывая их и применяя неравенство треугольника, получаем для подходящего ненулевого $h$

∣ L - L^{'} ∣ \cdot ∣ h ∣ < \frac{1}{2} ∣ L - L^{'} ∣ \cdot ∣ h ∣,

что невозможно. Значит, $L = L^{'}$ . Содержательно: линейное приближение приращения, если оно вообще существует, ровно одно — поэтому оборот <<производная $f$ в точке $x$ >> корректен, он называет единственный объект. Процессная форма этого факта — deriv_process_unique в ProcessDerivative.v: два постоянных процесса, отвечающих двум производным одной функции, эквивалентны. По разбору § 4.1.5 это $L 1$ -корректность роли <<наклон>>: производная определена однозначно.}

Аффинная функция и квадратичная потеря

Перед теоремой Ферма — две подготовительные производные из SECTION 5 файла. Производная аффинной функции $w \mapsto a \cdot w + b$ в любой точке равна $a$ — это deriv_affine; ошибка линейного приближения здесь тождественно нулевая. Производная квадратичной потери: для функции $w \mapsto (w - w_{⋆})^{2}$ производная в точке $x$ равна $2 (x - w_{⋆})$ — это quadratic_loss_derivative, прямой счёт в духе § 4.4.1.

Квадратичная потеря — модельная целевая функция: её минимум достигается при $w = w_{⋆}$ , и она будет нужна в § 4.5.4 как пример для градиентного спуска.

Теорема Ферма: минимум зануляет производную

Главный результат раздела — теорема Ферма. Если функция $f$ имеет в точке $x$ локальный минимум и дифференцируема в этой точке, то её производная там равна нулю. В коде это local_min_zero_deriv: из local_min f x и has_derivative f x L следует $L = 0$ .

Содержательно теорема говорит вот что. В точке локального минимума линейное приближение приращения не может иметь ненулевого наклона. Будь наклон $L$ положителен, шаг влево (отрицательный $h$ ) уменьшил бы значение; будь $L$ отрицателен, значение уменьшил бы шаг вправо. И то и другое противоречит тому, что в точке минимума $f (x) \leq f (x + h)$ для всех малых $h$ . Значит, $L = 0$ .

Доказательство разбирает знак $L$ . Если $L \neq = 0$ , берётся $ε = ∣ L ∣/2$ ; критерий производной даёт $δ$ , на котором ошибка приближения меньше $\frac{∣ L ∣}{2} ∣ h ∣$ . Тогда для шага нужного знака — влево при $L > 0$ , вправо при $L < 0$ — приращение $f (x + h) - f (x)$ оказывается строго отрицательным, что противоречит минимальности. Остаётся $L = 0$ .

Это полная теорема. Что касается аудита аксиом (предохранитель Части V): в финале Differentiation.v стоит, среди прочих, Print Assumptions local_min_zero_deriv — и именно по этому выводу, а не по заголовку файла, устанавливается фактический аксиомный статус теоремы. К общей оговорке глава вернётся в § 4.8.3.

Связь с градиентным спуском

Последний подраздел — мост к оптимизации. Лемма gradient_step_uses_derivative связывает шаг градиентного спуска с производной квадратичной потери: первый шаг

‘ g d_{w} e i g h t ‘ w_{0} w_{⋆} η 1 = w_{0} - η \cdot (2 (w_{0} - w_{⋆})) .

Правая часть — это <<вес минус скорость обучения, помноженная на производную потери>>: множитель $2 (w_{0} - w_{⋆})$ — ровно производная квадратичной потери из § 4.5.2.

{ Honest-замечание о статусе этой леммы (предохранитель Части V: громкие имена называть тем, что они есть). gradient_step_uses_derivative — не глубокая теорема. Её доказательство — это разворачивание определений gd_weight, gd_error, contraction и тождество ring. По существу это проверка согласованности: введённый в GradientDescent.v объект gd_weight действительно реализует <<градиентный шаг>> в смысле производной этой главы. Полезная сшивка двух файлов — но самостоятельным содержанием она не является, и называть её следует именно так.}

В саму теорию градиентного спуска — сходимость весов, скорость, выбор $η$ — глава не углубляется: это материал GradientDescent.v и, возможно, отдельной будущей главы. Здесь важно одно — идентификация направления шага с производной квадратичной потери; этим мост и исчерпывается.

Теорема о среднем: walk-точки

Классическая теорема о среднем и почему её нельзя взять прямо

Классическая теорема о среднем утверждает: для функции $f$ , дифференцируемой на отрезке $[a, b]$ , найдётся внутренняя точка $c$ , в которой

f^{'} (c) = \frac{f ( b ) - f ( a )}{b - a} .

Деление на $b - a$ здесь не составляет принципиальной трудности: коль скоро $a < b$ , знаменатель ненулевой, и частное законно. Существенно другое — сама форма теоремы: оборот <<найдётся внутренняя точка $c$ >>. Это чистое утверждение существования, и конструктивно оно слабое — та же трудность, что с argmax в теореме об экстремуме § 5.3, где пришлось брать индексную версию вместо точки максимума.

Поэтому MeanValueTheorem.v не доказывает классическую форму с точкой $c$ . Он доказывает её конструктивные следствия — те оценки приращения через границы производной, ради которых теорема о среднем обычно и применяется. Ход тот же, что в § 5.3: вместо неуловимой точки — сеточная конструкция, дающая проверяемые неравенства.

Walk-точки: лейбницево-точная цепочка{Walk-точки: лейбницево-точная цепочка}

Сеточная конструкция строится на walk-точках — цепочке $x, x + s, (x + s) + s, \dots$ с фиксированным шагом $s$ . В MeanValueTheorem.v это рекурсивная функция:

Fixpoint walk_point (x step : Q) (n : nat) : Q :=
  match n with
  | O => x
  | S n' => walk_point x step n' + step
  end.

Может возникнуть вопрос: зачем рекурсия, если $n$ -я точка — это просто $x + n \cdot s$ ? Причина — honest-деталь, и она прямо названа в шапке файла. Телескопирование, на котором держится всё доказательство § 4.6.4, складывает приращения функции по последовательным точкам цепочки. Чтобы слагаемые склеились, $n$ -я точка одной записи и $n$ -я точка другой должны совпадать лейбницево — синтаксически, как термы, — а не только по отношению Qeq. Рекурсивное определение walk_point это совпадение обеспечивает; замкнутая формула $x + n \cdot s$ — нет. Лемма walk_point_qeq отдельно доказывает, что walk-точка Qeq-равна $x + n \cdot s$ , а walk_point_in_interval — что при шаге $(b - a) / (N + 1)$ все точки остаются в отрезке $[a, b]$ .

Здесь же файл вводит равномерную дифференцируемость на отрезке — усиление поточечного критерия:

Definition udiff_on (f f' : Q -> Q) (a b : Q) : Prop :=
  a < b /\
  forall eps : Q, 0 < eps ->
    exists delta : Q, 0 < delta /\
      forall x h : Q, a <= x -> x <= b ->
        0 < Qabs h -> Qabs h < delta ->
        Qabs (f (x + h) - f x - f' x * h) < eps * Qabs h.

Отличие от has_derivative — в порядке кванторов. У поточечного критерия для каждой точки $x$ свой $δ$ . У udiff_on один и тот же $δ$ годится для всех точек отрезка сразу. Именно это и нужно: одной оценкой накрыть все шаги сетки, сколько бы их ни было. В терминах § 4.1.5 это усиление Rules: равномерная дифференцируемость — то же по роли, что равномерная непрерывность в § 5.3.

Архимедова сетка: шаг можно сделать сколь угодно малым

Чтобы сетка приближала отрезок как угодно точно, её шаг должен быть сколь угодно мал. Лемма walk_step_pos устанавливает, что шаг $(b - a) / (N + 1)$ положителен, а walk_step_small — что для всякого $δ > 0$ найдётся такое число делений $N$ , при котором этот шаг меньше $δ$ .

{ Доказательство walk_step_small опирается на архимедово свойство. В самом MeanValueTheorem.v используется лемма с именем Archimedean_nat; близкие архимедовы леммы в других файлах цепи могут называться иначе. Содержательно это один и тот же шаг рассуждения: найти конечное $N$ , при котором рациональная сетка становится тоньше заданного $δ$ . Архимедовость — то самое <<топливо>> $ε$ -рассуждений, которое в § 5.1 уже делало шкалу процессов сколь угодно мелкой, — здесь позволяет за конечное число делений сделать сетку как угодно частой. Никакой завершённой бесконечности для этого не нужно.}

Главная теорема: ограниченная производная — ограниченное приращение

Главная теорема файла — bounded_deriv_bounded_increment. Если на отрезке $[a, b]$ функция равномерно дифференцируема и её производная ограничена по модулю числом $M$ , то полное приращение функции от $a$ до конца сетки оценивается так:

f (walk- конец) - f (a) \leq (M + ε) \cdot (b - a),

причём $ε > 0$ можно взять любым.

Идея доказательства — телескопирование. Полное приращение от $a$ до конца сетки записывается как сумма приращений по отдельным шагам walk-цепочки. Каждый шаг оценивается равномерной дифференцируемостью: приращение на одном шаге не больше $(M + ε /2)$ , помноженного на длину шага. Индукция по числу шагов $k$ собирает эти оценки: после $k$ шагов накопленное приращение не превосходит $k \cdot (M + ε /2) \cdot s$ , а при $k$ , равном полному числу делений, это даёт $(M + ε) \cdot (b - a)$ . Полный код — большая индукция; здесь важна схема: равномерность даёт оценку одного шага, телескоп складывает шаги.

Назовём результат честно (предохранитель Части V). Это не классическая теорема о среднем с точкой $c$ . Это сеточное следствие теоремы о среднем: оценка полного приращения через верхнюю границу производной. Картину замыкает лемма walk_endpoint_qeq — конец walk-цепочки при шаге $(b - a) / (N + 1)$ Qeq-равен правому концу $b$ ; то есть сетка действительно проходит весь отрезок от $a$ до $b$ .

Следствия: монотонность и Липшиц

Нулевая производная — почти постоянство

Первое следствие главной теоремы — случай нулевой производной. Если на отрезке $[a, b]$ производная функции тождественно равна нулю, то полное приращение функции сколь угодно мало: для всякого $ε > 0$

f (walk- конец) - f (a) \leq ε \cdot (b - a) .

В коде это zero_deriv_near_constant — прямое следствие § 4.6.4 при $M = 0$ .

Формулировку стоит прочесть аккуратно. Теорема не утверждает полной формы << $f$ постоянна на всём отрезке >>. Текущий файл доказывает именно сеточную $ε$ -форму: приращение между концами walk-цепочки можно сделать сколь угодно малым. Полное утверждение о равенстве всех значений — скажем, $f (x) = f (y)$ для любых $x, y$ из отрезка — вполне формулируемо как пропозиция, но потребовало бы отдельной теоремы и дополнительных мостов; здесь оно не доказывается. Под $P 4$ сеточная $ε$ -форма уместна и содержательна: она говорит, что разность $f$ на концах можно загнать ниже любого порога. Это сеточный результат — оценка по сетке walk-точек.

Знак производной задаёт монотонность

{ Второе следствие связывает знак производной с ростом и убыванием. Лемма pos_deriv_increases: если на отрезке производная отделена снизу положительным числом $c$ , то функция на сетке выросла — приращение $f (walk- конец) - f (a)$ строго положительно. Двойственная лемма neg_deriv_decreases: если производная отделена сверху отрицательным числом, функция убыла.}

Содержательно это классическое следствие теоремы о среднем — <<положительная производная означает рост>>, — но в сеточной форме и без точки $c$ . Доказательства повторяют телескоп § 4.6.4, только оценка одного шага берётся не сверху, а снизу. Это сеточные результаты, как и всё в § 4.6–4.7.

Липшицевость из ограниченной производной

Третье следствие — липшицевость. Лемма bounded_deriv_lipschitz_local даёт локальную оценку: вблизи точки $∣ f (x + h) - f (x) ∣ \leq (∣ L ∣ + 1) \cdot ∣ h ∣$ — приращение функции пропорционально шагу с постоянным коэффициентом. Лемма nonneg_deriv_approx_nondec утверждает, что неотрицательная производная делает функцию приближённо неубывающей. Лемма udiff_continuous_at замыкает связь с § 4.3: равномерная дифференцируемость влечёт непрерывность в каждой точке отрезка — через udiff_pointwise (равномерная дифференцируемость даёт поточечную) и deriv_implies_continuous из § 4.3.1.

Здесь стоит отметить, как замкнулся круг. В § 5.3 липшицевость вводилась как условие — конструктивная замена равномерной непрерывности, которую над $Q$ нельзя получить даром. Теперь липшицевость выводится — из ограниченной производной. В разборе § 4.1.5 это значит: Rules производной порождают правило, которое в § 5.3 приходилось требовать для непрерывности. То, что в главе о непрерывности приходилось требовать, глава о производной доказывает.

Точные случаи: аффинная и квадратичная

Завершают раздел точные случаи — функции, для которых сеточная картина и классическая теорема о среднем сходятся. Лемма affine_udiff устанавливает, что аффинная функция равномерно дифференцируема на любом отрезке; quadratic_udiff — то же для квадрата. А лемма mvt_quadratic_midpoint даёт для квадрата точное равенство теоремы о среднем:

2 \cdot \frac{a + b}{2} \cdot (b - a) = b^{2} - a^{2} .

Содержательно: для квадрата та самая <<точка $c$ >> из классической теоремы находится явно и точно — это середина отрезка $(a + b) /2$ . Здесь сеточная картина § 4.6 и классическая формулировка встречаются в одной проверяемой точке.

{ Одно honest-замечание о файле. MeanValueTheorem.v заканчивается на лемме mvt_quadratic_midpoint — без финального блока Check и Print Assumptions, который есть, например, в Differentiation.v. Это не признак незавершённости доказательств: все восемнадцать лемм файла закрыты Qed. Это лишь отсутствие сводки аксиомного аудита в конце файла; такой аудит для нужной теоремы запускается командой Print Assumptions отдельно.}

Что построено и что готовится. Итог главы

Итог в трёх столбцах

Соберём сделанное в режиме инфраструктуры — что построено, чего нет и что глава готовит дальше.

Построено и проверено:

division-free критерий производной has_derivative и его экстенсиональные леммы;
производная как процесс разностных отношений deriv_process с безопасным ненулевым шагом $h_{n} = 1/ (n + 1)$ ; мост deriv_process_converges между критерием и процессом; deriv_process_cauchy;
линейность дифференцирования (скаляр, противоположность, сумма, разность) — в форме критерия и в процессной форме (deriv_sum_process, deriv_scale_process);
дифференцируемость влечёт непрерывность;
правило произведения (полная теорема, дробление $ε /3$ ) — в форме критерия и процессной (deriv_product_process); степенное правило индукцией; единственность производной;
теорема Ферма local_min_zero_deriv;
равномерная дифференцируемость udiff_on и walk-точки;
bounded_deriv_bounded_increment — сеточное следствие теоремы о среднем — и монотонность с липшицевостью как дальнейшие следствия.

Не построено в этой главе:

классическая теорема о среднем с точкой $c$ — доказаны только сеточные следствия, и это сознательный выбор;
производная функции на фактор-классах RealPoint — глава работает лишь с функциями $Q \to Q$ ;
производные высших порядков и ряд Тейлора — за пределами опорных файлов;
цепное правило для композиции — в Differentiation.v его нет;
правило Лопиталя — вынесено за пределы главы; отдельный файл для него в репозитории есть, но включение потребовало бы своего раздела и отдельной сверки, что перегрузило бы и без того плотную главу.

Готовит дальше:

интеграл — следующий аналитический слой Части V;
градиентный спуск как приложение — мост к нему намечен в § 4.5.4, полная теория содержится в GradientDescent.v.

Что осталось бы для производной на классах

Глава честно ограничилась функциями $Q \to Q$ . Назовём конкретно, какого шага не хватает до производной на фактор-классах RealPoint — так же, как § 5.1 называла недостающее звено для расстояния на классах.

Понадобилось бы, во-первых, доказать корректность критерия has_derivative относительно эквивалентности — что производная не меняется при замене представителя класса другим эквивалентным. Во-вторых, поднять само определение с рациональных функций на функции фактор-классов. Ни того ни другого в опорных файлах нет; это честная граница главы, очерченная конкретно, а не общими словами.

Оговорка о статусе аксиом

{ Предохранитель Части V требует точности в вопросе об аксиомах. Все три опорных файла — Differentiation.v, ProcessDerivative.v, MeanValueTheorem.v — в своих шапках заявляют статус << AXIOMS: none >> (ProcessDerivative.v — << 0 axioms, 16 Qed >>). Однако все они импортируют файлы, через которые проходит классический слой: Differentiation.v опирается на SeriesConvergence.v и GradientDescent.v, а те — на MonotoneConvergence.v, несущий аксиому classic; ProcessDerivative.v опирается на Differentiation.v. Кроме того, MeanValueTheorem.v импортирует EVT_idx.v, а в EVT_idx.v аксиома classic объявлена локально (этот файл разбирался в § 5.3). Это не значит, что каждая теорема о среднем зависит от classic — значит лишь, что для конкретной теоремы нужно смотреть Print Assumptions.}

{ Точная формулировка — и именно не огульная — такова. Импорты проходят через файлы с классическим слоем, и поэтому заголовок файла сам по себе не заменяет команды Print Assumptions для конкретной теоремы (правило, принятое ещё с Главы 4.6). Не следует утверждать <<зависимости тянут classic>> как общий приговор каждой теореме — фактический аксиомный статус даёт только Print Assumptions именно этой теоремы. В финале Differentiation.v такая проверка выписана для ключевых теорем — deriv_product, deriv_power_succ, local_min_zero_deriv, gradient_step_uses_derivative, — и именно эти выводы дают фактическую картину. У MeanValueTheorem.v и ProcessDerivative.v финального блока Print Assumptions нет; для нужной теоремы его следует запускать отдельно.}

{ Для полноты аудита назовём и два honest-факта из глубины цепи, установленных дословной сверкой исходных файлов: лемма partial_sum_tail в SeriesConvergence.v оставлена незавершённой через Abort (с авторским комментарием, что прямая формулировка телескопа неудобна и свойство Коши доказывается иначе), а доказательство mct_inc_least в MonotoneConvergence.v содержит Restart — первая попытка доказательства брошена и заменена второй. На теоремы настоящей главы это не влияет, но в честной картине зависимостей такие места должны быть названы.}

Итог главы

Глава построила производную — слой анализа над непрерывностью § 5.3. Главный поворот в том, как устроено само понятие. Существование производной задаётся без деления — division-free критерием $o (h)$ , который говорит, какое число линейно приближает приращение. Вычислительная же сторона — это процесс разностных отношений с безопасным ненулевым шагом, и мост deriv_process_converges связывает обе стороны. Главная осторожность главы: из теоремы о среднем доказаны сеточные следствия, а не классическая форма с точкой $c$ .

Построено: division-free критерий производной и производная-процесс, связанные мостом; линейность, правило произведения, степенное правило, единственность; теорема Ферма; сеточная теорема о среднем и её следствия — монотонность и липшицевость.

На чём стоит: на $δ$ - $ε$ -аппарате непрерывности § 5.3, на архимедовом свойстве как топливе $ε$ -рассуждений, на процессной онтологии $P 4$ , в которой производная — не завершённый предел, а процесс приближений наклона.

Дальше: интеграл как следующий аналитический слой Части V; градиентный спуск как приложение производной к оптимизации.

Часть: Часть V. Топология и анализ процессов · Том: «Математика»

Понятия: Формализация

Навигация: ← Глава 3. Непрерывность · Глава 5. Интеграл →

E/R/R-разметка в шапке файла ProcessDerivative.v; здесь разворачивается по образцу Части I. ↩

Путь Мудрости

Проводник