The Fourier inversion theorem
ProvedFamousTheorems.fourierinv_fourier_eqFourier inversion. If and its Fourier transform are both integrable, then applying the inverse transform to recovers :
The transform loses no information — a function is determined by its frequency content. Both integrability hypotheses are needed for the inverse integral to converge absolutely; without them inversion still holds but must be interpreted in the or distributional sense. This is the theorem that makes Fourier methods a genuine change of representation rather than a one-way summary, and it is why solving a differential equation on the frequency side gives back a solution on the original side. Formalization note. The equality is almost everywhere, and both f and its transform are assumed integrable. The result is Mathlib's MeasureTheory.Integrable.fourierInv_fourier_eq.
import Mathlib
namespace FamousTheorems
universe u_1 u_2 u_3 u_4 u_5 u_6 u_7 u_8 u_9 u_10 u_11 u_12 u_13 u_14 u_15 u_16 u_17 u_18 u_19 u_20 u_21 u_22 u_23 u_24 u_25
open Filter Set Topology DirectSum
theorem fourierinv_fourier_eq :
∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V]
[inst_1 : InnerProductSpace ℝ V] [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V]
[inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace ℂ E] {f : V → E} [CompleteSpace E],
MeasureTheory.Integrable f MeasureTheory.volume →
MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume →
∀ {v : V}, ContinuousAt f v → FourierTransformInv.fourierInv (FourierTransform.fourier f) v = f v := by sorry
end FamousTheorems