Речь идёт про равенство
, где в левой части
обозначает некоторую функцию одной переменной, по которой идёт интегрирование, а в правой части
обозначает функцию от
.
Так здесь целая теорема спрятана, причем нетривиальная.
Я бы её сформулировал так:
Через
я буду обозначать бесконечно малую по той базе, которая указана под именем функции.
Теорема:
Пусть есть функция
, определенная в точке
и в некоторой её (возможно, полу-)окрестности
, причем
(т.е. она непрерывна в
). Так же она интегрируема в этой (возможно, полу-)окрестности. Это значит, что
Тогда:
Доказательство:
Опять буду делать по определению предела.
Выберем произвольный
. Т.к.
непрерывна в
, это значит, что
такая, что для любых
таких, что
и при которых
определена, выполняется
. Выберем произвольный
такой, что как отрезок он является подмножеством области определения нашей альфы, и
.
Из двойного неравенства для альфы получаем следующее:
А дальше все то же самое, что и в предыдущем доказательстве.
Учитывая
получаем, что
а значит (см (2) ):
что и доказывает нужное нам утверждение.
Дргими словами, если обозначить за
то получаем, что
что и требовалось доказать.
По итогу, это равенство просто маскирует в себе всю содержательную часть предыдущего доказательства. Через супремум/инфимум тоже наверное можно, но вряд ли будет сильно уж проще.
И если посмотреть на доказательство (любое из двух), видно, что от всей этой ерунды с контролем областей определения пока избавиться не получается.
Мат.анализ на уровне 18 века.
Ну да, мне нужен анализ с актуальными бесконечно малыми и без пределов. Но без логических вывертов, как в нестандартном анализе или SDG. Или хотя бы какая-то техника, позволяющая нормально делать обычный мат.анализ без постоянного контроля областей определения.
обоснование допустимости перестановки предельных переходов
Если нету пределов, то и таких теорем тоже нету.
Вы все эти теоремы просто к формализму свести хотите?
В определенном смысле да. Я хочу сузить класс функций, но получить гладкость преобразований. Чтобы, например, была возможность алгоритмически определять корректность областей определения. Иными словами, есть у меня функция
. Я пишу
И я не хочу постоянно проверять, корректно ли брать предел по такой-то базе для такой-то функции. Т.е. чтобы если я попытался взять, например,
то компилятор бы подсветил мне, что такой переход делать нельзя.