Определение функции

[EminentVictorians]

dgwuqtj в сообщении #1651443 писал(а):

третье — это оценка интеграла через супремум подынтегральной функции.

Можно вот это равенство более подробно?

$$ \lim_{\Delta x \to 0} \frac{\int_{x_0}^{x_0 + \Delta x} o(1)}{\Delta x} = \lim_{\Delta x \to 0} \frac{o(\Delta x)}{\Delta x}$$

По-моему, здесь довольно большой угол срезан.

[dgwuqtj]

Речь идёт про равенство $\int_{x_0}^{x_0 + \Delta x} o(1) = o(\Delta x)$, где в левой части $o(1)$ обозначает некоторую функцию одной переменной, по которой идёт интегрирование, а в правой части $o(\Delta x)$ обозначает функцию от $\Delta x$. Это следует из оценки $|\int_a^b f| \leq |a - b| \sup_{x \in [a, b]} |f(x)|$, где $[a, b] = [b, a]$ при $a > b$. Просто потому что $\sup_{x \in [x_0, x_0 + \Delta x]} |o(1)| = o(1)$. Когда такие вещи формализуют в пруфчекерах, появляются длинные списки из всяких очевидных лемм...

[Padawan]

EminentVictorians в сообщении #1650811 писал(а):

Примерно такой матанализ мне нужен.

Мат.анализ на уровне 18 века. За бортом останется большая и важная часть мат.анализа -- обоснование допустимости перестановки предельных переходов, перемены порядка суммирования и т.д. Вы все эти теоремы просто к формализму свести хотите?

[drzewo]

Переписывать и перетрактовывать разными способами известные вещи легче чем решать задачи. В этом все дело.

[EminentVictorians]

dgwuqtj в сообщении #1651519 писал(а):

Речь идёт про равенство $\int_{x_0}^{x_0 + \Delta x} o(1) = o(\Delta x)$, где в левой части $o(1)$ обозначает некоторую функцию одной переменной, по которой идёт интегрирование, а в правой части $o(\Delta x)$ обозначает функцию от $\Delta x$.

Так здесь целая теорема спрятана, причем нетривиальная.

Я бы её сформулировал так:

Через $\alpha(x)_{x \to x_0}$ я буду обозначать бесконечно малую по той базе, которая указана под именем функции.

Теорема:
Пусть есть функция $\alpha(x)_{x \to x_0}$, определенная в точке $x_0$ и в некоторой её (возможно, полу-)окрестности $U(x_0)$, причем $f(x_0) = 0$ (т.е. она непрерывна в $x_0$). Так же она интегрируема в этой (возможно, полу-)окрестности. Это значит, что

$$\forall x \in U(x_0)$$

$$\exists \int\limits_{x_0}^{x}\alpha(x)_{x \to x_0}$$

Тогда:

$$\lim\limits_{\Delta x \to 0}^{}\frac{\int\limits_{x_0}^{x_0 + \Delta x} \alpha(x)_{x \to x_0}}{\Delta x} = 0$$

Доказательство:

Опять буду делать по определению предела.

Выберем произвольный $\varepsilon > 0$. Т.к. $\alpha(x)_{x \to x_0}$ непрерывна в $x_0$, это значит, что $\exists \delta > 0$ такая, что для любых $x$ таких, что $|x - x_0| < \delta$ и при которых $\alpha(x)$ определена, выполняется $- \varepsilon < \alpha(x) < \varepsilon$. Выберем произвольный $\Delta x$ такой, что как отрезок он является подмножеством области определения нашей альфы, и $|\Delta x| < \delta$.

Из двойного неравенства для альфы получаем следующее:

$$ - \varepsilon |\Delta x| \quad \leqslant \int\limits_{\operatorname{min} (x_0, x_0 + \Delta x)}^{\operatorname{max} (x_0, x_0 + \Delta x) } \alpha(x) \quad \leqslant \quad \varepsilon |\Delta x| \quad \quad (1)$$

$$ - \varepsilon \quad \leqslant \frac{\int\limits_{\operatorname{min} (x_0, x_0 + \Delta x)}^{\operatorname{max} (x_0, x_0 + \Delta x) } \alpha(x)}{|\Delta x|} \quad \leqslant \quad \varepsilon \quad \quad (2)$$

А дальше все то же самое, что и в предыдущем доказательстве.

Учитывая

$$ \left| \int\limits_{x_0}^{x_0 + \Delta x}\alpha(x) \right| = \left| \int\limits_{\operatorname{min} (x_0, x_0 + \Delta x)}^{\operatorname{max} (x_0, x_0 + \Delta x) } \alpha(x) \right|$$

получаем, что

$$\frac{ \int\limits_{\operatorname{min} (x_0, x_0 + \Delta x)}^{\operatorname{max} (x_0, x_0 + \Delta x) } \alpha(x) }{|\Delta x|} = \frac{\int\limits_{x_0}^{x_0 + \Delta x}\alpha(x)}{\Delta x}$$

а значит (см (2) ):

$$ - \varepsilon \quad \leqslant \frac{\int\limits_{x_0}^{x_0 + \Delta x}\alpha(x)}{\Delta x} \quad \leqslant \quad \varepsilon$$

что и доказывает нужное нам утверждение.


Дргими словами, если обозначить за

$$\beta (\Delta x) = \frac{\int\limits_{x_0}^{x_0 + \Delta x}\alpha(x)}{\Delta x}$$

то получаем, что

$$\int\limits_{x_0}^{x_0 + \Delta x}\alpha(x) = \beta (\Delta x)_{\Delta x \to 0} \Delta x = o(\Delta x)$$

что и требовалось доказать.




По итогу, это равенство просто маскирует в себе всю содержательную часть предыдущего доказательства. Через супремум/инфимум тоже наверное можно, но вряд ли будет сильно уж проще.


И если посмотреть на доказательство (любое из двух), видно, что от всей этой ерунды с контролем областей определения пока избавиться не получается.

Padawan в сообщении #1651577 писал(а):

Мат.анализ на уровне 18 века.

Ну да, мне нужен анализ с актуальными бесконечно малыми и без пределов. Но без логических вывертов, как в нестандартном анализе или SDG. Или хотя бы какая-то техника, позволяющая нормально делать обычный мат.анализ без постоянного контроля областей определения.

Padawan в сообщении #1651577 писал(а):

обоснование допустимости перестановки предельных переходов

Если нету пределов, то и таких теорем тоже нету.

Padawan в сообщении #1651577 писал(а):

Вы все эти теоремы просто к формализму свести хотите?

В определенном смысле да. Я хочу сузить класс функций, но получить гладкость преобразований. Чтобы, например, была возможность алгоритмически определять корректность областей определения. Иными словами, есть у меня функция $f(x) + g(x)$. Я пишу

$$\lim\limits_{B}^{} f(x) + g(x) = \lim\limits_{B}^{} f(x) + \lim\limits_{B}^{} g(x)$$

И я не хочу постоянно проверять, корректно ли брать предел по такой-то базе для такой-то функции. Т.е. чтобы если я попытался взять, например,

$$\lim\limits_{x \to + \infty}^{} \sqrt{x} + \sqrt{-x}$$

то компилятор бы подсветил мне, что такой переход делать нельзя.

[dgwuqtj]

EminentVictorians в сообщении #1651681 писал(а):

Через супремум/инфимум тоже наверное можно, но вряд ли будет сильно уж проще.

Оно концептуально проще, к тому же оценка интеграла через супремум подыинтегральной функции - это довольно фундаментальная вещь. Другое дело, что супремум по сужающемуся отрезку тоже бесконечно малый, но этот факт к интегралам не относится.