11.3. Fubiniの定理🔗

Fubiniの定理は，符号がある関数でも絶対可積分なら積分順序を交換できる，という定理である． Tonelliが「非負ならよい」という定理であるのに対し，Fubiniは「絶対値が積分できるならよい」という定理である．

Theorem11.3.1

uses 1used by 1✓L∃∀N

Tagsleanok

Fubiniの定理. f\in\calL^1(X\times Y) とする．このとき，\mu-a.e. の x\in X に対して f_x\in\calL^1(Y) であり， \nu-a.e. の y\in Y に対して f^y\in\calL^1(X) である．さらに，g(x):=\int_Y f(x,y)\,d\nu(y) と h(y):=\int_X f(x,y)\,d\mu(x) は a.e. の値を適当に定めれば g\in\calL^1(X)，h\in\calL^1(Y) となり，

\int_{X\times Y} f\,d(\mu\otimes\nu)=\int_X\!\int_Y f(x,y)\,d\nu(y)\,d\mu(x)=\int_Y\!\int_X f(x,y)\,d\mu(x)\,d\nu(y)

が成り立つ．

Lean code for Theorem11.3.1●5 theorems

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.ae_integrable_section_right.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E]
  [MeasureTheory.SFinite ν] {f : α × β → E}
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y ↦ f (x, y)) ν

theorem NoteKsk.Chapter11.ae_integrable_section_right.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E]
  [MeasureTheory.SFinite ν]
  {f : α × β → E}
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  ∀ᵐ (x : α) ∂μ,
    MeasureTheory.Integrable
      (fun y ↦ f (x, y)) ν

Almost-everywhere integrability of sections.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.fubini_integral_prod.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] (f : α × β → E)
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

theorem NoteKsk.Chapter11.fubini_integral_prod.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  (f : α × β → E)
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν =
    ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

Fubini's theorem for Bochner integrals.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.fubini_integral_prod_symm.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (f : α × β → E)
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

theorem NoteKsk.Chapter11.fubini_integral_prod_symm.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  (f : α × β → E)
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  ∫ (z : α × β), f z ∂μ.prod ν =
    ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Fubini's theorem with the order of integration reversed.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.integrable_integral_section_right.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite ν] {f : α × β → E}
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  MeasureTheory.Integrable (fun x ↦ ∫ (y : β), f (x, y) ∂ν) μ

theorem NoteKsk.Chapter11.integrable_integral_section_right.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite ν]
  {f : α × β → E}
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  MeasureTheory.Integrable
    (fun x ↦ ∫ (y : β), f (x, y) ∂ν) μ

Integrability of the function obtained by integrating the right section.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.integrable_integral_section_left.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {f : α × β → E}
  (hf : MeasureTheory.Integrable f (μ.prod ν)) :
  MeasureTheory.Integrable (fun y ↦ ∫ (x : α), f (x, y) ∂μ) ν

theorem NoteKsk.Chapter11.integrable_integral_section_left.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {f : α × β → E}
  (hf :
    MeasureTheory.Integrable f
      (μ.prod ν)) :
  MeasureTheory.Integrable
    (fun y ↦ ∫ (x : α), f (x, y) ∂μ) ν

Integrability of the function obtained by integrating the left section.

Proof for Theorem 11.3.1

uses 0

Fubiniの定理はTonelliの定理から導く．まず |f| にTonelliを適用し，f\in\calL^1(X\times Y) ならほとんどすべての切片で \int_Y |f(x,y)|\,d\nu(y)<\infty，\int_X |f(x,y)|\,d\mu(x)<\infty となることを得る．そのうえで f=f^+-f^- と分解し，f^+ と f^- にTonelliを適用して差を取る．つまり，証明の流れは「積測度の構成 \to 集合に関するFubini \to 非負関数のTonelli \to 可積分関数のFubini」である．

