Fourier–Plancherel infrastructure on ℝ

This file prepares the ingredients required for the Fourier–Plancherel theorem on the real line. The goal is to express the Fourier integral in the more familiar e^{-2π i x ξ} form and to record basic properties (measurability, integrability, norm preservation of the kernel) that are frequently used when extending the Fourier transform from Schwartz functions to the L² setting.

The actual isometry statement is postponed to a later stage; here we progressively organise the supporting lemmas so that subsequent files can invoke them without having to unfold the Fourier kernel repeatedly.

def Frourio.fourierKernel (ξ t : ℝ) : ℂ

Fourier kernel on ℝ, written explicitly as exp(-2π i t ξ).

Equations

• Frourio.fourierKernel ξ t = Complex.exp (↑(-(2 * Real.pi * ξ * t)) * Complex.I)

@[simp]

theorem Frourio.fourierKernel_zero_left (t : ℝ) : fourierKernel 0 t = 1

@[simp]

theorem Frourio.fourierKernel_zero_right (ξ : ℝ) : fourierKernel ξ 0 = 1

theorem Frourio.fourierKernel_norm (ξ t : ℝ) : ‖fourierKernel ξ t‖ = 1

theorem Frourio.fourierKernel_mul_eq (ξ t : ℝ) (z : ℂ) : fourierKernel ξ t * z = Real.fourierChar (-(t * ξ)) • z

theorem Frourio.fourierKernel_eq_char (ξ t : ℝ) : fourierKernel ξ t = ↑(Real.fourierChar (-(t * ξ)))

theorem Frourio.fourierKernel_mul_norm (ξ t : ℝ) (z : ℂ) : ‖fourierKernel ξ t * z‖ = ‖z‖

theorem Frourio.fourierKernel_neg_div_two_pi (τ t : ℝ) : fourierKernel (-τ / (2 * Real.pi)) t = Complex.exp (Complex.I * ↑τ * ↑t)

theorem Frourio.integral_fourierIntegral_rescale_sq (g : ℝ → ℂ) : ∫ (τ : ℝ), ‖Real.fourierIntegral g (-τ / (2 * Real.pi))‖ ^ 2 = 2 * Real.pi * ∫ (ξ : ℝ), ‖Real.fourierIntegral g ξ‖ ^ 2

theorem Frourio.fourierKernel_conj (ξ t : ℝ) : (starRingEnd ℂ) (fourierKernel ξ t) = fourierKernel (-ξ) t

theorem Frourio.fourierKernel_neg (ξ t : ℝ) : fourierKernel (-ξ) t = (starRingEnd ℂ) (fourierKernel ξ t)

theorem Frourio.integrable_fourierKernel_mul_iff {f : ℝ → ℂ} (ξ : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => fourierKernel ξ t * f t) MeasureTheory.volume ↔ MeasureTheory.Integrable f MeasureTheory.volume

theorem Frourio.integrable_fourierKernel_mul {f : ℝ → ℂ} (ξ : ℝ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : MeasureTheory.Integrable (fun (t : ℝ) => fourierKernel ξ t * f t) MeasureTheory.volume

theorem Frourio.integrable_conj_of_integrable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℂ} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.Integrable (fun (t : α) => (starRingEnd ℂ) (f t)) μ

def Frourio.fourierIntegral (f : ℝ → ℂ) (ξ : ℝ) : ℂ

The Fourier integral expressed via the explicit kernel.

Equations

• Frourio.fourierIntegral f ξ = ∫ (t : ℝ), Frourio.fourierKernel ξ t * f t

theorem Frourio.fourierIntegral_eq_real (f : ℝ → ℂ) (ξ : ℝ) : Real.fourierIntegral f ξ = fourierIntegral f ξ

theorem Frourio.norm_fourierIntegral_le (f : ℝ → ℂ) (ξ : ℝ) : ‖fourierIntegral f ξ‖ ≤ ∫ (t : ℝ), ‖f t‖

theorem Frourio.fourierIntegral_smul (c : ℂ) {f : ℝ → ℂ} (_hf : MeasureTheory.Integrable f MeasureTheory.volume) (ξ : ℝ) : fourierIntegral (fun (t : ℝ) => c * f t) ξ = c * fourierIntegral f ξ

theorem Frourio.fourierIntegral_add {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ξ : ℝ) : fourierIntegral (fun (t : ℝ) => f t + g t) ξ = fourierIntegral f ξ + fourierIntegral g ξ

theorem Frourio.fourierIntegral_sub {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ξ : ℝ) : fourierIntegral (fun (t : ℝ) => f t - g t) ξ = fourierIntegral f ξ - fourierIntegral g ξ

theorem Frourio.fourierIntegral_conj {f : ℝ → ℂ} (_hf : MeasureTheory.Integrable f MeasureTheory.volume) (ξ : ℝ) : (starRingEnd ℂ) (fourierIntegral f ξ) = fourierIntegral (fun (t : ℝ) => (starRingEnd ℂ) (f t)) (-ξ)

theorem Frourio.integrand_norm_sq (ξ t : ℝ) (f : ℝ → ℂ) : ‖fourierKernel ξ t * f t‖ ^ 2 = ‖f t‖ ^ 2

