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:

𝕜 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} [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

vector_fourier.fourier_integral e μ L f w = ∫ (v : V), ↑(⇑e (⇑multiplicative.of_add (-⇑(⇑L v) w))) • f v ∂μ

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 : ℂ) :

vector_fourier.fourier_integral e μ L (r • f) = r • vector_fourier.fourier_integral e μ L f

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) :

‖vector_fourier.fourier_integral e μ L f 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} [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) :

measure_theory.integrable f μ ↔ measure_theory.integrable (λ (v : V), ↑(⇑e (⇑multiplicative.of_add (-⇑(⇑L v) w))) • f v) μ

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} [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 →ₗ[𝕜] 𝕜} [complete_space E] (he : continuous ⇑e) (hL : continuous (λ (p : V × W), ⇑(⇑L p.fst) p.snd)) {f g : V → E} (hf : measure_theory.integrable f μ) (hg : measure_theory.integrable g μ) :

vector_fourier.fourier_integral e μ L f + vector_fourier.fourier_integral e μ L g = vector_fourier.fourier_integral e μ L (f + g)

theorem vector_fourier.fourier_integral_continuous {𝕜 : 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 →ₗ[𝕜] 𝕜} [complete_space E] [topological_space.first_countable_topology W] (he : continuous ⇑e) (hL : continuous (λ (p : V × W), ⇑(⇑L p.fst) p.snd)) {f : V → E} (hf : measure_theory.integrable f μ) :

continuous (vector_fourier.fourier_integral e μ L f)

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

fourier.fourier_integral e μ f w = vector_fourier.fourier_integral e μ (linear_map.mul 𝕜 𝕜) f w

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.fourier_integral_smul_const {𝕜 : 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) (r : ℂ) :

fourier.fourier_integral e μ (r • f) = r • fourier.fourier_integral e μ f

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 : 𝕜) :

‖fourier.fourier_integral e μ f 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 𝕜] [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.

noncomputable def real.fourier_char :

multiplicative ℝ →* ↥circle

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

Equations

real.fourier_char = {to_fun := λ (z : multiplicative ℝ), ⇑exp_map_circle (2 * real.pi * ⇑multiplicative.to_add z), map_one' := real.fourier_char._proof_1, map_mul' := real.fourier_char._proof_2}

theorem real.fourier_char_apply (x : ℝ) :

↑(⇑real.fourier_char (⇑multiplicative.of_add x)) = cexp (↑(2 * real.pi * x) * complex.I)

@[continuity]

theorem real.continuous_fourier_char :

continuous ⇑real.fourier_char

theorem real.vector_fourier_integral_eq_integral_exp_smul {E : Type u_1} [normed_add_comm_group E] [complete_space E] [normed_space ℂ E] {V : Type u_2} [add_comm_group V] [module ℝ V] [measurable_space V] {W : Type u_3} [add_comm_group W] [module ℝ W] (L : V →ₗ[ℝ ] W →ₗ[ℝ ] ℝ) (μ : measure_theory.measure V) (f : V → E) (w : W) :

vector_fourier.fourier_integral real.fourier_char μ L f w = ∫ (v : V), cexp (↑((-2) * real.pi * ⇑(⇑L v) w) * complex.I) • f v ∂μ

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

real.fourier_integral f w = fourier.fourier_integral real.fourier_char measure_theory.measure_space.volume f w

theorem real.fourier_integral_def {E : Type u_1} [normed_add_comm_group E] [complete_space E] [normed_space ℂ E] (f : ℝ → E) (w : ℝ) :

real.fourier_integral f w = ∫ (v : ℝ), ↑(⇑real.fourier_char (⇑multiplicative.of_add (-(v * w)))) • f v

theorem real.fourier_integral_eq_integral_exp_smul {E : Type u_1} [normed_add_comm_group E] [complete_space E] [normed_space ℂ E] (f : ℝ → E) (w : ℝ) :

real.fourier_integral f w = ∫ (v : ℝ), cexp (↑((-2) * real.pi * v * w) * complex.I) • f v