Remark (ベクトル値の場合). Fubiniの定理は，実数値関数だけでなく有限次元ベクトル値関数にも同じ形で成り立つ．その場合は，絶対値をノルムに置き換えて \int_{X\times Y}\|f(x,y)\|\,d(\mu\otimes\nu)<\infty を確認すればよい．この講義の範囲では，各成分に実数値のFubiniの定理を適用すると思えば十分である．

Corollary11.3.2

Statement uses 2

Statement dependency previews

Preview

Theorem 11.2.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Proposition 11.3.3

Loading preview

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

✓L∃∀N

積分順序の交換判定. f\in M(X\times Y) とする．このとき，|f|\ge0 にTonelliを適用すると

\int_{X\times Y}|f|\,d(\mu\otimes\nu) = \int_X\!\int_Y |f(x,y)|\,d\nu(y)\,d\mu(x) = \int_Y\!\int_X |f(x,y)|\,d\mu(x)\,d\nu(y)

が [0,\infty] の値として成り立つ．したがって，この3つの量のどれか一つが有限なら f\in\calL^1(X\times Y) であり，

\int_X\!\int_Y f(x,y)\,d\nu(y)\,d\mu(x)=\int_Y\!\int_X f(x,y)\,d\mu(x)\,d\nu(y)

が成り立つ．実際の計算では，直接の積分，x から先に積分する反復積分，y から先に積分する反復積分のうち，有限性を確かめやすいものを一つ調べればよい．

Lean code for Corollary11.3.2●1 theorem

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.integral_integral_swap.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {f : α → β → E}
  (hf : MeasureTheory.Integrable (Function.uncurry f) (μ.prod ν)) :
  ∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ = ∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν

theorem NoteKsk.Chapter11.integral_integral_swap.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {f : α → β → E}
  (hf :
    MeasureTheory.Integrable
      (Function.uncurry f) (μ.prod ν)) :
  ∫ (x : α), ∫ (y : β), f x y ∂ν ∂μ =
    ∫ (y : β), ∫ (x : α), f x y ∂μ ∂ν

Exchange of iterated integrals for an integrable function.

Proposition11.3.3

uses 1used by 0⚠L∃∀N

Tagsexample

順序交換できない例. Q=(0,1)^2 上で

f(x,y):=\frac{x^2-y^2}{(x^2+y^2)^2}

とおく．この関数は原点の近くで絶対可積分ではないので，Fubiniの定理は適用できない．実際，0<y<x/2 では

|f(x,y)| \ge \frac{12}{25}\frac1{x^2}

であるから，

\int_0^1\int_0^{x/2}|f(x,y)|\,dy\,dx \ge \int_0^1\frac{6}{25}\frac{dx}{x} =\infty

となる．

一方で，反復積分そのものはそれぞれ計算できる． x>0 を固定すると

\int_0^1 f(x,y)\,dy = \left[\frac{y}{x^2+y^2}\right]_{y=0}^{1} = \frac1{1+x^2}

である．したがって

\int_0^1\left(\int_0^1 f(x,y)\,dy\right)dx = \int_0^1\frac{dx}{1+x^2} = \frac{\pi}{4}

である．逆に，y>0 を固定すると

\int_0^1 f(x,y)\,dx = \left[-\frac{x}{x^2+y^2}\right]_{x=0}^{1} = -\frac1{1+y^2}

であるから，

\int_0^1\left(\int_0^1 f(x,y)\,dx\right)dy = -\int_0^1\frac{dy}{1+y^2} = -\frac{\pi}{4}

となる．このように，絶対可積分性を確認せずに積分順序を交換すると，反復積分の値が変わることがある．

Lean code for Proposition11.3.3●3 theorems, 3 incomplete

theoremdefined in NoteKsk/«11fubini».lean

contains sorry

theorem NoteKsk.Chapter11.fubiniCounterexample_not_integrable :
  ¬MeasureTheory.Integrable NoteKsk.Chapter11.fubiniCounterexample
      (MeasureTheory.volume.restrict (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1))

