mathlib documentation

analysis.fourier.fourier_transform

The Fourier transform #

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.fourier_integral_norm_le {π•œ : 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} (hf : measure_theory.integrable f ΞΌ) (w : W) :

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 {π•œ : 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} (hf : measure_theory.integrable f ΞΌ) (w : W) :

If f is integrable, then the Fourier integral is convergent for all w.

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

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 : π•œ) :
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 : β„‚) :

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.

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