#import "../../utils/core.typ": * 

== Замена переменной в интеграле Лебега

#def(label: "def-diffeomorphism")[
    Пусть $Omega_1$ и $Omega_2 subset RR^m$ открытые. $Phi: Omega_1 --> Omega_2$ называется _диффеоморфизмом_, если
    1. $Phi$ --- биекция,
    2. $Phi$ --- непрерывно дифференцируема на $Omega_1$,
    3. $Phi^(-1)$ --- непрерывно дифференцируема на $Omega_2$.
]

#th(name: "замена переменной в интеграле по мере Лебега", label: "substitution")[
    $Omega subset RR^m$ открытое. $Phi: Omega --> tilde(Omega)$ диффеоморфизм. $f: tilde(Omega) --> overline(RR)$, $f >= 0$ измерима (или суммируема). Тогда $ integral_tilde(Omega) f dif lambda_m (x) = integral_Omega f(Phi(x)) abs(Jj_Phi (x)) dif lambda_m (x), $
    где $Jj_Phi(x) = det Phi' (x)$ --- якобиан.
]

#example(name: "авторский, не бейте если не нравится", label: "substitution-example")[
    Давайте попробуем изуродовать нормальный интеграл, сделав в него подстановку.
    $
        integral_([0;1]times [0;1] times[0;1]) f(p) dif lambda_3 (p),
        space f(x, y, z) = 1 - y.
    $
    Это интеграл линейной функции в кубе. Что-то вроде общей массы снега в кубе $1 times 1 times 1$ метр, где плотность снега убывает линейно с нуля до единицы, чем дальше от земли и чем ближе к поверхности.

    Подстановка такая:
    $
        Phi vec(x, y, z) =
        vec(y/2, 1 - z^2, x/3) = 
        mat(0, 1/2, 0; 0, 0, -1; 1/3, 0, 0) dot vec(x, y, z^2) + vec(0, 1, 0).
    $
    Она сжимает параллелепипед $[0;3] times [0;2] times [0;1]$ в куб, переворачивает ее, и меняет местами координатные оси ($x ~~> y$, $y ~~> z$ и $z ~~> x$). Производная равна
    $
        Phi' vec(x, y, z) = mat(0, 1/2, 0; 0, 0, -1; 1/3, 0, 0) dot mat(1, 0, 0; 0, 1, 0; 0, 0, 2z) = mat(0, 1/2, 0; 0, 0, -2z; 1/3, 0, 0).
    $
    Тогда якобиан --- $-1/3 z$.

    Тогда
    $
        integral_([0;1]^3) f dif lambda_3 = integral_[0;3] integral_[0;2] integral_[0;1] z^2 dot abs(-1/3z) dif z dif y dif x.
    $

    Нетрудно увидеть, что оба интеграла равны $1/2$.

    Кажется, это довольно неплохой пример, поэтому я буду использовать его дальше.
]

#make_theorem("Частные случаи", color: proof_color)()[
    1. Сдвиг. Прибавляем к каждому $x$ какой-то вектор. Тогда якобиан равен единице, так как матрица производной --- единичная.
        $ integral_(RR^m) f dif lambda_m = integral_(RR^m) f(x + a) dif lambda_m $
        Здесь мы подвинули $x$ на вектор $a$. Интегрируя функцию по $RR^m$, множество не меняется.
    
    2. Линейное отображение $Phi(x) = T x$. Тогда $Jj_Phi = det T$. Тогда
        $ integral_(RR^m) f dif lambda_m = abs(det T) integral_(RR^m) f(T_x) dif lambda_m (x) $
    
    3. Сжатие/растяжение: $Phi(x) = c x$. Тогда получается диагональная матрица с определителем $c^m$:
        $ integral_(RR^m) f dif lambda_m = abs(c)^m integral_(RR^m) f(c x) dif lambda_m (x) $
]

#lemma(label: "diffeomorphism-decomposition")[
    $Phi: Omega -> tilde(Omega)$ диффеоморфизм, $Omega$, $tilde(Omega) subset RR^m$, $a in Omega$, $0 < k < m$. Тогда существует окрестность $U_a$ такая, что $Phi bar_(U_a) = Phi_1 compose Phi_2$, где $Phi_1$, $Phi_2$ --- диффеоморфизмы. $Phi_1$ не меняет какие-то (не обязательно любые) $k$ координат (и возможно их переставляет), а $Phi_2$ --- остальные $m - k$ координат.
]