theorem NoteKsk.Chapter11.fubiniCounterexample_not_integrable :
  ¬MeasureTheory.Integrable
      NoteKsk.Chapter11.fubiniCounterexample
      (MeasureTheory.volume.restrict
        (Set.Ioo 0 1 ×ˢ Set.Ioo 0 1))

The counterexample is not absolutely integrable on `(0, 1)²`.

theoremdefined in NoteKsk/«11fubini».lean

contains sorry

theorem NoteKsk.Chapter11.fubiniCounterexample_integral_y_first :
  ∫ (x : ℝ) (y : ℝ) in 0..1,
      NoteKsk.Chapter11.fubiniCounterexample (x, y) =
    Real.pi / 4

theorem NoteKsk.Chapter11.fubiniCounterexample_integral_y_first :
  ∫ (x : ℝ) (y : ℝ) in 0..1,
      NoteKsk.Chapter11.fubiniCounterexample
        (x, y) =
    Real.pi / 4

Integrating first in the second variable gives `π / 4`.

theoremdefined in NoteKsk/«11fubini».lean

contains sorry

theorem NoteKsk.Chapter11.fubiniCounterexample_integral_x_first :
  ∫ (y : ℝ) (x : ℝ) in 0..1,
      NoteKsk.Chapter11.fubiniCounterexample (x, y) =
    -Real.pi / 4

theorem NoteKsk.Chapter11.fubiniCounterexample_integral_x_first :
  ∫ (y : ℝ) (x : ℝ) in 0..1,
      NoteKsk.Chapter11.fubiniCounterexample
        (x, y) =
    -Real.pi / 4

Integrating first in the first variable gives `-π / 4`.

Proposition11.3.4

uses 0used by 0XL∃∀N

Tagsexample

積分領域の入れ替え. 連続関数 \varphi:[0,1]\to\RR に対して Fubiniより \int_0^1(\int_0^x \varphi(y)\,dy)dx=\int_0^1(\int_y^1 \varphi(y)\,dx)dy=\int_0^1(1-y)\varphi(y)\,dy である．これは領域 0\le y\le x\le1 を，0\le y\le1，y\le x\le1 と読み替えただけである．例えば \varphi(y)=e^{y^2} のように原始関数が初等的に書けない場合でも，順序交換により計算しやすい形へ変えられる．

Proposition11.3.5

Statement uses 2

Statement dependency previews

Preview

Theorem 11.2.1

Loading preview

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

used by 1⚠L∃∀N

Tagsexample

畳み込み積分. 以下の積分は \RR^d 上のLebesgue積分とする． f,g\in\calL^1(\RR^d) に対して，ほとんどすべての x\in\RR^d で

(f*g)(x):=\int_{\RR^d} f(x-y)g(y)\,dy

と定める．この積分が a.e. で意味をもつことと，f*g\in\calL^1(\RR^d) であることはFubini--Tonelliから分かる．

実際，非負関数 |f(x-y)||g(y)| にTonelliを適用し，内側の積分で平行移動 u=x-y を用いると，

\int_{\RR^d}\!\int_{\RR^d}|f(x-y)||g(y)|\,dy\,dx = \int_{\RR^d}\left(\int_{\RR^d}|f(x-y)|\,dx\right)|g(y)|\,dy = \|f\|_1\|g\|_1 <\infty

となる．したがって，ほとんどすべての x について \int_{\RR^d}|f(x-y)||g(y)|\,dy<\infty であり，畳み込み f*g が a.e. で定義できる．さらに三角不等式と上の計算から

\|f*g\|_1 \le \int_{\RR^d}\!\int_{\RR^d}|f(x-y)||g(y)|\,dy\,dx = \|f\|_1\|g\|_1

を得る．これはYoungの不等式の最も基本的な場合であり，畳み込みが \calL^1(\RR^d) を再び \calL^1(\RR^d) に送ることを表している．

