Documentation

Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Fourier transform of the Gaussian #

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

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 : ) :
    Complex.exp (-b * (T + c * Complex.I) ^ 2) = Real.exp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))

    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 : ) :
    Complex.exp (-b * (T + c * Complex.I) ^ 2) = Real.exp (-(b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re)))
    theorem GaussianFourier.verticalIntegral_norm_le {b : } (hb : 0 < b.re) (c : ) {T : } (hT : 0 T) :
    GaussianFourier.verticalIntegral b c T 2 * |c| * Real.exp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
    theorem GaussianFourier.integrable_cexp_neg_mul_sq_add_real_mul_I {b : } (hb : 0 < b.re) (c : ) :
    MeasureTheory.Integrable (fun (x : ) => Complex.exp (-b * (x + c * Complex.I) ^ 2)) MeasureTheory.volume
    theorem GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I {b : } (hb : 0 < b.re) (c : ) :
    ∫ (x : ), Complex.exp (-b * (x + c * Complex.I) ^ 2) = (Real.pi / b) ^ (1 / 2)
    theorem integral_cexp_quadratic {b : } (hb : b.re < 0) (c : ) (d : ) :
    ∫ (x : ), Complex.exp (b * x ^ 2 + c * x + d) = (Real.pi / -b) ^ (1 / 2) * Complex.exp (d - c ^ 2 / (4 * b))
    theorem integrable_cexp_quadratic' {b : } (hb : b.re < 0) (c : ) (d : ) :
    MeasureTheory.Integrable (fun (x : ) => Complex.exp (b * x ^ 2 + c * x + d)) MeasureTheory.volume
    theorem integrable_cexp_quadratic {b : } (hb : 0 < b.re) (c : ) (d : ) :
    MeasureTheory.Integrable (fun (x : ) => Complex.exp (-b * x ^ 2 + c * x + d)) MeasureTheory.volume
    theorem fourierIntegral_gaussian {b : } (hb : 0 < b.re) (t : ) :
    ∫ (x : ), Complex.exp (Complex.I * t * x) * Complex.exp (-b * x ^ 2) = (Real.pi / b) ^ (1 / 2) * Complex.exp (-t ^ 2 / (4 * b))
    @[deprecated fourierIntegral_gaussian]
    theorem fourier_transform_gaussian {b : } (hb : 0 < b.re) (t : ) :
    ∫ (x : ), Complex.exp (Complex.I * t * x) * Complex.exp (-b * x ^ 2) = (Real.pi / b) ^ (1 / 2) * Complex.exp (-t ^ 2 / (4 * b))

    Alias of fourierIntegral_gaussian.

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

    Alias of fourierIntegral_gaussian_pi'.

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

    Alias of fourierIntegral_gaussian_pi.

    theorem GaussianFourier.integrable_cexp_neg_sum_mul_add {ι : Type u_2} [Fintype ι] {b : ι} (hb : ∀ (i : ι), 0 < (b i).re) (c : ι) :
    MeasureTheory.Integrable (fun (v : ι) => Complex.exp (-i : ι, b i * (v i) ^ 2 + i : ι, c i * (v i))) MeasureTheory.volume
    theorem GaussianFourier.integrable_cexp_neg_mul_sum_add {b : } {ι : Type u_2} [Fintype ι] (hb : 0 < b.re) (c : ι) :
    MeasureTheory.Integrable (fun (v : ι) => Complex.exp (-b * i : ι, (v i) ^ 2 + i : ι, c i * (v i))) MeasureTheory.volume
    theorem GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace {b : } {ι : Type u_2} [Fintype ι] (hb : 0 < b.re) (c : ) (w : EuclideanSpace ι) :
    MeasureTheory.Integrable (fun (v : EuclideanSpace ι) => Complex.exp (-b * v ^ 2 + c * w, v⟫_)) MeasureTheory.volume
    theorem GaussianFourier.integrable_cexp_neg_mul_sq_norm_add {b : } {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [FiniteDimensional V] [MeasurableSpace V] [BorelSpace V] (hb : 0 < b.re) (c : ) (w : V) :
    MeasureTheory.Integrable (fun (v : V) => Complex.exp (-b * v ^ 2 + c * w, v⟫_)) 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} [Fintype ι] {b : ι} (hb : ∀ (i : ι), 0 < (b i).re) (c : ι) :
    ∫ (v : ι), Complex.exp (-i : ι, b i * (v i) ^ 2 + i : ι, c i * (v i)) = i : ι, (Real.pi / b i) ^ (1 / 2) * Complex.exp (c i ^ 2 / (4 * b i))
    theorem GaussianFourier.integral_cexp_neg_mul_sum_add {b : } {ι : Type u_2} [Fintype ι] (hb : 0 < b.re) (c : ι) :
    ∫ (v : ι), Complex.exp (-b * i : ι, (v i) ^ 2 + i : ι, c i * (v i)) = (Real.pi / b) ^ ((Fintype.card ι) / 2) * Complex.exp ((i : ι, c i ^ 2) / (4 * b))
    theorem GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace {b : } {ι : Type u_2} [Fintype ι] (hb : 0 < b.re) (c : ) (w : EuclideanSpace ι) :
    ∫ (v : EuclideanSpace ι), Complex.exp (-b * v ^ 2 + c * w, v⟫_) = (Real.pi / b) ^ ((Fintype.card ι) / 2) * Complex.exp (c ^ 2 * w ^ 2 / (4 * b))
    theorem GaussianFourier.integral_cexp_neg_mul_sq_norm_add {b : } {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [FiniteDimensional V] [MeasurableSpace V] [BorelSpace V] (hb : 0 < b.re) (c : ) (w : V) :
    ∫ (v : V), Complex.exp (-b * v ^ 2 + c * w, v⟫_) = (Real.pi / b) ^ ((FiniteDimensional.finrank V) / 2) * Complex.exp (c ^ 2 * w ^ 2 / (4 * b))
    theorem fourierIntegral_gaussian_innerProductSpace' {b : } {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace V] [FiniteDimensional V] [MeasurableSpace V] [BorelSpace V] (hb : 0 < b.re) (x : V) (w : V) :
    Real.fourierIntegral (fun (v : V) => Complex.exp (-b * v ^ 2 + 2 * Real.pi * Complex.I * x, v⟫_)) w = (Real.pi / b) ^ ((FiniteDimensional.finrank V) / 2) * Complex.exp (-Real.pi ^ 2 * x - w ^ 2 / b)