Theorems · Theorem · harmonic analysis

GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace

∀ {b : ℂ} {ι : Type u_2} [inst : Fintype ι],
  0 < b.re →
    ∀ (c : ℂ) (w : EuclideanSpace ℝ ι),
      ∫ (v : EuclideanSpace ℝ ι), Complex.exp (-b * ↑‖v‖ ^ 2 + c * ↑(inner ℝ w v)) =
        (↑Real.pi / b) ^ (↑(Fintype.card ι) / 2) * Complex.exp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Defined in

Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Cited by

1 results in Mathlib

Foundations

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

Assumes

Fintype