11.2. HardyZeta.ExponentialFourier🔗

theorem fourier_exp_neg_abs {a : ℝ} (ha : 0 < a) (w : ℝ) :
    𝓕 (fun u : ℝ ↦ (Real.exp (-a * |u|) : ℂ)) w =
      1 / ((a : ℂ) - 2 * Real.pi * w * I) +
      1 / ((a : ℂ) + 2 * Real.pi * w * I) := bya:ℝha:0 < aw:ℝ⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  let f : ℝ → ℂ := fun u ↦ exp ((-2 * Real.pi * (w * u) : ℝ) * I) *
    (Real.exp (-a * |u|) : ℂ)a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  have he (u : ℝ) : f u = exp ((-2 * Real.pi * (w * u) : ℝ) * I + (-a * |u|)) := by
    simp [f, ofReal_exp, exp_add]a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  have hl (u : ℝ) (hu : u ∈ Iic 0) : f u = exp (((a : ℂ) - 2 * Real.pi * w * I) * u) := by
    rw [he,a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)u:ℝhu:u ∈ Iic 0⊢ cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|) = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u) abs_of_nonpos hua:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)u:ℝhu:u ∈ Iic 0⊢ cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑(-u)) = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)]a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)u:ℝhu:u ∈ Iic 0⊢ cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑(-u)) = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)
    push_casta:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)u:ℝhu:u ∈ Iic 0⊢ cexp (-2 * ↑Real.pi * (↑w * ↑u) * I + -↑a * -↑u) = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)
    congr 1a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)u:ℝhu:u ∈ Iic 0⊢ -2 * ↑Real.pi * (↑w * ↑u) * I + -↑a * -↑u = (↑a - 2 * ↑Real.pi * ↑w * I) * ↑u
    ringa:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  have hr (u : ℝ) (hu : u ∈ Ioi 0) : f u = exp (((-a : ℂ) - 2 * Real.pi * w * I) * u) := by
    rw [he,a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)u:ℝhu:u ∈ Ioi 0⊢ cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|) = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u) abs_of_pos hua:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)u:ℝhu:u ∈ Ioi 0⊢ cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑u) = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)]a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)u:ℝhu:u ∈ Ioi 0⊢ cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑u) = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)
    push_casta:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)u:ℝhu:u ∈ Ioi 0⊢ cexp (-2 * ↑Real.pi * (↑w * ↑u) * I + -↑a * ↑u) = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)
    congr 1a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)u:ℝhu:u ∈ Ioi 0⊢ -2 * ↑Real.pi * (↑w * ↑u) * I + -↑a * ↑u = (-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u
    ringa:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  have hal : 0 < ((a : ℂ) - 2 * Real.pi * w * I).re := by simpa using haa:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).re⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  have har : ((-a : ℂ) - 2 * Real.pi * w * I).re < 0 := by simpa using neg_neg_of_pos haa:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  have hil : IntegrableOn f (Iic 0) :=
    (integrableOn_exp_mul_complex_Iic hal 0).congr_fun (fun u hu ↦ (hl u hu).symm)
      measurableSet_Iica:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volume⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  have hir : IntegrableOn f (Ioi 0) :=
    (integrableOn_exp_mul_complex_Ioi har 0).congr_fun (fun u hu ↦ (hr u hu).symm)
      measurableSet_Ioia:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  rw [Real.fourier_eq'a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ ∫ (v : ℝ), cexp (↑(-2 * Real.pi * inner ℝ v w) * I) • ↑(Real.exp (-a * |v|)) =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)]a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ ∫ (v : ℝ), cexp (↑(-2 * Real.pi * inner ℝ v w) * I) • ↑(Real.exp (-a * |v|)) =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  simp only [RCLike.inner_apply, conj_trivial, smul_eq_mul]a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ ∫ (v : ℝ), cexp (↑(-2 * Real.pi * (w * v)) * I) * ↑(Real.exp (-a * |v|)) =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  change (∫ u, f u) = _a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ ∫ (u : ℝ), f u = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  rw [← intervalIntegral.integral_Iic_add_Ioi hil hir,a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ ∫ (x : ℝ) in Iic 0, f x ∂volume + ∫ (x : ℝ) in Ioi 0, f x ∂volume =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
    setIntegral_congr_fun measurableSet_Iic hl,a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ ∫ (x : ℝ) in Iic 0, cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑x) ∂volume + ∫ (x : ℝ) in Ioi 0, f x ∂volume =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I) setIntegral_congr_fun measurableSet_Ioi hr,a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ ∫ (x : ℝ) in Iic 0, cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑x) ∂volume +
    ∫ (x : ℝ) in Ioi 0, cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑x) ∂volume =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
    integral_exp_mul_complex_Iic hal,a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑0) / (↑a - 2 * ↑Real.pi * ↑w * I) +
    ∫ (x : ℝ) in Ioi 0, cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑x) ∂volume =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I) integral_exp_mul_complex_Ioi hara:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑0) / (↑a - 2 * ↑Real.pi * ↑w * I) +
    -cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑0) / (-↑a - 2 * ↑Real.pi * ↑w * I) =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)]a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑0) / (↑a - 2 * ↑Real.pi * ↑w * I) +
    -cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑0) / (-↑a - 2 * ↑Real.pi * ↑w * I) =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  simp only [ofReal_zero, mul_zero, exp_zero]a:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + -1 / (-↑a - 2 * ↑Real.pi * ↑w * I) =
  1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  congr 1e_aa:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ -1 / (-↑a - 2 * ↑Real.pi * ↑w * I) = 1 / (↑a + 2 * ↑Real.pi * ↑w * I)
  rw [show (-a : ℂ) - 2 * Real.pi * w * I = -((a : ℂ) + 2 * Real.pi * w * I) bya:ℝha:0 < aw:ℝ⊢ 𝓕 (fun u => ↑(Real.exp (-a * |u|))) w = 1 / (↑a - 2 * ↑Real.pi * ↑w * I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * I) ringAll goals completed! 🐙,
    neg_div_neg_eqe_aa:ℝha:0 < aw:ℝf:ℝ → ℂ := fun u => cexp (↑(-2 * Real.pi * (w * u)) * I) * ↑(Real.exp (-a * |u|))he:∀ (u : ℝ), f u = cexp (↑(-2 * Real.pi * (w * u)) * I + -↑a * ↑|u|)hl:∀ u ∈ Iic 0, f u = cexp ((↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hr:∀ u ∈ Ioi 0, f u = cexp ((-↑a - 2 * ↑Real.pi * ↑w * I) * ↑u)hal:0 < (↑a - 2 * ↑Real.pi * ↑w * I).rehar:(-↑a - 2 * ↑Real.pi * ↑w * I).re < 0hil:IntegrableOn f (Iic 0) volumehir:IntegrableOn f (Ioi 0) volume⊢ 1 / (↑a + 2 * ↑Real.pi * ↑w * I) = 1 / (↑a + 2 * ↑Real.pi * ↑w * I)]All goals completed! 🐙

theorem integrable_exp_neg_abs {a : ℝ} (ha : 0 < a) :
    Integrable (fun u : ℝ ↦ (Real.exp (-a * |u|) : ℂ)) := bya:ℝha:0 < a⊢ Integrable (fun u => ↑(Real.exp (-a * |u|))) volume
  have hl : IntegrableOn (fun u : ℝ ↦ (Real.exp (-a * |u|) : ℂ)) (Iic 0) := by
    apply (integrableOn_exp_mul_complex_Iic (a := (a : ℂ)) (bya:ℝha:0 < a⊢ 0 < (↑a).re simpa using haAll goals completed! 🐙) 0).congr_fun
      (s := Iic 0) _ measurableSet_Iic
    intro u hua:ℝha:0 < au:ℝhu:u ∈ Iic 0⊢ (fun x => cexp (↑a * ↑x)) u = (fun u => ↑(Real.exp (-a * |u|))) u
    simp [abs_of_nonpos (show u ≤ 0 from hu), ofReal_exp]a:ℝha:0 < ahl:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Iic 0) volume⊢ Integrable (fun u => ↑(Real.exp (-a * |u|))) volume
  have hr : IntegrableOn (fun u : ℝ ↦ (Real.exp (-a * |u|) : ℂ)) (Ioi 0) := by
    have h := integrableOn_exp_mul_complex_Ioi (a := (-a : ℂ))
      (bya:ℝha:0 < ahl:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Iic 0) volume⊢ (-↑a).re < 0 simpa using neg_neg_of_pos haAll goals completed! 🐙) 0a:ℝha:0 < ahl:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Iic 0) volumeh:IntegrableOn (fun x => cexp (-↑a * ↑x)) (Ioi 0) volume⊢ IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Ioi 0) volume
    apply h.congr_fun (s := Ioi 0) _ measurableSet_Ioia:ℝha:0 < ahl:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Iic 0) volumeh:IntegrableOn (fun x => cexp (-↑a * ↑x)) (Ioi 0) volume⊢ EqOn (fun x => cexp (-↑a * ↑x)) (fun u => ↑(Real.exp (-a * |u|))) (Ioi 0)
    intro u hua:ℝha:0 < ahl:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Iic 0) volumeh:IntegrableOn (fun x => cexp (-↑a * ↑x)) (Ioi 0) volumeu:ℝhu:u ∈ Ioi 0⊢ (fun x => cexp (-↑a * ↑x)) u = (fun u => ↑(Real.exp (-a * |u|))) u
    simp [abs_of_pos (show 0 < u from hu), ofReal_exp]a:ℝha:0 < ahl:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Iic 0) volumehr:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Ioi 0) volume⊢ Integrable (fun u => ↑(Real.exp (-a * |u|))) volume
  have h := hl.union hra:ℝha:0 < ahl:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Iic 0) volumehr:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Ioi 0) volumeh:IntegrableOn (fun u => ↑(Real.exp (-a * |u|))) (Iic 0 ∪ Ioi 0) volume⊢ Integrable (fun u => ↑(Real.exp (-a * |u|))) volume
  simpa only [Iic_union_Ioi, integrableOn_univ] using hAll goals completed! 🐙