Source indexedtheorem · leanprover/lean4:v4.32.0

integral_exp_mul_I_scaled_of_ne

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:188 to 213

Source documentation

Scaled finite-height exponential integral, away from zero frequency.

Exact Lean statement

theorem integral_exp_mul_I_scaled_of_ne {a T : ℝ} (ha : a ≠ 0) :
    ∫ t in (-T)..T, Complex.exp (((t * a : ℝ) : ℂ) * I) =
      (2 * Real.sin (T * a) : ℂ) / (a : ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem integral_exp_mul_I_scaled_of_ne {a T : ℝ} (ha : a ≠ 0) :    ∫ t in (-T)..T, Complex.exp (((t * a : ℝ) : ℂ) * I) =      (2 * Real.sin (T * a) : ℂ) / (a : ℂ) := by  have hc : ((a : ℂ) * I) ≠ 0 := by    exact mul_ne_zero (Complex.ofReal_ne_zero.mpr ha) Complex.I_ne_zero  calc    ∫ t in (-T)..T, Complex.exp (((t * a : ℝ) : ℂ) * I)        = ∫ t in (-T)..T, Complex.exp (((a : ℂ) * I) * t) := by          apply intervalIntegral.integral_congr          intro t _ht          push_cast          ring_nf    _ = (2 * Real.sin (T * a) : ℂ) / (a : ℂ) := by          rw [integral_exp_mul_complex (c := ((a : ℂ) * I)) hc]          have harg : ((a : ℂ) * I) * (T : ℂ) = ((T * a : ℝ) : ℂ) * I := by            push_cast            ring_nf          have hneg :              ((a : ℂ) * I) * ((-T : ℝ) : ℂ) = (((-(T * a) : ℝ) : ℂ) * I) := by            push_cast            ring_nf          rw [harg, hneg]          simp only [Complex.exp_mul_I, Complex.cos_neg, Complex.sin_neg, ofReal_neg,            Complex.ofReal_sin]          field_simp [Complex.ofReal_ne_zero.mpr ha, Complex.I_ne_zero]          ring_nf