11.4. 変数変換🔗

ここからはLebesgue測度に固有の話に戻る．変数変換では，写像によって面積や体積がどれだけ伸び縮みするかを補正する必要がある．この補正係数がJacobianの絶対値である．

Theorem11.4.1

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 11.4.2

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Tagsleanok

一般の変数変換公式. U,V\subset\RR^d を開集合とし，\Phi:U\to V を C^1 級微分同相写像とする． f\in M^+(V) または f\in\calL^1(V) なら

\int_V f(x)\,d\lambda_d(x)=\int_U f(\Phi(u))\,|\det D\Phi(u)|\,d\lambda_d(u)

が成り立つ．

Lean code for Theorem11.4.1●2 theorems

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E}
  {φ : E → E} {φ' : E → E →L[ℝ] E} (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (hs : MeasurableSet s)
  (hφ' : ∀ x ∈ s, HasFDerivWithinAt φ (φ' x) s x) (hφ : Set.InjOn φ s)
  (g : E → ENNReal) :
  ∫⁻ (x : E) in φ '' s, g x ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(φ' x).det| * g (φ x) ∂μ

theorem NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {s : Set E} {φ : E → E}
  {φ' : E → E →L[ℝ] E}
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure]
  (hs : MeasurableSet s)
  (hφ' :
    ∀ x ∈ s,
      HasFDerivWithinAt φ (φ' x) s x)
  (hφ : Set.InjOn φ s) (g : E → ENNReal) :
  ∫⁻ (x : E) in φ '' s, g x ∂μ =
    ∫⁻ (x : E) in s,
      ENNReal.ofReal |(φ' x).det| *
        g (φ x) ∂μ

Jacobian change-of-variables formula for nonnegative functions.

This is the formal replacement for the lecture's affine/linear change of
variables statements.  Those are obtained by taking `f` to be an affine map and
`f'` to be its constant derivative.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {φ : E → E}
  {φ' : E → E →L[ℝ] E} (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (hs : MeasurableSet s)
  (hφ' : ∀ x ∈ s, HasFDerivWithinAt φ (φ' x) s x) (hφ : Set.InjOn φ s)
  (g : E → F) :
  ∫ (x : E) in φ '' s, g x ∂μ =
    ∫ (x : E) in s, |(φ' x).det| • g (φ x) ∂μ

theorem NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  {s : Set E} {φ : E → E}
  {φ' : E → E →L[ℝ] E}
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure]
  (hs : MeasurableSet s)
  (hφ' :
    ∀ x ∈ s,
      HasFDerivWithinAt φ (φ' x) s x)
  (hφ : Set.InjOn φ s) (g : E → F) :
  ∫ (x : E) in φ '' s, g x ∂μ =
    ∫ (x : E) in s,
      |(φ' x).det| • g (φ x) ∂μ

Jacobian change-of-variables formula for Bochner integrals.

The lecture statement for a diffeomorphism is represented here by mathlib's
image formula on a measurable set with an injectivity hypothesis.

本節で扱う affine 変換，集合の体積の変換，平行四辺形の面積，極座標公式は，いずれもこの一般の変数変換公式から得られる．ただし極座標では，原点や角度の端点のような零集合を除いたり，球面を局所座標で分けたりして，一般公式を局所的に適用する．

Theorem11.4.2

uses 1used by 1✓L∃∀N

affine 変数変換. T\in GL(d,\RR)，b\in\RR^d とする． f\in M^+(\RR^d) または f\in\calL^1(\RR^d) なら

\int_{\RR^d} f(Tu+b)|\det T|\,d\lambda_d(u)=\int_{\RR^d}f(x)\,d\lambda_d(x)

が成り立つ．

Lean code for Theorem11.4.2●2 theorems

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E}
  {φ : E → E} {φ' : E → E →L[ℝ] E} (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (hs : MeasurableSet s)
  (hφ' : ∀ x ∈ s, HasFDerivWithinAt φ (φ' x) s x) (hφ : Set.InjOn φ s)
  (g : E → ENNReal) :
  ∫⁻ (x : E) in φ '' s, g x ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(φ' x).det| * g (φ x) ∂μ

theorem NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {s : Set E} {φ : E → E}
  {φ' : E → E →L[ℝ] E}
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure]
  (hs : MeasurableSet s)
  (hφ' :
    ∀ x ∈ s,
      HasFDerivWithinAt φ (φ' x) s x)
  (hφ : Set.InjOn φ s) (g : E → ENNReal) :
  ∫⁻ (x : E) in φ '' s, g x ∂μ =
    ∫⁻ (x : E) in s,
      ENNReal.ofReal |(φ' x).det| *
        g (φ x) ∂μ

Jacobian change-of-variables formula for nonnegative functions.

This is the formal replacement for the lecture's affine/linear change of
variables statements.  Those are obtained by taking `f` to be an affine map and
`f'` to be its constant derivative.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {φ : E → E}
  {φ' : E → E →L[ℝ] E} (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (hs : MeasurableSet s)
  (hφ' : ∀ x ∈ s, HasFDerivWithinAt φ (φ' x) s x) (hφ : Set.InjOn φ s)
  (g : E → F) :
  ∫ (x : E) in φ '' s, g x ∂μ =
    ∫ (x : E) in s, |(φ' x).det| • g (φ x) ∂μ

theorem NoteKsk.Chapter11.integral_image_eq_integral_abs_det_fderiv_smul.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  {s : Set E} {φ : E → E}
  {φ' : E → E →L[ℝ] E}
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure]
  (hs : MeasurableSet s)
  (hφ' :
    ∀ x ∈ s,
      HasFDerivWithinAt φ (φ' x) s x)
  (hφ : Set.InjOn φ s) (g : E → F) :
  ∫ (x : E) in φ '' s, g x ∂μ =
    ∫ (x : E) in s,
      |(φ' x).det| • g (φ x) ∂μ

Jacobian change-of-variables formula for Bochner integrals.

The lecture statement for a diffeomorphism is represented here by mathlib's
image formula on a measurable set with an injectivity hypothesis.

この公式は一般の変数変換公式で \Phi(u)=Tu+b とした特殊な場合である．このとき D\Phi=T は定数行列なので，Jacobian |\det D\Phi| は |\det T| になる．

Remark (向きと絶対値). \det T<0 のとき，向きつきの記法では符号が現れることがある．しかしLebesgue積分は集合上の積分なので向きを持たない．そのため変数変換では \det T ではなく |\det T| が現れる．

例えば1次元で f=1_{[0,1]} とし，x=-y とおく． Lebesgue積分では

\int_{\RR}1_{[0,1]}(x)\,d\lambda_1(x) = \int_{\RR}1_{[0,1]}(-y)\,d\lambda_1(y) = \lambda_1([-1,0]) =1

である．ここで出てくるのは |-1|=1 であり，符号は変わらない．一方，向きつきの微分形式として dx を扱うなら dx=-dy なので， 1-形式 1_{[0,1]}(x)\,dx を標準の向きをもつ y-軸へ引き戻すと

\int_{\RR}1_{[-1,0]}(y)(-dy) = -1

となる．この計算は，y が -1 から 0 へ増えるとき，対応する x=-y は 1 から 0 へ動くため，向きが反転していることを表している．通常の定積分の変数変換で同じ向きの区間を積分したい場合は，端点の順序も合わせて反転させるので，この符号が相殺される．

Lebesgue積分は体積を測る体系であり，向きは捨てて絶対値を取る．これに対して，線積分，面積分の向きつき版，微分形式の積分，Stokesの定理などは，向きまで含めて計算する体系である．したがって，そこではJacobianの符号や境界の向きが本質的な情報として残る．

Corollary11.4.3

uses 1used by 1✓L∃∀N

集合の体積の変換. T\in GL(d,\RR)，b\in\RR^d とし，A\subset\RR^d をLebesgue可測集合とする．このとき TA+b はLebesgue可測であり，\lambda_d(TA+b)=|\det T|\,\lambda_d(A) が成り立つ．

Lean code for Corollary11.4.3●1 theorem

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set E}
  {φ : E → E} {φ' : E → E →L[ℝ] E} (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (hs : MeasurableSet s)
  (hφ' : ∀ x ∈ s, HasFDerivWithinAt φ (φ' x) s x) (hφ : Set.InjOn φ s)
  (g : E → ENNReal) :
  ∫⁻ (x : E) in φ '' s, g x ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(φ' x).det| * g (φ x) ∂μ

theorem NoteKsk.Chapter11.lintegral_image_eq_lintegral_abs_det_fderiv_mul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {s : Set E} {φ : E → E}
  {φ' : E → E →L[ℝ] E}
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure]
  (hs : MeasurableSet s)
  (hφ' :
    ∀ x ∈ s,
      HasFDerivWithinAt φ (φ' x) s x)
  (hφ : Set.InjOn φ s) (g : E → ENNReal) :
  ∫⁻ (x : E) in φ '' s, g x ∂μ =
    ∫⁻ (x : E) in s,
      ENNReal.ofReal |(φ' x).det| *
        g (φ x) ∂μ

Jacobian change-of-variables formula for nonnegative functions.

This is the formal replacement for the lecture's affine/linear change of
variables statements.  Those are obtained by taking `f` to be an affine map and
`f'` to be its constant derivative.

Proposition11.4.4

uses 1used by 0XL∃∀N

Tagsexample

平行四辺形の面積. T=\begin{pmatrix}a&c\\ b&d\end{pmatrix} とし，Q:=[0,1]^2 とする．このとき TQ は原点を頂点にもつ平行四辺形であり， \lambda_2(TQ)=|\det T|\lambda_2(Q)=|ad-bc| である．

Proposition11.4.5

uses 1used by 0XL∃∀N

Tagsexample

極座標. \Phi(r,\theta)=(r\cos\theta,r\sin\theta) とおくと，Jacobianは |\det D\Phi(r,\theta)|=r である．厳密には原点と角度の端点を除いて微分同相な領域に分けて適用するが，零集合は積分値に影響しない．したがって非負可測関数または可積分関数 f:\RR^2\to\eRR に対して

\int_{\RR^2}f(x,y)\,dx\,dy=\int_0^\infty\!\int_0^{2\pi} f(r\cos\theta,r\sin\theta)\,r\,d\theta\,dr

が成り立つ．例えば f=1_{\{x^2+y^2\le R^2\}} とすれば， \lambda_2(\{x^2+y^2\le R^2\})=\int_0^R\int_0^{2\pi}r\,d\theta\,dr=\pi R^2 である．

Theorem11.4.6

uses 1used by 0XL∃∀N

\RR^n の極座標. n\ge2 とし，S^{n-1}:=\{u\in\RR^n\mid |u|=1\} とおく． \sigma を S^{n-1} 上の標準的な球面測度，すなわち正規化していない (n-1) 次元の表面積測度とする． f:\RR^n\to\eRR が非負可測関数または可積分関数なら，

\int_{\RR^n} f(x)\,dx = \int_0^\infty\int_{S^{n-1}} f(ru)\,r^{n-1}\,d\sigma(u)\,dr

が成り立つ．

Remark. この公式では，半径方向の長さ dr と，半径 r の球面 rS^{n-1} の表面積要素が分かれて現れる．球面の表面積は拡大率 r^{n-1} で伸びるため，Jacobianに対応する因子として r^{n-1} が出る．証明としては，球面 S^{n-1} を局所座標で覆い，各座標片で写像 (r,u)\mapsto ru に一般の変数変換公式を適用し，最後に足し合わせると考えればよい．例えば f=1_{\{|x|\le R\}} とすると， \lambda_n(\{x\in\RR^n\mid |x|\le R\})=\sigma(S^{n-1})R^n/n が得られる．

Remark (余面積公式). 余面積公式は，写像の値を固定したレベル集合に沿って積分を分解する定理である．例えば十分正則な写像 F:\RR^n\to\RR^m（m\le n）に対して，Jacobian J_F(x):=\sqrt{\det(DF(x)DF(x)^{\mathsf T})} を用いると，非負可測関数 g について形式的には

\int_{\RR^n} g(x)J_F(x)\,dx = \int_{\RR^m}\left(\int_{F^{-1}(y)} g(x)\,d\mathcal H^{n-m}(x)\right)dy

という形の公式が成り立つ．ここで \mathcal H^{n-m} はレベル集合上の (n-m) 次元面積測度である．一般の変数変換公式は，余面積公式の m=n の場合から得られる．実際，F=\Phi:U\to V が微分同相なら，レベル集合 \Phi^{-1}(y) は1点だけであり，\mathcal H^0 は点を数える測度になる．そこで g(u)=f(\Phi(u)) とおけば，余面積公式は

\int_U f(\Phi(u))|\det D\Phi(u)|\,du = \int_V f(y)\,dy

となり，一般の変数変換公式そのものになる．一方，F(x)=|x| と見れば，レベル集合 F^{-1}(r) は球面 rS^{n-1} であり，\RR^n の極座標公式は「半径ごとに球面上で積分する」公式として理解できる．