#proof[
    Пусть $x, u in RR^k$, $y, v in RR^(m - k)$. Порежем координаты: $Phi(x, y) = (phi(x, y), psi(x, y))$, где $phi$ действует в $RR^k$, а $psi$ в $RR^(m - k)$. Пусть $Phi_1(u, v) = (u, f(u, v))$ и $Phi_2(u, v) = (g(u, v), v)$. Тогда $ (phi(x, y), psi(x, y)) = Phi(x, y) = Phi_1 compose Phi_2 = Phi_1(g(u, v), v) = (g(u, v), f(g(u, v), v)). $
    Отсюда можно однозначно определить $g$: $g(u, v) = phi(u, v)$. Теперь $Phi_2$ определяется однозначно: $Phi_2(u, v) = (phi(u, v), v)$. Отсюда $psi(u, v) = f compose Phi_2(u, v)$. Получится формула для $f$: $f(x, y) = psi compose Phi_2^(-1)(x, y)$. Для того, чтобы это получилось, необходима обратимость $Phi_2$ в некоторой окрестности $U_a$.

    Воспользуемся теоремой об обратной функции#rf("inverse-fn"). Непрерывную дифференцируемость легко увидеть: посмотрим на определитель $Phi'_2$:
    $ Phi'_2 = mat(phi'_u, phi'_v; 0, E) ==> det Phi'_2 = det phi'_u. $
    $phi'_u$ --- минор $k times k$ матрицы $Phi'$, так как это производные каких-то $k$ координат функции $Phi$. Так как $Phi$ непрерывно дифференцируемая биекция, то $det Phi' != 0$. 
    Действительно, если продифференцировать $Phi^(-1) (Phi (x)) = id$ получится $Phi' dot (Phi^(-1))' (Phi) = E$, значит $det Phi' != 0$ так как иначе произведение тоже имело бы определитель $0$. Отмечу, что производная композиции существует, так как по определению диффеоморфизма#rf("def-diffeomorphism") $Phi^(-1)$ --- непрерывно дифференцируема. 
    Это неверно для произвольной непрерывной биекции ($x^3$, например).
    Раз $det Phi' != $, у $Phi$ найдется какой-то ненулевой минор размера $k times k$.
    Это не обязательно угловой минор: может быть какой-то другой, поэтому переменные, возможно, придется переставить, чтобы такой угловой минор получить. Если мы переставим переменные с помощью какой-то перестановки $Phi_0$ в $Phi$, получив какой-то новый диффеоморфизм, то можно применить обратную перестановку к $Phi_1$, и так как $Phi_1 compose Phi_2 = Phi_0 compose Phi$, то $(Phi_0^(-1) compose Phi_1) compose Phi_2 = Phi$.
]