Equality of squared norms of the integrand, used repeatedly when working with L² functions.

theorem Frourio.fourierIntegral_apply (f : ℝ → ℂ) (ξ : ℝ) : fourierIntegral f ξ = ∫ (t : ℝ), fourierKernel ξ t * f t

Helper lemma for rewriting the pointwise value of the Fourier integral in terms of the explicit kernel.

theorem Frourio.fourierIntegral_abs_le (f : ℝ → ℂ) (ξ : ℝ) : ‖fourierIntegral f ξ‖ ≤ ∫ (t : ℝ), ‖f t‖

Pointwise boundedness for the explicit kernel formulation.

Behaviour on Schwartz functions

theorem Frourio.Schwartz.integrable_fourierKernel_mul (f : SchwartzMap ℝ ℂ) (ξ : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => fourierKernel ξ t * f t) MeasureTheory.volume

Multiplying a Schwartz function by the Fourier kernel keeps it integrable.

theorem Frourio.Schwartz.fourierIntegral_eq_fourierTransform (f : SchwartzMap ℝ ℂ) (ξ : ℝ) : fourierIntegral (fun (t : ℝ) => f t) ξ = ((SchwartzMap.fourierTransformCLE ℝ) f) ξ

Identify our explicit kernel formulation with mathlib's Fourier transform on Schwartz functions.

theorem Frourio.Schwartz.fourierIntegral_conj_eq_neg (f : SchwartzMap ℝ ℂ) (ξ : ℝ) : fourierIntegral (fun (t : ℝ) => (starRingEnd ℂ) (f t)) ξ = (starRingEnd ℂ) (fourierIntegral (fun (t : ℝ) => f t) (-ξ))

Conjugating a Schwartz function before applying the Fourier integral is the same as conjugating the transform and negating the frequency.

theorem Frourio.Schwartz.fourierIntegral_conj_eq_neg_real (f : SchwartzMap ℝ ℂ) (ξ : ℝ) : Real.fourierIntegral (fun (t : ℝ) => (starRingEnd ℂ) (f t)) ξ = (starRingEnd ℂ) (Real.fourierIntegral (fun (t : ℝ) => f t) (-ξ))

Real-notation variant of fourierIntegral_conj_eq_neg.

theorem Frourio.Schwartz.integrable_fourierIntegral (f : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => f t) ξ) MeasureTheory.volume

theorem Frourio.Schwartz.integrable_fourierIntegral_neg (f : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => f t) (-ξ)) MeasureTheory.volume

The Fourier transform of a Schwartz function remains integrable after negating the frequency.

theorem Frourio.Schwartz.integrable_conj_fourierIntegral (f : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (ξ : ℝ) => (starRingEnd ℂ) (fourierIntegral (fun (t : ℝ) => f t) ξ)) MeasureTheory.volume

The conjugate of the Fourier transform of a Schwartz function is integrable.

def Frourio.Schwartz.conjFourierTransform (f : SchwartzMap ℝ ℂ) : ℝ → ℂ

The conjugated Fourier transform as a function.

Equations

• Frourio.Schwartz.conjFourierTransform f ξ = (starRingEnd ℂ) (Frourio.fourierIntegral (fun (t : ℝ) => f t) ξ)

def Frourio.Schwartz.doubleFourierTransform (f : SchwartzMap ℝ ℂ) : ℝ → ℂ

The Fourier integral of the conjugated Fourier transform.

Equations

• Frourio.Schwartz.doubleFourierTransform f = Frourio.fourierIntegral (Frourio.Schwartz.conjFourierTransform f)

theorem Frourio.Schwartz.fourierIntegral_conj_fourierIntegral (f : SchwartzMap ℝ ℂ) : doubleFourierTransform f = fun (t : ℝ) => (starRingEnd ℂ) (f t)

Taking the Fourier integral of the conjugated Fourier transform recovers the conjugate.

theorem Frourio.Schwartz.schwartz_approximates_smooth_compactly_supported (g : ℝ → ℂ) (hg_compact : HasCompactSupport g) (hg_smooth : ContDiff ℝ (↑⊤) g) (ε : ℝ) (hε_pos : ε > 0) : ∃ (φ : SchwartzMap ℝ ℂ), MeasureTheory.eLpNorm (g - ⇑φ) 2 MeasureTheory.volume < ENNReal.ofReal ε

Smooth compactly supported functions can be approximated by Schwartz functions in L²(ℝ)

Towards Fourier–Plancherel

The lemmas collected above allow us to treat the Fourier transform in its classical exponential form inside L² developments. The remaining step – extending the transform to a unitary map on L²(ℝ) – will rely on the density of Schwartz functions together with the continuity of the Fourier transform; this part is deferred to future work.

theorem Frourio.fourier_plancherel (f : SchwartzMap ℝ ℂ) : ∫ (t : ℝ), ‖f t‖ ^ 2 = ∫ (ξ : ℝ), ‖fourierIntegral (fun (t : ℝ) => f t) ξ‖ ^ 2

Fourier–Plancherel theorem for Schwartz functions written with the explicit kernel exp (-2π i ξ t).

With this normalisation the Fourier transform is an isometry on L², so no additional constant appears in the equality.