Lean code for Proposition11.3.5●3 declarations, 1 incomplete

defdefined in NoteKsk/«11fubini».lean

complete

def NoteKsk.Chapter11.convolutionRd {d : ℕ}
  (f g : NoteKsk.Chapter11.Rd d → ℝ) (x : NoteKsk.Chapter11.Rd d) : ℝ

def NoteKsk.Chapter11.convolutionRd {d : ℕ}
  (f g : NoteKsk.Chapter11.Rd d → ℝ)
  (x : NoteKsk.Chapter11.Rd d) : ℝ

Definition body

def convolutionRd {d : ℕ} (f g : Rd d → ℝ) (x : Rd d) : ℝ :=
  MeasureTheory.convolution f g (ContinuousLinearMap.mul ℝ ℝ)
    (volume : Measure (Rd d)) x

Convolution on `ℝᵈ`, using mathlib's convolution API.

theoremdefined in NoteKsk/«11fubini».lean

complete

theorem NoteKsk.Chapter11.convolutionRd_apply {d : ℕ}
  (f g : NoteKsk.Chapter11.Rd d → ℝ) (x : NoteKsk.Chapter11.Rd d) :
  NoteKsk.Chapter11.convolutionRd f g x =
    ∫ (y : NoteKsk.Chapter11.Rd d), f (x - y) * g y

theorem NoteKsk.Chapter11.convolutionRd_apply
  {d : ℕ}
  (f g : NoteKsk.Chapter11.Rd d → ℝ)
  (x : NoteKsk.Chapter11.Rd d) :
  NoteKsk.Chapter11.convolutionRd f g x =
    ∫ (y : NoteKsk.Chapter11.Rd d),
      f (x - y) * g y

The symmetric integral expression used in the lecture notes.

theoremdefined in NoteKsk/«11fubini».lean

contains sorry

theorem NoteKsk.Chapter11.convolution_l1_bound {d : ℕ}
  {f g : NoteKsk.Chapter11.Rd d → ℝ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hg : MeasureTheory.Integrable g MeasureTheory.volume) :
  MeasureTheory.Integrable (NoteKsk.Chapter11.convolutionRd f g)
      MeasureTheory.volume ∧
    ∫ (x : NoteKsk.Chapter11.Rd d),
        ‖NoteKsk.Chapter11.convolutionRd f g x‖ ≤
      (∫ (x : NoteKsk.Chapter11.Rd d), ‖f x‖) *
        ∫ (x : NoteKsk.Chapter11.Rd d), ‖g x‖

theorem NoteKsk.Chapter11.convolution_l1_bound
  {d : ℕ}
  {f g : NoteKsk.Chapter11.Rd d → ℝ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hg :
    MeasureTheory.Integrable g
      MeasureTheory.volume) :
  MeasureTheory.Integrable
      (NoteKsk.Chapter11.convolutionRd f
        g)
      MeasureTheory.volume ∧
    ∫ (x : NoteKsk.Chapter11.Rd d),
        ‖NoteKsk.Chapter11.convolutionRd f
            g x‖ ≤
      (∫ (x : NoteKsk.Chapter11.Rd d),
          ‖f x‖) *
        ∫ (x : NoteKsk.Chapter11.Rd d),
          ‖g x‖

The `L¹ * L¹ → L¹` estimate for convolution.

This is the basic Young inequality used in the text.  Mathlib supplies the
integrability part as `Integrable.integrable_convolution`; the norm estimate is
kept as the lecture-note statement.

Proposition11.3.6

uses 1used by 0⚠L∃∀N

Tagsexample

近似単位元. (\eta_\eps)_{\eps>0} を \RR^d 上の近似単位元とする．ここでは，\eta_\eps\ge0，\int_{\RR^d}\eta_\eps(y)\,dy=1 であり，任意の \delta>0 に対して

\int_{\{|y|\ge\delta\}}\eta_\eps(y)\,dy\longrightarrow0 \qquad(\eps\downarrow0)

