theorem FourierDistributions.fourierDistrib_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (u : TemperedDistribution V ℂ) (φ : SchwartzMap V ℂ) : (FourierTransform.fourier u) φ = u (FourierTransform.fourier φ)

Defining identity for the Fourier transform of a tempered distribution: (𝓕 u)(φ) = u(𝓕 φ), where the right-hand side uses the Fourier transform on Schwartz functions.

noncomputable def FourierDistributions.fourierTempDistribCLE {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : TemperedDistribution V ℂ ≃L[ℂ] TemperedDistribution V ℂ

The Fourier transform on tempered distributions, packaged as a continuous linear equivalence of 𝓢'(V, ℂ) with itself.

theorem FourierDistributions.fourier_tempDistrib_isomorphism {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : ∃ (e : TemperedDistribution V ℂ ≃L[ℂ] TemperedDistribution V ℂ), (∀ (u : TemperedDistribution V ℂ), e u = FourierTransform.fourier u) ∧ ∀ (u : TemperedDistribution V ℂ), e.symm u = FourierTransformInv.fourierInv u

Existence of the Fourier isomorphism on tempered distributions: there is a continuous linear equivalence 𝓢' ≃L[ℂ] 𝓢' that agrees with 𝓕 on distributions and whose inverse is the inverse Fourier transform 𝓕⁻.

@[simp]

theorem FourierDistributions.fourierTempDistribCLE_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (u : TemperedDistribution V ℂ) : fourierTempDistribCLE u = FourierTransform.fourier u

The Fourier CLE coincides with the standard Fourier transform 𝓕 of tempered distributions.

@[simp]

theorem FourierDistributions.fourierTempDistribCLE_symm_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (u : TemperedDistribution V ℂ) : fourierTempDistribCLE.symm u = FourierTransformInv.fourierInv u

The inverse of the Fourier CLE coincides with the inverse Fourier transform 𝓕⁻ of tempered distributions.

theorem FourierDistributions.fourier_lineDeriv_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (u : TemperedDistribution V ℂ) (m : V) : FourierTransform.fourier (LineDeriv.lineDerivOp m u) = (2 * ↑Real.pi * Complex.I) • (TemperedDistribution.smulLeftCLM ℂ fun (x : V) => ↑(inner ℝ x m)) (FourierTransform.fourier u)

Fourier-derivative exchange (first order): the Fourier transform converts the directional derivative ∂_m u into multiplication by 2πi ⟨·, m⟩ of 𝓕 u.

theorem FourierDistributions.lineDeriv_fourier_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (u : TemperedDistribution V ℂ) (m : V) : LineDeriv.lineDerivOp m (FourierTransform.fourier u) = FourierTransform.fourier (-(2 * ↑Real.pi * Complex.I) • (TemperedDistribution.smulLeftCLM ℂ fun (x : V) => ↑(inner ℝ x m)) u)

Derivative-of-Fourier transform identity: differentiating 𝓕 u in the direction m corresponds to taking the Fourier transform of -2πi ⟨·, m⟩ · u.

def FourierDistributions.iteratedMulOp {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {n : ℕ} : (Fin n → V) → TemperedDistribution V ℂ → TemperedDistribution V ℂ

Iterated multiplication by linear functionals: for a tuple m : Fin n → V, the operator iteratedMulOp m multiplies a tempered distribution by ∏ ⟨·, m i⟩. Defined by recursion.

@[simp]

theorem FourierDistributions.iteratedMulOp_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (m : Fin 0 → V) (u : TemperedDistribution V ℂ) : iteratedMulOp m u = u

The empty iterated multiplication operator is the identity on tempered distributions.

theorem FourierDistributions.fourier_iteratedLineDerivOp_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (u : TemperedDistribution V ℂ) {n : ℕ} (m : Fin n → V) : FourierTransform.fourier (LineDeriv.iteratedLineDerivOp m u) = (2 * ↑Real.pi * Complex.I) ^ n • iteratedMulOp m (FourierTransform.fourier u)

Higher-order Fourier-derivative exchange: for any multi-index m : Fin n → V, 𝓕 (∂^{m} u) = (2πi)^n · iteratedMulOp m (𝓕 u), generalising the first-order identity.

theorem FourierDistributions.iteratedLineDerivOp_fourier_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (u : TemperedDistribution V ℂ) {n : ℕ} (m : Fin n → V) : LineDeriv.iteratedLineDerivOp m (FourierTransform.fourier u) = FourierTransform.fourier ((-(2 * ↑Real.pi * Complex.I)) ^ n • iteratedMulOp m u)

Higher-order multi-derivative-of-Fourier identity: ∂^{m} (𝓕 u) = 𝓕 ((-2πi)^n · iteratedMulOp m u).

theorem FourierDistributions.fourier_tempDistrib_multiindex_exchange {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] : (∃ (e : TemperedDistribution V ℂ ≃L[ℂ] TemperedDistribution V ℂ), (∀ (u : TemperedDistribution V ℂ), e u = FourierTransform.fourier u) ∧ ∀ (u : TemperedDistribution V ℂ), e.symm u = FourierTransformInv.fourierInv u) ∧ (∀ (u : TemperedDistribution V ℂ) {n : ℕ} (m : Fin n → V), FourierTransform.fourier (LineDeriv.iteratedLineDerivOp m u) = (2 * ↑Real.pi * Complex.I) ^ n • iteratedMulOp m (FourierTransform.fourier u)) ∧ ∀ (u : TemperedDistribution V ℂ) {n : ℕ} (m : Fin n → V), LineDeriv.iteratedLineDerivOp m (FourierTransform.fourier u) = FourierTransform.fourier ((-(2 * ↑Real.pi * Complex.I)) ^ n • iteratedMulOp m u)

Packaged statement of the Fourier–tempered-distribution exchange: the Fourier isomorphism on 𝓢' together with the multi-index versions of the differentiation–multiplication correspondence.