#example(name: "все еще авторский, чтобы вам понимать было сложнее")[
    Это очень сложная лемма для понимания. Даже сложнее самого доказательства теоремы, я бы сказал. Поэтому давайте посмотрим на ее особенно внимательно.

    Рассмотим диффеоморфизм из моего примера#rf("substitution-example"), и декомпозируем его на два: первый оставит одну координату, а второй --- две. 
    $ Phi vec(x, y, z) = vec(y/2, 1 - z^2, x/3). $
    Будем следовать ходу доказательства. Разрежем координаты.

    $ Phi(x, y, z) = (y/2, (1 - z^2, x / 3)) $
    Рассмотрим $Phi_1 (x, y, z) = (x, f(x, y, z))$ и $Phi_2 (x, y, z) = (g(x, y, z), y, z)$. Мы хотим, чтобы $Phi_1 compose Phi_2 = Phi$:
    $ Phi_1 compose Phi_2 = (g(x, y, z), f(g(x, y, z), y, z)) = (y/2, (1 - z^2, x / 3)) = Phi. $
    Отсюда находится $g(x, y, z) = y/2$. Тогда мы хотим, чтобы $f(y/2, y, z) = (1-z^2, x/3)$. Только вот, что-то не получается. $f$, фактически --- функция от двух аргументов --- $y$ и $z$, а в результате мы хотим что-то, зависимое от $x$??
    
    Почему у нас не получилось? Давайте посмотрим на $Phi_2$:
    $ Phi_2 (x, y, z) = (y/2, y, z). $
    Это необратимая функция, а нам необходима обратимость, чтобы $f compose Phi_2 = (1 - z^2, x/3)$ решалось для $f$. Но как же так? Разве нам не обещали обратимость в доказательстве?

    Обещали, но не говорили, по каким конкретно координатам. Чтобы была обратимость, требуется, чтобы определитель $Phi'_2$ был не равен нулю:
    $
        Phi'_2 = mat(0, 1/2, 0; 0, 1, 0; 0, 0, 1),
    $ а для этого требуется, чтобы определитель $phi'_u$ из доказательства был ненулевым. А что такое в нашем случае $phi$? Это $phi(x, y, z) = y/2$ --- первая одна координата, а $phi'_x = 0$. Получается, что обратимости $phi_x$ нет, значит нет обратимости $Phi_2$.

    Ок, а как тогда нормально декомпозировать? Давайте для начала посмотрим на $Phi'$:
    $
        Phi' = mat(0, 1/2, 0; 0, 0, -2z; 1/3, 0, 0).
    $

    Проблемы начались, как только мы попыталсь обратить $Phi_2$. Так давайте выберем $Phi_2$ как-то по-другому. Этот диффеоморфизм обязан сохранять $2$ координаты, быть обратимым, и посчитать что-то, чтобы следующий диффеоморфизм ($Phi_1$) мог сохранить одну. Попробуем просто угадать.

    Например, скажем, что $y$ и $z$ мы обязательно сохраним. Тогда у нас должен иметься способ вывести $x$. $Phi(x, y, z) = (y/2, 1 - z^2, x/3)$. Например, попробуем $Phi_2 (x, y, z) = (x/3, y, z)$. Так мы посчитали $x/3$, и $Phi_1$ не придется его пересчитывать. Тогда $Phi_1 (x, y, z) = (y/2, 1 - z^2, x)$. Их композиция и правда $Phi$.

    Хорошо, а как без угадывания? В построении из леммы, мы хотели, чтобы $phi'_u$ --- уголовой минор матрицы $Phi'$, был ненулевым. Тогда $Phi_2$ будет обратимым автоматически. Давайте заставим этот минор быть ненулевым. Для этого мы добавим третий диффеоморфизм $Phi_0^(-1)$ в конец, который будет переставлять переменные как мы хотим. То есть теперь
    $
        Phi = Phi_0^(-1) compose Phi_1 compose Phi_2,
    $
    и $Phi_0$ --- просто перестановка переменных. В нашем примере подойдет перестановка
    $
        Phi_0 (x, y, z) = (z, x, y), space Phi_0^(-1) (x, y, z) = (y, z, x).
    $
    Тогда
    $
        Phi_1 compose Phi_2 = Phi_0 compose Phi = (x/2, y/3, 1-z^2)
    $
    и
    $
        Phi_1 compose Phi_2 = mat(
            1/2, 0, 0; 0, 1/3, 0; 0, 0, -2z
        )
    $
    А вот у этой штуки уже угловой минор имеет определитель $1/2$.

    Давайте доделаем, для честности.
    $
        Phi_1 (x, y, z) &= (x, f_y (x, y, z), f_z (x, y, z)), \
        Phi_2 (x, y, z) &= (g(x, y, z), y, z).
    $
    $
        Phi_1 compose Phi_2 = (g(x, y, z), f_y (g(x, y, z), y, z), f_z (g(x, y, z), y, z)) = (x/3, y/2, 1-z^2).
    $
    Отсюда $g(x, y, z) = x/3$, $f(x, y, z) = (y/2, 1 - z^2)$, и
    $
        Phi_1 (x, y, z) = (x, y/2, 1-z^2),\
        Phi_2 (x, y, z) = (x/3, y, z).
    $
    Только пока что $Phi_1 compose Phi_2 != Phi$, надо еще сделать что-то с $Phi_0$. Приделаем $Phi_0^(-1)$ к $Phi_1$, получим $Phi'_1$:
    $
        Phi'_1 (x, y, z) = Phi_0^(-1) compose Phi_1 = (y/2, 1 - z^2, x)
    $
    И вот теперь $Phi'_1 compose Phi_2 = Phi$.
    
    /*
    Сохранить $y$ и $z$ не получиться --- мы уже пробовали. Попробуем сохранить $x$ и $z$:
    $ Phi_2 (x, y, z) = (x, g(x, y, z), z). $
    Тогда $Phi_1$ обязан сохранить $y$:
    $ Phi_1 (x, y, z) = (f_x (x, y, z), y, f_z (x, y, z)). $
    И требуется, чтобы
    $
        Phi_1 compose Phi_2 = Phi ==>
        (f_x (x, g(x, y, z), z), g(x, y, z), f_z (x, g(x, y, z), z)) = (y/2, 1 - z^2, x / 3).
    $
    Отсюда легко найти $g(x, y, z) = 1 - z^2$. Тогда
    $ f(x, 1 - z^2, z) = (y/2, x/3)$. Снова не повезло.

    К этому моменту становиться понятно, что чтобы получить обратимость $Phi_2$, нужно сохранить в $Phi_2$ такие координаты, чтобы по остальным можно было вывести $phi$. В нашем случае $phi = z/2$, а значит сохранить нужно $x$ и $y$. Попытка номер 3:
    $
        Phi_1 (x, y, z) &= (f_x (x, y, z), f_y (x, y, z), z),\
        Phi_2 (x, y, z) &= (x, y, g(x, y, z)).
    $
    И мы хотим, чтобы композиция была правильной:
    $
        Phi_1 compose Phi_2 = (f_x (x, y, g(x, y, z)), f_y (x, y, g(x, y, z)), g(x, y, z)) = (y/2, 1 - z^2, x / 3).
    $
    Отсюда, $g(x, y, z) = x/3$, и
    $
        f(x, y, x/3) = 
    $

    В доказательстве мы претворялись, что $Phi$ разбивается как $(phi, psi)$, но ничего не мешает нам разбить $Phi$, например, как $(psi_x, phi_y, psi_z)$. Давайте так и сделаем: $Phi = (#text(red, $y/2$), #text(blue, $1-z^2$), #text(red, $x/3$))$. Тогда $Phi_1$ будет оставлять на месте вторую координату, а $Phi_2$ --- первую и третью, то есть:
    $
        Phi_1 compose Phi_2 = (f_x (x, y, z), ) compose
    $
    */
]

#follow(label: "diffeomorphism-decomposition+")[
    Эту лемму#rf("diffeomorphism-decomposition") можно применить много раз.

    $Phi: Omega -> tilde(Omega)$ диффеоморфизм, $Omega, tilde(Omega) in RR^m$, $a in Omega$. Тогда найдется окрестность $U_a$ такая, что $Phi bar_(U_a) = Phi_1 compose Phi_2 compose ... compose Phi_m$, где каждая функция $Phi_i$ диффеоморфизм, который оставляет на месте все координаты, кроме одной.
]

#example(name: "да, все еще от меня, и все еще непонятный")[
    Можно просто расширить рассужение из леммы с двух функций на $n$. Доказательство получиться аналогично, просто будет больше букв и индексов. Но давайте сделаем по другому. Я покажу на примере, не строго, как получить это по индукции.

    Давайте снова посмотрим на наш пример, и декомпозируем $Phi$ полностью. Мы знаем, что
    $
        Phi'_1 = (y/2, 1-z^2, x), Phi_2 = (x/3, y, z) ==> Phi'_1 compose Phi_2 = Phi.
    $
    $Phi_2$ уже оставляет все координаты кроме одной ($x$).

    Разложим $Phi'_1$ на $Phi_3$ и $Phi_4$ (да, нумерация совсем сбилась, ну и ладно). И $Phi_3$, и $Phi_4$ должны сохранять на месте 2 координаты... Только лемма такого не умеет: она суммарно может сохранить 3 координаты, а мы хотим 4. С другой стороны, у нас уже одна координата стоит на месте: $x$. Давайте рассмотрим диффеоморфизм $Psi: RR^2 --> RR^2$ такой, что $Phi'_1(x, y, z) = (Psi (y, z), x)$. Тогда про $x$ не нужно думать вообще. Применим рассуждения из леммы к $Psi$ и разложим его как $Psi_1 compose Psi_2$. Абсолютно аналогичными рассуждениями,
    $
        Psi_1 (y, z) = (y, 1 - z^2), space Psi_2 (y, z) = (y/2, z).
    $
    Нетрудно убедиться, что и правда, $Psi_1 compose Psi_2 = Psi$.

    Теперь восстановим $Phi_3$ и $Phi_4$:
    $
        (Phi_3 compose Phi_4) (x, y, z) = ((Psi_1 compose Psi_2)(y, z), x).
    $
    Подойдут, например
    $
        Phi_4 (x, y, z) &= (x, Psi_2 (y, z)) = (x, y/2, z),\
        Phi_3 (x, y, z) &= (Psi_1 (y, z), x) = (y, 1-z^2, x).
    $
]

