Theorems · Theorem · harmonic analysis

GaussianFourier.integrable_cexp_neg_mul_sq_norm_add

∀ {b : ℂ} {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V],
  0 < b.re →
    ∀ (c : ℂ) (w : V),
      MeasureTheory.Integrable (fun v => Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑(inner ℝ 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.

Defined in

Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Cited by

1 results in Mathlib

Foundations

Depth 298 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpace