Skip to content

Commit e059984

Browse files
committed
feat: the Fourier transform is self-adjoint (#10833)
Also extend the notation `𝓕` for the Fourier transform to inner product spaces, introduce a notation `𝓕⁻` for the inverse Fourier transform, and generalize a few results from the real line to inner product spaces.
1 parent ae9f685 commit e059984

File tree

5 files changed

+174
-41
lines changed

5 files changed

+174
-41
lines changed

β€ŽMathlib/Analysis/Fourier/FourierTransform.lean

Lines changed: 136 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,10 @@ Authors: David Loeffler
55
-/
66
import Mathlib.Analysis.Complex.Circle
77
import Mathlib.MeasureTheory.Group.Integral
8+
import Mathlib.MeasureTheory.Integral.SetIntegral
89
import Mathlib.MeasureTheory.Measure.Haar.OfBasis
10+
import Mathlib.MeasureTheory.Constructions.Prod.Integral
11+
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
912

1013
#align_import analysis.fourier.fourier_transform from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"
1114

@@ -33,12 +36,17 @@ where `e [x]` is notational sugar for `(e (Multiplicative.ofAdd x) : β„‚)` (avai
3336
`fourier_transform`). This includes the cases `W` is the dual of `V` and `L` is the canonical
3437
pairing, or `W = V` and `L` is a bilinear form (e.g. an inner product).
3538
36-
In namespace `fourier`, we consider the more familiar special case when `V = W = π•œ` and `L` is the
39+
In namespace `Fourier`, we consider the more familiar special case when `V = W = π•œ` and `L` is the
3740
multiplication map (but still allowing `π•œ` to be an arbitrary ring equipped with a measure).
3841
3942
The most familiar case of all is when `V = W = π•œ = ℝ`, `L` is multiplication, `ΞΌ` is volume, and
40-
`e` is `Real.fourierChar`, i.e. the character `fun x ↦ exp ((2 * Ο€ * x) * I)`. The Fourier integral
41-
in this case is defined as `Real.fourierIntegral`.
43+
`e` is `Real.fourierChar`, i.e. the character `fun x ↦ exp ((2 * Ο€ * x) * I)` (for which we
44+
introduce the notation `𝐞` in the locale `FourierTransform`).
45+
46+
Another familiar case (which generalizes the previous one) is when `V = W` is an inner product space
47+
over `ℝ` and `L` is the scalar product. We introduce two notations `𝓕` for the Fourier transform in
48+
this case and `𝓕⁻ f (v) = 𝓕 f (-v)` for the inverse Fourier transform. These notations make
49+
in particular sense for `V = W = ℝ`.
4250
4351
## Main results
4452
@@ -56,6 +64,7 @@ open MeasureTheory Filter
5664
open scoped Topology
5765

5866
-- To avoid messing around with multiplicative vs. additive characters, we make a notation.
67+
/-- Notation for multiplicative character applied in an additive setting. -/
5968
scoped[FourierTransform] notation e "[" x "]" => (e (Multiplicative.ofAdd x) : β„‚)
6069

6170
open FourierTransform
@@ -66,7 +75,9 @@ open FourierTransform
6675
namespace VectorFourier
6776

6877
variable {π•œ : Type*} [CommRing π•œ] {V : Type*} [AddCommGroup V] [Module π•œ V] [MeasurableSpace V]
69-
{W : Type*} [AddCommGroup W] [Module π•œ W] {E : Type*} [NormedAddCommGroup E] [NormedSpace β„‚ E]
78+
{W : Type*} [AddCommGroup W] [Module π•œ W]
79+
{E F G : Type*} [NormedAddCommGroup E] [NormedSpace β„‚ E] [NormedAddCommGroup F] [NormedSpace β„‚ F]
80+
[NormedAddCommGroup G] [NormedSpace β„‚ G]
7081

7182
section Defs
7283

@@ -174,6 +185,63 @@ theorem fourierIntegral_continuous [FirstCountableTopology W] (he : Continuous e
174185

175186
end Continuous
176187

188+
section Fubini
189+
190+
variable [TopologicalSpace π•œ] [TopologicalRing π•œ] [TopologicalSpace V] [BorelSpace V]
191+
[TopologicalSpace W] [MeasurableSpace W] [BorelSpace W]
192+
{e : Multiplicative π•œ β†’* π•Š} {ΞΌ : Measure V} {L : V β†’β‚—[π•œ] W β†’β‚—[π•œ] π•œ}
193+
{Ξ½ : Measure W} [SigmaFinite ΞΌ] [SigmaFinite Ξ½] [SecondCountableTopology V]
194+
195+
variable [CompleteSpace E] [CompleteSpace F]
196+
197+
/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.
198+
Version where the multiplication is replaced by a general bilinear form `M`. -/
199+
theorem integral_bilin_fourierIntegral_eq_flip
200+
{f : V β†’ E} {g : W β†’ F} (M : E β†’L[β„‚] F β†’L[β„‚] G) (he : Continuous e)
201+
(hL : Continuous fun p : V Γ— W => L p.1 p.2) (hf : Integrable f ΞΌ) (hg : Integrable g Ξ½) :
202+
∫ ΞΎ, M (fourierIntegral e ΞΌ L f ΞΎ) (g ΞΎ) βˆ‚Ξ½ =
203+
∫ x, M (f x) (fourierIntegral e Ξ½ L.flip g x) βˆ‚ΞΌ := by
204+
by_cases hG : CompleteSpace G; swap; Β· simp [integral, hG]
205+
calc
206+
∫ ΞΎ, M (fourierIntegral e ΞΌ L f ΞΎ) (g ΞΎ) βˆ‚Ξ½
207+
= ∫ ΞΎ, M.flip (g ΞΎ) (∫ x, e[-L x ΞΎ] β€’ f x βˆ‚ΞΌ) βˆ‚Ξ½ := rfl
208+
_ = ∫ ΞΎ, (∫ x, M.flip (g ΞΎ) (e[-L x ΞΎ] β€’ f x) βˆ‚ΞΌ) βˆ‚Ξ½ := by
209+
congr with ΞΎ
210+
apply (ContinuousLinearMap.integral_comp_comm _ _).symm
211+
exact (fourier_integral_convergent_iff he hL _).1 hf
212+
_ = ∫ x, (∫ ΞΎ, M.flip (g ΞΎ) (e[-L x ΞΎ] β€’ f x) βˆ‚Ξ½) βˆ‚ΞΌ := by
213+
rw [integral_integral_swap]
214+
have : Integrable (fun (p : W Γ— V) ↦ β€–Mβ€– * (β€–g p.1β€– * β€–f p.2β€–)) (Ξ½.prod ΞΌ) :=
215+
(hg.norm.prod_mul hf.norm).const_mul _
216+
apply this.mono
217+
Β· have A : AEStronglyMeasurable (fun (p : W Γ— V) ↦ e[-L p.2 p.1] β€’ f p.2) (Ξ½.prod ΞΌ) := by
218+
apply (Continuous.aestronglyMeasurable ?_).smul hf.1.snd
219+
refine (continuous_induced_rng.mp he).comp (continuous_ofAdd.comp ?_)
220+
exact (hL.comp continuous_swap).neg
221+
exact M.flip.continuousβ‚‚.comp_aestronglyMeasurable (hg.1.fst.prod_mk A)
222+
Β· apply eventually_of_forall
223+
rintro ⟨ξ, x⟩
224+
simp only [ofAdd_neg, map_inv, coe_inv_unitSphere, SMulHomClass.map_smul,
225+
ContinuousLinearMap.flip_apply, Function.uncurry_apply_pair, norm_smul, norm_inv,
226+
norm_eq_of_mem_sphere, inv_one, one_mul, norm_mul, norm_norm]
227+
exact (M.le_opNormβ‚‚ (f x) (g ΞΎ)).trans (le_of_eq (by ring))
228+
_ = ∫ x, (∫ ΞΎ, M (f x) (e[-L.flip ΞΎ x] β€’ g ΞΎ) βˆ‚Ξ½) βˆ‚ΞΌ := by simp
229+
_ = ∫ x, M (f x) (∫ ΞΎ, e[-L.flip ΞΎ x] β€’ g ΞΎ βˆ‚Ξ½) βˆ‚ΞΌ := by
230+
congr with x
231+
apply ContinuousLinearMap.integral_comp_comm
232+
apply (fourier_integral_convergent_iff he _ _).1 hg
233+
exact hL.comp continuous_swap
234+
235+
/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint. -/
236+
theorem integral_fourierIntegral_smul_eq_flip
237+
{f : V β†’ β„‚} {g : W β†’ F} (he : Continuous e)
238+
(hL : Continuous fun p : V Γ— W => L p.1 p.2) (hf : Integrable f ΞΌ) (hg : Integrable g Ξ½) :
239+
∫ ΞΎ, (fourierIntegral e ΞΌ L f ΞΎ) β€’ (g ΞΎ) βˆ‚Ξ½ =
240+
∫ x, (f x) β€’ (fourierIntegral e Ξ½ L.flip g x) βˆ‚ΞΌ :=
241+
integral_bilin_fourierIntegral_eq_flip (ContinuousLinearMap.lsmul β„‚ β„‚) he hL hf hg
242+
243+
end Fubini
244+
177245
end VectorFourier
178246

179247
/-! ## Fourier theory for functions on `π•œ` -/
@@ -232,12 +300,14 @@ def fourierChar : Multiplicative ℝ β†’* π•Š where
232300
map_mul' x y := by simp only; rw [toAdd_mul, mul_add, expMapCircle_add]
233301
#align real.fourier_char Real.fourierChar
234302

235-
theorem fourierChar_apply (x : ℝ) : Real.fourierChar[x] = Complex.exp (↑(2 * Ο€ * x) * Complex.I) :=
303+
@[inherit_doc] scoped[FourierTransform] notation "𝐞" => Real.fourierChar
304+
305+
theorem fourierChar_apply (x : ℝ) : 𝐞[x] = Complex.exp (↑(2 * Ο€ * x) * Complex.I) :=
236306
by rfl
237307
#align real.fourier_char_apply Real.fourierChar_apply
238308

239309
@[continuity]
240-
theorem continuous_fourierChar : Continuous Real.fourierChar :=
310+
theorem continuous_fourierChar : Continuous 𝐞 :=
241311
(map_continuous expMapCircle).comp (continuous_const.mul continuous_toAdd)
242312
#align real.continuous_fourier_char Real.continuous_fourierChar
243313

@@ -251,23 +321,71 @@ theorem vector_fourierIntegral_eq_integral_exp_smul {V : Type*} [AddCommGroup V]
251321
by simp_rw [VectorFourier.fourierIntegral, Real.fourierChar_apply, mul_neg, neg_mul]
252322
#align real.vector_fourier_integral_eq_integral_exp_smul Real.vector_fourierIntegral_eq_integral_exp_smul
253323

254-
/-- The Fourier integral for `f : ℝ β†’ E`, with respect to the standard additive character and
255-
measure on `ℝ`. -/
256-
def fourierIntegral (f : ℝ β†’ E) (w : ℝ) :=
257-
Fourier.fourierIntegral fourierChar volume f w
324+
325+
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace β„‚ E]
326+
{V : Type*} [NormedAddCommGroup V]
327+
[InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V]
328+
{W : Type*} [NormedAddCommGroup W]
329+
[InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [FiniteDimensional ℝ W]
330+
331+
open scoped RealInnerProductSpace
332+
333+
/-- The Fourier transform of a function on an inner product space, with respect to the standard
334+
additive character `Ο‰ ↦ exp (2 i Ο€ Ο‰)`. -/
335+
def fourierIntegral (f : V β†’ E) (w : V) : E :=
336+
VectorFourier.fourierIntegral 𝐞 volume (innerβ‚— V) f w
258337
#align real.fourier_integral Real.fourierIntegral
259338

260-
theorem fourierIntegral_def (f : ℝ β†’ E) (w : ℝ) :
261-
fourierIntegral f w = ∫ v : ℝ, fourierChar[-(v * w)] β€’ f v :=
262-
rfl
263-
#align real.fourier_integral_def Real.fourierIntegral_def
339+
/-- The inverse Fourier transform of a function on an inner product space, defined as the Fourier
340+
transform but with opposite sign in the exponential. -/
341+
def fourierIntegralInv (f : V β†’ E) (w : V) : E :=
342+
VectorFourier.fourierIntegral 𝐞 volume (-innerβ‚— V) f w
264343

265344
@[inherit_doc] scoped[FourierTransform] notation "𝓕" => Real.fourierIntegral
345+
@[inherit_doc] scoped[FourierTransform] notation "𝓕⁻" => Real.fourierIntegralInv
346+
347+
lemma fourierIntegral_eq (f : V β†’ E) (w : V) :
348+
𝓕 f w = ∫ v, 𝐞[-βŸͺv, w⟫] β€’ f v := rfl
266349

267-
theorem fourierIntegral_eq_integral_exp_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace β„‚ E]
268-
(f : ℝ β†’ E) (w : ℝ) :
350+
lemma fourierIntegral_eq' (f : V β†’ E) (w : V) :
351+
𝓕 f w = ∫ v, Complex.exp ((↑(-2 * Ο€ * βŸͺv, w⟫) * Complex.I)) β€’ f v := by
352+
simp_rw [fourierIntegral_eq, Real.fourierChar_apply, mul_neg, neg_mul]
353+
354+
lemma fourierIntegralInv_eq (f : V β†’ E) (w : V) :
355+
𝓕⁻ f w = ∫ v, 𝐞[βŸͺv, w⟫] β€’ f v := by
356+
simp [fourierIntegralInv, VectorFourier.fourierIntegral]
357+
358+
lemma fourierIntegralInv_eq' (f : V β†’ E) (w : V) :
359+
𝓕⁻ f w = ∫ v, Complex.exp ((↑(2 * Ο€ * βŸͺv, w⟫) * Complex.I)) β€’ f v := by
360+
simp_rw [fourierIntegralInv_eq, Real.fourierChar_apply]
361+
362+
lemma fourierIntegralInv_eq_fourierIntegral_neg (f : V β†’ E) (w : V) :
363+
𝓕⁻ f w = 𝓕 f (-w) := by
364+
simp [fourierIntegral_eq, fourierIntegralInv_eq]
365+
366+
lemma fourierIntegral_comp_linearIsometry (A : W ≃ₗᡒ[ℝ] V) (f : V β†’ E) (w : W) :
367+
𝓕 (f ∘ A) w = (𝓕 f) (A w) := by
368+
simp only [fourierIntegral_eq, ofAdd_neg, map_inv, coe_inv_unitSphere, Function.comp_apply,
369+
← MeasurePreserving.integral_comp A.measurePreserving A.toHomeomorph.measurableEmbedding,
370+
← A.inner_map_map]
371+
372+
lemma fourierIntegralInv_comp_linearIsometry (A : W ≃ₗᡒ[ℝ] V) (f : V β†’ E) (w : W) :
373+
𝓕⁻ (f ∘ A) w = (𝓕⁻ f) (A w) := by
374+
simp [fourierIntegralInv_eq_fourierIntegral_neg, fourierIntegral_comp_linearIsometry]
375+
376+
theorem fourierIntegral_real_eq (f : ℝ β†’ E) (w : ℝ) :
377+
fourierIntegral f w = ∫ v : ℝ, 𝐞[-(v * w)] β€’ f v :=
378+
rfl
379+
#align real.fourier_integral_def Real.fourierIntegral_real_eq
380+
381+
@[deprecated] alias fourierIntegral_def := fourierIntegral_real_eq -- deprecated on 2024-02-21
382+
383+
theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ β†’ E) (w : ℝ) :
269384
𝓕 f w = ∫ v : ℝ, Complex.exp (↑(-2 * Ο€ * v * w) * Complex.I) β€’ f v := by
270-
simp_rw [fourierIntegral_def, Real.fourierChar_apply, mul_neg, neg_mul, mul_assoc]
271-
#align real.fourier_integral_eq_integral_exp_smul Real.fourierIntegral_eq_integral_exp_smul
385+
simp_rw [fourierIntegral_real_eq, Real.fourierChar_apply, mul_neg, neg_mul, mul_assoc]
386+
#align real.fourier_integral_eq_integral_exp_smul Real.fourierIntegral_real_eq_integral_exp_smul
387+
388+
@[deprecated] alias fourierIntegral_eq_integral_exp_smul :=
389+
fourierIntegral_real_eq_integral_exp_smul -- deprecated on 2024-02-21
272390

273391
end Real

β€ŽMathlib/Analysis/Fourier/PoissonSummation.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ theorem Real.fourierCoeff_tsum_comp_add {f : C(ℝ, β„‚)}
9797
exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _
9898
-- Minor tidying to finish
9999
_ = 𝓕 f m := by
100-
rw [fourierIntegral_eq_integral_exp_smul]
100+
rw [fourierIntegral_real_eq_integral_exp_smul]
101101
congr 1 with x : 1
102102
rw [smul_eq_mul, comp_apply, coe_mk, coe_mk, ContinuousMap.toFun_eq_coe, fourier_coe_apply]
103103
congr 2

0 commit comments

Comments
Β (0)