simp [Real.fourierChar, expMapCircle, Multiplicative.ofAdd]
case left.hf.hu_cont.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => 𝐞 (Multiplicative.ofAdd (-(i * (x / (2 * π)))))
case left.hf.hu_cont.hg.hf.hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcont : Continuous ψ
hsupp : Integrable ψ volume
hσ : 1 < σ'
ν : Measure (ℝ × ℝ) := (volume.restrict (Ici (-x.log))).prod volume
i : ℝ
⊢ Continuous fun x => ⟨cexp (-(2 * ↑π * (↑i * (↑x / (2 * ↑π))) * I)), ⋯⟩