# mathlib3documentation

analysis.fourier.fourier_transform

# The Fourier transform #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We set up the Fourier transform for complex-valued functions on finite-dimensional spaces.

## Design choices #

In namespace vector_fourier, we define the Fourier integral in the following context:

• 𝕜 is a commutative ring.
• V and W are 𝕜-modules.
• e is a unitary additive character of 𝕜, i.e. a homomorphism (multiplicative 𝕜) →* circle.
• μ is a measure on V.
• L is a 𝕜-bilinear form V × W → 𝕜.
• E is a complete normed ℂ-vector space.

With these definitions, we define fourier_integral to be the map from functions V → E to functions W → E that sends f to

λ w, ∫ v in V, e [-L v w] • f v ∂μ,

where e [x] is notational sugar for (e (multiplicative.of_add x) : ℂ) (available in locale fourier_transform). This includes the cases W is the dual of V and L is the canonical pairing, or W = V and L is a bilinear form (e.g. an inner product).

In namespace fourier, we consider the more familiar special case when V = W = 𝕜 and L is the multiplication map (but still allowing 𝕜 to be an arbitrary ring equipped with a measure).

The most familiar case of all is when V = W = 𝕜 = ℝ, L is multiplication, μ is volume, and e is real.fourier_char, i.e. the character λ x, exp ((2 * π * x) * I). The Fourier integral in this case is defined as real.fourier_integral.

## Main results #

At present the only nontrivial lemma we prove is continuous_fourier_integral, stating that the Fourier transform of an integrable function is continuous (under mild assumptions).

## Fourier theory for functions on general vector spaces #

noncomputable def vector_fourier.fourier_integral {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [ V] {W : Type u_3} [ W] {E : Type u_4} [ E] (e : →* circle) (μ : measure_theory.measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V E) (w : W) :
E

The Fourier transform integral for f : V → E, with respect to a bilinear form L : V × W → 𝕜 and an additive character e.

Equations
theorem vector_fourier.fourier_integral_smul_const {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [ V] {W : Type u_3} [ W] {E : Type u_4} [ E] (e : →* circle) (μ : measure_theory.measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V E) (r : ) :
(r f) = r
theorem vector_fourier.norm_fourier_integral_le_integral_norm {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [ V] {W : Type u_3} [ W] {E : Type u_4} [ E] (e : →* circle) (μ : measure_theory.measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V E) (w : W) :
w (v : V), f v μ

The uniform norm of the Fourier integral of f is bounded by the L¹ norm of f.

theorem vector_fourier.fourier_integral_comp_add_right {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [ V] {W : Type u_3} [ W] {E : Type u_4} [ E] (e : →* circle) (μ : measure_theory.measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V E) (v₀ : V) :
(f λ (v : V), v + v₀) = λ (w : W), (e (multiplicative.of_add ((L v₀) w))) w

The Fourier integral converts right-translation into scalar multiplication by a phase factor.

theorem vector_fourier.fourier_integral_convergent_iff {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [ V] {W : Type u_3} [ W] {E : Type u_4} [ E] [borel_space V] {e : →* circle} {μ : measure_theory.measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : continuous e) (hL : continuous (λ (p : V × W), (L p.fst) p.snd)) {f : V E} (w : W) :

For any w, the Fourier integral is convergent iff f is integrable.

theorem vector_fourier.fourier_integral_add {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [ V] {W : Type u_3} [ W] {E : Type u_4} [ E] [borel_space V] {e : →* circle} {μ : measure_theory.measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : continuous e) (hL : continuous (λ (p : V × W), (L p.fst) p.snd)) {f g : V E} (hf : μ) (hg : μ) :
+ = (f + g)
theorem vector_fourier.fourier_integral_continuous {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [ V] {W : Type u_3} [ W] {E : Type u_4} [ E] [borel_space V] {e : →* circle} {μ : measure_theory.measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} (he : continuous e) (hL : continuous (λ (p : V × W), (L p.fst) p.snd)) {f : V E} (hf : μ) :

The Fourier integral of an L^1 function is a continuous function.

## Fourier theory for functions on 𝕜#

noncomputable def fourier.fourier_integral {𝕜 : Type u_1} [comm_ring 𝕜] {E : Type u_2} [ E] (e : →* circle) (μ : measure_theory.measure 𝕜) (f : 𝕜 E) (w : 𝕜) :
E

The Fourier transform integral for f : 𝕜 → E, with respect to the measure μ and additive character e.

Equations
• w = f w
theorem fourier.fourier_integral_def {𝕜 : Type u_1} [comm_ring 𝕜] {E : Type u_2} [ E] (e : →* circle) (μ : measure_theory.measure 𝕜) (f : 𝕜 E) (w : 𝕜) :
w = (v : 𝕜), (e (multiplicative.of_add (-(v * w)))) f v μ
theorem fourier.fourier_integral_smul_const {𝕜 : Type u_1} [comm_ring 𝕜] {E : Type u_2} [ E] (e : →* circle) (μ : measure_theory.measure 𝕜) (f : 𝕜 E) (r : ) :
(r f) = r
theorem fourier.norm_fourier_integral_le_integral_norm {𝕜 : Type u_1} [comm_ring 𝕜] {E : Type u_2} [ E] (e : →* circle) (μ : measure_theory.measure 𝕜) (f : 𝕜 E) (w : 𝕜) :
w (x : 𝕜), f x μ

The uniform norm of the Fourier transform of f is bounded by the L¹ norm of f.

theorem fourier.fourier_integral_comp_add_right {𝕜 : Type u_1} [comm_ring 𝕜] {E : Type u_2} [ E] (e : →* circle) (μ : measure_theory.measure 𝕜) (f : 𝕜 E) (v₀ : 𝕜) :
(f λ (v : 𝕜), v + v₀) = λ (w : 𝕜), (e (multiplicative.of_add (v₀ * w))) w

The Fourier transform converts right-translation into scalar multiplication by a phase factor.

noncomputable def real.fourier_char  :

The standard additive character of ℝ, given by λ x, exp (2 * π * x * I).

Equations
@[continuity]
theorem real.vector_fourier_integral_eq_integral_exp_smul {E : Type u_1} [ E] {V : Type u_2} [ V] {W : Type u_3} [ W] (L : V →ₗ[] ) (μ : measure_theory.measure V) (f : V E) (w : W) :
= (v : V), cexp (((-2) * real.pi * (L v) w) * complex.I) f v μ
noncomputable def real.fourier_integral {E : Type u_1} [ E] (f : E) (w : ) :
E

The Fourier integral for f : ℝ → E, with respect to the standard additive character and measure on ℝ.

Equations
theorem real.fourier_integral_def {E : Type u_1} [ E] (f : E) (w : ) :
theorem real.fourier_integral_eq_integral_exp_smul {E : Type u_1} [ E] (f : E) (w : ) :
= (v : ), cexp (((-2) * real.pi * v * w) * complex.I) f v