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

Proved

BookProof.ChapterH3.duhamel_scalar_smul

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterH3.

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

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

Preamble

-- Generated from ChapterH3.lean — theorem BookProof.ChapterH3.duhamel_scalar_smul
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_smul (z g : ℂ) (δ : ℝ) :
    (∫ s in (0:ℝ)..δ, Complex.exp ((↑(δ - s)) * z) * g)
      = δ * BookProof.ChapterH1.phi 1 (δ * z) * g := by sorry

View graph