@[reducible, inline]

abbrev FourierAnalysis.MultiIndex (n : ℕ) : Type

A multi-index of dimension n: an n-tuple $\vec{\alpha} = (\alpha^1, \dots, \alpha^n)$ of non-negative integers, encoded as a function Fin n → ℕ.

def FourierAnalysis.MultiIndex.order {n : ℕ} (α : MultiIndex n) : ℕ

The order of a multi-index $\vec{\alpha}$: $|\vec{\alpha}| := \alpha^1 + \cdots + \alpha^n$.

noncomputable def FourierAnalysis.multiIndexMonomial {n : ℕ} (x : Fin n → ℂ) (α : MultiIndex n) : ℂ

The monomial $x^{\vec{\alpha}} := (x^1)^{\alpha^1} \cdots (x^n)^{\alpha^n}$ for $x \in \mathbb{C}^n$ and multi-index $\vec{\alpha}$.

noncomputable def FourierAnalysis.iteratedPartialDeriv {n : ℕ} (i : Fin n) (k : ℕ) (f : (Fin n → ℝ) → ℂ) : (Fin n → ℝ) → ℂ

The k-fold partial derivative of f with respect to the i-th coordinate, $\partial_i^k f$, defined by iterating one-variable differentiation along the i-th axis.

noncomputable def FourierAnalysis.multiIndexDeriv {n : ℕ} (α : MultiIndex n) (f : (Fin n → ℝ) → ℂ) : (Fin n → ℝ) → ℂ

The differential operator $\partial_{\vec{\alpha}} := \partial_1^{\alpha^1} \cdots \partial_n^{\alpha^n}$ associated to a multi-index $\vec{\alpha}$.

def FourierAnalysis.IsCk (n k : ℕ) (f : (Fin n → ℝ) → ℂ) : Prop

The space $C^k$: predicate that f : ℝ^n → ℂ is k-times continuously differentiable.

def FourierAnalysis.IsC0 (n : ℕ) (f : (Fin n → ℝ) → ℂ) : Prop

The space $C_0$: predicate that f : ℝ^n → ℂ is continuous and vanishes at infinity, i.e. $\lim_{|x| \to \infty} f(x) = 0$.

noncomputable def FourierAnalysis.supNorm (n : ℕ) (f : (Fin n → ℝ) → ℂ) : ℝ

The supremum norm $\|f\|_{C_0} := \sup_{x \in \mathbb{R}^n} |f(x)|$.

noncomputable def FourierAnalysis.fourierTransform (f : ℝ → ℂ) (ξ : ℝ) : ℂ

The one-dimensional Fourier transform $\hat{f}(\xi) := \int_{\mathbb{R}} f(x) e^{-2\pi i \xi x}\, dx$.

noncomputable def FourierAnalysis.inverseFourierTransform (f : ℝ → ℂ) (x : ℝ) : ℂ

The one-dimensional inverse Fourier transform $f^{\vee}(x) := \int_{\mathbb{R}} f(\xi) e^{2\pi i \xi x}\, d\xi$.

noncomputable def FourierAnalysis.complexL2Inner (f g : ℝ → ℂ) : ℂ

The complex $L^2$ inner product on $\mathbb{R}$: $\langle f, g \rangle := \int_{\mathbb{R}} f(x) \overline{g(x)}\, dx$.

noncomputable def FourierAnalysis.complexL2Norm (f : ℝ → ℂ) : ℝ

The complex $L^2$ norm on $\mathbb{R}$: $\|f\| := \langle f, f \rangle^{1/2}$.

noncomputable def FourierAnalysis.complexL2InnerND {n : ℕ} (f g : (Fin n → ℝ) → ℂ) : ℂ

The complex $L^2$ inner product on $\mathbb{R}^n$: $\langle f, g \rangle := \int_{\mathbb{R}^n} f(x) \overline{g(x)}\, d^n x$.

noncomputable def FourierAnalysis.complexL2NormND {n : ℕ} (f : (Fin n → ℝ) → ℂ) : ℝ

The complex $L^2$ norm on $\mathbb{R}^n$: $\|f\| := \langle f, f \rangle^{1/2}$.

def FourierAnalysis.translate (y : ℝ) (f : ℝ → ℂ) : ℝ → ℂ

Translation of a function on $\mathbb{R}$ by y: $(\tau_y f)(x) := f(x - y)$.

noncomputable def FourierAnalysis.complexConvolution (f g : ℝ → ℂ) : ℝ → ℂ

The complex convolution on $\mathbb{R}$: $(f * g)(x) := \int_{\mathbb{R}} f(x - y) g(y)\, dy$.

