10.6. 積分記号下の連続性と微分🔗

Theorem10.6.1

uses 1used by 0✓L∃∀N

Tagsleanok

積分記号下の連続性. I\subset\RR を開区間とし，t_0\in I とする．関数 F:I\times X\to\RR が次を満たすとする．

各 t\in I に対して，F(t,\cdot)\in M(X;\RR) である
ほとんどすべての x\in X に対して，t\mapsto F(t,x) は t_0 で連続である
ある g\in\calL^1(X) が存在して，g\ge0 a.e. on X かつ |F(t,x)|\le g(x) がすべての t\in I と a.e. の x\in X で成り立つ

このとき

G(t):=\int_X F(t,x)\,d\mu(x)

は t_0 で連続である．

Lean code for Theorem10.6.1●2 theorems

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.continuous_integral_of_dominated.{u_1, u_2, u_3}
  {α : Type u_1} {X : Type u_2} {G : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [TopologicalSpace X]
  [FirstCountableTopology X] [NormedAddCommGroup G] [NormedSpace ℝ G]
  {F : X → α → G} {bound : α → ℝ}
  (hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) μ)
  (hbound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a)
  (hbound_int : MeasureTheory.Integrable bound μ)
  (hcont : ∀ᵐ (a : α) ∂μ, Continuous fun x ↦ F x a) :
  Continuous fun x ↦ ∫ (a : α), F x a ∂μ

