# Fourier transform of the Gaussian #

We prove that the Fourier transform of the Gaussian function is another Gaussian:

• integral_cexp_quadratic: general formula for ∫ (x : ℝ), exp (b * x ^ 2 + c * x + d)
• fourierIntegral_gaussian: for all complex b and t with 0 < re b, we have ∫ x:ℝ, exp (I * t * x) * exp (-b * x^2) = (π / b) ^ (1 / 2) * exp (-t ^ 2 / (4 * b)).
• fourierIntegral_gaussian_pi: a variant with b and t scaled to give a more symmetric statement, and formulated in terms of the Fourier transform operator 𝓕.

We also give versions of these formulas in finite-dimensional inner product spaces, see integral_cexp_neg_mul_sq_norm_add and fourierIntegral_gaussian_innerProductSpace.

## Fourier integral of Gaussian functions #

The integral of the Gaussian function over the vertical edges of a rectangle with vertices at (±T, 0) and (±T, c).

Equations
Instances For
theorem GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I (b : ) (c : ) (T : ) :
(-b * (T + ) ^ 2).exp = (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2)).exp

Explicit formula for the norm of the Gaussian function along the vertical edges.

theorem GaussianFourier.norm_cexp_neg_mul_sq_add_mul_I' {b : } (hb : b.re 0) (c : ) (T : ) :
(-b * (T + ) ^ 2).exp = (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re))).exp
theorem GaussianFourier.verticalIntegral_norm_le {b : } (hb : 0 < b.re) (c : ) {T : } (hT : 0 T) :
2 * |c| * (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2)).exp
theorem GaussianFourier.tendsto_verticalIntegral {b : } (hb : 0 < b.re) (c : ) :
Filter.Tendsto Filter.atTop (nhds 0)
theorem GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I {b : } (hb : 0 < b.re) (c : ) :
MeasureTheory.Integrable (fun (x : ) => (-b * (x + ) ^ 2).exp) MeasureTheory.volume
theorem GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I {b : } (hb : 0 < b.re) (c : ) :
∫ (x : ), (-b * (x + ) ^ 2).exp = ( / b) ^ (1 / 2)
theorem integral_cexp_quadratic {b : } (hb : b.re < 0) (c : ) (d : ) :
∫ (x : ), (b * x ^ 2 + c * x + d).exp = () ^ (1 / 2) * (d - c ^ 2 / (4 * b)).exp
theorem integrable_cexp_quadratic' {b : } (hb : b.re < 0) (c : ) (d : ) :
MeasureTheory.Integrable (fun (x : ) => (b * x ^ 2 + c * x + d).exp) MeasureTheory.volume
theorem integrable_cexp_quadratic {b : } (hb : 0 < b.re) (c : ) (d : ) :
MeasureTheory.Integrable (fun (x : ) => (-b * x ^ 2 + c * x + d).exp) MeasureTheory.volume
theorem fourierIntegral_gaussian {b : } (hb : 0 < b.re) (t : ) :
∫ (x : ), ( * x).exp * (-b * x ^ 2).exp = ( / b) ^ (1 / 2) * (-t ^ 2 / (4 * b)).exp
@[deprecated fourierIntegral_gaussian]
theorem fourier_transform_gaussian {b : } (hb : 0 < b.re) (t : ) :
∫ (x : ), ( * x).exp * (-b * x ^ 2).exp = ( / b) ^ (1 / 2) * (-t ^ 2 / (4 * b)).exp

Alias of fourierIntegral_gaussian.

