mathlib3 documentation

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:

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} [add_comm_group V] [module 𝕜 V] [measurable_space V] {W : Type u_3} [add_comm_group W] [module 𝕜 W] {E : Type u_4} [normed_add_comm_group E] [normed_space E] [complete_space E] (e : multiplicative 𝕜 →* 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} [add_comm_group V] [module 𝕜 V] [measurable_space V] {W : Type u_3} [add_comm_group W] [module 𝕜 W] {E : Type u_4} [normed_add_comm_group E] [normed_space E] [complete_space E] (e : multiplicative 𝕜 →* circle) (μ : measure_theory.measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V E) (r : ) :
theorem vector_fourier.norm_fourier_integral_le_integral_norm {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [add_comm_group V] [module 𝕜 V] [measurable_space V] {W : Type u_3} [add_comm_group W] [module 𝕜 W] {E : Type u_4} [normed_add_comm_group E] [normed_space E] [complete_space E] (e : multiplicative 𝕜 →* circle) (μ : measure_theory.measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V E) (w : W) :

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

theorem vector_fourier.fourier_integral_comp_add_right {𝕜 : Type u_1} [comm_ring 𝕜] {V : Type u_2} [add_comm_group V] [module 𝕜 V] [measurable_space V] {W : Type u_3} [add_comm_group W] [module 𝕜 W] {E : Type u_4} [normed_add_comm_group E] [normed_space E] [complete_space E] [has_measurable_add V] (e : multiplicative 𝕜 →* circle) (μ : measure_theory.measure V) [μ.is_add_right_invariant] (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V E) (v₀ : V) :
vector_fourier.fourier_integral e μ L (f λ (v : V), v + v₀) = λ (w : W), (e (multiplicative.of_add ((L v₀) w))) vector_fourier.fourier_integral e μ L f 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} [add_comm_group V] [module 𝕜 V] [measurable_space V] {W : Type u_3} [add_comm_group W] [module 𝕜 W] {E : Type u_4} [normed_add_comm_group E] [normed_space E] [topological_space 𝕜] [topological_ring 𝕜] [topological_space V] [borel_space V] [topological_space W] {e : multiplicative 𝕜 →* 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.

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 𝕜] [measurable_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] (e : multiplicative 𝕜 →* 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
theorem fourier.fourier_integral_def {𝕜 : Type u_1} [comm_ring 𝕜] [measurable_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] (e : multiplicative 𝕜 →* circle) (μ : measure_theory.measure 𝕜) (f : 𝕜 E) (w : 𝕜) :
fourier.fourier_integral e μ f w = (v : 𝕜), (e (multiplicative.of_add (-(v * w)))) f v μ
theorem fourier.norm_fourier_integral_le_integral_norm {𝕜 : Type u_1} [comm_ring 𝕜] [measurable_space 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] (e : multiplicative 𝕜 →* circle) (μ : measure_theory.measure 𝕜) (f : 𝕜 E) (w : 𝕜) :

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

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

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

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

Equations
noncomputable def real.fourier_integral {E : Type u_1} [normed_add_comm_group E] [complete_space E] [normed_space E] (f : E) (w : ) :
E

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

Equations