`BookProof.ChapterShannonSampling.integral_exp_mul_ofReal` (T a : ℝ) (hT : 0 < T) : (∫ ξ in (-(T / 2))..(T / 2), Complex.exp (2 * π * I * a * ξ)) = (T : ℂ) * (sinc (a * T) : ℝ)

Proved

BookProof.ChapterShannonSampling.integral_exp_mul_ofReal

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterShannonSampling.

BookProof.ChapterShannonSampling.integral_exp_mul_ofReal (T a : ℝ) (hT : 0 < T) : (∫ ξ in (-(T / 2))..(T / 2), Complex.exp (2 * π * I * a * ξ)) = (T : ℂ) * (sinc (a * T) : ℝ)

Formalization note: Lean 4 identifier BookProof.ChapterShannonSampling.integral_exp_mul_ofReal.

Preamble

-- Generated from ChapterShannonSampling.lean — theorem BookProof.ChapterShannonSampling.integral_exp_mul_ofReal
import Mathlib
import Definitions.Def_ChapterShannonSampling
open BookProof.ChapterShannonSampling



open MeasureTheory Complex AddCircle intervalIntegral Set
open scoped Real ComplexConjugate

Formal statement

theorem BookProof.ChapterShannonSampling.integral_exp_mul_ofReal (T a : ℝ) (hT : 0 < T) :
    (∫ ξ in (-(T / 2))..(T / 2), Complex.exp (2 * π * I * a * ξ))
      = (T : ℂ) * (sinc (a * T) : ℝ) := by sorry

View graph