theorem fourierIntegral_gaussian_pi' {b : } (hb : 0 < b.re) (c : ) :
(Real.fourierIntegral fun (x : ) => ( * x ^ 2 + 2 * * c * x).exp) = fun (t : ) => 1 / b ^ (1 / 2) * ( * (t + ) ^ 2).exp
@[deprecated fourierIntegral_gaussian_pi']
theorem fourier_transform_gaussian_pi' {b : } (hb : 0 < b.re) (c : ) :
(Real.fourierIntegral fun (x : ) => ( * x ^ 2 + 2 * * c * x).exp) = fun (t : ) => 1 / b ^ (1 / 2) * ( * (t + ) ^ 2).exp

Alias of fourierIntegral_gaussian_pi'.

theorem fourierIntegral_gaussian_pi {b : } (hb : 0 < b.re) :
(Real.fourierIntegral fun (x : ) => ( * x ^ 2).exp) = fun (t : ) => 1 / b ^ (1 / 2) * ( * t ^ 2).exp
@[deprecated fourierIntegral_gaussian_pi]
theorem GaussianFourier.root_.fourier_transform_gaussian_pi {b : } (hb : 0 < b.re) :
(Real.fourierIntegral fun (x : ) => ( * x ^ 2).exp) = fun (t : ) => 1 / b ^ (1 / 2) * ( * t ^ 2).exp

Alias of fourierIntegral_gaussian_pi.

theorem GaussianFourier.integrable_cexp_neg_sum_mul_add {ι : Type u_2} [] {b : ι} (hb : ∀ (i : ι), 0 < (b i).re) (c : ι) :
MeasureTheory.Integrable (fun (v : ι) => (-i : ι, b i * (v i) ^ 2 + i : ι, c i * (v i)).exp) MeasureTheory.volume
theorem GaussianFourier.integrable_cexp_neg_mul_sum_add {b : } {ι : Type u_2} [] (hb : 0 < b.re) (c : ι) :
MeasureTheory.Integrable (fun (v : ι) => (-b * i : ι, (v i) ^ 2 + i : ι, c i * (v i)).exp) MeasureTheory.volume
theorem GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace {b : } {ι : Type u_2} [] (hb : 0 < b.re) (c : ) (w : ) :
MeasureTheory.Integrable (fun (v : ) => (-b * v ^ 2 + c * w, v⟫_).exp) MeasureTheory.volume
theorem GaussianFourier.integrable_cexp_neg_mul_sq_norm_add {b : } {V : Type u_1} [] [] [] [] (hb : 0 < b.re) (c : ) (w : V) :
MeasureTheory.Integrable (fun (v : V) => (-b * v ^ 2 + c * w, v⟫_).exp) MeasureTheory.volume

In a real inner product space, the complex exponential of minus the square of the norm plus a scalar product is integrable. Useful when discussing the Fourier transform of a Gaussian.

theorem GaussianFourier.integral_cexp_neg_sum_mul_add {ι : Type u_2} [] {b : ι} (hb : ∀ (i : ι), 0 < (b i).re) (c : ι) :
∫ (v : ι), (-i : ι, b i * (v i) ^ 2 + i : ι, c i * (v i)).exp = i : ι, ( / b i) ^ (1 / 2) * (c i ^ 2 / (4 * b i)).exp
theorem GaussianFourier.integral_cexp_neg_mul_sum_add {b : } {ι : Type u_2} [] (hb : 0 < b.re) (c : ι) :
∫ (v : ι), (-b * i : ι, (v i) ^ 2 + i : ι, c i * (v i)).exp = ( / b) ^ (() / 2) * ((i : ι, c i ^ 2) / (4 * b)).exp
theorem GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace {b : } {ι : Type u_2} [] (hb : 0 < b.re) (c : ) (w : ) :
∫ (v : ), (-b * v ^ 2 + c * w, v⟫_).exp = ( / b) ^ (() / 2) * (c ^ 2 * w ^ 2 / (4 * b)).exp
theorem GaussianFourier.integral_cexp_neg_mul_sq_norm_add {b : } {V : Type u_1} [] [] [] [] (hb : 0 < b.re) (c : ) (w : V) :
∫ (v : V), (-b * v ^ 2 + c * w, v⟫_).exp = ( / b) ^ ( / 2) * (c ^ 2 * w ^ 2 / (4 * b)).exp
theorem GaussianFourier.integral_cexp_neg_mul_sq_norm {b : } {V : Type u_1} [] [] [] [] (hb : 0 < b.re) :
∫ (v : V), (-b * v ^ 2).exp = ( / b) ^ ( / 2)
theorem GaussianFourier.integral_rexp_neg_mul_sq_norm {V : Type u_1} [] [] [] [] {b : } (hb : 0 < b) :
∫ (v : V), (-b * v ^ 2).exp = () ^ ( / 2)
theorem fourierIntegral_gaussian_innerProductSpace' {b : } {V : Type u_1} [] [] [] [] (hb : 0 < b.re) (x : V) (w : V) :
Real.fourierIntegral (fun (v : V) => (-b * v ^ 2 + * x, v⟫_).exp) w = ( / b) ^ ( / 2) * (- ^ 2 * x - w ^ 2 / b).exp
theorem fourierIntegral_gaussian_innerProductSpace {b : } {V : Type u_1} [] [] [] [] (hb : 0 < b.re) (w : V) :
Real.fourierIntegral (fun (v : V) => (-b * v ^ 2).exp) w = ( / b) ^ ( / 2) * (- ^ 2 * w ^ 2 / b).exp