∀ {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