Linear change of variables for the Fourier transform

Precomposing a function by a continuous real linear automorphism rescales its Fourier transform by the inverse absolute determinant and precomposes it by the adjoint of the inverse. This is the change of coordinates needed to transport Fourier identities from the standard integer lattice to an arbitrary full lattice. For a dilation x ↦ c • x it reads 𝓕 (f (c • ·)) y = |c ^ n|⁻¹ • 𝓕 f (c⁻¹ • y) in dimension n, so that dilating a function does not change the L¹ norm of its Fourier transform, while replacing g by g (R⁻¹ • ·), R > 0, multiplies the Lʳ norm of its inverse Fourier transform by R ^ (n - n / r).

The Jacobian factor comes from Mathlib's MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar. The formulas use the total Bochner integral, so no integrability hypothesis is necessary. They apply to functions with values in any complex normed space, including Schwartz functions by coercion.

Main results

• ContinuousLinearEquiv.fourier_comp: change of variables for the Fourier transform.
• ContinuousLinearEquiv.fourierInv_comp: the corresponding inverse-transform formula.
• TauCeti.fourier_comp_smul, TauCeti.fourierInv_comp_smul: the dilation formulas.
• TauCeti.support_fourier_comp_smul: dilating a function by c dilates the support of its Fourier transform by c.
• TauCeti.integral_norm_fourierInv_comp_smul: dilation preserves the L¹ norm of the inverse Fourier transform.
• TauCeti.eLpNorm_fourierInv_comp_inv_smul: dilation rescales the Lʳ norm of the inverse Fourier transform.
• TauCeti.fourier_fourierChar_smul: modulation by the character 𝐞 ⟪·, c⟫ translates the Fourier transform by c.
• TauCeti.fourier_smul_const: the Fourier transform of f · • v is 𝓕 f · • v.
• TauCeti.exp_inner_mul_I_eq_fourierChar: the exponential exp(i ⟪y, ξ⟫) is the Fourier character at the frequency ξ / 2π.

theorem ContinuousLinearEquiv.fourier_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (A : E ≃L[ℝ] E) (f : E → F) (y : E) : FourierTransform.fourier (f ∘ ⇑A) y = |LinearMap.det ↑↑A|⁻¹ • FourierTransform.fourier f ((ContinuousLinearMap.adjoint ↑A.symm) y)

Fourier change of variables under a real linear automorphism. The frequency transforms by the adjoint of the inverse, and the scalar is the inverse absolute determinant.

theorem ContinuousLinearEquiv.fourierInv_comp {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (A : E ≃L[ℝ] E) (f : E → F) (y : E) : FourierTransformInv.fourierInv (f ∘ ⇑A) y = |LinearMap.det ↑↑A|⁻¹ • FourierTransformInv.fourierInv f ((ContinuousLinearMap.adjoint ↑A.symm) y)

The inverse Fourier transform has the same linear change-of-variables law.

theorem TauCeti.fourier_comp_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : E → F) (c : ℝ) (y : E) : FourierTransform.fourier (fun (x : E) => f (c • x)) y = |c ^ Module.finrank ℝ E|⁻¹ • FourierTransform.fourier f (c⁻¹ • y)

Fourier transform of a dilation: 𝓕 (f (c • ·)) y = |c ^ n|⁻¹ • 𝓕 f (c⁻¹ • y), where n is the dimension. For c = 0 both sides vanish, or agree trivially in dimension zero.

theorem TauCeti.support_fourier_comp_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : E → F) {c : ℝ} (hc : c ≠ 0) : Function.support (FourierTransform.fourier fun (x : E) => f (c • x)) = c • Function.support (FourierTransform.fourier f)

Frequencies of a dilation: the Fourier transform of f (c • ·) is supported on the dilate c • support (𝓕 f) of the support of 𝓕 f.

theorem TauCeti.fourierInv_comp_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : E → F) (c : ℝ) (y : E) : FourierTransformInv.fourierInv (fun (x : E) => f (c • x)) y = |c ^ Module.finrank ℝ E|⁻¹ • FourierTransformInv.fourierInv f (c⁻¹ • y)

Inverse Fourier transform of a dilation: 𝓕⁻ (f (c • ·)) y = |c ^ n|⁻¹ • 𝓕⁻ f (c⁻¹ • y), where n is the dimension.

theorem TauCeti.integral_norm_fourierInv_comp_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : E → F) {c : ℝ} (hc : c ≠ 0) : ∫ (y : E), ‖FourierTransformInv.fourierInv (fun (x : E) => f (c • x)) y‖ = ∫ (y : E), ‖FourierTransformInv.fourierInv f y‖

Dilating a function does not change the L¹ norm of its inverse Fourier transform: ∫ ‖𝓕⁻ (f (c • ·))‖ = ∫ ‖𝓕⁻ f‖.

theorem TauCeti.eLpNorm_fourierInv_comp_inv_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (g : E → F) {R : ℝ} (hR : 0 < R) (r : ENNReal) : MeasureTheory.eLpNorm (FourierTransformInv.fourierInv fun (ξ : E) => g (R⁻¹ • ξ)) r MeasureTheory.volume = ENNReal.ofReal (R ^ (↑(Module.finrank ℝ E) - ↑(Module.finrank ℝ E) / r.toReal)) * MeasureTheory.eLpNorm (FourierTransformInv.fourierInv g) r MeasureTheory.volume

Dilating a function rescales the Lʳ norm of its inverse Fourier transform: for R > 0, the inverse Fourier transform of ξ ↦ g (R⁻¹ • ξ) has Lʳ norm R ^ (n - n / r) times that of 𝓕⁻ g, where n is the dimension.

Translation in frequency

theorem TauCeti.fourier_fourierChar_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (f : E → F) (c ζ : E) : FourierTransform.fourier (fun (y : E) => Real.fourierChar (inner ℝ y c) • f y) ζ = FourierTransform.fourier f (ζ - c)

Modulation: multiplying by the character 𝐞 ⟪·, c⟫ translates the Fourier transform, 𝓕 (𝐞 ⟪·, c⟫ • f) ζ = 𝓕 f (ζ - c).

theorem TauCeti.fourier_smul_const {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] (f : E → ℂ) (v : F) (w : E) : FourierTransform.fourier (fun (z : E) => f z • v) w = FourierTransform.fourier f w • v

The Fourier transform of a scalar function times a constant vector: 𝓕 (f · • v) w = 𝓕 f w • v.

theorem TauCeti.exp_inner_mul_I_eq_fourierChar {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (y ξ : E) : Complex.exp (↑(inner ℝ y ξ) * Complex.I) = ↑(Real.fourierChar (inner ℝ y ((2 * Real.pi)⁻¹ • ξ)))

The exponential exp(i ⟪y, ξ⟫) is the Fourier character 𝐞 ⟪y, ξ / 2π⟫.