Fourier transform of dilations

3 fully proved

Dilations

TheoremFourier transform of a dilation#✓fully proved

Let \(E\) be a complex normed space, and write \(\hat g(y) = \int_{\mathbb{R}} e^{-2\pi i x y} g(x)\,dx\) for the Fourier transform of a function \(g : \mathbb{R} \to E\). For every \(f : \mathbb{R} \to E\), every real \(a \ne 0\) and every real \(y\), the Fourier transform of \(x \mapsto f(ax)\) at \(y\) equals \(|a|^{-1} \hat f(y/a)\).

No integrability hypothesis is needed because Mathlib's Bochner integral is totalized, so the identity also uses that convention for nonintegrable functions.

theorem fourier_comp_mul_left (f : ℝ → E) {a : ℝ} (ha : a ≠ 0) (y : ℝ) :
    𝓕 (fun x => f (a * x)) y = (|a|⁻¹ : ℝ) • 𝓕 f (y / a)

Used by 1

Used byFourier transform of a dilation by a positive factor

TheoremFourier transform of a dilation by a positive factor#✓fully proved

Write \(\hat g(y) = \int_{\mathbb{R}} e^{-2\pi i x y} g(x)\,dx\) for the Fourier transform of a function \(g : \mathbb{R} \to \mathbb{C}\). For every \(f : \mathbb{R} \to \mathbb{C}\), every real \(a > 0\) and every real \(y\), the Fourier transform of \(x \mapsto f(ax)\) at \(y\) equals \(a^{-1} \hat f(y/a)\).

No integrability hypothesis is needed because Mathlib's Bochner integral is totalized, so the identity also uses that convention for nonintegrable functions.

theorem fourier_comp_mul_left_of_pos (f : ℝ → ℂ) {a : ℝ} (ha : 0 < a) (y : ℝ) :
    𝓕 (fun x => f (a * x)) y = ((a : ℂ)⁻¹) • 𝓕 f (y / a)

Uses 1 · Used by 2

Proof usesFourier transform of a dilation

Used byFourier transform of a dilated Schwartz function · Wiener's Tauberian theorem on \(L^1(\mathbb{R})\)

Schwartz Map

TheoremFourier transform of a dilated Schwartz function#✓fully proved

Write \(\hat g(y) = \int_{\mathbb{R}} e^{-2\pi i x y} g(x)\,dx\) for the Fourier transform of a function \(g : \mathbb{R} \to \mathbb{C}\). For every Schwartz function \(f : \mathbb{R} \to \mathbb{C}\), every real \(a > 0\) and every real \(y\), the Fourier transform of \(x \mapsto f(ax)\) at \(y\) equals \(a^{-1} \hat f(y/a)\).

theorem fourier_coe_comp_mul_left_of_pos (f : SchwartzMap ℝ ℂ) {a : ℝ} (ha : 0 < a)
    (y : ℝ) :
    𝓕 (fun x => (f : ℝ → ℂ) (a * x)) y
      = ((a : ℂ)⁻¹) • 𝓕 (f : ℝ → ℂ) (y / a)

Uses 1

Proof usesFourier transform of a dilation by a positive factor

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.