が成り立つものをいう．典型例は，\eta\in\calL^1(\RR^d)，\eta\ge0，\int\eta=1 から \eta_\eps(x)=\eps^{-d}\eta(x/\eps) と作るものである．

f\in\calL^1(\RR^d) とする．畳み込みの例により f*\eta_\eps\in\calL^1(\RR^d) である．さらに \eps\downarrow0 のとき

\|f*\eta_\eps-f\|_1\longrightarrow0

が成り立つ．これが近似単位元という名前の意味である．

証明の要点はFubini--Tonelliによるノルム評価である． (\tau_y f)(x):=f(x-y) と書くと，\int\eta_\eps=1 より

(f*\eta_\eps)(x)-f(x) = \int_{\RR^d}\eta_\eps(y)\bigl(f(x-y)-f(x)\bigr)\,dy

である．三角不等式とTonelliにより

\|f*\eta_\eps-f\|_1 \le \int_{\RR^d}\eta_\eps(y)\|\tau_y f-f\|_1\,dy

\|f*\eta_\eps-f\|_1 \le \alpha + 2\|f\|_1\int_{\{|y|\ge\delta\}}\eta_\eps(y)\,dy

であり，右辺の第2項は \eps\downarrow0 で 0 に収束する．よって f*\eta_\eps\to f が \calL^1 で成り立つ．

Lean code for Proposition11.3.6●1 theorem, incomplete

theoremdefined in NoteKsk/«11fubini».lean

contains sorry

theorem NoteKsk.Chapter11.approximate_identity_l1_tendsto {d : ℕ}
  {η : ℝ → NoteKsk.Chapter11.Rd d → ℝ} {f : NoteKsk.Chapter11.Rd d → ℝ}
  (hη_nonneg :
    ∀ (ε : ℝ) (x : NoteKsk.Chapter11.Rd d), 0 < ε → 0 ≤ η ε x)
  (hη_mass :
    ∀ (ε : ℝ), 0 < ε → ∫ (x : NoteKsk.Chapter11.Rd d), η ε x = 1)
  (hη_tail :
    ∀ δ > 0,
      Filter.Tendsto
        (fun ε ↦ ∫ (x : NoteKsk.Chapter11.Rd d) in {x | δ ≤ ‖x‖}, η ε x)
        (nhdsWithin 0 (Set.Ioi 0)) (nhds 0))
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
  Filter.Tendsto
    (fun ε ↦
      ∫ (x : NoteKsk.Chapter11.Rd d),
        ‖NoteKsk.Chapter11.convolutionRd f (η ε) x - f x‖)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem NoteKsk.Chapter11.approximate_identity_l1_tendsto
  {d : ℕ}
  {η : ℝ → NoteKsk.Chapter11.Rd d → ℝ}
  {f : NoteKsk.Chapter11.Rd d → ℝ}
  (hη_nonneg :
    ∀ (ε : ℝ)
      (x : NoteKsk.Chapter11.Rd d),
      0 < ε → 0 ≤ η ε x)
  (hη_mass :
    ∀ (ε : ℝ),
      0 < ε →
        ∫ (x : NoteKsk.Chapter11.Rd d),
            η ε x =
          1)
  (hη_tail :
    ∀ δ > 0,
      Filter.Tendsto
        (fun ε ↦
          ∫ (x :
            NoteKsk.Chapter11.Rd d) in
            {x | δ ≤ ‖x‖}, η ε x)
        (nhdsWithin 0 (Set.Ioi 0))
        (nhds 0))
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume) :
  Filter.Tendsto
    (fun ε ↦
      ∫ (x : NoteKsk.Chapter11.Rd d),
        ‖NoteKsk.Chapter11.convolutionRd f
              (η ε) x -
            f x‖)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Convergence of an approximation to the identity in `L¹`.

The hypotheses encode the usual positivity, mass-one, and tail concentration
conditions for the kernels `η ε`.