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

Fourier inversion theorem (Theorem 4.1), forward direction: for a continuous $f \in L^1(\mathbb{R}^n)$ with $\hat{f} \in L^1$, the inverse Fourier transform of $\hat{f}$ recovers $f$, i.e. $(\hat{f})^\vee = f$.

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

Fourier inversion theorem (Theorem 4.1), reverse direction: for a continuous $f \in L^1(\mathbb{R}^n)$ with $f^\vee \in L^1$, the Fourier transform of $f^\vee$ recovers $f$, i.e. $(f^\vee)^\wedge = f$.

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

Fourier inversion theorem (Theorem 4.1, combined): under the integrability hypotheses, both $(\hat{f})^\vee = f$ and $(f^\vee)^\wedge = f$. That is, the Fourier transform $\wedge$ and its inverse $\vee$ are mutual inverses.