#th(name: "Линделёфа", label: "lindelof")[
    Из любого покрытия $Omega subset RR^m$ открытыми множествами можно выбрать не более чем счетное подпокрытие.
]

#proof[
    Пусть $Omega subset Union_(alpha in I) G_alpha$, где $G_alpha$ открытые. Возьмем $a in Omega$. Найдется $beta in I$ такое, что $a in G_beta$. Оно открытое, поэтому $B_r (a) subset G_beta$. Пошевелим точку так, чтобы радиус и координаты точки стали рациональными, в нем все еще лежала точка $a$, то есть сделаем шар такой, что $a in B_tilde(r) (b) subset B_r (a) subset G_beta.$ Но таких шариков не более чем счетно. Для каждого шарика оставляем один элемент покрытия, который его содержит, получаем что хотели.
]

#th(label: "measure-diffeomorphism")[
    Пусть $Phi: Omega -> tilde(Omega)$ --- диффеоморфизм, $Omega, tilde(Omega) in RR^m$. $A subset tilde(Omega)$ измеримо. Тогда $ lambda_m A = integral_(Phi^(-1) (A)) abs(Jj_Phi) dif lambda_m. $
]

Сейчас мы докажем, что из этой теоремы будет следовать формула замены переменной#rf("substitution"), причем не просто целиком из теоремы, а для любого частного случая $Phi$ получается, что можно подставлять в интеграл $Phi$. То есть чтобы доказать формулу замены переменной, нужно доказать эту формулу для произвольного диффеоморфизма. Однако это сложно сделать сразу, поэтому мы будем доказывать формулу по шагам, каждый раз доказывая ее для каких-то $Phi$ (через это доказывая теорему о замене переменной), и затем пользоваться заменой переменной для доказанных частных случаев чтобы доказать теорему для новых $Phi$.

#pr(label: "substitution-temp")[
    Если теорема#rf("measure-diffeomorphism") верна для конкретного $Phi$, то для того же $Phi$ верна формула замены переменной#rf("substitution").
]

#proof[
    1. $f = bb(1)_A$. Из теоремы#rf("measure-diffeomorphism"), 
        $ 
            integral_tilde(Omega) bb(1)_A dif lambda_m =
            lambda_m A =^rf("measure-diffeomorphism")
            integral_(Phi^(-1) (A)) abs(Jj_Phi) dif lambda_m =
            integral_Omega underbrace(bb(1)_(Phi^(-1) (A)), bb(1)_A compose Phi) abs(Jj_Phi) dif lambda_m =
            integral_Omega (bb(1)_A compose Phi) dot abs(Jj_Phi) dif lambda_m.
        $

    2. $f$ --- простая: верно по линейности.

    3. $f >= 0$ измеримая: записываем#rf("simple-approx") последовательность простых $0 <= phi_1 <= phi_2 <= ...$, $phi_n --> f$ поточечно. По теореме Леви#rf("levy") получаем что хотим. Не буду писать, все уже поняли.

    4. $f$ суммируема: ну там поделили на плюс минус и вычли.
]

#line(length: 100%)

#let Omegat = $tilde(Omega)$
#let Omegatt = $tilde(Omegat)$