noncomputable def FourierAnalysis.complexConvolutionND {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (x : Fin n → ℝ) : ℂ

The complex convolution on $\mathbb{R}^n$: $(f * g)(x) := \int_{\mathbb{R}^n} f(y) g(x - y)\, d^n y$.

noncomputable def FourierAnalysis.fourierTransformND (n : ℕ) (f : (Fin n → ℝ) → ℂ) (ξ : Fin n → ℝ) : ℂ

The $n$-dimensional Fourier transform $\hat{f}(\xi) := \int_{\mathbb{R}^n} f(x) e^{-2\pi i \xi \cdot x}\, d^n x$.

noncomputable def FourierAnalysis.inverseFourierTransformND (n : ℕ) (g : (Fin n → ℝ) → ℂ) (x : Fin n → ℝ) : ℂ

The $n$-dimensional inverse Fourier transform $g^{\vee}(x) := \int_{\mathbb{R}^n} g(\xi) e^{2\pi i \xi \cdot x}\, d^n \xi$.

def FourierAnalysis.euclidNormSq {n : ℕ} (x : Fin n → ℝ) : ℝ

The squared Euclidean norm $|x|^2 := \sum_i (x_i)^2$ on $\mathbb{R}^n$.

def FourierAnalysis.translateFn {n : ℕ} (y : Fin n → ℝ) (f : (Fin n → ℝ) → ℂ) (x : Fin n → ℝ) : ℂ

Translation in $\mathbb{R}^n$: $(\tau_y f)(x) := f(x - y)$ (Definition 2.0.6).

theorem FourierAnalysis.fourierTransform_bound (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ξ : ℝ) : ‖fourierTransform f ξ‖ ≤ ∫ (x : ℝ), ‖f x‖

For $f \in L^1(\mathbb{R})$, the Fourier transform is pointwise bounded: $|\hat{f}(\xi)| \le \|f\|_{L^1}$ (part of Lemma 2.0.1).

theorem FourierAnalysis.fourierTransform_continuous (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : Continuous (fourierTransform f)

For $f \in L^1(\mathbb{R})$, the Fourier transform $\hat{f}$ is continuous (part of Lemma 2.0.1).

theorem FourierAnalysis.fourierTransform_tendsto_zero (f : ℝ → ℂ) (_hf : MeasureTheory.Integrable f MeasureTheory.volume) : Filter.Tendsto (fourierTransform f) (Filter.cocompact ℝ) (nhds 0)

Riemann–Lebesgue: for $f \in L^1(\mathbb{R})$, $\hat{f}(\xi) \to 0$ as $|\xi| \to \infty$. This is the vanishing-at-infinity property in the definition of $C_0$.

theorem FourierAnalysis.fourier_L1_properties (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : Continuous (fourierTransform f) ∧ (∀ (ξ : ℝ), ‖fourierTransform f ξ‖ ≤ ∫ (x : ℝ), ‖f x‖) ∧ Filter.Tendsto (fourierTransform f) (Filter.cocompact ℝ) (nhds 0)

Lemma 2.0.1 (combined form): if $f \in L^1(\mathbb{R})$ then $\hat{f}$ is continuous, satisfies $\|\hat{f}\|_{C_0} \le \|f\|_{L^1}$, and vanishes at infinity.

theorem FourierAnalysis.fourier_translate (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (y ξ : ℝ) : fourierTransform (translate y f) ξ = Complex.exp (↑(-2 * Real.pi * ξ * y) * Complex.I) * fourierTransform f ξ

Translation/modulation duality (Theorem 2.1 (2.0.19a) in 1D): $(\tau_y f)^{\wedge}(\xi) = e^{-2\pi i \xi y} \hat{f}(\xi)$.

theorem FourierAnalysis.fourier_modulate (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (η ξ : ℝ) : fourierTransform (fun (x : ℝ) => Complex.exp (↑(2 * Real.pi * η * x) * Complex.I) * f x) ξ = fourierTransform f (ξ - η)

Modulation/translation duality (Theorem 2.1 (2.0.19b) in 1D): if $h(x) = e^{2\pi i \eta x} f(x)$ then $\hat{h}(\xi) = \hat{f}(\xi - \eta)$.

theorem FourierAnalysis.fourier_dilation (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (t : ℝ) (ht : t ≠ 0) (ξ : ℝ) : fourierTransform (fun (x : ℝ) => f (t⁻¹ * x)) ξ = ↑|t| * fourierTransform f (t * ξ)

Dilation (Theorem 2.1 (2.0.19c) in 1D): if $h(x) = f(t^{-1} x)$ then $\hat{h}(\xi) = |t|\, \hat{f}(t \xi)$.

theorem FourierAnalysis.fourier_convolution (f g : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ξ : ℝ) : fourierTransform (complexConvolution f g) ξ = fourierTransform f ξ * fourierTransform g ξ

Convolution maps to product (Theorem 2.1 (2.0.19d) in 1D): $(f * g)^{\wedge}(\xi) = \hat{f}(\xi)\, \hat{g}(\xi)$.

theorem FourierAnalysis.fourier_deriv_freq (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hxf : MeasureTheory.Integrable (fun (x : ℝ) => ↑x * f x) MeasureTheory.volume) (ξ : ℝ) : deriv (fourierTransform f) ξ = fourierTransform (fun (x : ℝ) => ↑(-2 * Real.pi) * Complex.I * ↑x * f x) ξ

Differentiation in frequency (Theorem 2.1 (2.0.19e) in 1D, order 1): $\dfrac{d}{d\xi}\hat{f}(\xi) = [(-2\pi i x) f(x)]^{\wedge}(\xi)$, under integrability of $f$ and $x f(x)$.

theorem FourierAnalysis.fourier_of_deriv (f : ℝ → ℂ) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hf'_int : MeasureTheory.Integrable (deriv f) MeasureTheory.volume) (hf_decay : Filter.Tendsto f (Filter.cocompact ℝ) (nhds 0)) (hf_diff : Differentiable ℝ f := by fun_prop) (ξ : ℝ) : fourierTransform (deriv f) ξ = ↑(2 * Real.pi) * Complex.I * ↑ξ * fourierTransform f ξ

Derivative becomes multiplication (Theorem 2.1 (2.0.19f) in 1D, order 1): $(f')^{\wedge}(\xi) = 2\pi i \xi\, \hat{f}(\xi)$, when $f, f' \in L^1$, $f$ is differentiable and vanishes at infinity.

theorem FourierAnalysis.fourier_conj (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ξ : ℝ) : (starRingEnd ℂ) (fourierTransform f ξ) = inverseFourierTransform (fun (x : ℝ) => (starRingEnd ℂ) (f x)) ξ

Conjugation identity (Theorem 2.1 (2.0.19g) in 1D, first half): $\overline{\hat{f}}(\xi) = (\bar{f})^{\vee}(\xi)$.

theorem FourierAnalysis.fourier_reverse_conj (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ξ : ℝ) : (starRingEnd ℂ) (inverseFourierTransform f ξ) = fourierTransform (fun (x : ℝ) => (starRingEnd ℂ) (f x)) ξ

Conjugation identity (Theorem 2.1 (2.0.19g) in 1D, second half): $\overline{f^{\vee}}(\xi) = (\bar{f})^{\wedge}(\xi)$.

theorem FourierAnalysis.fourier_translateND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (y ξ : Fin n → ℝ) : fourierTransformND n (translateFn y f) ξ = Complex.exp (↑(-2 * Real.pi) * Complex.I * ↑(∑ j : Fin n, ξ j * y j)) * fourierTransformND n f ξ

$n$-dimensional translation identity (Theorem 2.1 (2.0.19a)): $(\tau_y f)^{\wedge}(\xi) = e^{-2\pi i \xi \cdot y}\, \hat{f}(\xi)$.

theorem FourierAnalysis.fourier_modulateND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (η ξ : Fin n → ℝ) : fourierTransformND n (fun (x : Fin n → ℝ) => Complex.exp (↑(2 * Real.pi) * Complex.I * ↑(∑ j : Fin n, η j * x j)) * f x) ξ = fourierTransformND n f (ξ - η)

$n$-dimensional modulation identity (Theorem 2.1 (2.0.19b)): if $h(x) = e^{2\pi i \eta \cdot x} f(x)$ then $\hat{h}(\xi) = \hat{f}(\xi - \eta)$.

theorem FourierAnalysis.fourier_convolutionND {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (ξ : Fin n → ℝ) (hfg : MeasureTheory.Integrable (Function.uncurry fun (x y : Fin n → ℝ) => f y * g (x - y) * Complex.exp (↑(-2 * Real.pi) * Complex.I * ↑(∑ j : Fin n, ξ j * x j))) (MeasureTheory.volume.prod MeasureTheory.volume)) : fourierTransformND n (complexConvolutionND f g) ξ = fourierTransformND n f ξ * fourierTransformND n g ξ

$n$-dimensional convolution identity (Theorem 2.1 (2.0.19d)): $(f * g)^{\wedge}(\xi) = \hat{f}(\xi)\, \hat{g}(\xi)$, given joint integrability of the relevant uncurried integrand.

theorem FourierAnalysis.sum_update_decomp_coord {n : ℕ} (ξ : Fin n → ℝ) (i : Fin n) (t : ℝ) (x : Fin n → ℝ) : ∑ j : Fin n, Function.update ξ i t j * x j = t * x i + ∑ j ∈ Finset.univ.erase i, ξ j * x j

Decomposes the sum $\sum_j (\text{update } \xi\, i\, t)_j\, x_j$ as the contribution $t\, x_i$ from the updated coordinate plus the sum over the remaining indices.

theorem FourierAnalysis.continuous_cexp_update_coord {n : ℕ} (ξ : Fin n → ℝ) (i : Fin n) (t : ℝ) : Continuous fun (x : Fin n → ℝ) => Complex.exp (↑(-2 * Real.pi) * Complex.I * ↑(∑ j : Fin n, Function.update ξ i t j * x j))

Continuity of the exponential kernel $e^{-2\pi i (\text{update } \xi\, i\, t) \cdot x}$ viewed as a function of x.

theorem FourierAnalysis.hasDerivAt_fourierTransformND_coord {n : ℕ} (g : (Fin n → ℝ) → ℂ) (i : Fin n) (ξ : Fin n → ℝ) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) (hxg_int : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => ↑(x i) * g x) MeasureTheory.volume) : HasDerivAt (fun (t : ℝ) => fourierTransformND n g (Function.update ξ i t)) (fourierTransformND n (fun (x : Fin n → ℝ) => ↑(-2 * Real.pi) * Complex.I * ↑(x i) * g x) ξ) (ξ i)

Partial derivative of $\hat{g}(\xi)$ in the $i$-th frequency coordinate equals the Fourier transform of $-2\pi i x_i\, g(x)$ at $\xi$ (a key step in Theorem 2.1 (2.0.19e)).

theorem FourierAnalysis.integrable_pow_xi_mul {n : ℕ} {i : Fin n} {g : (Fin n → ℝ) → ℂ} {k : ℕ} (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) (hkg : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => ↑(|x i| ^ k) * g x) MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => (↑(-2 * Real.pi) * Complex.I * ↑(x i)) ^ k * g x) MeasureTheory.volume

Helper: if $|x_i|^k\, g(x)$ is integrable, then $(-2\pi i x_i)^k\, g(x)$ is integrable.

theorem FourierAnalysis.iteratedPartialDeriv_fourierTransformND {n : ℕ} (i : Fin n) (k : ℕ) (g : (Fin n → ℝ) → ℂ) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) (hkg_int : ∀ j ≤ k, MeasureTheory.Integrable (fun (x : Fin n → ℝ) => ↑(|x i| ^ j) * g x) MeasureTheory.volume) (ξ : Fin n → ℝ) : iteratedPartialDeriv i k (fourierTransformND n g) ξ = fourierTransformND n (fun (x : Fin n → ℝ) => (↑(-2 * Real.pi) * Complex.I * ↑(x i)) ^ k * g x) ξ

Iterated partial differentiation in frequency yields multiplication in space: $\partial_i^k \hat{g}(\xi) = [(-2\pi i x_i)^k\, g(x)]^{\wedge}(\xi)$, under integrability of $|x_i|^j g(x)$ for all $j \le k$.

theorem FourierAnalysis.ft_deriv_eq_ft_mulND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (β : MultiIndex n) (hβf_int : ∀ (α : MultiIndex n), α.order ≤ β.order → MeasureTheory.Integrable (fun (x : Fin n → ℝ) => multiIndexMonomial (fun (i : Fin n) => ↑(x i)) α * f x) MeasureTheory.volume) (ξ : Fin n → ℝ) : multiIndexDeriv β (fourierTransformND n f) ξ = fourierTransformND n (fun (x : Fin n → ℝ) => multiIndexMonomial (fun (i : Fin n) => ↑(-2 * Real.pi) * Complex.I * ↑(x i)) β * f x) ξ

Multi-index version of Theorem 2.1 (2.0.19e): if all moments $x^{\vec{\alpha}} f$ with $|\vec{\alpha}| \le |\vec{\beta}|$ are in $L^1$, then $\partial_{\vec{\beta}}\hat{f}(\xi) = [(-2\pi i x)^{\vec{\beta}} f(x)]^{\wedge}(\xi)$.

theorem FourierAnalysis.ft_contDiff_of_moments_integrableND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (β : MultiIndex n) (hβf_int : ∀ (α : MultiIndex n), α.order ≤ β.order → MeasureTheory.Integrable (fun (x : Fin n → ℝ) => multiIndexMonomial (fun (i : Fin n) => ↑(x i)) α * f x) MeasureTheory.volume) : ContDiff ℝ (↑β.order) (fourierTransformND n f)

Smoothness consequence of Theorem 2.1 (2.0.19e): if $x^{\vec{\alpha}} f \in L^1$ for all $|\vec{\alpha}| \le |\vec{\beta}|$ then $\hat{f} \in C^{|\vec{\beta}|}$.

theorem FourierAnalysis.multiIndexMonomial_mul_smooth_compact {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (β : MultiIndex n) : (ContDiff ℝ ↑⊤ fun (x : Fin n → ℝ) => multiIndexMonomial (fun (i : Fin n) => ↑(-2 * Real.pi) * Complex.I * ↑(x i)) β * f x) ∧ HasCompactSupport fun (x : Fin n → ℝ) => multiIndexMonomial (fun (i : Fin n) => ↑(-2 * Real.pi) * Complex.I * ↑(x i)) β * f x

Multiplying a smooth compactly supported function by a polynomial monomial $(-2\pi i x)^{\vec{\beta}}$ keeps it smooth and compactly supported.

theorem FourierAnalysis.fourierTransformND_partialDeriv {n : ℕ} (g : (Fin n → ℝ) → ℂ) (j : Fin n) (ξ : Fin n → ℝ) (hg_diff : Differentiable ℝ g) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) (hg'_int : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => deriv (fun (t : ℝ) => g (Function.update x j t)) (x j)) MeasureTheory.volume) (hg_decay : Filter.Tendsto g (Filter.cocompact (Fin n → ℝ)) (nhds 0)) : fourierTransformND n (fun (x : Fin n → ℝ) => deriv (fun (t : ℝ) => g (Function.update x j t)) (x j)) ξ = ↑(2 * Real.pi) * Complex.I * ↑(ξ j) * fourierTransformND n g ξ

Single partial derivative version of Theorem 2.1 (2.0.19f): $(\partial_j g)^{\wedge}(\xi) = 2\pi i\, \xi_j\, \hat{g}(\xi)$, when g is differentiable, integrable, has integrable partial derivative, and vanishes at infinity.

theorem FourierAnalysis.iteratedPartialDeriv_succ_apply {n : ℕ} (j : Fin n) (k : ℕ) (g : (Fin n → ℝ) → ℂ) : iteratedPartialDeriv j (k + 1) g = fun (x : Fin n → ℝ) => deriv (fun (t : ℝ) => iteratedPartialDeriv j k g (Function.update x j t)) (x j)

Unfolding equation for iteratedPartialDeriv: $\partial_j^{k+1} g$ is the one-variable derivative along the $j$-th axis of $\partial_j^k g$.

theorem FourierAnalysis.partialDeriv_eq_fderiv_apply {n : ℕ} (f : (Fin n → ℝ) → ℂ) (j : Fin n) (hf : Differentiable ℝ f) : (fun (x : Fin n → ℝ) => deriv (fun (t : ℝ) => f (Function.update x j t)) (x j)) = fun (x : Fin n → ℝ) => (fderiv ℝ f x) (Pi.single j 1)

The one-variable derivative along the $j$-th axis equals the Fréchet derivative applied to the standard basis vector $e_j$.

theorem FourierAnalysis.contDiff_partialDeriv {n : ℕ} (f : (Fin n → ℝ) → ℂ) (j : Fin n) (m : ℕ) (hf : ContDiff ℝ (↑(m + 1)) f) : ContDiff ℝ ↑m fun (x : Fin n → ℝ) => deriv (fun (t : ℝ) => f (Function.update x j t)) (x j)

If f is $C^{m+1}$ then its partial derivative along the $j$-th axis is $C^m$.

theorem FourierAnalysis.contDiff_iteratedPartialDeriv {n : ℕ} (j : Fin n) (k : ℕ) (g : (Fin n → ℝ) → ℂ) (m : ℕ) (hg : ContDiff ℝ (↑(k + m)) g) : ContDiff ℝ (↑m) (iteratedPartialDeriv j k g)

If g is $C^{k+m}$ then $\partial_j^k g$ is $C^m$.

theorem FourierAnalysis.iteratedPartialDeriv_differentiable {n : ℕ} (j : Fin n) (k : ℕ) (g : (Fin n → ℝ) → ℂ) (hg : ContDiff ℝ (↑(k + 1)) g) : Differentiable ℝ (iteratedPartialDeriv j k g)

If g is $C^{k+1}$ then $\partial_j^k g$ is differentiable.

theorem FourierAnalysis.fourierTransformND_iteratedPartialDeriv {n : ℕ} (g : (Fin n → ℝ) → ℂ) (j : Fin n) (k : ℕ) (ξ : Fin n → ℝ) (hg_smooth : ContDiff ℝ (↑k) g) (hg_deriv_int : ∀ m ≤ k, MeasureTheory.Integrable (iteratedPartialDeriv j m g) MeasureTheory.volume) (hg_deriv_decay : ∀ m ≤ k - 1, Filter.Tendsto (iteratedPartialDeriv j m g) (Filter.cocompact (Fin n → ℝ)) (nhds 0)) : fourierTransformND n (iteratedPartialDeriv j k g) ξ = (↑(2 * Real.pi) * Complex.I * ↑(ξ j)) ^ k * fourierTransformND n g ξ

Iterated partial derivative version of Theorem 2.1 (2.0.19f): $(\partial_j^k g)^{\wedge}(\xi) = (2\pi i\, \xi_j)^k\, \hat{g}(\xi)$, under suitable smoothness, integrability and decay hypotheses on g and its lower-order partial derivatives.

theorem FourierAnalysis.ft_of_derivND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (β : MultiIndex n) (hf_smooth : ContDiff ℝ (↑β.order) f) (hf_deriv_int : ∀ (α : MultiIndex n), α.order ≤ β.order → MeasureTheory.Integrable (multiIndexDeriv α f) MeasureTheory.volume) (hf_deriv_decay : ∀ (α : MultiIndex n), α.order ≤ β.order - 1 → Filter.Tendsto (multiIndexDeriv α f) (Filter.cocompact (Fin n → ℝ)) (nhds 0)) (ξ : Fin n → ℝ) : fourierTransformND n (multiIndexDeriv β f) ξ = multiIndexMonomial (fun (i : Fin n) => ↑(2 * Real.pi) * Complex.I * ↑(ξ i)) β * fourierTransformND n f ξ

Multi-index version of Theorem 2.1 (2.0.19f): $(\partial_{\vec{\beta}} f)^{\wedge}(\xi) = (2\pi i\, \xi)^{\vec{\beta}}\, \hat{f}(\xi)$, under smoothness, integrability of $\partial_{\vec{\alpha}} f$ for $|\vec{\alpha}| \le |\vec{\beta}|$, and decay at infinity for $|\vec{\alpha}| \le |\vec{\beta}| - 1$.

theorem FourierAnalysis.fourier_dilationND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (t : ℝ) (ht : t ≠ 0) (ξ : Fin n → ℝ) : fourierTransformND n (fun (x : Fin n → ℝ) => f (t⁻¹ • x)) ξ = ↑(|t| ^ n) * fourierTransformND n f (t • ξ)

$n$-dimensional dilation (Theorem 2.1 (2.0.19c)): if $h(x) = f(t^{-1} x)$ then $\hat{h}(\xi) = |t|^n\, \hat{f}(t \xi)$.

theorem FourierAnalysis.fourier_reverse_conjND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ξ : Fin n → ℝ) : (starRingEnd ℂ) (inverseFourierTransformND n f ξ) = fourierTransformND n (fun (x : Fin n → ℝ) => (starRingEnd ℂ) (f x)) ξ

$n$-dimensional conjugation identity (Theorem 2.1 (2.0.19g), second half): $\overline{f^{\vee}}(\xi) = (\bar{f})^{\wedge}(\xi)$.

theorem FourierAnalysis.fourier_transform_properties {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (t : ℝ) (ht : t ≠ 0) : (∀ (y ξ : Fin n → ℝ), fourierTransformND n (translateFn y f) ξ = Complex.exp (↑(-2 * Real.pi) * Complex.I * ↑(∑ j : Fin n, ξ j * y j)) * fourierTransformND n f ξ) ∧ (∀ (η ξ : Fin n → ℝ), fourierTransformND n (fun (x : Fin n → ℝ) => Complex.exp (↑(2 * Real.pi) * Complex.I * ↑(∑ j : Fin n, η j * x j)) * f x) ξ = fourierTransformND n f (ξ - η)) ∧ (∀ (ξ : Fin n → ℝ), fourierTransformND n (fun (x : Fin n → ℝ) => f (t⁻¹ • x)) ξ = ↑(|t| ^ n) * fourierTransformND n f (t • ξ)) ∧ (∀ (ξ : Fin n → ℝ), MeasureTheory.Integrable (Function.uncurry fun (x y : Fin n → ℝ) => f y * g (x - y) * Complex.exp (↑(-2 * Real.pi) * Complex.I * ↑(∑ j : Fin n, ξ j * x j))) (MeasureTheory.volume.prod MeasureTheory.volume) → fourierTransformND n (complexConvolutionND f g) ξ = fourierTransformND n f ξ * fourierTransformND n g ξ) ∧ (∀ (β : MultiIndex n), (∀ (α : MultiIndex n), α.order ≤ β.order → MeasureTheory.Integrable (fun (x : Fin n → ℝ) => multiIndexMonomial (fun (i : Fin n) => ↑(x i)) α * f x) MeasureTheory.volume) → ContDiff ℝ (↑β.order) (fourierTransformND n f) ∧ ∀ (ξ : Fin n → ℝ), multiIndexDeriv β (fourierTransformND n f) ξ = fourierTransformND n (fun (x : Fin n → ℝ) => multiIndexMonomial (fun (i : Fin n) => ↑(-2 * Real.pi) * Complex.I * ↑(x i)) β * f x) ξ) ∧ (∀ (β : MultiIndex n), ContDiff ℝ (↑β.order) f → (∀ (α : MultiIndex n), α.order ≤ β.order → MeasureTheory.Integrable (multiIndexDeriv α f) MeasureTheory.volume) → (∀ (α : MultiIndex n), α.order ≤ β.order - 1 → Filter.Tendsto (multiIndexDeriv α f) (Filter.cocompact (Fin n → ℝ)) (nhds 0)) → ∀ (ξ : Fin n → ℝ), fourierTransformND n (multiIndexDeriv β f) ξ = multiIndexMonomial (fun (i : Fin n) => ↑(2 * Real.pi) * Complex.I * ↑(ξ i)) β * fourierTransformND n f ξ) ∧ (∀ (ξ : Fin n → ℝ), (starRingEnd ℂ) (fourierTransformND n f ξ) = inverseFourierTransformND n (fun (x : Fin n → ℝ) => (starRingEnd ℂ) (f x)) ξ) ∧ ∀ (ξ : Fin n → ℝ), (starRingEnd ℂ) (inverseFourierTransformND n f ξ) = fourierTransformND n (fun (x : Fin n → ℝ) => (starRingEnd ℂ) (f x)) ξ

Combined statement of the main Fourier transform identities of Theorem 2.1: translation, modulation, dilation, convolution, derivative-versus-multiplication in both directions, and conjugation identities.

theorem FourierAnalysis.fourierTransform_eq_mathlib (f : ℝ → ℂ) : fourierTransform f = FourierTransform.fourier f

Bridge lemma: our 1D fourierTransform agrees with Mathlib's 𝓕.

noncomputable def FourierAnalysis.mulByPoly (f : ℝ → ℂ) (k : ℕ) : ℝ → ℂ

Auxiliary 1D operator: $(\text{mulByPoly}\, f\, k)(x) := (-2\pi i x)^k\, f(x)$.

theorem FourierAnalysis.mulByPoly_zero (f : ℝ → ℂ) : mulByPoly f 0 = f

mulByPoly f 0 = f.

theorem FourierAnalysis.mulByPoly_step (f : ℝ → ℂ) (k : ℕ) : (fun (x : ℝ) => ↑(-2 * Real.pi) * Complex.I * ↑x * mulByPoly f k x) = mulByPoly f (k + 1)

Recursion step: $(-2\pi i x) \cdot (\text{mulByPoly}\, f\, k)(x) = (\text{mulByPoly}\, f\, (k+1))(x)$.

theorem FourierAnalysis.mulByPoly_smooth (f : ℝ → ℂ) (hf : ContDiff ℝ (↑⊤) f) (k : ℕ) : ContDiff ℝ (↑⊤) (mulByPoly f k)

mulByPoly f k is smooth whenever f is smooth.

theorem FourierAnalysis.mulByPoly_compact_support (f : ℝ → ℂ) (hf : HasCompactSupport f) (k : ℕ) : HasCompactSupport (mulByPoly f k)

mulByPoly f k has compact support whenever f does.

theorem FourierAnalysis.mulByPoly_integrable (f : ℝ → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hsupp : HasCompactSupport f) (k : ℕ) : MeasureTheory.Integrable (mulByPoly f k) MeasureTheory.volume

mulByPoly f k is integrable for smooth, compactly supported f.

theorem FourierAnalysis.mulByPoly_x_integrable (f : ℝ → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hsupp : HasCompactSupport f) (k : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => ↑x * mulByPoly f k x) MeasureTheory.volume

$x \cdot (\text{mulByPoly}\, f\, k)(x)$ is integrable for smooth, compactly supported f.

theorem FourierAnalysis.iteratedDeriv_fourierTransform (k : ℕ) (f : ℝ → ℂ) : ContDiff ℝ (↑⊤) f → HasCompactSupport f → iteratedDeriv k (fourierTransform f) = fourierTransform (mulByPoly f k)

For smooth, compactly supported f, the $k$-th derivative of $\hat{f}$ is the Fourier transform of $(-2\pi i x)^k f(x)$ (iterated form of Theorem 2.1 (2.0.19e) in 1D).

theorem FourierAnalysis.schwartz_ft_smooth (f : ℝ → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) : ContDiff ℝ (↑⊤) (fourierTransform f)

For $f \in C_c^{\infty}(\mathbb{R})$, $\hat{f}$ is smooth (part of Proposition 2.0.2 in 1D).

theorem FourierAnalysis.schwartz_rapid_decay_aux (N : ℕ) (f : ℝ → ℂ) : ContDiff ℝ (↑⊤) f → HasCompactSupport f → ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : ℝ), ‖fourierTransform f ξ‖ ≤ C * (1 + |ξ|)⁻¹ ^ N

Auxiliary inductive form of the rapid decay estimate for the 1D Fourier transform: for every $N \in \mathbb{N}$ and $f \in C_c^{\infty}(\mathbb{R})$, there exists $C > 0$ with $|\hat{f}(\xi)| \le C\,(1 + |\xi|)^{-N}$.

theorem FourierAnalysis.schwartz_rapid_decay (f : ℝ → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (N : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : ℝ), ‖fourierTransform f ξ‖ ≤ C * (1 + |ξ|)⁻¹ ^ N

Rapid decay of $\hat{f}$ for $f \in C_c^{\infty}(\mathbb{R})$ (Proposition 2.0.2 in 1D): for every $N$ there exists $C_N > 0$ such that $|\hat{f}(\xi)| \le C_N\,(1 + |\xi|)^{-N}$.

theorem FourierAnalysis.schwartz_rapid_decay_deriv (f : ℝ → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (N k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : ℝ), ‖iteratedDeriv k (fourierTransform f) ξ‖ ≤ C * (1 + |ξ|)⁻¹ ^ N

Rapid decay of the $k$-th derivative of $\hat{f}$ for $f \in C_c^{\infty}(\mathbb{R})$ (derivative form of Proposition 2.0.2 in 1D).

theorem FourierAnalysis.schwartz_decay_of_compact_support (f : ℝ → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) : MeasureTheory.Integrable (fourierTransform f) MeasureTheory.volume

For $f \in C_c^{\infty}(\mathbb{R})$, $\hat{f} \in L^1$ (part of Proposition 2.0.2 in 1D).

theorem FourierAnalysis.fourierTransformND_eq_fourier_bridge_early (n : ℕ) (f : (Fin n → ℝ) → ℂ) (ξ : Fin n → ℝ) : fourierTransformND n f ξ = FourierTransform.fourier (f ∘ WithLp.ofLp) (WithLp.toLp 2 ξ)

Bridge lemma identifying our fourierTransformND with Mathlib's $\mathcal{F}$ via the $L^2$ Euclidean-space identification.

theorem FourierAnalysis.piNorm_le_euclidean {n : ℕ} (ξ : Fin n → ℝ) : ‖ξ‖ ≤ ‖WithLp.toLp 2 ξ‖

The $L^{\infty}$ (sup) norm on $\mathbb{R}^n$ is bounded above by the Euclidean ($L^2$) norm.

theorem FourierAnalysis.schwartz_FT_partial_IBP_bound {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (N : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : Fin n → ℝ), ‖fourierTransformND n f ξ‖ ≤ C * (1 + ‖ξ‖)⁻¹ ^ N

Rapid decay estimate for the $n$-dimensional Fourier transform via the Schwartz seminorm machinery: for $f \in C_c^{\infty}(\mathbb{R}^n)$ and every $N$ there exists $C_N > 0$ with $|\hat{f}(\xi)| \le C_N (1 + \|\xi\|)^{-N}$.

theorem FourierAnalysis.schwartz_rapid_decayND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (N : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : Fin n → ℝ), ‖fourierTransformND n f ξ‖ ≤ C * (1 + ‖ξ‖)⁻¹ ^ N

Rapid decay of $\hat{f}$ for $f \in C_c^{\infty}(\mathbb{R}^n)$ (Proposition 2.0.2): for every $N$ there exists $C_N > 0$ such that $|\hat{f}(\xi)| \le C_N\,(1 + \|\xi\|)^{-N}$.

theorem FourierAnalysis.schwartz_rapid_decay_derivND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (N : ℕ) (β : MultiIndex n) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : Fin n → ℝ), ‖multiIndexDeriv β (fourierTransformND n f) ξ‖ ≤ C * (1 + ‖ξ‖)⁻¹ ^ N

Rapid decay of every derivative $\partial_{\vec{\beta}} \hat{f}$ for $f \in C_c^{\infty}(\mathbb{R}^n)$ (derivative form of Proposition 2.0.2).

theorem FourierAnalysis.schwartz_ft_smoothND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) : ContDiff ℝ (↑⊤) (fourierTransformND n f)

For $f \in C_c^{\infty}(\mathbb{R}^n)$, the Fourier transform $\hat{f}$ is smooth (part of Proposition 2.0.2).

theorem FourierAnalysis.schwartz_decay_of_compact_supportND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) : MeasureTheory.Integrable (fourierTransformND n f) MeasureTheory.volume

For $f \in C_c^{\infty}(\mathbb{R}^n)$, $\hat{f} \in L^1$ (part of Proposition 2.0.2).

theorem FourierAnalysis.fourier_gaussian (a : ℝ) (ha : 0 < a) (ξ : ℝ) : fourierTransform (fun (x : ℝ) => Complex.exp ↑(-Real.pi * a * x ^ 2)) ξ = ↑a ^ (-1 / 2) * Complex.exp ↑(-Real.pi * ξ ^ 2 / a)

1D Gaussian Fourier transform (Proposition 3.0.3, real parameter): $\mathcal{F}\!\left[e^{-\pi a x^2}\right](\xi) = a^{-1/2}\, e^{-\pi \xi^2 / a}$ for $a > 0$.

theorem FourierAnalysis.fourier_gaussian_real_nD {n : ℕ} (a : ℝ) (ha : 0 < a) (ξ : Fin n → ℝ) : fourierTransformND n (fun (x : Fin n → ℝ) => Complex.exp (↑(-Real.pi) * ↑a * ↑(euclidNormSq x))) ξ = ↑a ^ (-↑n / 2) * Complex.exp (↑(-Real.pi) * ↑(euclidNormSq ξ) / ↑a)

$n$-dimensional Gaussian Fourier transform (Proposition 3.0.3, real parameter): $\mathcal{F}\!\left[e^{-\pi a |x|^2}\right](\xi) = a^{-n/2}\, e^{-\pi |\xi|^2 / a}$ for $a > 0$.

theorem FourierAnalysis.fourier_gaussian_complex {n : ℕ} (z : ℂ) (hz : 0 < z.re) (_him : z.im ≠ 0) (ξ : Fin n → ℝ) : fourierTransformND n (fun (x : Fin n → ℝ) => Complex.exp (↑(-Real.pi) * z * ↑(euclidNormSq x))) ξ = z ^ (-↑n / 2) * Complex.exp (↑(-Real.pi) * ↑(euclidNormSq ξ) / z)

$n$-dimensional Gaussian Fourier transform with complex parameter $z = a + ib$ ($a > 0$, $b \ne 0$): $\mathcal{F}\!\left[e^{-\pi z |x|^2}\right](\xi) = z^{-n/2}\, e^{-\pi |\xi|^2 / z}$ (Proposition 3.0.3, complex form).

theorem FourierAnalysis.fourier_integral_swap (f g : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (x : ℝ), fourierTransform f x * g x = ∫ (x : ℝ), f x * fourierTransform g x

Multiplication formula in 1D: $\int_{\mathbb{R}} \hat{f}(x)\, g(x)\, dx = \int_{\mathbb{R}} f(x)\, \hat{g}(x)\, dx$ for $f, g \in L^1$.

theorem FourierAnalysis.fourier_inner_swap (f g : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : complexL2Inner (fourierTransform f) g = complexL2Inner f (inverseFourierTransform g)

1D inner-product swap identity: $\langle \hat{f}, g \rangle = \langle f, g^{\vee} \rangle$ for $f, g \in L^1$.

theorem FourierAnalysis.fourier_L2_inner_product_interaction (f g : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (x : ℝ), fourierTransform f x * g x = ∫ (x : ℝ), f x * fourierTransform g x ∧ complexL2Inner (fourierTransform f) g = complexL2Inner f (inverseFourierTransform g)

Combined 1D multiplication and inner-product swap identities.

theorem FourierAnalysis.fourierTransform_eq_mathlib_fourier (f : ℝ → ℂ) (ξ : ℝ) : fourierTransform f ξ = FourierTransform.fourier f ξ

Pointwise version of the bridge fourierTransform_eq_mathlib.

theorem FourierAnalysis.inverseFourierTransform_eq_mathlib_fourierInv (f : ℝ → ℂ) (x : ℝ) : inverseFourierTransform f x = FourierTransformInv.fourierInv f x

Pointwise bridge: our 1D inverseFourierTransform agrees with Mathlib's 𝓕⁻.

theorem FourierAnalysis.fourier_inversion (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransform f) MeasureTheory.volume) (hf_cont : Continuous f) (x : ℝ) : inverseFourierTransform (fourierTransform f) x = f x

1D Fourier inversion: $(f^{\wedge})^{\vee}(x) = f(x)$ for continuous $f \in L^1$ with $\hat{f} \in L^1$.

theorem FourierAnalysis.fourier_inversion_reverse (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf_check : MeasureTheory.Integrable (inverseFourierTransform f) MeasureTheory.volume) (hf_cont : Continuous f) (x : ℝ) : fourierTransform (inverseFourierTransform f) x = f x

1D reverse Fourier inversion: $(f^{\vee})^{\wedge}(x) = f(x)$ for continuous $f \in L^1$ with $f^{\vee} \in L^1$.

theorem FourierAnalysis.plancherel_ft_memLp (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransform f) MeasureTheory.volume) (hf_cont : Continuous f) : MeasureTheory.MemLp (fourierTransform f) 2 MeasureTheory.volume

1D Plancherel preparation: under integrability and $L^2$ hypotheses for $f$, the Fourier transform $\hat{f}$ also lies in $L^2$.

theorem FourierAnalysis.plancherel (f g : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransform f) MeasureTheory.volume) (hg_hat : MeasureTheory.Integrable (fourierTransform g) MeasureTheory.volume) (hf_cont : Continuous f) (hg_cont : Continuous g) : complexL2Inner (fourierTransform f) (fourierTransform g) = complexL2Inner f g

1D Plancherel/Parseval identity: $\langle \hat{f}, \hat{g} \rangle = \langle f, g \rangle$ under suitable integrability, $L^2$, and continuity hypotheses on $f$ and $g$.

theorem FourierAnalysis.plancherel_norm (f : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransform f) MeasureTheory.volume) (hf_cont : Continuous f) : complexL2Inner (fourierTransform f) (fourierTransform f) = complexL2Inner f f

1D Plancherel norm identity: $\|\hat{f}\|_{L^2}^2 = \|f\|_{L^2}^2$.

theorem FourierAnalysis.fourierTransformND_eq_fourier_bridge (n : ℕ) (f : (Fin n → ℝ) → ℂ) (ξ : Fin n → ℝ) : fourierTransformND n f ξ = FourierTransform.fourier (f ∘ WithLp.ofLp) (WithLp.toLp 2 ξ)

Bridge identifying our $n$-dimensional fourierTransformND with Mathlib's $\mathcal{F}$ on the Euclidean space, via the $L^2$ identification.

theorem FourierAnalysis.inverseFourierTransformND_eq_fourierInv_bridge (n : ℕ) (g : (Fin n → ℝ) → ℂ) (x : Fin n → ℝ) : inverseFourierTransformND n g x = FourierTransformInv.fourierInv (g ∘ WithLp.ofLp) (WithLp.toLp 2 x)

Bridge identifying our $n$-dimensional inverseFourierTransformND with Mathlib's 𝓕⁻ on the Euclidean space.

theorem FourierAnalysis.fourier_inversionND (n : ℕ) (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransformND n f) MeasureTheory.volume) (hf_cont : Continuous f) (x : Fin n → ℝ) : inverseFourierTransformND n (fourierTransformND n f) x = f x

$n$-dimensional Fourier inversion: $(\hat{f})^{\vee}(x) = f(x)$ for continuous $f \in L^1$ with $\hat{f} \in L^1$.

theorem FourierAnalysis.fourier_integral_swapND {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (x : Fin n → ℝ), fourierTransformND n f x * g x = ∫ (x : Fin n → ℝ), f x * fourierTransformND n g x

$n$-dimensional multiplication formula: $\int_{\mathbb{R}^n} \hat{f}(x)\, g(x)\, d^n x = \int_{\mathbb{R}^n} f(x)\, \hat{g}(x)\, d^n x$.

theorem FourierAnalysis.fourier_conjND {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ξ : Fin n → ℝ) : (starRingEnd ℂ) (fourierTransformND n f ξ) = inverseFourierTransformND n (fun (x : Fin n → ℝ) => (starRingEnd ℂ) (f x)) ξ

$n$-dimensional conjugation identity (Theorem 2.1 (2.0.19g), first half): $\overline{\hat{f}}(\xi) = (\bar{f})^{\vee}(\xi)$.

theorem FourierAnalysis.fourier_inner_swapND {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) : complexL2InnerND (fourierTransformND n f) g = complexL2InnerND f (inverseFourierTransformND n g)

$n$-dimensional inner-product swap identity: $\langle \hat{f}, g \rangle = \langle f, g^{\vee} \rangle$.

theorem FourierAnalysis.fourierTransformND_bound {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (ξ : Fin n → ℝ) : ‖fourierTransformND n f ξ‖ ≤ ∫ (x : Fin n → ℝ), ‖f x‖

$n$-dimensional pointwise bound (Lemma 2.0.1): $|\hat{f}(\xi)| \le \|f\|_{L^1}$ for $f \in L^1(\mathbb{R}^n)$.

theorem FourierAnalysis.fourierTransformND_continuous {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : Continuous (fourierTransformND n f)

$n$-dimensional continuity of $\hat{f}$ for $f \in L^1(\mathbb{R}^n)$ (Lemma 2.0.1).

theorem FourierAnalysis.fourierTransformND_tendsto_zero {n : ℕ} (f : (Fin n → ℝ) → ℂ) (_hf : MeasureTheory.Integrable f MeasureTheory.volume) : Filter.Tendsto (fourierTransformND n f) (Filter.cocompact (Fin n → ℝ)) (nhds 0)

$n$-dimensional Riemann–Lebesgue: $\hat{f}(\xi) \to 0$ as $|\xi| \to \infty$ for $f \in L^1(\mathbb{R}^n)$.

theorem FourierAnalysis.fourier_L1_properties_nD {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) : (∀ (ξ : Fin n → ℝ), ‖fourierTransformND n f ξ‖ ≤ ∫ (x : Fin n → ℝ), ‖f x‖) ∧ Continuous (fourierTransformND n f) ∧ Filter.Tendsto (fourierTransformND n f) (Filter.cocompact (Fin n → ℝ)) (nhds 0)

$n$-dimensional Lemma 2.0.1 (combined): for $f \in L^1(\mathbb{R}^n)$, $\hat{f}$ is bounded by $\|f\|_{L^1}$, continuous, and tends to $0$ at infinity.

theorem FourierAnalysis.plancherel_ft_memLpND (n : ℕ) (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransformND n f) MeasureTheory.volume) (hf_cont : Continuous f) : MeasureTheory.MemLp (fourierTransformND n f) 2 MeasureTheory.volume

$n$-dimensional Plancherel preparation: under integrability and $L^2$ hypotheses for $f$, the Fourier transform $\hat{f}$ also lies in $L^2$.

theorem FourierAnalysis.plancherelND (n : ℕ) (f g : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransformND n f) MeasureTheory.volume) (hg_hat : MeasureTheory.Integrable (fourierTransformND n g) MeasureTheory.volume) (hf_cont : Continuous f) (hg_cont : Continuous g) : complexL2InnerND (fourierTransformND n f) (fourierTransformND n g) = complexL2InnerND f g

$n$-dimensional Plancherel/Parseval identity: $\langle \hat{f}, \hat{g} \rangle = \langle f, g \rangle$.

theorem FourierAnalysis.plancherel_normND (n : ℕ) (f : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransformND n f) MeasureTheory.volume) (hf_cont : Continuous f) : complexL2InnerND (fourierTransformND n f) (fourierTransformND n f) = complexL2InnerND f f

$n$-dimensional Plancherel norm identity: $\|\hat{f}\|_{L^2}^2 = \|f\|_{L^2}^2$.

theorem FourierAnalysis.plancherel_theorem_full (n : ℕ) (f g : (Fin n → ℝ) → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hf_cont : Continuous f) (hg_cont : Continuous g) (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hf_hat : MeasureTheory.Integrable (fourierTransformND n f) MeasureTheory.volume) (hg_hat : MeasureTheory.Integrable (fourierTransformND n g) MeasureTheory.volume) : MeasureTheory.MemLp (fourierTransformND n f) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (fourierTransformND n g) 2 MeasureTheory.volume ∧ complexL2InnerND (fourierTransformND n f) (fourierTransformND n g) = complexL2InnerND f g ∧ complexL2InnerND (fourierTransformND n f) (fourierTransformND n f) = complexL2InnerND f f

Combined statement of the Plancherel theorem in $n$ dimensions: $\hat{f}, \hat{g} \in L^2$, $\langle \hat{f}, \hat{g} \rangle = \langle f, g \rangle$, and $\|\hat{f}\|_{L^2}^2 = \|f\|_{L^2}^2$.

theorem FourierAnalysis.proposition_2_0_2 {n : ℕ} (f : (Fin n → ℝ) → ℂ) (hf_smooth : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) : ContDiff ℝ (↑⊤) (fourierTransformND n f) ∧ (∀ (N : ℕ), ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : Fin n → ℝ), ‖fourierTransformND n f ξ‖ ≤ C * (1 + ‖ξ‖)⁻¹ ^ N) ∧ (∀ (N : ℕ) (β : MultiIndex n), ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : Fin n → ℝ), ‖multiIndexDeriv β (fourierTransformND n f) ξ‖ ≤ C * (1 + ‖ξ‖)⁻¹ ^ N) ∧ MeasureTheory.Integrable (fourierTransformND n f) MeasureTheory.volume

Proposition 2.0.2: for $f \in C_c^{\infty}(\mathbb{R}^n)$, $\hat{f}$ is smooth, rapidly decaying at infinity together with all its derivatives, and lies in $L^1$.