`BookProof.ChapterH3.duhamel_scalar` (z : ℂ) (δ : ℝ) : (∫ s in (0:ℝ)..δ, Complex.exp ((↑(δ - s)) * z)) = δ * BookProof.ChapterH1.phi 1 (δ * z)

Proved

BookProof.ChapterH3.duhamel_scalar

by leonardopedro · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterH3.

BookProof.ChapterH3.duhamel_scalar (z : ℂ) (δ : ℝ) : (∫ s in (0:ℝ)..δ, Complex.exp ((↑(δ - s)) * z)) = δ * BookProof.ChapterH1.phi 1 (δ * z)

Formalization note: Lean 4 identifier BookProof.ChapterH3.duhamel_scalar.

Preamble

-- Generated from ChapterH3.lean — theorem BookProof.ChapterH3.duhamel_scalar
import Mathlib
import Definitions.Def_ChapterH3
import Definitions.Def_ChapterH1
open BookProof.ChapterH1
open BookProof.ChapterH3


open scoped BigOperators
open intervalIntegral


noncomputable section

Formal statement

theorem BookProof.ChapterH3.duhamel_scalar (z : ℂ) (δ : ℝ) :
    (∫ s in (0:ℝ)..δ, Complex.exp ((↑(δ - s)) * z))
      = δ * BookProof.ChapterH1.phi 1 (δ * z) := by sorry

View graph