#proof(name: "теоремы")[
    Запасайтесь попкорном.

    *Шаг 1: Пусть $Omega = Union U_n$ --- не более чем счетное объединение открытых множеств. Если теорема верна для каждого $U_n$, то она верна и для $Omega$*. Пусть $A = usb A_n$, $A_n subset U_n$. Тогда $Phi^(-1) (A_n)$ дизъюнктны, так как $Phi$ --- биекция. Тогда
    $ 
        lambda A =
        sum lambda A_n =^rf("measure-diffeomorphism")
        sum integral_(Phi^(-1) (A_n)) abs(Jj_Phi) dif lambda =^rf("mfn-props''", "set-additive")
        integral_(Phi^(-1) (A)) abs(Jj_Phi) dif lambda.
    $

    *Шаг 2: Если теорема верна для диффеоморфизмов $Phi$ и $Psi$, то она верна и для $Phi compose Psi$*. Пусть $ Omega -->^Phi Omegat -->^Psi Omegatt, A subset Omegatt. $
    Тогда
    $
        lambda A =^rf("measure-diffeomorphism")
        integral_(Psi^(-1)(A)) abs(Jj_psi (x)) dif lambda(x) =^((*))
        integral_(Phi^(-1)(Psi^(-1)(A))) abs(Jj_Psi (Phi (x))) dot abs(Jj_Phi (x)) dif lambda(x) newline(=)
        integral_(Phi^(-1)(Psi^(-1)(A))) abs(det (Psi'(Phi (x)))) dot abs(det Phi' (x)) dif lambda(x) =
        integral_(Phi^(-1)(Psi^(-1)(A))) abs(det (Psi'(Phi) Phi')) dif lambda newline(=)
        integral_(Phi^(-1)(Psi^(-1)(A))) abs(det (Psi compose Phi)') dif lambda =
        integral_(Phi^(-1)(Psi^(-1)(A))) abs(Jj_(Phi compose Psi)) dif lambda.
    $
    Переход $(*)$ верен по теореме о замене переменной#rf("substitution"), которой, как мы выяснили#rf("substitution-temp"), здесь можно пользоватся.

    *Шаг 3: $m = 1$*. $ integral_(a, b] abs(phi') dif lambda_1 = abs(phi(a) - phi(b)) = lambda_1 (phi(a), phi(b)]. $ Это формула Ньютона-Лейбница. 

    Определим $nu A = integral_(phi^(-1)(A)) abs(phi') dif lambda_1$ --- мера, которая на ячейках совпадает с $lambda_1$. Значит $nu = lambda_1$ по единственности продолжения#rf("standard-continuation-unique"). Значит и для всех остальных измеримых множеств формула работает.

    *Шаг 4: Теорема верна для диффеоморфизмов, которые оставляют все координаты кроме одной*.

    $Phi: Omega --> Omegat$ диффеоморфизм, не изменяющий $m - 1$ координаты. Диффеоморфизм может их переставлять, но нам и не важно, то теореме Тонелли#rf("tonelli") или Фубини#rf("fubini"), перестановка не меняет значение интеграла. Более того, потребуем, чтобы диффеоморфизм не трогал именно первые $m - 1$ координаты. Пусть $(y, t)$, где $y in RR^(m - 1)$, $t in RR$ --- аргументы $Phi$. Тогда $Phi(y, t) = (y, phi(y, t))$.
    $ lambda_m Phi(A) =_"Кавальери"^rf("cavalieri") integral_(RR^(m - 1)) lambda_1 (Phi (A))_y dif lambda_(m - 1) (y). $
    Посмотрим на сечения поближе: 
    $ 
        (Phi(A))_y =
        {s in RR: exists a in A space Phi(a) = (y, s)} =
        {s in RR: exists x in A_y space Phi(y, x) = (y, s)} newline(=)
        {s in RR: exists x in A_y space phi(y, x) = s} =
        phi(y, A_y).
    $
    Значит
    $
        integral_(RR^(m - 1)) lambda_1 (Phi (A))_y dif lambda_(m - 1) (y) = integral_(RR^(m - 1)) lambda_1 (phi(y, A_y)) dif lambda_(m - 1) (y) = \ integral_(RR^(m - 1)) integral_(A_y) abs(phi'_t (y, t)) dif lambda_1 (t) dif lambda_(m - 1) (y).
    $
    В последнем переходе мы воспользовались предыдущим шагом: мера $lambda_1$ равняется внутреннему интегралу, так как для одномерного случая мы уже это знаем. Посмотрим на $Phi'$:
    $
        Phi' = mat(E, 0; phi'_(y_1) ... phi'_(y_(m - 1)), phi'_t).
    $
    Якобиан $Phi$ тогда равен $phi'_t$. Значит
    $
        integral_(RR^(m - 1)) integral_(A_y) abs(phi'_t (y, t)) dif lambda_1 (t) dif lambda_(m - 1) (y) = 
        integral_(RR^(m - 1)) integral_(A_y) abs(Jj_Phi) dif lambda_1 (t) dif lambda_(m - 1) (y) 
        =^(rf("tonelli") rf("fubini"))_"Тонелли\nФубини"
        integral_A abs(Jj_Phi) dif lambda_m.
    $

    #line(length: 100%)

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

    Рассматрим каждую точку $a in Omega$. Применим к каждой точке лемму#rf("diffeomorphism-decomposition+"). $U_a$ --- окрестность из леммы, $Phi bar_(U_a) = Phi_1 compose Phi_2 compose ... compose Phi_m$, где $Phi_i$ оставляют $m - 1$ координату.

    По теореме Линделёфа#rf("lindelof") оставляем не более чем счетное количество окрестностей.
    
    Шаг 1 говорит, что достаточно проверить теорему только для этих $U_a$, и для всего $Omega$ она будет верна. Шаг 2 говорит, что достаточно проверить утверждение для произвольного $Phi_j$, и для композиции всех теорема тоже будет верна. Шаг 4 осуществляет проверку для $Phi_j$, опираясь на шаг 3.

    Теорема доказана.

    Значит формула замены переменной тоже доказана#rf("substitution-temp").
]

#notice[
    Можно записать формулу по-другому:
    $ integral_(Phi(A)) f dif lambda_m = integral_A (f compose Phi) abs(Jj_Phi) dif lambda_m. $
    Здесь $Phi: Omega --> Omegat$ диффеоморфизм, $A subset Omega$.
]

#proof[
    $
        integral_(Phi(A)) f dif lambda_m =
        integral_(Omegat) bb(1)_(Phi(A)) dot f dif lambda_m =^rf("substitution")
        integral_Omega f compose Phi dot bb(1)_A dot abs(Jj_Phi) dif lambda =
        integral_A (f compose Phi) abs(Jj_Phi) dif lambda_m.
    $
]

#notice[
    $Phi: Omega --> Omegat$ такое, что $exists e in Omega$ и $tilde(e) in Omegat$, такое, что $lambda e = lambda tilde(e) = 0$, и $Phi bar_(Omega without e): Omega without e --> tilde(Omega) without tilde(e)$ --- диффеоморфизм, и то формула все равно верна.
]

#proof[
    Выкинем из интегралов слева и справа эти множества нулевой меры. Интегралы не изменятся.
]

