Theorem: F_mul (PrimeNumberTheoremAnd/Fourier.lean)

State before:
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ 𝓕 (fun x => c * f x) u = c * 𝓕 f u
Tactic:
simp [fourierIntegral_real_eq, ← integral_mul_left]
State after:
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ ∫ (v : ℝ), 𝐞 (-(v * u)) • (c * f v) = ∫ (a : ℝ), c * 𝐞 (-(a * u)) • f a

State before:
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ ∫ (v : ℝ), 𝐞 (-(v * u)) • (c * f v) = ∫ (a : ℝ), c * 𝐞 (-(a * u)) • f a
Tactic:
congr
State after:
case e_f
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ (fun v => 𝐞 (-(v * u)) • (c * f v)) = fun a => c * 𝐞 (-(a * u)) • f a

State before:
case e_f
f : ℝ → ℂ
c : ℂ
u : ℝ
⊢ (fun v => 𝐞 (-(v * u)) • (c * f v)) = fun a => c * 𝐞 (-(a * u)) • f a
Tactic:
ext
State after:
case e_f.h
f : ℝ → ℂ
c : ℂ
u x✝ : ℝ
⊢ 𝐞 (-(x✝ * u)) • (c * f x✝) = c * 𝐞 (-(x✝ * u)) • f x✝

State before:
case e_f.h
f : ℝ → ℂ
c : ℂ
u x✝ : ℝ
⊢ 𝐞 (-(x✝ * u)) • (c * f x✝) = c * 𝐞 (-(x✝ * u)) • f x✝
Tactic:
simp [Real.fourierChar, expMapCircle]
State after:
case e_f.h
f : ℝ → ℂ
c : ℂ
u x✝ : ℝ
⊢ cexp (-(2 * ↑π * (↑x✝ * ↑u) * I)) * (c * f x✝) = c * (cexp (-(2 * ↑π * (↑x✝ * ↑u) * I)) * f x✝)

State before:
case e_f.h
f : ℝ → ℂ
c : ℂ
u x✝ : ℝ
⊢ cexp (-(2 * ↑π * (↑x✝ * ↑u) * I)) * (c * f x✝) = c * (cexp (-(2 * ↑π * (↑x✝ * ↑u) * I)) * f x✝)
Tactic:
ring
State after:
no goals