@[reducible, inline]

abbrev FourierAnalysis.SchwartzSpace : Type

theorem FourierAnalysis.fourier_schwartz_equiv : ∃ (Φ : SchwartzSpace ≃L[ℂ] SchwartzSpace), ∀ (f : SchwartzSpace), ⇑(Φ f) = FourierTransform.fourier ⇑f

theorem FourierAnalysis.real_inner_eq_mul (x y : ℝ) : inner ℝ x y = x * y

theorem FourierAnalysis.fourier_transform_scaling (f : ℝ → ℂ) (a : ℝ) (ha : 0 < a) (y : ℝ) : FourierTransform.fourier (fun (x : ℝ) => f (a * x)) y = (↑a)⁻¹ • FourierTransform.fourier f (y / a)

theorem FourierAnalysis.fderiv_fourier_eq_fourier_neg_smul (f : SchwartzSpace) : (SchwartzMap.fderivCLM ℂ ℝ ℂ) (FourierTransform.fourier f) = FourierTransform.fourier (-(2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulRightCLM ℂ ℂ (innerSL ℝ)) f)

theorem FourierAnalysis.fourier_fderiv_eq_smul_fourier (f : SchwartzSpace) : FourierTransform.fourier ((SchwartzMap.fderivCLM ℂ ℝ ℂ) f) = (2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulRightCLM ℂ ℂ (innerSL ℝ)) (FourierTransform.fourier f)

theorem FourierAnalysis.fourier_fderiv_interchange (f : SchwartzSpace) : (SchwartzMap.fderivCLM ℂ ℝ ℂ) (FourierTransform.fourier f) = FourierTransform.fourier (-(2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulRightCLM ℂ ℂ (innerSL ℝ)) f) ∧ FourierTransform.fourier ((SchwartzMap.fderivCLM ℂ ℝ ℂ) f) = (2 * ↑Real.pi * Complex.I) • (SchwartzMap.smulRightCLM ℂ ℂ (innerSL ℝ)) (FourierTransform.fourier f)

theorem FourierAnalysis.poisson_summation (f : SchwartzSpace) : ∑' (n : ℤ), f ↑n = ∑' (n : ℤ), FourierTransform.fourier ⇑f ↑n

@[reducible, inline]

noncomputable abbrev FourierAnalysis.mellinTransform (f : ℝ → ℂ) (s : ℂ) : ℂ

@[reducible, inline]

noncomputable abbrev FourierAnalysis.gammaFunction (s : ℂ) : ℂ

theorem FourierAnalysis.euler_reflection_formula (s : ℂ) : Complex.Gamma s * Complex.Gamma (1 - s) = ↑Real.pi / Complex.sin (↑Real.pi * s)