theorem NoteKsk.Chapter10.continuous_integral_of_dominated.{u_1,
    u_2, u_3}
  {α : Type u_1} {X : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [TopologicalSpace X]
  [FirstCountableTopology X]
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  {F : X → α → G} {bound : α → ℝ}
  (hF_meas :
    ∀ (x : X),
      MeasureTheory.AEStronglyMeasurable
        (F x) μ)
  (hbound :
    ∀ (x : X),
      ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a)
  (hbound_int :
    MeasureTheory.Integrable bound μ)
  (hcont :
    ∀ᵐ (a : α) ∂μ,
      Continuous fun x ↦ F x a) :
  Continuous fun x ↦ ∫ (a : α), F x a ∂μ

Continuity under the integral sign by dominated convergence.

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.continuousAt_integral_of_dominated.{u_1, u_2, u_3}
  {α : Type u_1} {X : Type u_2} {G : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [TopologicalSpace X]
  [FirstCountableTopology X] [NormedAddCommGroup G] [NormedSpace ℝ G]
  {F : X → α → G} {bound : α → ℝ} {x₀ : X}
  (hF_meas :
    ∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ)
  (hbound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a)
  (hbound_int : MeasureTheory.Integrable bound μ)
  (hcont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x ↦ F x a) x₀) :
  ContinuousAt (fun x ↦ ∫ (a : α), F x a ∂μ) x₀

theorem NoteKsk.Chapter10.continuousAt_integral_of_dominated.{u_1,
    u_2, u_3}
  {α : Type u_1} {X : Type u_2}
  {G : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [TopologicalSpace X]
  [FirstCountableTopology X]
  [NormedAddCommGroup G] [NormedSpace ℝ G]
  {F : X → α → G} {bound : α → ℝ} {x₀ : X}
  (hF_meas :
    ∀ᶠ (x : X) in nhds x₀,
      MeasureTheory.AEStronglyMeasurable
        (F x) μ)
  (hbound :
    ∀ᶠ (x : X) in nhds x₀,
      ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a)
  (hbound_int :
    MeasureTheory.Integrable bound μ)
  (hcont :
    ∀ᵐ (a : α) ∂μ,
      ContinuousAt (fun x ↦ F x a) x₀) :
  ContinuousAt
    (fun x ↦ ∫ (a : α), F x a ∂μ) x₀

Pointwise continuity under the integral sign by dominated convergence.

Proof for Theorem 10.6.1

uses 0

t_n\to t_0 とする．仮定より F(t_n,x)\to F(t_0,x) が a.e. で成り立ち，また |F(t_n,x)|\le g(x) である．したがってTheorem 10.4.1より

\int_X F(t_n,x)\,d\mu(x)\to \int_X F(t_0,x)\,d\mu(x)

である．つまり，t_0 に収束する任意の点列 \{t_n\}\subset I に対して G(t_n)\to G(t_0) が成り立つ．実数上の関数では，これは t_0 での連続性と同値である．したがって G は t_0 で連続である．

Remark (点列で連続性を判定できる理由). 上の証明では，t_0 に収束する任意の点列 t_n に対して G(t_n)\to G(t_0) を示した．実数上の関数については，この性質は通常の \eps-\delta による連続性と同値である．実際，もし G が t_0 で連続でなければ，ある \eps_0>0 が存在して，どれほど t を t_0 に近づけても |G(t)-G(t_0)|\ge\eps_0 となる点が見つかる．各 n について |t_n-t_0|<1/n かつ |G(t_n)-G(t_0)|\ge\eps_0 を満たす t_n\in I を選べば， t_n\to t_0 なのに G(t_n)\not\to G(t_0) となる．したがって，任意の点列について G(t_n)\to G(t_0) が成り立つなら，G は t_0 で連続でなければならない．

Remark (局所支配で十分であること). Theorem 10.6.1の仮定 (3) は， I 全体ではなく t_0 の近傍でだけ仮定してもよい．すなわち，ある \delta>0 と g\in\calL^1(X) が存在して， g\ge0 a.e. on X かつ |F(t,x)|\le g(x) が t\in I\cap(t_0-\delta,t_0+\delta) と a.e. の x について成り立てば十分である．実際，t_n\to t_0 なら，有限個を除いて t_n\in I\cap(t_0-\delta,t_0+\delta) である．極限を調べるとき有限個の項は影響しないので，その後は同じ優関数 g を用いてTheorem 10.4.1を適用できる．

Theorem10.6.2

uses 1used by 1✓L∃∀N

Tagsleanok

積分記号下の微分. I \subset \RR を開区間とし，関数 F:I \times X \to \RR が次を満たすとする．

ほとんどすべての x \in X に対して，t \mapsto F(t,x) は I 上で C^1 級である
各 t \in I に対して，F(t,\cdot) と \partial_tF(t,\cdot) は M(X;\RR) に属する
ある t_0 \in I について F(t_0,\cdot)\in\calL^1(X) である
ある g\in\calL^1(X) が存在して，g\ge0 a.e. on X かつ |\partial_tF(t,x)|\le g(x) がすべての t \in I と a.e. の x \in X で成り立つ

このとき G(t):=\int_X F(t,x)\,d\mu(x) は I 上でよく定義されて微分可能であり， G'(t)=\int_X \partial_tF(t,x)\,d\mu(x) が成り立つ．

Lean code for Theorem10.6.2●2 theorems

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.hasFDerivAt_integral_under_dominated_loc_of_lip.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {H : Type u_4}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup H] [NormedSpace 𝕜 H] {F : H → α → E} {x₀ : H}
  {bound : α → ℝ} {s : Set H} {F' : α → H →L[𝕜] E} (hs : s ∈ nhds x₀)
  (hF_meas :
    ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ)
  (hF_int : MeasureTheory.Integrable (F x₀) μ)
  (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ)
  (h_lip :
    ∀ᵐ (a : α) ∂μ,
      LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) s)
  (hbound_int : MeasureTheory.Integrable bound μ)
  (h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀) :
  MeasureTheory.Integrable F' μ ∧
    HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

theorem NoteKsk.Chapter10.hasFDerivAt_integral_under_dominated_loc_of_lip.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {𝕜 : Type u_2}
  {E : Type u_3} {H : Type u_4}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedSpace 𝕜 E] [NormedAddCommGroup H]
  [NormedSpace 𝕜 H] {F : H → α → E}
  {x₀ : H} {bound : α → ℝ} {s : Set H}
  {F' : α → H →L[𝕜] E} (hs : s ∈ nhds x₀)
  (hF_meas :
    ∀ᶠ (x : H) in nhds x₀,
      MeasureTheory.AEStronglyMeasurable
        (F x) μ)
  (hF_int :
    MeasureTheory.Integrable (F x₀) μ)
  (hF'_meas :
    MeasureTheory.AEStronglyMeasurable F'
      μ)
  (h_lip :
    ∀ᵐ (a : α) ∂μ,
      LipschitzOnWith
        (Real.nnabs (bound a))
        (fun x ↦ F x a) s)
  (hbound_int :
    MeasureTheory.Integrable bound μ)
  (h_diff :
    ∀ᵐ (a : α) ∂μ,
      HasFDerivAt (fun x ↦ F x a) (F' a)
        x₀) :
  MeasureTheory.Integrable F' μ ∧
    HasFDerivAt
      (fun x ↦ ∫ (a : α), F x a ∂μ)
      (∫ (a : α), F' a ∂μ) x₀

Differentiation under the integral sign, Fréchet derivative form.

The lecture statement is the one-dimensional real special case.  Mathlib's
theorem works over `ℝ` or `ℂ` and for Fréchet derivatives.

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.hasDerivAt_integral_under_dominated_loc_of_lip.{u_1,
    u_2, u_3}
  {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [RCLike 𝕜] [NormedAddCommGroup E]
  [NormedSpace ℝ E] [NormedSpace 𝕜 E] {F : 𝕜 → α → E} {x₀ : 𝕜}
  {bound : α → ℝ} {s : Set 𝕜} {F' : α → E} (hs : s ∈ nhds x₀)
  (hF_meas :
    ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) μ)
  (hF_int : MeasureTheory.Integrable (F x₀) μ)
  (hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ)
  (h_lip :
    ∀ᵐ (a : α) ∂μ,
      LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) s)
  (hbound_int : MeasureTheory.Integrable bound μ)
  (h_diff : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x ↦ F x a) (F' a) x₀) :
  MeasureTheory.Integrable F' μ ∧
    HasDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

theorem NoteKsk.Chapter10.hasDerivAt_integral_under_dominated_loc_of_lip.{u_1,
    u_2, u_3}
  {α : Type u_1} {𝕜 : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [RCLike 𝕜]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedSpace 𝕜 E] {F : 𝕜 → α → E}
  {x₀ : 𝕜} {bound : α → ℝ} {s : Set 𝕜}
  {F' : α → E} (hs : s ∈ nhds x₀)
  (hF_meas :
    ∀ᶠ (x : 𝕜) in nhds x₀,
      MeasureTheory.AEStronglyMeasurable
        (F x) μ)
  (hF_int :
    MeasureTheory.Integrable (F x₀) μ)
  (hF'_meas :
    MeasureTheory.AEStronglyMeasurable F'
      μ)
  (h_lip :
    ∀ᵐ (a : α) ∂μ,
      LipschitzOnWith
        (Real.nnabs (bound a))
        (fun x ↦ F x a) s)
  (hbound_int :
    MeasureTheory.Integrable bound μ)
  (h_diff :
    ∀ᵐ (a : α) ∂μ,
      HasDerivAt (fun x ↦ F x a) (F' a)
        x₀) :
  MeasureTheory.Integrable F' μ ∧
    HasDerivAt
      (fun x ↦ ∫ (a : α), F x a ∂μ)
      (∫ (a : α), F' a ∂μ) x₀

Differentiation under the integral sign, one-dimensional derivative form.

Proof for Theorem 10.6.2

uses 0

まず G(t) が well-defined であることを示す．任意の t \in I と a.e. の x \in X に対して， 1変数の微分積分学の基本定理より F(t,x)-F(t_0,x)=\int_{t_0}^t \partial_sF(s,x)\,ds である．したがって

|F(t,x)| \le |F(t_0,x)|+\int_{t_0}^t |\partial_sF(s,x)|\,ds \le |F(t_0,x)|+|t-t_0|\,g(x).

右辺は可積分だから，F(t,\cdot) も可積分である．よって G(t) はよく定義される．

次に t \in I を固定し， h を十分小さく取って t+h \in I とする．差商 Q_h(x):=(F(t+h,x)-F(t,x))/h を考える．仮定 (1) と平均値の定理より， a.e. の x に対してある \theta=\theta(x,h)\in(0,1) が存在して Q_h(x)=\partial_tF(t+\theta h,x) となる．したがって仮定 (4) より |Q_h(x)|\le g(x) が a.e. で成り立つ．また t \mapsto F(t,x) の微分可能性から Q_h(x)\to \partial_tF(t,x) a.e. on X である．よってTheorem 10.4.1を Q_h に適用できて \lim_{h\to 0}\int_X Q_h(x)\,d\mu(x)=\int_X \partial_tF(t,x)\,d\mu(x) を得る．左辺は

\int_X Q_h(x)\,d\mu(x) =\frac{1}{h} \left(\int_X F(t+h,x)\,d\mu(x)-\int_X F(t,x)\,d\mu(x)\right) =\frac{G(t+h)-G(t)}{h}

だから G'(t)=\int_X \partial_tF(t,x)\,d\mu(x) が従う．

Remark (微分公式の局所版). Theorem 10.6.2も，固定した点 t\in I での微分公式を示すだけなら局所的な仮定で十分である．具体的には，F(t,\cdot)\in\calL^1(X) であり，さらに t のある近傍 J\subset I と g_t\in\calL^1(X) が存在して， |\partial_sF(s,x)|\le g_t(x) がすべての s\in J と a.e. の x について成り立てば，差商 (F(t+h,x)-F(t,x))/h は h が十分小さい範囲で g_t によって支配される．したがって同じ証明により，G は t で微分可能で G'(t)=\int_X \partial_tF(t,x)\,d\mu(x) が成り立つ．各 t\in I でこのような局所支配が成り立つなら，G は I 上で微分可能である．

Proposition10.6.3

uses 0used by 0XL∃∀N

Tagsexample

a>0 を固定し，([0,\infty),\calL([0,\infty)),\lambda) 上で

F(t,x):=e^{-tx}, \quad (t,x)\in (a,\infty)\times[0,\infty) を考える．このとき G(t):=\int_0^{\infty}e^{-tx}\,dx は微分可能で，

G'(t)=\int_0^{\infty}(-x)e^{-tx}\,dx が成り立つ．

Proof for Proposition 10.6.3

uses 0

各 x\ge 0 に対して t\mapsto e^{-tx} は C^1 級で， \partial_tF(t,x)=-xe^{-tx} である．さらに t\ge a なら |\partial_tF(t,x)|=xe^{-tx}\le xe^{-ax} である．右辺は \int_0^{\infty}xe^{-ax}\,dx<\infty を満たすので可積分である．したがってTheorem 10.6.2の仮定が成り立ち， G'(t)=\int_0^{\infty}(-x)e^{-tx}\,dx を得る．

Proposition10.6.4

uses 1used by 0✓L∃∀N

Tagsexample

Laplace変換の微分. a\in\RR とし，f\in M([0,\infty);\RR) が (1+t)e^{-at}|f(t)|\in\calL^1([0,\infty)) を満たすとする． s>a に対して

\mathcal Lf(s):=\int_0^\infty e^{-st}f(t)\,d\lambda(t) と定める．このとき \mathcal Lf は (a,\infty) 上で微分可能であり，

(\mathcal Lf)'(s)=-\int_0^\infty te^{-st}f(t)\,d\lambda(t) が成り立つ．

Lean code for Proposition10.6.4●1 theorem

theoremdefined in NoteKsk/«10limits».lean

complete

theorem NoteKsk.Chapter10.hasDerivAt_laplace_transform_of_dominated_loc_of_lip
  {f bound : ℝ → ℝ} {s₀ : ℝ} {U : Set ℝ} (hU : U ∈ nhds s₀)
  (hF_meas :
    ∀ᶠ (s : ℝ) in nhds s₀,
      MeasureTheory.AEStronglyMeasurable
        (fun t ↦ Real.exp (-(s * t)) * f t)
        (MeasureTheory.volume.restrict (Set.Ici 0)))
  (hF_int :
    MeasureTheory.Integrable (fun t ↦ Real.exp (-(s₀ * t)) * f t)
      (MeasureTheory.volume.restrict (Set.Ici 0)))
  (hF'_meas :
    MeasureTheory.AEStronglyMeasurable
      (fun t ↦ -t * Real.exp (-(s₀ * t)) * f t)
      (MeasureTheory.volume.restrict (Set.Ici 0)))
  (h_lip :
    ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ici 0),
      LipschitzOnWith (Real.nnabs (bound t))
        (fun s ↦ Real.exp (-(s * t)) * f t) U)
  (hbound_int :
    MeasureTheory.Integrable bound
      (MeasureTheory.volume.restrict (Set.Ici 0)))
  (h_diff :
    ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ici 0),
      HasDerivAt (fun s ↦ Real.exp (-(s * t)) * f t)
        (-t * Real.exp (-(s₀ * t)) * f t) s₀) :
  MeasureTheory.Integrable (fun t ↦ -t * Real.exp (-(s₀ * t)) * f t)
      (MeasureTheory.volume.restrict (Set.Ici 0)) ∧
    HasDerivAt
      (fun s ↦ ∫ (t : ℝ) in Set.Ici 0, Real.exp (-(s * t)) * f t)
      (∫ (t : ℝ) in Set.Ici 0, -t * Real.exp (-(s₀ * t)) * f t) s₀

theorem NoteKsk.Chapter10.hasDerivAt_laplace_transform_of_dominated_loc_of_lip
  {f bound : ℝ → ℝ} {s₀ : ℝ} {U : Set ℝ}
  (hU : U ∈ nhds s₀)
  (hF_meas :
    ∀ᶠ (s : ℝ) in nhds s₀,
      MeasureTheory.AEStronglyMeasurable
        (fun t ↦
          Real.exp (-(s * t)) * f t)
        (MeasureTheory.volume.restrict
          (Set.Ici 0)))
  (hF_int :
    MeasureTheory.Integrable
      (fun t ↦ Real.exp (-(s₀ * t)) * f t)
      (MeasureTheory.volume.restrict
        (Set.Ici 0)))
  (hF'_meas :
    MeasureTheory.AEStronglyMeasurable
      (fun t ↦
        -t * Real.exp (-(s₀ * t)) * f t)
      (MeasureTheory.volume.restrict
        (Set.Ici 0)))
  (h_lip :
    ∀ᵐ (t :
      ℝ) ∂MeasureTheory.volume.restrict
        (Set.Ici 0),
      LipschitzOnWith
        (Real.nnabs (bound t))
        (fun s ↦
          Real.exp (-(s * t)) * f t)
        U)
  (hbound_int :
    MeasureTheory.Integrable bound
      (MeasureTheory.volume.restrict
        (Set.Ici 0)))
  (h_diff :
    ∀ᵐ (t :
      ℝ) ∂MeasureTheory.volume.restrict
        (Set.Ici 0),
      HasDerivAt
        (fun s ↦
          Real.exp (-(s * t)) * f t)
        (-t * Real.exp (-(s₀ * t)) * f t)
        s₀) :
  MeasureTheory.Integrable
      (fun t ↦
        -t * Real.exp (-(s₀ * t)) * f t)
      (MeasureTheory.volume.restrict
        (Set.Ici 0)) ∧
    HasDerivAt
      (fun s ↦
        ∫ (t : ℝ) in Set.Ici 0,
          Real.exp (-(s * t)) * f t)
      (∫ (t : ℝ) in Set.Ici 0,
        -t * Real.exp (-(s₀ * t)) * f t)
      s₀

Laplace-transform style differentiation formula on `[0, ∞)`, stated as a
direct application of the preceding mathlib parametric-integral theorem.

The analytic hypotheses are packaged in the same form as
`hasDerivAt_integral_under_dominated_loc_of_lip`: local measurability,
integrability at the base point, measurability of the derivative, a local
Lipschitz domination, integrability of the bound, and the pointwise derivative
formula.

Proof for Proposition 10.6.4

uses 0

F(s,t):=e^{-st}f(t) とおく．各 t\ge0 に対して s\mapsto F(s,t) は C^1 級で， \partial_sF(s,t)=-te^{-st}f(t) である．また各 s>a に対して F(s,\cdot) と \partial_sF(s,\cdot) は可測である．また s>a なら e^{-st}\le e^{-at} だから |F(s,t)|\le e^{-at}|f(t)| かつ |\partial_sF(s,t)|\le te^{-at}|f(t)| である．仮定より右辺はいずれも可積分である．したがってTheorem 10.6.2を I=(a,\infty) に適用でき， (\mathcal Lf)'(s)=\int_0^\infty \partial_sF(s,t)\,d\lambda(t) =-\int_0^\infty te^{-st}f(t)\,d\lambda(t) を得る．

Remark (Laplace変換の局所条件). 上の仮定は (a,\infty) 全体で微分可能性を得るための十分条件である．固定した s_0 で微分公式を示すだけなら，より局所的な条件で足りる．例えば，ある b<s_0 が存在して (1+t)e^{-bt}|f(t)|\in\calL^1([0,\infty)) であれば， \mathcal Lf は s_0 で微分可能で， (\mathcal Lf)'(s_0)=-\int_0^\infty te^{-s_0t}f(t)\,d\lambda(t) が成り立つ．実際，\delta>0 を小さく取って b<s_0-\delta とすれば， s\in(s_0-\delta,s_0+\delta) では |e^{-st}f(t)|\le e^{-bt}|f(t)| かつ |te^{-st}f(t)|\le te^{-bt}|f(t)| であり，右辺はいずれも可積分である．したがって前の remark の局所版を適用できる．

Proposition10.6.5

uses 0used by 0XL∃∀N

Tagsexample

導関数のLaplace変換. a\in\RR とし，f:[0,\infty)\to\RR は C^1 級で， e^{-at}|f(t)|\in\calL^1([0,\infty)) かつ e^{-at}|f'(t)|\in\calL^1([0,\infty)) を満たすとする． s>a に対して \mathcal Lf(s):=\int_0^\infty e^{-st}f(t)\,d\lambda(t)， \mathcal L(f')(s):=\int_0^\infty e^{-st}f'(t)\,d\lambda(t) と定める．このとき \mathcal L(f')(s)=s\mathcal Lf(s)-f(0) が成り立つ．

Proof for Proposition 10.6.5

uses 0

s>a を固定する． s>a かつ t\ge0 より e^{-st}\le e^{-at} だから， e^{-st}f と e^{-st}f' は可積分である．

R>0 とする．有限区間 [0,R] 上で部分積分すると， \int_0^R e^{-st}f'(t)\,dt=e^{-sR}f(R)-f(0)+s\int_0^R e^{-st}f(t)\,dt である．あとは R\to\infty とすればよいが，境界項 e^{-sR}f(R) が 0 に収束することを確認する．

h(t):=e^{-st}f(t) とおくと，h は C^1 級で h'(t)=e^{-st}f'(t)-se^{-st}f(t) である．上で見た可積分性より h,h'\in\calL^1([0,\infty)) である．したがって h(R)=h(0)+\int_0^R h'(t)\,dt は R\to\infty で有限の極限をもつ．もしその極限が 0 でなければ，十分大きい t で |h(t)| は正の定数で下から押さえられ，h\in\calL^1([0,\infty)) に反する．よって e^{-sR}f(R)=h(R)\to0 である．

以上より R\to\infty として \int_0^\infty e^{-st}f'(t)\,d\lambda(t) =-f(0)+s\int_0^\infty e^{-st}f(t)\,d\lambda(t) を得る．