#example(label: "gaussian-integral")[
    Полярные координаты: $(r, t) ~~> (r cos t, r sin t)$, преобразовывающие "полосу" в плоскость без прямой.

    Тогда $ vec(r, t) -->^Phi vec(r cos t, r sin t), Phi' = mat(cos t, -r sin t; sin t, r cos t) ==> Jj_Phi = det Phi' = r cos^2 t + r sin^2 t = r. $
    Записываем формулу замены переменной#rf("substitution") (теорема Фубини#rf("fubini") позволяет записать интеграл по двумерному множеству как двойной):
    $
        integral_(RR^2) f dif lambda_2 = integral_([0, +oo)) integral_([0, 2pi]) r f (r cos t, r sin t) dif lambda_1 (t) dif lambda_1 (r). 
    $
    Подставим $f(x, y) = e^(-x^2 - y^2)$, $f(r cos t, r sin t) = e^(-r^2)$:
    $
        integral_(RR^2) e^(-x^2 - y^2) dif x dif y = integral_0^(+oo) integral_0^(2pi) r e^(-r^2) dif t dif r = 2pi integral_0^(+oo) r e^(-r^2) dif r = (- pi e^(-r^2)) bar_0^(+oo) = pi.
    $
    Кстати,
    $
        integral_(RR^2) e^(-x^2 - y^2) dif x dif y = integral_RR e^(-x^2) dif x dot integral_RR e^(-y^2) dif y = (integral_RR e^(-x^2) dif x)^2 ==> integral_RR e^(-x^2) dif x = sqrt(pi).
    $
    Этот интеграл иногда оказывается полезен.
 ]
